diff options
Diffstat (limited to 'Data/Matrix/BaseChange.agda')
| -rw-r--r-- | Data/Matrix/BaseChange.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Data/Matrix/BaseChange.agda b/Data/Matrix/BaseChange.agda index 2135c13..04b9f9c 100644 --- a/Data/Matrix/BaseChange.agda +++ b/Data/Matrix/BaseChange.agda @@ -95,7 +95,7 @@ resp = cong (Mat.₁ func) ⟨ε⟩-homo {A} = MonoidHomomorphism.ε-homo (MonEndo.mapₘ A (mk-⇒ +-monoidHomomorphism)) opaque - unfolding I _ᵀ _∷ₕ_ Endo.mapₛ + unfolding I _∷ₕ_ Endo.mapₛ ident : {A : ℕ} → change (I R) MatS.≋ I S {A} ident {zero} = PW.[] ident {suc A} = (1#-homo PW.∷ ⟨ε⟩-homo) PW.∷ map-⟨ε⟩∷ₕI |