Skip to content

Commit d48de47

Browse files
plt-amyplt-amy
committed
defn: fundamental pregroupoids
This aux. definition allows us to compute indexed co/products as co/limits even when the indexing type does not have an h-level.
1 parent ef62ca3 commit d48de47

File tree

8 files changed

+230
-143
lines changed

8 files changed

+230
-143
lines changed

‎src/Cat/Diagram/Colimit/Coproduct.lagda.md‎

Lines changed: 35 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,9 @@ description: |
88
```agda
99
open import Cat.Diagram.Coproduct.Indexed
1010
open import Cat.Instances.Shape.Terminal
11+
open import Cat.Instances.Discrete.Pre
1112
open import Cat.Diagram.Colimit.Base
1213
open import Cat.Instances.Shape.Two
13-
open import Cat.Instances.Discrete
1414
open import Cat.Diagram.Coproduct
1515
open import Cat.Functor.Constant
1616
open import Cat.Functor.Kan.Base
@@ -110,71 +110,60 @@ Colimit→Coproduct colim .has-is-coproduct =
110110

111111
## Indexed coproducts as colimits
112112

113-
Similarly to the product case, when $I$ is a groupoid, indexed
114-
coproducts correspond to colimits of discrete diagrams of shape $I$.
113+
Similarly to the product case, coproducts indexed by a type $I$
114+
correspond to colimits of shape the [[fundamental pregroupoid]] of $I$.
115115

116116
```agda
117-
module _ {I : Type ℓ'} (i-is-grpd : is-groupoid I) (F : I → Ob) where
117+
module _ {I : Type ℓ'} (F : I → Ob) where
118118
open _=>_
119119
120-
Inj→Cocone : ∀ {x} → (∀ i → Hom (F i) x)
121-
→ Disc-adjunct {C = C} {iss = i-is-grpd} F => Const x
120+
Inj→Cocone : ∀ {x} → (∀ i → Hom (F i) x) → Π₁-adjunct C F => Const x
122121
Inj→Cocone inj .η i = inj i
123-
Inj→Cocone inj .is-natural i j p =
122+
Inj→Cocone inj .is-natural i j = elim! $
124123
J (λ j p → inj j ∘ subst (Hom (F i) ⊙ F) p id ≡ id ∘ inj i)
125-
(elimr (transport-refl id) ∙ sym (idl _)) p
124+
(elimr (transport-refl id) ∙ sym (idl _))
126125
127126
is-indexed-coproduct→is-colimit
128127
: ∀ {x} {inj : ∀ i → Hom (F i) x}
129128
→ is-indexed-coproduct C F inj
130-
→ is-colimit (Disc-adjunct F) x (Inj→Cocone inj)
131-
is-indexed-coproduct→is-colimit {x = x} {inj} ic =
132-
to-is-colimitp mc refl
133-
where
134-
module ic = is-indexed-coproduct ic
135-
open make-is-colimit
136-
137-
mc : make-is-colimit (Disc-adjunct F) x
138-
mc .ψ i = inj i
139-
mc .commutes {i} {j} p =
140-
J (λ j p → inj j ∘ subst (Hom (F i) ⊙ F) p id ≡ inj i)
141-
(elimr (transport-refl id))
142-
p
143-
mc .universal eta p = ic.match eta
144-
mc .factors eta p = ic.commute
145-
mc .unique eta p other q = ic.unique eta q
129+
→ is-colimit (Π₁-adjunct C F) x (Inj→Cocone inj)
130+
is-indexed-coproduct→is-colimit {x = x} {inj} ic = to-is-colimitp mc refl where
131+
module ic = is-indexed-coproduct ic
132+
open make-is-colimit
133+
134+
mc : make-is-colimit (Π₁-adjunct C F) x
135+
mc .ψ i = inj i
136+
mc .commutes {i} {j} = elim! $
137+
J (λ j p → inj j ∘ subst (Hom (F i) ⊙ F) p id ≡ inj i)
138+
(elimr (transport-refl id))
139+
mc .universal eta p = ic.match eta
140+
mc .factors eta p = ic.commute
141+
mc .unique eta p other q = ic.unique eta q
146142
147143
is-colimit→is-indexed-coprduct
148144
: ∀ {K : Functor ⊤Cat C}
149-
→ {eta : Disc-adjunct {iss = i-is-grpd} F => K F∘ !F}
150-
→ is-lan !F (Disc-adjunct F) K eta
145+
→ {eta : Π₁-adjunct C F => K F∘ !F}
146+
→ is-lan !F (Π₁-adjunct C F) K eta
151147
→ is-indexed-coproduct C F (eta .η)
152148
is-colimit→is-indexed-coprduct {K = K} {eta} colim = ic where
153149
module colim = is-colimit colim
154150
open is-indexed-coproduct hiding (eta)
155151
156152
ic : is-indexed-coproduct C F (eta .η)
157-
ic .match k =
158-
colim.universal k
159-
(J (λ j p → k j ∘ subst (Hom (F _) ⊙ F) p id ≡ k _)
160-
(elimr (transport-refl _)))
161-
ic .commute =
162-
colim.factors _ _
163-
ic .unique k comm =
164-
colim.unique _ _ _ comm
165-
166-
IC→Colimit
167-
: Indexed-coproduct C F
168-
→ Colimit {C = C} (Disc-adjunct {iss = i-is-grpd} F)
169-
IC→Colimit ic =
170-
to-colimit (is-indexed-coproduct→is-colimit has-is-ic)
153+
ic .match k = colim.universal k comm where abstract
154+
comm : {x y : I} (h : ∥ x ≡ y ∥₀) → k y ∘ Π₁-adjunct₁ C F h ≡ k x
155+
comm = elim! $ J
156+
(λ y p → k y ∘ path→iso (ap F p) .to ≡ k _) (elimr (transport-refl _))
157+
ic .commute = colim.factors _ _
158+
ic .unique k comm = colim.unique _ _ _ comm
159+
160+
IC→Colimit : Indexed-coproduct C F → Colimit (Π₁-adjunct C F)
161+
IC→Colimit ic = to-colimit (is-indexed-coproduct→is-colimit has-is-ic)
171162
where open Indexed-coproduct ic
172163
173-
Colimit→IC
174-
: Colimit {C = C} (Disc-adjunct {iss = i-is-grpd} F)
175-
→ Indexed-coproduct C F
164+
Colimit→IC : Colimit (Π₁-adjunct C F) → Indexed-coproduct C F
176165
Colimit→IC colim .Indexed-coproduct.ΣF = _
177-
Colimit→IC colim .Indexed-coproduct.ι = _
178-
Colimit→IC colim .Indexed-coproduct.has-is-ic =
179-
is-colimit→is-indexed-coprduct (Colimit.has-colimit colim)
166+
Colimit→IC colim .Indexed-coproduct.ι = _
167+
Colimit→IC colim .Indexed-coproduct.has-is-ic = is-colimit→is-indexed-coprduct $
168+
Colimit.has-colimit colim
180169
```

‎src/Cat/Diagram/Coproduct/Copower.lagda.md‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -119,8 +119,7 @@ uniqueness properties of colimiting maps.
119119
cocomplete→copowering
120120
: ∀ {o ℓ} {C : Precategory o ℓ}
121121
→ is-cocomplete ℓ ℓ C → Functor (Sets ℓ ×ᶜ C) C
122-
cocomplete→copowering colim = Copowers.Copowering λ S F →
123-
Colimit→IC _ (is-hlevel-suc 2 (S .is-tr)) F (colim _)
122+
cocomplete→copowering colim = Copowers.Copowering λ S F → Colimit→IC _ F (colim _)
124123
```
125124
-->
126125

‎src/Cat/Diagram/Initial/Weak.lagda.md‎

Lines changed: 15 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ open import Cat.Diagram.Limit.Product
77
open import Cat.Diagram.Limit.Base
88
open import Cat.Diagram.Equaliser
99
open import Cat.Diagram.Initial
10+
open import Cat.Univalent
1011
open import Cat.Prelude
1112
1213
import Cat.Reasoning as Cat
@@ -128,36 +129,36 @@ since $j$ equalises $f$ and $g$ by construction, we have $f = g$!
128129
```
129130

130131
Putting this together, we can show that, if a [[complete category]] has
131-
a small weakly initial family indexed by a [[set]], then it has an
132-
initial object.
132+
a small weakly initial family, then it has an initial object.
133133

134134
```agda
135135
is-complete-weak-initial→initial
136-
: ∀ {κ} {I : Type κ} (F : I → ⌞ C ⌟) ⦃ _ : ∀ {n} → H-Level I (2 + n) ⦄
136+
: ∀ {κ} {I : Type κ} (F : I → ⌞ C ⌟)
137137
→ is-complete κ (ℓ ⊔ κ) C
138138
→ is-weak-initial-fam F
139139
→ Initial C
140-
is-complete-weak-initial→initial {κ = κ} F compl wif = record { has⊥ = equal-is-initial } where
140+
is-complete-weak-initial→initial {κ = κ} {I} F compl wif =
141+
record { has⊥ = equal-is-initial } where
141142
```
142143

143144
<details>
144145
<summary>The proof is by pasting together the results above.</summary>
145146

146147
```agda
147-
open Indexed-product
148+
open Indexed-product
148149
149-
prod : Indexed-product C F
150-
prod = Limit→IP C (hlevel 3) F (is-complete-lower κ ℓ κ κ compl _)
150+
prod : Indexed-product C F
151+
prod = Limit→IP C F (is-complete-lower κ ℓ κ κ compl _)
151152
152-
prod-is-wi : is-weak-initial (prod .ΠF)
153-
prod-is-wi = is-wif→is-weak-initial F wif (prod .has-is-ip)
153+
prod-is-wi : is-weak-initial (prod .ΠF)
154+
prod-is-wi = is-wif→is-weak-initial F wif (prod .has-is-ip)
154155
155-
equal : Joint-equaliser C {I = Hom (prod .ΠF) (prod .ΠF)} λ h → h
156-
equal = Limit→Joint-equaliser C _ id (is-complete-lower κ κ lzero ℓ compl _)
157-
open Joint-equaliser equal using (has-is-je)
156+
equal : Joint-equaliser C {I = Hom (prod .ΠF) (prod .ΠF)} λ h → h
157+
equal = Limit→Joint-equaliser C _ id (is-complete-lower κ κ lzero ℓ compl _)
158+
open Joint-equaliser equal using (has-is-je)
158159
159-
equal-is-initial = is-weak-initial→equaliser _ prod-is-wi has-is-je λ f g →
160-
Limit→Equaliser C (is-complete-lower κ (ℓ ⊔ κ) lzero lzero compl _)
160+
equal-is-initial = is-weak-initial→equaliser _ prod-is-wi has-is-je λ f g →
161+
Limit→Equaliser C (is-complete-lower κ (ℓ ⊔ κ) lzero lzero compl _)
161162
```
162163

163164
</details>

‎src/Cat/Diagram/Limit/Product.lagda.md‎

Lines changed: 35 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,9 @@ description: |
88
```agda
99
open import Cat.Instances.Shape.Terminal
1010
open import Cat.Diagram.Product.Indexed
11+
open import Cat.Instances.Discrete.Pre
1112
open import Cat.Instances.Shape.Two
1213
open import Cat.Diagram.Limit.Base
13-
open import Cat.Instances.Discrete
1414
open import Cat.Functor.Constant
1515
open import Cat.Functor.Kan.Base
1616
open import Cat.Diagram.Product
@@ -112,72 +112,61 @@ Limit→Product lim .has-is-product =
112112

113113
## Indexed products as limits
114114

115-
In the particular case where $I$ is a groupoid, e.g. because it arises
116-
as the space of objects of a [[univalent category]], an [[indexed product]] for
117-
$F : I \to \cC$ is the same thing as a limit over $F$, considered as
118-
a functor $\rm{Disc}{I} \to \cC$. We can not lift this restriction: If
119-
$I$ is not a groupoid, then its path spaces $x = y$ are not necessarily
120-
sets, and so the `Disc`{.Agda} construction does not apply to it.
115+
We can also compute the *indexed* product of a *family* $F : I \to \cC$
116+
of objects as a limit, replacing the function $F$ with a diagram indexed
117+
by the [[fundamental pregroupoid]] of $I$.
121118

122119
```agda
123-
module _ {ℓ} {I : Type ℓ} (i-is-grpd : is-groupoid I) (F : I → Ob) where
120+
module _ {ℓ} {I : Type ℓ} (F : I → Ob) where
124121
open _=>_
125122
126-
Proj→Cone : ∀ {x} → (∀ i → Hom x (F i))
127-
→ Const x => Disc-adjunct {C = C} {iss = i-is-grpd} F
123+
Proj→Cone : ∀ {x} → (∀ i → Hom x (F i)) → Const x => Π₁-adjunct C F
128124
Proj→Cone π .η i = π i
129-
Proj→Cone π .is-natural i j p =
125+
Proj→Cone π .is-natural i j = elim! $
130126
J (λ j p → π j ∘ id ≡ subst (Hom (F i) ⊙ F) p id ∘ π i)
131127
(idr _ ∙ introl (transport-refl id))
132-
p
133128
134129
is-indexed-product→is-limit
135130
: ∀ {x} {π : ∀ i → Hom x (F i)}
136131
→ is-indexed-product C F π
137-
→ is-limit (Disc-adjunct F) x (Proj→Cone π)
138-
is-indexed-product→is-limit {x = x} {π} ip =
139-
to-is-limitp ml refl
140-
where
141-
module ip = is-indexed-product ip
142-
open make-is-limit
143-
144-
ml : make-is-limit (Disc-adjunct F) x
145-
ml .ψ j = π j
146-
ml .commutes {i} {j} p =
147-
J (λ j p → subst (Hom (F i) ⊙ F) p id ∘ π i ≡ π j)
148-
(eliml (transport-refl _))
149-
p
150-
ml .universal eps p = ip.tuple eps
151-
ml .factors eps p = ip.commute
152-
ml .unique eps p other q = ip.unique eps q
132+
→ is-limit (Π₁-adjunct C F) x (Proj→Cone π)
133+
is-indexed-product→is-limit {x = x} {π} ip = to-is-limitp ml refl where
134+
module ip = is-indexed-product ip
135+
open make-is-limit
136+
137+
ml : make-is-limit (Π₁-adjunct C F) x
138+
ml .ψ j = π j
139+
ml .commutes {i} {j} = elim! $
140+
J (λ j p → subst (Hom (F i) ⊙ F) p id ∘ π i ≡ π j)
141+
(eliml (transport-refl _))
142+
ml .universal eps p = ip.tuple eps
143+
ml .factors eps p = ip.commute
144+
ml .unique eps p other q = ip.unique eps q
153145
154146
is-limit→is-indexed-product
155147
: ∀ {K : Functor ⊤Cat C}
156-
→ {eps : K F∘ !F => Disc-adjunct {iss = i-is-grpd} F}
157-
→ is-ran !F (Disc-adjunct F) K eps
148+
→ {eps : K F∘ !F => Π₁-adjunct C F}
149+
→ is-ran !F (Π₁-adjunct C F) K eps
158150
→ is-indexed-product C F (eps .η)
159151
is-limit→is-indexed-product {K = K} {eps} lim = ip where
160152
module lim = is-limit lim
161153
open is-indexed-product
162154
163155
ip : is-indexed-product C F (eps .η)
164-
ip .tuple k =
165-
lim.universal k
166-
(J (λ j p → subst (Hom (F _) ⊙ F) p id ∘ k _ ≡ k j)
167-
(eliml (transport-refl _)))
168-
ip .commute =
169-
lim.factors _ _
170-
ip .unique k comm =
171-
lim.unique _ _ _ comm
172-
173-
IP→Limit : Indexed-product C F → Limit {C = C} (Disc-adjunct {iss = i-is-grpd} F)
174-
IP→Limit ip =
175-
to-limit (is-indexed-product→is-limit has-is-ip)
156+
ip .tuple k = lim.universal k comm where abstract
157+
comm : {x y : I} (h : ∥ x ≡ y ∥₀) → Π₁-adjunct₁ C F h ∘ k x ≡ k y
158+
comm {x} = elim! $ J
159+
(λ y p → path→iso (ap F p) .to ∘ k x ≡ k y) (eliml (transport-refl _))
160+
ip .commute = lim.factors _ _
161+
ip .unique k comm = lim.unique _ _ _ comm
162+
163+
IP→Limit : Indexed-product C F → Limit (Π₁-adjunct C F)
164+
IP→Limit ip = to-limit (is-indexed-product→is-limit has-is-ip)
176165
where open Indexed-product ip
177166
178-
Limit→IP : Limit {C = C} (Disc-adjunct {iss = i-is-grpd} F) → Indexed-product C F
167+
Limit→IP : Limit (Π₁-adjunct C F) → Indexed-product C F
179168
Limit→IP lim .Indexed-product.ΠF = _
180-
Limit→IP lim .Indexed-product.π = _
181-
Limit→IP lim .Indexed-product.has-is-ip =
182-
is-limit→is-indexed-product (Limit.has-limit lim)
169+
Limit→IP lim .Indexed-product.π = _
170+
Limit→IP lim .Indexed-product.has-is-ip = is-limit→is-indexed-product $
171+
Limit.has-limit lim
183172
```

‎src/Cat/Diagram/Projective/Strong.lagda.md‎

Lines changed: 13 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -106,12 +106,10 @@ ones for projective objects, so we omit the details.
106106
```agda
107107
preserves-strong-epis→strong-projective {P = P} hom-epi {X} {Y} e e-strong p =
108108
epi→surjective (el! (Hom P X)) (el! (Hom P Y))
109-
(e ∘_)
110-
(λ {c} → hom-epi e-strong .fst {c = c})
111-
p
109+
(e ∘_) (λ {c} → hom-epi e-strong .fst {c = c}) p
112110
113111
strong-projective→preserves-strong-epis {P = P} pro {X} {Y} {f = f} f-strong =
114-
surjective→strong-epi (el! (Hom P X)) (el! (Hom P Y)) (f ∘_) $ λ p →
112+
surjective→strong-epi (el! (Hom P X)) (el! (Hom P Y)) (f ∘_) $ λ p →
115113
pro f f-strong p
116114
```
117115
</details>
@@ -142,18 +140,20 @@ retract→strong-projective
142140
<summary>These proofs are more or less identical to the corresponding
143141
ones for projective objects.
144142
</summary>
143+
145144
```agda
146145
indexed-coproduct-strong-projective {P = P} {ι = ι} Idx-pro P-pro coprod {X} {Y} e e-strong p = do
147146
s ← Idx-pro
148-
(λ i → Σ[ sᵢ ∈ Hom (P i) X ] (e ∘ sᵢ ≡ p ∘ ι i)) (λ i → hlevel 2)
149-
(λ i → P-pro i e e-strong (p ∘ ι i))
147+
(λ i → Σ[ sᵢ ∈ Hom (P i) X ] (e ∘ sᵢ ≡ p ∘ ι i)) (λ i → hlevel 2)
148+
(λ i → P-pro i e e-strong (p ∘ ι i))
150149
pure (match (λ i → s i .fst) , unique₂ (λ i → pullr commute ∙ s i .snd))
151150
where open is-indexed-coproduct coprod
152151
153152
retract→strong-projective P-pro s r e e-strong p = do
154153
(t , t-factor) ← P-pro e e-strong (p ∘ r .retract)
155154
pure (t ∘ s , pulll t-factor ∙ cancelr (r .is-retract))
156155
```
156+
157157
</details>
158158

159159
Moreover, if $\cC$ has a [[zero object]] and a strong projective
@@ -174,11 +174,13 @@ zero+indexed-coproduct-strong-projective→strong-projective
174174
<summary>Following the general theme, the proof is identical
175175
to the non-strong case.
176176
</summary>
177+
177178
```agda
178179
zero+indexed-coproduct-strong-projective→strong-projective {ι = ι} z coprod ∐P-pro i =
179180
retract→strong-projective ∐P-pro (ι i) $
180181
zero→ι-has-retract C coprod z i
181182
```
183+
182184
</details>
183185

184186
## Enough strong projectives
@@ -235,15 +237,11 @@ so the corresponding coproduct is a strong projective.
235237
open Strong-projectives
236238
237239
strong-projectives : Strong-projectives
238-
strong-projectives .Pro X =
239-
∐! (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) (Pᵢ ⊙ fst)
240+
strong-projectives .Pro X = ∐! (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) (Pᵢ ⊙ fst)
240241
strong-projectives .present {X = X} =
241242
∐!.match (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) (Pᵢ ⊙ fst) snd
242-
strong-projectives .present-strong-epi =
243-
strong-sep
244-
strong-projectives .projective {X = X} =
245-
indexed-coproduct-strong-projective
246-
(Idx-pro X)
247-
(Pᵢ-pro ⊙ fst)
248-
(∐!.has-is-ic (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) (Pᵢ ⊙ fst))
243+
strong-projectives .present-strong-epi = strong-sep
244+
strong-projectives .projective {X = X} = indexed-coproduct-strong-projective
245+
(Idx-pro X) (Pᵢ-pro ⊙ fst)
246+
(∐!.has-is-ic (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) (Pᵢ ⊙ fst))
249247
```

0 commit comments

Comments
 (0)