Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Rework displayed category reasoning. #1153

Merged
merged 2 commits into from
Sep 11, 2024
Merged

Rework displayed category reasoning. #1153

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2e6ba2b
Rework displayed category reasoning.
jpoiret Sep 6, 2024
a845cdb
Adapt proofs to new displayed category reasoning.
jpoiret Sep 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions Cubical/Categories/Category/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,10 @@ record Category ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
_∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ]
g ∘ f = f ⋆ g

⟨_⟩⋆⟨_⟩ : {x y z : ob} {f f' : Hom[ x , y ]} {g g' : Hom[ y , z ]}
→ f ≡ f' → g ≡ g' → f ⋆ g ≡ f' ⋆ g'
⟨ ≡f ⟩⋆⟨ ≡g ⟩ = cong₂ _⋆_ ≡f ≡g

infixr 9 _⋆_
infixr 9 _∘_

Expand Down
4 changes: 2 additions & 2 deletions Cubical/Categories/Constructions/TotalCategory/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ module _ {C : Category ℓC ℓC'} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} where
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-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ᴰ))
R.rectify (Fᴰ .F-seqᴰ (f , fᴰ) (g , gᴰ))

121 changes: 45 additions & 76 deletions Cubical/Categories/Displayed/Cartesian.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,73 +149,54 @@ module Covariant
module _ (fᴰ-isIsoᴰ : isIsoᴰ Cᴰ f-isIso fᴰ) where
open isIsoᴰ fᴰ-isIsoᴰ

private basepath : {c : B.ob} (g : B [ b , c ]) → inv B.⋆ f B.⋆ g ≡ g
basepath g =
sym (B.⋆Assoc _ _ _)
∙ cong (B._⋆ g) sec
∙ B.⋆IdL _
{-# INLINE basepath #-}

isIsoᴰ→isOpcartesian : isOpcartesian fᴰ
isIsoᴰ→isOpcartesian g .equiv-proof fgᴰ .fst .fst =
R.reind
(basepath g)
( sym (B.⋆Assoc _ _ _)
∙ B.⟨ sec ⟩⋆⟨ refl ⟩
∙ B.⋆IdL _)
(invᴰ ⋆ᴰ fgᴰ)
isIsoᴰ→isOpcartesian g .equiv-proof fgᴰ .fst .snd =
R.≡[]-rectify $
(refl R.[ refl ]⋆[ sym (basepath g) ] symP (R.reind-filler (basepath g) _))
R.[ _ ]∙[ _ ]
symP (Cᴰ.⋆Assocᴰ fᴰ invᴰ fgᴰ)
R.[ sym $ B.⋆Assoc f inv (f B.⋆ g) ]∙[ _ ]
(retᴰ R.[ ret ]⋆[ refl ] refl)
R.[ _ ]∙[ _ ]
Cᴰ.⋆IdLᴰ fgᴰ
R.rectify $ R.≡out $
R.⟨ refl ⟩⋆⟨ sym $ R.reind-filler _ _ ⟩
∙ sym (R.⋆Assoc _ _ _)
∙ R.⟨ R.≡in retᴰ ⟩⋆⟨ refl ⟩
∙ R.⋆IdL _
isIsoᴰ→isOpcartesian g .equiv-proof fgᴰ .snd (gᴰ , gᴰ-infib) =
Σ≡Prop (λ _ → isOfHLevelPathP' 1 Cᴰ.isSetHomᴰ _ _) $
R.≡[]-rectify $
symP (R.reind-filler (basepath g) _)
R.[ sym (basepath g) ]∙[ _ ]
(refl R.[ refl ]⋆[ refl ] symP gᴰ-infib)
R.[ _ ]∙[ _ ]
symP (Cᴰ.⋆Assocᴰ invᴰ fᴰ gᴰ)
R.[ sym (B.⋆Assoc inv f g) ]∙[ _ ]
(secᴰ R.[ sec ]⋆[ refl ] refl)
R.[ _ ]∙[ _ ]
Cᴰ.⋆IdLᴰ gᴰ
R.rectify $ R.≡out $
sym (R.reind-filler _ _)
∙ R.⟨ refl ⟩⋆⟨ sym $ R.≡in gᴰ-infib ⟩
∙ sym (R.⋆Assoc _ _ _)
∙ R.⟨ R.≡in secᴰ ⟩⋆⟨ refl ⟩
∙ R.⋆IdL _

module _ (opcart : isOpcartesian fᴰ) where
open isIsoᴰ

isOpcartesian→isIsoᴰ : isIsoᴰ Cᴰ f-isIso fᴰ
isOpcartesian→isIsoᴰ .invᴰ =
opcart inv .equiv-proof (R.reind (sym ret) idᴰ) .fst .fst
isOpcartesian→isIsoᴰ .retᴰ = R.≡[]-rectify $
opcart inv .equiv-proof (R.reind (sym ret) idᴰ) .fst .snd
R.[ _ ]∙[ ret ]
R.reind-filler-sym ret idᴰ
isOpcartesian→isIsoᴰ .retᴰ = R.rectify $ R.≡out $
R.≡in (opcart inv .equiv-proof (R.reind (sym ret) idᴰ) .fst .snd)
∙ sym (R.reind-filler _ _)
isOpcartesian→isIsoᴰ .secᴰ =
let
≡-any-two-in-fib = isContr→isProp $
opcart (inv B.⋆ f) .equiv-proof
(fᴰ ⋆ᴰ (isOpcartesian→isIsoᴰ .invᴰ) ⋆ᴰ fᴰ)
-- Reindexed idᴰ is a valid lift for the composition.
idᴰ-in-fib = R.≡[]-rectify $
(refl {x = fᴰ} R.[ refl ]⋆[ _ ] R.reind-filler-sym sec idᴰ)
R.[ _ ]∙[ _ ]
⋆IdRᴰ fᴰ
R.[ B.⋆IdR f ]∙[ _ ]
symP (⋆IdLᴰ fᴰ)
R.[ sym (B.⋆IdL f) ]∙[ _ ]
(symP (isOpcartesian→isIsoᴰ .retᴰ) R.[ sym ret ]⋆[ refl ] refl {x = fᴰ})
R.[ _ ]∙[ _ ]
⋆Assocᴰ fᴰ (isOpcartesian→isIsoᴰ .invᴰ) fᴰ
in R.≡[]-rectify $
(cong fst $ ≡-any-two-in-fib
((isOpcartesian→isIsoᴰ .invᴰ) ⋆ᴰ fᴰ , refl)
(R.reind (sym sec) idᴰ , idᴰ-in-fib))

R.[ _ ]∙[ _ ]
R.reind-filler-sym sec idᴰ
idᴰ-in-fib = R.rectify $ R.≡out $
R.⟨ refl ⟩⋆⟨ sym $ R.reind-filler _ _ ⟩
∙ R.⋆IdR _
∙ sym (R.⋆IdL _)
∙ R.⟨ sym $ R.≡in $ isOpcartesian→isIsoᴰ .retᴰ ⟩⋆⟨ refl ⟩
∙ R.⋆Assoc _ _ _
in R.rectify $ R.≡out $
R.≡in (cong fst $ ≡-any-two-in-fib
((isOpcartesian→isIsoᴰ .invᴰ) ⋆ᴰ fᴰ , refl)
(R.reind (sym sec) idᴰ , idᴰ-in-fib))
∙ sym (R.reind-filler _ _)

-- Construction of the substitution functor for a general opfibration.
module _
Expand All @@ -236,17 +217,16 @@ module Covariant
f ⋆ᴰ cleavage σ y .snd .fst)
substituteArrow f =
map-snd
(λ p → R.≡[]-rectify $
p
R.[ _ ]∙[ sym (B.⋆IdL _ ∙ sym (B.⋆IdR _)) ]
symP (R.reind-filler _ _))
(λ p → R.rectify $ R.≡out $
R.≡in p
∙ sym (R.reind-filler _ _))
(cart .fst)
, λ g' →
Σ≡Prop
(λ _ → isOfHLevelPathP' 1 isSetHomᴰ _ _)
(cong fst $ cart .snd $
map-snd
(λ p → R.≡[]-rectify $ p R.[ _ ]∙[ _ ] R.reind-filler _ _)
(λ p → R.rectify $ R.≡out $ R.≡in p ∙ R.reind-filler _ _)
g')
where
cart : isContr (Σ _ _)
Expand All @@ -260,33 +240,22 @@ module Covariant
substitutionFunctor .F-id {x} = cong fst $
substituteArrow (VerticalCategory Cᴰ a .Category.id) .snd $
VerticalCategory Cᴰ b .Category.id
, R.≡[]-rectify
((refl R.[ refl ]⋆[ refl ] symP (R.reind-filler refl idᴰ))
R.[ cong₂ B._⋆_ refl refl ]∙[ _ ]
⋆IdRᴰ (cleavage σ x .snd .fst)
R.[ B.⋆IdR σ ]∙[ _ ]
symP (⋆IdLᴰ (cleavage σ x .snd .fst))
R.[ sym (B.⋆IdL σ) ]∙[ _ ]
(R.reind-filler refl idᴰ R.[ refl ]⋆[ refl ] refl))
, (R.rectify $ R.≡out $
R.⟨ refl ⟩⋆⟨ sym $ R.reind-filler _ _ ⟩
∙ R.⋆IdR _
∙ sym (R.⋆IdL _)
∙ R.⟨ R.reind-filler _ _ ⟩⋆⟨ refl ⟩)
substitutionFunctor .F-seq {x} {y} {z} f g = cong fst $
substituteArrow (VerticalCategory Cᴰ a .Category._⋆_ f g) .snd $
VerticalCategory Cᴰ b .Category._⋆_ (stepf .fst) (stepg .fst)
, R.≡[]-rectify
((refl
R.[ refl ]⋆[ sym (B.⋆IdL B.id) ]
R.reind-filler-sym (sym $ B.⋆IdL B.id) (stepf .fst ⋆ᴰ stepg .fst))
R.[ cong₂ B._⋆_ refl (sym $ B.⋆IdL B.id) ]∙[ _ ]
symP (⋆Assocᴰ (cleavage σ x .snd .fst) (stepf .fst) (stepg .fst))
R.[ sym (B.⋆Assoc σ B.id B.id) ]∙[ _ ]
(stepf .snd R.[ (B.⋆IdR σ ∙ sym (B.⋆IdL σ)) ]⋆[ refl ] refl)
R.[ cong₂ B._⋆_ (B.⋆IdR σ ∙ sym (B.⋆IdL σ)) refl ]∙[ _ ]
⋆Assocᴰ f (cleavage σ y .snd .fst) (stepg .fst)
R.[ B.⋆Assoc B.id σ B.id ]∙[ _ ]
(refl R.[ refl ]⋆[ (B.⋆IdR σ ∙ sym (B.⋆IdL σ)) ] stepg .snd)
R.[ cong₂ B._⋆_ refl (B.⋆IdR σ ∙ sym (B.⋆IdL σ)) ]∙[ _ ]
symP (⋆Assocᴰ f g (cleavage σ z .snd .fst))
R.[ sym (B.⋆Assoc B.id B.id σ) ]∙[ cong₂ B._⋆_ (B.⋆IdL B.id) refl ]
(R.reind-filler (B.⋆IdL B.id) (f ⋆ᴰ g) R.[ B.⋆IdL B.id ]⋆[ refl ] refl))
, (R.rectify $ R.≡out $
R.⟨ refl ⟩⋆⟨ sym $ R.reind-filler _ _ ⟩
∙ sym (R.⋆Assoc _ _ _)
∙ R.⟨ R.≡in $ stepf .snd ⟩⋆⟨ refl ⟩
∙ R.⋆Assoc _ _ _
∙ R.⟨ refl ⟩⋆⟨ R.≡in $ stepg .snd ⟩
∙ sym (R.⋆Assoc _ _ _)
∙ R.⟨ R.reind-filler _ _ ⟩⋆⟨ refl ⟩)
where
stepf = substituteArrow f .fst
stepg = substituteArrow g .fst
44 changes: 18 additions & 26 deletions Cubical/Categories/Displayed/Constructions/Reindex/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,35 +93,27 @@ module _
reindex .Categoryᴰ.Hom[_][_,_] f aᴰ bᴰ = Hom[ F-hom f ][ aᴰ , bᴰ ]
reindex .Categoryᴰ.idᴰ = R.reind (sym F-id) idᴰ
reindex .Categoryᴰ._⋆ᴰ_ fᴰ gᴰ = R.reind (sym $ F-seq _ _) (fᴰ ⋆ᴰ gᴰ)
reindex .Categoryᴰ.⋆IdLᴰ fᴰ = R.≡[]-rectify $
R.reind-filler-sym (F-seq _ _) _
R.[ _ ]∙[ _ ]
(R.reind-filler-sym F-id idᴰ R.[ _ ]⋆[ refl ] refl)
R.[ _ ]∙[ _ ]
⋆IdLᴰ fᴰ
reindex .Categoryᴰ.⋆IdRᴰ fᴰ = R.≡[]-rectify $
R.reind-filler-sym (F-seq _ _) _
R.[ _ ]∙[ _ ]
(refl R.[ refl ]⋆[ _ ] R.reind-filler-sym F-id idᴰ)
R.[ _ ]∙[ _ ]
⋆IdRᴰ fᴰ
reindex .Categoryᴰ.⋆Assocᴰ fᴰ gᴰ hᴰ = R.≡[]-rectify $
R.reind-filler-sym (F-seq _ _) _
R.[ _ ]∙[ _ ]
(R.reind-filler-sym (F-seq _ _) _ R.[ _ ]⋆[ refl ] refl)
R.[ _ ]∙[ _ ]
⋆Assocᴰ fᴰ gᴰ hᴰ
R.[ _ ]∙[ _ ]
(refl R.[ refl ]⋆[ _ ] R.reind-filler (sym $ F-seq _ _) _)
R.[ _ ]∙[ _ ]
R.reind-filler (sym $ F-seq _ _) _
reindex .Categoryᴰ.⋆IdLᴰ fᴰ = R.rectify $ R.≡out $
sym (R.reind-filler _ _)
∙ R.⟨ sym $ R.reind-filler _ idᴰ ⟩⋆⟨ refl ⟩
∙ R.⋆IdL _
reindex .Categoryᴰ.⋆IdRᴰ fᴰ = R.rectify $ R.≡out $
sym (R.reind-filler _ _)
∙ R.⟨ refl ⟩⋆⟨ sym $ R.reind-filler _ idᴰ ⟩
∙ R.⋆IdR _
reindex .Categoryᴰ.⋆Assocᴰ fᴰ gᴰ hᴰ = R.rectify $ R.≡out $
sym (R.reind-filler _ _)
∙ R.⟨ sym $ R.reind-filler _ _ ⟩⋆⟨ refl ⟩
∙ R.⋆Assoc _ _ _
∙ R.⟨ refl ⟩⋆⟨ R.reind-filler _ _ ⟩
∙ R.reind-filler _ _
reindex .Categoryᴰ.isSetHomᴰ = isSetHomᴰ

π : Functorᴰ F reindex Dᴰ
π .F-obᴰ = λ z → z
π .F-homᴰ = λ z → z
π .F-idᴰ = symP (transport-filler _ _)
π .F-seqᴰ fᴰ gᴰ = symP (transport-filler _ _)
π .F-idᴰ = R.≡out $ sym (R.reind-filler _ _)
π .F-seqᴰ fᴰ gᴰ = R.≡out $ sym (R.reind-filler _ _)

GlobalSectionReindex→Section : GlobalSection reindex → Section F Dᴰ
GlobalSectionReindex→Section Fᴰ = compFunctorᴰGlobalSection π Fᴰ
Expand All @@ -142,9 +134,9 @@ module _
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-idᴰ = R.rectify $ R.≡out $ R.≡in (FGᴰ .F-idᴰ) ∙ (R.reind-filler _ _)
introS .F-seqᴰ fᴰ gᴰ =
R.≡[]-rectify (R.≡[]∙ _ _ (FGᴰ .F-seqᴰ fᴰ gᴰ) (R.reind-filler _ _))
R.rectify $ R.≡out $ R.≡in (FGᴰ .F-seqᴰ fᴰ gᴰ) ∙ (R.reind-filler _ _)

module _
{C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
Expand Down
Loading
Loading