From d78e5c014a5d5132a721703d6e53a2eb459c3203 Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Fri, 15 Dec 2023 13:12:51 +0530 Subject: [PATCH] Update changes --- src/Realizability/Assembly/Path.agda | 11 ++- .../Assembly/Regular/Cobase.agda | 8 +- .../Assembly/Regular/Everything.agda | 3 +- src/Realizability/Tripos/Everything.agda | 1 + src/Realizability/Tripos/Predicate.agda | 98 +++++++++++++++++++ 5 files changed, 117 insertions(+), 4 deletions(-) create mode 100644 src/Realizability/Tripos/Everything.agda create mode 100644 src/Realizability/Tripos/Predicate.agda diff --git a/src/Realizability/Assembly/Path.agda b/src/Realizability/Assembly/Path.agda index 3010f3e..7971b57 100644 --- a/src/Realizability/Assembly/Path.agda +++ b/src/Realizability/Assembly/Path.agda @@ -4,9 +4,11 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.HLevels open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Equiv open import Cubical.Functions.FunExtEquiv open import Cubical.Data.Sigma open import Cubical.HITs.PropositionalTruncation hiding (map) +open import Cubical.HITs.PropositionalTruncation.Monad open import Cubical.Categories.Category module Realizability.Assembly.Path {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where @@ -55,7 +57,14 @@ CatIsoToPath {X , xs} {Y , ys} x∼y = ΣPathP (P , λ i → record {B = λ i p' → Type ℓ} {f = xs ._⊩_ xᵣ} {g = ys ._⊩_ yᵣ} - λ {x y} p' → hPropExt {A = xᵣ ⊩X x} {B = yᵣ ⊩Y y} (xs .⊩isPropValued xᵣ x) (ys .⊩isPropValued yᵣ y) (λ xᵣ⊩x → {!!}) λ yᵣ⊩y → {!!} + λ {x y} p' → + hPropExt + {A = xᵣ ⊩X x} + {B = yᵣ ⊩Y y} + (xs .⊩isPropValued xᵣ x) + (ys .⊩isPropValued yᵣ y) + (λ xᵣ⊩x → {!!}) + λ yᵣ⊩y → {!!} ⊩isPropValuedOverP : PathP (λ i → ∀ (a : A) (p : P i) → isProp (⊩overP i a p)) (xs .⊩isPropValued) (ys .⊩isPropValued) ⊩isPropValuedOverP = diff --git a/src/Realizability/Assembly/Regular/Cobase.agda b/src/Realizability/Assembly/Regular/Cobase.agda index 0716ad8..a080860 100644 --- a/src/Realizability/Assembly/Regular/Cobase.agda +++ b/src/Realizability/Assembly/Regular/Cobase.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical #-} +{-# OPTIONS --cubical --allow-unsolved-metas #-} open import Realizability.CombinatoryAlgebra open import Cubical.Foundations.Prelude @@ -50,7 +50,11 @@ module do (f~ , f~tracks) ← f .tracker (b , bTracksSurjectivity) ← isSurjectivelyTrackedE - return (s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ b) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id))) ⨾ Id , λ z zᵣ zᵣ⊩z → ∣ {!!} , {!!} , {!!} ∣₁) + return + (s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ b) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id))) ⨾ Id , + λ z zᵣ zᵣ⊩z → + do + return ({!!} , {!!})) module _ (cl : CharLemma) where open ASMKernelPairs diff --git a/src/Realizability/Assembly/Regular/Everything.agda b/src/Realizability/Assembly/Regular/Everything.agda index b395b8a..b69d543 100644 --- a/src/Realizability/Assembly/Regular/Everything.agda +++ b/src/Realizability/Assembly/Regular/Everything.agda @@ -3,4 +3,5 @@ module Realizability.Assembly.Regular.Everything where open import Realizability.Assembly.Regular.CharLemma open import Realizability.Assembly.Regular.CharLemmaProof -open import Realizability.Assembly.Regular.RegularProof +--open import Realizability.Assembly.Regular.RegularProof +open import Realizability.Assembly.Regular.Cobase diff --git a/src/Realizability/Tripos/Everything.agda b/src/Realizability/Tripos/Everything.agda new file mode 100644 index 0000000..fe061c9 --- /dev/null +++ b/src/Realizability/Tripos/Everything.agda @@ -0,0 +1 @@ +module Realizability.Tripos.Everything where diff --git a/src/Realizability/Tripos/Predicate.agda b/src/Realizability/Tripos/Predicate.agda new file mode 100644 index 0000000..c46f38d --- /dev/null +++ b/src/Realizability/Tripos/Predicate.agda @@ -0,0 +1,98 @@ +open import Realizability.CombinatoryAlgebra +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism +open import Cubical.Data.Sigma +open import Cubical.Data.Sum +open import Cubical.HITs.PropositionalTruncation +open import Cubical.HITs.PropositionalTruncation.Monad +open import Cubical.Relation.Binary.Order + +module Realizability.Tripos.Predicate {ℓ} {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) + +open Predicate +_⊩_ : ∀ {ℓ'} → A → (A → Type ℓ') → Type ℓ' +a ⊩ ϕ = ϕ a + +PredicateΣ : ∀ {ℓ' ℓ''} → (X : Type ℓ') → Type (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ'')) +PredicateΣ {ℓ'} {ℓ''} X = Σ[ isSetX ∈ isSet X ] (X → A → hProp (ℓ-max (ℓ-max ℓ ℓ') ℓ'')) + +isSetPredicateΣ : ∀ {ℓ' ℓ''} (X : Type ℓ') → isSet (PredicateΣ {ℓ'' = ℓ''} X) +isSetPredicateΣ X = isSetΣ (isProp→isSet isPropIsSet) λ isSetX → isSetΠ λ x → isSetΠ λ a → isSetHProp + +PredicateIsoΣ : ∀ {ℓ' ℓ''} (X : Type ℓ') → Iso (Predicate {ℓ'' = ℓ''} X) (PredicateΣ {ℓ'' = ℓ''} X) +PredicateIsoΣ {ℓ'} {ℓ''} X = + iso + (λ p → p .isSetX , λ x a → ∣ p ∣ x a , p .isPropValued x a) + (λ p → record { isSetX = p .fst ; ∣_∣ = λ x a → p .snd x a .fst ; isPropValued = λ x a → p .snd x a .snd }) + (λ b → refl) + λ a → refl + +Predicate≡Σ : ∀ {ℓ' ℓ''} (X : Type ℓ') → Predicate {ℓ'' = ℓ''} X ≡ PredicateΣ {ℓ'' = ℓ''} X +Predicate≡Σ {ℓ'} {ℓ''} X = isoToPath (PredicateIsoΣ X) + +isSetPredicate : ∀ {ℓ' ℓ''} (X : Type ℓ') → isSet (Predicate {ℓ'' = ℓ''} X) +isSetPredicate {ℓ'} {ℓ''} X = subst (λ predicateType → isSet predicateType) (sym (Predicate≡Σ X)) (isSetPredicateΣ {ℓ'' = ℓ''} X) + +module PredicateProperties {ℓ' ℓ''} (X : Type ℓ') where + 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 = ∥ ((pair ⨾ k ⨾ a) ⊩ ∣ ϕ ∣ x) ⊎ ((pair ⨾ k' ⨾ 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 + + _⋆ : (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 }