Follow

@mavaxavou@mathstodon.xyz Idris or Idris2?

Here's some Idris2 code that seems to do what you're asking for: I can manually specify the implicit parameters for compose:

record Cat where
constructor MkCat
object : Type
morphism : object -> object -> Type
compose : {a, b, c : object} -> morphism a b -> morphism b c -> morphism a c

composeEndomorphism : (c : Cat) -> (o : c.object) -> c.morphism o o -> c.morphism o o -> c.morphism o o
composeEndomorphism c o f g = c.compose {a = o} {b = o} {c = o} f g

· · Web · 1 · 0 · 0
Sign in to participate in the conversation
Mastodon @ SDF

"I appreciate SDF but it's a general-purpose server and the name doesn't make it obvious that it's about art." - Eugen Rochko