(** * Lifting saturation from categories to sigma/subcategories *)
Require Import Category.Core Category.Morphisms.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Category.Univalent.
Require Import Category.Sigma.Core Category.Sigma.OnObjects Category.Sigma.OnMorphisms.
Require Import HoTT.Types HoTT.Basics.

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

Local Notation pr1_type := Overture.pr1 (only parsing).

Local Open Scope path_scope.
Local Open Scope morphism_scope.

Local Open Scope function_scope.

(** TODO: Following a comment from Mike Shulman
    (https://github.com/HoTT/HoTT/pull/670##issuecomment-68907833),
    much of this can probably be subsumed by a general theorem proving
    that univalence lifts along suitable pseudomonic functors
    (http://ncatlab.org/nlab/show/pseudomonic+functor). *)

(** ** Lift saturation to sigma on objects whenever the property is an hProp *)
Section onobjects.
  Variable A : PreCategory.
  Variable Pobj : A -> Type.

  #[export] Instance iscategory_sig_obj `{forall a, IsHProp (Pobj a), A_cat : IsCategory A}
  : IsCategory (sig_obj A Pobj).
A: PreCategory
Pobj: A -> Type
H: forall a : A, IsHProp (Pobj a)
A_cat: IsCategory A
IsCategory {x : A | Pobj x}
  Proof.
A: PreCategory
Pobj: A -> Type
H: forall a : A, IsHProp (Pobj a)
A_cat: IsCategory A
IsCategory {x : A | Pobj x}
    intros s d.
A: PreCategory
Pobj: A -> Type
H: forall a : A, IsHProp (Pobj a)
A_cat: IsCategory A
s, d: {x : A | Pobj x}%category
IsEquiv (idtoiso {x : A | Pobj x} (y:=d))
    (* This makes typeclass search go faster. *)
    pose @isequiv_compose.
A: PreCategory
Pobj: A -> Type
H: forall a : A, IsHProp (Pobj a)
A_cat: IsCategory A
s, d: {x : A | Pobj x}%category
i:= @isequiv_compose: forall (A B C : Type) (f : A -> B),
IsEquiv f ->
forall g : B -> C, IsEquiv g -> IsEquiv (g o f)
IsEquiv (idtoiso {x : A | Pobj x} (y:=d))
    refine (isequiv_homotopic
              ((issig_full_isomorphic (sig_obj A Pobj) _ _ o (issig_full_isomorphic A _ _)^-1)
                 o (@idtoiso A s.1 d.1)
                 o pr1_path)
              _).
A: PreCategory
Pobj: A -> Type
H: forall a : A, IsHProp (Pobj a)
A_cat: IsCategory A
s, d: {x : A | Pobj x}%category
i:= @isequiv_compose: forall (A B C : Type) (f : A -> B),
IsEquiv f ->
forall g : B -> C, IsEquiv g -> IsEquiv (g o f)
(fun x : s = d =>
 issig_full_isomorphic {x : A | Pobj x} s d
   ((issig_full_isomorphic A s.1 d.1)^-1
      (idtoiso A x ..1))) ==
idtoiso {x : A | Pobj x} (y:=d)
    intro x; destruct x.
A: PreCategory
Pobj: A -> Type
H: forall a : A, IsHProp (Pobj a)
A_cat: IsCategory A
s: {x : A | Pobj x}%category
i:= @isequiv_compose: forall (A B C : Type) (f : A -> B),
IsEquiv f ->
forall g : B -> C, IsEquiv g -> IsEquiv (g o f)
issig_full_isomorphic {x : A | Pobj x} s s
  ((issig_full_isomorphic A s.1 s.1)^-1
     (idtoiso A 1 ..1)) = idtoiso {x : A | Pobj x} 1
    reflexivity.
  Defined.

  (** The converse is not true; consider [Pobj := fun _ => Empty]. *)
End onobjects.

(** ** Lift saturation to sigma on objects whenever the property is automatically and uniquely true of isomorphisms *)
Section onmorphisms.
  Variable A : PreCategory.
  Variable Pmor : forall s d, morphism A s d -> Type.

  Local Notation mor s d := { m : _ | Pmor s d m }.
  Context `(HPmor : forall s d, IsHSet (mor s d)).

  Variable Pidentity : forall x, @Pmor x x (@identity A _).
  Variable Pcompose : forall s d d' m1 m2,
                        @Pmor d d' m1
                        -> @Pmor s d m2
                        -> @Pmor s d' (m1 o m2).

  Local Notation identity x := (@identity A x; @Pidentity x).
  Local Notation compose m1 m2 := (m1.1 o m2.1; @Pcompose _ _ _ m1.1 m2.1 m1.2 m2.2)%morphism.

  Hypothesis P_associativity
  : forall x1 x2 x3 x4 (m1 : mor x1 x2) (m2 : mor x2 x3) (m3 : mor x3 x4),
      compose (compose m3 m2) m1 = compose m3 (compose m2 m1).

  Hypothesis P_left_identity
  : forall a b (f : mor a b),
      compose (identity b) f = f.

  Hypothesis P_right_identity
  : forall a b (f : mor a b),
      compose f (identity a) = f.

  Local Notation A' := (@sig_mor' A Pmor HPmor Pidentity Pcompose P_associativity P_left_identity P_right_identity).

  (** To have any hope of relating [IsCategory A] with [IsCategory
      A'], we assume that [Pmor] is automatically and uniquely true on
      isomorphisms. *)
  Context `{forall s d m, IsIsomorphism m -> Contr (Pmor s d m)}.

  Definition iscategory_sig_mor_helper {s d}
  : @Isomorphic A' s d -> @Isomorphic A s d.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
(s <~=~> d)%category -> (s <~=~> d)%category
  Proof.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
(s <~=~> d)%category -> (s <~=~> d)%category
    refine ((issig_full_isomorphic A _ _) o _ o (issig_full_isomorphic A' _ _)^-1).
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
{m : morphism A' s d &
{inverse : morphism A' d s &
{_ : (inverse o m)%morphism = 1 &
(m o inverse)%morphism = 1}}} ->
{m : morphism A s d &
{inverse : morphism A d s &
{_ : (inverse o m)%morphism = 1 &
(m o inverse)%morphism = 1}}}
    exact (functor_sigma
             pr1_type
             (fun _ =>
                functor_sigma
                  pr1_type
                  (fun _ =>
                     functor_sigma
                       pr1_path
                       (fun _ => pr1_path)))).
  Defined.

  Local Instance isequiv_iscategory_sig_mor_helper s d
  : IsEquiv (@iscategory_sig_mor_helper s d).
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
IsEquiv iscategory_sig_mor_helper
  Proof.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
IsEquiv iscategory_sig_mor_helper
    simple refine (isequiv_adjointify _ _ _ _).
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
(s <~=~> d)%category -> (s <~=~> d)%category
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
iscategory_sig_mor_helper o ?g == idmap
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
?g o iscategory_sig_mor_helper == idmap
    {
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
(s <~=~> d)%category -> (s <~=~> d)%category intro e.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
e: (s <~=~> d)%category
(s <~=~> d)%category
      exists (e : morphism _ _ _; center _).
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
e: (s <~=~> d)%category
IsIsomorphism (e; center (Pmor s d e))
      exists (e^-1%morphism; center _);
        simple refine (path_sigma _ _ _ _ _);
        first [ apply left_inverse
              | apply right_inverse
              | by apply path_ishprop ]. }
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
iscategory_sig_mor_helper
o (fun e : (s <~=~> d)%category =>
   {|
     morphism_isomorphic := (e; center (Pmor s d e));
     isisomorphism_isomorphic :=
       {|
         morphism_inverse :=
           (e^-1%morphism; center (Pmor d s e^-1));
         left_inverse :=
           path_sigma (Pmor s s)
             ((e^-1; center (Pmor d s e^-1))
              o (e; center (Pmor s d e)))%morphism 1
             left_inverse
             (path_ishprop
                (transport (Pmor s s) left_inverse
                   (((e^-1; center (Pmor d s e^-1))
                     o (e; center (Pmor s d e)))%morphism).2)
                1.2);
         right_inverse :=
           path_sigma (Pmor d d)
             ((e; center (Pmor s d e))
              o (e^-1; center (Pmor d s e^-1)))%morphism
             1 right_inverse
             (path_ishprop
                (transport (Pmor d d) right_inverse
                   (((e; center (Pmor s d e))
                     o (e^-1; center (Pmor d s e^-1)))%morphism).2)
                1.2)
       |}
   |}) == idmap
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
(fun e : (s <~=~> d)%category =>
 {|
   morphism_isomorphic := (e; center (Pmor s d e));
   isisomorphism_isomorphic :=
     {|
       morphism_inverse :=
         (e^-1%morphism; center (Pmor d s e^-1));
       left_inverse :=
         path_sigma (Pmor s s)
           ((e^-1; center (Pmor d s e^-1))
            o (e; center (Pmor s d e)))%morphism 1
           left_inverse
           (path_ishprop
              (transport 
                 (Pmor s s) left_inverse
                 (((e^-1; center (Pmor d s e^-1))
                   o (e; center (Pmor s d e)))%morphism).2)
              1.2);
       right_inverse :=
         path_sigma (Pmor d d)
           ((e; center (Pmor s d e))
            o (e^-1; center (Pmor d s e^-1)))%morphism
           1 right_inverse
           (path_ishprop
              (transport 
                 (Pmor d d) right_inverse
                 (((e; center (Pmor s d e))
                   o (e^-1; center (Pmor d s e^-1)))%morphism).2)
              1.2)
     |}
 |}) o iscategory_sig_mor_helper == idmap
    {
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
iscategory_sig_mor_helper
o (fun e : (s <~=~> d)%category =>
   {|
     morphism_isomorphic := (e; center (Pmor s d e));
     isisomorphism_isomorphic :=
       {|
         morphism_inverse :=
           (e^-1%morphism; center (Pmor d s e^-1));
         left_inverse :=
           path_sigma (Pmor s s)
             ((e^-1; center (Pmor d s e^-1))
              o (e; center (Pmor s d e)))%morphism 1
             left_inverse
             (path_ishprop
                (transport (Pmor s s) left_inverse
                   (((e^-1; center (Pmor d s e^-1))
                     o (e; center (Pmor s d e)))%morphism).2)
                1.2);
         right_inverse :=
           path_sigma (Pmor d d)
             ((e; center (Pmor s d e))
              o (e^-1; center (Pmor d s e^-1)))%morphism
             1 right_inverse
             (path_ishprop
                (transport (Pmor d d) right_inverse
                   (((e; center (Pmor s d e))
                     o (e^-1; center (Pmor d s e^-1)))%morphism).2)
                1.2)
       |}
   |}) == idmap intro; by apply path_isomorphic. }
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
(fun e : (s <~=~> d)%category =>
 {|
   morphism_isomorphic := (e; center (Pmor s d e));
   isisomorphism_isomorphic :=
     {|
       morphism_inverse :=
         (e^-1%morphism; center (Pmor d s e^-1));
       left_inverse :=
         path_sigma (Pmor s s)
           ((e^-1; center (Pmor d s e^-1))
            o (e; center (Pmor s d e)))%morphism 1
           left_inverse
           (path_ishprop
              (transport (Pmor s s) left_inverse
                 (((e^-1; center (Pmor d s e^-1))
                   o (e; center (Pmor s d e)))%morphism).2)
              1.2);
       right_inverse :=
         path_sigma (Pmor d d)
           ((e; center (Pmor s d e))
            o (e^-1; center (Pmor d s e^-1)))%morphism
           1 right_inverse
           (path_ishprop
              (transport (Pmor d d) right_inverse
                 (((e; center (Pmor s d e))
                   o (e^-1; center (Pmor d s e^-1)))%morphism).2)
              1.2)
     |}
 |}) o iscategory_sig_mor_helper == idmap
    {
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
(fun e : (s <~=~> d)%category =>
 {|
   morphism_isomorphic := (e; center (Pmor s d e));
   isisomorphism_isomorphic :=
     {|
       morphism_inverse :=
         (e^-1%morphism; center (Pmor d s e^-1));
       left_inverse :=
         path_sigma (Pmor s s)
           ((e^-1; center (Pmor d s e^-1))
            o (e; center (Pmor s d e)))%morphism 1
           left_inverse
           (path_ishprop
              (transport (Pmor s s) left_inverse
                 (((e^-1; center (Pmor d s e^-1))
                   o (e; center (Pmor s d e)))%morphism).2)
              1.2);
       right_inverse :=
         path_sigma (Pmor d d)
           ((e; center (Pmor s d e))
            o (e^-1; center (Pmor d s e^-1)))%morphism
           1 right_inverse
           (path_ishprop
              (transport (Pmor d d) right_inverse
                 (((e; center (Pmor s d e))
                   o (e^-1; center (Pmor d s e^-1)))%morphism).2)
              1.2)
     |}
 |}) o iscategory_sig_mor_helper == idmap intros x; apply path_isomorphic.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
s, d: A'
x: (s <~=~> d)%category
{|
  morphism_isomorphic :=
    (iscategory_sig_mor_helper x;
    center (Pmor s d (iscategory_sig_mor_helper x)));
  isisomorphism_isomorphic :=
    {|
      morphism_inverse :=
        ((iscategory_sig_mor_helper x)^-1%morphism;
        center
          (Pmor d s (iscategory_sig_mor_helper x)^-1));
      left_inverse :=
        path_sigma (Pmor s s)
          (((iscategory_sig_mor_helper x)^-1;
           center
             (Pmor d s
                (iscategory_sig_mor_helper x)^-1))
           o (iscategory_sig_mor_helper x;
             center
               (Pmor s d (iscategory_sig_mor_helper x))))%morphism
          1 left_inverse
          (path_ishprop
             (transport (Pmor s s) left_inverse
                ((((iscategory_sig_mor_helper x)^-1;
                  center
                    (Pmor d s
                       (iscategory_sig_mor_helper x)^-1))
                  o (iscategory_sig_mor_helper x;
                    center
                      (Pmor s d
                         (iscategory_sig_mor_helper x))))%morphism).2)
             1.2);
      right_inverse :=
        path_sigma (Pmor d d)
          ((iscategory_sig_mor_helper x;
           center
             (Pmor s d (iscategory_sig_mor_helper x)))
           o ((iscategory_sig_mor_helper x)^-1;
             center
               (Pmor d s
                  (iscategory_sig_mor_helper x)^-1)))%morphism
          1 right_inverse
          (path_ishprop
             (transport (Pmor d d) right_inverse
                (((iscategory_sig_mor_helper x;
                  center
                    (Pmor s d
                       (iscategory_sig_mor_helper x)))
                  o ((iscategory_sig_mor_helper x)^-1;
                    center
                      (Pmor d s
                         (iscategory_sig_mor_helper x)^-1)))%morphism).2)
             1.2)
    |}
|} = x
      exact (path_sigma' _ 1 (contr _)). }
  Defined.

  #[export] Instance iscategory_sig_mor `{A_cat : IsCategory A}
  : IsCategory A'.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
A_cat: IsCategory A
IsCategory A'
  Proof.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
A_cat: IsCategory A
IsCategory A'
    intros s d.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
A_cat: IsCategory A
s, d: A'
IsEquiv (idtoiso A' (y:=d))
    (* Use [equiv_compose] rather than "o" to speed up typeclass search. *)
    refine (isequiv_homotopic
              (equiv_compose iscategory_sig_mor_helper^-1 (@idtoiso _ _ _))
              _).
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
A_cat: IsCategory A
s, d: A'
equiv_compose iscategory_sig_mor_helper^-1
  (idtoiso A (y:=d)) == idtoiso A' (y:=d)
    intro x; apply path_isomorphic; cbn.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
A_cat: IsCategory A
s, d: A'
x: s = d
(idtoiso A x; center (Pmor s d (idtoiso A x))) =
idtoiso A' x
    destruct x; exact (path_sigma' _ 1 (contr _)).
  Defined.

  Definition iscategory_from_sig_mor `{A'_cat : IsCategory A'}
  : IsCategory A.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
A'_cat: IsCategory A'
IsCategory A
  Proof.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
A'_cat: IsCategory A'
IsCategory A
    intros s d.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
A'_cat: IsCategory A'
s, d: A
IsEquiv (idtoiso A (y:=d))
    refine (isequiv_homotopic
              (iscategory_sig_mor_helper
                 o (@idtoiso A' _ _))
              _).
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
A'_cat: IsCategory A'
s, d: A
(fun x : s = d =>
 iscategory_sig_mor_helper (idtoiso A' x)) ==
idtoiso A (y:=d)
    intro x; apply path_isomorphic; cbn.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
A'_cat: IsCategory A'
s, d: A
x: s = d
(idtoiso A' x).1 = idtoiso A x
    destruct x; reflexivity.
  Defined.

  #[export] Instance isequiv_iscategory_sig_mor `{Funext}
  : IsEquiv (@iscategory_sig_mor).
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
H0: Funext
IsEquiv (@iscategory_sig_mor)
  Proof.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: forall (s d : A) (m : morphism A s d),
IsIsomorphism m -> Contr (Pmor s d m)
H0: Funext
IsEquiv (@iscategory_sig_mor)
    exact (isequiv_iff_hprop _ (@iscategory_from_sig_mor)).
  Defined.
End onmorphisms.

(** ** Lift saturation to sigma on both objects and morphisms *)
Section on_both.
  Variable A : PreCategory.
  Variable Pobj : A -> Type.

  Local Notation obj := { x : _ | Pobj x } (only parsing).

  Variable Pmor : forall s d : obj, morphism A s.1 d.1 -> Type.

  Local Notation mor s d := { m : _ | Pmor s d m } (only parsing).
  Context `(HPmor : forall s d, IsHSet (mor s d)).

  Variable Pidentity : forall x, @Pmor x x (@identity A _).
  Variable Pcompose : forall s d d' m1 m2,
                        @Pmor d d' m1
                        -> @Pmor s d m2
                        -> @Pmor s d' (m1 o m2).

  Local Notation identity x := (@identity A x.1; @Pidentity x).
  Local Notation compose m1 m2 := (m1.1 o m2.1; @Pcompose _ _ _ m1.1 m2.1 m1.2 m2.2)%morphism.

  Hypothesis P_associativity
  : forall x1 x2 x3 x4 (m1 : mor x1 x2) (m2 : mor x2 x3) (m3 : mor x3 x4),
      compose (compose m3 m2) m1 = compose m3 (compose m2 m1).

  Hypothesis P_left_identity
  : forall a b (f : mor a b),
      compose (identity b) f = f.

  Hypothesis P_right_identity
  : forall a b (f : mor a b),
      compose f (identity a) = f.

  Local Notation A' := (@sig' A Pobj Pmor HPmor Pidentity Pcompose P_associativity P_left_identity P_right_identity).

  (** We must assume some relation on the properties; we assume that
      the path space of the extra data on objects is classified by
      isomorphisms of the extra data on objects. *)
  Local Definition Pmor_iso_T s d m m' left right :=
    ({ e : Pmor s d m
     | { e' : Pmor d s m'
       | { _ : transport (Pmor _ _) ((left : m' o m = 1)%morphism) (Pcompose e' e) = Pidentity _
         | transport (Pmor _ _) ((right : m o m' = 1)%morphism) (Pcompose e e') = Pidentity _ } } }).

  Global Arguments Pmor_iso_T / .

  Local Definition Pmor_iso_T' x (xp xp' : Pobj x)
    := { e : Pmor (x; xp) (x; xp') 1
       | { e' : Pmor (x; xp') (x; xp) 1
         | { _ : Pcompose e' e = Pcompose (Pidentity _) (Pidentity _)
           | Pcompose e e' = Pcompose (Pidentity _) (Pidentity _) } } }.

  Global Arguments Pmor_iso_T' / .

  Local Definition Pidtoiso x (xp xp' : Pobj x) (H : xp = xp')
  : Pmor_iso_T' xp xp'.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
x: A
xp, xp': Pobj x
H: xp = xp'
Pmor_iso_T' xp xp'
  Proof.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
x: A
xp, xp': Pobj x
H: xp = xp'
Pmor_iso_T' xp xp'
    destruct H.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
x: A
xp: Pobj x
Pmor_iso_T' xp xp
    exists (Pidentity _).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
x: A
xp: Pobj x
{e' : Pmor (x; xp) (x; xp) 1 &
{_
: Pcompose e' (Pidentity (x; xp)) =
  Pcompose (Pidentity (x; xp)) (Pidentity (x; xp)) &
Pcompose (Pidentity (x; xp)) e' =
Pcompose (Pidentity (x; xp)) (Pidentity (x; xp))}}
    exists (Pidentity _).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
x: A
xp: Pobj x
{_
: Pcompose (Pidentity (x; xp)) (Pidentity (x; xp)) =
  Pcompose (Pidentity (x; xp)) (Pidentity (x; xp)) &
Pcompose (Pidentity (x; xp)) (Pidentity (x; xp)) =
Pcompose (Pidentity (x; xp)) (Pidentity (x; xp))}
    split; reflexivity.
  Defined.

  Global Arguments Pidtoiso / .

  (** TODO: generalize this to a theorem [forall A P, IsHSet A -> IsHSet { x : A | P x } -> forall x, IsHSet (P x)], [inO_unsigma] of ##672 *)
  Local Instance ishset_pmor {s d m} : IsHSet (Pmor s d m).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
m: morphism A s.1 d.1
IsHSet (Pmor s d m)
  Proof.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
m: morphism A s.1 d.1
IsHSet (Pmor s d m)
    apply istrunc_S.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
m: morphism A s.1 d.1
is_mere_relation (Pmor s d m) paths
    intros p q.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
m: morphism A s.1 d.1
p, q: Pmor s d m
IsHProp (p = q)
    apply hprop_allpath.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
m: morphism A s.1 d.1
p, q: Pmor s d m
forall x y : p = q, x = y
    let H := constr:(_ : forall x y : mor s d, IsHProp (x = y)) in
    pose proof (@path_ishprop _ (H (m; p) (m; q))) as H'.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
m: morphism A s.1 d.1
p, q: Pmor s d m
H': forall x y : (m; p) = (m; q), x = y
forall x y : p = q, x = y
    intros x y.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
m: morphism A s.1 d.1
p, q: Pmor s d m
H': forall x y : (m; p) = (m; q), x = y
x, y: p = q
x = y
    specialize (H' (path_sigma' _ 1 x) (path_sigma' _ 1 y)).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
m: morphism A s.1 d.1
p, q: Pmor s d m
x, y: p = q
H': path_sigma'
  (fun m : morphism A s.1 d.1 => Pmor s d m) 1 x =
path_sigma'
  (fun m : morphism A s.1 d.1 => Pmor s d m) 1 y
x = y
    unfold path_sigma', path_sigma in H'.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
m: morphism A s.1 d.1
p, q: Pmor s d m
x, y: p = q
H': path_sigma_uncurried
  (fun m : morphism A s.1 d.1 => Pmor s d m)
  (m; p) (m; q) (1%path; x) =
path_sigma_uncurried
  (fun m : morphism A s.1 d.1 => Pmor s d m)
  (m; p) (m; q) (1%path; y)
x = y
    apply (ap (path_sigma_uncurried (Pmor s d) (m; p) (m; q)))^-1 in H'.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
m: morphism A s.1 d.1
p, q: Pmor s d m
x, y: p = q
H': (1%path; x) = (1%path; y)
x = y
    assert (H'' : H'..1 = idpath) by apply path_ishprop.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
m: morphism A s.1 d.1
p, q: Pmor s d m
x, y: p = q
H': (1%path; x) = (1%path; y)
H'': H' ..1 = 1%path
x = y
    exact (transport (fun H'1 => transport _ H'1 _ = _) H'' H'..2).
  Defined.

  Local Definition Pmor_iso_adjust x xp xp'
  : (Pmor_iso_T (x; xp) (x; xp') 1 1 (left_identity _ _ _ _) (right_identity _ _ _ _))
      <~> Pmor_iso_T' xp xp'.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
x: A
xp, xp': (fun x : A => Pobj x) x
Pmor_iso_T (x; xp) (x; xp') 1 1
  (left_identity A (x; xp).1 (x; xp).1 1)
  (right_identity A (x; xp').1 (x; xp').1 1) <~>
Pmor_iso_T' xp xp'
  Proof.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
x: A
xp, xp': (fun x : A => Pobj x) x
Pmor_iso_T (x; xp) (x; xp') 1 1
  (left_identity A (x; xp).1 (x; xp).1 1)
  (right_identity A (x; xp').1 (x; xp').1 1) <~>
Pmor_iso_T' xp xp'
    refine (equiv_functor_sigma_id _); intro.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
x: A
xp, xp': (fun x : A => Pobj x) x
a: Pmor (x; xp) (x; xp') 1
{e' : Pmor (x; xp') (x; xp) 1 &
{_
: transport (Pmor (x; xp) (x; xp))
    (left_identity A (x; xp).1 (x; xp).1 1)
    (Pcompose e' a) = Pidentity (x; xp) &
transport (Pmor (x; xp') (x; xp'))
  (right_identity A (x; xp').1 (x; xp').1 1)
  (Pcompose a e') = Pidentity (x; xp')}} <~>
{e' : Pmor (x; xp') (x; xp) 1 &
{_
: Pcompose e' a =
  Pcompose (Pidentity (x; xp)) (Pidentity (x; xp)) &
Pcompose a e' =
Pcompose (Pidentity (x; xp')) (Pidentity (x; xp'))}}
    refine (equiv_functor_sigma_id _); intro.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
x: A
xp, xp': (fun x : A => Pobj x) x
a: Pmor (x; xp) (x; xp') 1
a0: Pmor (x; xp') (x; xp) 1
{_
: transport (Pmor (x; xp) (x; xp))
    (left_identity A (x; xp).1 (x; xp).1 1)
    (Pcompose a0 a) = Pidentity (x; xp) &
transport (Pmor (x; xp') (x; xp'))
  (right_identity A (x; xp').1 (x; xp').1 1)
  (Pcompose a a0) = Pidentity (x; xp')} <~>
{_
: Pcompose a0 a =
  Pcompose (Pidentity (x; xp)) (Pidentity (x; xp)) &
Pcompose a a0 =
Pcompose (Pidentity (x; xp')) (Pidentity (x; xp'))}
    refine (equiv_functor_sigma' (equiv_iff_hprop _ _) (fun _ => equiv_iff_hprop _ _));
      cbn; intro H';
      first [ apply moveL_transport_V in H'
                | apply moveR_transport_p ];
      refine (H' @ _);
      first [ refine (_ @ ((P_left_identity (identity (x; _)))^)..2)
                | refine ((((P_left_identity (identity (x; _)))^)..2)^ @ _) ];
      exact (ap (fun p => transport _ p _) (path_ishprop _ _)).
  Defined.

  Global Arguments Pmor_iso_adjust / .

  Local Definition iso_A'_code {s d}
  : (@Isomorphic A' s d)
    -> { e : @Isomorphic A s.1 d.1
       | Pmor_iso_T s d e e^-1 (@left_inverse _ _ _ e e) right_inverse }.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
(s <~=~> d)%category ->
{e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
  Proof.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
(s <~=~> d)%category ->
{e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
    intro e.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
{e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
    simple refine (_; _).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
(s.1 <~=~> d.1)%category
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
(fun e : (s.1 <~=~> d.1)%category =>
 Pmor_iso_T s d e e^-1 left_inverse right_inverse)
  ?proj1
    {
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
(s.1 <~=~> d.1)%category exists (e : morphism _ _ _).1.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
IsIsomorphism e.1
      exists (e^-1%morphism).1.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
((e^-1).1 o e.1)%morphism = 1
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
(e.1 o (e^-1).1)%morphism = 1
      -
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
((e^-1).1 o e.1)%morphism = 1 exact (@left_inverse _ _ _ e e)..1.
      -
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
(e.1 o (e^-1).1)%morphism = 1 exact (@right_inverse _ _ _ e e)..1. }
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
(fun e : (s.1 <~=~> d.1)%category =>
 Pmor_iso_T s d e e^-1 left_inverse right_inverse)
  {|
    morphism_isomorphic := e.1;
    isisomorphism_isomorphic :=
      {|
        morphism_inverse := (e^-1%morphism).1;
        left_inverse := left_inverse ..1;
        right_inverse := right_inverse ..1
      |}
  |}
    {
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
(fun e : (s.1 <~=~> d.1)%category =>
 Pmor_iso_T s d e e^-1 left_inverse right_inverse)
  {|
    morphism_isomorphic := e.1;
    isisomorphism_isomorphic :=
      {|
        morphism_inverse := (e^-1%morphism).1;
        left_inverse := left_inverse ..1;
        right_inverse := right_inverse ..1
      |}
  |} exists (e : morphism _ _ _).2.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
{e'
: Pmor d s
    {|
      morphism_isomorphic := e.1;
      isisomorphism_isomorphic :=
        {|
          morphism_inverse := (e^-1%morphism).1;
          left_inverse := left_inverse ..1;
          right_inverse := right_inverse ..1
        |}
    |}^-1 &
{_
: transport (Pmor s s) left_inverse (Pcompose e' e.2) =
  Pidentity s &
transport (Pmor d d) right_inverse (Pcompose e.2 e') =
Pidentity d}}
      exists (e^-1%morphism).2; cbn.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
{_
: transport (Pmor s s) left_inverse ..1
    (Pcompose (e^-1%morphism).2 e.2) = Pidentity s &
transport (Pmor d d) right_inverse ..1
  (Pcompose e.2 (e^-1%morphism).2) = Pidentity d}
      exists (((@left_inverse _ _ _ e e))..2).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
e: (s <~=~> d)%category
transport (Pmor d d) right_inverse ..1
  (Pcompose e.2 (e^-1%morphism).2) = Pidentity d
      exact (@right_inverse _ _ _ e e)..2. }
  Defined.

  Local Definition iso_A'_decode_helper {s d}
        (e : { e : @Isomorphic A s.1 d.1
             | Pmor_iso_T s d e e^-1 (@left_inverse _ _ _ e e) right_inverse })
  : @IsIsomorphism A' _ _ (e.1:morphism A s.1 d.1; (e.2).1).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
IsIsomorphism (e.1 : morphism A s.1 d.1; (e.2).1)
  Proof.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
IsIsomorphism (e.1 : morphism A s.1 d.1; (e.2).1)
    eexists.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
(?morphism_inverse o (e.1; (e.2).1))%morphism = 1
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
((e.1; (e.2).1) o ?morphism_inverse)%morphism = 1 Unshelve.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
(?morphism_inverse o (e.1; (e.2).1))%morphism = 1
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
((e.1; (e.2).1) o ?morphism_inverse)%morphism = 1
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
morphism A' d s
    3:exact (e.1^-1%morphism; e.2.2.1).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
(((e.1)^-1; ((e.2).2).1) o (e.1; (e.2).1))%morphism =
1
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
((e.1; (e.2).1) o ((e.1)^-1; ((e.2).2).1))%morphism =
1
    {
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
(((e.1)^-1; ((e.2).2).1) o (e.1; (e.2).1))%morphism =
1 exact (path_sigma' _ left_inverse e.2.2.2.1). }
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
((e.1; (e.2).1) o ((e.1)^-1; ((e.2).2).1))%morphism =
1
    {
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
((e.1; (e.2).1) o ((e.1)^-1; ((e.2).2).1))%morphism =
1 exact (path_sigma' _ right_inverse e.2.2.2.2). }
  Defined.

  Local Definition iso_A'_decode {s d}
  : { e : @Isomorphic A s.1 d.1
    | Pmor_iso_T s d e e^-1 (@left_inverse _ _ _ e e) right_inverse }
    -> (@Isomorphic A' s d).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
{e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse} ->
(s <~=~> d)%category
  Proof.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
{e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse} ->
(s <~=~> d)%category
    intro e.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
(s <~=~> d)%category
    eexists.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
IsIsomorphism ?morphism_isomorphic Unshelve.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
IsIsomorphism ?morphism_isomorphic
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
morphism A' s d
    2:exact (e.1 : morphism _ _ _; e.2.1).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
e: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
IsIsomorphism (e.1 : morphism A s.1 d.1; (e.2).1)
    apply iso_A'_decode_helper.
  Defined.

  Local Definition equiv_iso_A'_eisretr_helper {s d}
        (x : {e : @Isomorphic A s.1 d.1
             | Pmor_iso_T s d e e^-1 (@left_inverse _ _ _ e e) right_inverse })
  : transport
      (fun e : @Isomorphic A s.1 d.1 =>
         Pmor_iso_T s d e e^-1 left_inverse right_inverse)
      (path_isomorphic (iso_A'_code (iso_A'_decode x)).1 x.1 1)
      (iso_A'_code (iso_A'_decode x)).2 = x.2.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
transport
  (fun e : (s.1 <~=~> d.1)%category =>
   Pmor_iso_T s d e e^-1 left_inverse right_inverse)
  (path_isomorphic (iso_A'_code (iso_A'_decode x)).1
     x.1 1) (iso_A'_code (iso_A'_decode x)).2 = x.2
  Proof.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
transport
  (fun e : (s.1 <~=~> d.1)%category =>
   Pmor_iso_T s d e e^-1 left_inverse right_inverse)
  (path_isomorphic (iso_A'_code (iso_A'_decode x)).1
     x.1 1) (iso_A'_code (iso_A'_decode x)).2 = x.2
    simple refine (path_sigma _ _ _ _ _); cycle 1.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
transport
  (fun e : Pmor s d x.1 =>
   {e' : Pmor d s (x.1)^-1 &
   {_
   : transport (Pmor s s)
       (left_inverse : ((x.1)^-1 o x.1)%morphism = 1)
       (Pcompose e' e) = Pidentity s &
   transport (Pmor d d)
     (right_inverse : (x.1 o (x.1)^-1)%morphism = 1)
     (Pcompose e e') = Pidentity d}}) ?p
  (transport
     (fun e : (s.1 <~=~> d.1)%category =>
      Pmor_iso_T s d e e^-1 left_inverse right_inverse)
     (path_isomorphic
        (iso_A'_code (iso_A'_decode x)).1 x.1 1)
     (iso_A'_code (iso_A'_decode x)).2).2 = (x.2).2
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
(transport
   (fun e : (s.1 <~=~> d.1)%category =>
    Pmor_iso_T s d e e^-1 left_inverse right_inverse)
   (path_isomorphic (iso_A'_code (iso_A'_decode x)).1
      x.1 1) (iso_A'_code (iso_A'_decode x)).2).1 =
(x.2).1
    (* Speed up typeclass search: *)
    1:pose @istrunc_sigma; pose @istrunc_paths;
      simple refine (path_sigma _ _ _ _ (path_ishprop _ _)).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
i:= @istrunc_sigma: forall (A : Type) (P : A -> Type)
(n : trunc_index),
IsTrunc n A ->
(forall a : A, IsTrunc n (P a)) ->
IsTrunc n {x : _ & P x}
i0:= istrunc_paths: forall (A : Type) (n : trunc_index),
IsTrunc n.+1 A ->
forall x y : A, IsTrunc n (x = y)
(transport
   (fun e : Pmor s d x.1 =>
    {e' : Pmor d s (x.1)^-1 &
    {_
    : transport (Pmor s s)
        (left_inverse : ((x.1)^-1 o x.1)%morphism = 1)
        (Pcompose e' e) = Pidentity s &
    transport (Pmor d d)
      (right_inverse : (x.1 o (x.1)^-1)%morphism = 1)
      (Pcompose e e') = Pidentity d}}) ?p
   (transport
      (fun e : (s.1 <~=~> d.1)%category =>
       Pmor_iso_T s d e e^-1 left_inverse
         right_inverse)
      (path_isomorphic
         (iso_A'_code (iso_A'_decode x)).1 x.1 1)
      (iso_A'_code (iso_A'_decode x)).2).2).1 =
((x.2).2).1
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: {x : A & Pobj x}
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
(transport
   (fun e : (s.1 <~=~> d.1)%category =>
    Pmor_iso_T s d e e^-1 left_inverse right_inverse)
   (path_isomorphic (iso_A'_code (iso_A'_decode x)).1
      x.1 1) (iso_A'_code (iso_A'_decode x)).2).1 =
(x.2).1
    all:repeat match goal with
                 | [ |- (transport ?P ?p ?z).1 = _ ] => rewrite (@ap_transport _ P _ _ _ p (fun _ x => x.1))
                 | [ |- (transport ?P ?p ?z).2.1 = _ ] => rewrite (@ap_transport _ P _ _ _ p (fun _ x => x.2.1))
                 | [ |- transport (fun _ => ?x) _ _ = _ ] => rewrite transport_const
                 | [ |- transport (fun x => ?f (@morphism_inverse _ _ _ (@morphism_isomorphic _ _ _ x) _)) _ _ = _ ]
                   => rewrite (@transport_compose _ _ _ _ f (fun x => (@morphism_inverse _ _ _ (@morphism_isomorphic _ _ _ x) (@isisomorphism_isomorphic _ _ _ x))))
                 | [ |- transport (?f o ?g) _ _ = _ ] => rewrite (@transport_compose _ _ _ _ f g)
                 | [ |- transport (fun x => ?f (?g x)) _ _ = _ ] => rewrite (@transport_compose _ _ _ _ f g)
                 | [ |- context[ap (@morphism_isomorphic ?a ?b ?c) (path_isomorphic ?i ?j ?x)] ]
                   => change (ap (@morphism_isomorphic a b c)) with ((path_isomorphic i j)^-1%function);
                     rewrite (@eissect _ _ (path_isomorphic i j) _ x)
                 | [ |- context[ap (fun e : Isomorphic _ _ => @morphism_inverse ?C ?s ?d _ _) (path_isomorphic ?i ?j ?x)] ]
                   => rewrite (@ap_morphism_inverse_path_isomorphic C s d i j x 1)
                 | [ |- transport ?P 1 ?x = ?y ] => change (x = y)
                 | [ |- (((iso_A'_code (iso_A'_decode ?x)).2).2).1 = ((?x.2).2).1 ] => reflexivity
                 | [ |- (((iso_A'_code (iso_A'_decode ?x)).2).1) = ((?x.2).1) ] => reflexivity
               end.
  Qed.

  Local Definition equiv_iso_A' {s d}
  : (@Isomorphic A' s d)
      <~> { e : @Isomorphic A s.1 d.1
          | Pmor_iso_T s d e e^-1 (@left_inverse _ _ _ e e) right_inverse }.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
(s <~=~> d)%category <~>
{e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
  Proof.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
(s <~=~> d)%category <~>
{e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
    refine (equiv_adjointify iso_A'_code iso_A'_decode _ _).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
(fun
   x : {e : (s.1 <~=~> d.1)%category &
       Pmor_iso_T s d e e^-1 left_inverse
         right_inverse} =>
 iso_A'_code (iso_A'_decode x)) == idmap
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
(fun x : (s <~=~> d)%category =>
 iso_A'_decode (iso_A'_code x)) == idmap
    {
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
(fun
   x : {e : (s.1 <~=~> d.1)%category &
       Pmor_iso_T s d e e^-1 left_inverse
         right_inverse} =>
 iso_A'_code (iso_A'_decode x)) == idmap intro.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
iso_A'_code (iso_A'_decode x) = x
      simple refine (path_sigma _ _ _ _ _).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
(iso_A'_code (iso_A'_decode x)).1 = x.1
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
transport
  (fun e : (s.1 <~=~> d.1)%category =>
   Pmor_iso_T s d e e^-1 left_inverse right_inverse)
  ?p (iso_A'_code (iso_A'_decode x)).2 = x.2
      {
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
(iso_A'_code (iso_A'_decode x)).1 = x.1 apply path_isomorphic; reflexivity. }
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
transport
  (fun e : (s.1 <~=~> d.1)%category =>
   Pmor_iso_T s d e e^-1 left_inverse right_inverse)
  (path_isomorphic (iso_A'_code (iso_A'_decode x)).1
     x.1 1) (iso_A'_code (iso_A'_decode x)).2 = x.2
      {
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
x: {e : (s.1 <~=~> d.1)%category &
Pmor_iso_T s d e e^-1 left_inverse right_inverse}
transport
  (fun e : (s.1 <~=~> d.1)%category =>
   Pmor_iso_T s d e e^-1 left_inverse right_inverse)
  (path_isomorphic (iso_A'_code (iso_A'_decode x)).1
     x.1 1) (iso_A'_code (iso_A'_decode x)).2 = x.2 apply equiv_iso_A'_eisretr_helper. }  }
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
(fun x : (s <~=~> d)%category =>
 iso_A'_decode (iso_A'_code x)) == idmap
    {
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
(fun x : (s <~=~> d)%category =>
 iso_A'_decode (iso_A'_code x)) == idmap intro.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
x: (s <~=~> d)%category
iso_A'_decode (iso_A'_code x) = x
      apply path_isomorphic.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
s, d: A'
x: (s <~=~> d)%category
iso_A'_decode (iso_A'_code x) = x
      reflexivity. }
  Defined.

  Context `{Pisotoid : forall x xp xp', IsEquiv (@Pidtoiso x xp xp')}.

  Local Arguments Pmor_iso_T : simpl never.

  #[export] Instance iscategory_sig `{A_cat : IsCategory A}
  : IsCategory A'.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
IsCategory A'
  Proof.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
IsCategory A'
    intros s d.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv (idtoiso A' (y:=d))
    snrefine (isequiv_homotopic
              ((equiv_iso_A'^-1)
                 o (functor_sigma _ _)
                 o (path_sigma_uncurried _ _ _)^-1)
              _); [exact _ | | | exact _ | |].
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
s.1 = d.1 -> (s.1 <~=~> d.1)%category
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
forall a : s.1 = d.1,
(fun p : s.1 = d.1 => transport Pobj p s.2 = d.2) a ->
(fun e : (s.1 <~=~> d.1)%category =>
 Pmor_iso_T s d e e^-1 left_inverse right_inverse)
  (?f a)
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv
  (equiv_iso_A'^-1 o functor_sigma ?f ?g
   o (path_sigma_uncurried Pobj s d)^-1)
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
equiv_iso_A'^-1 o functor_sigma ?f ?g
o (path_sigma_uncurried Pobj s d)^-1 ==
idtoiso A' (y:=d)
    (* [try exact _] leaves the third remaining goal unchanged, but takes ~9s to do so. *)
    {
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
s.1 = d.1 -> (s.1 <~=~> d.1)%category exact (@idtoiso A _ _). }
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
forall a : s.1 = d.1,
(fun p : s.1 = d.1 => transport Pobj p s.2 = d.2) a ->
(fun e : (s.1 <~=~> d.1)%category =>
 Pmor_iso_T s d e e^-1 left_inverse right_inverse)
  (idtoiso A a)
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv
  (equiv_iso_A'^-1
   o functor_sigma (idtoiso A (y:=d.1)) ?g
   o (path_sigma_uncurried Pobj s d)^-1)
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
equiv_iso_A'^-1
o functor_sigma (idtoiso A (y:=d.1)) ?g
o (path_sigma_uncurried Pobj s d)^-1 ==
idtoiso A' (y:=d)
    {
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
forall a : s.1 = d.1,
(fun p : s.1 = d.1 => transport Pobj p s.2 = d.2) a ->
(fun e : (s.1 <~=~> d.1)%category =>
 Pmor_iso_T s d e e^-1 left_inverse right_inverse)
  (idtoiso A a) destruct s as [s0 s1], d as [d0 d1]; cbn.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s0: A
s1: Pobj s0
d0: A
d1: Pobj d0
forall a : s0 = d0,
transport Pobj a s1 = d1 ->
Pmor_iso_T (s0; s1) (d0; d1) (idtoiso A a)
  (idtoiso A a)^-1 left_inverse right_inverse
      intro p; destruct p; cbn.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s0: A
s1, d1: Pobj s0
s1 = d1 ->
Pmor_iso_T (s0; s1) (s0; d1) 1 1
  (left_identity A s0 s0 1) (right_identity A s0 s0 1)
      refine ((@Pmor_iso_adjust s0 s1 d1)^-1 o _).
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s0: A
s1, d1: Pobj s0
s1 = d1 -> Pmor_iso_T' s1 d1
      exact (@Pidtoiso _ _ _). }
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv
  (equiv_iso_A'^-1
   o functor_sigma (idtoiso A (y:=d.1))
       ((fun (s0 : A) (s1 : Pobj s0) =>
         (fun (d0 : A) (d1 : Pobj d0) =>
          (fun p : s0 = d0 =>
           match
             p as p0 in (_ = o)
             return
               (forall d2 : Pobj o,
                transport Pobj p0 s1 = d2 ->
                Pmor_iso_T (s0; s1) (o; d2)
                  (idtoiso A p0) (idtoiso A p0)^-1
                  left_inverse right_inverse)
           with
           | 1%path =>
               fun d2 : Pobj s0 =>
               (Pmor_iso_adjust s1 d2)^-1
               o Pidtoiso (xp':=d2)
               :
               transport Pobj 1 s1 = d2 ->
               Pmor_iso_T (s0; s1) (s0; d2)
                 (idtoiso A 1) (idtoiso A 1)^-1
                 left_inverse right_inverse
           end d1)
          :
          forall a : (s0; s1).1 = (d0; d1).1,
          transport Pobj a (s0; s1).2 = (d0; d1).2 ->
          Pmor_iso_T (s0; s1) (d0; d1) (idtoiso A a)
            (idtoiso A a)^-1 left_inverse
            right_inverse) d.1 d.2) s.1 s.2)
   o (path_sigma_uncurried Pobj s d)^-1)
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
equiv_iso_A'^-1
o functor_sigma (idtoiso A (y:=d.1))
    ((fun (s0 : A) (s1 : Pobj s0) =>
      (fun (d0 : A) (d1 : Pobj d0) =>
       (fun p : s0 = d0 =>
        match
          p as p0 in (_ = o)
          return
            (forall d2 : Pobj o,
             transport Pobj p0 s1 = d2 ->
             Pmor_iso_T (s0; s1) 
               (o; d2) (idtoiso A p0)
               (idtoiso A p0)^-1 left_inverse
               right_inverse)
        with
        | 1%path =>
            fun d2 : Pobj s0 =>
            (Pmor_iso_adjust s1 d2)^-1
            o Pidtoiso (xp':=d2)
            :
            transport Pobj 1 s1 = d2 ->
            Pmor_iso_T (s0; s1) 
              (s0; d2) (idtoiso A 1) 
              (idtoiso A 1)^-1 left_inverse
              right_inverse
        end d1)
       :
       forall a : (s0; s1).1 = (d0; d1).1,
       transport Pobj a (s0; s1).2 = (d0; d1).2 ->
       Pmor_iso_T (s0; s1) 
         (d0; d1) (idtoiso A a) 
         (idtoiso A a)^-1 left_inverse right_inverse)
        d.1 d.2) s.1 s.2)
o (path_sigma_uncurried Pobj s d)^-1 ==
idtoiso A' (y:=d)
    { (* Do this in small steps to make it fast. *)
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv
  (equiv_iso_A'^-1
   o functor_sigma (idtoiso A (y:=d.1))
       ((fun (s0 : A) (s1 : Pobj s0) =>
         (fun (d0 : A) (d1 : Pobj d0) =>
          (fun p : s0 = d0 =>
           match
             p as p0 in (_ = o)
             return
               (forall d2 : Pobj o,
                transport Pobj p0 s1 = d2 ->
                Pmor_iso_T (s0; s1) (o; d2)
                  (idtoiso A p0) (idtoiso A p0)^-1
                  left_inverse right_inverse)
           with
           | 1%path =>
               fun d2 : Pobj s0 =>
               (Pmor_iso_adjust s1 d2)^-1
               o Pidtoiso (xp':=d2)
               :
               transport Pobj 1 s1 = d2 ->
               Pmor_iso_T (s0; s1) (s0; d2)
                 (idtoiso A 1) (idtoiso A 1)^-1
                 left_inverse right_inverse
           end d1)
          :
          forall a : (s0; s1).1 = (d0; d1).1,
          transport Pobj a (s0; s1).2 = (d0; d1).2 ->
          Pmor_iso_T (s0; s1) (d0; d1) (idtoiso A a)
            (idtoiso A a)^-1 left_inverse
            right_inverse) d.1 d.2) s.1 s.2)
   o (path_sigma_uncurried Pobj s d)^-1)
      napply isequiv_compose.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv (path_sigma_uncurried Pobj s d)^-1
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv
  (fun
     x : {p : s.1 = d.1 & transport Pobj p s.2 = d.2}
   =>
   equiv_iso_A'^-1
     (functor_sigma (idtoiso A (y:=d.1))
        (fun p : s.1 = d.1 =>
         match
           p as p0 in (_ = o)
           return
             (forall d1 : Pobj o,
              transport Pobj p0 s.2 = d1 ->
              Pmor_iso_T 
                (s.1; s.2) 
                (o; d1) (idtoiso A p0)
                (idtoiso A p0)^-1 left_inverse
                right_inverse)
         with
         | 1%path =>
             fun (d1 : Pobj s.1) (x0 : s.2 = d1) =>
             (Pmor_iso_adjust s.2 d1)^-1 (Pidtoiso x0)
         end d.2) x)) 1:apply isequiv_inverse.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv
  (fun
     x : {p : s.1 = d.1 & transport Pobj p s.2 = d.2}
   =>
   equiv_iso_A'^-1
     (functor_sigma (idtoiso A (y:=d.1))
        (fun p : s.1 = d.1 =>
         match
           p as p0 in (_ = o)
           return
             (forall d1 : Pobj o,
              transport Pobj p0 s.2 = d1 ->
              Pmor_iso_T (s.1; s.2) (o; d1)
                (idtoiso A p0) (idtoiso A p0)^-1
                left_inverse right_inverse)
         with
         | 1%path =>
             fun (d1 : Pobj s.1) (x0 : s.2 = d1) =>
             (Pmor_iso_adjust s.2 d1)^-1 (Pidtoiso x0)
         end d.2) x))
      napply isequiv_compose.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv
  (functor_sigma (idtoiso A (y:=d.1))
     (fun p : s.1 = d.1 =>
      match
        p as p0 in (_ = o)
        return
          (forall d1 : Pobj o,
           transport Pobj p0 s.2 = d1 ->
           Pmor_iso_T (s.1; s.2) (o; d1)
             (idtoiso A p0) (idtoiso A p0)^-1
             left_inverse right_inverse)
      with
      | 1%path =>
          fun (d1 : Pobj s.1) (x : s.2 = d1) =>
          (Pmor_iso_adjust s.2 d1)^-1 (Pidtoiso x)
      end d.2))
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv equiv_iso_A'^-1 2:apply isequiv_inverse.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv
  (functor_sigma (idtoiso A (y:=d.1))
     (fun p : s.1 = d.1 =>
      match
        p as p0 in (_ = o)
        return
          (forall d1 : Pobj o,
           transport Pobj p0 s.2 = d1 ->
           Pmor_iso_T (s.1; s.2) (o; d1)
             (idtoiso A p0) (idtoiso A p0)^-1
             left_inverse right_inverse)
      with
      | 1%path =>
          fun (d1 : Pobj s.1) (x : s.2 = d1) =>
          (Pmor_iso_adjust s.2 d1)^-1 (Pidtoiso x)
      end d.2))
      nrefine isequiv_functor_sigma.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
IsEquiv (idtoiso A (y:=d.1))
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
forall a : s.1 = d.1,
IsEquiv
  (match
     a as p in (_ = o)
     return
       (forall d1 : Pobj o,
        transport Pobj p s.2 = d1 ->
        Pmor_iso_T (s.1; s.2) 
          (o; d1) (idtoiso A p) 
          (idtoiso A p)^-1 left_inverse right_inverse)
   with
   | 1%path =>
       fun (d1 : Pobj s.1) (x : s.2 = d1) =>
       (Pmor_iso_adjust s.2 d1)^-1 (Pidtoiso x)
   end d.2) 1:apply A_cat.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
forall a : s.1 = d.1,
IsEquiv
  (match
     a as p in (_ = o)
     return
       (forall d1 : Pobj o,
        transport Pobj p s.2 = d1 ->
        Pmor_iso_T (s.1; s.2) (o; d1) (idtoiso A p)
          (idtoiso A p)^-1 left_inverse right_inverse)
   with
   | 1%path =>
       fun (d1 : Pobj s.1) (x : s.2 = d1) =>
       (Pmor_iso_adjust s.2 d1)^-1 (Pidtoiso x)
   end d.2)
      destruct s, d.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
proj1: A
proj2: Pobj proj1
proj0: A
proj3: Pobj proj0
forall a : (proj1; proj2).1 = (proj0; proj3).1,
IsEquiv
  (match
     a as p in (_ = o)
     return
       (forall d1 : Pobj o,
        transport Pobj p proj2 = d1 ->
        Pmor_iso_T (proj1; proj2) (o; d1)
          (idtoiso A p) (idtoiso A p)^-1 left_inverse
          right_inverse)
   with
   | 1%path =>
       fun (d1 : Pobj proj1) (x : proj2 = d1) =>
       (Pmor_iso_adjust proj2 d1)^-1 (Pidtoiso x)
   end proj3)
      simpl Overture.pr1.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
proj1: A
proj2: Pobj proj1
proj0: A
proj3: Pobj proj0
forall a : proj1 = proj0,
IsEquiv
  (match
     a as p in (_ = o)
     return
       (forall d1 : Pobj o,
        transport Pobj p proj2 = d1 ->
        Pmor_iso_T (proj1; proj2) (o; d1)
          (idtoiso A p) (idtoiso A p)^-1 left_inverse
          right_inverse)
   with
   | 1%path =>
       fun (d1 : Pobj proj1) (x : proj2 = d1) =>
       (Pmor_iso_adjust proj2 d1)^-1 (Pidtoiso x)
   end proj3)
      intro p; destruct p.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
proj1: A
proj2, proj3: Pobj proj1
IsEquiv
  (fun x : proj2 = proj3 =>
   (Pmor_iso_adjust proj2 proj3)^-1 (Pidtoiso x))
      eapply isequiv_compose.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
proj1: A
proj2, proj3: Pobj proj1
IsEquiv (Pidtoiso (xp':=proj3))
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
proj1: A
proj2, proj3: Pobj proj1
IsEquiv (Pmor_iso_adjust proj2 proj3)^-1
      -
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
proj1: A
proj2, proj3: Pobj proj1
IsEquiv (Pidtoiso (xp':=proj3)) exact _.
      -
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
proj1: A
proj2, proj3: Pobj proj1
IsEquiv (Pmor_iso_adjust proj2 proj3)^-1 eapply @isequiv_inverse. }
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
equiv_iso_A'^-1
o functor_sigma (idtoiso A (y:=d.1))
    ((fun (s0 : A) (s1 : Pobj s0) =>
      (fun (d0 : A) (d1 : Pobj d0) =>
       (fun p : s0 = d0 =>
        match
          p as p0 in (_ = o)
          return
            (forall d2 : Pobj o,
             transport Pobj p0 s1 = d2 ->
             Pmor_iso_T (s0; s1) (o; d2)
               (idtoiso A p0) (idtoiso A p0)^-1
               left_inverse right_inverse)
        with
        | 1%path =>
            fun d2 : Pobj s0 =>
            (Pmor_iso_adjust s1 d2)^-1
            o Pidtoiso (xp':=d2)
            :
            transport Pobj 1 s1 = d2 ->
            Pmor_iso_T (s0; s1) (s0; d2) (idtoiso A 1)
              (idtoiso A 1)^-1 left_inverse
              right_inverse
        end d1)
       :
       forall a : (s0; s1).1 = (d0; d1).1,
       transport Pobj a (s0; s1).2 = (d0; d1).2 ->
       Pmor_iso_T (s0; s1) (d0; d1) (idtoiso A a)
         (idtoiso A a)^-1 left_inverse right_inverse)
        d.1 d.2) s.1 s.2)
o (path_sigma_uncurried Pobj s d)^-1 ==
idtoiso A' (y:=d)
    {
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s, d: A'
equiv_iso_A'^-1
o functor_sigma (idtoiso A (y:=d.1))
    ((fun (s0 : A) (s1 : Pobj s0) =>
      (fun (d0 : A) (d1 : Pobj d0) =>
       (fun p : s0 = d0 =>
        match
          p as p0 in (_ = o)
          return
            (forall d2 : Pobj o,
             transport Pobj p0 s1 = d2 ->
             Pmor_iso_T (s0; s1) (o; d2)
               (idtoiso A p0) (idtoiso A p0)^-1
               left_inverse right_inverse)
        with
        | 1%path =>
            fun d2 : Pobj s0 =>
            (Pmor_iso_adjust s1 d2)^-1
            o Pidtoiso (xp':=d2)
            :
            transport Pobj 1 s1 = d2 ->
            Pmor_iso_T (s0; s1) (s0; d2) (idtoiso A 1)
              (idtoiso A 1)^-1 left_inverse
              right_inverse
        end d1)
       :
       forall a : (s0; s1).1 = (d0; d1).1,
       transport Pobj a (s0; s1).2 = (d0; d1).2 ->
       Pmor_iso_T (s0; s1) (d0; d1) (idtoiso A a)
         (idtoiso A a)^-1 left_inverse right_inverse)
        d.1 d.2) s.1 s.2)
o (path_sigma_uncurried Pobj s d)^-1 ==
idtoiso A' (y:=d) intro p; apply path_isomorphic; destruct p.
A: PreCategory
Pobj: A -> Type
Pmor: forall s d : {x : A & Pobj x},
morphism A s.1 d.1 -> Type
HPmor: forall s d : {x : A & Pobj x},
IsHSet {m : morphism A s.1 d.1 & Pmor s d m}
Pidentity: forall x : {x : A & Pobj x}, Pmor x x 1
Pcompose: forall (s d d' : {x : A & Pobj x})
(m1 : morphism A d.1 d'.1)
(m2 : morphism A s.1 d.1),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall
(x1 x2 x3 x4 : {x : A & Pobj x})
(m1 : {m : morphism A x1.1 x2.1 &
      Pmor x1 x2 m})
(m2 : {m : morphism A x2.1 x3.1 &
      Pmor x2 x3 m})
(m3 : {m : morphism A x3.1 x4.1 &
      Pmor x3 x4 m}),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose (identity b) f = f
P_right_identity: forall (a b : {x : A & Pobj x})
(f : {m : morphism A a.1 b.1 &
     Pmor a b m}),
compose f (identity a) = f
Pisotoid: forall (x : A) (xp xp' : Pobj x),
IsEquiv (Pidtoiso (xp':=xp'))
A_cat: IsCategory A
s: A'
equiv_iso_A'^-1
  (functor_sigma (idtoiso A (y:=s.1))
     (fun p : s.1 = s.1 =>
      match
        p as p0 in (_ = o)
        return
          (forall d1 : Pobj o,
           transport Pobj p0 s.2 = d1 ->
           Pmor_iso_T (s.1; s.2) (o; d1)
             (idtoiso A p0) (idtoiso A p0)^-1
             left_inverse right_inverse)
      with
      | 1%path =>
          fun (d1 : Pobj s.1) (x : s.2 = d1) =>
          (Pmor_iso_adjust s.2 d1)^-1 (Pidtoiso x)
      end s.2)
     ((path_sigma_uncurried Pobj s s)^-1 1%path)) =
idtoiso A' 1
      reflexivity. }
  Defined.
End on_both.