agda/examples/outdated-and-incorrect/cat/Iso.agda

open import Category

module Iso (ℂ : Cat) where

private open module C = Cat (η-Cat ℂ)

data _≅_ (A B : Obj) : Set where
  iso : (i : A ─→ B)(j : B ─→ A) ->
        i ∘ j == id -> j ∘ i == id ->
        A ≅ B