j
k
j a
j l
Conor McBride wrote:
...instance Category (:=:) where id = Refl Refl . Refl = Refl That and the identity-on-objects functor to sets and functions.
instance Category (:=:) where id = Refl Refl . Refl = Refl
That and the identity-on-objects functor to sets and functions.
Not sure what you mean by this, Conor. Can you please express this in Haskell code? Thanks, Martijn.
Back to the thread
Back to the list