diff --git a/docs/Realizability.Tripos.Algebra.Base.html b/docs/Realizability.Tripos.Algebra.Base.html
new file mode 100644
index 0000000..e384d25
--- /dev/null
+++ b/docs/Realizability.Tripos.Algebra.Base.html
@@ -0,0 +1,146 @@
+
+Realizability.Tripos.Algebra.Base {-# OPTIONS --allow-unsolved-metas #-}
+open import Realizability.CombinatoryAlgebra
+open import Realizability.Tripos.PosetReflection
+open import Realizability.Tripos.HeytingAlgebra
+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 renaming ( rec to sumRec )
+open import Cubical.Data.Vec
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty renaming ( elim to ⊥elim )
+open import Cubical.Data.Unit
+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
+open import Cubical.Algebra.Lattice
+open import Cubical.Algebra.Semilattice
+open import Cubical.Algebra.CommMonoid
+open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.Semigroup
+
+module Realizability.Tripos.Algebra.Base { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+open import Realizability.Tripos.Prealgebra.Predicate ca
+open import Realizability.Tripos.Prealgebra.Joins.Commutativity ca
+open import Realizability.Tripos.Prealgebra.Joins.Identity ca
+open import Realizability.Tripos.Prealgebra.Joins.Idempotency ca
+open import Realizability.Tripos.Prealgebra.Joins.Associativity ca
+
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+λ* = `λ* as fefermanStructure
+
+module AlgebraicProperties { ℓ' ℓ'' } ( X : Type ℓ' ) ( isSetX' : isSet X ) ( isNonTrivial : s ≡ k → ⊥ ) where
+ PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ open PredicateProperties { ℓ'' = ℓ'' } X
+ open Realizability.Tripos.PosetReflection.Properties _≤_ ( PreorderStr.isPreorder ( preorder≤ . snd ))
+ PredicateAlgebra = PosetReflection _≤_
+ open PreorderReasoning preorder≤
+
+ _∨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 isSetX' x y z x≤y y≤x , antiSym→x⊔z≤y⊔z X isSetX' y x z y≤x x≤y ))
+ (λ x y z ( y≤z , z≤y ) →
+ let
+ I : x ⊔ y ≤ y ⊔ x
+ I = a⊔b→b⊔a X isSetX' x y
+ II : y ⊔ x ≤ z ⊔ x
+ II = antiSym→x⊔z≤y⊔z X isSetX' y z x y≤z z≤y
+ III : z ⊔ x ≤ x ⊔ z
+ III = a⊔b→b⊔a X isSetX' z x
+ IV : x ⊔ z ≤ z ⊔ x
+ IV = a⊔b→b⊔a X isSetX' x z
+ V : z ⊔ x ≤ y ⊔ x
+ V = antiSym→x⊔z≤y⊔z X isSetX' z y x z≤y y≤z
+ VI : y ⊔ x ≤ x ⊔ y
+ VI = a⊔b→b⊔a X isSetX' y x
+ in
+ eq/ ( x ⊔ y ) ( x ⊔ z )
+
+ (( x ⊔ y
+ ≲⟨ I ⟩
+ y ⊔ x
+ ≲⟨ II ⟩
+ z ⊔ x
+ ≲⟨ III ⟩ (
+ x ⊔ z ◾ )) ,
+ ( x ⊔ z
+ ≲⟨ IV ⟩
+ z ⊔ x
+ ≲⟨ V ⟩
+ y ⊔ x
+ ≲⟨ VI ⟩
+ x ⊔ y
+ ◾ )))
+ a b
+
+ open SemigroupStr
+ PredicateAlgebra∨SemigroupStr : SemigroupStr PredicateAlgebra
+ SemigroupStr._·_ PredicateAlgebra∨SemigroupStr = _∨l_
+ IsSemigroup.is-set ( isSemigroup PredicateAlgebra∨SemigroupStr ) = squash/
+ IsSemigroup.·Assoc ( isSemigroup PredicateAlgebra∨SemigroupStr ) x y z =
+ elimProp3
+ (λ x y z → squash/ ( x ∨l ( y ∨l z )) (( x ∨l y ) ∨l z ))
+ (λ x y z →
+ eq/
+ ( x ⊔ ( y ⊔ z )) (( x ⊔ y ) ⊔ z )
+ ( x⊔_y⊔z≤x⊔y_⊔z X isSetX' isNonTrivial x y z ,
+ {!!} ))
+ x y z
+
+ private pre0' = pre0 { ℓ'' = ℓ'' } X isSetX' isNonTrivial
+
+ 0predicate : PredicateAlgebra
+ 0predicate = [ pre0' ]
+
+
+ PredicateAlgebra∨MonoidStr : MonoidStr PredicateAlgebra
+ MonoidStr.ε PredicateAlgebra∨MonoidStr = 0predicate
+ MonoidStr._·_ PredicateAlgebra∨MonoidStr = _∨l_
+ IsMonoid.isSemigroup ( MonoidStr.isMonoid PredicateAlgebra∨MonoidStr ) = PredicateAlgebra∨SemigroupStr . isSemigroup
+ IsMonoid.·IdR ( MonoidStr.isMonoid PredicateAlgebra∨MonoidStr ) x =
+ elimProp
+ (λ x → squash/ ( x ∨l 0predicate ) x )
+ (λ x →
+ eq/
+ ( x ⊔ pre0' ) x
+ (( x⊔0≤x X isSetX' isNonTrivial x ) , x≤x⊔0 X isSetX' isNonTrivial x )) x
+ IsMonoid.·IdL ( MonoidStr.isMonoid PredicateAlgebra∨MonoidStr ) x =
+ elimProp
+ (λ x → squash/ ( 0predicate ∨l x ) x )
+ (λ x →
+ eq/
+ ( pre0' ⊔ x ) x
+ (( 0⊔x≤x X isSetX' isNonTrivial x ) , x≤0⊔x X isSetX' isNonTrivial x )) x
+
+ PredicateAlgebra∨CommMonoidStr : CommMonoidStr PredicateAlgebra
+ CommMonoidStr.ε PredicateAlgebra∨CommMonoidStr = 0predicate
+ CommMonoidStr._·_ PredicateAlgebra∨CommMonoidStr = _∨l_
+ IsCommMonoid.isMonoid ( CommMonoidStr.isCommMonoid PredicateAlgebra∨CommMonoidStr ) = MonoidStr.isMonoid PredicateAlgebra∨MonoidStr
+ IsCommMonoid.·Comm ( CommMonoidStr.isCommMonoid PredicateAlgebra∨CommMonoidStr ) x y =
+ elimProp2 (λ x y → squash/ ( x ∨l y ) ( y ∨l x )) (λ x y → eq/ ( x ⊔ y ) ( y ⊔ x ) (( a⊔b→b⊔a X isSetX' x y ) , ( a⊔b→b⊔a X isSetX' y x ))) x y
+
+ PredicateAlgebra∨SemilatticeStr : SemilatticeStr PredicateAlgebra
+ SemilatticeStr.ε PredicateAlgebra∨SemilatticeStr = 0predicate
+ SemilatticeStr._·_ PredicateAlgebra∨SemilatticeStr = _∨l_
+ IsSemilattice.isCommMonoid ( SemilatticeStr.isSemilattice PredicateAlgebra∨SemilatticeStr ) = CommMonoidStr.isCommMonoid PredicateAlgebra∨CommMonoidStr
+ IsSemilattice.idem ( SemilatticeStr.isSemilattice PredicateAlgebra∨SemilatticeStr ) x =
+ elimProp
+ (λ x → squash/ ( x ∨l x ) x )
+ (λ x → eq/ ( x ⊔ x ) x (( x⊔x≤x X isSetX' isNonTrivial x ) , ( x≤x⊔x X isSetX' isNonTrivial x )))
+ x
+Realizability.Tripos.Everything module Realizability.Tripos.Everything where
open import Realizability.Tripos.Predicate
open import Realizability.Tripos.PosetReflection
-open import Realizability.Tripos.Algebra
+open import Realizability.Tripos.HeytingAlgebra
+open import Realizability.Tripos.Algebra
+open import Realizability.Tripos.Algebra.Base
+open import Realizability.Tripos.Prealgebra.Everything
Realizability.Tripos.Prealgebra.Everything module Realizability.Tripos.Prealgebra.Everything where
+
+open import Realizability.Tripos.Prealgebra.Predicate
+open import Realizability.Tripos.Prealgebra.Joins.Everything
+open import Realizability.Tripos.Prealgebra.Meets.Everything
+open import Realizability.Tripos.Prealgebra.Implication
+Realizability.Tripos.Prealgebra.Implication open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure renaming ( λ*-naturality to `λ*ComputationRule ; λ*-chain to `λ* ) hiding ( λ* )
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Univalence
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.Data.Fin
+open import Cubical.Data.Vec
+
+module Realizability.Tripos.Prealgebra.Implication { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+
+open import Realizability.Tripos.Prealgebra.Predicate ca
+
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+λ* = `λ* as fefermanStructure
+
+module _ { ℓ' ℓ'' } ( X : Type ℓ' ) ( isSetX' : isSet X ) where
+ PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ open PredicateProperties { ℓ'' = ℓ'' } X
+
+ a⊓b≤c→a≤b⇒c : ∀ a b c → ( a ⊓ b ≤ c ) → a ≤ ( b ⇒ c )
+ a⊓b≤c→a≤b⇒c a b c a⊓b≤c =
+ do
+ ( a~ , a~proves ) ← a⊓b≤c
+ let prover = ( ` a~ ̇ ( ` pair ̇ ( # fzero ) ̇ ( # fone )))
+ return
+ ( λ* prover ,
+ λ x aₓ aₓ⊩ax bₓ bₓ⊩bx →
+ subst
+ (λ r → r ⊩ ∣ c ∣ x )
+ ( sym ( λ*ComputationRule prover ( aₓ ∷ bₓ ∷ [] )))
+ ( a~proves
+ x
+ ( pair ⨾ aₓ ⨾ bₓ )
+ (( subst (λ r → r ⊩ ∣ a ∣ x ) ( sym ( pr₁pxy≡x _ _)) aₓ⊩ax ) ,
+ ( subst (λ r → r ⊩ ∣ b ∣ x ) ( sym ( pr₂pxy≡y _ _)) bₓ⊩bx ))))
+
+ a≤b⇒c→a⊓b≤c : ∀ a b c → a ≤ ( b ⇒ c ) → ( a ⊓ b ≤ c )
+ a≤b⇒c→a⊓b≤c a b c a≤b⇒c =
+ do
+ ( a~ , a~proves ) ← a≤b⇒c
+ let prover = ` a~ ̇ ( ` pr₁ ̇ ( # fzero )) ̇ ( ` pr₂ ̇ ( # fzero ))
+ return
+ ( λ* prover ,
+ λ { x abₓ ( pr₁abₓ⊩ax , pr₂abₓ⊩bx ) →
+ subst
+ (λ r → r ⊩ ∣ c ∣ x )
+ ( sym ( λ*ComputationRule prover ( abₓ ∷ [] )))
+ ( a~proves x ( pr₁ ⨾ abₓ ) pr₁abₓ⊩ax ( pr₂ ⨾ abₓ ) pr₂abₓ⊩bx ) })
+
+ ⇒isRightAdjointOf⊓ : ∀ a b c → ( a ⊓ b ≤ c ) ≡ ( a ≤ b ⇒ c )
+ ⇒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 )
+
+ antiSym→a⇒c≤b⇒c : ∀ a b c → a ≤ b → b ≤ a → ( a ⇒ c ) ≤ ( b ⇒ c )
+ antiSym→a⇒c≤b⇒c a b c a≤b b≤a =
+ do
+ ( α , αProves ) ← a≤b
+ ( β , βProves ) ← b≤a
+ let
+ prover : Term as 2
+ prover = ( # fzero ) ̇ ( ` β ̇ # fone )
+ return
+ ( λ* prover ,
+ (λ x r r⊩a⇒c r' r'⊩b →
+ subst
+ (λ witness → witness ⊩ ∣ c ∣ x )
+ ( sym ( λ*ComputationRule prover ( r ∷ r' ∷ [] )))
+ ( r⊩a⇒c ( β ⨾ r' ) ( βProves x r' r'⊩b ))))
+
+ antiSym→a⇒b≤a⇒c : ∀ a b c → b ≤ c → c ≤ b → ( a ⇒ b ) ≤ ( a ⇒ c )
+ antiSym→a⇒b≤a⇒c a b c b≤c c≤b =
+ do
+ ( β , βProves ) ← b≤c
+ ( γ , γProves ) ← c≤b
+ let
+ prover : Term as 2
+ prover = ` β ̇ (( # fzero ) ̇ ( # fone ))
+ return
+ ( λ* prover ,
+ (λ x α α⊩a⇒b a' a'⊩a →
+ subst
+ (λ r → r ⊩ ∣ c ∣ x )
+ ( sym ( λ*ComputationRule prover ( α ∷ a' ∷ [] )))
+ ( βProves x ( α ⨾ a' ) ( α⊩a⇒b a' a'⊩a ))))
+Realizability.Tripos.Prealgebra.Joins.Associativity {-# OPTIONS --allow-unsolved-metas #-}
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Empty renaming ( rec to ⊥rec )
+open import Cubical.Data.Fin
+open import Cubical.Data.Vec
+open import Cubical.Data.Sum
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure renaming ( λ*-naturality to `λ*ComputationRule ; λ*-chain to `λ* ) hiding ( λ* )
+
+module Realizability.Tripos.Prealgebra.Joins.Associativity { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+open import Realizability.Tripos.Prealgebra.Predicate ca
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+private
+ λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+ λ* = `λ* as fefermanStructure
+
+module _ { ℓ' ℓ'' } ( X : Type ℓ' ) ( isSetX' : isSet X ) ( isNonTrivial : s ≡ k → ⊥ ) where
+ private PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ open PredicateProperties { ℓ'' = ℓ'' } X
+
+ module →⊔Assoc ( x y z : Predicate { ℓ'' = ℓ'' } X ) where
+ →proverTerm : Term as 1
+ →proverTerm =
+ ` Id ̇
+ ( ` pr₁ ̇ ( # fzero )) ̇
+ ( ` pair ̇ ` true ̇ ( ` pair ̇ ` true ̇ ( ` pr₂ ̇ ( # fzero )))) ̇
+ ( ` Id ̇
+ ( ` pr₁ ̇ ( ` pr₂ ̇ ( # fzero ))) ̇
+ ( ` pair ̇ ` true ̇ ( ` pair ̇ ` false ̇ ( ` pr₂ ̇ ( ` pr₂ ̇ # fzero )))) ̇
+ ( ` pair ̇ ` false ̇ ( ` pr₂ ̇ ( ` pr₂ ̇ # fzero ))))
+
+ →prover = λ* →proverTerm
+
+ module Pr₁a≡true
+ ( a : A )
+ ( pr₁a≡true : pr₁ ⨾ a ≡ true ) where
+
+ private proof = →prover ⨾ a
+
+ proof≡pair⨾true⨾pair⨾true⨾pr₂a : proof ≡ pair ⨾ true ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))
+ proof≡pair⨾true⨾pair⨾true⨾pr₂a =
+ proof
+ ≡⟨ λ*ComputationRule →proverTerm ( a ∷ [] ) ⟩
+ ( Id ⨾
+ ( pr₁ ⨾ a ) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))) ⨾
+ ( Id ⨾
+ ( pr₁ ⨾ ( pr₂ ⨾ a )) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))))
+ ≡⟨ cong (λ x →
+ ( Id ⨾
+ x ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))) ⨾
+ ( Id ⨾
+ ( pr₁ ⨾ ( pr₂ ⨾ a )) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a ))))))
+ pr₁a≡true ⟩
+ ( Id ⨾
+ k ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))) ⨾
+ ( Id ⨾
+ ( pr₁ ⨾ ( pr₂ ⨾ a )) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))))
+ ≡⟨ ifTrueThen _ _ ⟩
+ pair ⨾ true ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))
+ ∎
+
+ pr₁⨾proof≡true : pr₁ ⨾ ( →prover ⨾ a ) ≡ true
+ pr₁⨾proof≡true =
+ ( pr₁ ⨾ ( →prover ⨾ a ))
+ ≡⟨ cong (λ x → pr₁ ⨾ x ) proof≡pair⨾true⨾pair⨾true⨾pr₂a ⟩
+ pr₁ ⨾ ( pair ⨾ true ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ pr₁pxy≡x _ _ ⟩
+ true
+ ∎
+
+ pr₁pr₂proof≡true : pr₁ ⨾ ( pr₂ ⨾ ( →prover ⨾ a )) ≡ true
+ pr₁pr₂proof≡true =
+ pr₁ ⨾ ( pr₂ ⨾ proof )
+ ≡⟨ cong (λ x → pr₁ ⨾ ( pr₂ ⨾ x )) proof≡pair⨾true⨾pair⨾true⨾pr₂a ⟩
+ pr₁ ⨾ ( pr₂ ⨾ ( pair ⨾ true ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))))
+ ≡⟨ cong (λ x → pr₁ ⨾ x ) ( pr₂pxy≡y _ _) ⟩
+ pr₁ ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))
+ ≡⟨ pr₁pxy≡x _ _ ⟩
+ true
+ ∎
+
+ pr₂pr₂proof≡pr₂a : pr₂ ⨾ ( pr₂ ⨾ proof ) ≡ pr₂ ⨾ a
+ pr₂pr₂proof≡pr₂a =
+ pr₂ ⨾ ( pr₂ ⨾ proof )
+ ≡⟨ cong (λ x → pr₂ ⨾ ( pr₂ ⨾ x )) proof≡pair⨾true⨾pair⨾true⨾pr₂a ⟩
+ pr₂ ⨾ ( pr₂ ⨾ ( pair ⨾ true ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))))
+ ≡⟨ cong (λ x → pr₂ ⨾ x ) ( pr₂pxy≡y _ _) ⟩
+ pr₂ ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))
+ ≡⟨ pr₂pxy≡y _ _ ⟩
+ pr₂ ⨾ a
+ ∎
+
+ module Pr₁a≡false
+ ( a : A )
+ ( pr₁a≡false : pr₁ ⨾ a ≡ false ) where
+ private proof = →prover ⨾ a
+ proof≡y⊔z : proof ≡ ( Id ⨾
+ ( pr₁ ⨾ ( pr₂ ⨾ a )) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a ))))
+ proof≡y⊔z =
+ proof
+ ≡⟨ λ*ComputationRule →proverTerm ( a ∷ [] ) ⟩
+ ( Id ⨾
+ ( pr₁ ⨾ a ) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))) ⨾
+ ( Id ⨾
+ ( pr₁ ⨾ ( pr₂ ⨾ a )) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))))
+ ≡⟨ cong (λ x →
+ ( Id ⨾
+ x ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))) ⨾
+ ( Id ⨾
+ ( pr₁ ⨾ ( pr₂ ⨾ a )) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a ))))))
+ pr₁a≡false ⟩
+ ( Id ⨾
+ k' ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ true ⨾ ( pr₂ ⨾ a ))) ⨾
+ ( Id ⨾
+ ( pr₁ ⨾ ( pr₂ ⨾ a )) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))))
+ ≡⟨ ifFalseElse _ _ ⟩
+ ( Id ⨾
+ ( pr₁ ⨾ ( pr₂ ⨾ a )) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a ))))
+ ∎
+
+ module _ ( pr₁pr₂a≡true : pr₁ ⨾ ( pr₂ ⨾ a ) ≡ true ) where
+ proof≡pair⨾true⨾pair⨾false⨾pr₂⨾pr₂⨾a : proof ≡ pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))
+ proof≡pair⨾true⨾pair⨾false⨾pr₂⨾pr₂⨾a =
+ proof
+ ≡⟨ proof≡y⊔z ⟩
+ Id ⨾
+ ( pr₁ ⨾ ( pr₂ ⨾ a )) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ cong
+ (λ x → ( Id ⨾
+ x ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))))
+ pr₁pr₂a≡true ⟩
+ Id ⨾ true ⨾ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ ifTrueThen _ _ ⟩
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a ))))
+ ∎
+
+ pr₁proof≡true : pr₁ ⨾ proof ≡ true
+ pr₁proof≡true =
+ pr₁ ⨾ proof
+ ≡⟨ cong (λ x → pr₁ ⨾ x ) proof≡pair⨾true⨾pair⨾false⨾pr₂⨾pr₂⨾a ⟩
+ pr₁ ⨾ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a ))))
+ ≡⟨ pr₁pxy≡x _ _ ⟩
+ true
+ ∎
+
+ pr₁pr₂proof≡k' : pr₁ ⨾ ( pr₂ ⨾ proof ) ≡ k'
+ pr₁pr₂proof≡k' =
+ pr₁ ⨾ ( pr₂ ⨾ proof )
+ ≡⟨ cong (λ x → pr₁ ⨾ ( pr₂ ⨾ x )) proof≡pair⨾true⨾pair⨾false⨾pr₂⨾pr₂⨾a ⟩
+ pr₁ ⨾ ( pr₂ ⨾ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))))
+ ≡⟨ cong (λ x → pr₁ ⨾ x ) ( pr₂pxy≡y _ _) ⟩
+ pr₁ ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ pr₁pxy≡x _ _ ⟩
+ false
+ ∎
+
+
+ pr₂pr₂proof≡pr₂pr₂a : pr₂ ⨾ ( pr₂ ⨾ proof ) ≡ pr₂ ⨾ ( pr₂ ⨾ a )
+ pr₂pr₂proof≡pr₂pr₂a =
+ pr₂ ⨾ ( pr₂ ⨾ proof )
+ ≡⟨ cong (λ x → pr₂ ⨾ ( pr₂ ⨾ x )) proof≡pair⨾true⨾pair⨾false⨾pr₂⨾pr₂⨾a ⟩
+ pr₂ ⨾ ( pr₂ ⨾ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))))
+ ≡⟨ cong (λ x → pr₂ ⨾ x ) ( pr₂pxy≡y _ _) ⟩
+ pr₂ ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ pr₂pxy≡y _ _ ⟩
+ pr₂ ⨾ ( pr₂ ⨾ a )
+ ∎
+
+ module _ ( pr₁pr₂a≡false : pr₁ ⨾ ( pr₂ ⨾ a ) ≡ false ) where
+
+ proof≡pair⨾false⨾pr₂pr₂a : proof ≡ pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a ))
+ proof≡pair⨾false⨾pr₂pr₂a =
+ proof
+ ≡⟨ proof≡y⊔z ⟩
+ Id ⨾
+ ( pr₁ ⨾ ( pr₂ ⨾ a )) ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ cong
+ (λ x →
+ Id ⨾
+ x ⨾
+ ( pair ⨾ true ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))) ⨾
+ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a ))))
+ pr₁pr₂a≡false ⟩
+ ifFalseElse _ _
+
+ pr₁proof≡false : pr₁ ⨾ proof ≡ false
+ pr₁proof≡false =
+ pr₁ ⨾ proof
+ ≡⟨ cong (λ x → pr₁ ⨾ x ) proof≡pair⨾false⨾pr₂pr₂a ⟩
+ pr₁ ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ pr₁pxy≡x _ _ ⟩
+ false
+ ∎
+
+ pr₂proof≡pr₂pr₂a : pr₂ ⨾ proof ≡ pr₂ ⨾ ( pr₂ ⨾ a )
+ pr₂proof≡pr₂pr₂a =
+ pr₂ ⨾ proof
+ ≡⟨ cong (λ x → pr₂ ⨾ x ) proof≡pair⨾false⨾pr₂pr₂a ⟩
+ pr₂ ⨾ ( pair ⨾ false ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ pr₂pxy≡y _ _ ⟩
+ pr₂ ⨾ ( pr₂ ⨾ a )
+ ∎
+
+
+ x⊔_y⊔z≤x⊔y_⊔z : ∀ x y z → ( x ⊔ ( y ⊔ z )) ≤ (( x ⊔ y ) ⊔ z )
+ x⊔_y⊔z≤x⊔y_⊔z x y z =
+ ( do
+ let
+
+ prover : Term as 1
+ prover =
+ ` Id ̇
+ ( ` pr₁ ̇ ( # fzero )) ̇
+ ( ` pair ̇ ` true ̇ ( ` pair ̇ ` true ̇ ( ` pr₂ ̇ ( # fzero )))) ̇
+ ( ` Id ̇
+ ( ` pr₁ ̇ ( ` pr₂ ̇ ( # fzero ))) ̇
+ ( ` pair ̇ ` true ̇ ( ` pair ̇ ` false ̇ ( ` pr₂ ̇ ( ` pr₂ ̇ # fzero )))) ̇
+ ( ` pair ̇ ` false ̇ ( ` pr₂ ̇ ( ` pr₂ ̇ # fzero ))))
+ return
+ ( λ* prover ,
+ λ x' a a⊩x⊔_y⊔z →
+ transport
+ ( propTruncIdempotent ((( x ⊔ y ) ⊔ z ) . isPropValued x' ( λ* prover ⨾ a )))
+ ( a⊩x⊔_y⊔z
+ >>= (λ { ( inl ( pr₁a≡true , pr₁a⊩x ))
+ → ∣ ∣ inl
+ ( Pr₁a≡true.pr₁⨾proof≡true a pr₁a≡true ,
+ transport
+ ( propTruncIdempotent isPropPropTrunc )
+ ∣ a⊩x⊔_y⊔z
+ >>= (λ { ( inl ( pr₁a≡k , pr₂a⊩x )) →
+ ∣ inl
+ ( Pr₁a≡true.pr₁pr₂proof≡true a pr₁a≡true ,
+ subst
+ (λ r → r ⊩ ∣ x ∣ x' )
+ ( sym ( Pr₁a≡true.pr₂pr₂proof≡pr₂a a pr₁a≡true ))
+ pr₂a⊩x ) ∣₁
+ ; ( inr ( pr₁a≡k' , pr₂a⊩y⊔z )) → ⊥rec ( Trivial.k≠k' ca isNonTrivial ( k ≡⟨ sym pr₁a≡true ⟩ pr₁ ⨾ a ≡⟨ pr₁a≡k' ⟩ k' ∎ )) }) ∣₁ ) ∣₁ ∣₁
+ ; ( inr ( pr₁a≡false , pr₂a⊩y⊔z ))
+ → ∣ pr₂a⊩y⊔z >>=
+ (λ { ( inl ( pr₁pr₂a≡k , pr₂pr₂a⊩y )) →
+ ∣ inl ( Pr₁a≡false.pr₁proof≡true a pr₁a≡false pr₁pr₂a≡k ,
+ ∣ inr
+ ( Pr₁a≡false.pr₁pr₂proof≡k' a pr₁a≡false pr₁pr₂a≡k ,
+ subst
+ (λ r → r ⊩ ∣ y ∣ x' )
+ ( sym ( Pr₁a≡false.pr₂pr₂proof≡pr₂pr₂a a pr₁a≡false pr₁pr₂a≡k ))
+ pr₂pr₂a⊩y ) ∣₁ ) ∣₁
+ ; ( inr ( pr₁pr₂a≡k' , pr₂pr₂a⊩z )) →
+ ∣ inr (
+ Pr₁a≡false.pr₁proof≡false a pr₁a≡false pr₁pr₂a≡k' ,
+ subst
+ (λ r → r ⊩ ∣ z ∣ x' )
+ ( sym ( Pr₁a≡false.pr₂proof≡pr₂pr₂a a pr₁a≡false pr₁pr₂a≡k' ))
+ pr₂pr₂a⊩z ) ∣₁ }) ∣₁
+ })))) where open →⊔Assoc x y z
+Realizability.Tripos.Prealgebra.Joins.Base open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Data.Unit
+open import Cubical.Data.Fin
+open import Cubical.Data.Vec
+open import Cubical.Data.Sum renaming ( rec to sumRec )
+open import Cubical.Data.Empty renaming ( rec* to ⊥*rec )
+open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.Relation.Binary.Order.Preorder
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure renaming ( λ*-naturality to `λ*ComputationRule ; λ*-chain to `λ* ) hiding ( λ* )
+
+module Realizability.Tripos.Prealgebra.Joins.Base { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+open import Realizability.Tripos.Prealgebra.Predicate ca
+open import Realizability.Tripos.Prealgebra.Joins.Commutativity ca
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+private λ* = `λ* as fefermanStructure
+
+module _ { ℓ' ℓ'' } ( X : Type ℓ' ) ( isSetX' : isSet X ) ( isNonTrivial : s ≡ k → ⊥ ) where
+ PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ open PredicateProperties { ℓ'' = ℓ'' } X
+ 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 ∣₁ ))
+Realizability.Tripos.Prealgebra.Joins.Commutativity open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure renaming ( λ*-naturality to `λ*ComputationRule ; λ*-chain to `λ* ) hiding ( λ* )
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Data.Fin
+open import Cubical.Data.Vec
+open import Cubical.Data.Sum renaming ( rec to sumRec )
+open import Cubical.Relation.Binary.Order.Preorder
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation.Monad
+
+module Realizability.Tripos.Prealgebra.Joins.Commutativity { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+
+open import Realizability.Tripos.Prealgebra.Predicate ca
+
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+private λ* = `λ* as fefermanStructure
+
+module _ { ℓ' ℓ'' } ( X : Type ℓ' ) ( isSetX' : isSet X ) where
+
+ private PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ open PredicateProperties { ℓ'' = ℓ'' } X
+ open PreorderReasoning preorder≤
+
+
+ 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 ∣₁ ))
+Realizability.Tripos.Prealgebra.Joins.Everything module Realizability.Tripos.Prealgebra.Joins.Everything where
+
+open import Realizability.Tripos.Prealgebra.Joins.Base
+open import Realizability.Tripos.Prealgebra.Joins.Identity
+open import Realizability.Tripos.Prealgebra.Joins.Idempotency
+open import Realizability.Tripos.Prealgebra.Joins.Associativity
+open import Realizability.Tripos.Prealgebra.Joins.Commutativity
+Realizability.Tripos.Prealgebra.Joins.Idempotency open import Cubical.Foundations.Prelude
+open import Cubical.Data.Unit
+open import Cubical.Data.Fin
+open import Cubical.Data.Vec
+open import Cubical.Data.Sum
+open import Cubical.Data.Empty renaming ( rec* to ⊥*rec )
+open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.Relation.Binary.Order.Preorder
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure renaming ( λ*-naturality to `λ*ComputationRule ; λ*-chain to `λ* ) hiding ( λ* )
+
+module Realizability.Tripos.Prealgebra.Joins.Idempotency { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+open import Realizability.Tripos.Prealgebra.Predicate ca
+open import Realizability.Tripos.Prealgebra.Joins.Commutativity ca
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+private λ* = `λ* as fefermanStructure
+
+module _ { ℓ' ℓ'' } ( X : Type ℓ' ) ( isSetX' : isSet X ) ( isNonTrivial : s ≡ k → ⊥ ) where
+ private PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ open PredicateProperties { ℓ'' = ℓ'' } X
+
+ x⊔x≤x : ∀ x → x ⊔ x ≤ x
+ x⊔x≤x x =
+ return
+ ( pr₂ ,
+ (λ x' a a⊩x⊔x →
+ transport
+ ( propTruncIdempotent ( x . isPropValued x' ( pr₂ ⨾ a )))
+ ( do
+ a⊩x⊔x ← a⊩x⊔x
+ let
+ goal : (( pr₁ ⨾ a ≡ k ) × ( pr₂ ⨾ a ) ⊩ ∣ x ∣ x' ) ⊎ (( pr₁ ⨾ a ≡ k' ) × ( pr₂ ⨾ a ) ⊩ ∣ x ∣ x' ) → ( pr₂ ⨾ a ) ⊩ ∣ x ∣ x'
+ goal = λ { ( inl (_ , pr₂a⊩x )) → pr₂a⊩x ; ( inr (_ , pr₂a⊩x )) → pr₂a⊩x }
+ return ( goal a⊩x⊔x ))))
+
+ x≤x⊔x : ∀ x → x ≤ x ⊔ x
+ x≤x⊔x x =
+ let prover = ` pair ̇ ` true ̇ # fzero in
+ ∣ λ* prover ,
+ (λ x' a a⊩x →
+ subst
+ (λ r → r ⊩ ∣ x ⊔ x ∣ x' )
+ ( sym ( λ*ComputationRule prover ( a ∷ [] )))
+ ∣ inl ( pr₁pxy≡x _ _ , subst (λ r → r ⊩ ∣ x ∣ x' ) ( sym ( pr₂pxy≡y _ _)) a⊩x ) ∣₁ ) ∣₁
+Realizability.Tripos.Prealgebra.Joins.Identity {-# OPTIONS --allow-unsolved-metas #-}
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Unit
+open import Cubical.Data.Fin
+open import Cubical.Data.Vec
+open import Cubical.Data.Sum
+open import Cubical.Data.Empty renaming ( rec* to ⊥*rec )
+open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.Relation.Binary.Order.Preorder
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure renaming ( λ*-naturality to `λ*ComputationRule ; λ*-chain to `λ* ) hiding ( λ* )
+
+module Realizability.Tripos.Prealgebra.Joins.Identity { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+open import Realizability.Tripos.Prealgebra.Predicate ca
+open import Realizability.Tripos.Prealgebra.Joins.Commutativity ca
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+private λ* = `λ* as fefermanStructure
+
+module _ { ℓ' ℓ'' } ( X : Type ℓ' ) ( isSetX' : isSet X ) ( isNonTrivial : s ≡ k → ⊥ ) where
+ private PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ open PredicateProperties { ℓ'' = ℓ'' } X
+ open PreorderReasoning preorder≤
+
+
+ pre0 : PredicateX
+ Predicate.isSetX pre0 = isSetX'
+ ∣ pre0 ∣ = λ x a → ⊥*
+ Predicate.isPropValued pre0 = λ x a → isProp⊥*
+
+ x⊔0≤x : ∀ x → x ⊔ pre0 ≤ x
+ x⊔0≤x x =
+ do
+ return
+ ( pr₂ ,
+ (λ x' a a⊩x⊔0 →
+ transport
+ ( propTruncIdempotent ( x . isPropValued x' ( pr₂ ⨾ a )))
+ ( do
+ a⊩x⊔0 ← a⊩x⊔0
+ let
+ goal : (( pr₁ ⨾ a ≡ k ) × ( pr₂ ⨾ a ) ⊩ ∣ x ∣ x' ) ⊎ (( pr₁ ⨾ a ≡ k' ) × ⊥* ) → ( pr₂ ⨾ a ) ⊩ ∣ x ∣ x'
+ goal = λ { ( inl ( pr₁a≡k , pr₂a⊩x )) → pr₂a⊩x ; ( inr (_ , bottom )) → ⊥*rec bottom }
+ return ( goal a⊩x⊔0 ))))
+
+ x≤0⊔x : ∀ x → x ≤ ( pre0 ⊔ x )
+ x≤0⊔x x =
+ let
+ proof : Term as 1
+ proof = ` pair ̇ ` false ̇ # fzero
+ in
+ return
+ (( λ* proof ) ,
+ (λ x' a a⊩x →
+ let
+ pr₁proofEq : pr₁ ⨾ ( λ* proof ⨾ a ) ≡ false
+ pr₁proofEq =
+ pr₁ ⨾ ( λ* proof ⨾ a )
+ ≡⟨ cong (λ x → pr₁ ⨾ x ) ( λ*ComputationRule proof ( a ∷ [] )) ⟩
+ pr₁ ⨾ ( pair ⨾ false ⨾ a )
+ ≡⟨ pr₁pxy≡x _ _ ⟩
+ false
+ ∎
+
+ pr₂proofEq : pr₂ ⨾ ( λ* proof ⨾ a ) ≡ a
+ pr₂proofEq =
+ pr₂ ⨾ ( λ* proof ⨾ a )
+ ≡⟨ cong (λ x → pr₂ ⨾ x ) ( λ*ComputationRule proof ( a ∷ [] )) ⟩
+ pr₂ ⨾ ( pair ⨾ false ⨾ a )
+ ≡⟨ pr₂pxy≡y _ _ ⟩
+ a
+ ∎
+ in
+ ∣ inr ( pr₁proofEq , subst (λ r → r ⊩ ∣ x ∣ x' ) ( sym pr₂proofEq ) a⊩x ) ∣₁ ))
+
+ x≤x⊔0 : ∀ x → x ≤ x ⊔ pre0
+ x≤x⊔0 x =
+ let
+ proof : Term as 1
+ proof = ` pair ̇ ` true ̇ # fzero
+ in return
+ (( λ* proof ) ,
+ (λ x' a a⊩x →
+ let
+ pr₁proofEq : pr₁ ⨾ ( λ* proof ⨾ a ) ≡ true
+ pr₁proofEq =
+ pr₁ ⨾ ( λ* proof ⨾ a )
+ ≡⟨ cong (λ x → pr₁ ⨾ x ) ( λ*ComputationRule proof ( a ∷ [] )) ⟩
+ pr₁ ⨾ ( pair ⨾ true ⨾ a )
+ ≡⟨ pr₁pxy≡x _ _ ⟩
+ true
+ ∎
+
+ pr₂proofEq : pr₂ ⨾ ( λ* proof ⨾ a ) ≡ a
+ pr₂proofEq =
+ pr₂ ⨾ ( λ* proof ⨾ a )
+ ≡⟨ cong (λ x → pr₂ ⨾ x ) ( λ*ComputationRule proof ( a ∷ [] )) ⟩
+ pr₂ ⨾ ( pair ⨾ true ⨾ a )
+ ≡⟨ pr₂pxy≡y _ _ ⟩
+ a
+ ∎
+ in
+ ∣ inl ( pr₁proofEq , subst (λ r → r ⊩ ∣ x ∣ x' ) ( sym pr₂proofEq ) a⊩x ) ∣₁ ))
+ 0⊔x≤x : ∀ x → pre0 ⊔ x ≤ x
+ 0⊔x≤x x =
+ pre0 ⊔ x
+ ≲⟨ a⊔b→b⊔a X isSetX' pre0 x ⟩
+ x ⊔ pre0
+ ≲⟨ x⊔0≤x x ⟩
+ x
+ ◾
+
+
+
+
+Realizability.Tripos.Prealgebra.Meets.Associativity open import Cubical.Foundations.Prelude
+open import Cubical.Data.Unit
+open import Cubical.Data.Fin
+open import Cubical.Data.Vec
+open import Cubical.Data.Sum
+open import Cubical.Data.Empty renaming ( rec* to ⊥*rec )
+open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.Relation.Binary.Order.Preorder
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure renaming ( λ*-naturality to `λ*ComputationRule ; λ*-chain to `λ* ) hiding ( λ* )
+
+module Realizability.Tripos.Prealgebra.Meets.Associativity { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+open import Realizability.Tripos.Prealgebra.Predicate ca
+open import Realizability.Tripos.Prealgebra.Joins.Commutativity ca
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+private λ* = `λ* as fefermanStructure
+
+module _ { ℓ' ℓ'' } ( X : Type ℓ' ) ( isSetX' : isSet X ) ( isNonTrivial : s ≡ k → ⊥ ) where
+ PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ open PredicateProperties { ℓ'' = ℓ'' } X
+ open PreorderReasoning preorder≤
+
+ x⊓_y⊓z≤x⊓y_⊓z : ∀ x y z → x ⊓ ( y ⊓ z ) ≤ ( x ⊓ y ) ⊓ z
+ x⊓_y⊓z≤x⊓y_⊓z x y z =
+ let
+ proof : Term as 1
+ proof = ` pair ̇ ( ` pair ̇ ( ` pr₁ ̇ # fzero ) ̇ ( ` pr₁ ̇ ( ` pr₂ ̇ # fzero ))) ̇ ( ` pr₂ ̇ ( ` pr₂ ̇ # fzero ))
+ in
+ return
+ ( λ* proof ,
+ λ x' a a⊩x⊓_y⊓z →
+ let
+ λ*eq = λ*ComputationRule proof ( a ∷ [] )
+
+ pr₁proofEq : pr₁ ⨾ ( λ* proof ⨾ a ) ≡ pair ⨾ ( pr₁ ⨾ a ) ⨾ ( pr₁ ⨾ ( pr₂ ⨾ a ))
+ pr₁proofEq =
+ pr₁ ⨾ ( λ* proof ⨾ a )
+ ≡⟨ cong (λ x → pr₁ ⨾ x ) λ*eq ⟩
+ pr₁ ⨾ ( pair ⨾ ( pair ⨾ ( pr₁ ⨾ a ) ⨾ ( pr₁ ⨾ ( pr₂ ⨾ a ))) ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ pr₁pxy≡x _ _ ⟩
+ pair ⨾ ( pr₁ ⨾ a ) ⨾ ( pr₁ ⨾ ( pr₂ ⨾ a ))
+ ∎
+
+ pr₁pr₁proofEq : pr₁ ⨾ ( pr₁ ⨾ ( λ* proof ⨾ a )) ≡ pr₁ ⨾ a
+ pr₁pr₁proofEq =
+ pr₁ ⨾ ( pr₁ ⨾ ( λ* proof ⨾ a ))
+ ≡⟨ cong (λ x → pr₁ ⨾ x ) pr₁proofEq ⟩
+ pr₁ ⨾ ( pair ⨾ ( pr₁ ⨾ a ) ⨾ ( pr₁ ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ pr₁pxy≡x _ _ ⟩
+ pr₁ ⨾ a
+ ∎
+
+ pr₂pr₁proofEq : pr₂ ⨾ ( pr₁ ⨾ ( λ* proof ⨾ a )) ≡ pr₁ ⨾ ( pr₂ ⨾ a )
+ pr₂pr₁proofEq =
+ pr₂ ⨾ ( pr₁ ⨾ ( λ* proof ⨾ a ))
+ ≡⟨ cong (λ x → pr₂ ⨾ x ) pr₁proofEq ⟩
+ pr₂ ⨾ ( pair ⨾ ( pr₁ ⨾ a ) ⨾ ( pr₁ ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ pr₂pxy≡y _ _ ⟩
+ pr₁ ⨾ ( pr₂ ⨾ a )
+ ∎
+
+ pr₂proofEq : pr₂ ⨾ ( λ* proof ⨾ a ) ≡ pr₂ ⨾ ( pr₂ ⨾ a )
+ pr₂proofEq =
+ pr₂ ⨾ ( λ* proof ⨾ a )
+ ≡⟨ cong (λ x → pr₂ ⨾ x ) λ*eq ⟩
+ pr₂ ⨾ ( pair ⨾ ( pair ⨾ ( pr₁ ⨾ a ) ⨾ ( pr₁ ⨾ ( pr₂ ⨾ a ))) ⨾ ( pr₂ ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ pr₂pxy≡y _ _ ⟩
+ pr₂ ⨾ ( pr₂ ⨾ a )
+ ∎
+ in
+ ( subst (λ r → r ⊩ ∣ x ∣ x' ) ( sym pr₁pr₁proofEq ) ( a⊩x⊓_y⊓z . fst ) ,
+ subst (λ r → r ⊩ ∣ y ∣ x' ) ( sym pr₂pr₁proofEq ) ( a⊩x⊓_y⊓z . snd . fst )) ,
+ subst (λ r → r ⊩ ∣ z ∣ x' ) ( sym pr₂proofEq ) ( a⊩x⊓_y⊓z . snd . snd ))
+
+ x⊓y_⊓z≤x⊓_y⊓z : ∀ x y z → ( x ⊓ y ) ⊓ z ≤ x ⊓ ( y ⊓ z )
+ x⊓y_⊓z≤x⊓_y⊓z x y z =
+ let
+ proof : Term as 1
+ proof = ` pair ̇ ( ` pr₁ ̇ ( ` pr₁ ̇ # fzero )) ̇ ( ` pair ̇ ( ` pr₂ ̇ ( ` pr₁ ̇ # fzero )) ̇ ( ` pr₂ ̇ # fzero ))
+ in
+ return
+ ( λ* proof ,
+ λ { x' a (( pr₁pr₁a⊩x , pr₂pr₁a⊩y ) , pr₂a⊩z ) →
+ let
+ λ*eq = λ*ComputationRule proof ( a ∷ [] )
+
+ pr₂proofEq : pr₂ ⨾ ( λ* proof ⨾ a ) ≡ pair ⨾ ( pr₂ ⨾ ( pr₁ ⨾ a )) ⨾ ( pr₂ ⨾ a )
+ pr₂proofEq =
+ pr₂ ⨾ ( λ* proof ⨾ a )
+ ≡⟨ cong (λ x → pr₂ ⨾ x ) λ*eq ⟩
+ pr₂ ⨾ ( pair ⨾ ( pr₁ ⨾ ( pr₁ ⨾ a )) ⨾ ( pair ⨾ ( pr₂ ⨾ ( pr₁ ⨾ a )) ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ pr₂pxy≡y _ _ ⟩
+ pair ⨾ ( pr₂ ⨾ ( pr₁ ⨾ a )) ⨾ ( pr₂ ⨾ a )
+ ∎
+
+ pr₁proofEq : pr₁ ⨾ ( λ* proof ⨾ a ) ≡ pr₁ ⨾ ( pr₁ ⨾ a )
+ pr₁proofEq =
+ pr₁ ⨾ ( λ* proof ⨾ a )
+ ≡⟨ cong (λ x → pr₁ ⨾ x ) λ*eq ⟩
+ pr₁ ⨾ ( pair ⨾ ( pr₁ ⨾ ( pr₁ ⨾ a )) ⨾ ( pair ⨾ ( pr₂ ⨾ ( pr₁ ⨾ a )) ⨾ ( pr₂ ⨾ a )))
+ ≡⟨ pr₁pxy≡x _ _ ⟩
+ pr₁ ⨾ ( pr₁ ⨾ a )
+ ∎
+
+ pr₁pr₂proofEq : pr₁ ⨾ ( pr₂ ⨾ ( λ* proof ⨾ a )) ≡ pr₂ ⨾ ( pr₁ ⨾ a )
+ pr₁pr₂proofEq =
+ pr₁ ⨾ ( pr₂ ⨾ ( λ* proof ⨾ a ))
+ ≡⟨ cong (λ x → pr₁ ⨾ x ) pr₂proofEq ⟩
+ pr₁ ⨾ ( pair ⨾ ( pr₂ ⨾ ( pr₁ ⨾ a )) ⨾ ( pr₂ ⨾ a ))
+ ≡⟨ pr₁pxy≡x _ _ ⟩
+ pr₂ ⨾ ( pr₁ ⨾ a )
+ ∎
+
+ pr₂pr₂proofEq : pr₂ ⨾ ( pr₂ ⨾ ( λ* proof ⨾ a )) ≡ pr₂ ⨾ a
+ pr₂pr₂proofEq =
+ pr₂ ⨾ ( pr₂ ⨾ ( λ* proof ⨾ a ))
+ ≡⟨ cong (λ x → pr₂ ⨾ x ) pr₂proofEq ⟩
+ pr₂ ⨾ ( pair ⨾ ( pr₂ ⨾ ( pr₁ ⨾ a )) ⨾ ( pr₂ ⨾ a ))
+ ≡⟨ pr₂pxy≡y _ _ ⟩
+ pr₂ ⨾ a
+ ∎
+
+ in
+ subst (λ r → r ⊩ ∣ x ∣ x' ) ( sym pr₁proofEq ) pr₁pr₁a⊩x ,
+ subst (λ r → r ⊩ ∣ y ∣ x' ) ( sym pr₁pr₂proofEq ) pr₂pr₁a⊩y ,
+ subst (λ r → r ⊩ ∣ z ∣ x' ) ( sym pr₂pr₂proofEq ) pr₂a⊩z })
+
+
+Realizability.Tripos.Prealgebra.Meets.Commutativity open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure renaming ( λ*-naturality to `λ*ComputationRule ; λ*-chain to `λ* ) hiding ( λ* )
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Data.Fin
+open import Cubical.Data.Vec
+open import Cubical.Data.Sum renaming ( rec to sumRec )
+open import Cubical.Relation.Binary.Order.Preorder
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation.Monad
+
+module Realizability.Tripos.Prealgebra.Meets.Commutativity { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+
+open import Realizability.Tripos.Prealgebra.Predicate ca
+
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+private λ* = `λ* as fefermanStructure
+
+module _ { ℓ' ℓ'' } ( X : Type ℓ' ) ( isSetX' : isSet X ) where
+
+ private PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ open PredicateProperties { ℓ'' = ℓ'' } X
+ open PreorderReasoning preorder≤
+
+ x⊓y≤y⊓x : ∀ x y → x ⊓ y ≤ y ⊓ x
+ x⊓y≤y⊓x x y =
+ do
+ let
+ proof : Term as 1
+ proof = ` pair ̇ ( ` pr₂ ̇ # fzero ) ̇ ( ` pr₁ ̇ # fzero )
+ return
+ ( λ* proof ,
+ (λ x' a a⊩x⊓y →
+ subst
+ (λ r → r ⊩ ∣ y ⊓ x ∣ x' )
+ ( sym ( λ*ComputationRule proof ( a ∷ [] ) ))
+ (( subst (λ r → r ⊩ ∣ y ∣ x' ) ( sym ( pr₁pxy≡x _ _)) ( a⊩x⊓y . snd )) ,
+ ( subst (λ r → r ⊩ ∣ x ∣ x' ) ( sym ( pr₂pxy≡y _ _)) ( a⊩x⊓y . fst )))))
+
+ 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
+ ( f , f⊩x≤y ) ← x≤y
+ ( g , g⊩y≤x ) ← y≤x
+ let
+ proof : Term as 1
+ proof = ` pair ̇ ( ` f ̇ ( ` pr₁ ̇ # fzero )) ̇ ( ` pr₂ ̇ # fzero )
+ return
+ (( λ* proof ) ,
+ (λ x' a a⊩x⊓z →
+ subst
+ (λ r → r ⊩ ∣ y ⊓ z ∣ x' )
+ ( sym ( λ*ComputationRule proof ( a ∷ [] )))
+ (( subst (λ r → r ⊩ ∣ y ∣ x' ) ( sym ( pr₁pxy≡x _ _)) ( f⊩x≤y x' ( pr₁ ⨾ a ) ( a⊩x⊓z . fst ))) ,
+ ( subst (λ r → r ⊩ ∣ z ∣ x' ) ( sym ( pr₂pxy≡y _ _)) ( a⊩x⊓z . snd )))))
+Realizability.Tripos.Prealgebra.Meets.Everything module Realizability.Tripos.Prealgebra.Meets.Everything where
+
+open import Realizability.Tripos.Prealgebra.Meets.Identity
+open import Realizability.Tripos.Prealgebra.Meets.Idempotency
+open import Realizability.Tripos.Prealgebra.Meets.Associativity
+open import Realizability.Tripos.Prealgebra.Meets.Commutativity
+Realizability.Tripos.Prealgebra.Meets.Idempotency open import Cubical.Foundations.Prelude
+open import Cubical.Data.Unit
+open import Cubical.Data.Fin
+open import Cubical.Data.Vec
+open import Cubical.Data.Sum
+open import Cubical.Data.Empty renaming ( rec* to ⊥*rec )
+open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.Relation.Binary.Order.Preorder
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure renaming ( λ*-naturality to `λ*ComputationRule ; λ*-chain to `λ* ) hiding ( λ* )
+
+module Realizability.Tripos.Prealgebra.Meets.Idempotency { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+open import Realizability.Tripos.Prealgebra.Predicate ca
+open import Realizability.Tripos.Prealgebra.Joins.Commutativity ca
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+private λ* = `λ* as fefermanStructure
+
+module _ { ℓ' ℓ'' } ( X : Type ℓ' ) ( isSetX' : isSet X ) ( isNonTrivial : s ≡ k → ⊥ ) where
+ PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ open PredicateProperties { ℓ'' = ℓ'' } X
+ open PreorderReasoning preorder≤
+
+ x⊓x≤x : ∀ x → x ⊓ x ≤ x
+ x⊓x≤x x = return ( pr₁ , (λ x' a a⊩x⊓x → a⊩x⊓x . fst ))
+
+ x≤x⊓x : ∀ x → x ≤ x ⊓ x
+ x≤x⊓x x =
+ let
+ proof : Term as 1
+ proof = ` pair ̇ # fzero ̇ # fzero
+ in
+ return
+ (( λ* proof ) ,
+ (λ x' a a⊩x →
+ let λ*eq = λ*ComputationRule proof ( a ∷ [] ) in
+ ( subst (λ r → r ⊩ ∣ x ∣ x' ) ( sym ( cong (λ x → pr₁ ⨾ x ) λ*eq ∙ pr₁pxy≡x _ _)) a⊩x ) ,
+ subst (λ r → r ⊩ ∣ x ∣ x' ) ( sym ( cong (λ x → pr₂ ⨾ x ) λ*eq ∙ pr₂pxy≡y _ _)) a⊩x ))
+Realizability.Tripos.Prealgebra.Meets.Identity open import Cubical.Foundations.Prelude
+open import Cubical.Data.Unit
+open import Cubical.Data.Fin
+open import Cubical.Data.Vec
+open import Cubical.Data.Sum
+open import Cubical.Data.Empty renaming ( rec* to ⊥*rec )
+open import Cubical.Data.Sigma
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.Relation.Binary.Order.Preorder
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure renaming ( λ*-naturality to `λ*ComputationRule ; λ*-chain to `λ* ) hiding ( λ* )
+
+module Realizability.Tripos.Prealgebra.Meets.Identity { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+open import Realizability.Tripos.Prealgebra.Predicate ca
+open import Realizability.Tripos.Prealgebra.Meets.Commutativity ca
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+private λ*ComputationRule = `λ*ComputationRule as fefermanStructure
+private λ* = `λ* as fefermanStructure
+
+module _ { ℓ' ℓ'' } ( X : Type ℓ' ) ( isSetX' : isSet X ) ( isNonTrivial : s ≡ k → ⊥ ) where
+ PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ open PredicateProperties { ℓ'' = ℓ'' } X
+ open PreorderReasoning preorder≤
+
+ pre1 : PredicateX
+ Predicate.isSetX pre1 = isSetX'
+ Predicate.∣ pre1 ∣ = λ x a → Unit*
+ Predicate.isPropValued pre1 = λ x a → isPropUnit*
+
+ x⊓1≤x : ∀ x → x ⊓ pre1 ≤ x
+ x⊓1≤x x = ∣ pr₁ , (λ x' a a⊩x⊓1 → a⊩x⊓1 . fst ) ∣₁
+
+ x≤x⊓1 : ∀ x → x ≤ x ⊓ pre1
+ x≤x⊓1 x =
+ do
+ let
+ proof : Term as 1
+ proof = ` pair ̇ # fzero ̇ ` true
+ return (( λ* proof ) , (λ x' a a⊩x → subst (λ r → ∣ x ⊓ pre1 ∣ x' r ) ( sym ( λ*ComputationRule proof ( a ∷ [] ))) ( subst (λ r → r ⊩ ∣ x ∣ x' ) ( sym ( pr₁pxy≡x _ _)) a⊩x , tt* )))
+Realizability.Tripos.Prealgebra.Predicate.Base open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure renaming ( ⟦_⟧ to `⟦_⟧ ; λ*-naturality to `λ*ComputationRule ; λ*-chain to `λ* ) hiding ( λ* )
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Sigma
+open import Cubical.Functions.FunExtEquiv
+
+module Realizability.Tripos.Prealgebra.Predicate.Base { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+
+record Predicate { ℓ' ℓ'' } ( X : Type ℓ' ) : Type ( ℓ-max ( ℓ-max ( ℓ-suc ℓ ) ( ℓ-suc ℓ' )) ( ℓ-suc ℓ'' )) where
+ field
+ isSetX : isSet X
+ ∣_∣ : X → A → Type ( ℓ-max ( ℓ-max ℓ ℓ' ) ℓ'' )
+ isPropValued : ∀ x a → isProp ( ∣_∣ x a )
+ infix 25 ∣_∣
+
+open Predicate
+infix 26 _⊩_
+_⊩_ : ∀ { ℓ' } → A → ( A → Type ℓ' ) → Type ℓ'
+a ⊩ ϕ = ϕ a
+
+PredicateΣ : ∀ { ℓ' ℓ'' } → ( X : Type ℓ' ) → Type ( ℓ-max ( ℓ-max ( ℓ-suc ℓ ) ( ℓ-suc ℓ' )) ( ℓ-suc ℓ'' ))
+PredicateΣ { ℓ' } { ℓ'' } X = Σ[ rel ∈ ( X → A → hProp ( ℓ-max ( ℓ-max ℓ ℓ' ) ℓ'' )) ] ( isSet X )
+
+isSetPredicateΣ : ∀ { ℓ' ℓ'' } ( X : Type ℓ' ) → isSet ( PredicateΣ { ℓ'' = ℓ'' } X )
+isSetPredicateΣ X = isSetΣ ( isSetΠ (λ x → isSetΠ λ a → isSetHProp )) λ _ → isProp→isSet isPropIsSet
+
+PredicateIsoΣ : ∀ { ℓ' ℓ'' } ( X : Type ℓ' ) → Iso ( Predicate { ℓ'' = ℓ'' } X ) ( PredicateΣ { ℓ'' = ℓ'' } X )
+PredicateIsoΣ { ℓ' } { ℓ'' } X =
+ iso
+ (λ p → (λ x a → ( a ⊩ ∣ p ∣ x ) , p . isPropValued x a ) , p . isSetX )
+ (λ p → record { isSetX = p . snd ; ∣_∣ = λ x a → p . fst x a . fst ; isPropValued = λ x a → p . fst x a . snd })
+ (λ b → refl )
+ λ a → refl
+
+Predicate≡PredicateΣ : ∀ { ℓ' ℓ'' } ( X : Type ℓ' ) → Predicate { ℓ'' = ℓ'' } X ≡ PredicateΣ { ℓ'' = ℓ'' } X
+Predicate≡PredicateΣ { ℓ' } { ℓ'' } X = isoToPath ( PredicateIsoΣ X )
+
+isSetPredicate : ∀ { ℓ' ℓ'' } ( X : Type ℓ' ) → isSet ( Predicate { ℓ'' = ℓ'' } X )
+isSetPredicate { ℓ' } { ℓ'' } X = subst (λ predicateType → isSet predicateType ) ( sym ( Predicate≡PredicateΣ X )) ( isSetPredicateΣ { ℓ'' = ℓ'' } X )
+
+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
+Realizability.Tripos.Prealgebra.Predicate.Properties open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Functions.FunExtEquiv
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty
+open import Cubical.Data.Unit
+open import Cubical.Data.Sum
+open import Cubical.HITs.PropositionalTruncation
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.Relation.Binary.Order.Preorder
+
+module
+ Realizability.Tripos.Prealgebra.Predicate.Properties
+ { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+
+open import Realizability.Tripos.Prealgebra.Predicate.Base ca
+
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming ( i to Id ; ia≡a to Ida≡a )
+open Predicate
+module PredicateProperties { ℓ' ℓ'' } ( X : Type ℓ' ) where
+ private PredicateX = Predicate { ℓ'' = ℓ'' } X
+ open Predicate
+ _≤_ : Predicate { ℓ'' = ℓ'' } X → Predicate { ℓ'' = ℓ'' } X → Type ( ℓ-max ( ℓ-max ℓ ℓ' ) ℓ'' )
+ ϕ ≤ ψ = ∃[ b ∈ A ] (∀ ( x : X ) ( a : A ) → a ⊩ ( ∣ ϕ ∣ x ) → ( b ⨾ a ) ⊩ ∣ ψ ∣ x )
+
+ isProp≤ : ∀ ϕ ψ → isProp ( ϕ ≤ ψ )
+ isProp≤ ϕ ψ = isPropPropTrunc
+
+ isRefl≤ : ∀ ϕ → ϕ ≤ ϕ
+ isRefl≤ ϕ = ∣ Id , (λ x a a⊩ϕx → subst (λ r → r ⊩ ∣ ϕ ∣ x ) ( sym ( Ida≡a a )) a⊩ϕx ) ∣₁
+
+ isTrans≤ : ∀ ϕ ψ ξ → ϕ ≤ ψ → ψ ≤ ξ → ϕ ≤ ξ
+ isTrans≤ ϕ ψ ξ ϕ≤ψ ψ≤ξ = do
+ ( a , ϕ≤[a]ψ ) ← ϕ≤ψ
+ ( b , ψ≤[b]ξ ) ← ψ≤ξ
+ return
+ (( B b a ) ,
+ (λ x a' a'⊩ϕx →
+ subst
+ (λ r → r ⊩ ∣ ξ ∣ x )
+ ( sym ( Ba≡gfa b a a' ))
+ ( ψ≤[b]ξ x ( a ⨾ a' )
+ ( ϕ≤[a]ψ x a' a'⊩ϕx ))))
+
+
+ open IsPreorder renaming
+ ( is-set to isSet
+ ; is-prop-valued to isPropValued
+ ; is-refl to isRefl
+ ; is-trans to isTrans )
+
+ preorder≤ : _
+ preorder≤ = preorder ( Predicate X ) _≤_ ( ispreorder ( isSetPredicate X ) isProp≤ isRefl≤ isTrans≤ )
+
+
+ infix 25 _⊔_
+ _⊔_ : PredicateX → PredicateX → PredicateX
+ ( ϕ ⊔ ψ ) . isSetX = ϕ . isSetX
+ ∣ ϕ ⊔ ψ ∣ x a = ∥ (( pr₁ ⨾ a ≡ k ) × (( pr₂ ⨾ a ) ⊩ ∣ ϕ ∣ x )) ⊎ (( pr₁ ⨾ a ≡ k' ) × (( pr₂ ⨾ a ) ⊩ ∣ ψ ∣ x )) ∥₁
+ ( ϕ ⊔ ψ ) . isPropValued x a = isPropPropTrunc
+
+ infix 25 _⊓_
+ _⊓_ : PredicateX → PredicateX → PredicateX
+ ( ϕ ⊓ ψ ) . isSetX = ϕ . isSetX
+ ∣ ϕ ⊓ ψ ∣ x a = (( pr₁ ⨾ a ) ⊩ ∣ ϕ ∣ x ) × (( pr₂ ⨾ a ) ⊩ ∣ ψ ∣ x )
+ ( ϕ ⊓ ψ ) . isPropValued x a = isProp× ( ϕ . isPropValued x ( pr₁ ⨾ a )) ( ψ . isPropValued x ( pr₂ ⨾ a ))
+
+ infix 25 _⇒_
+ _⇒_ : PredicateX → PredicateX → PredicateX
+ ( ϕ ⇒ ψ ) . isSetX = ϕ . isSetX
+ ∣ ϕ ⇒ ψ ∣ x a = ∀ b → ( b ⊩ ∣ ϕ ∣ x ) → ( a ⨾ b ) ⊩ ∣ ψ ∣ x
+ ( ϕ ⇒ ψ ) . isPropValued x a = isPropΠ λ a → isPropΠ λ a⊩ϕx → ψ . isPropValued _ _
+
+
+module Morphism { ℓ' ℓ'' } { X Y : Type ℓ' } ( isSetX : isSet X ) ( isSetY : isSet Y ) where
+ PredicateX = Predicate { ℓ'' = ℓ'' } X
+ PredicateY = Predicate { ℓ'' = ℓ'' } Y
+ module PredicatePropertiesX = PredicateProperties { ℓ'' = ℓ'' } X
+ module PredicatePropertiesY = PredicateProperties { ℓ'' = ℓ'' } Y
+ open PredicatePropertiesX renaming ( _≤_ to _≤X_ ; isProp≤ to isProp≤X )
+ open PredicatePropertiesY renaming ( _≤_ to _≤Y_ ; isProp≤ to isProp≤Y )
+ open Predicate hiding ( isSetX )
+
+ ⋆_ : ( X → Y ) → ( PredicateY → PredicateX )
+ ⋆ f =
+ λ ϕ →
+ record
+ { isSetX = isSetX
+ ; ∣_∣ = λ x a → a ⊩ ∣ ϕ ∣ ( f x )
+ ; isPropValued = λ x a → ϕ . isPropValued ( f x ) a }
+
+ `∀[_] : ( X → Y ) → ( PredicateX → PredicateY )
+ `∀[ f ] =
+ λ ϕ →
+ record
+ { isSetX = isSetY
+ ; ∣_∣ = λ y a → (∀ b x → f x ≡ y → ( a ⨾ b ) ⊩ ∣ ϕ ∣ x )
+ ; isPropValued = λ y a → isPropΠ λ a' → isPropΠ λ x → isPropΠ λ fx≡y → ϕ . isPropValued x ( a ⨾ a' ) }
+
+ `∃[_] : ( X → Y ) → ( PredicateX → PredicateY )
+ `∃[ f ] =
+ λ ϕ →
+ record
+ { isSetX = isSetY
+ ; ∣_∣ = λ y a → ∃[ x ∈ X ] ( f x ≡ y ) × ( a ⊩ ∣ ϕ ∣ x )
+ ; isPropValued = λ y a → isPropPropTrunc }
+
+
+
+ `∃isLeftAdjoint→ : ∀ ϕ ψ f → `∃[ f ] ϕ ≤Y ψ → ϕ ≤X ( ⋆ f ) ψ
+ `∃isLeftAdjoint→ ϕ ψ f p =
+ do
+ ( a~ , a~proves ) ← p
+ return ( a~ , (λ x a a⊩ϕx → a~proves ( f x ) a ∣ x , refl , a⊩ϕx ∣₁ ))
+
+
+ `∃isLeftAdjoint← : ∀ ϕ ψ f → ϕ ≤X ( ⋆ f ) ψ → `∃[ f ] ϕ ≤Y ψ
+ `∃isLeftAdjoint← ϕ ψ f p =
+ do
+ ( a~ , a~proves ) ← p
+ return
+ ( a~ ,
+ (λ y b b⊩∃fϕ →
+ equivFun
+ ( propTruncIdempotent≃
+ ( ψ . isPropValued y ( a~ ⨾ b )))
+ ( do
+ ( x , fx≡y , b⊩ϕx ) ← b⊩∃fϕ
+ return ( subst (λ y' → ( a~ ⨾ b ) ⊩ ∣ ψ ∣ y' ) fx≡y ( a~proves x b b⊩ϕx )))))
+
+ `∃isLeftAdjoint : ∀ ϕ ψ f → `∃[ f ] ϕ ≤Y ψ ≡ ϕ ≤X ( ⋆ f ) ψ
+ `∃isLeftAdjoint ϕ ψ f =
+ hPropExt
+ ( isProp≤Y ( `∃[ f ] ϕ ) ψ )
+ ( isProp≤X ϕ (( ⋆ f ) ψ ))
+ ( `∃isLeftAdjoint→ ϕ ψ f )
+ ( `∃isLeftAdjoint← ϕ ψ f )
+
+ `∀isRightAdjoint→ : ∀ ϕ ψ f → ψ ≤Y `∀[ f ] ϕ → ( ⋆ f ) ψ ≤X ϕ
+ `∀isRightAdjoint→ ϕ ψ f p =
+ do
+ ( a~ , a~proves ) ← p
+ let realizer = ( s ⨾ ( s ⨾ ( k ⨾ a~ ) ⨾ Id ) ⨾ ( k ⨾ k ))
+ return
+ ( realizer ,
+ (λ x a a⊩ψfx →
+ equivFun
+ ( propTruncIdempotent≃
+ ( ϕ . isPropValued x ( realizer ⨾ a ) ))
+ ( do
+ let ∀prover = a~proves ( f x ) a a⊩ψfx
+ return
+ ( subst
+ (λ ϕ~ → ϕ~ ⊩ ∣ ϕ ∣ x )
+ ( sym
+ ( realizer ⨾ a
+ ≡⟨ refl ⟩
+ s ⨾ ( s ⨾ ( k ⨾ a~ ) ⨾ Id ) ⨾ ( k ⨾ k ) ⨾ a
+ ≡⟨ sabc≡ac_bc _ _ _ ⟩
+ s ⨾ ( k ⨾ a~ ) ⨾ Id ⨾ a ⨾ ( k ⨾ k ⨾ a )
+ ≡⟨ cong (λ x → x ⨾ ( k ⨾ k ⨾ a )) ( sabc≡ac_bc _ _ _) ⟩
+ k ⨾ a~ ⨾ a ⨾ ( Id ⨾ a ) ⨾ ( k ⨾ k ⨾ a )
+ ≡⟨ cong (λ x → k ⨾ a~ ⨾ a ⨾ x ⨾ ( k ⨾ k ⨾ a )) ( Ida≡a a ) ⟩
+ k ⨾ a~ ⨾ a ⨾ a ⨾ ( k ⨾ k ⨾ a )
+ ≡⟨ cong (λ x → k ⨾ a~ ⨾ a ⨾ a ⨾ x ) ( kab≡a _ _) ⟩
+ ( k ⨾ a~ ⨾ a ) ⨾ a ⨾ k
+ ≡⟨ cong (λ x → x ⨾ a ⨾ k ) ( kab≡a _ _) ⟩
+ a~ ⨾ a ⨾ k
+ ∎ ))
+ ( ∀prover k x refl )))))
+
+ `∀isRightAdjoint← : ∀ ϕ ψ f → ( ⋆ f ) ψ ≤X ϕ → ψ ≤Y `∀[ f ] ϕ
+ `∀isRightAdjoint← ϕ ψ f p =
+ do
+ ( a~ , a~proves ) ← p
+ let realizer = ( s ⨾ ( s ⨾ ( k ⨾ s ) ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ ))) ⨾ ( s ⨾ ( k ⨾ k ) ⨾ Id ))
+ return
+ ( realizer ,
+ (λ y b b⊩ψy a x fx≡y →
+ subst
+ (λ r → r ⊩ ∣ ϕ ∣ x )
+ ( sym
+ ( realizer ⨾ b ⨾ a
+ ≡⟨ refl ⟩
+ s ⨾ ( s ⨾ ( k ⨾ s ) ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ ))) ⨾ ( s ⨾ ( k ⨾ k ) ⨾ Id ) ⨾ b ⨾ a
+ ≡⟨ cong (λ x → x ⨾ a ) ( sabc≡ac_bc _ _ _) ⟩
+ s ⨾ ( k ⨾ s ) ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ )) ⨾ b ⨾ ( s ⨾ ( k ⨾ k ) ⨾ Id ⨾ b ) ⨾ a
+ ≡⟨ cong (λ x → s ⨾ ( k ⨾ s ) ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ )) ⨾ b ⨾ x ⨾ a ) ( sabc≡ac_bc ( k ⨾ k ) Id b ) ⟩
+ s ⨾ ( k ⨾ s ) ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ )) ⨾ b ⨾ (( k ⨾ k ⨾ b ) ⨾ ( Id ⨾ b )) ⨾ a
+ ≡⟨ cong (λ x → s ⨾ ( k ⨾ s ) ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ )) ⨾ b ⨾ ( x ⨾ ( Id ⨾ b )) ⨾ a ) ( kab≡a _ _) ⟩
+ s ⨾ ( k ⨾ s ) ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ )) ⨾ b ⨾ ( k ⨾ ( Id ⨾ b )) ⨾ a
+ ≡⟨ cong (λ x → s ⨾ ( k ⨾ s ) ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ )) ⨾ b ⨾ ( k ⨾ x ) ⨾ a ) ( Ida≡a b ) ⟩
+ s ⨾ ( k ⨾ s ) ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ )) ⨾ b ⨾ ( k ⨾ b ) ⨾ a
+ ≡⟨ cong (λ x → x ⨾ ( k ⨾ b ) ⨾ a ) ( sabc≡ac_bc _ _ _) ⟩
+ k ⨾ s ⨾ b ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ ) ⨾ b ) ⨾ ( k ⨾ b ) ⨾ a
+ ≡⟨ cong (λ x → x ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ ) ⨾ b ) ⨾ ( k ⨾ b ) ⨾ a ) ( kab≡a _ _) ⟩
+ s ⨾ ( s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ ) ⨾ b ) ⨾ ( k ⨾ b ) ⨾ a
+ ≡⟨ sabc≡ac_bc _ _ _ ⟩
+ s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ ) ⨾ b ⨾ a ⨾ ( k ⨾ b ⨾ a )
+ ≡⟨ cong (λ x → s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ ) ⨾ b ⨾ a ⨾ x ) ( kab≡a b a ) ⟩
+ s ⨾ ( k ⨾ k ) ⨾ ( k ⨾ a~ ) ⨾ b ⨾ a ⨾ b
+ ≡⟨ cong (λ x → x ⨾ a ⨾ b ) ( sabc≡ac_bc ( k ⨾ k ) ( k ⨾ a~ ) b ) ⟩
+ k ⨾ k ⨾ b ⨾ ( k ⨾ a~ ⨾ b ) ⨾ a ⨾ b
+ ≡⟨ cong (λ x → x ⨾ ( k ⨾ a~ ⨾ b ) ⨾ a ⨾ b ) ( kab≡a _ _) ⟩
+ k ⨾ ( k ⨾ a~ ⨾ b ) ⨾ a ⨾ b
+ ≡⟨ cong (λ x → k ⨾ x ⨾ a ⨾ b ) ( kab≡a _ _) ⟩
+ k ⨾ a~ ⨾ a ⨾ b
+ ≡⟨ cong (λ x → x ⨾ b ) ( kab≡a _ _) ⟩
+ a~ ⨾ b
+ ∎ ))
+ ( a~proves x b ( subst (λ x' → b ⊩ ∣ ψ ∣ x' ) ( sym fx≡y ) b⊩ψy ))))
+
+ `∀isRightAdjoint : ∀ ϕ ψ f → ( ⋆ f ) ψ ≤X ϕ ≡ ψ ≤Y `∀[ f ] ϕ
+ `∀isRightAdjoint ϕ ψ f =
+ hPropExt
+ ( isProp≤X (( ⋆ f ) ψ ) ϕ )
+ ( isProp≤Y ψ ( `∀[ f ] ϕ ))
+ ( `∀isRightAdjoint← ϕ ψ f )
+ ( `∀isRightAdjoint→ ϕ ψ f )
+
+
+module BeckChevalley
+ { ℓ' ℓ'' : Level }
+ ( I J K : Type ℓ' )
+ ( isSetI : isSet I )
+ ( isSetJ : isSet J )
+ ( isSetK : isSet K )
+ ( f : J → I )
+ ( g : K → I ) where
+
+ module Morphism' = Morphism { ℓ' = ℓ' } { ℓ'' = ℓ'' }
+ open Morphism'
+
+ L = Σ[ k ∈ K ] Σ[ j ∈ J ] ( g k ≡ f j )
+
+ isSetL : isSet L
+ isSetL = isSetΣ isSetK λ k → isSetΣ isSetJ λ j → isProp→isSet ( isSetI _ _)
+
+ p : L → K
+ p ( k , _ , _) = k
+
+ q : L → J
+ q (_ , l , _) = l
+
+ q* = ⋆_ isSetL isSetJ q
+ g* = ⋆_ isSetK isSetI g
+
+ module `f = Morphism' isSetJ isSetI
+ open `f renaming ( `∃[_] to `∃[J→I][_] ; `∀[_] to `∀[J→I][_] )
+
+ module `q = Morphism' isSetL isSetK
+ open `q renaming ( `∃[_] to `∃[L→K][_] ; `∀[_] to `∀[L→K][_] )
+
+ `∃BeckChevalley→ : ∀ ϕ k a → a ⊩ ∣ g* ( `∃[J→I][ f ] ϕ ) ∣ k → a ⊩ ∣ `∃[L→K][ p ] ( q* ϕ ) ∣ k
+ `∃BeckChevalley→ ϕ k a p =
+ do
+ ( j , fj≡gk , a⊩ϕj ) ← p
+ return (( k , ( j , ( sym fj≡gk ))) , ( refl , a⊩ϕj ))
+
+ `∃BeckChevalley← : ∀ ϕ k a → a ⊩ ∣ `∃[L→K][ p ] ( q* ϕ ) ∣ k → a ⊩ ∣ g* ( `∃[J→I][ f ] ϕ ) ∣ k
+ `∃BeckChevalley← ϕ k a p =
+ do
+ ( x @( k' , j , gk'≡fj ) , k'≡k , a⊩ϕqj ) ← p
+ return ( j , ( subst (λ k → f j ≡ g k ) k'≡k ( sym gk'≡fj )) , a⊩ϕqj )
+
+ open Iso
+ `∃BeckChevalley : g* ∘ `∃[J→I][ f ] ≡ `∃[L→K][ p ] ∘ q*
+ `∃BeckChevalley =
+ funExt λ ϕ i →
+ PredicateIsoΣ K . inv
+ ( PredicateΣ≡ { ℓ'' = ℓ'' } K
+ ((λ k a → ( ∣ ( g* ∘ `∃[J→I][ f ] ) ϕ ∣ k a ) , (( g* ∘ `∃[J→I][ f ] ) ϕ . isPropValued k a )) , isSetK )
+ ((λ k a → ( ∣ ( `∃[L→K][ p ] ∘ q* ) ϕ ∣ k a ) , (( `∃[L→K][ p ] ∘ q* ) ϕ . isPropValued k a )) , isSetK )
+ ( funExt₂
+ (λ k a →
+ Σ≡Prop
+ (λ x → isPropIsProp { A = x })
+ ( hPropExt
+ ( g* ( `∃[J→I][ f ] ϕ ) . isPropValued k a )
+ ( `∃[L→K][ p ] ( q* ϕ ) . isPropValued k a )
+ ( `∃BeckChevalley→ ϕ k a )
+ ( `∃BeckChevalley← ϕ k a ))))
+ i )
+
+ `∀BeckChevalley→ : ∀ ϕ k a → a ⊩ ∣ g* ( `∀[J→I][ f ] ϕ ) ∣ k → a ⊩ ∣ `∀[L→K][ p ] ( q* ϕ ) ∣ k
+ `∀BeckChevalley→ ϕ k a p b ( k' , j , gk'≡fj ) k'≡k = p b j ( sym ( subst (λ k'' → g k'' ≡ f j ) k'≡k gk'≡fj ))
+
+ `∀BeckChevalley← : ∀ ϕ k a → a ⊩ ∣ `∀[L→K][ p ] ( q* ϕ ) ∣ k → a ⊩ ∣ g* ( `∀[J→I][ f ] ϕ ) ∣ k
+ `∀BeckChevalley← ϕ k a p b j fj≡gk = p b ( k , j , sym fj≡gk ) refl
+
+ `∀BeckChevalley : g* ∘ `∀[J→I][ f ] ≡ `∀[L→K][ p ] ∘ q*
+ `∀BeckChevalley =
+ funExt λ ϕ i →
+ PredicateIsoΣ K . inv
+ ( PredicateΣ≡ { ℓ'' = ℓ'' } K
+ ((λ k a → ( a ⊩ ∣ g* ( `∀[J→I][ f ] ϕ ) ∣ k ) , ( g* ( `∀[J→I][ f ] ϕ ) . isPropValued k a )) , isSetK )
+ ((λ k a → ( a ⊩ ∣ `∀[L→K][ p ] ( q* ϕ ) ∣ k ) , ( `∀[L→K][ p ] ( q* ϕ ) . isPropValued k a )) , isSetK )
+ ( funExt₂
+ (λ k a →
+ Σ≡Prop
+ (λ x → isPropIsProp { A = x })
+ ( hPropExt
+ ( g* ( `∀[J→I][ f ] ϕ ) . isPropValued k a )
+ ( `∀[L→K][ p ] ( q* ϕ ) . isPropValued k a )
+ ( `∀BeckChevalley→ ϕ k a )
+ ( `∀BeckChevalley← ϕ k a ))))
+ i )
+Realizability.Tripos.Prealgebra.Predicate open import Realizability.CombinatoryAlgebra
+open import Cubical.Foundations.Prelude
+
+module Realizability.Tripos.Prealgebra.Predicate { ℓ } { A : Type ℓ } ( ca : CombinatoryAlgebra A ) where
+
+open import Realizability.Tripos.Prealgebra.Predicate.Base ca public
+open import Realizability.Tripos.Prealgebra.Predicate.Properties ca public
+