diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-10 17:21:14 -0700 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-10 17:21:14 -0700 |
| commit | a408cbee9abbe2dbeee09bd36afc678efe7b6557 (patch) | |
| tree | 22d6f05d6ce81357629fa2864305b81d68eed52e /Data/Matrix/SemiadditiveDagger.agda | |
| parent | 7875edd03cce586a8c9f0b95dedffb390bfdbd61 (diff) | |
Use latest agda-categories
Diffstat (limited to 'Data/Matrix/SemiadditiveDagger.agda')
| -rw-r--r-- | Data/Matrix/SemiadditiveDagger.agda | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda index ebc6592..1415c7e 100644 --- a/Data/Matrix/SemiadditiveDagger.agda +++ b/Data/Matrix/SemiadditiveDagger.agda @@ -286,15 +286,15 @@ coproduct {A} {B} = record opaque unfolding _≋_ - !-unique : (E : Matrix 0 B) → []ᵥ ≋ E - !-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E)) + ¡-unique : (E : Matrix 0 B) → []ᵥ ≋ E + ¡-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E)) initial : Initial Mat initial = record { ⊥ = 0 ; ⊥-is-initial = record - { ! = []ᵥ - ; !-unique = !-unique + { ¡ = []ᵥ + ; ¡-unique = ¡-unique } } |