agda / agda-categories

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

Add `IsNI` to be consistent with `IsIso` in for morphisms #359

Closed 91khr closed 1 year ago

91khr commented 1 year ago

Sometimes we may say that a natural transformation is a natural isomorphism, so it may be better to add a helper to express this.

This is my first time trying to contribute to an Agda project, please excuse if there's anything missing.