Skip to main content

Iso

structure Iso[O, M] {
    cat: Category[O, M]
    hom: M
    inv: M
} constraint {
    is_iso_pair(cat, hom, inv)
}

An isomorphism in a category, with explicit inverse data.

GitHub

cat​

Iso.cat: Iso[O, M] -> Category[O, M]

The ambient category.

hom​

Iso.hom: Iso[O, M] -> M

The forward morphism.

inv​

Iso.inv: Iso[O, M] -> M

The inverse morphism.