Skip to content

Commit

Permalink
Rework displayed category reasoning. (#1153)
Browse files Browse the repository at this point in the history 
This new technique is both more performant, more readable and reduces
boilerplate.
  • Loading branch information
@jpoiret
jpoiret authored Sep 11, 2024
1 parent f3d8889 commit 581748b
Show file tree
Hide file tree
Showing 6 changed files with 134 additions and 194 deletions.
4 changes: 4 additions & 0 deletions Cubical/Categories/Category/Base.agda
View file
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
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
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
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

0 comments on commit 581748b

Please sign in to comment.