From 49be095ea698cd7e7ebf72e418d8a147328bcc38 Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Fri, 22 Dec 2023 04:05:02 +0530 Subject: [PATCH] Define join for predicate algebra --- src/Realizability/Tripos/Algebra.agda | 181 ++++++++++++++++-- src/Realizability/Tripos/Everything.agda | 2 + src/Realizability/Tripos/PosetReflection.agda | 12 +- src/Realizability/Tripos/Predicate.agda | 21 ++ 4 files changed, 199 insertions(+), 17 deletions(-) diff --git a/src/Realizability/Tripos/Algebra.agda b/src/Realizability/Tripos/Algebra.agda index 77d6b68..4783dd9 100644 --- a/src/Realizability/Tripos/Algebra.agda +++ b/src/Realizability/Tripos/Algebra.agda @@ -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 @@ -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 diff --git a/src/Realizability/Tripos/Everything.agda b/src/Realizability/Tripos/Everything.agda index e016e81..c25d2f9 100644 --- a/src/Realizability/Tripos/Everything.agda +++ b/src/Realizability/Tripos/Everything.agda @@ -1,2 +1,4 @@ module Realizability.Tripos.Everything where open import Realizability.Tripos.Predicate +open import Realizability.Tripos.PosetReflection +open import Realizability.Tripos.Algebra diff --git a/src/Realizability/Tripos/PosetReflection.agda b/src/Realizability/Tripos/PosetReflection.agda index d6dc526..82682cc 100644 --- a/src/Realizability/Tripos/PosetReflection.agda +++ b/src/Realizability/Tripos/PosetReflection.agda @@ -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 @@ -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≤ᴿ) diff --git a/src/Realizability/Tripos/Predicate.agda b/src/Realizability/Tripos/Predicate.agda index a91b6ad..c20af8b 100644 --- a/src/Realizability/Tripos/Predicate.agda +++ b/src/Realizability/Tripos/Predicate.agda @@ -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