Skip to content

Commit 4e87e9d

Browse files
phijorphijor
committed
Interpretation of symmetric containers is a strict 2-functor
1 parent 59507bc commit 4e87e9d

File tree

6 files changed

+145
-28
lines changed

6 files changed

+145
-28
lines changed

‎GpdCont/Prelude.agda‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,9 @@ module _ where
106106
p ∙ (q ∙ (r ∙ s)) ≡⟨ assoc p q (r ∙ s) ⟩
107107
(p ∙ q) ∙ (r ∙ s) ∎
108108

109+
reflSquare : (x : A) → Square (refl′ x) (refl′ x) (refl′ x) (refl′ x)
110+
reflSquare x = λ i j → x
111+
109112
compSquareFiller : (p : x ≡ y) (q : y ≡ z) (p∙q : x ≡ z) → Type _
110113
compSquareFiller {x} p q p∙q = Square p p∙q refl q
111114

‎GpdCont/SymmetricContainer/TwoCategory.agda‎

Lines changed: 87 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -2,43 +2,106 @@ module GpdCont.SymmetricContainer.TwoCategory where
22

33
open import GpdCont.Prelude
44
open import GpdCont.SymmetricContainer.Base
5-
open import GpdCont.SymmetricContainer.Morphism using (idMorphism ; isGroupoidMorphism)
5+
open import GpdCont.SymmetricContainer.Morphism using (idMorphism ; isGroupoidMorphism ; Morphism)
66
open import GpdCont.SymmetricContainer.WildCat using (Eval ; EvalFunctor ; module EvalFunctor ; SymmContWildCat)
7-
open import GpdCont.SymmetricContainer.Eval using (⟦-⟧-Path ; ⟦-⟧ᵗ-Path)
7+
open import GpdCont.SymmetricContainer.Eval using (⟦-⟧-Path ; ⟦-⟧ᵗ-Path ; ⟦_⟧)
88
open import GpdCont.TwoCategory.Base
99
open import GpdCont.TwoCategory.TwoDiscrete using (TwoDiscrete)
1010
open import GpdCont.TwoCategory.LaxFunctor
11+
open import GpdCont.TwoCategory.StrictFunctor
12+
open import GpdCont.TwoCategory.HomotopyGroupoid using () renaming (hGpdCat to hGpd)
1113
open import GpdCont.TwoCategory.GroupoidEndo using (Endo)
12-
open import GpdCont.WildCat.NatTrans using (WildNatTransPath)
14+
open import GpdCont.WildCat.NatTrans using (WildNatTransPath ; isGroupoidHom→WildNatTransSquare)
15+
open import GpdCont.WildCat.TypeOfHLevel using (idNatTransₗ ; idNatTransᵣ ; hGroupoidNatTransSquare)
1316
open import GpdCont.WildCat.TypeOfHLevel using (idNat ; _⊛_)
1417

1518
open import GpdCont.Polynomial using (poly⟨_,_⟩ ; Polynomial)
1619

1720
import Cubical.Foundations.GroupoidLaws as GL
21+
open import Cubical.Foundations.Path using (compPath→Square)
1822
open import Cubical.WildCat.Base using (WildCat)
1923
open import Cubical.WildCat.Functor using (WildFunctor ; WildNatTrans)
2024

25+
{-# INJECTIVE_FOR_INFERENCE ⟨_⟩ #-}
26+
2127
SymmContCat : (ℓ : Level) → TwoCategory (ℓ-suc ℓ) ℓ ℓ
2228
SymmContCat ℓ = TwoDiscrete (SymmContWildCat ℓ) λ _ _ → isGroupoidMorphism
2329

24-
private
25-
module SymmContWildCat {ℓ} = WildCat (SymmContWildCat ℓ)
26-
⟦-⟧-id-lax : ∀ {ℓ} (C : SymmetricContainer ℓ) → idNat ℓ (Eval C) ≡ EvalFunctor.on-hom (idMorphism C)
27-
⟦-⟧-id-lax C = WildNatTransPath (λ X → funExt λ x → ⟦-⟧ᵗ-Path C refl refl) λ { v i j x → poly⟨ Polynomial.shape x , v ∘ Polynomial.label x ⟩ }
28-
29-
⟦-⟧-trans-lax : ∀ {ℓ} {F G H : SymmetricContainer ℓ} (f : SymmContWildCat.Hom[ F , G ]) (g : SymmContWildCat.Hom[ G , H ])
30-
→ _⊛_ ℓ (EvalFunctor.on-hom f) (EvalFunctor.on-hom g) ≡ EvalFunctor.on-hom (f SymmContWildCat.⋆ g)
31-
⟦-⟧-trans-lax {H} f g = WildNatTransPath (λ X → funExt λ x → ⟦-⟧ᵗ-Path H refl refl) λ { v i j x → poly⟨ {!_ !} , {! !} ⟩ }
32-
33-
⟦-⟧ : ∀ {ℓ} → LaxFunctor (SymmContCat ℓ) (Endo ℓ)
34-
⟦-⟧ .LaxFunctor.F-ob = Eval
35-
⟦-⟧ .LaxFunctor.F-hom = EvalFunctor.on-hom
36-
⟦-⟧ .LaxFunctor.F-rel = cong EvalFunctor.on-hom
37-
⟦-⟧ .LaxFunctor.F-rel-id = refl
38-
⟦-⟧ .LaxFunctor.F-rel-trans = GL.cong-∙ EvalFunctor.on-hom
39-
⟦-⟧ .LaxFunctor.F-trans-lax = ⟦-⟧-trans-lax
40-
⟦-⟧ .LaxFunctor.F-trans-lax-natural = {! !}
41-
⟦-⟧ .LaxFunctor.F-id-lax = ⟦-⟧-id-lax
42-
⟦-⟧ .LaxFunctor.F-assoc f g h = {! !}
43-
⟦-⟧ .LaxFunctor.F-unit-left = {! !}
44-
⟦-⟧ .LaxFunctor.F-unit-right = {! !}
30+
module ⟦-⟧ {ℓ} where
31+
private
32+
module SymmCont = TwoCategory (SymmContCat ℓ)
33+
module Endo = TwoCategory (Endo ℓ)
34+
module hGpd = TwoCategory (hGpd ℓ)
35+
36+
⟦_⟧₀ = Eval
37+
⟦_⟧₁ = EvalFunctor.on-hom
38+
39+
hom-comp : ∀ {F G H : SymmCont.ob} (f : SymmCont.hom F G) (g : SymmCont.hom G H)
40+
→ ⟦ f ⟧₁ Endo.∙₁ ⟦ g ⟧₁ ≡ ⟦ f SymmCont.∙₁ g ⟧₁
41+
hom-comp f g = sym (EvalFunctor.on-hom-seq f g)
42+
43+
hom-id : (F : SymmCont.ob) → Endo.id-hom ⟦ F ⟧₀ ≡ ⟦ SymmCont.id-hom F ⟧₁
44+
hom-id f = sym EvalFunctor.on-hom-id
45+
46+
module _ {F G : SymmCont.ob} (f : SymmCont.hom F G) where
47+
private module f = Morphism f
48+
unit-left-filler : PathCompFiller (cong (Endo._∙₁ ⟦ f ⟧₁) (hom-id F)) (hom-comp (SymmCont.id-hom F) f)
49+
unit-left-filler .fst = Endo.comp-hom-unit-left ⟦ f ⟧₁
50+
unit-left-filler .snd = hGroupoidNatTransSquare ℓ λ X → reflSquare _
51+
52+
unit-left : PathP (λ i → Endo.comp-hom-unit-left ⟦ f ⟧₁ i ≡ ⟦ f ⟧₁) (Endo.comp-hom-unit-left ⟦ f ⟧₁) (refl′ ⟦ f ⟧₁)
53+
unit-left i j = Endo.comp-hom-unit-left ⟦ f ⟧₁ (i ∨ j)
54+
55+
unit-right-filler : PathCompFiller (cong (⟦ f ⟧₁ Endo.∙₁_) (hom-id G)) (hom-comp f (SymmCont.id-hom G))
56+
unit-right-filler .fst = Endo.comp-hom-unit-right ⟦ f ⟧₁
57+
unit-right-filler .snd = hGroupoidNatTransSquare ℓ λ X → reflSquare _
58+
59+
unit-right : PathP (λ i → Endo.comp-hom-unit-right ⟦ f ⟧₁ i ≡ ⟦ f ⟧₁) (Endo.comp-hom-unit-right ⟦ f ⟧₁) (refl′ ⟦ f ⟧₁)
60+
unit-right i j = Endo.comp-hom-unit-right ⟦ f ⟧₁ (i ∨ j)
61+
62+
module _ {F G H : SymmCont.ob} (f : SymmCont.hom F G) (g : SymmCont.hom G H) where
63+
open WildNatTrans
64+
comp-hom-nat-filler : ∀ {x y} (α : hGpd.hom x y) → (⟦ f ⟧₁ Endo.∙₁ ⟦ g ⟧₁) .N-hom {x} {y} α ≡ refl
65+
comp-hom-nat-filler α = sym GL.compPathRefl
66+
67+
module _ {F G H K : SymmCont.ob} (f : SymmCont.hom F G) (g : SymmCont.hom G H) (h : SymmCont.hom H K) where
68+
open WildNatTrans
69+
70+
assoc-filler-left : PathCompFiller (cong (Endo._∙₁ ⟦ h ⟧₁) (hom-comp f g)) (hom-comp (f SymmCont.∙₁ g) h)
71+
assoc-filler-left .fst = WildNatTransPath
72+
(λ X → refl)
73+
λ {x} {y} α →
74+
((⟦ f ⟧₁ Endo.∙₁ ⟦ g ⟧₁) Endo.∙₁ ⟦ h ⟧₁) .N-hom {x} {y} α ≡[ i ]⟨ ((hom-comp f g i) Endo.∙₁ ⟦ h ⟧₁) .N-hom {x} {y} α ⟩
75+
(⟦ f SymmCont.∙₁ g ⟧₁ Endo.∙₁ ⟦ h ⟧₁) .N-hom {x} {y} α ≡⟨ comp-hom-nat-filler (f SymmCont.∙₁ g) h {x} {y} α ⟩
76+
⟦ (f SymmCont.∙₁ g) SymmCont.∙₁ h ⟧₁ .N-hom {x} {y} α ∎
77+
assoc-filler-left .snd = hGroupoidNatTransSquare ℓ λ X → reflSquare _
78+
79+
assoc-filler-right : PathCompFiller (cong (⟦ f ⟧₁ Endo.∙₁_) (hom-comp g h)) (hom-comp f (g SymmCont.∙₁ h))
80+
assoc-filler-right .fst = WildNatTransPath (λ X → refl)
81+
λ {x} {y} α →
82+
(⟦ f ⟧₁ Endo.∙₁ (⟦ g ⟧₁ Endo.∙₁ ⟦ h ⟧₁)) .N-hom {x} {y} α ≡[ i ]⟨ (⟦ f ⟧₁ Endo.∙₁ (hom-comp g h i)) .N-hom {x} {y} α ⟩
83+
(⟦ f ⟧₁ Endo.∙₁ (⟦ g SymmCont.∙₁ h ⟧₁)) .N-hom {x} {y} α ≡⟨ comp-hom-nat-filler f (g SymmCont.∙₁ h) {x} {y} α ⟩
84+
⟦ f SymmCont.∙₁ (g SymmCont.∙₁ h) ⟧₁ .N-hom {x} {y} α ∎
85+
assoc-filler-right .snd = hGroupoidNatTransSquare ℓ λ X → reflSquare _
86+
87+
assoc : PathP
88+
(λ i → Endo.comp-hom-assoc ⟦ f ⟧₁ ⟦ g ⟧₁ ⟦ h ⟧₁ i ≡ ⟦ SymmCont.comp-hom-assoc f g h i ⟧₁)
89+
(assoc-filler-left .fst)
90+
(assoc-filler-right .fst)
91+
assoc = hGroupoidNatTransSquare ℓ λ X → reflSquare _
92+
93+
⟦-⟧ : ∀ {ℓ} → StrictFunctor (SymmContCat ℓ) (Endo ℓ)
94+
⟦-⟧ .StrictFunctor.F-ob = Eval
95+
⟦-⟧ .StrictFunctor.F-hom = EvalFunctor.on-hom
96+
⟦-⟧ .StrictFunctor.F-rel = cong EvalFunctor.on-hom
97+
⟦-⟧ .StrictFunctor.F-rel-id = refl
98+
⟦-⟧ .StrictFunctor.F-rel-trans = GL.cong-∙ EvalFunctor.on-hom
99+
⟦-⟧ .StrictFunctor.F-hom-comp = ⟦-⟧.hom-comp
100+
⟦-⟧ .StrictFunctor.F-hom-id = ⟦-⟧.hom-id
101+
⟦-⟧ .StrictFunctor.F-assoc-filler-left = ⟦-⟧.assoc-filler-left
102+
⟦-⟧ .StrictFunctor.F-assoc-filler-right = ⟦-⟧.assoc-filler-right
103+
⟦-⟧ .StrictFunctor.F-assoc = ⟦-⟧.assoc
104+
⟦-⟧ .StrictFunctor.F-unit-left-filler = ⟦-⟧.unit-left-filler
105+
⟦-⟧ .StrictFunctor.F-unit-left = ⟦-⟧.unit-left
106+
⟦-⟧ .StrictFunctor.F-unit-right-filler = ⟦-⟧.unit-right-filler
107+
⟦-⟧ .StrictFunctor.F-unit-right = ⟦-⟧.unit-right

‎GpdCont/TwoCategory/GroupoidEndo.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ open import GpdCont.TwoCategory.Base
55
open import GpdCont.TwoCategory.Isomorphism
66
open import GpdCont.TwoCategory.TwoDiscrete using (TwoDiscrete)
77
open import GpdCont.WildCat.TypeOfHLevel using (hGroupoidEndo ; isGroupoidEndoNatTrans)
8+
open import GpdCont.WildCat.NatTrans using (WildNatTransPath ; isGroupoidHom→WildNatTransSquare)
89

910
open import Cubical.Foundations.HLevels
1011
open import Cubical.Foundations.GroupoidLaws

‎GpdCont/WildCat/NatTrans.agda‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,3 +24,35 @@ WildNatTransPath : {F G : WildFunctor C D} {α β : WildNatTrans C D F G}
2424
→ α ≡ β
2525
WildNatTransPath ob-path hom-path i .N-ob x = ob-path x i
2626
WildNatTransPath ob-path hom-path i .N-hom f = hom-path f i
27+
28+
WildNatTransSquare : ∀ {ℓo ℓo′ ℓh ℓh′} {C : WildCat ℓo ℓh} {D : WildCat ℓo′ ℓh′} {F G : WildFunctor C D}
29+
→ {α₀₀ α₀₁ : WildNatTrans C D F G}
30+
→ {α₀₋ : α₀₀ ≡ α₀₁}
31+
→ {α₁₀ α₁₁ : WildNatTrans C D F G}
32+
→ {α₁₋ : α₁₀ ≡ α₁₁}
33+
→ {α₋₀ : α₀₀ ≡ α₁₀}
34+
→ {α₋₁ : α₀₁ ≡ α₁₁}
35+
→ (ob-square : ∀ (x : C .ob) → Square (cong N-ob α₀₋ ≡$ x) (cong N-ob α₁₋ ≡$ x) (cong N-ob α₋₀ ≡$ x) (cong N-ob α₋₁ ≡$ x))
36+
→ (hom-square : ∀ {x y} (f : C [ x , y ])
37+
→ SquareP (λ i j → (F .F-hom f) ⋆⟨ D ⟩ (ob-square y i j) ≡ (ob-square x i j) ⋆⟨ D ⟩ (G .F-hom f)) (λ j → α₀₋ j .N-hom f) (λ j → α₁₋ j .N-hom f) (λ i → α₋₀ i .N-hom f) (λ i → α₋₁ i .N-hom f)
38+
)
39+
→ Square α₀₋ α₁₋ α₋₀ α₋₁
40+
WildNatTransSquare ob-square hom-square i j .N-ob x = ob-square x i j
41+
WildNatTransSquare ob-square hom-square i j .N-hom f = hom-square f i j
42+
43+
isGroupoidHom→WildNatTransSquare : {F G : WildFunctor C D}
44+
→ (∀ {x y} → isGroupoid (D [ x , y ]))
45+
→ {α₀₀ α₀₁ : WildNatTrans C D F G}
46+
→ {α₀₋ : α₀₀ ≡ α₀₁}
47+
→ {α₁₀ α₁₁ : WildNatTrans C D F G}
48+
→ {α₁₋ : α₁₀ ≡ α₁₁}
49+
→ {α₋₀ : α₀₀ ≡ α₁₀}
50+
→ {α₋₁ : α₀₁ ≡ α₁₁}
51+
→ (ob-square : ∀ (x : C .ob) → Square (cong N-ob α₀₋ ≡$ x) (cong N-ob α₁₋ ≡$ x) (cong N-ob α₋₀ ≡$ x) (cong N-ob α₋₁ ≡$ x))
52+
→ Square α₀₋ α₁₋ α₋₀ α₋₁
53+
isGroupoidHom→WildNatTransSquare {C} {D} {F} {G} gpd-hom ob-square = WildNatTransSquare
54+
ob-square
55+
λ {x} {y} f → isSet→SquareP
56+
{A = λ i j → concatMor D (F .F-hom f) (ob-square y i j) ≡ concatMor D (ob-square x i j) (G .F-hom f)}
57+
(λ i j → gpd-hom _ _)
58+
_ _ _ _

‎GpdCont/WildCat/TypeOfHLevel.agda‎

Lines changed: 20 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -101,10 +101,11 @@ module _ (ℓ : Level) where
101101
hGroupoidEndo .⋆IdR = idNatTransᵣ
102102
hGroupoidEndo .⋆Assoc = assocNatTrans
103103

104+
open WildFunctor
105+
open WildNatTrans
106+
104107
isGroupoidEndoNatTrans : ∀ F G → isGroupoid (hGroupoidEndo [ F , G ])
105108
isGroupoidEndoNatTrans F G = isGroupoidRetract {B = NatTrans′} toNatTrans′ fromNatTrans′ retr isGroupoidNatTrans′ where
106-
open WildFunctor
107-
open WildNatTrans
108109
NatTrans′ = Σ[ α ∈ (∀ X → ⟨ F .F-ob X ⟩ → ⟨ G .F-ob X ⟩) ] ∀ X Y (H : ⟨ X ⟩ → ⟨ Y ⟩) → F .F-hom H ⋆ α Y ≡ α X ⋆ G .F-hom H
109110

110111
isGroupoidNatTrans′ : isGroupoid NatTrans′
@@ -124,6 +125,23 @@ module _ (ℓ : Level) where
124125
retr α i .N-ob = α .N-ob
125126
retr α i .N-hom = α .N-hom
126127

128+
hGroupoidNatTransPath : ∀ {F G} {α β : hGroupoidEndo [ F , G ]}
129+
→ (ob-path : ∀ X → α .N-ob X ≡ β .N-ob X)
130+
→ (∀ {x} {y} (f : hGroupoidCat [ x , y ]) → PathP (λ i → F .F-hom f ⋆ (ob-path y i) ≡ (ob-path x i) ⋆ G .F-hom f) _ _)
131+
→ α ≡ β
132+
hGroupoidNatTransPath = WildNatTransPath
133+
134+
hGroupoidNatTransSquare : ∀ {F G}
135+
→ {α₀₀ α₀₁ : hGroupoidEndo [ F , G ]}
136+
→ {α₀₋ : α₀₀ ≡ α₀₁}
137+
→ {α₁₀ α₁₁ : hGroupoidEndo [ F , G ]}
138+
→ {α₁₋ : α₁₀ ≡ α₁₁}
139+
→ {α₋₀ : α₀₀ ≡ α₁₀}
140+
→ {α₋₁ : α₀₁ ≡ α₁₁}
141+
→ (ob-square : ∀ X → Square (cong N-ob α₀₋ ≡$ X) (cong N-ob α₁₋ ≡$ X) (cong N-ob α₋₀ ≡$ X) (cong N-ob α₋₁ ≡$ X))
142+
→ Square α₀₋ α₁₋ α₋₀ α₋₁
143+
hGroupoidNatTransSquare = isGroupoidHom→WildNatTransSquare (λ {x} {y} → isGroupoidΠ λ _ → str y)
144+
127145
open WildCat hiding (_⋆_)
128146
hseq' : ∀ {ℓ} (x y z : hGroupoidCat ℓ .ob) (f : hGroupoidCat ℓ [ x , y ]) (g : hGroupoidCat ℓ [ y , z ]) → hGroupoidCat ℓ [ x , z ]
129147
hseq' x y z = concatMor (hGroupoidCat _) {x = x} {y = y} {z = z}

‎README.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ module 2·1-SymmetricContainers where
6363
open import GpdCont.SymmetricContainer.Examples using (CyclicList)
6464

6565
open import GpdCont.TwoCategory.Base using (TwoCategory)
66-
open import GpdCont.TwoCategory.LaxFunctor using (LaxFunctor)
66+
open import GpdCont.TwoCategory.StrictFunctor using (StrictFunctor)
6767
open import GpdCont.TwoCategory.GroupoidEndo using (Endo)
6868

6969

@@ -79,7 +79,7 @@ module 2·1-SymmetricContainers where
7979
11-Defintion : (G : SymmetricContainer ℓ) → (hGroupoid ℓ → hGroupoid ℓ)
8080
11-Defintion = ⟦_⟧
8181

82-
_ : LaxFunctor (SymmContCat ℓ) (Endo ℓ)
82+
_ : StrictFunctor (SymmContCat ℓ) (Endo ℓ)
8383
_ = ⟦-⟧
8484

8585
12-Example : SymmetricContainer ℓ-zero

0 commit comments

Comments
 (0)