diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-12-09 13:26:36 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-12-09 13:26:36 -0600 |
| commit | b5e583bb067749f80bd3f7e24e807674eba8b394 (patch) | |
| tree | 493fe472eef9460d7aad91b945326c6189a4f977 /Nat | |
| parent | 6272b4e84650b9833a53239b354770e0deba7b9a (diff) | |
Update Nat properties
Diffstat (limited to 'Nat')
| -rw-r--r-- | Nat/Properties.agda | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Nat/Properties.agda b/Nat/Properties.agda index 6e04346..0b3da1e 100644 --- a/Nat/Properties.agda +++ b/Nat/Properties.agda @@ -19,16 +19,15 @@ open import Categories.Object.Coproduct Nat using (Coproduct; IsCoproduct; IsCop open import Coeq Nat using (coequalizer-on-coproduct) open import FinMerge using (glue-iter; glue-unglue-once) open import FinMerge.Properties using (lemma₂; merge-unmerge; unmerge-merge) -open import Util using (compare; less; equal; greater; _<_<_) +open import FinMerge.Util using (compare; less; equal; greater) open Category Nat - makeZeroCoequalizer : {B : ℕ} {f g : 0 ⇒ B} → Coequalizer f g makeZeroCoequalizer = record { arr = id ; isCoequalizer = record - { equality = λ() + { equality = λ () ; coequalize = λ {_} {h} _ → h ; universal = λ _ → refl ; unique = λ h≈i∘id → Equiv.sym h≈i∘id |