-
Notifications
You must be signed in to change notification settings - Fork 5
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'main' of https://github.com/maxsnew/multi-poly-cats int…
…o coend
- Loading branch information
Showing
61 changed files
with
852 additions
and
1,822 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -4,3 +4,4 @@ | |
| *.log | ||
| *.synctex.gz | ||
| Everything.agda | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,128 @@ | ||
| -- The coproduct of two categories, with its universal property | ||
| {-# OPTIONS --safe #-} | ||
| module Cubical.Categories.Constructions.Coproduct where | ||
|
|
||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Foundations.Path | ||
| open import Cubical.Foundations.HLevels | ||
| open import Cubical.Foundations.Function | ||
|
|
||
| open import Cubical.Data.Sum as Sum hiding (rec; elim; _⊎_) | ||
| open import Cubical.Data.Empty as Empty 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.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.Instances.Path as PathC | ||
|
|
||
| private | ||
| variable | ||
| ℓC ℓC' ℓD ℓD' ℓE ℓE' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' : Level | ||
|
|
||
| open Category | ||
| open Categoryᴰ | ||
| open Functor | ||
| open Functorᴰ | ||
| open Section | ||
|
|
||
| module _ (C : Category ℓC ℓC')(D : Category ℓD ℓD') where | ||
| private | ||
| ⊎Ob = C .ob Sum.⊎ D .ob | ||
|
|
||
| Hom⊎ : ⊎Ob → ⊎Ob → Type (ℓ-max ℓC' ℓD') | ||
| Hom⊎ (inl c) (inl c') = Lift {j = ℓD'} $ C [ c , c' ] | ||
| Hom⊎ (inr d) (inr d') = Lift {j = ℓC'} $ D [ d , d' ] | ||
| Hom⊎ (inl c) (inr d') = ⊥* | ||
| Hom⊎ (inr d) (inl c') = ⊥* | ||
|
|
||
| -- the following inductive definition is isomorphic and very | ||
| -- slightly more ergonomic, but lives at a higher universe level | ||
| data Hom⊎' : ⊎Ob → ⊎Ob → Type (ℓ-max (ℓ-max ℓC ℓD) (ℓ-max ℓC' ℓD')) where | ||
| inl : ∀ {c c'} → C [ c , c' ] → Hom⊎' (inl c) (inl c') | ||
| inr : ∀ {d d'} → D [ d , d' ] → Hom⊎' (inr d) (inr d') | ||
|
|
||
| _⊎_ : Category (ℓ-max ℓC ℓD) (ℓ-max ℓC' ℓD') | ||
| _⊎_ .ob = ⊎Ob | ||
| _⊎_ .Hom[_,_] = Hom⊎ | ||
| _⊎_ .id {inl c} = lift $ C .id | ||
| _⊎_ .id {inr d} = lift $ D .id | ||
| _⊎_ ._⋆_ {inl c} {inl c'} {inl c''} f g = lift (f .lower ⋆⟨ C ⟩ g .lower ) | ||
| _⊎_ ._⋆_ {inr d} {inr d'} {inr d''} f g = lift (f .lower ⋆⟨ D ⟩ g .lower) | ||
| _⊎_ .⋆IdL {inl _} {inl _} f = cong lift (C .⋆IdL (f .lower)) | ||
| _⊎_ .⋆IdL {inr _} {inr _} f = cong lift (D .⋆IdL (f .lower)) | ||
| _⊎_ .⋆IdR {inl _} {inl _} f = cong lift (C .⋆IdR (f .lower)) | ||
| _⊎_ .⋆IdR {inr _} {inr _} f = cong lift (D .⋆IdR (f .lower)) | ||
| _⊎_ .⋆Assoc {inl _} {inl _} {inl _} {inl _} f g h = | ||
| cong lift (C .⋆Assoc (f .lower) (g .lower) (h .lower)) | ||
| _⊎_ .⋆Assoc {inr _} {inr _} {inr _} {inr _} f g h = | ||
| cong lift (D .⋆Assoc (f .lower) (g .lower) (h .lower)) | ||
| _⊎_ .isSetHom {inl _} {inl _} = isOfHLevelLift 2 (C .isSetHom) | ||
| _⊎_ .isSetHom {inr _} {inr _} = isOfHLevelLift 2 (D .isSetHom) | ||
| _⊎_ .isSetHom {inl _} {inr _} = isProp→isSet isProp⊥* | ||
| _⊎_ .isSetHom {inr _} {inl _} = isProp→isSet isProp⊥* | ||
|
|
||
| module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} where | ||
| -- TODO: should these be inl and inr? | ||
| Inl : Functor C (C ⊎ D) | ||
| Inl .F-ob = inl | ||
| Inl .F-hom = lift | ||
| Inl .F-id = refl | ||
| Inl .F-seq _ _ = refl | ||
|
|
||
| Inr : Functor D (C ⊎ D) | ||
| Inr .F-ob = inr | ||
| Inr .F-hom = lift | ||
| Inr .F-id = refl | ||
| Inr .F-seq _ _ = refl | ||
|
|
||
| module _ {Cᴰ : Categoryᴰ (C ⊎ D) ℓCᴰ ℓDᴰ} | ||
| (inl-case : Section Inl Cᴰ) | ||
| (inr-case : Section Inr Cᴰ) | ||
| where | ||
| elim : GlobalSection Cᴰ | ||
| elim .F-obᴰ (inl c) = inl-case .F-obᴰ c | ||
| elim .F-obᴰ (inr d) = inr-case .F-obᴰ d | ||
| elim .F-homᴰ {inl _} {inl _} f = inl-case .F-homᴰ (f .lower) | ||
| elim .F-homᴰ {inr _} {inr _} f = inr-case .F-homᴰ (f .lower) | ||
| elim .F-idᴰ {inl _} = inl-case .F-idᴰ | ||
| elim .F-idᴰ {inr _} = inr-case .F-idᴰ | ||
| elim .F-seqᴰ {inl _} {inl _} {inl _} f g = | ||
| inl-case .F-seqᴰ (f .lower) (g .lower) | ||
| elim .F-seqᴰ {inr _} {inr _} {inr _} f g = | ||
| inr-case .F-seqᴰ (f .lower) (g .lower) | ||
|
|
||
| module _ {E : Category ℓE ℓE'} | ||
| {F : Functor (C ⊎ D) E} | ||
| {Cᴰ : Categoryᴰ E ℓCᴰ ℓCᴰ'} | ||
| (inl-case : Section (F ∘F Inl) Cᴰ) | ||
| (inr-case : Section (F ∘F Inr) Cᴰ) | ||
| where | ||
| elimLocal : Section F Cᴰ | ||
| elimLocal = GlobalSectionReindex→Section _ _ | ||
| (elim (Reindex.introS _ inl-case) (Reindex.introS _ inr-case)) | ||
|
|
||
| module _ {E : Category ℓE ℓE'} | ||
| (inl-case : Functor C E) | ||
| (inr-case : Functor D E) | ||
| where | ||
| rec : Functor (C ⊎ D) E | ||
| rec = Weaken.introS⁻ {F = _} | ||
| (elim (Weaken.introS _ inl-case) | ||
| (Weaken.introS _ inr-case)) | ||
| module _ {E : Category ℓE ℓE'} | ||
| {F G : Functor (C ⊎ D) E} | ||
| (inl-case : F ∘F Inl ≡ G ∘F Inl) | ||
| (inr-case : F ∘F Inr ≡ G ∘F Inr) | ||
| where | ||
| extensionality : F ≡ G | ||
| extensionality = PathReflection (elimLocal | ||
| (reindS (Functor≡ (λ _ → refl) (λ _ → refl)) (PathReflection⁻ inl-case)) | ||
| (reindS (Functor≡ (λ _ → refl) (λ _ → refl)) (PathReflection⁻ inr-case))) | ||
|
|
||
| -- TODO: a version of extensionality for sections | ||
| -- TODO: a version of extensionality that produces a NatIso instead of a path |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
128 changes: 128 additions & 0 deletions
128
Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,128 @@ | ||
| -- Free category with a terminal object, over a Quiver | ||
| module Cubical.Categories.Constructions.Free.CategoryWithTerminal where | ||
|
|
||
| open import Cubical.Foundations.Prelude | ||
|
|
||
| open import Cubical.Categories.Category.Base | ||
| 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.Unit | ||
| open import Cubical.Categories.Displayed.Base | ||
| open import Cubical.Categories.Presheaf | ||
| 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 | ||
|
|
||
| private | ||
| variable | ||
| ℓg ℓg' ℓC ℓC' ℓCᴰ ℓCᴰ' : Level | ||
|
|
||
| CategoryWithTerminal' : (ℓC ℓC' : Level) → Type _ | ||
| CategoryWithTerminal' ℓC ℓC' = Σ[ C ∈ Category ℓC ℓC' ] Terminal' C | ||
|
|
||
| -- freely throw in a terminal object | ||
| module _ (Ob : Type ℓg) where | ||
|
|
||
| -- adjoin a new terminal object | ||
| Ob' = Ob ⊎ Unit | ||
|
|
||
| 𝟙' : Ob' | ||
| 𝟙' = inr tt | ||
|
|
||
| module _ (Q : QuiverOver Ob' ℓg') where | ||
| open Category | ||
| open QuiverOver | ||
| open UniversalElement | ||
|
|
||
| -- copied from Categories.Constructions.Free.Category.Quiver | ||
| -- and suitably modified | ||
| data Exp : Ob' → Ob' → Type (ℓ-max ℓg ℓg') where | ||
| ↑_ : ∀ g → Exp (Q .dom g) (Q .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) | ||
| !ₑ : ∀ {A} → Exp A 𝟙' | ||
| isProp!ₑ : ∀ {A} → isProp (Exp A 𝟙') | ||
|
|
||
| FC : Category _ _ | ||
| FC .ob = Ob' | ||
| FC .Hom[_,_] = Exp | ||
| FC .id = idₑ | ||
| FC ._⋆_ = _⋆ₑ_ | ||
| FC .⋆IdL = ⋆ₑIdL | ||
| FC .⋆IdR = ⋆ₑIdR | ||
| FC .⋆Assoc = ⋆ₑAssoc | ||
| FC .isSetHom = isSetExp | ||
|
|
||
| FCTerminal' : Terminal' FC | ||
| FCTerminal' .vertex = inr tt | ||
| FCTerminal' .element = tt | ||
| FCTerminal' .universal A .equiv-proof y = | ||
| uniqueExists !ₑ refl (λ _ _ _ → refl) (λ _ _ → isProp!ₑ _ _) | ||
|
|
||
| FreeCatw/Terminal' : CategoryWithTerminal' _ _ | ||
| FreeCatw/Terminal' = (FC , FCTerminal') | ||
|
|
||
| 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 | ||
| module FC = Category (FreeCatw/Terminal' .fst) | ||
| module Cᴰ = Categoryᴰ Cᴰ | ||
|
|
||
| -- 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ᴰ) | ||
|
|
||
| -- and given an interpretation of atomic morphisms | ||
| module _ (ψ : (e : Q .mor) → | ||
| Cᴰ.Hom[ ↑ e ][ ϕ* (Q .dom e) , ϕ* (Q .cod e) ]) where | ||
|
|
||
| -- extend it to all morphisms | ||
| -- (copied from | ||
| -- Cubical.Categories.Constructions.Free.Category.Quiver) | ||
| elim-F-homᴰ : ∀ {d d'} → (f : FC.Hom[ d , d' ]) → | ||
| Cᴰ.Hom[ f ][ ϕ* d , ϕ* d' ] | ||
| elim-F-homᴰ (↑ 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 g h i) = Cᴰ.⋆Assocᴰ | ||
| (elim-F-homᴰ f) (elim-F-homᴰ g) (elim-F-homᴰ h) 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-F-homᴰ {d = d} !ₑ = !tᴰ (ϕ* d) | ||
| elim-F-homᴰ {d = d} (isProp!ₑ f g i) = goal i | ||
| where | ||
| goal : elim-F-homᴰ f Cᴰ.≡[ isProp!ₑ f g ] elim-F-homᴰ g | ||
| goal = ≡[]-rectify Cᴰ | ||
| (≡[]∙ Cᴰ _ _ | ||
| (𝟙ηᴰ {f = f} (elim-F-homᴰ f)) | ||
| (symP (𝟙ηᴰ {f = g} (elim-F-homᴰ g)))) | ||
|
|
||
| elim : GlobalSection Cᴰ | ||
| elim .F-obᴰ = ϕ* | ||
| elim .F-homᴰ = elim-F-homᴰ | ||
| elim .F-idᴰ = refl | ||
| elim .F-seqᴰ _ _ = refl |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.