I have a data structure
record IdentityPreservingMorphism domain codomain where
constructor MkMorphismOfMonoids
func : domain -> codomain
funcRespId : (Monoid domain, Monoid codomain) => func (Algebra.neutral) = Algebra.neutral
which just says that an IdentityPreservingMorphism
is a morphism between monoids which needs to respect the identity.
I'm trying to prove that the identity morphisms is an IdentityPreservingMorphism
monoidIdentity : Monoid m => MorphismOfMonoids m m
monoidIdentity = MkMorphismOfMonoids
id
?respId
The easy shot for ?respId
at Refl
does not work because there are too many Monoid
instances available. How can I tell the compiler that I would like to use only the instance coming from the monoidIdentity
definition?