Skip to content

Commit

Permalink
Define join for predicate algebra
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahulc29
rahulc29 committed Dec 21, 2023
1 parent 04db06c commit 49be095
Show file tree
Hide file tree
Showing 4 changed files with 199 additions and 17 deletions.
181 changes: 167 additions & 14 deletions src/Realizability/Tripos/Algebra.agda
View file
Original file line number Diff line number Diff line change
@@ -1,22 +1,28 @@
{-# OPTIONS --allow-unsolved-metas #-}
open import Realizability.CombinatoryAlgebra
open import Realizability.Tripos.PosetReflection
open import Realizability.ApplicativeStructure renaming (λ*-naturality to `λ*ComputationRule; λ*-chain to `λ*) hiding (λ*)
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Structure
open import Cubical.Functions.FunExtEquiv
open import Cubical.Data.Fin
open import Cubical.Data.Sum
open import Cubical.Data.Sum renaming (rec to sumRec)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation
open import Cubical.HITs.PropositionalTruncation.Monad
open import Cubical.HITs.SetQuotients renaming (rec to quotRec; rec2 to quotRec2)
open import Cubical.Relation.Binary.Order.Preorder
open import Cubical.Relation.Binary.Order.Poset

module Realizability.Tripos.Algebra {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
open import Realizability.Tripos.Predicate ca

open CombinatoryAlgebra ca
open Realizability.CombinatoryAlgebra.Combinators ca
open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)

λ*ComputationRule = `λ*ComputationRule as fefermanStructure
λ* = `λ* as fefermanStructure
Expand Down Expand Up @@ -60,17 +66,164 @@ module AlgebraicProperties {ℓ' ℓ''} (X : Type ℓ') where
⇒isRightAdjointOf⊓ a b c = hPropExt (isProp≤ (a ⊓ b) c) (isProp≤ a (b ⇒ c)) (a⊓b≤c→a≤b⇒c a b c) (a≤b⇒c→a⊓b≤c a b c)

open Iso
open PreorderStr
open Realizability.Tripos.PosetReflection.Properties _≤_ (preorder≤ .snd .isPreorder)

⊔idempotent→ : ∀ x ϕ a → a ⊩ ∣ ϕ ⊔ ϕ ∣ x → a ⊩ ∣ ϕ ∣ x
⊔idempotent→ x ϕ a a⊩ϕ⊔ϕ =
equivFun (propTruncIdempotent≃ (ϕ .isPropValued x a))
(a⊩ϕ⊔ϕ >>= λ { (inl la⊩ϕx) → {!!} ; (inr ra⊩ϕx) → {!!} })
PredicateAlgebra = PosetReflection _≤_

⊔idempotent : ∀ a → a ⊔ a ≡ a
⊔idempotent a i =
PredicateIsoΣ X .inv
(PredicateΣ≡ {ℓ'' = ℓ''} X
((λ x a' → (a' ⊩ ∣ a ⊔ a ∣ x) , (a ⊔ a) .isPropValued x a') , ((a ⊔ a) .isSetX))
((λ x a' → (a' ⊩ ∣ a ∣ x) , (a .isPropValued x a')) , (a .isSetX))
(funExt₂ (λ x a' → Σ≡Prop (λ x → isPropIsProp {A = x}) (hPropExt isPropPropTrunc (a .isPropValued x a') (⊔idempotent→ x a a') {!!})))
i)
open PreorderReasoning preorder≤

-- ⊔ is commutative upto anti-symmetry
a⊔b→b⊔a : ∀ a b → a ⊔ b ≤ b ⊔ a
a⊔b→b⊔a a b =
do
let prover = ` Id ̇ (` pr₁ ̇ (# fzero)) ̇ (` pair ̇ ` k' ̇ (` pr₂ ̇ (# fzero))) ̇ (` pair ̇ ` k ̇ (` pr₂ ̇ (# fzero)))
let λ*eq = λ (r : A) → λ*ComputationRule prover (r ∷ [])
return
(λ* prover ,
λ x r r⊩a⊔b →
r⊩a⊔b >>=
λ { (inl (pr₁r≡k , pr₂r⊩a)) →
∣ inr ((pr₁ ⨾ (λ* prover ⨾ r)
≡⟨ cong (λ x → pr₁ ⨾ x) (λ*eq r) ⟩
pr₁ ⨾ (Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))
≡⟨ cong (λ x → pr₁ ⨾ (Id ⨾ x ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))) (pr₁r≡k) ⟩
pr₁ ⨾ (Id ⨾ k ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))
≡⟨ cong (λ x → pr₁ ⨾ x) (ifTrueThen _ _) ⟩
pr₁ ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r))
≡⟨ pr₁pxy≡x _ _ ⟩
k'
∎) ,
subst
(λ r → r ⊩ ∣ a ∣ x)
(sym
((pr₂ ⨾ (λ* prover ⨾ r)
≡⟨ cong (λ x → pr₂ ⨾ x) (λ*eq r) ⟩
pr₂ ⨾ (Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))
≡⟨ cong (λ x → pr₂ ⨾ (Id ⨾ x ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))) (pr₁r≡k) ⟩
pr₂ ⨾ (Id ⨾ k ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))
≡⟨ cong (λ x → pr₂ ⨾ x) (ifTrueThen _ _) ⟩
pr₂ ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r))
≡⟨ pr₂pxy≡y _ _ ⟩
pr₂ ⨾ r
∎)))
pr₂r⊩a) ∣₁
; (inr (pr₁r≡k' , pr₂r⊩b)) →
∣ inl (((pr₁ ⨾ (λ* prover ⨾ r)
≡⟨ cong (λ x → pr₁ ⨾ x) (λ*eq r) ⟩
pr₁ ⨾ (Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))
≡⟨ cong (λ x → pr₁ ⨾ (Id ⨾ x ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))) pr₁r≡k' ⟩
pr₁ ⨾ (Id ⨾ k' ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))
≡⟨ cong (λ x → pr₁ ⨾ x) (ifFalseElse _ _) ⟩
pr₁ ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r))
≡⟨ pr₁pxy≡x _ _ ⟩
k
∎) ,
subst
(λ r → r ⊩ ∣ b ∣ x)
(sym
((pr₂ ⨾ (λ* prover ⨾ r)
≡⟨ cong (λ x → pr₂ ⨾ x) (λ*eq r) ⟩
pr₂ ⨾ (Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))
≡⟨ cong (λ x → pr₂ ⨾ (Id ⨾ x ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))) pr₁r≡k' ⟩
pr₂ ⨾ (Id ⨾ k' ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r)))
≡⟨ cong (λ x → pr₂ ⨾ x) (ifFalseElse _ _) ⟩
pr₂ ⨾ (pair ⨾ k ⨾ (pr₂ ⨾ r))
≡⟨ pr₂pxy≡y _ _ ⟩
pr₂ ⨾ r
∎)))
pr₂r⊩b)) ∣₁ })

antiSym→x⊔z≤y⊔z : ∀ x y z → x ≤ y → y ≤ x → (x ⊔ z) ≤ (y ⊔ z)
antiSym→x⊔z≤y⊔z x y z x≤y y≤x =
do
(x⊨y , x⊨yProves) ← x≤y
let prover = ` Id ̇ (` pr₁ ̇ (# fzero)) ̇ (` pair ̇ ` k ̇ (` x⊨y ̇ (` pr₂ ̇ (# fzero)))) ̇ (` pair ̇ ` k' ̇ (` pr₂ ̇ (# fzero)))
return
(λ* prover ,
λ x' a a⊩x⊔zx' →
equivFun
(propTruncIdempotent≃
((y ⊔ z) .isPropValued x' (λ* prover ⨾ a)))
(do
a⊩x⊔z ← a⊩x⊔zx'
return
∣ sumRec
(λ { (pr₁⨾a≡k , pr₂⨾a⊩xx') →
inl
(((pr₁ ⨾ (λ* prover ⨾ a))
≡⟨ cong (λ x → pr₁ ⨾ x) (λ*ComputationRule prover (a ∷ [])) ⟩
(pr₁ ⨾ (Id ⨾ (pr₁ ⨾ a) ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))
≡⟨ cong (λ x → (pr₁ ⨾ (Id ⨾ x ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))) pr₁⨾a≡k ⟩
(pr₁ ⨾ (Id ⨾ k ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))
≡⟨ cong (λ x → pr₁ ⨾ x) (ifTrueThen _ _) ⟩
(pr₁ ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))))
≡⟨ pr₁pxy≡x _ _ ⟩
(k)
∎) ,
subst
(λ r → r ⊩ ∣ y ∣ x')
(sym
(pr₂ ⨾ (λ* prover ⨾ a)
≡⟨ cong (λ x → pr₂ ⨾ x) (λ*ComputationRule prover (a ∷ [])) ⟩
pr₂ ⨾ (Id ⨾ (pr₁ ⨾ a) ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a)))
≡⟨ cong (λ x → (pr₂ ⨾ (Id ⨾ x ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))) pr₁⨾a≡k ⟩
pr₂ ⨾ (Id ⨾ k ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a)))
≡⟨ cong (λ x → pr₂ ⨾ x) (ifTrueThen _ _) ⟩
pr₂ ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a)))
≡⟨ pr₂pxy≡y _ _ ⟩
x⊨y ⨾ (pr₂ ⨾ a)
∎))
(x⊨yProves x' (pr₂ ⨾ a) pr₂⨾a⊩xx')) })
(λ { (pr₁⨾a≡k' , pr₂a⊩zx') →
inr
((((pr₁ ⨾ (λ* prover ⨾ a))
≡⟨ cong (λ x → pr₁ ⨾ x) (λ*ComputationRule prover (a ∷ [])) ⟩
(pr₁ ⨾ (Id ⨾ (pr₁ ⨾ a) ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))
≡⟨ cong (λ x → (pr₁ ⨾ (Id ⨾ x ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))) pr₁⨾a≡k' ⟩
(pr₁ ⨾ (Id ⨾ k' ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))
≡⟨ cong (λ x → pr₁ ⨾ x) (ifFalseElse _ _) ⟩
(pr₁ ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a)))
≡⟨ pr₁pxy≡x _ _ ⟩
(k')
∎)) ,
subst
(λ r → r ⊩ ∣ z ∣ x')
(sym
((pr₂ ⨾ (λ* prover ⨾ a)
≡⟨ cong (λ x → pr₂ ⨾ x) (λ*ComputationRule prover (a ∷ [])) ⟩
pr₂ ⨾ (Id ⨾ (pr₁ ⨾ a) ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a)))
≡⟨ cong (λ x → (pr₂ ⨾ (Id ⨾ x ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))) pr₁⨾a≡k' ⟩
pr₂ ⨾ (Id ⨾ k' ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a)))
≡⟨ cong (λ x → pr₂ ⨾ x) (ifFalseElse _ _) ⟩
pr₂ ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))
≡⟨ pr₂pxy≡y _ _ ⟩
pr₂ ⨾ a
∎)))
pr₂a⊩zx') })
a⊩x⊔z ∣₁))

_l∨_ : PredicateAlgebra → PredicateAlgebra → PredicateAlgebra
a l∨ b =
quotRec2
squash/
(λ x y → [ x ⊔ y ])
(λ x y z (x≤y , y≤x) → eq/ (x ⊔ z) (y ⊔ z) (antiSym→x⊔z≤y⊔z x y z x≤y y≤x , antiSym→x⊔z≤y⊔z y x z y≤x x≤y))
(λ x y z (y≤z , z≤y) →
eq/ (x ⊔ y) (x ⊔ z)
((x ⊔ y
≲⟨ a⊔b→b⊔a x y ⟩
y ⊔ x
≲⟨ antiSym→x⊔z≤y⊔z y z x y≤z z≤y ⟩
z ⊔ x
≲⟨ a⊔b→b⊔a z x ⟩ (
x ⊔ z ◾)) ,
(x ⊔ z
≲⟨ a⊔b→b⊔a x z ⟩
z ⊔ x
≲⟨ antiSym→x⊔z≤y⊔z z y x z≤y y≤z ⟩
y ⊔ x
≲⟨ a⊔b→b⊔a y x ⟩
x ⊔ y
◾)))
a b
2 changes: 2 additions & 0 deletions src/Realizability/Tripos/Everything.agda
View file
Original file line number Diff line number Diff line change
@@ -1,2 +1,4 @@
module Realizability.Tripos.Everything where
open import Realizability.Tripos.Predicate
open import Realizability.Tripos.PosetReflection
open import Realizability.Tripos.Algebra
12 changes: 9 additions & 3 deletions src/Realizability/Tripos/PosetReflection.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ open IsPoset renaming
PosetReflection : {A : Type ℓ} (_≤_ : A → A → Type ℓ') → Type (ℓ-max ℓ ℓ')
PosetReflection {A = A} _≤_ = A / λ x y → x ≤ y × y ≤ x

module _ {A : Type ℓ} (_≤_ : A → A → Type ℓ') (isPreorder : IsPreorder _≤_) where
module Properties {A : Type ℓ} (_≤_ : A → A → Type ℓ') (isPreorder : IsPreorder _≤_) where
_≤ᴿ_ : PosetReflection _≤_ → PosetReflection _≤_ → hProp ℓ'
a ≤ᴿ b =
rec2
Expand Down Expand Up @@ -78,5 +78,11 @@ module _ {A : Type ℓ} (_≤_ : A → A → Type ℓ') (isPreorder : IsPreorder
y
z

isPoset : IsPoset (λ x y → ⟨ x ≤ᴿ y ⟩)
isPoset = isposet squash/ (λ x y → (x ≤ᴿ y) .snd) isRefl≤ᴿ isTrans≤ᴿ isAntisym≤ᴿ
_⊑_ : PosetReflection _≤_ → PosetReflection _≤_ → Type ℓ'
x ⊑ y = ⟨ x ≤ᴿ y ⟩

isPropValued⊑ : ∀ x y → isProp (x ⊑ y)
isPropValued⊑ x y = (x ≤ᴿ y) .snd

poset⊑ : Poset _ _
poset⊑ = poset (PosetReflection _≤_) _⊑_ (isposet squash/ isPropValued⊑ isRefl≤ᴿ isTrans≤ᴿ isAntisym≤ᴿ)
21 changes: 21 additions & 0 deletions src/Realizability/Tripos/Predicate.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,27 @@ isSetPredicate {ℓ'} {ℓ''} X = subst (λ predicateType → isSet predicateTyp
PredicateΣ≡ : ∀ {ℓ' ℓ''} (X : Type ℓ') → (P Q : PredicateΣ {ℓ'' = ℓ''} X) → (P .fst ≡ Q .fst) → P ≡ Q
PredicateΣ≡ X P Q ∣P∣≡∣Q∣ = Σ≡Prop (λ _ → isPropIsSet) ∣P∣≡∣Q∣

Predicate≡ :
∀ {ℓ' ℓ''} (X : Type ℓ')
→ (P Q : Predicate {ℓ'' = ℓ''} X)
→ (∀ x a → a ⊩ ∣ P ∣ x → a ⊩ ∣ Q ∣ x)
→ (∀ x a → a ⊩ ∣ Q ∣ x → a ⊩ ∣ P ∣ x)
-----------------------------------
→ P ≡ Q
Predicate≡ {ℓ'} {ℓ''} X P Q P→Q Q→P i =
PredicateIsoΣ X .inv
(PredicateΣ≡
{ℓ'' = ℓ''}
X
(PredicateIsoΣ X .fun P)
(PredicateIsoΣ X .fun Q)
(funExt₂
(λ x a → Σ≡Prop (λ A → isPropIsProp)
(hPropExt
(P .isPropValued x a)
(Q .isPropValued x a)
(P→Q x a)
(Q→P x a)))) i) where open Iso

module PredicateProperties {ℓ' ℓ''} (X : Type ℓ') where
PredicateX = Predicate {ℓ'' = ℓ''} X
Expand Down

0 comments on commit 49be095

Please sign in to comment.