From 1a546a33f63de50f4d5b8a1466234bc4eb291d54 Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Sun, 17 Dec 2023 20:26:07 +0530 Subject: [PATCH] Add more properties of tripos predicates --- src/Realizability/Tripos/Predicate.agda | 223 ++++++++++++++++++++++-- 1 file changed, 208 insertions(+), 15 deletions(-) diff --git a/src/Realizability/Tripos/Predicate.agda b/src/Realizability/Tripos/Predicate.agda index c46f38d..2636a9d 100644 --- a/src/Realizability/Tripos/Predicate.agda +++ b/src/Realizability/Tripos/Predicate.agda @@ -2,6 +2,10 @@ open import Realizability.CombinatoryAlgebra open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Function +open import Cubical.Functions.FunExtEquiv open import Cubical.Data.Sigma open import Cubical.Data.Sum open import Cubical.HITs.PropositionalTruncation @@ -23,24 +27,27 @@ _⊩_ : ∀ {ℓ'} → 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 ℓ ℓ') ℓ'')) +PredicateΣ {ℓ'} {ℓ''} X = Σ[ rel ∈ (X → A → hProp (ℓ-max (ℓ-max ℓ ℓ') ℓ'')) ] (isSet X) isSetPredicateΣ : ∀ {ℓ' ℓ''} (X : Type ℓ') → isSet (PredicateΣ {ℓ'' = ℓ''} X) -isSetPredicateΣ X = isSetΣ (isProp→isSet isPropIsSet) λ isSetX → isSetΠ λ x → isSetΠ λ a → isSetHProp +isSetPredicateΣ X = isSetΣ (isSetΠ (λ x → isSetΠ λ a → isSetHProp)) λ _ → isProp→isSet isPropIsSet 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 }) + (λ 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≡Σ : ∀ {ℓ' ℓ''} (X : Type ℓ') → Predicate {ℓ'' = ℓ''} X ≡ PredicateΣ {ℓ'' = ℓ''} X -Predicate≡Σ {ℓ'} {ℓ''} X = isoToPath (PredicateIsoΣ X) +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≡Σ X)) (isSetPredicateΣ {ℓ'' = ℓ''} 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∣ module PredicateProperties {ℓ' ℓ''} (X : Type ℓ') where PredicateX = Predicate {ℓ'' = ℓ''} X @@ -58,10 +65,21 @@ module PredicateProperties {ℓ' ℓ''} (X : Type ℓ') where 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)))) + 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) + 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≤) @@ -87,12 +105,187 @@ module PredicateProperties {ℓ' ℓ''} (X : Type ℓ') where 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 hiding (PredicateX) renaming (_≤_ to _≤X_ ; isProp≤ to isProp≤X) + open PredicatePropertiesY hiding (PredicateX) renaming (_≤_ to _≤Y_ ; isProp≤ to isProp≤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 } + + -- Adjunction proofs + + `∃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)))) - _⋆ : (X → Y) → (PredicateY → PredicateX) - f ⋆ = λ ϕ → record { isSetX = isSetX ; ∣_∣ = λ x a → a ⊩ ∣ ϕ ∣ (f x) ; isPropValued = λ x a → ϕ .isPropValued (f x) a } + `∀isRightAdjoint : ∀ ϕ ψ f → (⋆ f) ψ ≤X ϕ ≡ ψ ≤Y `∀[ f ] ϕ + `∀isRightAdjoint ϕ ψ f = + hPropExt + (isProp≤X ((⋆ f) ψ) ϕ) + (isProp≤Y ψ (`∀[ f ] ϕ)) + (`∀isRightAdjoint← ϕ ψ f) + (`∀isRightAdjoint→ ϕ ψ f) - `∀_ : (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') } +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][_]) + + 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) {!!})) i) + + - `∃_ : (X → Y) → (PredicateX → PredicateY) - `∃ f = λ ϕ → record { isSetX = isSetY ; ∣_∣ = λ y a → ∃[ x ∈ X ] (f x ≡ y) × (a ⊩ ∣ ϕ ∣ x) ; isPropValued = λ y a → isPropPropTrunc } +