-
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.
rec for free cat with terminal object, non-triviality example
- Loading branch information
Showing
5 changed files
with
315 additions
and
110 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 |
|---|---|---|
| @@ -1,105 +1,5 @@ | ||
| {- | ||
| Weaken a category to be a displayed category. | ||
| Later: weaken a displayed category to depend on fewer parameters? | ||
| -} | ||
|
|
||
| {-# OPTIONS --safe #-} | ||
| -- | ||
| module Cubical.Categories.Displayed.Constructions.Weaken where | ||
|
|
||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Foundations.HLevels | ||
| open import Cubical.Data.Sigma | ||
|
|
||
| open import Cubical.Categories.Category.Base | ||
| open import Cubical.Categories.Functor | ||
|
|
||
| open import Cubical.Categories.Displayed.Base | ||
| open import Cubical.Categories.Displayed.Section.Base | ||
| open import Cubical.Categories.Displayed.Properties | ||
| open import Cubical.Categories.Displayed.Functor | ||
| open import Cubical.Categories.Constructions.TotalCategory as TC | ||
| hiding (intro) | ||
| open import Cubical.Categories.Constructions.TotalCategory.More as TC | ||
|
|
||
| private | ||
| variable | ||
| ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level | ||
|
|
||
| open Categoryᴰ | ||
|
|
||
| module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where | ||
| open Category | ||
| weaken : Categoryᴰ C ℓD ℓD' | ||
| weaken .ob[_] x = D .ob | ||
| weaken .Hom[_][_,_] f d d' = D [ d , d' ] | ||
| weaken .idᴰ = D .id | ||
| weaken ._⋆ᴰ_ = D ._⋆_ | ||
| weaken .⋆IdLᴰ = D .⋆IdL | ||
| weaken .⋆IdRᴰ = D .⋆IdR | ||
| weaken .⋆Assocᴰ = D .⋆Assoc | ||
| weaken .isSetHomᴰ = D .isSetHom | ||
|
|
||
| open Functor | ||
| weakenΠ : Functor (∫C weaken) D | ||
| weakenΠ .F-ob = snd | ||
| weakenΠ .F-hom = snd | ||
| weakenΠ .F-id = refl | ||
| weakenΠ .F-seq _ _ = refl | ||
|
|
||
| module _ {C : Category ℓC ℓC'} | ||
| {D : Category ℓD ℓD'} | ||
| {E : Category ℓE ℓE'} | ||
| (F : Functor E C) | ||
| (G : Functor E D) | ||
| where | ||
| open Category | ||
| open Functor | ||
| open Section | ||
| introS : Section F (weaken C D) | ||
| introS .F-obᴰ x = G .F-ob x | ||
| introS .F-homᴰ f = G .F-hom f | ||
| introS .F-idᴰ = G .F-id | ||
| introS .F-seqᴰ _ _ = G .F-seq _ _ | ||
|
|
||
| module _ {C : Category ℓC ℓC'} | ||
| {D : Category ℓD ℓD'} | ||
| {E : Category ℓE ℓE'} | ||
| {Eᴰ : Categoryᴰ E ℓEᴰ ℓEᴰ'} | ||
| (F : Functor E C) | ||
| (G : Functor E D) | ||
| where | ||
| open Category | ||
| open Functor | ||
| open Functorᴰ | ||
| introF : Functorᴰ F Eᴰ (weaken C D) | ||
| introF .F-obᴰ {x} _ = G .F-ob x | ||
| introF .F-homᴰ {x} {y} {f} {xᴰ} {yᴰ} _ = G .F-hom f | ||
| introF .F-idᴰ = G .F-id | ||
| introF .F-seqᴰ _ _ = G .F-seq _ _ | ||
|
|
||
| introS⁻ : {C : Category ℓC ℓC'} | ||
| {D : Category ℓD ℓD'} | ||
| {E : Category ℓE ℓE'} | ||
| {F : Functor E C} | ||
| → Section F (weaken C D) | ||
| → Functor E D | ||
| introS⁻ {C = C}{D = D}{F = F} Fᴰ = | ||
| weakenΠ C D ∘F TC.intro' F Fᴰ | ||
|
|
||
| -- TODO: introS/introS⁻ is an Iso | ||
|
|
||
| module _ {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} where | ||
| open Functor | ||
| open Functorᴰ | ||
|
|
||
| weakenF : {D : Category ℓD ℓD'} {E : Category ℓE ℓE'} {F : Functor B C} | ||
| → (G : Functor D E) | ||
| → Functorᴰ F (weaken B D) (weaken C E) | ||
| weakenF G .F-obᴰ = G .F-ob | ||
| weakenF G .F-homᴰ = G .F-hom | ||
| weakenF G .F-idᴰ = G .F-id | ||
| weakenF G .F-seqᴰ = G .F-seq | ||
| open import Cubical.Categories.Displayed.Constructions.Weaken.Base public | ||
| open import Cubical.Categories.Displayed.Constructions.Weaken.Properties public |
100 changes: 100 additions & 0 deletions
100
Cubical/Categories/Displayed/Constructions/Weaken/Base.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,100 @@ | ||
| {- | ||
| Weaken a category to be a displayed category. | ||
| -} | ||
| {-# OPTIONS --safe #-} | ||
| -- | ||
| module Cubical.Categories.Displayed.Constructions.Weaken.Base where | ||
|
|
||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Foundations.HLevels | ||
| open import Cubical.Data.Sigma | ||
|
|
||
| open import Cubical.Categories.Category.Base | ||
| open import Cubical.Categories.Functor | ||
|
|
||
| open import Cubical.Categories.Displayed.Base | ||
| open import Cubical.Categories.Displayed.Section.Base | ||
| open import Cubical.Categories.Displayed.Properties | ||
| open import Cubical.Categories.Displayed.Functor | ||
| open import Cubical.Categories.Constructions.TotalCategory as TC | ||
| hiding (intro) | ||
| open import Cubical.Categories.Constructions.TotalCategory.More as TC | ||
|
|
||
| private | ||
| variable | ||
| ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level | ||
|
|
||
| open Categoryᴰ | ||
|
|
||
| module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where | ||
| open Category | ||
| weaken : Categoryᴰ C ℓD ℓD' | ||
| weaken .ob[_] x = D .ob | ||
| weaken .Hom[_][_,_] f d d' = D [ d , d' ] | ||
| weaken .idᴰ = D .id | ||
| weaken ._⋆ᴰ_ = D ._⋆_ | ||
| weaken .⋆IdLᴰ = D .⋆IdL | ||
| weaken .⋆IdRᴰ = D .⋆IdR | ||
| weaken .⋆Assocᴰ = D .⋆Assoc | ||
| weaken .isSetHomᴰ = D .isSetHom | ||
|
|
||
| open Functor | ||
| weakenΠ : Functor (∫C weaken) D | ||
| weakenΠ .F-ob = snd | ||
| weakenΠ .F-hom = snd | ||
| weakenΠ .F-id = refl | ||
| weakenΠ .F-seq _ _ = refl | ||
|
|
||
| module _ {C : Category ℓC ℓC'} | ||
| {D : Category ℓD ℓD'} | ||
| {E : Category ℓE ℓE'} | ||
| (F : Functor E C) | ||
| (G : Functor E D) | ||
| where | ||
| open Category | ||
| open Functor | ||
| open Section | ||
| introS : Section F (weaken C D) | ||
| introS .F-obᴰ x = G .F-ob x | ||
| introS .F-homᴰ f = G .F-hom f | ||
| introS .F-idᴰ = G .F-id | ||
| introS .F-seqᴰ _ _ = G .F-seq _ _ | ||
|
|
||
| module _ {C : Category ℓC ℓC'} | ||
| {D : Category ℓD ℓD'} | ||
| {E : Category ℓE ℓE'} | ||
| {Eᴰ : Categoryᴰ E ℓEᴰ ℓEᴰ'} | ||
| (F : Functor E C) | ||
| (G : Functor E D) | ||
| where | ||
| open Category | ||
| open Functor | ||
| open Functorᴰ | ||
| introF : Functorᴰ F Eᴰ (weaken C D) | ||
| introF .F-obᴰ {x} _ = G .F-ob x | ||
| introF .F-homᴰ {x} {y} {f} {xᴰ} {yᴰ} _ = G .F-hom f | ||
| introF .F-idᴰ = G .F-id | ||
| introF .F-seqᴰ _ _ = G .F-seq _ _ | ||
|
|
||
| introS⁻ : {C : Category ℓC ℓC'} | ||
| {D : Category ℓD ℓD'} | ||
| {E : Category ℓE ℓE'} | ||
| {F : Functor E C} | ||
| → Section F (weaken C D) | ||
| → Functor E D | ||
| introS⁻ {C = C}{D = D}{F = F} Fᴰ = | ||
| weakenΠ C D ∘F TC.intro' F Fᴰ | ||
|
|
||
| -- TODO: introS/introS⁻ is an Iso | ||
|
|
||
| module _ {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} where | ||
| open Functor | ||
| open Functorᴰ | ||
|
|
||
| weakenF : {D : Category ℓD ℓD'} {E : Category ℓE ℓE'} {F : Functor B C} | ||
| → (G : Functor D E) | ||
| → Functorᴰ F (weaken B D) (weaken C E) | ||
| weakenF G .F-obᴰ = G .F-ob | ||
| weakenF G .F-homᴰ = G .F-hom | ||
| weakenF G .F-idᴰ = G .F-id | ||
| weakenF G .F-seqᴰ = G .F-seq |
37 changes: 37 additions & 0 deletions
37
Cubical/Categories/Displayed/Constructions/Weaken/Properties.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,37 @@ | ||
| {-# OPTIONS --safe #-} | ||
| module Cubical.Categories.Displayed.Constructions.Weaken.Properties where | ||
|
|
||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Foundations.HLevels | ||
| open import Cubical.Data.Sigma | ||
|
|
||
| open import Cubical.Categories.Category.Base | ||
| open import Cubical.Categories.Functor | ||
| open import Cubical.Categories.Limits.Terminal.More | ||
| open import Cubical.Categories.Presheaf | ||
|
|
||
| open import Cubical.Categories.Displayed.Base | ||
| open import Cubical.Categories.Displayed.Section.Base | ||
| open import Cubical.Categories.Displayed.Properties | ||
| open import Cubical.Categories.Displayed.Functor | ||
| open import Cubical.Categories.Displayed.Limits.Terminal | ||
| open import Cubical.Categories.Constructions.TotalCategory as TC | ||
| hiding (intro) | ||
| open import Cubical.Categories.Constructions.TotalCategory.More as TC | ||
| open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk | ||
| open import Cubical.Categories.Displayed.Presheaf | ||
|
|
||
| private | ||
| variable | ||
| ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level | ||
|
|
||
| open Categoryᴰ | ||
| open UniversalElementᴰ | ||
| open UniversalElement | ||
| module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} | ||
| (termC : Terminal' C) (termD : Terminal' D) | ||
| where | ||
| termWeaken : LiftedTerminalᴰ (weaken C D) termC | ||
| termWeaken .vertexᴰ = termD .vertex | ||
| termWeaken .elementᴰ = termD .element | ||
| termWeaken .universalᴰ = termD .universal _ |
Oops, something went wrong.