From a0b1980c6466d0d089f22d31470821e5b5adb697 Mon Sep 17 00:00:00 2001 From: Johnson He Date: Thu, 20 Jun 2024 19:38:25 +0000 Subject: [PATCH] working on simple Gluing example for CartesianCategory Split Categories/Instances/Sets/More.agda into More and Properties.agda, because importing Categories/Limits/BinProducts caused cyclic imports. I don't know why, but compiling takes painfully long for Gluing/CartesianCategory. --- .../Categories/Displayed/Instances/Path.agda | 1 - .../Displayed/Instances/Sets/Properties.agda | 19 ++- Cubical/Categories/Instances/Sets/More.agda | 11 -- .../Categories/Instances/Sets/Properties.agda | 40 ++++++ .../Categories/Presheaf/Constructions.agda | 1 - Cubical/Categories/Profunctor/General.agda | 1 - Gluing/CartesianCategory.agda | 125 ++++++++++++++++++ 7 files changed, 183 insertions(+), 15 deletions(-) create mode 100644 Cubical/Categories/Instances/Sets/Properties.agda create mode 100644 Gluing/CartesianCategory.agda diff --git a/Cubical/Categories/Displayed/Instances/Path.agda b/Cubical/Categories/Displayed/Instances/Path.agda index ed2c537b..21c637a1 100644 --- a/Cubical/Categories/Displayed/Instances/Path.agda +++ b/Cubical/Categories/Displayed/Instances/Path.agda @@ -24,7 +24,6 @@ open import Cubical.Categories.Displayed.HLevels open import Cubical.Categories.Displayed.HLevels.More open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Section.Base -open import Cubical.Categories.Displayed.Constructions.Graph open import Cubical.Categories.Displayed.Instances.Terminal open import Cubical.Categories.Displayed.Constructions.StructureOver open import Cubical.Categories.Displayed.Properties diff --git a/Cubical/Categories/Displayed/Instances/Sets/Properties.agda b/Cubical/Categories/Displayed/Instances/Sets/Properties.agda index 25f608d9..d31bb010 100644 --- a/Cubical/Categories/Displayed/Instances/Sets/Properties.agda +++ b/Cubical/Categories/Displayed/Instances/Sets/Properties.agda @@ -1,4 +1,5 @@ -{-# OPTIONS --safe #-} +--{-# OPTIONS --safe #-} +{-# OPTIONS --allow-unsolved-metas #-} module Cubical.Categories.Displayed.Instances.Sets.Properties where open import Cubical.Foundations.Prelude @@ -13,6 +14,7 @@ open import Cubical.Data.Unit open import Cubical.Categories.Category open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.Sets.More +open import Cubical.Categories.Instances.Sets.Properties open import Cubical.Categories.Displayed.Base open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Fibration.Base @@ -20,6 +22,7 @@ open import Cubical.Categories.Displayed.Fibration.Properties open import Cubical.Categories.Displayed.Instances.Sets.Base open import Cubical.Categories.Displayed.Presheaf open import Cubical.Categories.Displayed.Limits.Terminal +open import Cubical.Categories.Displayed.Limits.BinProduct private @@ -55,3 +58,17 @@ VerticalTerminalsSETᴰ dᴰ .universalᴰ .equiv-proof _ = uniqueExists LiftedTerminalSETᴰ : ∀{ℓ ℓ'} → LiftedTerminal (SETᴰ ℓ ℓ') terminal'SET LiftedTerminalSETᴰ {ℓ} {ℓ'} = Vertical/𝟙→LiftedTerm _ (VerticalTerminalsSETᴰ _) + +module _ {ℓSETᴰ ℓSETᴰ' : Level} where + VerticalBinProdsSETᴰ : VerticalBinProducts (SETᴰ ℓSETᴰ ℓSETᴰ') + VerticalBinProdsSETᴰ {d = X} (Xᴰ , Xᴰ') .vertexᴰ x = + ⟨ Xᴰ x ⟩ × ⟨ Xᴰ' x ⟩ , isSet× (Xᴰ x .snd) (Xᴰ' x .snd) + VerticalBinProdsSETᴰ {d = X} (Xᴰ , Xᴰ') .elementᴰ = (λ _ → fst) , (λ _ → snd) + VerticalBinProdsSETᴰ {d = X} (Xᴰ , Xᴰ') .universalᴰ {x = Y} {xᴰ = Yᴰ} {f = h} .equiv-proof (f , g) = + uniqueExists (λ y yᴰ → f y yᴰ , g y yᴰ) refl + (λ h → isSet× + (SETᴰ ℓSETᴰ ℓSETᴰ' .isSetHomᴰ {yᴰ = Xᴰ}) + (SETᴰ ℓSETᴰ ℓSETᴰ' .isSetHomᴰ {yᴰ = Xᴰ'}) + _ + (f , g)) + λ h p → {!!} diff --git a/Cubical/Categories/Instances/Sets/More.agda b/Cubical/Categories/Instances/Sets/More.agda index 50ccf097..7824a1d3 100644 --- a/Cubical/Categories/Instances/Sets/More.agda +++ b/Cubical/Categories/Instances/Sets/More.agda @@ -13,7 +13,6 @@ open import Cubical.Data.Unit open import Cubical.Categories.Category open import Cubical.Categories.Functor -open import Cubical.Categories.Limits.Terminal.More open import Cubical.Categories.Bifunctor.Redundant open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Constructions.BinProduct @@ -51,13 +50,3 @@ module _ {A}{B} (f : CatIso (SET ℓ) A B) a where ∙ transportRefl _ ∙ transportRefl _ ∙ cong (f .fst) (transportRefl _ ∙ transportRefl _ )) - -open UniversalElement -terminal'SET : Terminal' (SET ℓ) -terminal'SET .vertex = Unit* , isSetUnit* -terminal'SET .element = tt -terminal'SET .universal X .equiv-proof y = uniqueExists - (λ _ → tt*) - (isPropUnit tt tt) - (λ _ p' q' → isSetUnit tt tt p' q') - (λ _ _ → funExt λ _ → isPropUnit* tt* tt*) diff --git a/Cubical/Categories/Instances/Sets/Properties.agda b/Cubical/Categories/Instances/Sets/Properties.agda new file mode 100644 index 00000000..2b107c9f --- /dev/null +++ b/Cubical/Categories/Instances/Sets/Properties.agda @@ -0,0 +1,40 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Instances.Sets.Properties where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.HLevels +open import Cubical.Data.Unit +open import Cubical.Data.Sigma + +open import Cubical.Categories.Category +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Presheaf +open import Cubical.Categories.Limits.Terminal.More +open import Cubical.Categories.Limits.BinProduct.More + +private variable ℓ : Level + +open UniversalElement +open Category + +terminal'SET : Terminal' (SET ℓ) +terminal'SET .vertex = Unit* , isSetUnit* +terminal'SET .element = tt +terminal'SET .universal X .equiv-proof y = uniqueExists + (λ _ → tt*) + (isPropUnit tt tt) + (λ _ p' q' → isSetUnit tt tt p' q') + (λ _ _ → funExt λ _ → isPropUnit* tt* tt*) + +module _ {ℓSET : Level} where + BinProducts'SET : BinProducts' (SET ℓSET) + BinProducts'SET (X , Y) .vertex = X .fst × Y .fst , isSet× (X .snd) (Y .snd) + BinProducts'SET (X , Y) .element = fst , snd + BinProducts'SET (X , Y) .universal Z .equiv-proof (f , g) = + uniqueExists (λ z → f z , g z) refl + (λ h → isSet× + (SET ℓSET .isSetHom {x = Z} {y = X}) + (SET ℓSET .isSetHom {x = Z} {y = Y}) + ((λ z → (h z) .fst) , λ z → (h z) .snd) (f , g)) + λ h p i z → (sym p) i .fst z , (sym p) i .snd z diff --git a/Cubical/Categories/Presheaf/Constructions.agda b/Cubical/Categories/Presheaf/Constructions.agda index 8d5d18be..70c6050a 100644 --- a/Cubical/Categories/Presheaf/Constructions.agda +++ b/Cubical/Categories/Presheaf/Constructions.agda @@ -12,7 +12,6 @@ open import Cubical.Categories.NaturalTransformation open import Cubical.Categories.Instances.Functors open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Presheaf.Base -open import Cubical.Categories.Presheaf.More open import Cubical.Categories.Bifunctor.Redundant private diff --git a/Cubical/Categories/Profunctor/General.agda b/Cubical/Categories/Profunctor/General.agda index 74ec2438..82628265 100644 --- a/Cubical/Categories/Profunctor/General.agda +++ b/Cubical/Categories/Profunctor/General.agda @@ -29,7 +29,6 @@ open import Cubical.Data.Sigma open import Cubical.Categories.Presheaf.Base open import Cubical.Categories.Presheaf.Representable -open import Cubical.Categories.Presheaf.More open import Cubical.Categories.Instances.Functors.More private diff --git a/Gluing/CartesianCategory.agda b/Gluing/CartesianCategory.agda new file mode 100644 index 00000000..9c499658 --- /dev/null +++ b/Gluing/CartesianCategory.agda @@ -0,0 +1,125 @@ +{-# OPTIONS --allow-unsolved-metas #-} +--{-# OPTIONS --safe #-} +module Gluing.CartesianCategory where + +open import Cubical.Foundations.Prelude +open import Cubical.Relation.Nullary hiding (⟪_⟫) +open import Cubical.Data.Nat +open import Cubical.Data.Nat.Properties +open import Cubical.Data.Bool +open import Cubical.Data.Sum + +open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Functor +open import Cubical.Categories.Constructions.Free.CartesianCategory.Base as Law +open import Cubical.Categories.Constructions.Free.CartesianCategory.ProductQuiver +open import Cubical.Categories.Limits.Cartesian.Base +open import Cubical.Categories.Limits.Terminal.More +open import Cubical.Categories.Limits.BinProduct.More +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Instances.Sets.More +open import Cubical.Categories.Instances.Sets.Properties + +open import Cubical.Categories.Displayed.Section.Base +open import Cubical.Categories.Displayed.Instances.Sets.Base +open import Cubical.Categories.Displayed.Instances.Sets.Properties +open import Cubical.Categories.Displayed.Constructions.Reindex.Properties + +open Category +open Section + +-- TODO: add an object that nothing uses, for a second example +module _ where + data OB : Type ℓ-zero where + ans : OB + + discreteOB : Discrete OB + discreteOB = sectionDiscrete {A = ℕ} + (λ _ → ans) + (λ _ → 0) + (λ { ans → refl }) + discreteℕ + + isSetOB : isSet OB + isSetOB = Discrete→isSet discreteOB + + data MOR : Type ℓ-zero where + t f : MOR + + discreteMOR : Discrete MOR + discreteMOR = sectionDiscrete {A = ℕ} + (λ { zero → t ; (suc _) → f }) + (λ { t → 0 ; f → 1 }) + (λ { t → refl ; f → refl }) + discreteℕ + + isSetMOR : isSet MOR + isSetMOR = Discrete→isSet discreteMOR + + interleaved mutual -- not actually mutually recursive, just to interleave + dom cod : MOR → ProdExpr OB + + dom t = ⊤ + cod t = ↑ ans + + dom f = ⊤ + cod f = ↑ ans + + QUIVER : ×Quiver _ + QUIVER .fst = OB + QUIVER .snd .ProductQuiver.mor = MOR + QUIVER .snd .ProductQuiver.dom = dom + QUIVER .snd .ProductQuiver.cod = cod + + private module Q = ×QuiverNotation QUIVER + + FREECC : CartesianCategory _ _ + FREECC = FreeCartesianCategory QUIVER + + open Terminal'Notation + (terminalToUniversalElement {C = FREECC .fst} (FREECC .snd .fst)) + + [ans] : FREECC .fst .ob + [ans] = ↑ ans + + [t] [f] : FREECC .fst [ 𝟙 , [ans] ] + [t] = ↑ₑ t + [f] = ↑ₑ f + + boolToExp : Bool → FREECC .fst [ 𝟙 , [ans] ] + boolToExp = if_then [t] else [f] + + [t]≠[f] : ¬ ([t] ≡ [f]) + [t]≠[f] p = true≢false (cong n p) + where + sem : Functor (FREECC .fst) (SET ℓ-zero) + sem = Law.rec _ + (SET ℓ-zero , + Terminal'ToTerminal terminal'SET , + BinProducts'ToBinProducts _ BinProducts'SET) + (λ { ans → Bool , isSetBool}) + λ { t → λ _ → true ; f → λ _ → false} + n : FREECC .fst [ 𝟙 , [ans] ] → Bool + n e = (sem ⟪ e ⟫) _ + + CanonicalForm : FREECC .fst [ 𝟙 , [ans] ] → Type _ + CanonicalForm e = ([t] ≡ e) ⊎ ([f] ≡ e) + + isSetCanonicalForm : ∀ {e} → isSet (CanonicalForm e) + isSetCanonicalForm {e = e} = isSet⊎ + (isProp→isSet (FREECC .fst .isSetHom [t] e)) + (isProp→isSet (FREECC .fst .isSetHom [f] e)) + + canonicity : ∀ e → CanonicalForm e + canonicity e = {!!} + where + pts = FREECC .fst [ 𝟙 ,-] + Canonicalize : Section pts (SETᴰ _ _) + Canonicalize = elimLocal _ + (VerticalTerminalsSETᴰ (pts ⟅ ⊤ ⟆)) + (λ Fcᴰ Fc'ᴰ → isFib→F⟪π₁⟫* (BinProducts'SET _) Fcᴰ isFibrationSet , + isFib→F⟪π₂⟫* (BinProducts'SET _) Fc'ᴰ isFibrationSet) + (λ Fcᴰ Fc'ᴰ → {!!}) + (λ { ans global-ans → CanonicalForm global-ans , isSetCanonicalForm}) + λ { t global-ans → λ ⟨⟩ → inl (sym (FREECC .fst .⋆IdL _) ∙ congS (λ x → x ⋆⟨ FREECC .fst ⟩ _) 𝟙η') + ; f global-ans → λ ⟨⟩ → inr (sym (FREECC .fst .⋆IdL _) ∙ congS (λ x → x ⋆⟨ FREECC .fst ⟩ _) 𝟙η') }