diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 903f8c96..145388a8 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -190,7 +190,7 @@ jobs: cd ~ git clone https://github.com/agda/cubical --branch master cd cubical - git checkout 2ae84643c74750b49865e44c05b508cb2117c740 + git checkout f77e2305673c591695052a376e1d9cd8b07dd6f1 cd .. echo "CUBICAL_DIR=$PWD/cubical" >> "$GITHUB_ENV" diff --git a/Cubical/Categories/Bifunctor/Base.agda b/Cubical/Categories/Bifunctor/Base.agda index ced03c80..b41f8864 100644 --- a/Cubical/Categories/Bifunctor/Base.agda +++ b/Cubical/Categories/Bifunctor/Base.agda @@ -15,7 +15,7 @@ open import Cubical.Foundations.Prelude hiding (Path) open import Cubical.Categories.Category open import Cubical.Categories.Functor open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.Constructions.BinProduct hiding (Fst; Snd) +open import Cubical.Categories.Constructions.BinProduct hiding (Fst; Snd; Sym) open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.Functors diff --git a/Cubical/Categories/Bifunctor/Redundant.agda b/Cubical/Categories/Bifunctor/Redundant.agda index 0c8ca873..a616a022 100644 --- a/Cubical/Categories/Bifunctor/Redundant.agda +++ b/Cubical/Categories/Bifunctor/Redundant.agda @@ -22,7 +22,7 @@ open import Cubical.Foundations.Prelude hiding (Path) open import Cubical.Categories.Category open import Cubical.Categories.Functor open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.Constructions.BinProduct hiding (Fst; Snd) +open import Cubical.Categories.Constructions.BinProduct hiding (Fst; Snd; Sym) open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.Functors import Cubical.Categories.Bifunctor as Separate diff --git a/Cubical/Categories/Constructions/BinProduct/More.agda b/Cubical/Categories/Constructions/BinProduct/More.agda index 6f130092..6a965908 100644 --- a/Cubical/Categories/Constructions/BinProduct/More.agda +++ b/Cubical/Categories/Constructions/BinProduct/More.agda @@ -23,13 +23,6 @@ private open Category open Functor --- Some more functor combinators -Δ : ∀ (C : Category ℓC ℓC') → Functor C (C ×C C) -Δ C = Id ,F Id - -Sym : {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} → Functor (C ×C D) (D ×C C) -Sym {C = C}{D = D} = Snd C D ,F Fst C D - -- helpful decomposition of morphisms used in several proofs -- about product category module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{E : Category ℓE ℓE'} where diff --git a/Cubical/Categories/Constructions/Coproduct.agda b/Cubical/Categories/Constructions/Coproduct.agda index e4a9cf32..20100ec4 100644 --- a/Cubical/Categories/Constructions/Coproduct.agda +++ b/Cubical/Categories/Constructions/Coproduct.agda @@ -17,7 +17,7 @@ open import Cubical.Categories.Functor.Base open import Cubical.Categories.Displayed.Section.Base open import Cubical.Categories.Displayed.Constructions.Weaken as Weaken -open import Cubical.Categories.Displayed.Constructions.Reindex as Reindex +open import Cubical.Categories.Displayed.Constructions.Reindex.Base as Reindex open import Cubical.Categories.Displayed.Instances.Path as PathC private diff --git a/Cubical/Categories/Constructions/Elements/More.agda b/Cubical/Categories/Constructions/Elements/More.agda deleted file mode 100644 index 43368619..00000000 --- a/Cubical/Categories/Constructions/Elements/More.agda +++ /dev/null @@ -1,53 +0,0 @@ -{-# OPTIONS --safe #-} - --- The Category of Elements - -module Cubical.Categories.Constructions.Elements.More where - -open import Cubical.Categories.Category -open import Cubical.Categories.Isomorphism - -open import Cubical.Categories.Instances.Sets -open import Cubical.Foundations.Equiv -open import Cubical.Foundations.Isomorphism -open import Cubical.Categories.Functor -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Data.Sigma -open import Cubical.Categories.Constructions.Elements - -import Cubical.Categories.Morphism as Morphism -import Cubical.Categories.Constructions.Slice as Slice - -open import Cubical.Foundations.Isomorphism.More -open import Cubical.Categories.Isomorphism.More -open import Cubical.Categories.Instances.Sets.More - -open Category -open Functor -open isUnivalent -module _ {ℓ ℓ'} {C : Category ℓ ℓ'} {ℓS} - (isUnivC : isUnivalent C) (F : Functor C (SET ℓS)) where - open Covariant {C = C} - - isUnivalent∫ : isUnivalent (∫ F) - isUnivalent∫ .univ (c , f) (c' , f') = isIsoToIsEquiv - ( isoToPath∫ - , (λ f≅f' → CatIso≡ _ _ - (Σ≡Prop (λ _ → (F ⟅ _ ⟆) .snd _ _) - (cong fst - (secEq (univEquiv isUnivC _ _) (F-Iso {F = ForgetElements F} f≅f'))))) - , λ f≡f' → ΣSquareSet (λ x → snd (F ⟅ x ⟆)) - ( cong (CatIsoToPath isUnivC) (F-pathToIso {F = ForgetElements F} f≡f') - ∙ retEq (univEquiv isUnivC _ _) (cong fst f≡f'))) where - - isoToPath∫ : ∀ {c c' f f'} - → CatIso (∫ F) (c , f) (c' , f') - → (c , f) ≡ (c' , f') - isoToPath∫ {f = f} f≅f' = ΣPathP - ( CatIsoToPath isUnivC (F-Iso {F = ForgetElements F} f≅f') - , toPathP ( (λ j → transport (λ i → fst - (F-isoToPath {F = F} isUnivC isUnivalentSET - (F-Iso {F = ForgetElements F} f≅f') (~ j) i)) f) - ∙ univSetβ (F-Iso {F = F ∘F ForgetElements F} f≅f') f - ∙ f≅f' .fst .snd)) diff --git a/Cubical/Categories/Constructions/Fiber.agda b/Cubical/Categories/Constructions/Fiber.agda index 3e966f72..2907ee9c 100644 --- a/Cubical/Categories/Constructions/Fiber.agda +++ b/Cubical/Categories/Constructions/Fiber.agda @@ -24,11 +24,12 @@ open import Cubical.Categories.Profunctor.Hom open import Cubical.Categories.Profunctor.Homomorphism.Unary open import Cubical.Categories.Profunctor.Homomorphism.Bilinear open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Properties open import Cubical.Categories.Displayed.Constructions.HomPropertyOver open import Cubical.Categories.Constructions.TotalCategory as TotalCat open import Cubical.Categories.Constructions.ChangeOfObjects + open import Cubical.Categories.Displayed.BinProduct +open import Cubical.Categories.Displayed.Constructions.Reindex.Base open import Cubical.Categories.Displayed.Constructions.BinProduct.More open import Cubical.Categories.Constructions.Endo as Endo import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning diff --git a/Cubical/Categories/Constructions/Free/CartesianCategory/Base.agda b/Cubical/Categories/Constructions/Free/CartesianCategory/Base.agda index a448ebc8..0f67a3b0 100644 --- a/Cubical/Categories/Constructions/Free/CartesianCategory/Base.agda +++ b/Cubical/Categories/Constructions/Free/CartesianCategory/Base.agda @@ -24,8 +24,7 @@ open import Cubical.Categories.Displayed.Limits.Terminal open import Cubical.Categories.Displayed.Limits.BinProduct open import Cubical.Categories.Displayed.Section.Base open import Cubical.Categories.Displayed.Presheaf -open import Cubical.Categories.Displayed.Properties -open import Cubical.Categories.Displayed.Constructions.Reindex +open import Cubical.Categories.Displayed.Constructions.Reindex.Base open import Cubical.Categories.Displayed.Constructions.Reindex.Properties open import Cubical.Categories.Displayed.Fibration.Base open import Cubical.Categories.Displayed.Constructions.Weaken as Wk diff --git a/Cubical/Categories/Constructions/Free/Category/Quiver.agda b/Cubical/Categories/Constructions/Free/Category/Quiver.agda deleted file mode 100644 index facb60c8..00000000 --- a/Cubical/Categories/Constructions/Free/Category/Quiver.agda +++ /dev/null @@ -1,147 +0,0 @@ --- Free category generated from base objects and generators --- This time not using a graph as the presentation of the generators -{-# OPTIONS --safe #-} - -module Cubical.Categories.Constructions.Free.Category.Quiver where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Path -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.HLevels - -open import Cubical.Data.Sigma -open import Cubical.Data.Quiver.Base as Quiver -open import Cubical.Data.Graph.Base as Graph -open import Cubical.Data.Graph.Displayed as Graph hiding (Section) - -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Constructions.BinProduct as BP -open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk -open import Cubical.Categories.Displayed.Instances.Path -open import Cubical.Categories.Displayed.Properties as Reindex -open import Cubical.Categories.Displayed.Constructions.Reindex as Reindex -open import Cubical.Categories.Functor.Base -open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.UnderlyingGraph hiding (Interp) - -open import Cubical.Categories.Displayed.Section.Base as Cat - -private - variable - ℓc ℓc' ℓd ℓd' ℓg ℓg' ℓh ℓh' ℓj ℓ : Level - ℓC ℓC' ℓCᴰ ℓCᴰ' : Level - -open Category -open Functor -open QuiverOver - -module _ (Q : Quiver ℓg ℓg') where - data Exp : Q .fst → Q .fst → Type (ℓ-max ℓg ℓg') where - ↑_ : ∀ g → Exp (Q .snd .dom g) (Q .snd .cod g) - idₑ : ∀ {A} → Exp A A - _⋆ₑ_ : ∀ {A B C} → (e : Exp A B) → (e' : Exp B C) → Exp A C - ⋆ₑIdL : ∀ {A B} (e : Exp A B) → idₑ ⋆ₑ e ≡ e - ⋆ₑIdR : ∀ {A B} (e : Exp A B) → e ⋆ₑ idₑ ≡ e - ⋆ₑAssoc : ∀ {A B C D} (e : Exp A B)(f : Exp B C)(g : Exp C D) - → (e ⋆ₑ f) ⋆ₑ g ≡ e ⋆ₑ (f ⋆ₑ g) - isSetExp : ∀ {A B} → isSet (Exp A B) - - FreeCat : Category _ _ - FreeCat .ob = Q .fst - FreeCat .Hom[_,_] = Exp - FreeCat .id = idₑ - FreeCat ._⋆_ = _⋆ₑ_ - FreeCat .⋆IdL = ⋆ₑIdL - FreeCat .⋆IdR = ⋆ₑIdR - FreeCat .⋆Assoc = ⋆ₑAssoc - FreeCat .isSetHom = isSetExp - - Interp : (𝓒 : Category ℓc ℓc') → Type (ℓ-max (ℓ-max (ℓ-max ℓg ℓg') ℓc) ℓc') - Interp 𝓒 = HetQG Q (Cat→Graph 𝓒) - - η : Interp FreeCat - η HetQG.$g x = x - η HetQG.<$g> e = ↑ e - - module _ {C : Category ℓC ℓC'} - (ı : Interp C) - (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where - Interpᴰ : Type _ - Interpᴰ = HetSection ı (Categoryᴰ→Graphᴰ Cᴰ) - - -- the eliminator constructs a *global* section. Use reindexing if - -- you want a local section - module _ (Cᴰ : Categoryᴰ FreeCat ℓCᴰ ℓCᴰ') - (ıᴰ : Interpᴰ η Cᴰ) - where - open HetSection - open Section - private module Cᴰ = Categoryᴰ Cᴰ - - elim-F-homᴰ : ∀ {d d'} → (f : FreeCat .Hom[_,_] d d') → - Cᴰ.Hom[ f ][ ıᴰ $gᴰ d , (ıᴰ $gᴰ d') ] - elim-F-homᴰ (↑ g) = ıᴰ <$g>ᴰ g - elim-F-homᴰ idₑ = Cᴰ.idᴰ - elim-F-homᴰ (f ⋆ₑ g) = elim-F-homᴰ f Cᴰ.⋆ᴰ elim-F-homᴰ g - elim-F-homᴰ (⋆ₑIdL f i) = Cᴰ.⋆IdLᴰ (elim-F-homᴰ f) i - elim-F-homᴰ (⋆ₑIdR f i) = Cᴰ.⋆IdRᴰ (elim-F-homᴰ f) i - elim-F-homᴰ (⋆ₑAssoc f f₁ f₂ i) = - Cᴰ.⋆Assocᴰ (elim-F-homᴰ f) (elim-F-homᴰ f₁) (elim-F-homᴰ f₂) i - elim-F-homᴰ (isSetExp f g p q i j) = isOfHLevel→isOfHLevelDep 2 - (λ x → Cᴰ.isSetHomᴰ) - (elim-F-homᴰ f) (elim-F-homᴰ g) - (cong elim-F-homᴰ p) (cong elim-F-homᴰ q) - (isSetExp f g p q) - i j - - elim : GlobalSection Cᴰ - elim .F-obᴰ = ıᴰ $gᴰ_ - elim .F-homᴰ = elim-F-homᴰ - elim .F-idᴰ = refl - elim .F-seqᴰ _ _ = refl - - -- The elimination principle for global sections implies an - -- elimination principle for local sections, this requires reindex - -- so caveat utilitor - module _ {C : Category ℓC ℓC'} - (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') - (F : Functor FreeCat C) - (ıᴰ : Interpᴰ (compGrHomHetQG (Functor→GraphHom F) η) Cᴰ) - where - private - open HetSection - F*Cᴰ = Reindex.reindex Cᴰ F - ıᴰ' : Interpᴰ η F*Cᴰ - ıᴰ' ._$gᴰ_ = ıᴰ $gᴰ_ - ıᴰ' ._<$g>ᴰ_ = ıᴰ <$g>ᴰ_ - - elimLocal : Section F Cᴰ - elimLocal = GlobalSectionReindex→Section Cᴰ F (elim F*Cᴰ ıᴰ') - - -- Elimination principle implies the recursion principle, which - -- allows for non-dependent functors to be defined - module _ {C : Category ℓC ℓC'} (ı : Interp C) where - open HetQG - private - ıᴰ : Interpᴰ η (weaken FreeCat C) - ıᴰ .HetSection._$gᴰ_ = ı .HetQG._$g_ - ıᴰ .HetSection._<$g>ᴰ_ = ı .HetQG._<$g>_ - - rec : Functor FreeCat C - rec = Wk.introS⁻ (elim (weaken FreeCat C) ıᴰ) - - -- Elimination principle also implies the uniqueness principle, - -- i.e., η law for sections/functors out of the free category - -- this version is for functors - module _ - {C : Category ℓC ℓC'} - (F G : Functor FreeCat C) - (agree-on-gen : - -- todo: some notation would simplify this considerably - Interpᴰ (compGrHomHetQG (Functor→GraphHom (F BP.,F G)) η) (PathC C)) - where - FreeCatFunctor≡ : F ≡ G - FreeCatFunctor≡ = PathReflection (elimLocal (PathC C) _ agree-on-gen) - - -- TODO: add analogous principle for Sections using PathCᴰ diff --git a/Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda b/Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda index d817b289..23726d2e 100644 --- a/Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda +++ b/Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda @@ -13,14 +13,13 @@ 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 -open import Cubical.Categories.Displayed.Properties open import Cubical.Categories.Displayed.Presheaf 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.Constructions.Reindex +open import Cubical.Categories.Displayed.Constructions.Reindex.Base open import Cubical.Categories.Displayed.Constructions.Reindex.Properties open import Cubical.Categories.Displayed.Reasoning diff --git a/Cubical/Categories/Constructions/Free/Functor/AltPresented.agda b/Cubical/Categories/Constructions/Free/Functor/AltPresented.agda index 72872f63..e3de7a16 100644 --- a/Cubical/Categories/Constructions/Free/Functor/AltPresented.agda +++ b/Cubical/Categories/Constructions/Free/Functor/AltPresented.agda @@ -1,13 +1,9 @@ -- This module defines the free category H equipped with a functor -- from a given category 𝓒 -{-# OPTIONS --safe --lossy-unification #-} +{-# OPTIONS --safe #-} module Cubical.Categories.Constructions.Free.Functor.AltPresented where open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Path -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Transport open import Cubical.Data.Sigma open import Cubical.Data.Sum as Sum hiding (rec; elim) @@ -15,9 +11,7 @@ open import Cubical.Data.Sum as Sum hiding (rec; elim) open import Cubical.Categories.Category.Base open import Cubical.Categories.Displayed.Base open import Cubical.Categories.Displayed.Functor -open import Cubical.Categories.Displayed.Properties as DCat open import Cubical.Categories.Functor.Base -open import Cubical.Categories.NaturalTransformation open import Cubical.Data.Quiver.Base @@ -25,7 +19,7 @@ open import Cubical.Categories.Displayed.Section.Base open import Cubical.Categories.Constructions.Presented as Presented open import Cubical.Categories.Constructions.BinProduct as BinProduct open import Cubical.Categories.Displayed.Constructions.Weaken as Weaken -open import Cubical.Categories.Displayed.Constructions.Reindex as Reindex +open import Cubical.Categories.Displayed.Constructions.Reindex.Base as Reindex open import Cubical.Categories.Displayed.Instances.Path as PathC open import Cubical.Categories.Constructions.Free.Category.Quiver as FreeCat hiding (rec; elim; elimLocal) diff --git a/Cubical/Categories/Constructions/Free/Profunctor.agda b/Cubical/Categories/Constructions/Free/Profunctor.agda deleted file mode 100644 index 669a1840..00000000 --- a/Cubical/Categories/Constructions/Free/Profunctor.agda +++ /dev/null @@ -1,112 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Categories.Constructions.Free.Profunctor where - --- open import Cubical.Foundations.Prelude --- open import Cubical.Foundations.Path --- open import Cubical.Foundations.Structure --- open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) --- open import Cubical.Foundations.HLevels --- open import Cubical.Categories.Category.Base --- open import Cubical.Categories.Constructions.BinProduct --- open import Cubical.Categories.Constructions.CoGraph --- open import Cubical.Categories.Functor.Base --- open import Cubical.Categories.Functors.HomFunctor --- open import Cubical.Categories.Profunctor.General --- open import Cubical.Categories.Profunctor.Morphism --- open import Cubical.Categories.NaturalTransformation.Base hiding (_⟦_⟧) --- open import Cubical.Data.Graph.Base --- open import Cubical.Data.Empty --- open import Cubical.Data.Sigma --- open import Cubical.Data.Sum - --- open import Cubical.Data.Graph.Properties --- open import Cubical.Categories.Constructions.Free.General --- open import Cubical.Categories.Constructions.Free.UnderlyingGraph - --- open import Cubical.Tactics.CategorySolver.Reflection - --- private --- variable --- ℓc ℓc' ℓd ℓd' ℓg ℓg' ℓh ℓh' ℓr ℓr' : Level - --- open Category --- open Functor --- open NatTrans - --- module FreeProfunctor (G : Graph ℓg ℓg') --- (H : Graph ℓh ℓh') --- (R : G .Node → H .Node → Type ℓr) where --- module FG = FreeCategory G --- module FH = FreeCategory H - --- data R-type : Type (ℓ-max ℓg ℓh) where --- ↑g : G .Node → R-type --- ↑h : H .Node → R-type --- data R-generator : R-type → R-type → --- Type (ℓ-max ℓr (ℓ-max (ℓ-max ℓg ℓg') (ℓ-max ℓh ℓh'))) where --- ↑g : ∀ {a b} → G .Edge a b → R-generator (↑g a) (↑g b) --- ↑h : ∀ {a b} → H .Edge a b → R-generator (↑h a) (↑h b) --- ↑r : ∀ {a b} → R a b → R-generator (↑g a) (↑h b) - --- R-graph : Graph _ _ --- R-graph .Node = R-type --- R-graph .Edge = R-generator - --- module FRcat = FreeCategory R-graph - --- G-i : Functor FG.FreeCat FRcat.FreeCat --- G-i = --- FG.Semantics.sem _ --- (record { _$g_ = ↑g ; _<$g>_ = λ x → FRcat.↑ (↑g x) }) - --- H-i : Functor FH.FreeCat FRcat.FreeCat --- H-i = --- FH.Semantics.sem _ --- (record { _$g_ = ↑h ; _<$g>_ = λ x → FRcat.↑ (↑h x) }) - --- FR : FG.FreeCat o-[ _ ]-* FH.FreeCat --- FR = HomFunctor FRcat.FreeCat ∘F ((G-i ^opF) ×F H-i) - --- ηR : ∀ {a b} → R a b → ⟨ FR ⟅ a , b ⟆ ⟩ --- ηR r = FRcat.↑ (↑r r) - --- module Semantics {𝓒 : Category ℓc ℓc'} --- {𝓓 : Category ℓd ℓd'} {𝓡 : 𝓒 o-[ ℓr' ]-* 𝓓} --- (ıG : Interp G 𝓒) --- (ıH : Interp H 𝓓) --- (ıR : ∀ {A B} → R A B → ⟨ 𝓡 ⟅ ıG $g A , ıH $g B ⟆ ⟩) --- where --- sem𝓒 = FG.Semantics.sem 𝓒 ıG --- sem𝓓 = FH.Semantics.sem 𝓓 ıH - --- open ProfHom --- CGR = CoGraph {C = 𝓒} {D = 𝓓} 𝓡 --- sem𝓡CoGraph : Functor FRcat.FreeCat CGR --- sem𝓡CoGraph = --- FRcat.Semantics.sem CGR --- (record { _$g_ = sem𝓡-ob ; _<$g>_ = sem𝓡-gen }) where --- sem𝓡-ob : R-type → CGR .ob --- sem𝓡-ob (↑g x) = inl (sem𝓒 ⟅ x ⟆ ) --- sem𝓡-ob (↑h x) = inr (sem𝓓 ⟅ x ⟆ ) - --- sem𝓡-gen : ∀ {x y} → R-generator x y → CGR [ sem𝓡-ob x , sem𝓡-ob y ] --- sem𝓡-gen (↑g x) = ↑o (ıG <$g> x) --- sem𝓡-gen (↑r x) = ↑p (ıR x) --- sem𝓡-gen (↑h x) = ↑* (ıH <$g> x) - --- sem𝓡CG-G : sem𝓡CoGraph ∘F G-i ≡ (↑oF 𝓡 ∘F sem𝓒) --- sem𝓡CG-G = FG.induction _ _ (GrHom≡ (λ v → refl) (λ e → refl)) - --- sem𝓡CG-H : sem𝓡CoGraph ∘F H-i ≡ (↑*F 𝓡 ∘F sem𝓓) --- sem𝓡CG-H = FH.induction _ _ (GrHom≡ (λ v → refl) (λ e → refl)) - --- sem𝓡 : ProfHom FR sem𝓒 sem𝓓 𝓡 --- sem𝓡 .R-hom b c x = ↑p-r 𝓡 (sem𝓡CoGraph ⟪ x ⟫) --- sem𝓡 .R-nat b' b c c' f p g = --- cong (↑p-r 𝓡) ((λ i → sem𝓡CoGraph .F-seq (p ∘⟨ FRcat.FreeCat ⟩ --- G-i ⟪ f ⟫) (H-i ⟪ g ⟫) i) --- ∙ (λ i → (sem𝓡CoGraph ⟪ H-i ⟪ g ⟫ ⟫) ∘⟨ CGR ⟩ --- sem𝓡CoGraph .F-seq (G-i ⟪ f ⟫) p i) --- ∙ λ i → sem𝓡CG-H i ⟪ g ⟫ ∘⟨ CGR ⟩ --- sem𝓡CoGraph ⟪ p ⟫ ∘⟨ CGR ⟩ sem𝓡CG-G i ⟪ f ⟫) --- ∙ ↑pH-r 𝓡 .R-nat _ _ _ _ (sem𝓒 ⟪ f ⟫) (sem𝓡CoGraph ⟪ p ⟫) (sem𝓓 ⟪ g ⟫) diff --git a/Cubical/Categories/Constructions/Quotient/More.agda b/Cubical/Categories/Constructions/Quotient/More.agda index 08020f95..75ffd3fe 100644 --- a/Cubical/Categories/Constructions/Quotient/More.agda +++ b/Cubical/Categories/Constructions/Quotient/More.agda @@ -15,7 +15,6 @@ open import Cubical.HITs.SetQuotients as SetQuotients open import Cubical.Categories.Constructions.Quotient open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Properties open import Cubical.Categories.Displayed.Section.Base open import Cubical.Categories.Displayed.Constructions.Reindex.Eq diff --git a/Cubical/Categories/Constructions/TotalCategory/More.agda b/Cubical/Categories/Constructions/TotalCategory/More.agda deleted file mode 100644 index 87e063d5..00000000 --- a/Cubical/Categories/Constructions/TotalCategory/More.agda +++ /dev/null @@ -1,129 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Categories.Constructions.TotalCategory.More 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.Constructions.TotalCategory -open import Cubical.Categories.Functor -open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Section.Base -open import Cubical.Categories.Displayed.Functor -import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning - -private - variable - ℓC ℓC' ℓD ℓD' ℓE ℓE' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' ℓEᴰ ℓEᴰ' : Level - --- Projections out of the total category -module _ {C : Category ℓC ℓC'} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} where - open Functor - open Section - - Snd : Section (Fst {Cᴰ = Cᴰ}) Cᴰ - Snd .F-obᴰ = snd - Snd .F-homᴰ = snd - Snd .F-idᴰ = refl - Snd .F-seqᴰ _ _ = refl - - module _ {D : Category ℓD ℓD'} - (F : Functor D C) - (Fᴰ : Section F Cᴰ) - where - --- A section -{- - Cᴰ - ↗ | - / | - s / | - / | - / ↓ - E ---→ C - F --} --- --- is equivalent to a functor --- intro' F s --- E ------------→ ∫ C Cᴰ --- - intro' : Functor D (∫C Cᴰ) - intro' .F-ob d = F ⟅ d ⟆ , Fᴰ .F-obᴰ _ - intro' .F-hom f = (F ⟪ f ⟫) , (Fᴰ .F-homᴰ _) - intro' .F-id = ΣPathP (F .F-id , Fᴰ .F-idᴰ) - intro' .F-seq f g = ΣPathP (F .F-seq f g , Fᴰ .F-seqᴰ _ _) - - module _ {D : Category ℓD ℓD'} - {F : Functor C D} - {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - (Fᴰ : Functorᴰ F Cᴰ Dᴰ) - where --- A displayed functor --- --- Fᴰ --- Cᴰ -----→ Dᴰ --- | | --- | | --- ↓ ↓ --- C ------→ D --- F --- --- is equivalent to a section -{- - Dᴰ - ↗ | - / | - elim Fᴰ / | - / | - / ↓ - ∫ Cᴰ ----→ D - F ∘F Fst --} - open Functorᴰ - private - module Dᴰ = Categoryᴰ Dᴰ - module R = HomᴰReasoning Dᴰ - elim : Section (F ∘F Fst) Dᴰ - elim = compFunctorᴰSection Fᴰ Snd - - module _ {D : Category ℓD ℓD'} - (F : Functor C D) - (Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ') - (Fᴰ : Section (F ∘F (Fst {Cᴰ = Cᴰ})) Dᴰ) - where - open Functorᴰ - private - module Dᴰ = Categoryᴰ Dᴰ - module R = HomᴰReasoning Dᴰ - -- this is a recursion principle for an *arbitrary* displayed - -- category Cᴰ. - - -- this is a dependent uncurry - recᴰ : Functorᴰ F Cᴰ Dᴰ - recᴰ .F-obᴰ {x} xᴰ = Fᴰ .F-obᴰ (x , xᴰ) - recᴰ .F-homᴰ {f = f} fᴰ = Fᴰ .F-homᴰ (f , fᴰ) - recᴰ .F-idᴰ = R.≡[]-rectify (Fᴰ .F-idᴰ) - recᴰ .F-seqᴰ {x} {y} {z} {f} {g} {xᴰ} {yᴰ} {zᴰ} fᴰ gᴰ = - R.≡[]-rectify (Fᴰ .F-seqᴰ (f , fᴰ) (g , gᴰ)) - - --- Total functor of a displayed functor -module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} - {F : Functor C D} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - (Fᴰ : Functorᴰ F Cᴰ Dᴰ) - where - -module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} {F : Functor C D} - {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - (Fᴰ : Functorᴰ F Cᴰ Dᴰ) where - open Functor - private - module Fᴰ = Functorᴰ Fᴰ - - -- this should be the real definition of ∫F but it's different - -- upstream. - ∫F' : Functor (∫C Cᴰ) (∫C Dᴰ) - ∫F' = intro' (F ∘F Fst {Cᴰ = Cᴰ}) (elim Fᴰ) diff --git a/Cubical/Categories/Displayed/Constructions/BinProduct/More.agda b/Cubical/Categories/Displayed/Constructions/BinProduct/More.agda index 29db71d0..0bf9e889 100644 --- a/Cubical/Categories/Displayed/Constructions/BinProduct/More.agda +++ b/Cubical/Categories/Displayed/Constructions/BinProduct/More.agda @@ -21,11 +21,9 @@ open import Cubical.Categories.Displayed.Section.Base open import Cubical.Categories.Displayed.BinProduct open import Cubical.Categories.Constructions.TotalCategory as TotalCat -open import Cubical.Categories.Constructions.TotalCategory.More - as TotalCat open import Cubical.Categories.Displayed.Constructions.TotalCategory + as TotalCatᴰ hiding (introS; introF) open import Cubical.Categories.Displayed.Instances.Terminal as Unitᴰ -open import Cubical.Categories.Displayed.Instances.Terminal.More as Unitᴰ hiding (introF) private diff --git a/Cubical/Categories/Displayed/Constructions/Comma.agda b/Cubical/Categories/Displayed/Constructions/Comma.agda index 7e53a444..ac34179e 100644 --- a/Cubical/Categories/Displayed/Constructions/Comma.agda +++ b/Cubical/Categories/Displayed/Constructions/Comma.agda @@ -25,15 +25,11 @@ open import Cubical.Categories.Isomorphism open import Cubical.Categories.NaturalTransformation open import Cubical.Categories.Displayed.Base 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.Constructions.TotalCategory as TotalCat hiding (intro) -open import Cubical.Categories.Constructions.TotalCategory.More as TotalCat open import Cubical.Categories.Displayed.Constructions.TotalCategory - as TotalCatᴰ hiding (intro) -open import Cubical.Categories.Displayed.Constructions.TotalCategory.More as TotalCatᴰ open import Cubical.Categories.Displayed.Constructions.SimpleTotalCategoryR open import Cubical.Categories.Displayed.Constructions.SimpleTotalCategoryL @@ -205,7 +201,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}{E : Category ℓE where open Functorᴰ intro : Functor B (Comma F G) - intro = TotalCat.intro' (H ,F K) αF where + intro = TotalCat.intro (H ,F K) αF where αF : Section _ _ αF = mkPropHomsSection (hasPropHomsCommaᴰ _ _) (α ⟦_⟧) @@ -245,7 +241,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}{E : Category ℓE open NatIso mkIsoCommaFunctor : Functor B (IsoComma F G) - mkIsoCommaFunctor = TotalCat.intro' (H ,F K) + mkIsoCommaFunctor = TotalCat.intro (H ,F K) (TotalCatᴰ.introS _ _ (mkPropHomsSection (hasPropHomsCommaᴰ _ _) (α .trans ⟦_⟧) diff --git a/Cubical/Categories/Displayed/Constructions/Reindex.agda b/Cubical/Categories/Displayed/Constructions/Reindex.agda deleted file mode 100644 index f7c3e965..00000000 --- a/Cubical/Categories/Displayed/Constructions/Reindex.agda +++ /dev/null @@ -1,138 +0,0 @@ -{- - - Given any displayed cat and functor to the base - - A - | - | - | - | - ↓ - Δ ----→ Γ - γ - - - There is a universal displayed category over Δ equipped with a - displayed functor - - γ* A ----→ A - | | - | | - | | - | | - ↓ ↓ - Δ -----→ Γ - γ - - - We write γ* A as reindex (defined upstream). - - The universality says that a section - - γ* A - ↗ | - / | - M / | - / | - / ↓ - Θ ---→ Δ - δ - - is equivalent to a section - - A - ↗ | - / | - / | - / | - / ↓ - Θ ---→ Γ - δγ - - that factorizes through the universal displayed functor. - --} -{-# OPTIONS --safe #-} --- -module Cubical.Categories.Displayed.Constructions.Reindex where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Data.Sigma -import Cubical.Data.Equality as Eq -import Cubical.Data.Equality.Conversion as Eq - -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Constructions.BinProduct - renaming (Fst to FstBP ; Snd to SndBP) -open import Cubical.Categories.Functor - -open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Constructions.TotalCategory -open import Cubical.Categories.Constructions.TotalCategory.More as TotalCat -open import Cubical.Categories.Displayed.Properties -open import Cubical.Categories.Displayed.Functor -open import Cubical.Categories.Displayed.Section.Base -import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning -open import Cubical.Categories.Displayed.Magmoid - -private - variable - ℓB ℓB' ℓBᴰ ℓBᴰ' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level - -open Category -open Functor - -module _ - {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} - (Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ') (F : Functor C D) - where - - private - module C = Category C - module D = Category D - - open Categoryᴰ Dᴰ - open Functor F - open Functorᴰ - - forgetReindex : Functorᴰ F (reindex Dᴰ F) Dᴰ - forgetReindex .F-obᴰ = λ z → z - forgetReindex .F-homᴰ = λ z → z - forgetReindex .F-idᴰ = symP (transport-filler _ _) - forgetReindex .F-seqᴰ fᴰ gᴰ = symP (transport-filler _ _) - - GlobalSectionReindex→Section : GlobalSection (reindex Dᴰ F) → Section F Dᴰ - GlobalSectionReindex→Section Fᴰ = compFunctorᴰGlobalSection forgetReindex Fᴰ - -module _ - {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} - {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - {F : Functor C D} - {B : Category ℓB ℓB'} - (G : Functor B C) - (FGᴰ : Section (F ∘F G) Dᴰ) - where - private - module R = HomᴰReasoning Dᴰ - open Functor - open Section - - introS : Section G (reindex Dᴰ F) - introS .F-obᴰ = FGᴰ .F-obᴰ - introS .F-homᴰ = FGᴰ .F-homᴰ - introS .F-idᴰ = R.≡[]-rectify (R.≡[]∙ _ _ (FGᴰ .F-idᴰ) (R.reind-filler _ _)) - introS .F-seqᴰ fᴰ gᴰ = - R.≡[]-rectify (R.≡[]∙ _ _ (FGᴰ .F-seqᴰ fᴰ gᴰ) (R.reind-filler _ _)) - -module _ - {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} - {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - {F : Functor C D} - {B : Category ℓB ℓB'} {Bᴰ : Categoryᴰ B ℓBᴰ ℓBᴰ'} - (G : Functor B C) - (FGᴰ : Functorᴰ (F ∘F G) Bᴰ Dᴰ) - where - introF : Functorᴰ G Bᴰ (reindex Dᴰ F) - introF = TotalCat.recᴰ _ _ (introS _ - (reindS' (Eq.refl , Eq.refl) (TotalCat.elim FGᴰ))) diff --git a/Cubical/Categories/Displayed/Constructions/Reindex/Eq.agda b/Cubical/Categories/Displayed/Constructions/Reindex/Eq.agda index 707f18ce..a48bd07d 100644 --- a/Cubical/Categories/Displayed/Constructions/Reindex/Eq.agda +++ b/Cubical/Categories/Displayed/Constructions/Reindex/Eq.agda @@ -17,11 +17,10 @@ open import Cubical.Categories.Functor open import Cubical.Categories.Displayed.Base open import Cubical.Categories.Displayed.Constructions.TotalCategory + hiding (introF; introS) open import Cubical.Categories.Constructions.TotalCategory as TotalCat hiding (intro) -open import Cubical.Categories.Constructions.TotalCategory.More as TotalCat -open import Cubical.Categories.Displayed.Properties as Reindex hiding (reindex) -import Cubical.Categories.Displayed.Constructions.Reindex as Reindex +import Cubical.Categories.Displayed.Constructions.Reindex.Base as Reindex open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Section.Base import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning diff --git a/Cubical/Categories/Displayed/Constructions/Reindex/Properties.agda b/Cubical/Categories/Displayed/Constructions/Reindex/Properties.agda index cb29117c..8574538c 100644 --- a/Cubical/Categories/Displayed/Constructions/Reindex/Properties.agda +++ b/Cubical/Categories/Displayed/Constructions/Reindex/Properties.agda @@ -16,7 +16,7 @@ open import Cubical.Categories.Functor open import Cubical.Categories.Presheaf open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Properties +open import Cubical.Categories.Displayed.Constructions.Reindex.Base hiding (π) open import Cubical.Categories.Displayed.Limits.Terminal open import Cubical.Categories.Displayed.Limits.BinProduct import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning diff --git a/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryL.agda b/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryL.agda index c0a04c03..961faade 100644 --- a/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryL.agda +++ b/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryL.agda @@ -15,18 +15,16 @@ open import Cubical.Categories.Functor open import Cubical.Categories.Displayed.Base open import Cubical.Categories.Displayed.Reasoning -open import Cubical.Categories.Displayed.Constructions.Reindex as Reindex +open import Cubical.Categories.Displayed.Constructions.Reindex.Base as Reindex hiding (introS) open import Cubical.Categories.Displayed.Constructions.Reindex.Eq as ReindexEq open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk hiding (introS; introF) -open import Cubical.Categories.Displayed.Properties open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Functor.More open import Cubical.Categories.Displayed.Instances.Terminal open import Cubical.Categories.Constructions.TotalCategory as TotalCat hiding (intro) -open import Cubical.Categories.Constructions.TotalCategory.More as TotalCat open import Cubical.Categories.Displayed.Section.Base open import Cubical.Categories.Displayed.Constructions.SimpleTotalCategoryR as STotalCatR @@ -64,7 +62,7 @@ module _ {E : Category ℓE ℓE'} (F : Functor E C) (Fᴰ : Section F (weaken C D)) - (Gᴰ : Section (Sym {C = C}{D = D} ∘F TotalCat.intro' F Fᴰ) Cᴰ) + (Gᴰ : Section (Sym {C = C}{D = D} ∘F TotalCat.intro F Fᴰ) Cᴰ) where open Section diff --git a/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryR.agda b/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryR.agda index 29f6d123..6af915fe 100644 --- a/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryR.agda +++ b/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryR.agda @@ -27,22 +27,18 @@ open import Cubical.Categories.Functor open import Cubical.Categories.Displayed.Base open import Cubical.Categories.Displayed.Section.Base open import Cubical.Categories.Displayed.Reasoning -open import Cubical.Categories.Displayed.Constructions.Reindex as Reindex +open import Cubical.Categories.Displayed.Constructions.Reindex.Base as Reindex hiding (introS; introF) open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk hiding (introS; introF) -open import Cubical.Categories.Displayed.Properties open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Functor.More open import Cubical.Categories.Displayed.Instances.Terminal open import Cubical.Categories.Constructions.TotalCategory as TotalCat hiding (intro) -open import Cubical.Categories.Constructions.TotalCategory.More as TotalCat open import Cubical.Categories.Displayed.Constructions.TotalCategory as TotalCatᴰ -open import Cubical.Categories.Displayed.Constructions.TotalCategory.More - as TotalCatᴰ hiding (introS) - + hiding (introS) private variable ℓB ℓB' ℓBᴰ ℓBᴰ' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level @@ -75,7 +71,7 @@ module _ {E : Category ℓE ℓE'} (F : Functor E C) (Fᴰ : Section F (weaken C D)) - (Gᴰ : Section (TotalCat.intro' F Fᴰ) Cᴰ) + (Gᴰ : Section (TotalCat.intro F Fᴰ) Cᴰ) where open Functorᴰ diff --git a/Cubical/Categories/Displayed/Constructions/Slice.agda b/Cubical/Categories/Displayed/Constructions/Slice.agda index 335fe7ff..a8c3c26d 100644 --- a/Cubical/Categories/Displayed/Constructions/Slice.agda +++ b/Cubical/Categories/Displayed/Constructions/Slice.agda @@ -16,12 +16,9 @@ import Cubical.Data.Equality as Eq open import Cubical.Categories.Category.Base open import Cubical.Categories.Morphism open import Cubical.Categories.Constructions.TotalCategory as TotalCat -open import Cubical.Categories.Constructions.TotalCategory.More as TotalCat open import Cubical.Categories.Displayed.Constructions.PropertyOver open import Cubical.Categories.Displayed.Constructions.TotalCategory as TotalCatᴰ -open import Cubical.Categories.Displayed.Constructions.TotalCategory.More - as TotalCatᴰ open import Cubical.Categories.Constructions.BinProduct as BP open import Cubical.Categories.Constructions.BinProduct.More as BP open import Cubical.Categories.Functor.Base @@ -30,7 +27,6 @@ open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk open import Cubical.Categories.Displayed.Constructions.Reindex.Eq as Reindex open import Cubical.Categories.Displayed.BinProduct open import Cubical.Categories.Displayed.Constructions.BinProduct.More as BPᴰ -open import Cubical.Categories.Displayed.Properties as Disp open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Functor.More open import Cubical.Categories.Displayed.Instances.Hom diff --git a/Cubical/Categories/Displayed/Constructions/TotalCategory/More.agda b/Cubical/Categories/Displayed/Constructions/TotalCategory/More.agda deleted file mode 100644 index 2473cec4..00000000 --- a/Cubical/Categories/Displayed/Constructions/TotalCategory/More.agda +++ /dev/null @@ -1,77 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Categories.Displayed.Constructions.TotalCategory.More where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels - -open import Cubical.Data.Sigma -import Cubical.Data.Equality as Eq - -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Functor -open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.HLevels -open import Cubical.Categories.Displayed.Functor -open import Cubical.Categories.Displayed.Section.Base --- open import Cubical.Categories.Displayed.Instances.Terminal -open import Cubical.Categories.Constructions.TotalCategory - as TotalCat - hiding (intro) -open import Cubical.Categories.Constructions.TotalCategory.More - as TotalCat -open import Cubical.Categories.Displayed.Constructions.TotalCategory - -private - variable - ℓC ℓC' ℓD ℓD' ℓE ℓE' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' ℓEᴰ ℓEᴰ' : Level - --- Projection out of the displayed total category -module _ {C : Category ℓC ℓC'} - {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} - (Dᴰ : Categoryᴰ (∫C Cᴰ) ℓDᴰ ℓDᴰ') - where - - open Functor - open Functorᴰ - open Section - private - module Cᴰ = Categoryᴰ Cᴰ - module Dᴰ = Categoryᴰ Dᴰ - ∫∫Cᴰ = ∫C {C = C} (∫Cᴰ Cᴰ Dᴰ) - - hasPropHoms∫Cᴰ : hasPropHoms Cᴰ → hasPropHoms Dᴰ → hasPropHoms (∫Cᴰ Cᴰ Dᴰ) - hasPropHoms∫Cᴰ ph-Cᴰ ph-Dᴰ f cᴰ cᴰ' = isPropΣ - (ph-Cᴰ f (cᴰ .fst) (cᴰ' .fst)) - (λ fᴰ → ph-Dᴰ (f , fᴰ) (cᴰ .snd) (cᴰ' .snd)) - - Assocᴰ : Functor ∫∫Cᴰ (∫C Dᴰ) - Assocᴰ .F-ob x = (x .fst , x .snd .fst) , x .snd .snd - Assocᴰ .F-hom f = (f .fst , f .snd .fst) , f .snd .snd - Assocᴰ .F-id = refl - Assocᴰ .F-seq _ _ = refl - - Assocᴰ⁻ : Functor (∫C Dᴰ) ∫∫Cᴰ - Assocᴰ⁻ .F-ob x = x .fst .fst , x .fst .snd , x .snd - Assocᴰ⁻ .F-hom f = f .fst .fst , f .fst .snd , f .snd - Assocᴰ⁻ .F-id = refl - Assocᴰ⁻ .F-seq _ _ = refl - - -- Functor into the displayed total category - module _ {E : Category ℓE ℓE'} (F : Functor E C) - (Fᴰ : Section F Cᴰ) - (Gᴰ : Section (TotalCat.intro' F Fᴰ) Dᴰ) - where - introS : Section F (∫Cᴰ Cᴰ Dᴰ) - introS .F-obᴰ d = Fᴰ .F-obᴰ d , Gᴰ .F-obᴰ d - introS .F-homᴰ f = Fᴰ .F-homᴰ f , Gᴰ .F-homᴰ f - introS .F-idᴰ = ΣPathP (Fᴰ .F-idᴰ , Gᴰ .F-idᴰ) - introS .F-seqᴰ f g = ΣPathP (Fᴰ .F-seqᴰ f g , Gᴰ .F-seqᴰ f g) - - module _ {E : Category ℓE ℓE'} {Eᴰ : Categoryᴰ E ℓEᴰ ℓEᴰ'} (F : Functor E C) - (Fᴰ : Functorᴰ F Eᴰ Cᴰ) - (Gᴰ : Section (∫F Fᴰ) Dᴰ) - where - introF : Functorᴰ F Eᴰ (∫Cᴰ Cᴰ Dᴰ) - introF = TotalCat.recᴰ _ _ (introS _ (elim Fᴰ) - (reindS' (Eq.refl , Eq.refl) Gᴰ)) - diff --git a/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda b/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda deleted file mode 100644 index 6d9c9625..00000000 --- a/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda +++ /dev/null @@ -1,100 +0,0 @@ -{- - 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 index 86a909ad..a0ee6045 100644 --- a/Cubical/Categories/Displayed/Constructions/Weaken/Properties.agda +++ b/Cubical/Categories/Displayed/Constructions/Weaken/Properties.agda @@ -2,25 +2,15 @@ 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.Foundations.Equiv open import Cubical.Categories.Category.Base -open import Cubical.Categories.Functor open import Cubical.Categories.Limits.Terminal.More open import Cubical.Categories.Limits.BinProduct.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.Displayed.Limits.BinProduct -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 diff --git a/Cubical/Categories/Displayed/Functor/More.agda b/Cubical/Categories/Displayed/Functor/More.agda index a9b76e47..aee24de3 100644 --- a/Cubical/Categories/Displayed/Functor/More.agda +++ b/Cubical/Categories/Displayed/Functor/More.agda @@ -7,10 +7,8 @@ open import Cubical.Foundations.Prelude open import Cubical.Categories.Category.Base open import Cubical.Categories.Functor import Cubical.Data.Equality as Eq -import Cubical.Data.Equality.More as Eq open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Properties open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Constructions.Weaken.Base import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning diff --git a/Cubical/Categories/Displayed/HLevels/More.agda b/Cubical/Categories/Displayed/HLevels/More.agda deleted file mode 100644 index 86eefede..00000000 --- a/Cubical/Categories/Displayed/HLevels/More.agda +++ /dev/null @@ -1,73 +0,0 @@ -{-# OPTIONS --safe #-} --- -module Cubical.Categories.Displayed.HLevels.More 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.Constructions.BinProduct - renaming (Fst to FstBP ; Snd to SndBP) -open import Cubical.Categories.Functor - -open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.HLevels -open import Cubical.Categories.Displayed.Section.Base -open import Cubical.Categories.Displayed.Properties -open import Cubical.Categories.Displayed.Functor - -private - variable - ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level - -module _ - {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} - {F : Functor C D} - {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - where - open Category - open Functor - private - module Dᴰ = Categoryᴰ Dᴰ - mkPropHomsSection : - (propHoms : hasPropHoms Dᴰ) - → (F-obᴰ : (x : C .ob) → Dᴰ.ob[ F .F-ob x ]) - → (F-homᴰ : {x y : C .ob} - (f : C [ x , y ]) → Dᴰ [ F .F-hom f ][ F-obᴰ x , F-obᴰ y ]) - → Section F Dᴰ - mkPropHomsSection propHoms F-obᴰ F-homᴰ .Section.F-obᴰ = F-obᴰ - mkPropHomsSection propHoms F-obᴰ F-homᴰ .Section.F-homᴰ = F-homᴰ - mkPropHomsSection propHoms F-obᴰ F-homᴰ .Section.F-idᴰ = - isProp→PathP (λ i → propHoms _ _ _) _ _ - mkPropHomsSection propHoms F-obᴰ F-homᴰ .Section.F-seqᴰ _ _ = - isProp→PathP (λ i → propHoms _ _ _) _ _ - - mkContrHomsSection : - (contrHoms : hasContrHoms Dᴰ) - → (F-obᴰ : (x : C .ob) → Dᴰ.ob[ F .F-ob x ]) - → Section F Dᴰ - mkContrHomsSection contrHoms F-obᴰ = mkPropHomsSection - (hasContrHoms→hasPropHoms Dᴰ contrHoms) - F-obᴰ - λ {x}{y} f → contrHoms (F .F-hom f) (F-obᴰ x) (F-obᴰ y) .fst - - module _ {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} where - private - module Cᴰ = Categoryᴰ Cᴰ - -- Alternate version: maybe Dᴰ.Hom[_][_,_] isn't always - -- contractible, but it is in the image of F-obᴰ - mkContrHomsFunctor' - : (F-obᴰ : {x : C .ob} → Cᴰ.ob[ x ] → Dᴰ.ob[ F .F-ob x ]) - → (F-homᴰ : {x y : C .ob} - {f : C [ x , y ]} {xᴰ : Cᴰ.ob[ x ]} {yᴰ : Cᴰ.ob[ y ]} - → Cᴰ [ f ][ xᴰ , yᴰ ] - → isContr (Dᴰ [ F .F-hom f ][ F-obᴰ xᴰ , F-obᴰ yᴰ ])) - → Functorᴰ F Cᴰ Dᴰ - mkContrHomsFunctor' F-obᴰ F-homᴰ .Functorᴰ.F-obᴰ = F-obᴰ - mkContrHomsFunctor' F-obᴰ F-homᴰ .Functorᴰ.F-homᴰ fᴰ = F-homᴰ fᴰ .fst - mkContrHomsFunctor' F-obᴰ F-homᴰ .Functorᴰ.F-idᴰ = - symP (toPathP (isProp→PathP (λ i → isContr→isProp (F-homᴰ Cᴰ.idᴰ)) _ _)) - mkContrHomsFunctor' F-obᴰ F-homᴰ .Functorᴰ.F-seqᴰ fᴰ gᴰ = - symP (toPathP (isProp→PathP - (λ i → isContr→isProp (F-homᴰ (fᴰ Cᴰ.⋆ᴰ gᴰ))) _ _)) diff --git a/Cubical/Categories/Displayed/Instances/Hom.agda b/Cubical/Categories/Displayed/Instances/Hom.agda index d8b6ed43..bc7fa9e3 100644 --- a/Cubical/Categories/Displayed/Instances/Hom.agda +++ b/Cubical/Categories/Displayed/Instances/Hom.agda @@ -21,8 +21,6 @@ open import Cubical.Categories.Constructions.BinProduct open import Cubical.Categories.Constructions.BinProduct.More open import Cubical.Categories.Displayed.Base open import Cubical.Categories.Displayed.HLevels -open import Cubical.Categories.Displayed.HLevels.More -open import Cubical.Categories.Displayed.Properties open import Cubical.Categories.Displayed.Instances.Terminal open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Section.Base diff --git a/Cubical/Categories/Displayed/Instances/Path.agda b/Cubical/Categories/Displayed/Instances/Path.agda deleted file mode 100644 index ada3f9fd..00000000 --- a/Cubical/Categories/Displayed/Instances/Path.agda +++ /dev/null @@ -1,78 +0,0 @@ -{- - Paths between objects as a category displayed over C × C. - - If C is univalent, this is equivalent to the IsoComma category. - - Universal property: a section of the Path bundle is a path between - functors - --} -{-# OPTIONS --safe #-} -module Cubical.Categories.Displayed.Instances.Path where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Data.Unit - -open import Cubical.Categories.Category -open import Cubical.Categories.Functor -open import Cubical.Categories.Profunctor.Relator as Relator -open import Cubical.Categories.Constructions.BinProduct -open import Cubical.Categories.Constructions.BinProduct.More -open import Cubical.Categories.Displayed.Base -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.Instances.Terminal -open import Cubical.Categories.Displayed.Constructions.StructureOver -open import Cubical.Categories.Displayed.Properties - -private - variable - ℓC ℓC' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓS ℓR : Level - -open Section -open Functor - -module _ (C : Category ℓC ℓC') where - private - module C = Category C - open StructureOver - PathC' : StructureOver (C ×C C) _ _ - PathC' .ob[_] (c , d) = c ≡ d - PathC' .Hom[_][_,_] (f , g) c≡c' d≡d' = - PathP (λ i → C.Hom[ c≡c' i , d≡d' i ]) f g - PathC' .idᴰ = λ i → C.id - PathC' ._⋆ᴰ_ f≡f' g≡g' = λ i → f≡f' i ⋆⟨ C ⟩ g≡g' i - PathC' .isPropHomᴰ = isOfHLevelPathP' 1 C.isSetHom _ _ - - PathC : Categoryᴰ (C ×C C) ℓC ℓC' - PathC = StructureOver→Catᴰ PathC' - - hasPropHomsPathC : hasPropHoms PathC - hasPropHomsPathC = hasPropHomsStructureOver PathC' - - -- The universal functor into PathC - Refl : Section (Δ C) PathC - Refl = mkPropHomsSection hasPropHomsPathC (λ _ → refl) λ _ → refl - -module _ {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'} - {F1 F2 : Functor D C} - where - -- "Equality/Path Reflection Rule" - PathReflection : - ∀ (Fᴰ : Section (F1 ,F F2) (PathC C)) → F1 ≡ F2 - PathReflection Fᴰ = Functor≡ Fᴰ.F-obᴰ Fᴰ.F-homᴰ - where module Fᴰ = Section Fᴰ - - -- Could also implement this using J and Refl, not sure which is - -- preferable - PathReflection⁻ : - F1 ≡ F2 → Section (F1 ,F F2) (PathC C) - PathReflection⁻ P = mkPropHomsSection (hasPropHomsPathC C) - (λ x i → P i .F-ob x) - λ f i → P i .F-hom f - --- TODO: there should also be a "J"-style elimination principle. diff --git a/Cubical/Categories/Displayed/Instances/Path/Displayed.agda b/Cubical/Categories/Displayed/Instances/Path/Displayed.agda index ce6efba6..c4083aba 100644 --- a/Cubical/Categories/Displayed/Instances/Path/Displayed.agda +++ b/Cubical/Categories/Displayed/Instances/Path/Displayed.agda @@ -12,25 +12,17 @@ module Cubical.Categories.Displayed.Instances.Path.Displayed where open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels -open import Cubical.Data.Unit open import Cubical.Categories.Category open import Cubical.Categories.Functor open import Cubical.Categories.Constructions.TotalCategory as TotalCategory -open import Cubical.Categories.Constructions.TotalCategory.More as TotalCategory -open import Cubical.Categories.Profunctor.Relator as Relator -open import Cubical.Categories.Constructions.BinProduct -open import Cubical.Categories.Constructions.BinProduct.More open import Cubical.Categories.Displayed.Base open import Cubical.Categories.Displayed.BinProduct open import Cubical.Categories.Displayed.Constructions.BinProduct.More as BPᴰ open import Cubical.Categories.Displayed.HLevels 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 private variable @@ -69,7 +61,7 @@ module _ {C : Category ℓC ℓC'} where -- TODO: do we need any of the alternate formulations? PathReflection : - Section (TotalCategory.intro' F (introS F M N)) PathCᴰ + Section (TotalCategory.intro F (introS F M N)) PathCᴰ → M ≡ N PathReflection M≡N i .F-obᴰ d = M≡N .F-obᴰ d i PathReflection M≡N i .F-homᴰ f = M≡N .F-homᴰ f i diff --git a/Cubical/Categories/Displayed/Instances/Terminal/More.agda b/Cubical/Categories/Displayed/Instances/Terminal/More.agda index bad93acf..ebfd3a61 100644 --- a/Cubical/Categories/Displayed/Instances/Terminal/More.agda +++ b/Cubical/Categories/Displayed/Instances/Terminal/More.agda @@ -9,11 +9,10 @@ open import Cubical.Categories.Category.Base open import Cubical.Categories.Functor open import Cubical.Categories.Instances.Terminal open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Instances.Terminal +open import Cubical.Categories.Displayed.Instances.Terminal as Terminal open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Section.Base -open import Cubical.Categories.Displayed.HLevels -open import Cubical.Categories.Displayed.Constructions.PropertyOver as PO +open import Cubical.Categories.Displayed.Fibration.Base private variable @@ -23,34 +22,23 @@ open Category open Categoryᴰ open Section open Functorᴰ +open CartesianOver module _ {C : Category ℓC ℓC'} where - hasContrHomsUnitᴰ : hasContrHoms (Unitᴰ C) - hasContrHomsUnitᴰ = hasContrHomsPropertyOver C _ + isFibrationUnitᴰ : isFibration (Unitᴰ C) + isFibrationUnitᴰ _ = CartesianOver→CartesianLift (Unitᴰ C) ue + where + ue : CartesianOver (Unitᴰ C) _ _ + ue .f*cᴰ' = tt + ue .π = tt + ue .isCartesian _ _ _ = + uniqueExists _ (isPropUnit _ _) (λ _ → isSetUnit _ _) + λ _ _ → isPropUnit _ _ - ttS : GlobalSection (Unitᴰ C) - ttS .F-obᴰ = λ _ → tt - ttS .F-homᴰ = λ _ → tt - ttS .F-idᴰ = refl - ttS .F-seqᴰ _ _ = refl - -module _ {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'} - {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - {F : Functor C D} - where - recᴰ : (s : Section F Dᴰ) → Functorᴰ F (Unitᴰ C) Dᴰ - recᴰ s .F-obᴰ {x} _ = s .F-obᴰ x - recᴰ s .F-homᴰ {f = f} _ = s .F-homᴰ f - recᴰ s .F-idᴰ = s .F-idᴰ - recᴰ s .F-seqᴰ _ _ = s .F-seqᴰ _ _ - -module _ {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'} - {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} - (F : Functor C D) where - introF : Functorᴰ F Cᴰ (Unitᴰ D) - introF .F-obᴰ = λ _ → tt - introF .F-homᴰ = λ _ → tt - introF .F-idᴰ = refl - introF .F-seqᴰ _ _ = refl + module _ (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where + preservesCartesianLiftsIntro : + PreservesCartesianLifts {Cᴰ = Cᴰ} (Terminal.introF Id) + preservesCartesianLiftsIntro _ _ _ _ _ _ _ _ = uniqueExists _ + refl + (λ _ → isSetUnit _ _) + λ _ _ → refl diff --git a/Cubical/Categories/Displayed/Instances/Terminal/Properties.agda b/Cubical/Categories/Displayed/Instances/Terminal/Properties.agda deleted file mode 100644 index c6520357..00000000 --- a/Cubical/Categories/Displayed/Instances/Terminal/Properties.agda +++ /dev/null @@ -1,47 +0,0 @@ -{-# OPTIONS --safe --lossy-unification #-} -module Cubical.Categories.Displayed.Instances.Terminal.Properties where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Data.Sigma -open import Cubical.Data.Unit -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Functor -open import Cubical.Categories.Instances.Terminal -open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Instances.Terminal -open import Cubical.Categories.Displayed.Instances.Terminal.More as Terminal -open import Cubical.Categories.Displayed.Functor -open import Cubical.Categories.Displayed.Fibration.Base -open import Cubical.Categories.Displayed.Section.Base -open import Cubical.Categories.Displayed.HLevels -open import Cubical.Categories.Displayed.Constructions.PropertyOver as PO - -private - variable - ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level - -open Category -open Categoryᴰ -open Section -open Functorᴰ -open CartesianOver - -module _ {C : Category ℓC ℓC'} where - isFibrationUnitᴰ : isFibration (Unitᴰ C) - isFibrationUnitᴰ _ = CartesianOver→CartesianLift (Unitᴰ C) ue - where - ue : CartesianOver (Unitᴰ C) _ _ - ue .f*cᴰ' = tt - ue .π = tt - ue .isCartesian _ _ _ = - uniqueExists _ (isPropUnit _ _) (λ _ → isSetUnit _ _) - λ _ _ → isPropUnit _ _ - - module _ (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where - preservesCartesianLiftsIntro : - PreservesCartesianLifts {Cᴰ = Cᴰ} (Terminal.introF Id) - preservesCartesianLiftsIntro _ _ _ _ _ _ _ _ = uniqueExists _ - refl - (λ _ → isSetUnit _ _) - λ _ _ → refl diff --git a/Cubical/Categories/Displayed/Section/Base.agda b/Cubical/Categories/Displayed/Section/Base.agda deleted file mode 100644 index 6beab3dd..00000000 --- a/Cubical/Categories/Displayed/Section/Base.agda +++ /dev/null @@ -1,306 +0,0 @@ -{- - Local Sections of a displayed category. - - Cᴰ - ↗ | - / | - s / | - / | - / ↓ - D ---→ C - F - - Every Section can be implemented as a Functorᴰ out of Unitᴰ (see - Displayed.Instances.Terminal): - - Fᴰ - D ----→ Cᴰ - ∥ | - ∥ | - ∥ | - ∥ | - ∥ ↓ - D ----→ C - F - - And vice-versa any Functorᴰ - - Fᴰ - Dᴰ ----→ Cᴰ - | | - | | - | | - | | - ↓ ↓ - D -----→ C - F - - Can be implemented as a Section (see - Displayed.Constructions.TotalCategory) - - Cᴰ - ↗ | - / | - s / | - / | - / ↓ - ∫Dᴰ ---→ C - F - - Both options are sometimes more ergonomic. One of the main - cosmetic differences is - - 1. When defining a Functorᴰ, the object of the base category is - implicit - 2. When defining a Section, the object of the base category is - explicit - - Definitionally, there is basically no difference as these are - definitional isomorphisms. - - Style advice is to use Sections by default, and use Functorᴰ only - for things like displayed adjoints where they make more sense - intuitively. - - Elimination rules are naturally stated in terms of local sections - (and often global sections, see below). Intro rules can be - formulated as either constructing a Section or a Functorᴰ. Good - style is to offer both intro for Section and intro' for Functorᴰ. - --} -{-# OPTIONS --safe #-} -module Cubical.Categories.Displayed.Section.Base where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.HLevels - -open import Cubical.Data.Sigma -import Cubical.Data.Equality as Eq -import Cubical.Data.Equality.More as Eq - -open import Cubical.Categories.Category -open import Cubical.Categories.Functor -open import Cubical.Categories.Functors.Equality -open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Functor -import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning - -private - variable - ℓB ℓB' ℓBᴰ ℓBᴰ' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level - -open Category -open Categoryᴰ -open Functor - -module _ {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'} - (F : Functor D C) - (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') - where - private - module C = Category C - module D = Category D - module Cᴰ = Categoryᴰ Cᴰ - module F = Functor F - - -- Section without a qualifier means *local* section. - record Section : Type (ℓ-max (ℓ-max ℓC ℓC') - (ℓ-max (ℓ-max ℓD ℓD') - (ℓ-max ℓCᴰ ℓCᴰ'))) - where - field - F-obᴰ : ∀ d → Cᴰ.ob[ F ⟅ d ⟆ ] - F-homᴰ : ∀ {d d'} (f : D.Hom[ d , d' ]) - → Cᴰ.Hom[ F ⟪ f ⟫ ][ F-obᴰ d , F-obᴰ d' ] - F-idᴰ : ∀ {d} → F-homᴰ (D.id {d}) Cᴰ.≡[ F .F-id ] Cᴰ.idᴰ - F-seqᴰ : ∀ {d d' d''} - → (f : D.Hom[ d , d' ])(g : D.Hom[ d' , d'' ]) - → F-homᴰ (f D.⋆ g) Cᴰ.≡[ F .F-seq f g ] F-homᴰ f Cᴰ.⋆ᴰ F-homᴰ g - -{- - A Global Section is a local section over the identity functor. - - Cᴰ - ↗ | - / | - s / | - / | - / ↓ - C ==== C - - - So global sections are by definition local sections - - All local sections can be implemented as global sections into the - reindexed displayed category. See Reindex.agda for details. - - But this isomorphism is not a definitional equality. Constructing a - local section is preferable as they are more flexible, but often - elimination principles are naturally proven first about global - sections and then generalized to local sections using reindexing. - - Style is offer both: elim to construct a local section and elim' to - construct a global section. --} - -module _ {C : Category ℓC ℓC'} - (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') - where - GlobalSection : Type _ - GlobalSection = Section Id Cᴰ - --- Reindexing a section. Makes -module _ {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'} - {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} - where - open Section - private - module Cᴰ = Categoryᴰ Cᴰ - module R = HomᴰReasoning Cᴰ - reindS : ∀ {F G}(H : Path (Functor D C) F G) → Section F Cᴰ → Section G Cᴰ - reindS H = subst (λ F → Section F Cᴰ) H - - reindS' : ∀ {F G : Functor D C} (H : FunctorEq F G) - → Section F Cᴰ - → Section G Cᴰ - reindS' {F}{G} (H-ob , H-hom) Fᴰ = record - { F-obᴰ = Gᴰ-obᴰ (F-singl .fst) - ; F-homᴰ = Gᴰ-homᴰ F-singl - ; F-idᴰ = Gᴰ-idᴰ F-singl (G .F-id) - ; F-seqᴰ = Gᴰ-seqᴰ F-singl (G .F-seq) - } where - F-singl : FunctorSingl F - F-singl = (_ , H-ob) , (_ , H-hom) - - Gᴰ-obᴰ : (G : Eq.singl (F .F-ob)) → (d : D .ob) → Cᴰ.ob[ G .fst d ] - Gᴰ-obᴰ (_ , Eq.refl) = Fᴰ .F-obᴰ - - Gᴰ-homᴰ : (G : FunctorSingl F) → ∀ {d d'} (f : D [ d , d' ]) - → Cᴰ.Hom[ G .snd .fst f - ][ Gᴰ-obᴰ (G .fst) d - , Gᴰ-obᴰ (G .fst) d' ] - Gᴰ-homᴰ ((_ , Eq.refl), (_ , Eq.refl)) = Fᴰ .F-homᴰ - - Gᴰ-idᴰ : (G : FunctorSingl F) - (G-id : ∀ {x} → G .snd .fst (D .id {x}) ≡ C .id) - → ∀ {d} → Gᴰ-homᴰ G (D .id {d}) Cᴰ.≡[ G-id ] Cᴰ.idᴰ - Gᴰ-idᴰ ((_ , Eq.refl), (_ , Eq.refl)) G-id = R.≡[]-rectify (Fᴰ .F-idᴰ) - - Gᴰ-seqᴰ : (G : FunctorSingl F) - (G-seq : ∀ {d d' d''}(f : D [ d , d' ])(g : D [ d' , d'' ]) - → G .snd .fst (f ⋆⟨ D ⟩ g) - ≡ G .snd .fst f ⋆⟨ C ⟩ G .snd .fst g) - → ∀ {d d' d'' : D .ob} (f : D [ d , d' ]) (g : D [ d' , d'' ]) - → Gᴰ-homᴰ G (f ⋆⟨ D ⟩ g) - Cᴰ.≡[ G-seq f g ] (Gᴰ-homᴰ G f Cᴰ.⋆ᴰ Gᴰ-homᴰ G g) - Gᴰ-seqᴰ ((_ , Eq.refl), (_ , Eq.refl)) G-seq f g = - R.≡[]-rectify (Fᴰ .F-seqᴰ f g) -{- - - Composition of a Section and a Functor - - Cᴰ - ↗ | - / | - s / | - / | - / ↓ - E ---→ D ---→ C - F - --} -module _ {B : Category ℓB ℓB'} - {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'} - {F : Functor C D} - {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - where - open Functor - open Section - private - module Dᴰ = Categoryᴰ Dᴰ - module R = HomᴰReasoning Dᴰ - compSectionFunctor : Section F Dᴰ → (G : Functor B C) → Section (F ∘F G) Dᴰ - compSectionFunctor Fᴰ G .F-obᴰ d = Fᴰ .F-obᴰ (G .F-ob d) - compSectionFunctor Fᴰ G .F-homᴰ f = Fᴰ .F-homᴰ (G .F-hom f) - compSectionFunctor Fᴰ G .F-idᴰ = R.≡[]-rectify (R.≡[]∙ _ _ - (cong (Fᴰ .F-homᴰ) (G .F-id)) - (Fᴰ .F-idᴰ)) - compSectionFunctor Fᴰ G .F-seqᴰ f g = R.≡[]-rectify (R.≡[]∙ _ _ - (cong (Fᴰ .F-homᴰ) (G .F-seq f g)) - (Fᴰ .F-seqᴰ (G .F-hom f) (G .F-hom g))) - -module _ {D : Category ℓD ℓD'} - {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - where - open Functor - open Section - private - module Dᴰ = Categoryᴰ Dᴰ - module R = HomᴰReasoning Dᴰ - - compGSectionFunctor : {C : Category ℓC ℓC'} - → GlobalSection Dᴰ - → (G : Functor C D) - → Section G Dᴰ - compGSectionFunctor s G = reindS' (Eq.refl , Eq.refl) (compSectionFunctor s G) -{- - - Composition of a Section and a Functorᴰ - - Fᴰ' - Cᴰ ---→ Cᴰ' - ↗ | | - / | | - s / | | - / | | - / ↓ ↓ - D ---→ C ----→ C' - F F' - --} -module _ {B : Category ℓB ℓB'} - {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'} - {F : Functor C D} - {G : Functor B C} - {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} - {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - where - open Functor - open Functorᴰ - open Section - private - module Dᴰ = Categoryᴰ Dᴰ - module Cᴰ = Categoryᴰ Cᴰ - module R = HomᴰReasoning Dᴰ - compFunctorᴰSection : Functorᴰ F Cᴰ Dᴰ → Section G Cᴰ → Section (F ∘F G) Dᴰ - compFunctorᴰSection Fᴰ Gᴰ .F-obᴰ d = Fᴰ .F-obᴰ (Gᴰ .F-obᴰ d) - compFunctorᴰSection Fᴰ Gᴰ .F-homᴰ f = Fᴰ .F-homᴰ (Gᴰ .F-homᴰ f) - compFunctorᴰSection Fᴰ Gᴰ .F-idᴰ = R.≡[]-rectify (R.≡[]∙ _ _ - (λ i → Fᴰ .F-homᴰ (Gᴰ .F-idᴰ i)) - (Fᴰ .F-idᴰ)) - compFunctorᴰSection Fᴰ Gᴰ .F-seqᴰ f g = R.≡[]-rectify (R.≡[]∙ _ _ - (λ i → Fᴰ .F-homᴰ (Gᴰ .F-seqᴰ f g i)) - (Fᴰ .F-seqᴰ (Gᴰ .F-homᴰ f) (Gᴰ .F-homᴰ g))) - -module _ {C : Category ℓC ℓC'} - {D : Category ℓD ℓD'} - {F : Functor C D} - {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} - {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - where - open Functor - open Functorᴰ - open Section - private - module Dᴰ = Categoryᴰ Dᴰ - module Cᴰ = Categoryᴰ Cᴰ - module R = HomᴰReasoning Dᴰ - - compFunctorᴰGlobalSection : Functorᴰ F Cᴰ Dᴰ → GlobalSection Cᴰ → Section F Dᴰ - compFunctorᴰGlobalSection Fᴰ Gᴰ = reindS' (Eq.refl , Eq.refl) - (compFunctorᴰSection Fᴰ Gᴰ) diff --git a/Cubical/Categories/Functors/Equality.agda b/Cubical/Categories/Functors/Equality.agda deleted file mode 100644 index 30b60b90..00000000 --- a/Cubical/Categories/Functors/Equality.agda +++ /dev/null @@ -1,38 +0,0 @@ -{-# OPTIONS --safe #-} --- -module Cubical.Categories.Functors.Equality where - -open import Cubical.Foundations.Prelude - -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Functor -import Cubical.Data.Equality as Eq -import Cubical.Data.Equality.More as Eq - -private - variable - ℓ ℓB ℓB' ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level - -module _ - {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} - (F : Functor C D) - where - open Functor - - private - module C = Category C - module D = Category D - - FunctorSingl : Type _ - FunctorSingl = Σ[ ob' ∈ Eq.singl (F .F-ob) ] - Eq.singlP (Eq.ap (λ F-ob → ∀ {x}{y} → C [ x , y ] → D [ F-ob x , F-ob y ]) - (ob' .snd)) - (F .F-hom) - - module _ (G : Functor C D) where - FunctorEq : Type _ - FunctorEq = Σ[ FG-ob ∈ F .F-ob Eq.≡ G .F-ob ] - Eq.HEq (Eq.ap (λ F-ob → ∀ {x} {y} → C [ x , y ] → D [ F-ob x , F-ob y ]) - FG-ob) - (F .F-hom) - (G .F-hom) diff --git a/Cubical/Categories/Functors/More.agda b/Cubical/Categories/Functors/More.agda index 7b13a392..c7e43940 100644 --- a/Cubical/Categories/Functors/More.agda +++ b/Cubical/Categories/Functors/More.agda @@ -63,80 +63,3 @@ ActionOnMorphisms→Functor {F₀ = F₀} F₁ .F-ob = F₀ ActionOnMorphisms→Functor {F₀ = F₀} F₁ .F-hom = F₁ .F-hom ActionOnMorphisms→Functor {F₀ = F₀} F₁ .F-id = F₁ .F-id ActionOnMorphisms→Functor {F₀ = F₀} F₁ .F-seq = F₁ .F-seq - -module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'} - {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} {E : Category ℓE ℓE'} - {G : Functor D E} - (isFullyFaithfulG : isFullyFaithful G) - where - - private - GFF : ∀ {x y} → D [ x , y ] ≃ E [ G ⟅ x ⟆ , G ⟅ y ⟆ ] - GFF = _ , (isFullyFaithfulG _ _) - - GFaith : ∀ {x y} → (D [ x , y ]) ↪ (E [ G ⟅ x ⟆ , G ⟅ y ⟆ ]) - GFaith = _ , isEquiv→isEmbedding (GFF .snd) - -- this would be convenient as FF.Reasoning - G-hom⁻ : ∀ {x y} → E [ G ⟅ x ⟆ , G ⟅ y ⟆ ] → D [ x , y ] - G-hom⁻ = invIsEq (isFullyFaithfulG _ _) - - - isFullyFaithfulPostcomposeF : isFullyFaithful (postcomposeF C G) - isFullyFaithfulPostcomposeF F F' .equiv-proof α = - uniqueExists - (natTrans (λ x → G-hom⁻ (α ⟦ x ⟧)) λ f → - isEmbedding→Inj (GFaith .snd) _ _ - ( G .F-seq _ _ - ∙ cong₂ (seq' E) refl (secEq GFF _) - ∙ α.N-hom _ - ∙ sym (cong₂ (seq' E) (secEq GFF _) refl) - ∙ sym (G .F-seq _ _))) - (makeNatTransPath (funExt λ c → secIsEq (isFullyFaithfulG _ _) (α ⟦ c ⟧))) - (λ _ → isSetNatTrans _ _) - λ β G∘β≡α → makeNatTransPath (funExt λ c → - isEmbedding→Inj (isEquiv→isEmbedding (isFullyFaithfulG _ _)) _ _ - (secIsEq (isFullyFaithfulG _ _) _ ∙ sym (cong (_⟦ c ⟧) G∘β≡α))) - - where module α = NatTrans α - -module _ {F : Functor C D} {G : Functor D E} where - open Category - open Functor - - module _ - (isFullyFaithfulF : isFullyFaithful F) - (isFullyFaithfulG : isFullyFaithful G) - where - isFullyFaithfulG∘F : isFullyFaithful (G ∘F F) - isFullyFaithfulG∘F x y = - equivIsEquiv - (compEquiv (_ , isFullyFaithfulF x y) - (_ , isFullyFaithfulG (F ⟅ x ⟆) (F ⟅ y ⟆))) - - module _ - (isFullG : isFull G) - (isFullF : isFull F) - where - isFullG∘F : isFull (G ∘F F) - isFullG∘F x y G∘F[f] = - rec - isPropPropTrunc - (λ Ff → rec - isPropPropTrunc - (λ f → ∣ f .fst , cong (G .F-hom) (f .snd) ∙ Ff .snd ∣₁) - (isFullF x y (Ff .fst))) - (isFullG (F ⟅ x ⟆) (F ⟅ y ⟆) G∘F[f]) - - module _ - (isFaithfulF : isFaithful F) - (isFaithfulG : isFaithful G) - where - - isFaithfulG∘F : isFaithful (G ∘F F) - isFaithfulG∘F x y = - isEmbedding→Inj - (compEmbedding - ((λ v → F-hom G v) , - (injEmbedding (E .isSetHom) (isFaithfulG (F ⟅ x ⟆) (F ⟅ y ⟆) _ _))) - ((λ z → F-hom F z) , - (injEmbedding (D .isSetHom) (isFaithfulF x y _ _))) .snd) diff --git a/Cubical/Categories/Instances/Sets/More.agda b/Cubical/Categories/Instances/Sets/More.agda index 7824a1d3..91232346 100644 --- a/Cubical/Categories/Instances/Sets/More.agda +++ b/Cubical/Categories/Instances/Sets/More.agda @@ -18,9 +18,6 @@ open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Constructions.BinProduct open import Cubical.Categories.Presheaf -open import Cubical.Foundations.Isomorphism.More - - private variable ℓ ℓ' : Level @@ -41,12 +38,3 @@ open Functor ×Sets : Functor ((SET ℓ) ×C (SET ℓ)) (SET ℓ) ×Sets = BifunctorToParFunctor ×SetsBif - -module _ {A}{B} (f : CatIso (SET ℓ) A B) a where - open isUnivalent - univSetβ : transport (cong fst (CatIsoToPath isUnivalentSET f)) a - ≡ f .fst a - univSetβ = (transportRefl _ - ∙ transportRefl _ - ∙ transportRefl _ - ∙ cong (f .fst) (transportRefl _ ∙ transportRefl _ )) diff --git a/Cubical/Categories/Isomorphism/More.agda b/Cubical/Categories/Isomorphism/More.agda index 080b28f3..3d434f77 100644 --- a/Cubical/Categories/Isomorphism/More.agda +++ b/Cubical/Categories/Isomorphism/More.agda @@ -10,53 +10,14 @@ open import Cubical.Categories.Category open import Cubical.Categories.Functor.Base open import Cubical.Categories.Isomorphism -open import Cubical.Foundations.Isomorphism.More private variable ℓC ℓC' ℓD ℓD' : Level open Category -open Functor -open isUnivalent -module _ {C : Category ℓC ℓC'} (isUnivC : isUnivalent C) where - op-Iso-pathToIso : ∀ {x y : C .ob} (p : x ≡ y) - → op-Iso (pathToIso {C = C} p) ≡ pathToIso {C = C ^op} p - op-Iso-pathToIso = - J (λ y p → op-Iso (pathToIso {C = C} p) ≡ pathToIso {C = C ^op} p) - (CatIso≡ _ _ refl) - - op-Iso-pathToIso' : ∀ {x y : C .ob} (p : x ≡ y) - → op-Iso (pathToIso {C = C ^op} p) ≡ pathToIso {C = C} p - op-Iso-pathToIso' = - J (λ y p → op-Iso (pathToIso {C = C ^op} p) ≡ pathToIso {C = C} p) - (CatIso≡ _ _ refl) - - isUnivalentOp : isUnivalent (C ^op) - isUnivalentOp .univ x y = isIsoToIsEquiv - ( (λ f^op → CatIsoToPath isUnivC (op-Iso f^op)) - , (λ f^op → CatIso≡ _ _ - (cong fst - (cong op-Iso ((secEq (univEquiv isUnivC _ _) (op-Iso f^op)))))) - , λ p → cong (CatIsoToPath isUnivC) (op-Iso-pathToIso' p) - ∙ retEq (univEquiv isUnivC _ _) p) - -module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{F : Functor C D} where - module _ (isUnivC : isUnivalent C) (isUnivD : isUnivalent D) where - isoToPathC = CatIsoToPath isUnivC - isoToPathD = CatIsoToPath isUnivD - - F-isoToPath : {x y : C .ob} → (f : CatIso C x y) → - isoToPathD (F-Iso {F = F} f) ≡ cong (F .F-ob) (isoToPathC f) - F-isoToPath f = isoFunInjective (equivToIso (univEquiv isUnivD _ _)) _ _ - ( secEq (univEquiv isUnivD _ _) _ - ∙ sym (sym (F-pathToIso {F = F} (isoToPathC f)) - ∙ cong (F-Iso {F = F}) (secEq (univEquiv isUnivC _ _) f))) - +open isIso module _ {C : Category ℓC ℓC'} where - open Category C - open isIso - ⋆InvLMove⁻ : {x y z : C .ob} (f : CatIso C x y) {g : C [ y , z ]}{h : C [ x , z ]} diff --git a/Cubical/Categories/Limits/Terminal/More.agda b/Cubical/Categories/Limits/Terminal/More.agda index e24e8d41..b0aec2c7 100644 --- a/Cubical/Categories/Limits/Terminal/More.agda +++ b/Cubical/Categories/Limits/Terminal/More.agda @@ -5,7 +5,6 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.Foundations.Equiv open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Isomorphism.More open import Cubical.HITs.PropositionalTruncation.Base open import Cubical.Data.Sigma open import Cubical.Data.Unit diff --git a/Cubical/Categories/Monad/Algebra.agda b/Cubical/Categories/Monad/Algebra.agda index 30ac60bb..f01daeb8 100644 --- a/Cubical/Categories/Monad/Algebra.agda +++ b/Cubical/Categories/Monad/Algebra.agda @@ -6,18 +6,14 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.HLevels + open import Cubical.Data.Sigma + open import Cubical.Categories.Category open import Cubical.Categories.Functor renaming (𝟙⟨_⟩ to funcId) -open import Cubical.Categories.NaturalTransformation.Base -open import Cubical.Categories.NaturalTransformation.Properties -open import Cubical.Categories.Functors.HomFunctor -open import Cubical.Categories.Constructions.BinProduct open import Cubical.Categories.Monad.ExtensionSystem open import Cubical.Categories.Adjoint.UniversalElements -open import Cubical.Foundations.Isomorphism.More - private variable ℓ ℓ' : Level diff --git a/Cubical/Categories/Monad/ExtensionSystem.agda b/Cubical/Categories/Monad/ExtensionSystem.agda index e12d7227..48d01593 100644 --- a/Cubical/Categories/Monad/ExtensionSystem.agda +++ b/Cubical/Categories/Monad/ExtensionSystem.agda @@ -24,9 +24,6 @@ open import Cubical.Categories.Monad.Base open import Cubical.Tactics.CategorySolver.Reflection open import Cubical.Tactics.FunctorSolver.Reflection - -open import Cubical.Foundations.Isomorphism.More - private variable ℓ ℓ' : Level diff --git a/Cubical/Categories/Monad/Strength/Cartesian/ExtensionSystem.agda b/Cubical/Categories/Monad/Strength/Cartesian/ExtensionSystem.agda index 718c3a4a..618bb149 100644 --- a/Cubical/Categories/Monad/Strength/Cartesian/ExtensionSystem.agda +++ b/Cubical/Categories/Monad/Strength/Cartesian/ExtensionSystem.agda @@ -7,12 +7,9 @@ module Cubical.Categories.Monad.Strength.Cartesian.ExtensionSystem where open import Cubical.Foundations.Prelude + open import Cubical.Categories.Category open import Cubical.Categories.Functor renaming (𝟙⟨_⟩ to funcId) -open import Cubical.Categories.NaturalTransformation.Base -open import Cubical.Categories.NaturalTransformation.Properties -open import Cubical.Categories.Functors.HomFunctor -open import Cubical.Categories.Constructions.BinProduct open import Cubical.Categories.Limits.BinProduct open import Cubical.Categories.Limits.BinProduct.More open import Cubical.Categories.Limits.Terminal @@ -20,9 +17,6 @@ open import Cubical.Categories.Limits.Terminal.More open import Cubical.Categories.Limits.Cartesian.Base open import Cubical.Categories.Comonad.Instances.Environment open import Cubical.Categories.Monad.ExtensionSystem as Monad -open import Cubical.Categories.Comonad.ExtensionSystem as - Comonad renaming (pull to comonad-pull) -open import Cubical.Categories.Isomorphism open import Cubical.Tactics.CategorySolver.Reflection diff --git a/Cubical/Categories/NaturalTransformation/More.agda b/Cubical/Categories/NaturalTransformation/More.agda index 03b9ec84..016aba62 100644 --- a/Cubical/Categories/NaturalTransformation/More.agda +++ b/Cubical/Categories/NaturalTransformation/More.agda @@ -87,15 +87,6 @@ module _ {A : Category ℓA ℓA'} (NatIso→FUNCTORIso A B β) ) -module _ {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where - open NatTrans - -- whiskering - -- αF - _∘ˡⁱ_ : ∀ {G H : Functor C D} (α : NatIso G H) → (F : Functor B C) - → NatIso (G ∘F F) (H ∘F F) - _∘ˡⁱ_ {G} {H} α F .trans = α .trans ∘ˡ F - _∘ˡⁱ_ {G} {H} α F .nIso x = α .nIso (F ⟅ x ⟆) - module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} {F G : Functor C D} (α : NatTrans F G) where isNatIso : Type _ diff --git a/Cubical/Categories/Presheaf/More.agda b/Cubical/Categories/Presheaf/More.agda index d0d1bfba..e05157d5 100644 --- a/Cubical/Categories/Presheaf/More.agda +++ b/Cubical/Categories/Presheaf/More.agda @@ -20,7 +20,6 @@ open import Cubical.Categories.Presheaf.Representable open import Cubical.Categories.Instances.Sets.More open import Cubical.Categories.Isomorphism.More -open import Cubical.Categories.Constructions.Elements.More open Category open Functor @@ -117,12 +116,3 @@ module UniversalElementNotation {ℓo}{ℓh} ( (∘ᴾAssoc C P _ _ _ ∙ cong (action C P _) β) ∙ sym β) - -module _ - {C : Category ℓ ℓ'} (isUnivC : isUnivalent C) (P : Presheaf C ℓS) where - open Contravariant - isPropUniversalElement : isProp (UniversalElement C P) - isPropUniversalElement = isOfHLevelRetractFromIso 1 - (invIso (TerminalElement≅UniversalElement C P)) - (isPropTerminal (∫ᴾ_ {C = C} P) - (isUnivalentOp (isUnivalent∫ (isUnivalentOp isUnivC) P))) diff --git a/Cubical/Categories/Profunctor/FunctorComprehension.agda b/Cubical/Categories/Profunctor/FunctorComprehension.agda index 32c4e56b..fe6d5ba9 100644 --- a/Cubical/Categories/Profunctor/FunctorComprehension.agda +++ b/Cubical/Categories/Profunctor/FunctorComprehension.agda @@ -34,33 +34,27 @@ open import Cubical.Data.Sigma open import Cubical.Data.Sigma.More open import Cubical.Data.Unit -open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Category open import Cubical.Categories.Functor -open import Cubical.Categories.Functors.More +open import Cubical.Categories.Functor.ComposeProperty open import Cubical.Categories.Isomorphism open import Cubical.Categories.Instances.Functors open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.NaturalTransformation.More open import Cubical.Categories.Displayed.Constructions.PropertyOver -open import Cubical.Categories.Isomorphism.More open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Instances.Sets.More open import Cubical.Categories.Constructions.BinProduct open import Cubical.Categories.Presheaf.Base open import Cubical.Categories.Presheaf.Properties open import Cubical.Categories.Presheaf.Representable open import Cubical.Categories.Presheaf.More -open import Cubical.Categories.Instances.Functors.More open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Constructions.Comma open import Cubical.Categories.Displayed.Constructions.Graph open import Cubical.Categories.Displayed.Constructions.Weaken.Base open import Cubical.Categories.Displayed.Base open import Cubical.Categories.Displayed.HLevels -open import Cubical.Categories.Displayed.HLevels.More open import Cubical.Categories.Displayed.Constructions.SimpleTotalCategoryL open import Cubical.Categories.Constructions.TotalCategory as TotalCat -open import Cubical.Categories.Constructions.TotalCategory.More as TotalCat open import Cubical.Categories.Displayed.Constructions.TotalCategory as TotalCatᴰ open import Cubical.Categories.Yoneda @@ -228,7 +222,7 @@ module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} private 𝓟 = PresheafCategory D ℓS Pup : Functor C (𝓟up D ℓS) - Pup = TotalCat.intro' P + Pup = TotalCat.intro P (mkContrHomsSection (hasContrHomsPropertyOver _ _) ues) Pus : Functor C (𝓟us D ℓS) diff --git a/Cubical/Data/Equality/More.agda b/Cubical/Data/Equality/More.agda deleted file mode 100644 index d3e50764..00000000 --- a/Cubical/Data/Equality/More.agda +++ /dev/null @@ -1,26 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Data.Equality.More where - -open import Cubical.Foundations.Prelude - using (Type; Level; ℓ-zero; ℓ-suc; ℓ-max; Σ; Σ-syntax; _,_) - - --- Import the builtin equality type defined as an inductive family -open import Agda.Builtin.Equality - -private - variable - a b ℓ ℓ' : Level - A : Type a - B : Type b - x y z : A -open import Cubical.Data.Equality.Base - -HEq : {A0 A1 : Type ℓ}(Aeq : A0 ≡ A1) (a0 : A0)(a1 : A1) → Type _ -HEq Aeq a0 a1 = transport (λ A → A) Aeq a0 ≡ a1 - -singlP : {A0 A1 : Type ℓ}(Aeq : A0 ≡ A1) (a : A0) → Type _ -singlP {A1 = A1} Aeq a = Σ[ x ∈ A1 ] HEq Aeq a x - -singl : {A : Type ℓ}(a : A) → Type _ -singl {A = A} a = singlP refl a diff --git a/Cubical/Data/Graph/Displayed.agda b/Cubical/Data/Graph/Displayed.agda deleted file mode 100644 index 34c1df19..00000000 --- a/Cubical/Data/Graph/Displayed.agda +++ /dev/null @@ -1,53 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Data.Graph.Displayed where - -open import Cubical.Foundations.Prelude -open import Cubical.Data.Graph.Base -open import Cubical.Data.Sigma -open import Cubical.Categories.Category.Base -open import Cubical.Categories.UnderlyingGraph -open import Cubical.Categories.Displayed.Base - -private - variable - ℓc ℓc' ℓcᴰ ℓcᴰ' ℓd ℓd' ℓg ℓg' ℓgᴰ ℓgᴰ' ℓh ℓh' ℓhᴰ ℓhᴰ' ℓj ℓ : Level - -open Graph -module _ (G : Graph ℓg ℓg') where - record Graphᴰ ℓgᴰ ℓgᴰ' : Type (ℓ-max (ℓ-max ℓg ℓg') (ℓ-suc (ℓ-max ℓgᴰ ℓgᴰ'))) - where - no-eta-equality - field - Node[_] : G .Node → Type ℓgᴰ - Edge[_][_,_] : ∀ {u v} (e : G .Edge u v) (uᴰ : Node[ u ]) (vᴰ : Node[ v ]) - → Type ℓgᴰ' - -open Graphᴰ -open Categoryᴰ - -module _ {G : Graph ℓg ℓg'}{H : Graph ℓh ℓh'} - (ϕ : GraphHom G H) - (Hᴰ : Graphᴰ H ℓhᴰ ℓhᴰ') - where - private - module G = Graph G - module Hᴰ = Graphᴰ Hᴰ - open GraphHom - record Section : Type (ℓ-max (ℓ-max ℓg ℓg') - (ℓ-max (ℓ-max ℓh ℓh') - (ℓ-max ℓhᴰ ℓhᴰ'))) where - field - _$gᴰ_ : ∀ (u : G.Node) → Hᴰ.Node[ ϕ $g u ] - _<$g>ᴰ_ : - ∀ {u v : G.Node} → (e : G.Edge u v) - → Hᴰ.Edge[ ϕ <$g> e ][ _$gᴰ_ u , _$gᴰ_ v ] - -Categoryᴰ→Graphᴰ : {C : Category ℓc ℓc'}(Cᴰ : Categoryᴰ C ℓcᴰ ℓcᴰ') - → Graphᴰ (Cat→Graph C) ℓcᴰ ℓcᴰ' -Categoryᴰ→Graphᴰ Cᴰ .Node[_] = Cᴰ .ob[_] -Categoryᴰ→Graphᴰ Cᴰ .Edge[_][_,_] = Cᴰ .Hom[_][_,_] - --- TODO --- CatSection→GrSection : {C : Category ℓc ℓc'}{Cᴰ : Categoryᴰ C ℓcᴰ ℓcᴰ'} --- → Cat.Section F Cᴰ --- → Section diff --git a/Cubical/Data/Quiver/Base.agda b/Cubical/Data/Quiver/Base.agda deleted file mode 100644 index f7ce3080..00000000 --- a/Cubical/Data/Quiver/Base.agda +++ /dev/null @@ -1,117 +0,0 @@ --- A Quiver is an endo-span of types. --- ob <- mor -> ob --- This is often used in set theory as the data over which a category --- is defined to be algebraic structure. - --- A Quiver is equivalent to a Graph (modulo universe issues), but --- they are not definitionally isomorphic: turning a quiver into a --- graph introduces a Path between objects/nodes in the definition of --- an Edge. - --- Since avoiding Paths generally leads to cleaner code, Graphs or --- Quivers may be preferable depending on the variance of a --- construction. - --- 1. *Using* a Graph generally requires fewer paths between --- objects. For instance, Graphs are preferable to be used in the --- definition of a category because composition can be defined by --- sharing a common middle variable Hom[ A , B ] × Hom[ B , C ] → --- Hom[ A , C ], which in a Quiver would need a path (e e' : mor) → --- (cod e ≡ dom e') → mor. --- --- 2. *Producing* a Quiver generally requires fewer paths between --- objects. For instance, Quivers are preferable to be used in the --- definition of generating data for free and presented categories. --- As an example, the "Funny tensor product" C ⊗ D of categories is --- defined by generators and relations. The generators are easy to --- define as a Quiver, but if defined as a graph, then the --- generators require a path between objects. - --- So as a principle, to get the most general definitions, --- 1. *Produce* Graphs --- 2. *Use* Quivers --- when you can get away with it. - -{-# OPTIONS --safe #-} -module Cubical.Data.Quiver.Base where - -open import Cubical.Foundations.Prelude -open import Cubical.Data.Graph.Base -open import Cubical.Data.Graph.Displayed as DG hiding (Section) -open import Cubical.Data.Sigma -open import Cubical.Categories.Category.Base -open import Cubical.Categories.UnderlyingGraph -open import Cubical.Categories.Displayed.Base - -private - variable - ℓC ℓC' ℓg ℓg' ℓgᴰ ℓgᴰ' ℓq ℓq' ℓh ℓh' ℓj ℓ : Level - --- Useful in certain applications to separate this into components -record QuiverOver (ob : Type ℓg) ℓg' : Type (ℓ-suc (ℓ-max ℓg ℓg')) where - field - mor : Type ℓg' - dom : mor → ob - cod : mor → ob - -open QuiverOver -Quiver : ∀ ℓg ℓg' → Type _ -Quiver ℓg ℓg' = Σ[ ob ∈ Type ℓg ] QuiverOver ob ℓg' - --- A "heteromorphism" from a Quiver to a Graph -record HetQG (Q : Quiver ℓq ℓq') (G : Graph ℓg ℓg') - : Type (ℓ-max (ℓ-max ℓq ℓq') (ℓ-max ℓg ℓg')) where - field - _$g_ : Q .fst → G .Node - _<$g>_ : (e : Q .snd .mor) - → G .Edge (_$g_ (Q .snd .dom e)) (_$g_ (Q .snd .cod e)) -open HetQG public - -module _ {G : Graph ℓg ℓg'} - {H : Graph ℓh ℓh'} - {Q : Quiver ℓq ℓq'} - where - compGrHomHetQG : GraphHom G H → HetQG Q G → HetQG Q H - compGrHomHetQG ϕ h ._$g_ q = ϕ GraphHom.$g (h HetQG.$g q) - compGrHomHetQG ϕ h ._<$g>_ e = ϕ GraphHom.<$g> (h HetQG.<$g> e) - --- Universal property: --- HetQG Q G ≅ QHom Q (Graph→Quiver G) -Graph→Quiver : Graph ℓg ℓg' → Quiver ℓg (ℓ-max ℓg ℓg') -Graph→Quiver g .fst = g .Node -Graph→Quiver g .snd .mor = Σ[ A ∈ g .Node ] Σ[ B ∈ g .Node ] g .Edge A B -Graph→Quiver g .snd .dom x = x .fst -Graph→Quiver g .snd .cod x = x .snd .fst - --- | The use of ≡ in this definition is the raison d'etre for the --- | Quiver-Graph distinction --- HetQG Q G ≅ QHom (Quiver→Graph Q) G -Quiver→Graph : Quiver ℓq ℓq' → Graph _ _ -Quiver→Graph Q .Node = Q .fst -Quiver→Graph Q .Edge A B = - Σ[ e ∈ Q .snd .mor ] - (Q .snd .dom e ≡ A) - × (Q .snd .cod e ≡ B) - -Cat→Quiver : Category ℓC ℓC' → Quiver _ _ -Cat→Quiver 𝓒 = Graph→Quiver (Cat→Graph 𝓒) - --- A "heterogeneous" local section of a displayed graph -module _ {Q : Quiver ℓq ℓq'}{G : Graph ℓg ℓg'} - (ϕ : HetQG Q G) - (Gᴰ : Graphᴰ G ℓgᴰ ℓgᴰ') - where - private --- module G = Graph G --- module H = Graph H - module Gᴰ = Graphᴰ Gᴰ - open HetQG - record HetSection : Type (ℓ-max (ℓ-max ℓq ℓq') - (ℓ-max (ℓ-max ℓg ℓg') - (ℓ-max ℓgᴰ ℓgᴰ'))) where - field - _$gᴰ_ : ∀ (u : Q .fst) → Gᴰ.Node[ ϕ $g u ] - _<$g>ᴰ_ : ∀ (e : Q .snd .mor) - → Gᴰ.Edge[ ϕ <$g> e - ][ _$gᴰ_ (Q .snd .dom e) - , _$gᴰ_ (Q .snd .cod e) ] diff --git a/Cubical/Data/Sigma/More.agda b/Cubical/Data/Sigma/More.agda index 80edf8d2..9f804dde 100644 --- a/Cubical/Data/Sigma/More.agda +++ b/Cubical/Data/Sigma/More.agda @@ -1,6 +1,3 @@ -{- - --} {-# OPTIONS --safe #-} module Cubical.Data.Sigma.More where diff --git a/Cubical/Foundations/Isomorphism/More.agda b/Cubical/Foundations/Isomorphism/More.agda deleted file mode 100644 index 058388ce..00000000 --- a/Cubical/Foundations/Isomorphism/More.agda +++ /dev/null @@ -1,20 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Foundations.Isomorphism.More where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Equiv.Base -open import Cubical.Foundations.Isomorphism - -private - variable - ℓ ℓ' : Level - A B C : Type ℓ - -isoToIsIso : {f : A → B} → isIso f → Iso A B -isoToIsIso {f = f} fIsIso .Iso.fun = f -isoToIsIso fIsIso .Iso.inv = fIsIso .fst -isoToIsIso fIsIso .Iso.rightInv = fIsIso .snd .fst -isoToIsIso fIsIso .Iso.leftInv = fIsIso .snd .snd - -isIsoToIsEquiv : {f : A → B} → isIso f → isEquiv f -isIsoToIsEquiv fIsIso = isoToIsEquiv (isoToIsIso fIsIso) diff --git a/Cubical/Tactics/AltFunctorSolver/Solver.agda b/Cubical/Tactics/AltFunctorSolver/Solver.agda index e1883cb0..c5131012 100644 --- a/Cubical/Tactics/AltFunctorSolver/Solver.agda +++ b/Cubical/Tactics/AltFunctorSolver/Solver.agda @@ -2,10 +2,6 @@ module Cubical.Tactics.AltFunctorSolver.Solver where open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) -open import Cubical.Foundations.GroupoidLaws -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Path open import Cubical.Data.Sum as Sum open import Cubical.Data.Quiver.Base as Quiver @@ -14,15 +10,8 @@ open import Cubical.Categories.Category open import Cubical.Categories.Constructions.Power open import Cubical.Categories.Functor renaming (Id to IdF) open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.UnderlyingGraph -open import Cubical.Categories.Displayed.Base -open import Cubical.Categories.Displayed.Constructions.Weaken as Weaken -open import Cubical.Categories.Displayed.Instances.Path.Displayed -open import Cubical.Categories.Displayed.Functor.More open import Cubical.Categories.Displayed.Section.Base -open import Cubical.Categories.Displayed.Properties open import Cubical.Categories.Constructions.Free.Category.Quiver as FreeCat open import Cubical.Categories.Constructions.Free.Functor.AltPresented diff --git a/Gluing/Category.agda b/Gluing/Category.agda index 84823f0e..80e66eb3 100644 --- a/Gluing/Category.agda +++ b/Gluing/Category.agda @@ -2,8 +2,6 @@ module Gluing.Category where open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Equiv -open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.HLevels open import Cubical.Foundations.Structure @@ -14,7 +12,6 @@ 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 (⟪_⟫) @@ -22,19 +19,10 @@ open import Cubical.Categories.Category renaming (isIso to isIsoC) open import Cubical.Categories.Functor open import Cubical.Categories.Constructions.Free.Category.Quiver as Free 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 private variable diff --git a/Gluing/Terminal.agda b/Gluing/Terminal.agda index 08abd317..c69aa0bf 100644 --- a/Gluing/Terminal.agda +++ b/Gluing/Terminal.agda @@ -4,50 +4,25 @@ 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.Displayed.Instances.Sets.Properties open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Instances.Sets.More open import Cubical.Categories.Instances.Sets.Properties -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 open Section