Require Import Theory.Category.

Generalizable All Variables.

Class IsInverse {𝒞 : Category} {A B : 𝒞} (f : A ⇒ B) (g : B ⇒ A) : Prop ≔ mkInverse

{ iso_left

: f ∘ g ≈ id

; iso_right : g ∘ f ≈ id }.

Arguments mkInverse {_ _ _ _ _} _ _.

Definition inverse_of {𝒞 : Category} {A B : 𝒞} {g : B ⇒ A} (f : A ⇒ B) `{!IsInverse f g} : B ⇒ A ≔ g.

Arguments inverse_of {_ _ _ _} _ {_}.

Notation "f ⁻¹" ≔ (inverse_of f) (at level 0, no associativity).

Structure Iso {𝒞 : Category} (A B : 𝒞) ≔ mkIso

{ iso_from	:> A ⇒ B
; iso_to	: B ⇒ A

; iso_inverse : IsInverse iso_from iso_to }.

Existing Instance iso_inverse.

Arguments mkIso

{_ _ _ _} _ _.

Arguments iso_from {_ _ _} _.

Arguments iso_to

{_ _ _} _.

Infix "≅" ≔ Iso (at level 70).
Notation "I '⋅≅-left'"≔ (iso_left I) (at level 0, only parsing).
Notation "I '⋅≅-right'"≔ (iso_left I) (at level 0, only parsing).

Notation "'Iso.make' ⦃ 'from' ≔ from ; 'to' ≔ to ⦄" ≔
  (@mkIso _ _ _ from to (mkInverse _ _)) (only parsing).

Section Iso_Equivalence.

  Context {𝒞 : Category}.

  Program Definition refl {A : 𝒞} : A ≅ A ≔
    Iso.make ⦃ from ≔ id

; to

≔ id ⦄.

  Show proof.
  Show proof.

  Program Definition sym {A B : 𝒞} (iso_AB : A ≅ B) : B ≅ A ≔
    Iso.make ⦃ from ≔ iso_AB⁻¹

; to	≔ iso_AB ⦄.

  Show proof.
  Show proof.

  Program Definition trans {A B C : 𝒞} (iso_AB : A ≅ B) (iso_BC : B ≅ C) : A ≅ C ≔
    Iso.make ⦃ from ≔ iso_BC ∘ iso_AB

; to	≔ iso_AB ⁻¹ ∘ iso_BC ⁻¹ ⦄.

  Show proof.
  Show proof.

End Iso_Equivalence.

Notation "≅-refl" ≔ refl (only parsing).
Notation "≅-sym" ≔ sym (only parsing).
Notation "≅-trans" ≔ trans (only parsing).