diff options
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 } } |