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" := (isomorphism_inverse 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.