Morphisms.v

(** * Definitions and theorems about {iso,epi,mono,}morphisms in a precategory *)
Require Import Category.Core Functor.Core.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Local Open Scope category_scope.
Local Open Scope morphism_scope.

(** ** Definition of isomorphism *)
Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) :=
  {
    morphism_inverse : morphism C d s;
    left_inverse : morphism_inverse o m = identity _;
    right_inverse : m o morphism_inverse = identity _
  }.

Arguments morphism_inverse {C s d} m {_}.

Local Notation "m ^-1" := (morphism_inverse m) : morphism_scope.

#[export]
Hint Resolve left_inverse right_inverse : category morphism.
#[export]
Hint Rewrite @left_inverse @right_inverse : category.
#[export]
Hint Rewrite @left_inverse @right_inverse : morphism.

Class Isomorphic {C : PreCategory} s d :=
  {
    morphism_isomorphic : morphism C s d;
    isisomorphism_isomorphic : IsIsomorphism morphism_isomorphic
  }.

(*Coercion Build_Isomorphic : IsIsomorphism >-> Isomorphic.*)
Coercion morphism_isomorphic : Isomorphic >-> morphism.
(* Use :> and remove the two following lines,
   once Coq 8.16 is the minimum required version. *)
#[export] Existing Instance isisomorphism_isomorphic.
Coercion isisomorphism_isomorphic : Isomorphic >-> IsIsomorphism.

Local Infix "<~=~>" := Isomorphic : category_scope.

Global Existing Instance isisomorphism_isomorphic.

(** ** Theorems about isomorphisms *)
Section iso_contr.
  Variable C : PreCategory.



  Variables s d : C.

  Local Notation IsIsomorphism_sig_T m :=
    { inverse : morphism C d s
    | { _ : inverse o m = identity _
      | m o inverse = identity _ } } (only parsing).

  Section IsIsomorphism.
    Variable m : morphism C s d.

    (** *** The inverse of a morphism is unique *)
    Lemma inverse_unique (m_inv0 m_inv1 : morphism C d s)
          (left_inverse_0 : m_inv0 o m = identity _)
          (right_inverse_1 : m o m_inv1 = identity _)
    : m_inv0 = m_inv1.C: PreCategory
s, d: C
m: morphism C s d
m_inv0, m_inv1: morphism C d s
left_inverse_0: m_inv0 o m = 1
right_inverse_1: m o m_inv1 = 1
m_inv0 = m_inv1
    Proof.C: PreCategory
s, d: C
m: morphism C s d
m_inv0, m_inv1: morphism C d s
left_inverse_0: m_inv0 o m = 1
right_inverse_1: m o m_inv1 = 1
m_inv0 = m_inv1
      transitivity (m_inv0 o m o m_inv1);
      try solve [ by (rewrite -> ?associativity; rewrite_hyp;
                      autorewrite with morphism)
                | by (rewrite <- ?associativity; rewrite_hyp;
                      autorewrite with morphism) ].
    Qed.

    (** *** Equivalence between the record and sigma versions of [IsIsomorphism] *)
    Lemma issig_isisomorphism
    : IsIsomorphism_sig_T m <~> IsIsomorphism m.C: PreCategory
s, d: C
m: morphism C s d
{inverse : morphism C d s &
{_ : inverse o m = 1 & m o inverse = 1}} <~>
IsIsomorphism m
    Proof.C: PreCategory
s, d: C
m: morphism C s d
{inverse : morphism C d s &
{_ : inverse o m = 1 & m o inverse = 1}} <~>
IsIsomorphism m
      issig.
    Defined.

    (** *** Being an isomorphism is a mere proposition *)
    Global Instance istrunc_isisomorphism : IsHProp (IsIsomorphism m).C: PreCategory
s, d: C
m: morphism C s d
IsHProp (IsIsomorphism m)
    Proof.C: PreCategory
s, d: C
m: morphism C s d
IsHProp (IsIsomorphism m)
      eapply istrunc_equiv_istrunc; [ exact issig_isisomorphism | ].C: PreCategory
s, d: C
m: morphism C s d
IsHProp
  {inverse : morphism C d s &
  {_ : inverse o m = 1 & m o inverse = 1}}
      apply hprop_allpath.C: PreCategory
s, d: C
m: morphism C s d
forall
x
 y : {inverse : morphism C d s &
     {_ : inverse o m = 1 & m o inverse = 1}}, x = y
      intros [x [? ?]] [y [? ?]].C: PreCategory
s, d: C
m: morphism C s d
x: morphism C d s
proj1: x o m = 1
proj2: m o x = 1
y: morphism C d s
proj0: y o m = 1
proj3: m o y = 1
(x; proj1; proj2) = (y; proj0; proj3)
      let H := fresh in
      assert (H : x = y) by (apply inverse_unique; assumption);
        destruct H.C: PreCategory
s, d: C
m: morphism C s d
x: morphism C d s
proj1: x o m = 1
proj2: m o x = 1
proj0: x o m = 1
proj3: m o x = 1
(x; proj1; proj2) = (x; proj0; proj3)
      repeat match goal with
               | _ => progress simpl
               | _ => exact (center _)
               | _ => (exists idpath)
               | _ => apply path_sigma_uncurried
             end.
    Qed.
  End IsIsomorphism.

  Local Notation Isomorphic_sig_T :=
    { m : morphism C s d
    | IsIsomorphism m } (only parsing).

  (** *** Equivalence between record and sigma versions of [Isomorphic] *)
  Lemma issig_isomorphic
  : Isomorphic_sig_T <~> Isomorphic s d.C: PreCategory
s, d: C
{m : morphism C s d & IsIsomorphism m} <~> s <~=~> d
  Proof.C: PreCategory
s, d: C
{m : morphism C s d & IsIsomorphism m} <~> s <~=~> d
    issig.
  Defined.

  Local Notation Isomorphic_full_sig_T :=
    { m : morphism C s d
    | IsIsomorphism_sig_T m } (only parsing).

  (** *** Equivalence between record and fully sigma versions of [Isomorphic] *)
  Definition issig_full_isomorphic
  : Isomorphic_full_sig_T <~> Isomorphic s d
    := (issig_isomorphic oE equiv_functor_sigma_id issig_isisomorphism).

  (** *** Isomorphisms form an hSet *)
  Global Instance trunc_Isomorphic : IsHSet (Isomorphic s d).C: PreCategory
s, d: C
IsHSet (s <~=~> d)
  Proof.C: PreCategory
s, d: C
IsHSet (s <~=~> d)
    eapply istrunc_equiv_istrunc; [ exact issig_isomorphic | ].C: PreCategory
s, d: C
IsHSet {m : morphism C s d & IsIsomorphism m}
    typeclasses eauto.
  Qed.

  (** *** Equality between isomorphisms is determined by equality between their forward components *)
  Definition path_isomorphic (i j : Isomorphic s d)
  : @morphism_isomorphic _ _ _ i = @morphism_isomorphic _ _ _ j
    -> i = j.C: PreCategory
s, d: C
i, j: s <~=~> d
i = j -> i = j
  Proof.C: PreCategory
s, d: C
i, j: s <~=~> d
i = j -> i = j
    destruct i, j; simpl.C: PreCategory
s, d: C
morphism_isomorphic0: morphism C s d
isisomorphism_isomorphic0: IsIsomorphism
  morphism_isomorphic0
morphism_isomorphic1: morphism C s d
isisomorphism_isomorphic1: IsIsomorphism
  morphism_isomorphic1
morphism_isomorphic0 = morphism_isomorphic1 ->
{|
  morphism_isomorphic := morphism_isomorphic0;
  isisomorphism_isomorphic :=
    isisomorphism_isomorphic0
|} =
{|
  morphism_isomorphic := morphism_isomorphic1;
  isisomorphism_isomorphic :=
    isisomorphism_isomorphic1
|}
    intro; path_induction.C: PreCategory
s, d: C
morphism_isomorphic0: morphism C s d
isisomorphism_isomorphic0, isisomorphism_isomorphic1: IsIsomorphism
  morphism_isomorphic0
{|
  morphism_isomorphic := morphism_isomorphic0;
  isisomorphism_isomorphic :=
    isisomorphism_isomorphic0
|} =
{|
  morphism_isomorphic := morphism_isomorphic0;
  isisomorphism_isomorphic :=
    isisomorphism_isomorphic1
|}
    f_ap.C: PreCategory
s, d: C
morphism_isomorphic0: morphism C s d
isisomorphism_isomorphic0, isisomorphism_isomorphic1: IsIsomorphism
  morphism_isomorphic0
isisomorphism_isomorphic0 = isisomorphism_isomorphic1
    exact (center _).
  Defined.

  (** *** Relations between [path_isomorphic], [ap morphism_inverse], and [ap morphism_isomorphic] *)
  Definition ap_morphism_isomorphic_path_isomorphic (i j : Isomorphic s d) p
  : ap (@morphism_isomorphic _ _ _) (path_isomorphic i j p) = p.C: PreCategory
s, d: C
i, j: s <~=~> d
p: i = j
ap (@morphism_isomorphic C s d)
  (path_isomorphic i j p) = p
  Proof.C: PreCategory
s, d: C
i, j: s <~=~> d
p: i = j
ap (@morphism_isomorphic C s d)
  (path_isomorphic i j p) = p
    unfold path_isomorphic.C: PreCategory
s, d: C
i, j: s <~=~> d
p: i = j
ap (@morphism_isomorphic C s d)
  (paths_rect (morphism C s d) i
     (fun (morphism_isomorphic1 : morphism C s d)
        (_ : i = morphism_isomorphic1) =>
      forall
      isisomorphism_isomorphic1 : IsIsomorphism
                                    morphism_isomorphic1,
      {|
        morphism_isomorphic := i;
        isisomorphism_isomorphic := i
      |} =
      {|
        morphism_isomorphic := morphism_isomorphic1;
        isisomorphism_isomorphic :=
          isisomorphism_isomorphic1
      |})
     (fun isisomorphism_isomorphic1 : IsIsomorphism i
      =>
      ap11 1 (center (i = isisomorphism_isomorphic1)))
     j p j) = p
    destruct i, j.C: PreCategory
s, d: C
morphism_isomorphic0: morphism C s d
isisomorphism_isomorphic0: IsIsomorphism
  morphism_isomorphic0
morphism_isomorphic1: morphism C s d
isisomorphism_isomorphic1: IsIsomorphism
  morphism_isomorphic1
p: {|
  morphism_isomorphic := morphism_isomorphic0;
  isisomorphism_isomorphic :=
    isisomorphism_isomorphic0
|} =
{|
  morphism_isomorphic := morphism_isomorphic1;
  isisomorphism_isomorphic :=
    isisomorphism_isomorphic1
|}
ap (@morphism_isomorphic C s d)
  (paths_rect (morphism C s d) morphism_isomorphic0
     (fun (morphism_isomorphic1 : morphism C s d)
        (_ : morphism_isomorphic0 =
             morphism_isomorphic1) =>
      forall
      isisomorphism_isomorphic1 : IsIsomorphism
                                    morphism_isomorphic1,
      {|
        morphism_isomorphic := morphism_isomorphic0;
        isisomorphism_isomorphic :=
          isisomorphism_isomorphic0
      |} =
      {|
        morphism_isomorphic := morphism_isomorphic1;
        isisomorphism_isomorphic :=
          isisomorphism_isomorphic1
      |})
     (fun
        isisomorphism_isomorphic1 : IsIsomorphism
                                      morphism_isomorphic0
      =>
      ap11 1
        (center
           (isisomorphism_isomorphic0 =
            isisomorphism_isomorphic1)))
     morphism_isomorphic1 p isisomorphism_isomorphic1) =
p
    path_induction_hammer.
  Qed.

  Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q
  : ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.C: PreCategory
s, d: C
i, j: s <~=~> d
p: i = j
q: (fun e : s <~=~> d => e^-1) i =
(fun e : s <~=~> d => e^-1) j
ap (fun e : s <~=~> d => e^-1) (path_isomorphic i j p) =
q
  Proof.C: PreCategory
s, d: C
i, j: s <~=~> d
p: i = j
q: (fun e : s <~=~> d => e^-1) i =
(fun e : s <~=~> d => e^-1) j
ap (fun e : s <~=~> d => e^-1) (path_isomorphic i j p) =
q
    apply path_ishprop.
  Qed.

  (** *** Equality between isomorphisms is equivalent to by equality between their forward components *)
  Global Instance isequiv_path_isomorphic {i j}
  : IsEquiv (path_isomorphic i j).C: PreCategory
s, d: C
i, j: s <~=~> d
IsEquiv (path_isomorphic i j)
  Proof.C: PreCategory
s, d: C
i, j: s <~=~> d
IsEquiv (path_isomorphic i j)
    intros.C: PreCategory
s, d: C
i, j: s <~=~> d
IsEquiv (path_isomorphic i j)
    apply (isequiv_adjointify
             (path_isomorphic i j)
             (ap (@morphism_isomorphic _ _ _)));
      intro; [ destruct i | destruct i, j ];
      path_induction_hammer.
  Defined.
End iso_contr.

Section iso_equiv_relation.
  Variable C : PreCategory.

  (** *** The identity is an isomorphism *)
  Global Instance isisomorphism_identity (x : C) : IsIsomorphism (identity x)
    := {| morphism_inverse := identity x;
          left_inverse := left_identity C x x (identity x);
          right_inverse := right_identity C x x (identity x) |}.

  (** *** Inverses of isomorphisms are isomorphisms *)
  Definition isisomorphism_inverse `(@IsIsomorphism C x y m) : IsIsomorphism m^-1
    := {| morphism_inverse := m;
          left_inverse := right_inverse;
          right_inverse := left_inverse |}.

  Local Ltac iso_comp_t inv_lemma :=
    etransitivity; [ | apply inv_lemma ];
    first [ rewrite -> ?associativity; apply ap
          | rewrite <- ?associativity; apply ap ];
    first [ rewrite -> ?associativity; rewrite inv_lemma
          | rewrite <- ?associativity; rewrite inv_lemma ];
    auto with morphism.

  (** *** Composition of isomorphisms gives an isomorphism *)
  Global Instance isisomorphism_compose `(@IsIsomorphism C y z m0) `(@IsIsomorphism C x y m1)
  : IsIsomorphism (m0 o m1).C: PreCategory
y, z: C
m0: morphism C y z
H: IsIsomorphism m0
x: C
m1: morphism C x y
H0: IsIsomorphism m1
IsIsomorphism (m0 o m1)
  Proof.C: PreCategory
y, z: C
m0: morphism C y z
H: IsIsomorphism m0
x: C
m1: morphism C x y
H0: IsIsomorphism m1
IsIsomorphism (m0 o m1)
    exists (m1^-1 o m0^-1);
    [ abstract iso_comp_t @left_inverse
    | abstract iso_comp_t @right_inverse ].
  Defined.

  #[local]
  Hint Immediate isisomorphism_inverse : typeclass_instances.

  (** *** Being isomorphic is a reflexive relation *)
  Global Instance isomorphic_refl : Reflexive (@Isomorphic C)
    := fun x : C => {| morphism_isomorphic := identity x |}.

  (** *** Being isomorphic is a symmetric relation *)
  Global Instance isomorphic_sym : Symmetric (@Isomorphic C)
    := fun x y X => {| morphism_isomorphic := X^-1 |}.

  (** *** Being isomorphic is a transitive relation *)
  Global Instance isomorphic_trans : Transitive (@Isomorphic C)
    := fun x y z X Y => {| morphism_isomorphic := @morphism_isomorphic _ _ _ Y o @morphism_isomorphic _ _ _ X |}.

  (** *** Equality gives rise to isomorphism *)
  Definition idtoiso (x y : C) (H : x = y) : Isomorphic x y
    := match H in (_ = y0) return (x <~=~> y0) with
         | 1%path => reflexivity x
       end.
End iso_equiv_relation.

#[export]
Hint Immediate isisomorphism_inverse : typeclass_instances.

(** ** Epimorphisms and Monomorphisms *)
(** Quoting Wikipedia:

    In category theory, an epimorphism (also called an epic morphism
    or, colloquially, an epi) is a morphism [f : X → Y] which is
    right-cancellative in the sense that, for all morphisms [g, g' : Y
    → Z], [g ∘ f = g' ∘ f → g = g']

    Epimorphisms are analogues of surjective functions, but they are
    not exactly the same. The dual of an epimorphism is a monomorphism
    (i.e. an epimorphism in a category [C] is a monomorphism in the
    dual category [Cᵒᵖ]).  *)

Class IsEpimorphism {C} {x y} (m : morphism C x y) :=
  is_epimorphism : forall z (m1 m2 : morphism C y z),
                     m1 o m = m2 o m
                     -> m1 = m2.
Class IsMonomorphism {C} {x y} (m : morphism C x y) :=
  is_monomorphism : forall z (m1 m2 : morphism C z x),
                      m o m1 = m o m2
                      -> m1 = m2.

(** We make [IsEpimorphism] and [IsMonomorphism] transparent to
    typeclass search so that we can infer things like [IsHProp]
    automatically. *)
#[global] Typeclasses Transparent IsEpimorphism IsMonomorphism.

Record Epimorphism {C} x y :=
  {
    Epimorphism_morphism :> morphism C x y;
    Epimorphism_IsEpimorphism :> IsEpimorphism Epimorphism_morphism
  }.

Record Monomorphism {C} x y :=
  {
    Monomorphism_morphism :> morphism C x y;
    Monomorphism_IsMonomorphism :> IsMonomorphism Monomorphism_morphism
  }.

Global Existing Instances Epimorphism_IsEpimorphism Monomorphism_IsMonomorphism.

Local Notation "x ->> y" := (Epimorphism x y).
Local Notation "x (-> y" := (Monomorphism x y).

Class IsSectionOf C x y (s : morphism C x y) (r : morphism C y x)
  := is_sect_morphism : r o s = identity _.

Arguments IsSectionOf [C x y] s r.

Section EpiMono.
  Variable C : PreCategory.

  Section properties.
    (** *** The identity is an epimorphism *)
    Global Instance isepimorphism_identity (x : C)
    : IsEpimorphism (identity x).C: PreCategory
x: C
IsEpimorphism 1
    Proof.C: PreCategory
x: C
IsEpimorphism 1
      repeat intro; autorewrite with morphism in *; trivial.
    Qed.

    (** *** The identity is a monomorphism *)
    Global Instance ismonomorphism_identity (x : C)
    : IsMonomorphism (identity x).C: PreCategory
x: C
IsMonomorphism 1
    Proof.C: PreCategory
x: C
IsMonomorphism 1
      repeat intro; autorewrite with morphism in *; trivial.
    Qed.

    (** *** Composition of epimorphisms gives an epimorphism *)
    Global Instance isepimorphism_compose s d d' m0 m1
    : IsEpimorphism m0
      -> IsEpimorphism m1
      -> IsEpimorphism (@compose C s d d' m0 m1).C: PreCategory
s, d, d': C
m0: morphism C d d'
m1: morphism C s d
IsEpimorphism m0 ->
IsEpimorphism m1 -> IsEpimorphism (m0 o m1)
    Proof.C: PreCategory
s, d, d': C
m0: morphism C d d'
m1: morphism C s d
IsEpimorphism m0 ->
IsEpimorphism m1 -> IsEpimorphism (m0 o m1)
      repeat intro.C: PreCategory
s, d, d': C
m0: morphism C d d'
m1: morphism C s d
X: IsEpimorphism m0
X0: IsEpimorphism m1
z: C
m2, m3: morphism C d' z
X1: m2 o (m0 o m1) = m3 o (m0 o m1)
m2 = m3
      rewrite <- !associativity in *.C: PreCategory
s, d, d': C
m0: morphism C d d'
m1: morphism C s d
X: IsEpimorphism m0
X0: IsEpimorphism m1
z: C
m2, m3: morphism C d' z
X1: m2 o m0 o m1 = m3 o m0 o m1
m2 = m3
      apply_hyp.
    Qed.

    (** *** Composition of monomorphisms gives a monomorphism *)
    Global Instance ismonomorphism_compose s d d' m0 m1
    : IsMonomorphism m0
      -> IsMonomorphism m1
      -> IsMonomorphism (@compose C s d d' m0 m1).C: PreCategory
s, d, d': C
m0: morphism C d d'
m1: morphism C s d
IsMonomorphism m0 ->
IsMonomorphism m1 -> IsMonomorphism (m0 o m1)
    Proof.C: PreCategory
s, d, d': C
m0: morphism C d d'
m1: morphism C s d
IsMonomorphism m0 ->
IsMonomorphism m1 -> IsMonomorphism (m0 o m1)
      repeat intro.C: PreCategory
s, d, d': C
m0: morphism C d d'
m1: morphism C s d
X: IsMonomorphism m0
X0: IsMonomorphism m1
z: C
m2, m3: morphism C z s
X1: m0 o m1 o m2 = m0 o m1 o m3
m2 = m3
      rewrite !associativity in *.C: PreCategory
s, d, d': C
m0: morphism C d d'
m1: morphism C s d
X: IsMonomorphism m0
X0: IsMonomorphism m1
z: C
m2, m3: morphism C z s
X1: m0 o (m1 o m2) = m0 o (m1 o m3)
m2 = m3
      apply_hyp.
    Qed.
  End properties.

  (** *** Existence of {epi,mono}morphisms are a preorder *)
  Section equiv.
    Global Instance reflexive_epimorphism : Reflexive (@Epimorphism C)
      := fun x => Build_Epimorphism (isepimorphism_identity x).

    Global Instance reflexive_monomorphism : Reflexive (@Monomorphism C)
      := fun x => Build_Monomorphism (ismonomorphism_identity x).

    Global Instance transitive_epimorphism : Transitive (@Epimorphism C)
      := fun _ _ _ m0 m1 => Build_Epimorphism (isepimorphism_compose m1 m0).

    Global Instance transitive_monomorphism : Transitive (@Monomorphism C)
      := fun _ _ _ m0 m1 => Build_Monomorphism (ismonomorphism_compose m1 m0).
  End equiv.

  Section sect.
    Local Ltac epi_mono_sect_t :=
      let t :=
          (solve [ autorewrite with morphism;
                   reflexivity
                 | rewrite_hyp;
                   autorewrite with morphism;
                   reflexivity ]) in
      first [ rewrite -> ?associativity; t
            | rewrite <- ?associativity; t].

    (** *** Retractions are epimorphisms *)
    Global Instance isepimorphism_retr `(@IsSectionOf C x y s r)
    : IsEpimorphism r | 1000.C: PreCategory
x, y: C
s: morphism C x y
r: morphism C y x
H: IsSectionOf s r
IsEpimorphism r
    Proof.C: PreCategory
x, y: C
s: morphism C x y
r: morphism C y x
H: IsSectionOf s r
IsEpimorphism r
      (intros ? m1 m2 ?).C: PreCategory
x, y: C
s: morphism C x y
r: morphism C y x
H: IsSectionOf s r
z: C
m1, m2: morphism C x z
X: m1 o r = m2 o r
m1 = m2
      unfold IsSectionOf in *.C: PreCategory
x, y: C
s: morphism C x y
r: morphism C y x
H: r o s = 1
z: C
m1, m2: morphism C x z
X: m1 o r = m2 o r
m1 = m2
      transitivity ((m1 o r) o s);
        [ | transitivity ((m2 o r) o s) ];
        epi_mono_sect_t.
    Qed.

    (** *** Sections are monomorphisms *)
    Global Instance ismonomorphism_sect `(@IsSectionOf C x y s r)
    : IsMonomorphism s | 1000.C: PreCategory
x, y: C
s: morphism C x y
r: morphism C y x
H: IsSectionOf s r
IsMonomorphism s
    Proof.C: PreCategory
x, y: C
s: morphism C x y
r: morphism C y x
H: IsSectionOf s r
IsMonomorphism s
      (intros ? m1 m2 ?).C: PreCategory
x, y: C
s: morphism C x y
r: morphism C y x
H: IsSectionOf s r
z: C
m1, m2: morphism C z x
X: s o m1 = s o m2
m1 = m2
      transitivity (r o (s o m1));
        [ | transitivity (r o (s o m2)) ];
        epi_mono_sect_t.
    Qed.

    (** *** Isomorphisms are both sections and retractions *)
    Global Instance issect_isisomorphism `(@IsIsomorphism C x y m)
    : IsSectionOf m m^-1 | 1000
      := left_inverse.

    Global Instance isretr_isisomorphism `(@IsIsomorphism C x y m)
    : IsSectionOf m^-1 m | 1000
      := right_inverse.
  End sect.

  (** *** Isomorphisms are therefore epimorphisms and monomorphisms *)
  Section iso.
    Global Instance isepimorphism_isisomorphism `(@IsIsomorphism C s d m)
    : IsEpimorphism m | 1000
      := _.
    Global Instance ismonomorphism_isisomorphism `(@IsIsomorphism C s d m)
    : IsMonomorphism m | 1000
      := _.
  End iso.
End EpiMono.

#[export] Hint Immediate isisomorphism_inverse : typeclass_instances.

#[export]
Hint Immediate
  isepimorphism_identity ismonomorphism_identity
  ismonomorphism_compose isepimorphism_compose
  : category morphism.

(** ** Lemmas about [idtoiso] *)
Section iso_lemmas.
  Local Ltac idtoiso_t :=
    path_induction; simpl; autorewrite with morphism; reflexivity.

  (** *** [transport]ing across an equality of morphisms is the same as conjugating with [idtoiso] *)
  Lemma idtoiso_of_transport (C D : PreCategory) s d
        (m1 m2 : morphism C s d)
        (p : m1 = m2)
        (s' d' : morphism C s d -> D) u
  : @transport _ (fun m => morphism D (s' m) (d' m)) _ _ p u
    = idtoiso _ (ap d' p) o u o (idtoiso _ (ap s' p))^-1.C, D: PreCategory
s, d: C
m1, m2: morphism C s d
p: m1 = m2
s', d': morphism C s d -> D
u: morphism D (s' m1) (d' m1)
transport
  (fun m : morphism C s d => morphism D (s' m) (d' m))
  p u =
idtoiso D (ap d' p) o u o (idtoiso D (ap s' p))^-1
  Proof.C, D: PreCategory
s, d: C
m1, m2: morphism C s d
p: m1 = m2
s', d': morphism C s d -> D
u: morphism D (s' m1) (d' m1)
transport
  (fun m : morphism C s d => morphism D (s' m) (d' m))
  p u =
idtoiso D (ap d' p) o u o (idtoiso D (ap s' p))^-1 idtoiso_t. Qed.

  (** *** [idtoiso] respects inverse *)
  Lemma idtoiso_inv (C : PreCategory) (s d : C) (p : s = d)
  : (idtoiso _ p)^-1 = idtoiso _ (p^)%path.C: PreCategory
s, d: C
p: s = d
(idtoiso C p)^-1 = idtoiso C p^
  Proof.C: PreCategory
s, d: C
p: s = d
(idtoiso C p)^-1 = idtoiso C p^
    path_induction; reflexivity.
  Defined.

  (** *** [idtoiso] respects composition *)
  Lemma idtoiso_comp (C : PreCategory) (s d d' : C)
        (m1 : d = d') (m2 : s = d)
  : idtoiso _ m1 o idtoiso _ m2 = idtoiso _ (m2 @ m1)%path.C: PreCategory
s, d, d': C
m1: d = d'
m2: s = d
idtoiso C m1 o idtoiso C m2 = idtoiso C (m2 @ m1)
  Proof.C: PreCategory
s, d, d': C
m1: d = d'
m2: s = d
idtoiso C m1 o idtoiso C m2 = idtoiso C (m2 @ m1) idtoiso_t. Qed.

  (** These are useful when tactics are too slow and [rewrite] doesn't
      work. *)
  Lemma idtoiso_comp3 (C : PreCategory) (s d d' d'' : C)
        (m0 : d' = d'') (m1 : d = d') (m2 : s = d)
  : idtoiso _ m0 o (idtoiso _ m1 o idtoiso _ m2) = idtoiso _ ((m2 @ m1) @ m0)%path.C: PreCategory
s, d, d', d'': C
m0: d' = d''
m1: d = d'
m2: s = d
idtoiso C m0 o (idtoiso C m1 o idtoiso C m2) =
idtoiso C ((m2 @ m1) @ m0)
  Proof.C: PreCategory
s, d, d', d'': C
m0: d' = d''
m1: d = d'
m2: s = d
idtoiso C m0 o (idtoiso C m1 o idtoiso C m2) =
idtoiso C ((m2 @ m1) @ m0) idtoiso_t. Qed.

  Lemma idtoiso_comp3' (C : PreCategory) (s d d' d'' : C)
        (m0 : d' = d'') (m1 : d = d') (m2 : s = d)
  : (idtoiso _ m0 o idtoiso _ m1) o idtoiso _ m2 = idtoiso _ (m2 @ (m1 @ m0))%path.C: PreCategory
s, d, d', d'': C
m0: d' = d''
m1: d = d'
m2: s = d
idtoiso C m0 o idtoiso C m1 o idtoiso C m2 =
idtoiso C (m2 @ (m1 @ m0))
  Proof.C: PreCategory
s, d, d', d'': C
m0: d' = d''
m1: d = d'
m2: s = d
idtoiso C m0 o idtoiso C m1 o idtoiso C m2 =
idtoiso C (m2 @ (m1 @ m0)) idtoiso_t. Qed.

  Lemma idtoiso_comp4 (C : PreCategory) (s d d' d'' d''' : C)
        (m0 : d'' = d''') (m1 : d' = d'') (m2 : d = d') (m3 : s = d)
  : idtoiso _ m0 o (idtoiso _ m1 o (idtoiso _ m2 o idtoiso _ m3)) = idtoiso _ (((m3 @ m2) @ m1) @ m0)%path.C: PreCategory
s, d, d', d'', d''': C
m0: d'' = d'''
m1: d' = d''
m2: d = d'
m3: s = d
idtoiso C m0
o (idtoiso C m1 o (idtoiso C m2 o idtoiso C m3)) =
idtoiso C (((m3 @ m2) @ m1) @ m0)
  Proof.C: PreCategory
s, d, d', d'', d''': C
m0: d'' = d'''
m1: d' = d''
m2: d = d'
m3: s = d
idtoiso C m0
o (idtoiso C m1 o (idtoiso C m2 o idtoiso C m3)) =
idtoiso C (((m3 @ m2) @ m1) @ m0) idtoiso_t. Qed.

  Lemma idtoiso_comp4' (C : PreCategory) (s d d' d'' d''' : C)
        (m0 : d'' = d''') (m1 : d' = d'') (m2 : d = d') (m3 : s = d)
  : ((idtoiso _ m0 o idtoiso _ m1) o idtoiso _ m2) o idtoiso _ m3 = idtoiso _ (m3 @ (m2 @ (m1 @ m0)))%path.C: PreCategory
s, d, d', d'', d''': C
m0: d'' = d'''
m1: d' = d''
m2: d = d'
m3: s = d
idtoiso C m0 o idtoiso C m1 o idtoiso C m2
o idtoiso C m3 = idtoiso C (m3 @ (m2 @ (m1 @ m0)))
  Proof.C: PreCategory
s, d, d', d'', d''': C
m0: d'' = d'''
m1: d' = d''
m2: d = d'
m3: s = d
idtoiso C m0 o idtoiso C m1 o idtoiso C m2
o idtoiso C m3 = idtoiso C (m3 @ (m2 @ (m1 @ m0))) idtoiso_t. Qed.

  Lemma idtoiso_comp5 (C : PreCategory) (s d d' d'' d''' d'''' : C)
        (m0 : d''' = d'''') (m1 : d'' = d''') (m2 : d' = d'') (m3 : d = d') (m4 : s = d)
  : idtoiso _ m0 o (idtoiso _ m1 o (idtoiso _ m2 o (idtoiso _ m3 o idtoiso _ m4)))
    = idtoiso _ ((((m4 @ m3) @ m2) @ m1) @ m0)%path.C: PreCategory
s, d, d', d'', d''', d'''': C
m0: d''' = d''''
m1: d'' = d'''
m2: d' = d''
m3: d = d'
m4: s = d
idtoiso C m0
o (idtoiso C m1
   o (idtoiso C m2 o (idtoiso C m3 o idtoiso C m4))) =
idtoiso C ((((m4 @ m3) @ m2) @ m1) @ m0)
  Proof.C: PreCategory
s, d, d', d'', d''', d'''': C
m0: d''' = d''''
m1: d'' = d'''
m2: d' = d''
m3: d = d'
m4: s = d
idtoiso C m0
o (idtoiso C m1
   o (idtoiso C m2 o (idtoiso C m3 o idtoiso C m4))) =
idtoiso C ((((m4 @ m3) @ m2) @ m1) @ m0) idtoiso_t. Qed.

  Lemma idtoiso_comp5' (C : PreCategory) (s d d' d'' d''' d'''' : C)
        (m0 : d''' = d'''') (m1 : d'' = d''') (m2 : d' = d'') (m3 : d = d') (m4 : s = d)
  : (((idtoiso _ m0 o idtoiso _ m1) o idtoiso _ m2) o idtoiso _ m3) o idtoiso _ m4
    = idtoiso _ (m4 @ (m3 @ (m2 @ (m1 @ m0))))%path.C: PreCategory
s, d, d', d'', d''', d'''': C
m0: d''' = d''''
m1: d'' = d'''
m2: d' = d''
m3: d = d'
m4: s = d
idtoiso C m0 o idtoiso C m1 o idtoiso C m2
o idtoiso C m3 o idtoiso C m4 =
idtoiso C (m4 @ (m3 @ (m2 @ (m1 @ m0))))
  Proof.C: PreCategory
s, d, d', d'', d''', d'''': C
m0: d''' = d''''
m1: d'' = d'''
m2: d' = d''
m3: d = d'
m4: s = d
idtoiso C m0 o idtoiso C m1 o idtoiso C m2
o idtoiso C m3 o idtoiso C m4 =
idtoiso C (m4 @ (m3 @ (m2 @ (m1 @ m0)))) idtoiso_t. Qed.

  (** *** [idtoiso] respects application of functors on morphisms and objects *)
  Lemma idtoiso_functor (C D : PreCategory) (s d : C) (m : s = d)
        (F : Functor C D)
  : F _1 (idtoiso _ m) = idtoiso _ (ap (object_of F) m).C, D: PreCategory
s, d: C
m: s = d
F: Functor C D
F _1 (idtoiso C m) = idtoiso D (ap F m)
  Proof.C, D: PreCategory
s, d: C
m: s = d
F: Functor C D
F _1 (idtoiso C m) = idtoiso D (ap F m)
    path_induction; simpl; apply identity_of.
  Defined.

  (** *** Functors preserve isomorphisms *)
  Global Instance iso_functor C D (F : Functor C D) `(@IsIsomorphism C s d m)
  : IsIsomorphism (F _1 m).C, D: PreCategory
F: Functor C D
s, d: C
m: morphism C s d
H: IsIsomorphism m
IsIsomorphism (F _1 m)
  Proof.C, D: PreCategory
F: Functor C D
s, d: C
m: morphism C s d
H: IsIsomorphism m
IsIsomorphism (F _1 m)
    refine ({| morphism_inverse := F _1 m^-1 |}).C, D: PreCategory
F: Functor C D
s, d: C
m: morphism C s d
H: IsIsomorphism m
F _1 m^-1 o F _1 m = 1
C, D: PreCategory
F: Functor C D
s, d: C
m: morphism C s d
H: IsIsomorphism m
F _1 m o F _1 m^-1 = 1
    -C, D: PreCategory
F: Functor C D
s, d: C
m: morphism C s d
H: IsIsomorphism m
F _1 m^-1 o F _1 m = 1 abstract (rewrite <- composition_of, ?left_inverse, ?right_inverse, identity_of; reflexivity).
    -C, D: PreCategory
F: Functor C D
s, d: C
m: morphism C s d
H: IsIsomorphism m
F _1 m o F _1 m^-1 = 1 abstract (rewrite <- composition_of, ?left_inverse, ?right_inverse, identity_of; reflexivity).
  Defined.
End iso_lemmas.

#[export]
Hint Extern 1 (@IsIsomorphism _ _ _ (@morphism_of ?C ?D ?F ?s ?d ?m))
=> apply (@iso_functor C D F s d m) : typeclass_instances.

#[export]
Hint Rewrite idtoiso_of_transport idtoiso_inv idtoiso_comp idtoiso_functor.

(** ** Lemmas about how to move isomorphisms around equalities, following [HoTT.PathGroupoids] *)
Section iso_concat_lemmas.
  Variable C : PreCategory.

  Local Ltac iso_concat_t' :=
    intros;
    repeat match goal with
             | [ H : ?x = ?y |- _ ] => atomic y; induction H
             | [ H : ?x = ?y |- _ ] => atomic x; symmetry in H; induction H
           end;
    repeat first [ done
                 | rewrite -> ?associativity;
                   progress rewrite ?left_identity, ?right_identity, ?left_inverse, ?right_inverse
                 | rewrite <- ?associativity;
                   progress rewrite ?left_identity, ?right_identity, ?left_inverse, ?right_inverse
                 | rewrite -> ?associativity; progress f_ap; []
                 | rewrite <- ?associativity; progress f_ap; [] ].

  Local Ltac iso_concat_t_id_fin :=
    match goal with
      | [ |- context[@identity ?C ?x] ]
        => generalize dependent (identity x)
    end;
    iso_concat_t'.

  Local Ltac iso_concat_t_id lem :=
    first [ solve [
                etransitivity; [ | eapply lem ];
                iso_concat_t_id_fin
              ]
          | solve [
                etransitivity; [ symmetry; eapply lem | ];
                iso_concat_t_id_fin
          ] ].

  Local Ltac iso_concat_t :=
    iso_concat_t';
    try first [ solve [ iso_concat_t_id @left_identity ]
              | solve [ iso_concat_t_id @right_identity ] ].

  Definition iso_compose_pV `(@IsIsomorphism C x y p)
  : p o p^-1 = identity _
    := right_inverse.
  Definition iso_compose_Vp `(@IsIsomorphism C x y p)
  : p^-1 o p = identity _
    := left_inverse.

  Definition iso_compose_V_pp `(@IsIsomorphism C y z p) `(q : morphism C x y)
  : p^-1 o (p o q) = q.C: PreCategory
y, z: C
p: morphism C y z
H: IsIsomorphism p
x: C
q: morphism C x y
p^-1 o (p o q) = q
  Proof.C: PreCategory
y, z: C
p: morphism C y z
H: IsIsomorphism p
x: C
q: morphism C x y
p^-1 o (p o q) = q iso_concat_t. Qed.

  Definition iso_compose_p_Vp `(@IsIsomorphism C x z p) `(q : morphism C y z)
  : p o (p^-1 o q) = q.C: PreCategory
x, z: C
p: morphism C x z
H: IsIsomorphism p
y: C
q: morphism C y z
p o (p^-1 o q) = q
  Proof.C: PreCategory
x, z: C
p: morphism C x z
H: IsIsomorphism p
y: C
q: morphism C y z
p o (p^-1 o q) = q iso_concat_t. Qed.

  Definition iso_compose_pp_V `(p : morphism C y z) `(@IsIsomorphism C x y q)
  : (p o q) o q^-1 = p.C: PreCategory
y, z: C
p: morphism C y z
x: C
q: morphism C x y
H: IsIsomorphism q
p o q o q^-1 = p
  Proof.C: PreCategory
y, z: C
p: morphism C y z
x: C
q: morphism C x y
H: IsIsomorphism q
p o q o q^-1 = p iso_concat_t. Qed.

  Definition iso_compose_pV_p `(p : morphism C x z) `(@IsIsomorphism C x y q)
  : (p o q^-1) o q = p.C: PreCategory
x, z: C
p: morphism C x z
y: C
q: morphism C x y
H: IsIsomorphism q
p o q^-1 o q = p
  Proof.C: PreCategory
x, z: C
p: morphism C x z
y: C
q: morphism C x y
H: IsIsomorphism q
p o q^-1 o q = p iso_concat_t. Qed.

  Definition iso_inv_pp `(@IsIsomorphism C y z p) `(@IsIsomorphism C x y q)
  : (p o q)^-1 = q^-1 o p^-1.C: PreCategory
y, z: C
p: morphism C y z
H: IsIsomorphism p
x: C
q: morphism C x y
H0: IsIsomorphism q
(p o q)^-1 = q^-1 o p^-1
  Proof.C: PreCategory
y, z: C
p: morphism C y z
H: IsIsomorphism p
x: C
q: morphism C x y
H0: IsIsomorphism q
(p o q)^-1 = q^-1 o p^-1 iso_concat_t. Qed.

  Definition iso_inv_Vp `(@IsIsomorphism C y z p) `(@IsIsomorphism C x z q)
  : (p^-1 o q)^-1 = q^-1 o p.C: PreCategory
y, z: C
p: morphism C y z
H: IsIsomorphism p
x: C
q: morphism C x z
H0: IsIsomorphism q
(p^-1 o q)^-1 = q^-1 o p
  Proof.C: PreCategory
y, z: C
p: morphism C y z
H: IsIsomorphism p
x: C
q: morphism C x z
H0: IsIsomorphism q
(p^-1 o q)^-1 = q^-1 o p iso_concat_t. Qed.

  Definition iso_inv_pV `(@IsIsomorphism C x y p) `(@IsIsomorphism C x z q)
  : (p o q^-1)^-1 = q o p^-1.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C x z
H0: IsIsomorphism q
(p o q^-1)^-1 = q o p^-1
  Proof.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C x z
H0: IsIsomorphism q
(p o q^-1)^-1 = q o p^-1 iso_concat_t. Qed.

  Definition iso_inv_VV `(@IsIsomorphism C x y p) `(@IsIsomorphism C y z q)
  : (p^-1 o q^-1)^-1 = q o p.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C y z
H0: IsIsomorphism q
(p^-1 o q^-1)^-1 = q o p
  Proof.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C y z
H0: IsIsomorphism q
(p^-1 o q^-1)^-1 = q o p iso_concat_t. Qed.

  Definition iso_moveR_Mp `(p : morphism C x y) `(q : morphism C x z) `(@IsIsomorphism C y z r)
  : p = (r^-1 o q) -> (r o p) = q.C: PreCategory
x, y: C
p: morphism C x y
z: C
q: morphism C x z
r: morphism C y z
H: IsIsomorphism r
p = r^-1 o q -> r o p = q
  Proof.C: PreCategory
x, y: C
p: morphism C x y
z: C
q: morphism C x z
r: morphism C y z
H: IsIsomorphism r
p = r^-1 o q -> r o p = q iso_concat_t. Qed.

  Definition iso_moveR_pM `(@IsIsomorphism C x y p) `(q : morphism C x z) `(r : morphism C y z)
  : r = (q o p^-1) -> (r o p) = q.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C x z
r: morphism C y z
r = q o p^-1 -> r o p = q
  Proof.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C x z
r: morphism C y z
r = q o p^-1 -> r o p = q iso_concat_t. Qed.

  Definition iso_moveR_Vp `(p : morphism C x y) `(q : morphism C x z) `(@IsIsomorphism C z y r)
  : p = (r o q) -> (r^-1 o p) = q.C: PreCategory
x, y: C
p: morphism C x y
z: C
q: morphism C x z
r: morphism C z y
H: IsIsomorphism r
p = r o q -> r^-1 o p = q
  Proof.C: PreCategory
x, y: C
p: morphism C x y
z: C
q: morphism C x z
r: morphism C z y
H: IsIsomorphism r
p = r o q -> r^-1 o p = q iso_concat_t. Qed.

  Definition iso_moveR_pV `(@IsIsomorphism C x y p) `(q : morphism C y z) `(r : morphism C x z)
  : r = (q o p) -> (r o p^-1) = q.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C y z
r: morphism C x z
r = q o p -> r o p^-1 = q
  Proof.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C y z
r: morphism C x z
r = q o p -> r o p^-1 = q iso_concat_t. Qed.

  Definition iso_moveL_Mp `(p : morphism C x y) `(q : morphism C x z) `(@IsIsomorphism C y z r)
  : (r^-1 o q) = p -> q = (r o p).C: PreCategory
x, y: C
p: morphism C x y
z: C
q: morphism C x z
r: morphism C y z
H: IsIsomorphism r
r^-1 o q = p -> q = r o p
  Proof.C: PreCategory
x, y: C
p: morphism C x y
z: C
q: morphism C x z
r: morphism C y z
H: IsIsomorphism r
r^-1 o q = p -> q = r o p iso_concat_t. Qed.

  Definition iso_moveL_pM `(@IsIsomorphism C x y p) `(q : morphism C x z) `(r : morphism C y z)
  : (q o p^-1) = r -> q = (r o p).C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C x z
r: morphism C y z
q o p^-1 = r -> q = r o p
  Proof.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C x z
r: morphism C y z
q o p^-1 = r -> q = r o p iso_concat_t. Qed.

  Definition iso_moveL_Vp `(p : morphism C x y) `(q : morphism C x z) `(@IsIsomorphism C _ _ r)
  : (r o q) = p -> q = (r^-1 o p).C: PreCategory
x, y: C
p: morphism C x y
z: C
q: morphism C x z
r: morphism C z y
H: IsIsomorphism r
r o q = p -> q = r^-1 o p
  Proof.C: PreCategory
x, y: C
p: morphism C x y
z: C
q: morphism C x z
r: morphism C z y
H: IsIsomorphism r
r o q = p -> q = r^-1 o p iso_concat_t. Qed.

  Definition iso_moveL_pV `(@IsIsomorphism C x y p) `(q : morphism C y z) r
  : (q o p) = r -> q = (r o p^-1).C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C y z
r: morphism C x z
q o p = r -> q = r o p^-1
  Proof.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
z: C
q: morphism C y z
r: morphism C x z
q o p = r -> q = r o p^-1 iso_concat_t. Qed.

  Definition iso_moveL_1M `(p : morphism C x y) `(@IsIsomorphism C x y q)
  : p o q^-1 = identity _ -> p = q.C: PreCategory
x, y: C
p, q: morphism C x y
H: IsIsomorphism q
p o q^-1 = 1 -> p = q
  Proof.C: PreCategory
x, y: C
p, q: morphism C x y
H: IsIsomorphism q
p o q^-1 = 1 -> p = q iso_concat_t. Qed.

  Definition iso_moveL_M1 `(p : morphism C x y) `(@IsIsomorphism C x y q)
  : q^-1 o p = identity _ -> p = q.C: PreCategory
x, y: C
p, q: morphism C x y
H: IsIsomorphism q
q^-1 o p = 1 -> p = q
  Proof.C: PreCategory
x, y: C
p, q: morphism C x y
H: IsIsomorphism q
q^-1 o p = 1 -> p = q iso_concat_t. Qed.

  Definition iso_moveL_1V `(p : morphism C x y) `(@IsIsomorphism C y x q)
  : p o q = identity _ -> p = q^-1.C: PreCategory
x, y: C
p: morphism C x y
q: morphism C y x
H: IsIsomorphism q
p o q = 1 -> p = q^-1
  Proof.C: PreCategory
x, y: C
p: morphism C x y
q: morphism C y x
H: IsIsomorphism q
p o q = 1 -> p = q^-1 iso_concat_t. Qed.

  Definition iso_moveL_V1 `(p : morphism C x y) `(@IsIsomorphism C y x q)
  : q o p = identity _ -> p = q^-1.C: PreCategory
x, y: C
p: morphism C x y
q: morphism C y x
H: IsIsomorphism q
q o p = 1 -> p = q^-1
  Proof.C: PreCategory
x, y: C
p: morphism C x y
q: morphism C y x
H: IsIsomorphism q
q o p = 1 -> p = q^-1 iso_concat_t. Qed.

  Definition iso_moveR_M1 `(@IsIsomorphism C x y p) q
  : identity _ = p^-1 o q -> p = q.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
q: morphism C x y
1 = p^-1 o q -> p = q
  Proof.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
q: morphism C x y
1 = p^-1 o q -> p = q iso_concat_t. Qed.

  Definition iso_moveR_1M `(@IsIsomorphism C x y p) q
  : identity _ = q o p^-1 -> p = q.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
q: morphism C x y
1 = q o p^-1 -> p = q
  Proof.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
q: morphism C x y
1 = q o p^-1 -> p = q iso_concat_t. Qed.

  Definition iso_moveR_1V `(@IsIsomorphism C x y p) q
  : identity _ = q o p -> p^-1 = q.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
q: morphism C y x
1 = q o p -> p^-1 = q
  Proof.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
q: morphism C y x
1 = q o p -> p^-1 = q iso_concat_t. Qed.

  Definition iso_moveR_V1 `(@IsIsomorphism C x y p) q
  : identity _ = p o q -> p^-1 = q.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
q: morphism C y x
1 = p o q -> p^-1 = q
  Proof.C: PreCategory
x, y: C
p: morphism C x y
H: IsIsomorphism p
q: morphism C y x
1 = p o q -> p^-1 = q iso_concat_t. Qed.
End iso_concat_lemmas.

(** ** Tactics for moving inverses around *)
Ltac iso_move_inverse' :=
  match goal with
    | [ |- _^-1 o _ = _ ] => apply iso_moveR_Vp
    | [ |- _ = _^-1 o _ ] => apply iso_moveL_Vp
    | [ |- _ o _^-1 = _ ] => apply iso_moveR_pV
    | [ |- _ = _ o _^-1 ] => apply iso_moveL_pV
    | [ |- _ o (_ o _^-1) = _ ] => rewrite <- associativity
    | [ |- _ = _ o (_ o _^-1) ] => rewrite <- associativity
    | [ |- (_^-1 o _) o _ = _ ] => rewrite -> associativity
    | [ |- _ = (_^-1 o _) o _ ] => rewrite -> associativity
  end.

Ltac iso_move_inverse := progress repeat iso_move_inverse'.

(** ** Tactics for collapsing [p ∘ p⁻¹] and [p⁻¹ ∘ p] *)
(** Now the tactics for collapsing [p ∘ p⁻¹] (and [p⁻¹ ∘ p]) in the
    middle of a chain of compositions of isomorphisms. *)

Ltac iso_collapse_inverse_left' :=
  first [ apply ap
        | progress rewrite ?iso_compose_p_Vp, ?iso_compose_V_pp ].

Ltac iso_collapse_inverse_left :=
  rewrite -> ?Category.Core.associativity;
  progress repeat iso_collapse_inverse_left'.

Ltac iso_collapse_inverse_right' :=
  first [ apply ap10; apply ap
        | progress rewrite ?iso_compose_pV_p, ?iso_compose_pp_V ].

Ltac iso_collapse_inverse_right :=
  rewrite <- ?Category.Core.associativity;
  progress repeat iso_collapse_inverse_right'.

Ltac iso_collapse_inverse :=
  progress repeat first [ iso_collapse_inverse_left
                        | iso_collapse_inverse_right ].

Section associativity_composition.
  Variable C : PreCategory.
  Variables x0 x1 x2 x3 x4 : C.

  (** This lemma is helpful for backwards reasoning. *)
  Lemma compose4associativity_helper
    (a : morphism C x3 x4) (b : morphism C x2 x3)
    (c : morphism C x1 x2) (d : morphism C x0 x1)
  : a o b o c o d = (a o ((b o c) o d)).C: PreCategory
x0, x1, x2, x3, x4: C
a: morphism C x3 x4
b: morphism C x2 x3
c: morphism C x1 x2
d: morphism C x0 x1
a o b o c o d = a o (b o c o d)
  Proof.C: PreCategory
x0, x1, x2, x3, x4: C
a: morphism C x3 x4
b: morphism C x2 x3
c: morphism C x1 x2
d: morphism C x0 x1
a o b o c o d = a o (b o c o d)
    rewrite !associativity; reflexivity.
  Qed.
End associativity_composition.

Module Export CategoryMorphismsNotations.
  Notation "m ^-1" := (morphism_inverse m) : morphism_scope.

  Infix "<~=~>" := Isomorphic : category_scope.

  Notation "x ->> y" := (Epimorphism x y).
  Notation "x (-> y" := (Monomorphism x y).
End CategoryMorphismsNotations.