Displayed Category Constructions #1108
Conversation
|
Same here, I don't know the problem. |
|
Could it be that I'm merging in a branch with a name that isn't |
| (isProp→isSet (isPropHomP _ _ _ _)) | ||
| (Cᴰ .isSetHomᴰ) | ||
|
|
||
| -- Examples of ∃F instantiated |
There was a problem hiding this comment.
I thought I'd at least try to demonstrate to y'all that this construction does indeed generalize what we'd discussed in #1106
These examples can probably be removed though
|
Now the button to run CI appeared. Not sure what changed, but I clicked it. |
I pushed another commit to fix a naming typo. Seems like that did the trick |
| @@ -0,0 +1,173 @@ | |||
| {-# OPTIONS --safe #-} | |||
| -- | |||
| module Cubical.Categories.Displayed.AdjointToReindex where | |||
There was a problem hiding this comment.
Adjoint isn't specific enough. It's the left adjoint. (I'm not sure if the right adjoint always exists or if it requires a Conduche condition.)
This could also be called dependent sum, though I think that's confusing because to me a dependent sum is the special case where F is a projection.
There was a problem hiding this comment.
Yes, having a right adjoint is exactly being Conduché.
| g ⋆⟨ C ⟩ h , | ||
| F-seq g h ◁ (λ i → p i ⋆⟨ D ⟩ q i) , | ||
| (Cᴰ._⋆ᴰ_ gᴰ hᴰ) | ||
| ⋆IdLᴰ ∃F {d}{d'}{g}{c , pc , xc}{c' , pc' , xc'} (f , p , x) = |
There was a problem hiding this comment.
These proofs can probably be simplified using https://github.com/agda/cubical/blob/master/Cubical/Categories/Displayed/Reasoning.agda
| @@ -0,0 +1,65 @@ | |||
| -- | Full subcategories (not necessarily prop) viewed as displayed categories. | |||
| {-# OPTIONS --safe #-} | |||
| module Cubical.Categories.Displayed.Constructions.FullSubcategory where | |||
There was a problem hiding this comment.
If we don't like "Full subcategory" we could call this FullyFaithful because every displayed cat where Fst is fully faithful is equivalent to one of this form. We should also consider removing Cubical.Categories.Constructions.FullSubcategory and replacing it by this. But there is some univalent stuff in there now that would have to be ported
| λ f g → cong {x = f ⋆⟨ ∫C Cᴰ ⟩ g} fst refl | ||
|
|
||
| -- Functor into the total category | ||
| module TotalCategory {D : Category ℓD ℓD'} |
There was a problem hiding this comment.
Should this be a named module? The analogs of this, e.g., Data.Sum.elim are not in named modules, you just tend to have to import the module as Sum to use them without name clashes.
| @@ -157,3 +172,56 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} | |||
| ∫F .F-hom (_ , fᴰ) = _ , Fᴰ.F-homᴰ fᴰ | |||
| ∫F .F-id = ΣPathP (_ , Fᴰ.F-idᴰ) | |||
| ∫F .F-seq _ _ = ΣPathP (_ , (Fᴰ.F-seqᴰ _ _)) | |||
|
|
|||
| -- Projections out of the total category | |||
There was a problem hiding this comment.
This should be in a different file. I think we should move ∫C to Displayed.TotalCategory or Displayed.TotalCategory.Base and this can be in that or Displayed.TotalCategory.Properties
| intro .F-seq f g = ΣPathP (F .F-seq f g , Fᴰ .F-seqᴰ _ _) | ||
|
|
||
| -- Projection out of the displayed total category | ||
| module _ {C : Category ℓC ℓC'} |
There was a problem hiding this comment.
Same comment here as above, should be in a different file.
|
|
||
| open Functor | ||
|
|
||
| Preorderᴰ→FstFaithful : isFaithful (Fst {Cᴰ = Preorderᴰ→Catᴰ}) |
Cubical/Categories/Displayed/TotalCategory/DisplayedTotalCategory.agda
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
LGTM. @jpoiret @felixwellen and/or @ecavallo this is ready for review
|
Whitespace is fixed, and the left adjoint has been moved. Should be ready for review |
|
@felixwellen anything we can do to move this along? |
Meant to be the first thrust of #1106 code as we separate that large hunk of code into modular and manageable PRs
Here we add the following things to reason about displayed categories