diff options
Diffstat (limited to 'Category/Instance/One')
| -rw-r--r-- | Category/Instance/One/Properties.agda | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/Category/Instance/One/Properties.agda b/Category/Instance/One/Properties.agda index 1452669..c6261bb 100644 --- a/Category/Instance/One/Properties.agda +++ b/Category/Instance/One/Properties.agda @@ -8,7 +8,7 @@ open import Categories.Category.Core using (Category) open import Categories.Category.Instance.One using () renaming (One to One′) One : Category o ℓ e -One = One′ +One = One′ {o} {ℓ} {e} open import Categories.Category.Cocartesian One using (Cocartesian) open import Categories.Category.Cocomplete.Finitely One using (FinitelyCocomplete) @@ -16,20 +16,20 @@ open import Categories.Object.Initial One using (Initial) open import Categories.Category.Cocartesian One using (BinaryCoproducts) -One-Initial : Initial -One-Initial = _ +initial : Initial +initial = _ -One-BinaryCoproducts : BinaryCoproducts -One-BinaryCoproducts = _ +coproducts : BinaryCoproducts +coproducts = _ -One-Cocartesian : Cocartesian -One-Cocartesian = record - { initial = One-Initial - ; coproducts = One-BinaryCoproducts +cocartesian : Cocartesian +cocartesian = record + { initial = initial + ; coproducts = coproducts } -One-FinitelyCocomplete : FinitelyCocomplete -One-FinitelyCocomplete = record - { cocartesian = One-Cocartesian +finitelyCocomplete : FinitelyCocomplete +finitelyCocomplete = record + { cocartesian = cocartesian ; coequalizer = _ } |