Skip to content

Commit 3cdcd8b

Browse files
phijorphijor
committed
Define strict 2-functors of 2-categories
1 parent 97360d7 commit 3cdcd8b

File tree

1 file changed

+108
-0
lines changed

1 file changed

+108
-0
lines changed

‎GpdCont/TwoCategory/StrictFunctor.agda‎

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
module GpdCont.TwoCategory.StrictFunctor where
2+
3+
open import GpdCont.Prelude
4+
open import GpdCont.TwoCategory.Base
5+
import Cubical.Foundations.Path as Path
6+
import Cubical.Foundations.GroupoidLaws as GL
7+
8+
module _ {ℓo ℓo′ ℓh ℓh′ ℓr ℓr′}
9+
(C : TwoCategory ℓo ℓh ℓr)
10+
(D : TwoCategory ℓo′ ℓh′ ℓr′)
11+
where
12+
private
13+
ℓ = ℓ-max (ℓ-max ℓo (ℓ-max ℓh ℓr)) (ℓ-max ℓo′ (ℓ-max ℓh′ ℓr′))
14+
module C = TwoCategory C
15+
module D = TwoCategory D
16+
17+
record StrictFunctor : Type ℓ where
18+
no-eta-equality
19+
field
20+
F-ob : C.ob → D.ob
21+
F-hom : {x y : C.ob} → C.hom x y → D.hom (F-ob x) (F-ob y)
22+
F-rel : {x y : C.ob} {f g : C.hom x y} → C.rel f g → D.rel (F-hom f) (F-hom g)
23+
24+
₀ = F-ob
25+
₁ = F-hom
26+
₂ = F-rel
27+
28+
-- F-hom is (locally) a functor
29+
field
30+
F-rel-id : {x y : C.ob} {f : C.hom x y}
31+
→ F-rel (C.id-rel f) ≡ D.id-rel (F-hom f)
32+
F-rel-trans : {x y : C.ob} {f g h : C.hom x y}
33+
→ (r : C.rel f g)
34+
→ (s : C.rel g h)
35+
→ F-rel (r C.∙ᵥ s) ≡ (F-rel r) D.∙ᵥ (F-rel s)
36+
37+
-- Strictness constraints
38+
field
39+
-- Strict functoriality
40+
F-hom-comp : {x y z : C.ob} (f : C.hom x y) (g : C.hom y z)
41+
→ (F-hom f D.∙₁ F-hom g) ≡ (F-hom (f C.∙₁ g))
42+
F-hom-id : (x : C.ob) → D.id-hom (F-ob x) ≡ F-hom (C.id-hom x)
43+
44+
field
45+
-- Strict associativity
46+
-- ====================
47+
--
48+
-- The two fillers F-assoc-filler-{left,right} are uniquely determined;
49+
-- see `GpdCont.Prelude.isContrCompSquareFiller`. They are here to allow simpler
50+
-- proofs of `F-assoc`: For some functors these fillers are constant, and as such
51+
-- the type of `F-assoc` simplifies to a non-dependent path:
52+
--
53+
-- flip F-assoc : D.comp-hom-assoc (F₁ f) (F₁ g) (F₁ h) ≡ cong F₁ (C.comp-hom-assoc f g h)
54+
F-assoc-filler-left : {x y z w : C.ob} (f : C.hom x y) (g : C.hom y z) (h : C.hom z w)
55+
→ PathCompFiller (cong (D._∙₁ F-hom h) (F-hom-comp f g)) (F-hom-comp (f C.∙₁ g) h)
56+
57+
F-assoc-filler-right : {x y z w : C.ob} (f : C.hom x y) (g : C.hom y z) (h : C.hom z w)
58+
→ PathCompFiller (cong (F-hom f D.∙₁_) (F-hom-comp g h)) (F-hom-comp f (g C.∙₁ h))
59+
60+
F-assoc : {x y z w : C.ob} (f : C.hom x y) (g : C.hom y z) (h : C.hom z w)
61+
→ PathP (λ i → D.comp-hom-assoc (F-hom f) (F-hom g) (F-hom h) i ≡ F-hom (C.comp-hom-assoc f g h i))
62+
(F-assoc-filler-left f g h .fst)
63+
(F-assoc-filler-right f g h .fst)
64+
65+
-- Strict unitality
66+
-- ================
67+
--
68+
-- Like for associativity, implementations can provide a filler of their own choice.
69+
70+
-- Strict left-unitality
71+
F-unit-left-filler : {x y : C.ob} (f : C.hom x y)
72+
→ PathCompFiller (cong (D._∙₁ F-hom f) (F-hom-id x)) (F-hom-comp (C.id-hom x) f)
73+
F-unit-left : {x y : C.ob} (f : C.hom x y)
74+
→ PathP (λ i → D.comp-hom-unit-left (F-hom f) i ≡ F-hom (C.comp-hom-unit-left f i))
75+
(F-unit-left-filler f .fst)
76+
(refl′ (F-hom f))
77+
78+
-- Strict right-unitality
79+
F-unit-right-filler : {x y : C.ob} (f : C.hom x y)
80+
→ PathCompFiller (cong (F-hom f D.∙₁_) (F-hom-id y)) (F-hom-comp f (C.id-hom y))
81+
F-unit-right : {x y : C.ob} (f : C.hom x y)
82+
→ PathP (λ i → D.comp-hom-unit-right (F-hom f) i ≡ F-hom (C.comp-hom-unit-right f i))
83+
(F-unit-right-filler f .fst)
84+
(refl′ (F-hom f))
85+
86+
module _ {ℓo ℓh ℓr}
87+
(C : TwoCategory ℓo ℓh ℓr)
88+
where
89+
private
90+
module C = TwoCategory C
91+
92+
idStrictFunctor : StrictFunctor C C
93+
idStrictFunctor .StrictFunctor.F-ob = id _
94+
idStrictFunctor .StrictFunctor.F-hom = id _
95+
idStrictFunctor .StrictFunctor.F-rel = id _
96+
idStrictFunctor .StrictFunctor.F-rel-id = refl
97+
idStrictFunctor .StrictFunctor.F-rel-trans r s = refl
98+
idStrictFunctor .StrictFunctor.F-hom-comp f g = refl
99+
idStrictFunctor .StrictFunctor.F-hom-id x = refl
100+
idStrictFunctor .StrictFunctor.F-assoc-filler-left f g h .fst = refl′ (C.comp-hom (C.comp-hom f g) h)
101+
idStrictFunctor .StrictFunctor.F-assoc-filler-left f g h .snd = refl
102+
idStrictFunctor .StrictFunctor.F-assoc-filler-right f g h .fst = refl′ (C.comp-hom f (C.comp-hom g h))
103+
idStrictFunctor .StrictFunctor.F-assoc-filler-right f g h .snd = refl
104+
idStrictFunctor .StrictFunctor.F-assoc f g h = λ i j → C.comp-hom-assoc f g h i
105+
idStrictFunctor .StrictFunctor.F-unit-left-filler f = refl , refl
106+
idStrictFunctor .StrictFunctor.F-unit-left f i j = C.comp-hom-unit-left f i
107+
idStrictFunctor .StrictFunctor.F-unit-right-filler f = refl , refl
108+
idStrictFunctor .StrictFunctor.F-unit-right f = λ i j → C.comp-hom-unit-right f i

0 commit comments

Comments
 (0)