search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

Update Kleisli.agda #324

Closed tetrapharmakon closed 2 years ago

tetrapharmakon commented 2 years ago

A morphism f : A => F B in the Kleisli category of a monad M on C is an isomorphism if and only if its Kleisli extension f* : F A => F B is an isomorphism in C

JacquesCarette commented 2 years ago

Did you see the 2 comments that I left on this PR?