# Library Isomorphism

Require Import Setoid Utf8 Ensembles ProofIrrelevance.
Require Export Notations Morphism.

Set Implicit Arguments.

# Isomorphism

Record is_isomorphism X Y (f : XY) :=
{
isomorphism_inverse : YX;
isomorphism_right_inverse
: x, (f isomorphism_inverse) x = (λ x, x) x;
isomorphism_left_inverse
: x, (isomorphism_inverse f) x = (λ x, x) x
}.

Notation "i -1" := i) (at level 10).

Record isomorphic X Y :=
{
isomorphic_morphism :> XY;
isomorphic_is_isomorphism :> is_isomorphism isomorphic_morphism
}.

Hint Resolve isomorphic_is_isomorphism.

Infix "≅" := (isomorphic) (at level 70) : type_scope.

Lemma isomorphic_eq X Y (f g : X Y) :
isomorphic_morphism f = isomorphic_morphism g
→ isomorphism_inverse f = isomorphism_inverse g
→ f = g.
Proof.
destruct f as [ ? [ ] ], g as [ ? [ ] ]; simpl;
repeat intro; subst; repeat f_equal;
apply ProofIrrelevance.proof_irrelevance.
Qed.

Notation relation A := (AAType).

Definition Reflexive {A} (R : relation A) := x, R x x.
Definition Symmetric {A} (R : relation A) := x y, R x yR y x.
Definition Transitive {A} (R : relation A) := x y z, R x yR y zR x z.

Record Equivalence {A : Type} (R : relation A)
:= Build_Equivalence
{ Equivalence_Reflexive : Reflexive R;
Equivalence_Symmetric : Symmetric R;
Equivalence_Transitive : Transitive R }.

Section isomorphic_relation.
Local Ltac t :=
intros; simpl;
repeat match goal with
| [ H : _ _ |- _ ] ⇒ destruct H as [ ? [] ]; simpl in ×
| [ H : _ |- _ ] ⇒ rewrite H
end;
reflexivity.

Definition isomorphic_reflexive : Reflexive isomorphic.
repeat intro.
(λ x, x).
(λ x, x);
t.
Defined.

Definition isomorphic_symmetric : Symmetric isomorphic.
intros x y f.
eexists (f -1).
f;
t.
Defined.

Definition isomorphic_transitive : Transitive isomorphic.
intros x y z f g.
(g f).
(f -1 g -1);
t.
Defined.
End isomorphic_relation.

Hint Resolve @isomorphic_reflexive @isomorphic_symmetric.
Hint Immediate @isomorphic_reflexive @isomorphic_symmetric @isomorphic_transitive.