From b4969a1e31a81e0950a898d588e51a30e49f65b3 Mon Sep 17 00:00:00 2001 From: Max New Date: Wed, 22 May 2024 16:14:11 -0400 Subject: [PATCH] rec for free cat with terminal object, non-triviality example --- .../Free/CategoryWithTerminal.agda | 50 +++++-- .../Displayed/Constructions/Weaken.agda | 104 +------------- .../Displayed/Constructions/Weaken/Base.agda | 100 +++++++++++++ .../Constructions/Weaken/Properties.agda | 37 +++++ Gluing/Terminal.agda | 134 ++++++++++++++++++ 5 files changed, 315 insertions(+), 110 deletions(-) create mode 100644 Cubical/Categories/Displayed/Constructions/Weaken/Base.agda create mode 100644 Cubical/Categories/Displayed/Constructions/Weaken/Properties.agda create mode 100644 Gluing/Terminal.agda diff --git a/Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda b/Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda index c22b9771..42bc43d9 100644 --- a/Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda +++ b/Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda @@ -1,12 +1,15 @@ +{-# OPTIONS --safe #-} -- Free category with a terminal object, over a Quiver module Cubical.Categories.Constructions.Free.CategoryWithTerminal where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels open import Cubical.Categories.Category.Base +open import Cubical.Categories.Functor open import Cubical.Categories.Limits.Terminal.More open import Cubical.Data.Quiver.Base -open import Cubical.Data.Sum.Base as Sum hiding (elim) +open import Cubical.Data.Sum.Base as Sum hiding (elim; rec) open import Cubical.Data.Unit open import Cubical.Categories.Displayed.Base open import Cubical.Categories.Presheaf @@ -15,10 +18,16 @@ open import Cubical.Categories.Displayed.Limits.Terminal open import Cubical.Foundations.Equiv open import Cubical.Data.Sigma.Properties open import Cubical.Categories.Displayed.Section.Base +open import Cubical.Categories.Displayed.Constructions.Weaken as Wk +open import Cubical.Categories.Displayed.Reasoning private variable - ℓg ℓg' ℓC ℓC' ℓCᴰ ℓCᴰ' : Level + ℓg ℓg' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level + +open Section +open Functor +open UniversalElementᴰ CategoryWithTerminal' : (ℓC ℓC' : Level) → Type _ CategoryWithTerminal' ℓC ℓC' = Σ[ C ∈ Category ℓC ℓC' ] Terminal' C @@ -73,10 +82,6 @@ module _ (Ob : Type ℓg) where module _ (Cᴰ : Categoryᴰ (FreeCatw/Terminal' .fst) ℓCᴰ ℓCᴰ') (term'ᴰ : LiftedTerminalᴰ Cᴰ (FreeCatw/Terminal' .snd)) where - open import Cubical.Foundations.HLevels - open import Cubical.Categories.Displayed.Reasoning - open Section - open UniversalElementᴰ open LiftedTerminalᴰNotation Cᴰ term'ᴰ private @@ -86,8 +91,9 @@ module _ (Ob : Type ℓg) where -- given an interpretation of atomic objects module _ (ϕ : (v : Ob) → Cᴰ.ob[ inl v ]) where -- extend it to all objects - ϕ* : (v : Ob') → Cᴰ.ob[ v ] - ϕ* = Sum.elim (λ a → ϕ a) (λ b → term'ᴰ .vertexᴰ) + private + ϕ* : (v : Ob') → Cᴰ.ob[ v ] + ϕ* = Sum.elim (λ a → ϕ a) (λ b → term'ᴰ .vertexᴰ) -- and given an interpretation of atomic morphisms module _ (ψ : (e : Q .mor) → @@ -126,3 +132,31 @@ module _ (Ob : Type ℓg) where elim .F-homᴰ = elim-F-homᴰ elim .F-idᴰ = refl elim .F-seqᴰ _ _ = refl + + -- module _ + -- {D : Category ℓD ℓD'} + -- {term' : Terminal' D} + -- (F : Functor FC D) + -- (Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ') + -- (term'ᴰ : Terminalᴰ Dᴰ term') + -- where + -- private + -- module Dᴰ = Categoryᴰ Dᴰ + -- open Terminal'Notation term' + -- module _ (ϕ : ∀ o → Dᴰ.ob[ F ⟅ o ⟆ ]) where + -- private + -- ϕ* : ∀ (o' : Ob') → Dᴰ.ob[ F .F-ob o' ] + -- ϕ* = {!!} + + module _ (D : Category ℓD ℓD') + (term' : Terminal' D) + (ϕ : Ob → D .ob) + where + private + open Terminal'Notation term' + ϕ* : Ob' → D .ob + ϕ* = Sum.elim (λ a → ϕ a) λ _ → 𝟙 + + module _ (ψ : ∀ e → D [ ϕ* (Q .dom e) , ϕ* (Q .cod e) ]) where + rec : Functor FC D + rec = Wk.introS⁻ (elim (weaken FC D) (termWeaken _ term') ϕ ψ) diff --git a/Cubical/Categories/Displayed/Constructions/Weaken.agda b/Cubical/Categories/Displayed/Constructions/Weaken.agda index 47c619d3..f477ff3c 100644 --- a/Cubical/Categories/Displayed/Constructions/Weaken.agda +++ b/Cubical/Categories/Displayed/Constructions/Weaken.agda @@ -1,105 +1,5 @@ -{- - - Weaken a category to be a displayed category. - - Later: weaken a displayed category to depend on fewer parameters? - --} - {-# OPTIONS --safe #-} --- module Cubical.Categories.Displayed.Constructions.Weaken where -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Data.Sigma - -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Functor - -open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Section.Base -open import Cubical.Categories.Displayed.Properties -open import Cubical.Categories.Displayed.Functor -open import Cubical.Categories.Constructions.TotalCategory as TC - hiding (intro) -open import Cubical.Categories.Constructions.TotalCategory.More as TC - -private - variable - ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level - -open Categoryᴰ - -module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where - open Category - weaken : Categoryᴰ C ℓD ℓD' - weaken .ob[_] x = D .ob - weaken .Hom[_][_,_] f d d' = D [ d , d' ] - weaken .idᴰ = D .id - weaken ._⋆ᴰ_ = D ._⋆_ - weaken .⋆IdLᴰ = D .⋆IdL - weaken .⋆IdRᴰ = D .⋆IdR - weaken .⋆Assocᴰ = D .⋆Assoc - weaken .isSetHomᴰ = D .isSetHom - - open Functor - weakenΠ : Functor (∫C weaken) D - weakenΠ .F-ob = snd - weakenΠ .F-hom = snd - weakenΠ .F-id = refl - weakenΠ .F-seq _ _ = refl - -module _ {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'} - {E : Category ℓE ℓE'} - (F : Functor E C) - (G : Functor E D) - where - open Category - open Functor - open Section - introS : Section F (weaken C D) - introS .F-obᴰ x = G .F-ob x - introS .F-homᴰ f = G .F-hom f - introS .F-idᴰ = G .F-id - introS .F-seqᴰ _ _ = G .F-seq _ _ - -module _ {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'} - {E : Category ℓE ℓE'} - {Eᴰ : Categoryᴰ E ℓEᴰ ℓEᴰ'} - (F : Functor E C) - (G : Functor E D) - where - open Category - open Functor - open Functorᴰ - introF : Functorᴰ F Eᴰ (weaken C D) - introF .F-obᴰ {x} _ = G .F-ob x - introF .F-homᴰ {x} {y} {f} {xᴰ} {yᴰ} _ = G .F-hom f - introF .F-idᴰ = G .F-id - introF .F-seqᴰ _ _ = G .F-seq _ _ - -introS⁻ : {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'} - {E : Category ℓE ℓE'} - {F : Functor E C} - → Section F (weaken C D) - → Functor E D -introS⁻ {C = C}{D = D}{F = F} Fᴰ = - weakenΠ C D ∘F TC.intro' F Fᴰ - --- TODO: introS/introS⁻ is an Iso - -module _ {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} where - open Functor - open Functorᴰ - - weakenF : {D : Category ℓD ℓD'} {E : Category ℓE ℓE'} {F : Functor B C} - → (G : Functor D E) - → Functorᴰ F (weaken B D) (weaken C E) - weakenF G .F-obᴰ = G .F-ob - weakenF G .F-homᴰ = G .F-hom - weakenF G .F-idᴰ = G .F-id - weakenF G .F-seqᴰ = G .F-seq +open import Cubical.Categories.Displayed.Constructions.Weaken.Base public +open import Cubical.Categories.Displayed.Constructions.Weaken.Properties public diff --git a/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda b/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda new file mode 100644 index 00000000..6d9c9625 --- /dev/null +++ b/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda @@ -0,0 +1,100 @@ +{- + Weaken a category to be a displayed category. +-} +{-# OPTIONS --safe #-} +-- +module Cubical.Categories.Displayed.Constructions.Weaken.Base where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Data.Sigma + +open import Cubical.Categories.Category.Base +open import Cubical.Categories.Functor + +open import Cubical.Categories.Displayed.Base +open import Cubical.Categories.Displayed.Section.Base +open import Cubical.Categories.Displayed.Properties +open import Cubical.Categories.Displayed.Functor +open import Cubical.Categories.Constructions.TotalCategory as TC + hiding (intro) +open import Cubical.Categories.Constructions.TotalCategory.More as TC + +private + variable + ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level + +open Categoryᴰ + +module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where + open Category + weaken : Categoryᴰ C ℓD ℓD' + weaken .ob[_] x = D .ob + weaken .Hom[_][_,_] f d d' = D [ d , d' ] + weaken .idᴰ = D .id + weaken ._⋆ᴰ_ = D ._⋆_ + weaken .⋆IdLᴰ = D .⋆IdL + weaken .⋆IdRᴰ = D .⋆IdR + weaken .⋆Assocᴰ = D .⋆Assoc + weaken .isSetHomᴰ = D .isSetHom + + open Functor + weakenΠ : Functor (∫C weaken) D + weakenΠ .F-ob = snd + weakenΠ .F-hom = snd + weakenΠ .F-id = refl + weakenΠ .F-seq _ _ = refl + +module _ {C : Category ℓC ℓC'} + {D : Category ℓD ℓD'} + {E : Category ℓE ℓE'} + (F : Functor E C) + (G : Functor E D) + where + open Category + open Functor + open Section + introS : Section F (weaken C D) + introS .F-obᴰ x = G .F-ob x + introS .F-homᴰ f = G .F-hom f + introS .F-idᴰ = G .F-id + introS .F-seqᴰ _ _ = G .F-seq _ _ + +module _ {C : Category ℓC ℓC'} + {D : Category ℓD ℓD'} + {E : Category ℓE ℓE'} + {Eᴰ : Categoryᴰ E ℓEᴰ ℓEᴰ'} + (F : Functor E C) + (G : Functor E D) + where + open Category + open Functor + open Functorᴰ + introF : Functorᴰ F Eᴰ (weaken C D) + introF .F-obᴰ {x} _ = G .F-ob x + introF .F-homᴰ {x} {y} {f} {xᴰ} {yᴰ} _ = G .F-hom f + introF .F-idᴰ = G .F-id + introF .F-seqᴰ _ _ = G .F-seq _ _ + +introS⁻ : {C : Category ℓC ℓC'} + {D : Category ℓD ℓD'} + {E : Category ℓE ℓE'} + {F : Functor E C} + → Section F (weaken C D) + → Functor E D +introS⁻ {C = C}{D = D}{F = F} Fᴰ = + weakenΠ C D ∘F TC.intro' F Fᴰ + +-- TODO: introS/introS⁻ is an Iso + +module _ {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} where + open Functor + open Functorᴰ + + weakenF : {D : Category ℓD ℓD'} {E : Category ℓE ℓE'} {F : Functor B C} + → (G : Functor D E) + → Functorᴰ F (weaken B D) (weaken C E) + weakenF G .F-obᴰ = G .F-ob + weakenF G .F-homᴰ = G .F-hom + weakenF G .F-idᴰ = G .F-id + weakenF G .F-seqᴰ = G .F-seq diff --git a/Cubical/Categories/Displayed/Constructions/Weaken/Properties.agda b/Cubical/Categories/Displayed/Constructions/Weaken/Properties.agda new file mode 100644 index 00000000..76dae29d --- /dev/null +++ b/Cubical/Categories/Displayed/Constructions/Weaken/Properties.agda @@ -0,0 +1,37 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Displayed.Constructions.Weaken.Properties where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Data.Sigma + +open import Cubical.Categories.Category.Base +open import Cubical.Categories.Functor +open import Cubical.Categories.Limits.Terminal.More +open import Cubical.Categories.Presheaf + +open import Cubical.Categories.Displayed.Base +open import Cubical.Categories.Displayed.Section.Base +open import Cubical.Categories.Displayed.Properties +open import Cubical.Categories.Displayed.Functor +open import Cubical.Categories.Displayed.Limits.Terminal +open import Cubical.Categories.Constructions.TotalCategory as TC + hiding (intro) +open import Cubical.Categories.Constructions.TotalCategory.More as TC +open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk +open import Cubical.Categories.Displayed.Presheaf + +private + variable + ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level + +open Categoryᴰ +open UniversalElementᴰ +open UniversalElement +module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} + (termC : Terminal' C) (termD : Terminal' D) + where + termWeaken : LiftedTerminalᴰ (weaken C D) termC + termWeaken .vertexᴰ = termD .vertex + termWeaken .elementᴰ = termD .element + termWeaken .universalᴰ = termD .universal _ diff --git a/Gluing/Terminal.agda b/Gluing/Terminal.agda new file mode 100644 index 00000000..8cf74e61 --- /dev/null +++ b/Gluing/Terminal.agda @@ -0,0 +1,134 @@ +{-# OPTIONS --safe #-} +-- Gluing for categories with a terminal object +module Gluing.Terminal where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Structure +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) + +open import Cubical.Data.Quiver.Base as Quiver +open import Cubical.Data.List as List hiding ([_]) +open import Cubical.Data.List.Properties as List +open import Cubical.Data.Nat as Nat +open import Cubical.Data.Bool as Bool +open import Cubical.Data.Sum as Sum +open import Cubical.Data.Empty as Empty +open import Cubical.Data.Unit as Unit +open import Cubical.Data.Sigma +open import Cubical.Data.W.Indexed +open import Cubical.Relation.Nullary hiding (⟪_⟫) + +open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Limits.Terminal.More +open import Cubical.Categories.Functor +open import Cubical.Categories.Bifunctor.Redundant +open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.NaturalTransformation.More +open import Cubical.Categories.NaturalTransformation.Base +open import Cubical.Categories.Constructions.Free.CategoryWithTerminal as Free +open import Cubical.Categories.Displayed.Base +open import Cubical.Categories.Displayed.Section.Base +open import Cubical.Categories.Displayed.Properties as Disp +open import Cubical.Categories.Displayed.Base +open import Cubical.Categories.Displayed.Instances.Sets.Base +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Instances.Sets.More +open import Cubical.Categories.Functors.Constant +open import Cubical.Categories.Functors.More +open import Cubical.Categories.Functors.HomFunctor + +open import Cubical.Categories.Profunctor.General +open import Cubical.Categories.Presheaf.Representable +open import Cubical.Categories.Presheaf.More +open import Cubical.Categories.Instances.Functors.More + +open Category +-- t : ⊤ -> b +-- f : ⊤ -> b +-- d : ⊤ → ⊤ +-- +-- nothing using e + +data OB : Type ℓ-zero where + b e : OB + +discreteOB : Discrete OB +discreteOB = sectionDiscrete {A = ℕ} + (λ { zero → b ; (suc _) → e }) + (λ { b → 0 ; e → 1 }) + (λ { b → refl ; e → refl }) + discreteℕ + +isSetOB : isSet OB +isSetOB = Discrete→isSet discreteOB + +data MOR : Type ℓ-zero where + t f d : MOR + +discreteMOR : Discrete MOR +discreteMOR = sectionDiscrete {A = ℕ} + (λ { zero → t ; 1 → f ; (suc (suc _)) → d }) + (λ { t → 0 ; f → 1 ; d → 2 }) + (λ { t → refl ; f → refl ; d → refl }) + discreteℕ + +isSetMOR : isSet MOR +isSetMOR = Discrete→isSet discreteMOR + +dom cod : MOR → Ob' OB +dom t = inr _ +dom f = inr _ +dom d = inr _ + +cod t = inl b +cod f = inl b +cod d = inr _ + +QUIVER : QuiverOver _ _ +QUIVER .QuiverOver.mor = MOR +QUIVER .QuiverOver.dom = dom +QUIVER .QuiverOver.cod = cod + +FQ = Free.FC OB QUIVER +T = (Free.FCTerminal' OB QUIVER) +open Terminal'Notation T + +[b] : FQ .ob +[b] = inl b + +[t] [f] : FQ [ 𝟙 , [b] ] +[t] = ↑ t +[f] = ↑ f + +boolToExp : Bool → FQ [ 𝟙 , [b] ] +boolToExp = if_then [t] else [f] + +[t]≠[f] : ¬ ([t] ≡ [f]) +[t]≠[f] = λ p → true≢false (cong n p) where + sem : Functor FQ (SET ℓ-zero) + sem = Free.rec _ QUIVER (SET _) terminal'SET ıO λ + { t → λ _ → true ; f → λ _ → false ; d → λ _ → tt* } + where + ıO : OB → hSet ℓ-zero + ıO b = Bool , isSetBool + ıO e = ⊥ , isProp→isSet isProp⊥ + + n : FQ [ 𝟙 , [b] ] → Bool + n exp = (sem ⟪ exp ⟫) _ + +-- Goal: +-- 1. show [t] ≠ [f] +-- 2. show ∀ e : ⊤ → b . e ≡ [t] + e ≡ [f] + +-- canonicity : isEquiv boolToExp +-- canonicity = record { equiv-proof = λ exp → uniqueExists {!!} {!!} {!!} {!!} } where +-- pts : Functor FQ (SET ℓ-zero) +-- pts = FQ [ 𝟙 ,-] + +-- Canonicalize : Section pts (SETᴰ _ _) +-- Canonicalize = {!Free.elimLocal!}