Skip to content

Commit 0229880

Browse files
TOTBWFTOTBWF
committed
chore: clean up the interface to initial objects
1 parent 4b4da21 commit 0229880

31 files changed

Lines changed: 503 additions & 377 deletions

‎src/Algebra/Group/Cat/FinitelyComplete.lagda.md‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -61,14 +61,13 @@ Zero-group = to-group zg where
6161
zg .make-group.idl x = refl
6262
6363
Zero-group-is-initial : is-initial (Groups ℓ) Zero-group
64-
Zero-group-is-initial (_ , G) .centre = ∫hom (λ x → G.unit) gh where
64+
Zero-group-is-initial .is-initial.¡ {_ , G} = ∫hom (λ x → G.unit) gh where
6565
module G = Group-on G
6666
gh : is-group-hom _ _ (λ x → G.unit)
6767
gh .pres-⋆ x y =
6868
G.unit ≡˘⟨ G.idl ⟩
6969
G.unit G.⋆ G.unit ∎
70-
Zero-group-is-initial (_ , G) .paths x =
71-
ext λ _ → sym (is-group-hom.pres-id (x .snd))
70+
Zero-group-is-initial .is-initial.¡-unique f = ext λ _ → is-group-hom.pres-id (f .snd)
7271
7372
Zero-group-is-terminal : is-terminal (Groups ℓ) Zero-group
7473
Zero-group-is-terminal .is-terminal.! = ∫hom (λ _ → lift tt) (record { pres-⋆ = λ _ _ → refl })

‎src/Algebra/Quasigroup/Instances/Initial.lagda.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -51,13 +51,13 @@ of quasigroups, as there is a unique function out of the empty type.
5151

5252
```agda
5353
Empty-quasigroup-is-initial : is-initial (Quasigroups ℓ) Empty-quasigroup
54-
Empty-quasigroup-is-initial A .centre .fst ()
55-
Empty-quasigroup-is-initial A .centre .snd .is-quasigroup-hom.pres-⋆ ()
56-
Empty-quasigroup-is-initial A .paths f = ext λ ()
54+
Empty-quasigroup-is-initial .is-initial.¡ .fst ()
55+
Empty-quasigroup-is-initial .is-initial.¡ .snd .is-quasigroup-hom.pres-⋆ ()
56+
Empty-quasigroup-is-initial .is-initial.¡-unique f = ext λ ()
5757
5858
Initial-quasigroup : Initial (Quasigroups ℓ)
5959
Initial-quasigroup .Initial.bot = Empty-quasigroup
60-
Initial-quasigroup .Initial.has⊥ = Empty-quasigroup-is-initial
60+
Initial-quasigroup .Initial.has-is-init = Empty-quasigroup-is-initial
6161
```
6262

6363
In fact, the empty quasigroup is a [[strict initial object]].

‎src/Algebra/Ring/Cat/Initial.lagda.md‎

Lines changed: 96 additions & 95 deletions
Original file line numberDiff line numberDiff line change
@@ -69,8 +69,9 @@ prove...], so here it is:
6969

7070
```agda
7171
Int-is-initial : is-initial (Rings ℓ) Liftℤ
72-
Int-is-initial R = contr z→r λ x → ext (lemma x) where
73-
module R = Kit R
72+
Int-is-initial = hom-contr→is-initial λ R → contr (z→r R) λ h → ext (lemma R h) where
73+
module _ (R : Ring ℓ) where
74+
module R = Kit R
7475
```
7576

7677
Note that we treat 1 with care: we could have this map 1 to `1r + 0r`,
@@ -79,10 +80,10 @@ embedding. This will result in a bit more work right now, but is work
7980
worth doing.
8081

8182
```agda
82-
e : Nat → ⌞ R ⌟
83-
e zero = R.0r
84-
e (suc zero) = R.1r
85-
e (suc (suc x)) = R.1r R.+ e (suc x)
83+
e : Nat → ⌞ R ⌟
84+
e zero = R.0r
85+
e (suc zero) = R.1r
86+
e (suc (suc x)) = R.1r R.+ e (suc x)
8687
```
8788

8889
Zero gets sent to zero, and "adding one" gets sent to adding one. Is
@@ -92,32 +93,32 @@ naturals to sums in $R$, and products of naturals to products in $R$.
9293
We'll need this later.
9394

9495
```agda
95-
e-suc : ∀ n → e (suc n) ≡ R.1r R.+ e n
96-
e-add : ∀ m n → e (m Nat.+ n) ≡ e m R.+ e n
97-
e-mul : ∀ m n → e (m Nat.* n) ≡ e m R.* e n
96+
e-suc : ∀ n → e (suc n) ≡ R.1r R.+ e n
97+
e-add : ∀ m n → e (m Nat.+ n) ≡ e m R.+ e n
98+
e-mul : ∀ m n → e (m Nat.* n) ≡ e m R.* e n
9899
```
99100

100101
<!--
101102
```agda
102-
e-suc zero = sym R.+-idr
103-
e-suc (suc n) = refl
104-
105-
e-add zero n = sym R.+-idl
106-
e-add (suc m) n =
107-
e (suc m Nat.+ n) ≡⟨ e-suc (m Nat.+ n) ⟩
108-
R.1r R.+ e (m Nat.+ n) ≡⟨ ap (R.1r R.+_) (e-add m n) ⟩
109-
R.1r R.+ (e m R.+ e n) ≡⟨ R.+-associative ⟩
110-
(R.1r R.+ e m) R.+ e n ≡˘⟨ ap (R._+ e n) (e-suc m) ⟩
111-
e (suc m) R.+ e n ∎
112-
113-
e-mul zero n = sym R.*-zerol
114-
e-mul (suc m) n =
115-
e (suc m Nat.* n) ≡⟨ e-add n (m Nat.* n) ⟩
116-
e n R.+ e (m Nat.* n) ≡⟨ ap (e n R.+_) (e-mul m n) ⟩
117-
e n R.+ e m R.* e n ≡˘⟨ ap (R._+ (e m R.* e n)) R.*-idl ⟩
118-
R.1r R.* e n R.+ e m R.* e n ≡˘⟨ R.*-distribr ⟩
119-
(R.1r R.+ e m) R.* e n ≡˘⟨ ap (R._* e n) (e-suc m) ⟩
120-
(e (suc m) R.* e n) ∎
103+
e-suc zero = sym R.+-idr
104+
e-suc (suc n) = refl
105+
106+
e-add zero n = sym R.+-idl
107+
e-add (suc m) n =
108+
e (suc m Nat.+ n) ≡⟨ e-suc (m Nat.+ n) ⟩
109+
R.1r R.+ e (m Nat.+ n) ≡⟨ ap (R.1r R.+_) (e-add m n) ⟩
110+
R.1r R.+ (e m R.+ e n) ≡⟨ R.+-associative ⟩
111+
(R.1r R.+ e m) R.+ e n ≡˘⟨ ap (R._+ e n) (e-suc m) ⟩
112+
e (suc m) R.+ e n ∎
113+
114+
e-mul zero n = sym R.*-zerol
115+
e-mul (suc m) n =
116+
e (suc m Nat.* n) ≡⟨ e-add n (m Nat.* n) ⟩
117+
e n R.+ e (m Nat.* n) ≡⟨ ap (e n R.+_) (e-mul m n) ⟩
118+
e n R.+ e m R.* e n ≡˘⟨ ap (R._+ (e m R.* e n)) R.*-idl ⟩
119+
R.1r R.* e n R.+ e m R.* e n ≡˘⟨ R.*-distribr ⟩
120+
(R.1r R.+ e m) R.* e n ≡˘⟨ ap (R._* e n) (e-suc m) ⟩
121+
(e (suc m) R.* e n) ∎
121122
```
122123
-->
123124

@@ -129,13 +130,13 @@ integers, i.e. we need $e(m) - e(n) = e(1 + m) - e(1 + n)$. This is
129130
annoying to show, but not _too_ annoying:
130131

131132
```agda
132-
e-tr : ∀ m n → e m R.- e n ≡ e (suc m) R.- e (suc n)
133-
e-tr m n = sym $
134-
(e (suc m) R.- e (suc n)) ≡⟨ ap₂ R._-_ (e-suc m) (e-suc n) ⟩
135-
(R.1r R.+ e m) R.- (R.1r R.+ e n) ≡⟨ ap₂ R._+_ refl (R.a.inv-comm ∙ R.+-commutes) ∙ R.+-associative ⟩
136-
R.1r R.+ e m R.+ (R.- R.1r) R.+ (R.- e n) ≡⟨ ap₂ R._+_ (R.pullr R.+-commutes ∙ R.pulll refl) refl ⟩
137-
R.1r R.+ (R.- R.1r) R.+ e m R.+ (R.- e n) ≡⟨ ap₂ R._+_ (R.eliml R.+-invr) refl ⟩
138-
e m R.- e n ∎
133+
e-tr : ∀ m n → e m R.- e n ≡ e (suc m) R.- e (suc n)
134+
e-tr m n = sym $
135+
(e (suc m) R.- e (suc n)) ≡⟨ ap₂ R._-_ (e-suc m) (e-suc n) ⟩
136+
(R.1r R.+ e m) R.- (R.1r R.+ e n) ≡⟨ ap₂ R._+_ refl (R.a.inv-comm ∙ R.+-commutes) ∙ R.+-associative ⟩
137+
R.1r R.+ e m R.+ (R.- R.1r) R.+ (R.- e n) ≡⟨ ap₂ R._+_ (R.pullr R.+-commutes ∙ R.pulll refl) refl ⟩
138+
R.1r R.+ (R.- R.1r) R.+ e m R.+ (R.- e n) ≡⟨ ap₂ R._+_ (R.eliml R.+-invr) refl ⟩
139+
e m R.- e n ∎
139140
```
140141

141142
We can now build the embedding $\ZZ \mono R$. It remains to show that
@@ -144,58 +145,58 @@ algebra, so I won't comment on it too much: it can be worked out on
144145
paper, following the ring laws.
145146

146147
```agda
147-
ℤ↪R : Int → ⌞ R ⌟
148-
ℤ↪R (pos x) = e x
149-
ℤ↪R (negsuc x) = R.- (e (suc x))
150-
151-
open is-ring-hom
152-
153-
z-nat-diff : ∀ x y → ℤ↪R (x ℕ- y) ≡ e x R.- e y
154-
z-nat-diff x zero = R.intror R.inv-unit
155-
z-nat-diff zero (suc y) = R.introl refl
156-
z-nat-diff (suc x) (suc y) = z-nat-diff x y ∙ e-tr x y
157-
158-
z-add : ∀ x y → ℤ↪R (x +ℤ y) ≡ ℤ↪R x R.+ ℤ↪R y
159-
z-add (pos x) (pos y) = e-add x y
160-
z-add (pos x) (negsuc y) = z-nat-diff x (suc y)
161-
z-add (negsuc x) (pos y) = z-nat-diff y (suc x) ∙ R.+-commutes
162-
z-add (negsuc x) (negsuc y) =
163-
R.- (e 1 R.+ e (suc x Nat.+ y)) ≡⟨ ap R.-_ (ap₂ R._+_ refl (e-add (suc x) y) ∙ R.extendl R.+-commutes) ⟩
164-
R.- (e (suc x) R.+ (e 1 R.+ e y)) ≡⟨ R.a.inv-comm ⟩
165-
(R.- (e 1 R.+ e y)) R.+ (R.- e (suc x)) ≡⟨ R.+-commutes ⟩
166-
(R.- e (suc x)) R.+ (R.- (e 1 R.+ e y)) ≡⟨ ap₂ R._+_ refl (ap R.-_ (sym (e-add 1 y))) ⟩
167-
(R.- e (suc x)) R.+ (R.- e (1 Nat.+ y)) ∎
168-
169-
z-mul : ∀ x y → ℤ↪R (x *ℤ y) ≡ ℤ↪R x R.* ℤ↪R y
170-
z-mul (pos x) (pos y) =
171-
ℤ↪R (assign pos (x Nat.* y)) ≡⟨ ap ℤ↪R (assign-pos (x Nat.* y)) ⟩
172-
e (x Nat.* y) ≡⟨ e-mul x y ⟩
173-
(e x R.* e y) ∎
174-
z-mul (posz) (negsuc y) = sym R.*-zerol
175-
z-mul (possuc x) (negsuc y) =
176-
R.- e (suc x Nat.* suc y) ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩
177-
R.- (e (suc x) R.* e (suc y)) ≡˘⟨ R.*-negater ⟩
178-
e (suc x) R.* (R.- e (suc y)) ∎
179-
z-mul (negsuc x) (posz) =
180-
ℤ↪R (assign neg (x Nat.* 0)) ≡⟨ ap ℤ↪R (ap (assign neg) (Nat.*-zeror x)) ⟩
181-
ℤ↪R 0 ≡⟨ sym R.*-zeror ⟩
182-
ℤ↪R (negsuc x) R.* R.0r ∎
183-
z-mul (negsuc x) (possuc y) =
184-
R.- e (suc x Nat.* suc y) ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩
185-
R.- (e (suc x) R.* e (suc y)) ≡⟨ sym R.*-negatel ⟩
186-
(R.- e (suc x)) R.* e (suc y) ∎
187-
z-mul (negsuc x) (negsuc y) =
188-
e (suc x Nat.* suc y) ≡⟨ e-mul (suc x) (suc y) ⟩
189-
e (suc x) R.* e (suc y) ≡˘⟨ R.inv-inv ⟩
190-
R.- (R.- (e (suc x) R.* e (suc y))) ≡˘⟨ ap R.-_ R.*-negater ⟩
191-
R.- (e (suc x) R.* ℤ↪R (negsuc y)) ≡˘⟨ R.*-negatel ⟩
192-
ℤ↪R (negsuc x) R.* ℤ↪R (negsuc y) ∎
193-
194-
z→r : Rings.Hom Liftℤ R
195-
z→r .fst (lift x) = ℤ↪R x
196-
z→r .snd .pres-id = refl
197-
z→r .snd .pres-+ (lift x) (lift y) = z-add x y
198-
z→r .snd .pres-* (lift x) (lift y) = z-mul x y
148+
ℤ↪R : Int → ⌞ R ⌟
149+
ℤ↪R (pos x) = e x
150+
ℤ↪R (negsuc x) = R.- (e (suc x))
151+
152+
open is-ring-hom
153+
154+
z-nat-diff : ∀ x y → ℤ↪R (x ℕ- y) ≡ e x R.- e y
155+
z-nat-diff x zero = R.intror R.inv-unit
156+
z-nat-diff zero (suc y) = R.introl refl
157+
z-nat-diff (suc x) (suc y) = z-nat-diff x y ∙ e-tr x y
158+
159+
z-add : ∀ x y → ℤ↪R (x +ℤ y) ≡ ℤ↪R x R.+ ℤ↪R y
160+
z-add (pos x) (pos y) = e-add x y
161+
z-add (pos x) (negsuc y) = z-nat-diff x (suc y)
162+
z-add (negsuc x) (pos y) = z-nat-diff y (suc x) ∙ R.+-commutes
163+
z-add (negsuc x) (negsuc y) =
164+
R.- (e 1 R.+ e (suc x Nat.+ y)) ≡⟨ ap R.-_ (ap₂ R._+_ refl (e-add (suc x) y) ∙ R.extendl R.+-commutes) ⟩
165+
R.- (e (suc x) R.+ (e 1 R.+ e y)) ≡⟨ R.a.inv-comm ⟩
166+
(R.- (e 1 R.+ e y)) R.+ (R.- e (suc x)) ≡⟨ R.+-commutes ⟩
167+
(R.- e (suc x)) R.+ (R.- (e 1 R.+ e y)) ≡⟨ ap₂ R._+_ refl (ap R.-_ (sym (e-add 1 y))) ⟩
168+
(R.- e (suc x)) R.+ (R.- e (1 Nat.+ y)) ∎
169+
170+
z-mul : ∀ x y → ℤ↪R (x *ℤ y) ≡ ℤ↪R x R.* ℤ↪R y
171+
z-mul (pos x) (pos y) =
172+
ℤ↪R (assign pos (x Nat.* y)) ≡⟨ ap ℤ↪R (assign-pos (x Nat.* y)) ⟩
173+
e (x Nat.* y) ≡⟨ e-mul x y ⟩
174+
(e x R.* e y) ∎
175+
z-mul (posz) (negsuc y) = sym R.*-zerol
176+
z-mul (possuc x) (negsuc y) =
177+
R.- e (suc x Nat.* suc y) ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩
178+
R.- (e (suc x) R.* e (suc y)) ≡˘⟨ R.*-negater ⟩
179+
e (suc x) R.* (R.- e (suc y)) ∎
180+
z-mul (negsuc x) (posz) =
181+
ℤ↪R (assign neg (x Nat.* 0)) ≡⟨ ap ℤ↪R (ap (assign neg) (Nat.*-zeror x)) ⟩
182+
ℤ↪R 0 ≡⟨ sym R.*-zeror ⟩
183+
ℤ↪R (negsuc x) R.* R.0r ∎
184+
z-mul (negsuc x) (possuc y) =
185+
R.- e (suc x Nat.* suc y) ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩
186+
R.- (e (suc x) R.* e (suc y)) ≡⟨ sym R.*-negatel ⟩
187+
(R.- e (suc x)) R.* e (suc y) ∎
188+
z-mul (negsuc x) (negsuc y) =
189+
e (suc x Nat.* suc y) ≡⟨ e-mul (suc x) (suc y) ⟩
190+
e (suc x) R.* e (suc y) ≡˘⟨ R.inv-inv ⟩
191+
R.- (R.- (e (suc x) R.* e (suc y))) ≡˘⟨ ap R.-_ R.*-negater ⟩
192+
R.- (e (suc x) R.* ℤ↪R (negsuc y)) ≡˘⟨ R.*-negatel ⟩
193+
ℤ↪R (negsuc x) R.* ℤ↪R (negsuc y) ∎
194+
195+
z→r : Rings.Hom Liftℤ R
196+
z→r .fst (lift x) = ℤ↪R x
197+
z→r .snd .pres-id = refl
198+
z→r .snd .pres-+ (lift x) (lift y) = z-add x y
199+
z→r .snd .pres-* (lift x) (lift y) = z-mul x y
199200
```
200201

201202
The last thing we must show is that this is the _unique_ ring
@@ -215,14 +216,14 @@ and that last expression is pretty exactly what our canonical map
215216
evaluates to on $n$. So we're done!
216217
217218
```agda
218-
module _ (f : Rings.Hom Liftℤ R) where
219-
private module f = is-ring-hom (f .snd)
219+
module _ (f : Rings.Hom Liftℤ R) where
220+
private module f = is-ring-hom (f .snd)
220221
221-
f-pos : ∀ x → e x ≡ f · lift (pos x)
222-
f-pos zero = sym f.pres-0
223-
f-pos (suc x) = e-suc x ∙ sym (f.pres-+ (lift 1) (lift (pos x)) ∙ ap₂ R._+_ f.pres-id (sym (f-pos x)))
222+
f-pos : ∀ x → e x ≡ f · lift (pos x)
223+
f-pos zero = sym f.pres-0
224+
f-pos (suc x) = e-suc x ∙ sym (f.pres-+ (lift 1) (lift (pos x)) ∙ ap₂ R._+_ f.pres-id (sym (f-pos x)))
224225
225-
lemma : ∀ i → z→r · lift i ≡ f · lift i
226-
lemma (pos x) = f-pos x
227-
lemma (negsuc x) = sym (f.pres-neg {lift (possuc x)} ∙ ap R.-_ (sym (f-pos (suc x))))
226+
lemma : ∀ i → z→r · lift i ≡ f · lift i
227+
lemma (pos x) = f-pos x
228+
lemma (negsuc x) = sym (f.pres-neg {lift (possuc x)} ∙ ap R.-_ (sym (f-pos (suc x))))
228229
```

‎src/Algebra/Ring/Module/Action.lagda.md‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ open import Algebra.Group
88
open import Algebra.Ring
99
1010
open import Cat.Displayed.Univalence.Thin
11+
open import Cat.Diagram.Initial
1112
open import Cat.Abelian.Base
1213
open import Cat.Abelian.Endo
1314
open import Cat.Prelude hiding (_+_)
@@ -125,5 +126,7 @@ former!
125126

126127
```agda
127128
ℤ-module-unique : ∀ {ℓ} (G : Abelian-group ℓ) → is-contr (Ring-action Liftℤ (G .snd))
128-
ℤ-module-unique G = Equiv→is-hlevel 0 (Action≃Hom Liftℤ G) (Int-is-initial _)
129+
ℤ-module-unique G =
130+
Equiv→is-hlevel 0 (Action≃Hom Liftℤ G)
131+
$ is-initial→hom-contr Int-is-initial _
129132
```

‎src/Algebra/Ring/Solver.agda‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ open import Algebra.Group.Ab
1919
open import Algebra.Group
2020
open import Algebra.Ring
2121

22+
open import Cat.Diagram.Initial
2223
open import Cat.Displayed.Total
2324
open import Cat.Prelude hiding (_+_ ; _*_ ; _-_)
2425

@@ -38,13 +39,14 @@ open ∫Hom
3839
module Algebra.Ring.Solver where
3940

4041
module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
42+
open is-initial
4143
private
4244
R' : Ring _
4345
R' = record { fst = el _ (CRing-on.has-is-set cring) ; snd = CRing-on.has-ring-on cring }
4446

4547
module R = Kit R'
4648

47-
ℤ↪R-rh = Int-is-initial R' .centre
49+
ℤ↪R-rh = Int-is-initial .¡ {R'}
4850
module ℤ↪R = is-ring-hom (ℤ↪R-rh .snd)
4951

5052
open CRing-on cring using (*-commutes)
@@ -56,7 +58,7 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
5658
: {h' : Int → R}
5759
→ is-ring-hom (Liftℤ {ℓ} .snd) (R' .snd) (h' ⊙ lower)
5860
→ ∀ x → embed-coe x ≡ h' x
59-
embed-lemma p x = Int-is-initial R' .paths (∫hom _ p) ·ₚ lift x
61+
embed-lemma p x = sym $ Int-is-initial .¡-unique (∫hom _ p) ·ₚ lift x
6062

6163
data Poly : Nat → Type ℓ
6264
data Normal : Nat → Type ℓ

‎src/Cat/Abelian/Base.lagda.md‎

Lines changed: 18 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ open import Cat.Diagram.Coequaliser
1010
open import Cat.Diagram.Biproduct
1111
open import Cat.Diagram.Coproduct
1212
open import Cat.Diagram.Terminal
13+
open import Cat.Diagram.Initial
1314
open import Cat.Diagram.Product
1415
open import Cat.Displayed.Total
1516
open import Cat.Instances.Slice
@@ -151,17 +152,21 @@ module _ {o ℓ} {C : Precategory o ℓ} (A : Ab-category C) where
151152
private module A = Ab-category A
152153
153154
id-zero→zero : ∀ {X} → A.id {X} ≡ A.0m → is-zero C X
154-
id-zero→zero idm .is-zero.has-is-initial B = contr A.0m λ h → sym $
155-
h ≡⟨ A.intror refl ⟩
156-
h A.∘ A.id ≡⟨ A.refl⟩∘⟨ idm ⟩
157-
h A.∘ A.0m ≡⟨ A.∘-zero-r ⟩
158-
A.0m ∎
159-
id-zero→zero idm .is-zero.has-is-terminal .is-terminal.! = A.0m
160-
id-zero→zero idm .is-zero.has-is-terminal .is-terminal.!-unique = λ h →
161-
h ≡⟨ A.introl refl ⟩
162-
A.id A.∘ h ≡⟨ idm A.⟩∘⟨refl ⟩
163-
A.0m A.∘ h ≡⟨ A.∘-zero-l ⟩
164-
A.0m ∎
155+
{-# INLINE id-zero→zero #-}
156+
id-zero→zero idm = to-is-zero $ record
157+
{ ! = A.0m
158+
; ¡ = A.0m
159+
; !-unique = λ h →
160+
h ≡⟨ A.introl refl ⟩
161+
A.id A.∘ h ≡⟨ idm A.⟩∘⟨refl ⟩
162+
A.0m A.∘ h ≡⟨ A.∘-zero-l ⟩
163+
A.0m ∎
164+
; ¡-unique = λ h →
165+
h ≡⟨ A.intror refl ⟩
166+
h A.∘ A.id ≡⟨ A.refl⟩∘⟨ idm ⟩
167+
h A.∘ A.0m ≡⟨ A.∘-zero-r ⟩
168+
A.0m ∎
169+
}
165170
```
166171
167172
Perhaps the simplest example of an $\Ab$-category is.. any ring! In the
@@ -204,7 +209,7 @@ record is-additive {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ lsuc ℓ) where
204209
module ∅ = Zero ∅
205210
206211
0m-unique : ∀ {A B} → ∅.zero→ {A} {B} ≡ 0m
207-
0m-unique = ap₂ _∘_ (∅.has⊥ _ .paths _) refl ∙ ∘-zero-l
212+
0m-unique = ap₂ _∘_ (∅.¡-unique _) refl ∙ ∘-zero-l
208213
```
209214
210215
Coincidence of finite products and finite coproducts leads to an object
@@ -412,7 +417,7 @@ monomorphism].
412417
path : f ∘ kernel f .Kernel.kernel ≡ f ∘ 0m
413418
path = Ker.equal f
414419
∙∙ ∅.zero-∘r _
415-
∙∙ ap₂ _∘_ (∅.has⊥ _ .paths 0m) refl
420+
∙∙ ap₂ _∘_ (sym $ ∅.¡-unique 0m) refl
416421
∙∙ ∘-zero-l ∙∙ sym ∘-zero-r
417422
```
418423
-->

0 commit comments

Comments
 (0)