-- Isomorphisms in a small category
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Category.Isomorphism
import Core

-- g is a two-sided inverse of f.
predicate InversePair (C f g : Set) :=
  f ∈ mor(C) ∧ g ∈ mor(C) ∧ dom(C)(g) = cod(C)(f) ∧ cod(C)(g) = dom(C)(f) ∧
  comp(C)(g, f) = id(C)(dom(C)(f)) ∧ comp(C)(f, g) = id(C)(cod(C)(f))

notation infixr 70 "∘" => call2(C.comp, _, _) via hypothesis InversePair(C, f, g) for C.mor

predicate Isomorphism (C f : Set) :=
  ∃ g, InversePair(C, f, g)

predicate Isomorphic (C a b : Set) :=
  ∃ f ∈ hom(C, a, b), Isomorphism(C, f)

theorem InversePair.morphism (C f g : Set)
  requires pair : InversePair(C, f, g)
  shows f ∈ mor(C)
proof
  simp [InversePair]

theorem InversePair.inverse_morphism (C f g : Set)
  requires pair : InversePair(C, f, g)
  shows g ∈ mor(C)
proof
  simp [InversePair]

theorem InversePair.dom (C f g : Set)
  requires pair : InversePair(C, f, g)
  shows dom(C)(g) = cod(C)(f)
proof
  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair
  exact domG

theorem InversePair.cod (C f g : Set)
  requires pair : InversePair(C, f, g)
  shows cod(C)(g) = dom(C)(f)
proof
  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair
  exact codG

theorem InversePair.left (C f g : Set)
  requires pair : InversePair(C, f, g)
  shows g ∘ f = id(C)(dom(C)(f))
proof
  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair
  exact leftLaw

theorem InversePair.right (C f g : Set)
  requires pair : InversePair(C, f, g)
  shows f ∘ g = id(C)(cod(C)(f))
proof
  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair
  exact rightLaw

theorem InversePair.symmetric (C f g : Set)
  requires pair : InversePair(C, f, g)
  shows InversePair(C, g, f)
proof
  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair
  unfold InversePair
  refine ⟨gInM, fInM, ?_, ?_, ?_, ?_⟩
  . cc
  . cc
  . cc
  . cc

section InverseLaws
variable (C : Set)
hypothesis category : Category(C)

theorem InversePair.hom (f g : Set)
  requires pair : InversePair(C, f, g)
  shows f : dom(C)(f) ⟶ cod(C)(f)
proof
  have fInM := InversePair.morphism with pair
  exact Morphism.of_morphism with category, fInM

theorem InversePair.inverse_hom (f g : Set)
  requires pair : InversePair(C, f, g)
  shows g : cod(C)(f) ⟶ dom(C)(f)
proof
  obtain ⟨fInM, gInM, domG, codG, gf, fg⟩ := pair
  unfold Morphism
  refine ⟨gInM, domG, codG⟩

theorem InversePair.inverse_of_hom (a b : Set) (f : a ⟶ b) (g : Set)
  requires pair : InversePair(C, f, g)
  shows g : b ⟶ a
proof
  have gHom : g : cod(C)(f) ⟶ dom(C)(f) := InversePair.inverse_hom with category, pair
  have domF : dom(C)(f) = a by cc
  have codF : cod(C)(f) = b by cc
  rw [domF, codF] at gHom
  exact gHom

theorem InversePair.left_hom (a b : Set) (f : a ⟶ b) (g : Set)
  requires pair : InversePair(C, f, g)
  shows g ∘ f = id(C)(a)
proof
  have law : g ∘ f = id(C)(dom(C)(f)) := InversePair.left with pair
  have domF : dom(C)(f) = a by cc
  rwa domF at law

theorem InversePair.right_hom (a b : Set) (f : a ⟶ b) (g : Set)
  requires pair : InversePair(C, f, g)
  shows f ∘ g = id(C)(b)
proof
  have law : f ∘ g = id(C)(cod(C)(f)) := InversePair.right with pair
  have codF : cod(C)(f) = b by cc
  rwa codF at law

-- Inverses are unique: a left inverse equals a right inverse.
theorem InversePair.unique (a b : Set) (f : a ⟶ b) (g k : b ⟶ a)
  requires gf : g ∘ f = id(C)(a)
  requires fk : f ∘ k = id(C)(b)
  shows g = k
proof
  calc
    g = g ∘ id(C)(b) := by simp [Category.id_right]
    _ = g ∘ (f ∘ k) := by rw fk
    _ = (g ∘ f) ∘ k := by rw Category.assoc
    _ = id(C)(a) ∘ k := by rw gf
    _ = k := by simp [Category.id_left]

theorem InversePair.eq_of_pairs (f g k : Set)
  requires first : InversePair(C, f, g)
  requires second : InversePair(C, f, k)
  shows g = k
proof
  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := InversePair.hom with category, first
  have gHom : g : cod(C)(f) ⟶ dom(C)(f) := InversePair.inverse_hom with category, first
  have kHom : k : cod(C)(f) ⟶ dom(C)(f) := InversePair.inverse_hom with category, second
  have gf : g ∘ f = id(C)(dom(C)(f)) := InversePair.left with first
  have fk : f ∘ k = id(C)(cod(C)(f)) := InversePair.right with second
  exact InversePair.unique with category, fHom, gHom, kHom, gf, fk

end InverseLaws

theorem InversePair.in_hom (C a b f g : Set)
  requires pair : InversePair(C, f, g)
  requires fHom : f ∈ hom(C, a, b)
  shows g ∈ hom(C, b, a)
proof
  obtain ⟨fInM, gInM, domG, codG, gf, fg⟩ := pair
  obtain ⟨fInM2, domF, codF⟩ := hom.membership.forward with fHom
  apply hom.membership.backward
  refine ⟨gInM, ?_, ?_⟩
  . cc
  . cc

theorem InversePair.id (C a : Set)
  requires category : Category(C)
  requires aInO : a ∈ obj(C)
  shows InversePair(C, id(C)(a), id(C)(a))
proof
  have idInM := Category.id_closed with category, aInO
  have domId := Category.id_dom with category, aInO
  have codId := Category.id_cod with category, aInO
  have idId := Category.id_id with category, aInO
  unfold InversePair
  refine ⟨idInM, idInM, ?_, ?_, ?_, ?_⟩
  . cc
  . cc
  . cc
  . cc

section InverseComposition
variable (C : Set)
hypothesis category : Category(C)

-- The inverse of a composite is the composite of the inverses, reversed.
theorem InversePair.comp (a b c : Set) (f : a ⟶ b) (g : b ⟶ c) (k l : Set)
  requires gPair : InversePair(C, g, k)
  requires fPair : InversePair(C, f, l)
  shows InversePair(C, g ∘ f, l ∘ k)
proof
  have kHom : k : c ⟶ b := InversePair.inverse_of_hom with category, gPair
  have lHom : l : b ⟶ a := InversePair.inverse_of_hom with category, fPair
  have gfHom : g ∘ f : a ⟶ c by synthesize
  have lkHom : l ∘ k : c ⟶ a by synthesize
  have kg : k ∘ g = id(C)(b) := InversePair.left_hom with category, gPair
  have gk : g ∘ k = id(C)(c) := InversePair.right_hom with category, gPair
  have lf : l ∘ f = id(C)(a) := InversePair.left_hom with category, fPair
  have fl : f ∘ l = id(C)(b) := InversePair.right_hom with category, fPair
  have leftLaw : (l ∘ k) ∘ (g ∘ f) = id(C)(a)
    calc
      (l ∘ k) ∘ (g ∘ f) = l ∘ (k ∘ (g ∘ f)) := by rw Category.assoc
      _ = l ∘ ((k ∘ g) ∘ f) := by rw Category.assoc
      _ = l ∘ (id(C)(b) ∘ f) := by rw kg
      _ = l ∘ f := by rw Category.id_left
      _ = id(C)(a) := lf
  have rightLaw : (g ∘ f) ∘ (l ∘ k) = id(C)(c)
    calc
      (g ∘ f) ∘ (l ∘ k) = g ∘ (f ∘ (l ∘ k)) := by rw Category.assoc
      _ = g ∘ ((f ∘ l) ∘ k) := by rw Category.assoc
      _ = g ∘ (id(C)(b) ∘ k) := by rw fl
      _ = g ∘ k := by rw Category.id_left
      _ = id(C)(c) := gk
  unfold InversePair
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
  . assumption
  . assumption
  . cc
  . cc
  . cc
  . cc

end InverseComposition

theorem Isomorphism.morphism (C f : Set)
  requires iso : Isomorphism(C, f)
  shows f ∈ mor(C)
proof
  obtain ⟨g, pair⟩ := iso
  exact InversePair.morphism with pair

theorem Isomorphism.of_pair (C f g : Set)
  requires pair : InversePair(C, f, g)
  shows Isomorphism(C, f)
proof
  refine ⟨g, pair⟩

theorem Isomorphism.inverse (C f g : Set)
  requires pair : InversePair(C, f, g)
  shows Isomorphism(C, g)
proof
  have symmetric := InversePair.symmetric with pair
  exact Isomorphism.of_pair with symmetric

theorem Isomorphism.id (C a : Set)
  requires category : Category(C)
  requires aInO : a ∈ obj(C)
  shows Isomorphism(C, id(C)(a))
proof
  have pair := InversePair.id with category, aInO
  exact Isomorphism.of_pair with pair

theorem Isomorphism.comp (C g f : Set)
  requires category : Category(C)
  requires gIso : Isomorphism(C, g)
  requires fIso : Isomorphism(C, f)
  requires composable : dom(C)(g) = cod(C)(f)
  shows Isomorphism(C, g ∘ f)
proof
  obtain ⟨k, gPair⟩ := gIso
  obtain ⟨l, fPair⟩ := fIso
  have gInM := InversePair.morphism with gPair
  have fInM := InversePair.morphism with fPair
  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *
  have gHom : g : cod(C)(f) ⟶ cod(C)(g) := Morphism.of_composable with *
  have pair := InversePair.comp with category, fHom, gHom, gPair, fPair
  exact Isomorphism.of_pair with pair

-- Cancellation against an isomorphism.
theorem InversePair.cancel_left (C f g u v : Set)
  requires category : Category(C)
  requires pair : InversePair(C, f, g)
  requires uInM : u ∈ mor(C)
  requires vInM : v ∈ mor(C)
  requires uComposable : dom(C)(f) = cod(C)(u)
  requires vComposable : dom(C)(f) = cod(C)(v)
  requires same : f ∘ u = f ∘ v
  shows u = v
proof
  obtain ⟨fInM, gInM, domG, codG, gf, fg⟩ := pair
  have unitU : id(C)(dom(C)(f)) ∘ u = u
    have law := Category.left_unit with category, uInM
    rwa ← uComposable at law
  have unitV : id(C)(dom(C)(f)) ∘ v = v
    have law := Category.left_unit with category, vInM
    rwa ← vComposable at law
  have assocU := Category.associative with
    category, gInM, fInM, uInM, domG, uComposable
  have assocV := Category.associative with
    category, gInM, fInM, vInM, domG, vComposable
  calc
    u = id(C)(dom(C)(f)) ∘ u := by rw unitU
    _ = (g ∘ f) ∘ u := by rw gf
    _ = g ∘ (f ∘ u) := assocU
    _ = g ∘ (f ∘ v) := by rw same
    _ = (g ∘ f) ∘ v := by rw assocV
    _ = id(C)(dom(C)(f)) ∘ v := by rw gf
    _ = v := unitV

theorem InversePair.cancel_right (C f g u v : Set)
  requires category : Category(C)
  requires pair : InversePair(C, f, g)
  requires uInM : u ∈ mor(C)
  requires vInM : v ∈ mor(C)
  requires uComposable : dom(C)(u) = cod(C)(f)
  requires vComposable : dom(C)(v) = cod(C)(f)
  requires same : u ∘ f = v ∘ f
  shows u = v
proof
  obtain ⟨fInM, gInM, domG, codG, gf, fg⟩ := pair
  have unitU := Category.id_right_of_dom with category, uInM, uComposable
  have unitV := Category.id_right_of_dom with category, vInM, vComposable
  have fgComposable : dom(C)(f) = cod(C)(g) by cc
  have assocU := Category.associative with
    category, uInM, fInM, gInM, uComposable, fgComposable
  have assocV := Category.associative with
    category, vInM, fInM, gInM, vComposable, fgComposable
  calc
    u = u ∘ id(C)(cod(C)(f)) := by rw unitU
    _ = u ∘ (f ∘ g) := by rw fg
    _ = (u ∘ f) ∘ g := by rw assocU
    _ = (v ∘ f) ∘ g := by rw same
    _ = v ∘ (f ∘ g) := assocV
    _ = v ∘ id(C)(cod(C)(f)) := by rw fg
    _ = v := unitV

-- A morphism that is inverted on both sides by the same morphism of each
-- side is an isomorphism; in particular a left and a right inverse agree.
theorem InversePair.of_left_right (C f g k : Set)
  requires category : Category(C)
  requires fInM : f ∈ mor(C)
  requires gInM : g ∈ mor(C)
  requires kInM : k ∈ mor(C)
  requires domG : dom(C)(g) = cod(C)(f)
  requires codK : cod(C)(k) = dom(C)(f)
  requires left : g ∘ f = id(C)(dom(C)(f))
  requires right : f ∘ k = id(C)(cod(C)(f))
  shows g = k ∧ InversePair(C, f, k)
proof
  have unitG := Category.id_right_of_dom with category, gInM, domG
  have unitK := Category.id_left_of_cod with category, kInM, codK
  have fkComposable : dom(C)(f) = cod(C)(k) by cc
  have assoc := Category.associative with
    category, gInM, fInM, kInM, domG, fkComposable
  have equal : g = k
    calc
      g = g ∘ id(C)(cod(C)(f)) := by rw unitG
      _ = g ∘ (f ∘ k) := by rw right
      _ = (g ∘ f) ∘ k := by rw assoc
      _ = id(C)(dom(C)(f)) ∘ k := by rw left
      _ = k := unitK
  constructor
  . exact equal
  . unfold InversePair
    refine ⟨fInM, kInM, ?_, codK, ?_, right⟩
    . cc
    . rw ← equal
      exact left

theorem Isomorphic.of_hom (C a b f : Set)
  requires fHom : f ∈ hom(C, a, b)
  requires iso : Isomorphism(C, f)
  shows Isomorphic(C, a, b)
proof
  refine ⟨f, fHom, iso⟩

theorem Isomorphic.reflexive (C a : Set)
  requires category : Category(C)
  requires aInO : a ∈ obj(C)
  shows Isomorphic(C, a, a)
proof
  have idHom := hom.id with category, aInO
  have iso := Isomorphism.id with category, aInO
  exact Isomorphic.of_hom with idHom, iso

theorem Isomorphic.symmetric (C a b : Set)
  requires h : Isomorphic(C, a, b)
  shows Isomorphic(C, b, a)
proof
  obtain ⟨f, fHom, g, pair⟩ := h
  have gHom := InversePair.in_hom with pair, fHom
  have gIso := Isomorphism.inverse with pair
  exact Isomorphic.of_hom with gHom, gIso

theorem Isomorphic.transitive (C a b c : Set)
  requires category : Category(C)
  requires first : Isomorphic(C, a, b)
  requires second : Isomorphic(C, b, c)
  shows Isomorphic(C, a, c)
proof
  obtain ⟨f, fHom, fIso⟩ := first
  obtain ⟨g, gHom, gIso⟩ := second
  have composable := hom.composable with gHom, fHom
  have compHom := hom.comp with category, gHom, fHom
  have compIso := Isomorphism.comp with category, gIso, fIso, composable
  exact Isomorphic.of_hom with compHom, compIso

-- Inverses transpose a commutative square: if e2 ∘ u = v ∘ e1 for
-- isomorphisms e1 : a → b and e2 : c → d with inverses k1 and k2, then
-- k2 ∘ v = u ∘ k1.
theorem InversePair.transpose (C a b c d e1 k1 e2 k2 u v : Set)
  requires category : Category(C)
  requires firstPair : InversePair(C, e1, k1)
  requires secondPair : InversePair(C, e2, k2)
  requires e1Hom : e1 ∈ hom(C, a, b)
  requires e2Hom : e2 ∈ hom(C, c, d)
  requires uHom : u ∈ hom(C, a, c)
  requires vHom : v ∈ hom(C, b, d)
  requires square : e2 ∘ u = v ∘ e1
  shows k2 ∘ v = u ∘ k1
proof
  have k1Hom := InversePair.in_hom with firstPair, e1Hom
  have k2Hom := InversePair.in_hom with secondPair, e2Hom
  have e1k1 : e1 ∘ k1 = id(C)(b)
    have law := InversePair.right with firstPair
    have codE := hom.cod with e1Hom
    rwa codE at law
  have k2e2 : k2 ∘ e2 = id(C)(c)
    have law := InversePair.left with secondPair
    have domE := hom.dom with e2Hom
    rwa domE at law
  have uk1Hom := hom.comp with category, uHom, k1Hom
  have unitV := Category.id_right_hom with category, vHom
  have unitUK := Category.id_left_hom with category, uk1Hom
  have assocOne := Category.assoc_hom with category, vHom, e1Hom, k1Hom
  have assocTwo := Category.assoc_hom with category, e2Hom, uHom, k1Hom
  have assocThree := Category.assoc_hom with category, k2Hom, e2Hom, uk1Hom
  calc
    k2 ∘ v = k2 ∘ (v ∘ id(C)(b)) := by rw unitV
    _ = k2 ∘ (v ∘ (e1 ∘ k1)) := by rw e1k1
    _ = k2 ∘ ((v ∘ e1) ∘ k1) := by rw assocOne
    _ = k2 ∘ ((e2 ∘ u) ∘ k1) := by rw square
    _ = k2 ∘ (e2 ∘ (u ∘ k1)) := by rw assocTwo
    _ = (k2 ∘ e2) ∘ (u ∘ k1) := by rw assocThree
    _ = id(C)(c) ∘ (u ∘ k1) := by rw k2e2
    _ = u ∘ k1 := unitUK

-- Isomorphism as a relation on the objects.
def isomorphismRelation (C : Set) : Set :=
  { p ∈ obj(C) × obj(C) | ∃ a ∈ obj(C), ∃ b ∈ obj(C), p = (a, b) ∧
    Isomorphic(C, a, b) }

theorem isomorphismRelation.relates (C a b : Set)
  requires aInO : a ∈ obj(C)
  requires bInO : b ∈ obj(C)
  requires iso : Isomorphic(C, a, b)
  shows relates(isomorphismRelation(C), a, b)
proof
  unfold relates
  apply isomorphismRelation.membership.backward
  constructor
  . exact product.pair with aInO, bInO
  . refine ⟨a, aInO, b, bInO, rfl, iso⟩

theorem isomorphismRelation.reflects (C a b : Set)
  requires related : relates(isomorphismRelation(C),
    a, b)
  shows Isomorphic(C, a, b)
proof
  unfold relates at related
  obtain ⟨bounded, c, cInO, d, dInO, shape, iso⟩ :=
    isomorphismRelation.membership.forward with related
  obtain ⟨aEqual, bEqual⟩ := orderedPair.injective with shape
  rw [aEqual, bEqual]
  exact iso

theorem isomorphismRelation.relation (C : Set)
  shows RelationOn(isomorphismRelation(C), obj(C))
proof
  unfold RelationOn
  unfold RelationBetween
  intros p member
  obtain ⟨bounded, rest⟩ := isomorphismRelation.membership.forward with member
  exact bounded

theorem isomorphismRelation.equivalence (C : Set)
  requires category : Category(C)
  shows Equivalence(obj(C), isomorphismRelation(C))
proof
  have relation := isomorphismRelation.relation at C
  unfold Equivalence
  refine ⟨relation, ?_, ?_, ?_⟩
  . intros a aInO
    have iso := Isomorphic.reflexive with category, aInO
    exact isomorphismRelation.relates with aInO, aInO, iso
  . intros a aInO b bInO related
    have iso := isomorphismRelation.reflects with related
    have back := Isomorphic.symmetric with iso
    exact isomorphismRelation.relates with bInO, aInO, back
  . intros a aInO b bInO c cInO first second
    have firstIso := isomorphismRelation.reflects with first
    have secondIso := isomorphismRelation.reflects with second
    have iso := Isomorphic.transitive with category, firstIso, secondIso
    exact isomorphismRelation.relates with aInO, cInO, iso

-- The isomorphism class of an object.
def isomorphismClass (C a : Set) : Set :=
  { b ∈ obj(C) | Isomorphic(C, a, b) }

theorem isomorphismClass.subset (C a : Set)
  shows isomorphismClass(C, a) ⊆ obj(C)
proof
  intros b member
  obtain ⟨bInO, iso⟩ := isomorphismClass.membership.forward with member
  exact bInO

theorem isomorphismClass.self (C a : Set)
  requires category : Category(C)
  requires aInO : a ∈ obj(C)
  shows a ∈ isomorphismClass(C, a)
proof
  have iso := Isomorphic.reflexive with category, aInO
  apply isomorphismClass.membership.backward
  refine ⟨aInO, iso⟩

theorem isomorphismClass.symmetric (C a b : Set)
  requires aInO : a ∈ obj(C)
  requires member : b ∈ isomorphismClass(C, a)
  shows a ∈ isomorphismClass(C, b)
proof
  obtain ⟨bInO, iso⟩ := isomorphismClass.membership.forward with member
  have back := Isomorphic.symmetric with iso
  apply isomorphismClass.membership.backward
  refine ⟨aInO, back⟩

theorem isomorphismClass.subset_of_isomorphic (C a b : Set)
  requires category : Category(C)
  requires iso : Isomorphic(C, a, b)
  shows isomorphismClass(C, b) ⊆
    isomorphismClass(C, a)
proof
  intros c member
  obtain ⟨cInO, second⟩ := isomorphismClass.membership.forward with member
  have chain := Isomorphic.transitive with category, iso, second
  apply isomorphismClass.membership.backward
  refine ⟨cInO, chain⟩

theorem isomorphismClass.eq_of_isomorphic (C a b : Set)
  requires category : Category(C)
  requires iso : Isomorphic(C, a, b)
  shows isomorphismClass(C, a) =
    isomorphismClass(C, b)
proof
  have back := Isomorphic.symmetric with iso
  have forward := isomorphismClass.subset_of_isomorphic with category, iso
  have backward := isomorphismClass.subset_of_isomorphic with category, back
  exact Subset.antisymmetric with backward, forward

theorem isomorphismClass.eq_of_member (C a b : Set)
  requires category : Category(C)
  requires member : b ∈ isomorphismClass(C, a)
  shows isomorphismClass(C, a) =
    isomorphismClass(C, b)
proof
  obtain ⟨bInO, iso⟩ := isomorphismClass.membership.forward with member
  exact isomorphismClass.eq_of_isomorphic with category, iso

theorem isomorphismClass.disjoint_or_equal (C a b : Set)
  requires category : Category(C)
  requires aInO : a ∈ obj(C)
  requires bInO : b ∈ obj(C)
  shows Disjoint(isomorphismClass(C, a),
    isomorphismClass(C, b)) ∨
    isomorphismClass(C, a) =
    isomorphismClass(C, b)
proof
  by_contra negated
  have notDisjoint : ¬Disjoint(isomorphismClass(C, a),
      isomorphismClass(C, b))
    intro disjoint
    apply negated
    left
    exact disjoint
  have common : Nonempty(isomorphismClass(C, a) ∩
      isomorphismClass(C, b))
    apply Nonempty.of_ne_empty
    intro emptyMeet
    apply notDisjoint
    unfold Disjoint
    exact emptyMeet
  obtain ⟨c, cInMeet⟩ := common
  obtain ⟨cInA, cInB⟩ := intersection.membership.forward with cInMeet
  have aClass := isomorphismClass.eq_of_member with category, cInA
  have bClass := isomorphismClass.eq_of_member with category, cInB
  apply negated
  right
  cc

-- The inverse of an isomorphism, as the unique morphism inverting it.
defunique inverseMorphism (C f : Set) (g ∈ mor(C)) :=
  InversePair(C, f, g)
requires category : Category(C)
requires iso : Isomorphism(C, f)
proof
  obtain ⟨g, pair⟩ := iso
  have gInM := InversePair.inverse_morphism with pair
  refine ⟨g, gInM, pair⟩
uniqueness
  intros u hu first v hv second
  exact InversePair.eq_of_pairs with category, first, second

theorem inverseMorphism.pair (C f : Set)
  requires category : Category(C)
  requires iso : Isomorphism(C, f)
  shows InversePair(C, f,
    inverseMorphism(C, f))
proof
  have selected := inverseMorphism.selected at C, f with
    category, iso
  exact selected.right

theorem inverseMorphism.morphism (C f : Set)
  requires category : Category(C)
  requires iso : Isomorphism(C, f)
  shows inverseMorphism(C, f) ∈ mor(C)
proof
  have selected := inverseMorphism.selected at C, f with
    category, iso
  exact selected.left

theorem inverseMorphism.eq (C f g : Set)
  requires category : Category(C)
  requires pair : InversePair(C, f, g)
  shows inverseMorphism(C, f) = g
proof
  have iso := Isomorphism.of_pair with pair
  have canonical := inverseMorphism.pair with category, iso
  exact InversePair.eq_of_pairs with category, canonical, pair

theorem inverseMorphism.in_hom (C a b f : Set)
  requires category : Category(C)
  requires iso : Isomorphism(C, f)
  requires fHom : f ∈ hom(C, a, b)
  shows inverseMorphism(C, f) ∈ hom(C, b, a)
proof
  have pair := inverseMorphism.pair with category, iso
  exact InversePair.in_hom with pair, fHom

theorem inverseMorphism.isomorphism (C f : Set)
  requires category : Category(C)
  requires iso : Isomorphism(C, f)
  shows Isomorphism(C, inverseMorphism(C, f))
proof
  have pair := inverseMorphism.pair with category, iso
  exact Isomorphism.inverse with pair

theorem inverseMorphism.involutive (C f : Set)
  requires category : Category(C)
  requires iso : Isomorphism(C, f)
  shows inverseMorphism(C, inverseMorphism(C, f)) = f
proof
  have pair := inverseMorphism.pair with category, iso
  have symmetric := InversePair.symmetric with pair
  exact inverseMorphism.eq with category, symmetric

theorem inverseMorphism.id (C a : Set)
  requires category : Category(C)
  requires aInO : a ∈ obj(C)
  shows inverseMorphism(C, id(C)(a)) = id(C)(a)
proof
  have pair := InversePair.id with category, aInO
  exact inverseMorphism.eq with category, pair

theorem inverseMorphism.comp (C g f : Set)
  requires category : Category(C)
  requires gIso : Isomorphism(C, g)
  requires fIso : Isomorphism(C, f)
  requires composable : dom(C)(g) = cod(C)(f)
  shows inverseMorphism(C, g ∘ f) =
    inverseMorphism(C, f) ∘
      inverseMorphism(C, g)
proof
  have gPair := inverseMorphism.pair with category, gIso
  have fPair := inverseMorphism.pair with category, fIso
  have gInM := Isomorphism.morphism with gIso
  have fInM := Isomorphism.morphism with fIso
  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *
  have gHom : g : cod(C)(f) ⟶ cod(C)(g) := Morphism.of_composable with *
  have pair := InversePair.comp with category, fHom, gHom, gPair, fPair
  exact inverseMorphism.eq with category, pair

theorem inverseMorphism.left (C f : Set)
  requires category : Category(C)
  requires iso : Isomorphism(C, f)
  shows inverseMorphism(C, f) ∘ f = id(C)(dom(C)(f))
proof
  have pair := inverseMorphism.pair with category, iso
  exact InversePair.left with pair

theorem inverseMorphism.right (C f : Set)
  requires category : Category(C)
  requires iso : Isomorphism(C, f)
  shows f ∘ inverseMorphism(C, f) = id(C)(cod(C)(f))
proof
  have pair := inverseMorphism.pair with category, iso
  exact InversePair.right with pair