Skip to content

Commit ac8faa2

Browse files
phijorphijor
committed
Turn summation of set-bundles into a strict 2-functor
1 parent c243c35 commit ac8faa2

File tree

8 files changed

+190
-157
lines changed

8 files changed

+190
-157
lines changed

‎GpdCont/ActionContainer/AsFamily.agda‎

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -10,17 +10,16 @@ open import GpdCont.Group.MapConjugator using (Conjugator)
1010
open import GpdCont.GroupAction.Base using (Action ; _⁺_)
1111
open import GpdCont.GroupAction.Equivariant using (isEquivariantMap[_][_,_])
1212
open import GpdCont.GroupAction.TwoCategory using (GroupAction ; isLocallyStrictGroupAction)
13-
open import GpdCont.GroupAction.Delooping as ActionDelooping renaming (Delooping to ActionDelooping)
13+
open import GpdCont.GroupAction.Delooping as ActionDelooping renaming (Deloopingˢ to ActionDelooping)
1414
open import GpdCont.SetBundle.Base ℓ using (SetBundle)
15-
open import GpdCont.SetBundle.Summation ℓ using (SetBundleΣ)
1615

1716
open import GpdCont.TwoCategory.Base using (TwoCategory)
18-
open import GpdCont.TwoCategory.LaxFunctor using (LaxFunctor)
19-
open import GpdCont.TwoCategory.LocalFunctor as LocalFunctor using (LocalFunctor)
17+
open import GpdCont.TwoCategory.StrictFunctor using (StrictFunctor)
18+
open import GpdCont.TwoCategory.StrictFunctor.LocalFunctor as LocalFunctor using (LocalFunctor)
2019
open import GpdCont.TwoCategory.Displayed.Base using (TwoCategoryᴰ)
2120
open import GpdCont.TwoCategory.Family.Base using (Fam ; Famᴰ)
22-
open import GpdCont.TwoCategory.Family.Functor renaming (LiftFunctor to FamFunctor)
23-
open import GpdCont.TwoCategory.HomotopySet using (SetEq ; isTwoCategorySetStr)
21+
open import GpdCont.TwoCategory.Family.Functor using (FamFunctor)
22+
open import GpdCont.TwoCategory.HomotopySet using (SetEq)
2423

2524
open import Cubical.Foundations.Equiv
2625
open import Cubical.Foundations.HLevels
@@ -136,14 +135,14 @@ module _
136135

137136
private
138137
𝔹ᴬ = ActionDelooping ℓ
139-
module 𝔹ᴬ = LaxFunctor 𝔹ᴬ
138+
module 𝔹ᴬ = StrictFunctor 𝔹ᴬ
140139

141-
Fam𝔹 : LaxFunctor FamAction FamSetBundle
140+
Fam𝔹 : StrictFunctor FamAction FamSetBundle
142141
Fam𝔹 = FamFunctor (ActionDelooping ℓ) ℓ
143142

144143
private
145144
module Fam𝔹 where
146-
open LaxFunctor Fam𝔹 public
145+
open StrictFunctor Fam𝔹 public
147146
open import GpdCont.TwoCategory.Family.Properties (ActionDelooping ℓ) ℓ public
148147

149148
module _ where

‎GpdCont/ActionContainer/AsSymmetricContainer.agda‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ open import GpdCont.Prelude
22

33
module GpdCont.ActionContainer.AsSymmetricContainer (ℓ : Level) where
44

5-
open import GpdCont.TwoCategory.LaxFunctor using (LaxFunctor ; compLaxFunctor)
6-
open import GpdCont.TwoCategory.LocalFunctor using (LocalFunctor ; isLocallyFullyFaithful)
5+
open import GpdCont.TwoCategory.StrictFunctor using (StrictFunctor ; compStrictFunctor)
6+
open import GpdCont.TwoCategory.StrictFunctor.LocalFunctor using (LocalFunctor ; isLocallyFullyFaithful)
77
open import GpdCont.TwoCategory.CompositeFunctor using (isLocallyFullyFaithfulCompositeRestrict)
88
open import GpdCont.GroupAction.Delooping using (isConnectedDeloopingBase)
99
open import GpdCont.ActionContainer.AsFamily ℓ
@@ -13,15 +13,15 @@ open import GpdCont.ActionContainer.AsFamily ℓ
1313
open import GpdCont.SetBundle.Base ℓ using () renaming (SetBundle to SymmCont)
1414
open import GpdCont.SetBundle.Summation ℓ using (SetBundleΣ ; isLocallyFullyFaithfulΣ-at-connBase)
1515

16-
ActToSymmCont : LaxFunctor ActCont SymmCont
17-
ActToSymmCont = compLaxFunctor Fam𝔹 SetBundleΣ
16+
ActToSymmCont : StrictFunctor ActCont SymmCont
17+
ActToSymmCont = compStrictFunctor Fam𝔹 SetBundleΣ
1818

1919
isLocallyFullyFaithfulActToSymmCont : isLocallyFullyFaithful ActToSymmCont
2020
isLocallyFullyFaithfulActToSymmCont =
2121
isLocallyFullyFaithfulCompositeRestrict Fam𝔹 SetBundleΣ isLocallyFullyFaithfulFam𝔹 Σ-ff-restrict
2222
where
2323
open import Cubical.Categories.Functor using (Functor)
24-
module Fam𝔹 = LaxFunctor Fam𝔹
24+
module Fam𝔹 = StrictFunctor Fam𝔹
2525

2626
Σ-ff-restrict : ∀ F G → Functor.isFullyFaithful (LocalFunctor SetBundleΣ (Fam𝔹.₀ F) (Fam𝔹.₀ G))
2727
Σ-ff-restrict F G = isLocallyFullyFaithfulΣ-at-connBase (Fam𝔹.₀ F) (Fam𝔹.₀ G) λ j → isConnectedDeloopingBase ℓ (F .snd j)

‎GpdCont/SetBundle/Summation.agda‎

Lines changed: 49 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,11 @@ open import GpdCont.Connectivity as Connectivity using (isPathConnected)
1313
open import GpdCont.TwoCategory.Base using (TwoCategory)
1414
open import GpdCont.TwoCategory.LaxFunctor using (LaxFunctor ; compLaxFunctor)
1515
open import GpdCont.TwoCategory.StrictFunctor using (StrictFunctor)
16-
open import GpdCont.TwoCategory.LocalFunctor using (LocalFunctor)
16+
open import GpdCont.TwoCategory.StrictFunctor.LocalFunctor using (LocalFunctor)
1717
open import GpdCont.TwoCategory.Displayed.Base using (TwoCategoryᴰ)
1818
open import GpdCont.TwoCategory.Displayed.LocallyThin using (LocallyThinOver ; IntoLocallyThin)
1919
open import GpdCont.TwoCategory.Displayed.LaxFunctor using (LaxFunctorᴰ)
20+
open import GpdCont.TwoCategory.Displayed.StrictFunctor using (StrictFunctorᴰ)
2021
open import GpdCont.TwoCategory.Displayed.Unit using (Unitᴰ ; UnitOver ; AddUnit ; ReindexUnit)
2122
open import GpdCont.TwoCategory.Family.Base using (Fam ; Famᴰ ; Fam₂J[_] ; Famᴰ₂ ; Fam₂PathP)
2223
open import GpdCont.TwoCategory.HomotopySet using (SetEq ; isTwoCategorySetStr)
@@ -108,41 +109,28 @@ private
108109
(congS (λ - → φ j , - b) (rᴰ j .fst)) ∙ (congS (λ - → φ j , - b) (sᴰ j .fst))
109110
goal = GL.cong-∙ (λ - → φ j , - b) (rᴰ j .fst) (sᴰ j .fst)
110111

111-
SetBundleΣFst : LaxFunctor FamSetBundle (hGpdCat ℓ)
112-
SetBundleΣFst .LaxFunctor.F-ob = ΣFst₀
113-
SetBundleΣFst .LaxFunctor.F-hom = ΣFst₁
114-
SetBundleΣFst .LaxFunctor.F-rel = ΣFst₂
115-
SetBundleΣFst .LaxFunctor.F-rel-id = refl
116-
SetBundleΣFst .LaxFunctor.F-rel-trans = ΣFst₂-rel-trans
117-
SetBundleΣFst .LaxFunctor.F-trans-lax (φ , f) (ψ , g) = refl
118-
SetBundleΣFst .LaxFunctor.F-trans-lax-natural {x = J , X} {y = K , Y} {f₁ = φ , f₁} {f₂ = .φ , f₂} {g₁ = ψ , g₁} {g₂ = .ψ , g₂} (Eq.refl , rᴰ) (Eq.refl , sᴰ) = Path.Square→compPath
119-
λ where
120-
i j (idx , b) .fst → ψ (φ idx)
121-
i j (idx , b) .snd → sᴰ (φ idx) .fst i (rᴰ idx .fst i b)
122-
SetBundleΣFst .LaxFunctor.F-id-lax (J , x) = refl
123-
SetBundleΣFst .LaxFunctor.F-assoc (φ , f) (ψ , g) (ρ , h) = refl′ (refl ∙ refl)
124-
SetBundleΣFst .LaxFunctor.F-unit-left (J , x) = sym GL.compPathRefl
125-
SetBundleΣFst .LaxFunctor.F-unit-right (J , x) = sym GL.compPathRefl
126-
127-
SetBundleΣFstˢ : StrictFunctor FamSetBundle (hGpdCat ℓ)
128-
SetBundleΣFstˢ .StrictFunctor.F-ob = ΣFst₀
129-
SetBundleΣFstˢ .StrictFunctor.F-hom = ΣFst₁
130-
SetBundleΣFstˢ .StrictFunctor.F-rel = ΣFst₂
131-
SetBundleΣFstˢ .StrictFunctor.F-rel-id = refl
132-
SetBundleΣFstˢ .StrictFunctor.F-rel-trans = ΣFst₂-rel-trans
133-
SetBundleΣFstˢ .StrictFunctor.F-hom-comp _ _ = refl
134-
SetBundleΣFstˢ .StrictFunctor.F-hom-id _ = refl
135-
SetBundleΣFstˢ .StrictFunctor.F-assoc-filler-left _ _ _ .fst = refl
136-
SetBundleΣFstˢ .StrictFunctor.F-assoc-filler-left _ _ _ .snd = refl
137-
SetBundleΣFstˢ .StrictFunctor.F-assoc-filler-right _ _ _ .fst = refl
138-
SetBundleΣFstˢ .StrictFunctor.F-assoc-filler-right _ _ _ .snd = refl
139-
SetBundleΣFstˢ .StrictFunctor.F-assoc _ _ _ = reflSquare _
140-
SetBundleΣFstˢ .StrictFunctor.F-unit-left-filler _ .fst = refl
141-
SetBundleΣFstˢ .StrictFunctor.F-unit-left-filler _ .snd = refl
142-
SetBundleΣFstˢ .StrictFunctor.F-unit-left f = reflSquare (ΣFst₁ f)
143-
SetBundleΣFstˢ .StrictFunctor.F-unit-right-filler _ .fst = refl
144-
SetBundleΣFstˢ .StrictFunctor.F-unit-right-filler _ .snd = refl
145-
SetBundleΣFstˢ .StrictFunctor.F-unit-right f = reflSquare (ΣFst₁ f)
112+
SetBundleΣFst : StrictFunctor FamSetBundle (hGpdCat ℓ)
113+
SetBundleΣFst .StrictFunctor.F-ob = ΣFst₀
114+
SetBundleΣFst .StrictFunctor.F-hom = ΣFst₁
115+
SetBundleΣFst .StrictFunctor.F-rel = ΣFst₂
116+
SetBundleΣFst .StrictFunctor.F-rel-id = refl
117+
SetBundleΣFst .StrictFunctor.F-rel-trans = ΣFst₂-rel-trans
118+
SetBundleΣFst .StrictFunctor.F-hom-comp _ _ = refl
119+
SetBundleΣFst .StrictFunctor.F-hom-id _ = refl
120+
SetBundleΣFst .StrictFunctor.F-assoc-filler-left _ _ _ .fst = refl
121+
SetBundleΣFst .StrictFunctor.F-assoc-filler-left _ _ _ .snd = refl
122+
SetBundleΣFst .StrictFunctor.F-assoc-filler-right _ _ _ .fst = refl
123+
SetBundleΣFst .StrictFunctor.F-assoc-filler-right _ _ _ .snd = refl
124+
SetBundleΣFst .StrictFunctor.F-assoc _ _ _ = reflSquare _
125+
SetBundleΣFst .StrictFunctor.F-unit-left-filler _ .fst = refl
126+
SetBundleΣFst .StrictFunctor.F-unit-left-filler _ .snd = refl
127+
SetBundleΣFst .StrictFunctor.F-unit-left f = reflSquare (ΣFst₁ f)
128+
SetBundleΣFst .StrictFunctor.F-unit-right-filler _ .fst = refl
129+
SetBundleΣFst .StrictFunctor.F-unit-right-filler _ .snd = refl
130+
SetBundleΣFst .StrictFunctor.F-unit-right f = reflSquare (ΣFst₁ f)
131+
132+
private
133+
module SetBundleΣFst = StrictFunctor SetBundleΣFst
146134

147135
private
148136
ΣSnd₀ : (x : FamSetBundle.ob) → SetBundle.ob[ ΣFst₀ x ]
@@ -158,28 +146,34 @@ private
158146
→ SetBundle.rel[_] {yᴰ = ΣSnd₀ y} (ΣFst₂ r) (ΣSnd₁ f) (ΣSnd₁ g)
159147
ΣSnd₂ (Eq.refl , rᴰ) = funExt λ (j , b) → rᴰ j .snd ≡$ b
160148

161-
SetBundleΣᵀ : IntoLocallyThin SetBundleΣFst (Unitᴰ FamSetBundle) SetBundleᵀ
162-
SetBundleΣᵀ .IntoLocallyThin.F-obᴰ {x} _ = ΣSnd₀ x
163-
SetBundleΣᵀ .IntoLocallyThin.F-homᴰ {x} {y} {f} _ = ΣSnd₁ {x} {y} f
164-
SetBundleΣᵀ .IntoLocallyThin.F-relᴰ {r} _ = ΣSnd₂ r
165-
SetBundleΣᵀ .IntoLocallyThin.F-trans-laxᴰ fᴰ gᴰ = refl
166-
SetBundleΣᵀ .IntoLocallyThin.F-id-laxᴰ xᴰ = refl
167-
168-
SetBundleΣᴰ : LaxFunctorᴰ SetBundleΣFst (Unitᴰ FamSetBundle) SetBundleᴰ
169-
SetBundleΣᴰ = IntoLocallyThin.toLaxFunctorᴰ SetBundleΣᵀ
170-
171-
SetBundleΣUnit : LaxFunctor (UnitOver FamSetBundle) SetBundle
172-
SetBundleΣUnit = LaxFunctorᴰ.toTotalFunctor SetBundleΣᴰ
173-
174-
SetBundleΣ : LaxFunctor FamSetBundle SetBundle
175-
SetBundleΣ = compLaxFunctor (AddUnit _) SetBundleΣUnit
149+
SetBundleΣᴰ : StrictFunctorᴰ SetBundleΣFst (Unitᴰ FamSetBundle) SetBundleᴰ
150+
SetBundleΣᴰ .StrictFunctorᴰ.F-obᴰ {x} _ = ΣSnd₀ x
151+
SetBundleΣᴰ .StrictFunctorᴰ.F-homᴰ {x} {y} {f} _ = ΣSnd₁ {x} {y} f
152+
SetBundleΣᴰ .StrictFunctorᴰ.F-relᴰ {r} _ = ΣSnd₂ r
153+
SetBundleΣᴰ .StrictFunctorᴰ.F-rel-idᴰ fᴰ = reflSquare _
154+
SetBundleΣᴰ .StrictFunctorᴰ.F-rel-transᴰ {y} {r} {s} tt tt = SetBundle.relᴰ≡ {yᴰ = ΣSnd₀ y} (SetBundleΣFst.F-rel-trans r s)
155+
SetBundleΣᴰ .StrictFunctorᴰ.F-hom-compᴰ {f} {g} _ _ = goal where
156+
goal : SetBundle.comp-homᴰ {zᴰ = ΣSnd₀ _} (ΣSnd₁ f) (ΣSnd₁ g) ≡ ΣSnd₁ (f FamSetBundle.∙₁ g)
157+
goal = refl
158+
SetBundleΣᴰ .StrictFunctorᴰ.F-hom-idᴰ _ = refl
159+
SetBundleΣᴰ .StrictFunctorᴰ.F-assoc-filler-leftᴰ {f} {g} {h} _ _ _ .fst = refl
160+
SetBundleΣᴰ .StrictFunctorᴰ.F-assoc-filler-leftᴰ {f} {g} {h} _ _ _ .snd = reflSquare _
161+
SetBundleΣᴰ .StrictFunctorᴰ.F-assoc-filler-rightᴰ {f} {g} {h} _ _ _ .fst = refl
162+
SetBundleΣᴰ .StrictFunctorᴰ.F-assoc-filler-rightᴰ {f} {g} {h} _ _ _ .snd = reflSquare _
163+
SetBundleΣᴰ .StrictFunctorᴰ.F-assocᴰ {f} {g} {h} _ _ _ = reflSquare _
164+
SetBundleΣᴰ .StrictFunctorᴰ.F-unit-left-fillerᴰ {f} _ .fst = refl
165+
SetBundleΣᴰ .StrictFunctorᴰ.F-unit-left-fillerᴰ {f} _ .snd = reflSquare _
166+
SetBundleΣᴰ .StrictFunctorᴰ.F-unit-leftᴰ {f} _ = reflSquare _
167+
SetBundleΣᴰ .StrictFunctorᴰ.F-unit-right-fillerᴰ {f} _ .fst = refl
168+
SetBundleΣᴰ .StrictFunctorᴰ.F-unit-right-fillerᴰ {f} _ .snd = reflSquare _
169+
SetBundleΣᴰ .StrictFunctorᴰ.F-unit-rightᴰ {f} _ = reflSquare _
170+
171+
SetBundleΣ : StrictFunctor FamSetBundle SetBundle
172+
SetBundleΣ = ReindexUnit FamSetBundle SetBundleΣFst SetBundleΣᴰ
176173

177174
private
178175
module SetBundleΣ where
179-
open LaxFunctor SetBundleΣ public
180-
181-
SetBundleΣ' : LaxFunctor FamSetBundle SetBundle
182-
SetBundleΣ' = ReindexUnit FamSetBundle (hGpdCat ℓ) SetBundleΣFst SetBundleᴰ SetBundleΣᴰ
176+
open StrictFunctor SetBundleΣ public
183177

184178
-- Local functors of Σ : Fam(SetBundle) → SetBundle are fully faithful whenever
185179
-- the familiy x in Σ(x, y) : Fam(SetBundle)(x, y) → SetBundle(Σx, Σy) has a connected bases.

‎GpdCont/TwoCategory/CompositeFunctor.agda‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
open import GpdCont.Prelude
22

33
open import GpdCont.TwoCategory.Base
4-
open import GpdCont.TwoCategory.LaxFunctor
4+
open import GpdCont.TwoCategory.StrictFunctor
55

66
module GpdCont.TwoCategory.CompositeFunctor
77
{ℓo₁ ℓh₁ ℓr₁}
@@ -10,21 +10,21 @@ module GpdCont.TwoCategory.CompositeFunctor
1010
{C : TwoCategory ℓo₁ ℓh₁ ℓr₁}
1111
{D : TwoCategory ℓo₂ ℓh₂ ℓr₂}
1212
{E : TwoCategory ℓo₃ ℓh₃ ℓr₃}
13-
(F : LaxFunctor C D)
14-
(G : LaxFunctor D E)
13+
(F : StrictFunctor C D)
14+
(G : StrictFunctor D E)
1515
where
1616
private
1717
module C = TwoCategory C
18-
module F = LaxFunctor F
18+
module F = StrictFunctor F
1919

20-
open import GpdCont.TwoCategory.LocalFunctor
20+
open import GpdCont.TwoCategory.StrictFunctor.LocalFunctor
2121
open import Cubical.Categories.Functor.Base using (Functor)
2222
open import Cubical.Categories.Functor.Properties using (isFullyFaithfulG∘F)
2323

2424
isLocallyFullyFaithfulCompositeRestrict :
2525
isLocallyFullyFaithful F
2626
→ (∀ (c₁ c₂ : C.ob) → Functor.isFullyFaithful (LocalFunctor G (F.₀ c₁) (F.₀ c₂)))
27-
→ isLocallyFullyFaithful (compLaxFunctor F G)
27+
→ isLocallyFullyFaithful (compStrictFunctor F G)
2828
isLocallyFullyFaithfulCompositeRestrict F-ff G-ff c₁ c₂ = isFullyFaithfulG∘F
2929
{F = LocalFunctor F c₁ c₂}
3030
{G = LocalFunctor G (F.₀ c₁) (F.₀ c₂)}

‎GpdCont/TwoCategory/Displayed/Unit.agda‎

Lines changed: 72 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,10 @@ private
1010
module C = TwoCategory C
1111

1212
open import GpdCont.TwoCategory.LaxFunctor
13+
open import GpdCont.TwoCategory.StrictFunctor
1314
open import GpdCont.TwoCategory.Displayed.Base
1415
open import GpdCont.TwoCategory.Displayed.LaxFunctor
16+
open import GpdCont.TwoCategory.Displayed.StrictFunctor
1517

1618
open import Cubical.Data.Unit using (Unit ; tt ; isOfHLevelUnit)
1719

@@ -43,42 +45,74 @@ UnitOver = TotalTwoCategory.∫ C Unitᴰ
4345
ForgetUnit : LaxFunctor UnitOver C
4446
ForgetUnit = TotalTwoCategory.Fst C Unitᴰ
4547

46-
AddUnit : LaxFunctor C UnitOver
47-
AddUnit .LaxFunctor.F-ob = _, tt
48-
AddUnit .LaxFunctor.F-hom = _, tt
49-
AddUnit .LaxFunctor.F-rel = _, tt
50-
AddUnit .LaxFunctor.F-rel-id = refl
51-
AddUnit .LaxFunctor.F-rel-trans r s = refl
52-
AddUnit .LaxFunctor.F-trans-lax f g .fst = C.id-rel (C.comp-hom f g)
53-
AddUnit .LaxFunctor.F-trans-lax f g .snd = tt
54-
AddUnit .LaxFunctor.F-trans-lax-natural r s i .fst = (C.trans-unit-right (C.comp-rel r s) ∙ (sym $ C.trans-unit-left _)) i
55-
AddUnit .LaxFunctor.F-trans-lax-natural r s i .snd = tt
56-
AddUnit .LaxFunctor.F-id-lax x = C.id-rel (C.id-hom x) , tt
57-
AddUnit .LaxFunctor.F-assoc f g h i .fst = {! !}
58-
AddUnit .LaxFunctor.F-assoc f g h i .snd = tt
59-
AddUnit .LaxFunctor.F-unit-left = {! !}
60-
AddUnit .LaxFunctor.F-unit-right = {! !}
48+
AddUnit : StrictFunctor C UnitOver
49+
AddUnit .StrictFunctor.F-ob = _, tt
50+
AddUnit .StrictFunctor.F-hom = _, tt
51+
AddUnit .StrictFunctor.F-rel = _, tt
52+
AddUnit .StrictFunctor.F-rel-id = refl
53+
AddUnit .StrictFunctor.F-rel-trans r s = refl
54+
AddUnit .StrictFunctor.F-hom-comp f g = refl
55+
AddUnit .StrictFunctor.F-hom-id x = refl
56+
AddUnit .StrictFunctor.F-assoc-filler-left f g h .fst = refl
57+
AddUnit .StrictFunctor.F-assoc-filler-left f g h .snd = reflSquare _
58+
AddUnit .StrictFunctor.F-assoc-filler-right f g h .fst = refl
59+
AddUnit .StrictFunctor.F-assoc-filler-right f g h .snd = reflSquare _
60+
AddUnit .StrictFunctor.F-assoc f g h = λ i j → C.comp-hom-assoc f g h i , tt
61+
AddUnit .StrictFunctor.F-unit-left-filler f .fst = refl
62+
AddUnit .StrictFunctor.F-unit-left-filler f .snd = reflSquare _
63+
AddUnit .StrictFunctor.F-unit-left f = λ i j → C.comp-hom-unit-left f i , tt
64+
AddUnit .StrictFunctor.F-unit-right-filler f .fst = refl
65+
AddUnit .StrictFunctor.F-unit-right-filler f .snd = reflSquare _
66+
AddUnit .StrictFunctor.F-unit-right f = λ i j → C.comp-hom-unit-right f i , tt
6167

62-
ReindexUnit : ∀ {ℓo′ ℓh′ ℓr′ ℓoᴰ ℓhᴰ ℓrᴰ} (D : TwoCategory ℓo′ ℓh′ ℓr′) (F : LaxFunctor C D)
63-
→ (Dᴰ : TwoCategoryᴰ D ℓoᴰ ℓhᴰ ℓrᴰ)
64-
→ LaxFunctorᴰ F Unitᴰ Dᴰ
65-
→ LaxFunctor C (TotalTwoCategory.∫ D Dᴰ)
66-
ReindexUnit D F Dᴰ Fᴰ = F′ where
67-
module F = LaxFunctor F
68-
module Fᴰ = LaxFunctorᴰ Fᴰ
69-
F′ : LaxFunctor C (TotalTwoCategory.∫ D Dᴰ)
70-
F′ .LaxFunctor.F-ob x = F.₀ x , Fᴰ.₀ tt
71-
F′ .LaxFunctor.F-hom f = F.₁ f , Fᴰ.₁ tt
72-
F′ .LaxFunctor.F-rel r = F.₂ r , Fᴰ.₂ tt
73-
F′ .LaxFunctor.F-rel-id i = F.F-rel-id i , Fᴰ.F-rel-idᴰ i
74-
F′ .LaxFunctor.F-rel-trans r s i .fst = F.F-rel-trans r s i
75-
F′ .LaxFunctor.F-rel-trans r s i .snd = Fᴰ.F-rel-transᴰ tt tt i
76-
F′ .LaxFunctor.F-trans-lax f g .fst = F.F-trans-lax f g
77-
F′ .LaxFunctor.F-trans-lax f g .snd = Fᴰ.F-trans-laxᴰ tt tt
78-
F′ .LaxFunctor.F-trans-lax-natural r s i .fst = {! !}
79-
F′ .LaxFunctor.F-trans-lax-natural r s i .snd = {! !}
80-
F′ .LaxFunctor.F-id-lax x = {! !}
81-
F′ .LaxFunctor.F-assoc f g h i .fst = F.F-assoc f g h i
82-
F′ .LaxFunctor.F-assoc f g h i .snd = Fᴰ.F-assocᴰ tt tt tt i
83-
F′ .LaxFunctor.F-unit-left = {! !}
84-
F′ .LaxFunctor.F-unit-right = {! !}
68+
module _
69+
{ℓo′ ℓh′ ℓr′ ℓoᴰ ℓhᴰ ℓrᴰ}
70+
{D : TwoCategory ℓo′ ℓh′ ℓr′}
71+
(F : StrictFunctor C D)
72+
{Dᴰ : TwoCategoryᴰ D ℓoᴰ ℓhᴰ ℓrᴰ}
73+
(Fᴰ : StrictFunctorᴰ F Unitᴰ Dᴰ)
74+
where
75+
76+
private
77+
∫D = TotalTwoCategory.∫ D Dᴰ
78+
79+
module F = StrictFunctor F
80+
module Fᴰ = StrictFunctorᴰ Fᴰ
81+
82+
ReindexUnit : StrictFunctor C ∫D
83+
ReindexUnit .StrictFunctor.F-ob x .fst = F.₀ x
84+
ReindexUnit .StrictFunctor.F-ob x .snd = Fᴰ.₀ tt
85+
ReindexUnit .StrictFunctor.F-hom f .fst = F.₁ f
86+
ReindexUnit .StrictFunctor.F-hom f .snd = Fᴰ.₁ tt
87+
ReindexUnit .StrictFunctor.F-rel r .fst = F.₂ r
88+
ReindexUnit .StrictFunctor.F-rel r .snd = Fᴰ.₂ tt
89+
ReindexUnit .StrictFunctor.F-rel-id {f = f} i .fst = F.F-rel-id {f = f} i
90+
ReindexUnit .StrictFunctor.F-rel-id {f = f} i .snd = Fᴰ.F-rel-idᴰ tt i
91+
ReindexUnit .StrictFunctor.F-rel-trans r s i .fst = F.F-rel-trans r s i
92+
ReindexUnit .StrictFunctor.F-rel-trans r s i .snd = Fᴰ.F-rel-transᴰ tt tt i
93+
ReindexUnit .StrictFunctor.F-hom-comp f g i .fst = F.F-hom-comp f g i
94+
ReindexUnit .StrictFunctor.F-hom-comp f g i .snd = Fᴰ.F-hom-compᴰ tt tt i
95+
ReindexUnit .StrictFunctor.F-hom-id x i .fst = F.F-hom-id x i
96+
ReindexUnit .StrictFunctor.F-hom-id x i .snd = Fᴰ.F-hom-idᴰ tt i
97+
ReindexUnit .StrictFunctor.F-assoc-filler-left f g h .fst i .fst = F.F-assoc-filler-left f g h .fst i
98+
ReindexUnit .StrictFunctor.F-assoc-filler-left f g h .fst i .snd = Fᴰ.F-assoc-filler-leftᴰ tt tt tt .fst i
99+
ReindexUnit .StrictFunctor.F-assoc-filler-left f g h .snd i j .fst = F.F-assoc-filler-left f g h .snd i j
100+
ReindexUnit .StrictFunctor.F-assoc-filler-left f g h .snd i j .snd = Fᴰ.F-assoc-filler-leftᴰ tt tt tt .snd i j
101+
ReindexUnit .StrictFunctor.F-assoc-filler-right f g h .fst i .fst = F.F-assoc-filler-right f g h .fst i
102+
ReindexUnit .StrictFunctor.F-assoc-filler-right f g h .fst i .snd = Fᴰ.F-assoc-filler-rightᴰ tt tt tt .fst i
103+
ReindexUnit .StrictFunctor.F-assoc-filler-right f g h .snd i j .fst = F.F-assoc-filler-right f g h .snd i j
104+
ReindexUnit .StrictFunctor.F-assoc-filler-right f g h .snd i j .snd = Fᴰ.F-assoc-filler-rightᴰ tt tt tt .snd i j
105+
ReindexUnit .StrictFunctor.F-assoc f g h i j .fst = F.F-assoc f g h i j
106+
ReindexUnit .StrictFunctor.F-assoc f g h i j .snd = Fᴰ.F-assocᴰ tt tt tt i j
107+
ReindexUnit .StrictFunctor.F-unit-left-filler f .fst i .fst = F.F-unit-left-filler f .fst i
108+
ReindexUnit .StrictFunctor.F-unit-left-filler f .fst i .snd = Fᴰ.F-unit-left-fillerᴰ tt .fst i
109+
ReindexUnit .StrictFunctor.F-unit-left-filler f .snd i j .fst = F.F-unit-left-filler f .snd i j
110+
ReindexUnit .StrictFunctor.F-unit-left-filler f .snd i j .snd = Fᴰ.F-unit-left-fillerᴰ tt .snd i j
111+
ReindexUnit .StrictFunctor.F-unit-left f i j .fst = F.F-unit-left f i j
112+
ReindexUnit .StrictFunctor.F-unit-left f i j .snd = Fᴰ.F-unit-leftᴰ tt i j
113+
ReindexUnit .StrictFunctor.F-unit-right-filler f .fst i .fst = F.F-unit-right-filler f .fst i
114+
ReindexUnit .StrictFunctor.F-unit-right-filler f .fst i .snd = Fᴰ.F-unit-right-fillerᴰ tt .fst i
115+
ReindexUnit .StrictFunctor.F-unit-right-filler f .snd i j .fst = F.F-unit-right-filler f .snd i j
116+
ReindexUnit .StrictFunctor.F-unit-right-filler f .snd i j .snd = Fᴰ.F-unit-right-fillerᴰ tt .snd i j
117+
ReindexUnit .StrictFunctor.F-unit-right f i j .fst = F.F-unit-right f i j
118+
ReindexUnit .StrictFunctor.F-unit-right f i j .snd = Fᴰ.F-unit-rightᴰ tt i j

0 commit comments

Comments
 (0)