From HoTT Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Homotopy.IdentitySystems.
From HoTT.WildCat Require Import Core PointedCat TwoOneCat NatTrans
  Universe Products Equiv Yoneda.
Require Import Truncations.Core.
Require Import ReflectiveSubuniverse.
Require Import Extensions.

Local Set Polymorphic Inductive Cumulativity.

Declare Scope pointed_scope.

Local Open Scope pointed_scope.
Local Open Scope path_scope.

Generalizable Variables A B f.

(** ** Pointed Types *)

Notation "'pt'" := (point _) : pointed_scope.
Notation "[ X , x ]" := (Build_pType X x) : pointed_scope.

(** The unit type is pointed *)
Instance ispointed_unit : IsPointed Unit := tt.

(** The Unit [pType] *)
Definition pUnit : pType := [Unit, tt].

(** A sigma type of pointed components is pointed. *)
Instance ispointed_sigma `{IsPointed A} `{IsPointed (B (point A))}
: IsPointed (sig B)
  := (point A; point (B (point A))).

(** A product of pointed types is pointed. *)
Instance ispointed_prod `{IsPointed A, IsPointed B} : IsPointed (A * B)
  := (point A, point B).

(** We override the notation for products in pointed_scope *)
Notation "X * Y" := ([X * Y, ispointed_prod]) : pointed_scope.

(** A pointed type family consists of a type family over a pointed type and a section of that family at the basepoint. By making this a Record, it has one fewer universe variable, and is cumulative. We declare [pfam_pr1] to be a coercion [pFam >-> Funclass]. *)
Record pFam (A : pType) := { pfam_pr1 :> A -> Type; dpoint : pfam_pr1 (point A)}.

Arguments Build_pFam {A} _ _.
Arguments pfam_pr1 {A} P : rename.
Arguments dpoint {A} P : rename.

(** The constant pointed family *)
Definition pfam_const {A : pType} (B : pType) : pFam A
  := Build_pFam (fun _ => pointed_type B) (point B).

(** [IsTrunc] for a pointed type family *)
Class IsTrunc_pFam n {A} (P : pFam A)
  := trunc_pfam_is_trunc : forall x, IsTrunc n (P x).

(** Pointed dependent functions *)
Record pForall (A : pType) (P : pFam A) := {
  pointed_fun : forall x, P x ;
  dpoint_eq : pointed_fun (point A) = dpoint P ;
}.

Arguments dpoint_eq {A P} f : rename.
Arguments pointed_fun {A P} f : rename.
Coercion pointed_fun : pForall >-> Funclass.

(** ** Pointed functions *)

(** A pointed map is a map with a proof that it preserves the point. We define it as as a notation for a non-dependent version of [pForall]. *)
Notation "A ->* B" := (pForall A (pfam_const B)) : pointed_scope.

Definition Build_pMap {A B : pType} (f : A -> B) (p : f (point A) = point B)
  : A ->* B
  := Build_pForall A (pfam_const B) f p.

(** The [&] is a bidirectionality hint that tells Coq to unify with the typing context after type checking the arguments to the left.  In practice, this allows Coq to infer [A] and [B] from the context. *)
Arguments Build_pMap {A B} & f p.

(** Pointed maps preserve the base point *)
Definition point_eq {A B : pType} (f : A ->* B)
  : f (point A) = point B
  := dpoint_eq f.

(** The identity pointed map *)
Definition pmap_idmap {A : pType} : A ->* A
  := Build_pMap idmap 1.

(** Composition of pointed maps *)
Definition pmap_compose {A B C : pType} (g : B ->* C) (f : A ->* B)
  : A ->* C
  := Build_pMap (g o f) (ap g (point_eq f) @ point_eq g).

Infix "o*" := pmap_compose : pointed_scope.

(** ** Pointed homotopies *)

(** A pointed homotopy is a homotopy with a proof that the preservation paths agree. We define it instead as a special case of a [pForall]. This means that we can define pointed homotopies between pointed homotopies. *)
Definition pfam_phomotopy {A : pType} {P : pFam A} (f g : pForall A P) : pFam A
  := Build_pFam (fun x => f x = g x) (dpoint_eq f @ (dpoint_eq g)^).

Definition pHomotopy {A : pType} {P : pFam A} (f g : pForall A P)
  := pForall A (pfam_phomotopy f g).

Infix "==*" := pHomotopy : pointed_scope.

Definition Build_pHomotopy {A : pType} {P : pFam A} {f g : pForall A P}
  (p : f == g) (q : p (point A) = dpoint_eq f @ (dpoint_eq g)^)
  : f ==* g
  := Build_pForall A (pfam_phomotopy f g) p q.

(** The underlying homotopy of a pointed homotopy *)
Coercion pointed_htpy {A : pType} {P : pFam A} {f g : pForall A P} (h : f ==* g)
  : f == g
  := h.

(** This is the form that the underlying proof of a pointed homotopy used to take before we changed it to be defined in terms of [pForall]. *)
Definition point_htpy {A : pType} {P : pFam A} {f g : pForall A P}
  (h : f ==* g) : h (point A) @ dpoint_eq g = dpoint_eq f.
A: pType
P: pFam A
f, g: pForall A P
h: f ==* g
h pt @ dpoint_eq g = dpoint_eq f
Proof.
A: pType
P: pFam A
f, g: pForall A P
h: f ==* g
h pt @ dpoint_eq g = dpoint_eq f
  apply moveR_pM.
A: pType
P: pFam A
f, g: pForall A P
h: f ==* g
h pt = dpoint_eq f @ (dpoint_eq g)^
  exact (dpoint_eq h).
Defined.

(** ** Pointed equivalences *)

(** A pointed equivalence is a pointed map and a proof that it is an equivalence *)
Record pEquiv (A B : pType) := {
  pointed_equiv_fun : pForall A (pfam_const B) ;
  pointed_isequiv :: IsEquiv pointed_equiv_fun ;
}.

Arguments Build_pEquiv {A B} & _ _.

(** TODO: It might be better behaved to define [pEquiv] as an equivalence and a proof that this equivalence is pointed. In pEquiv.v we have another constructor [Build_pEquiv'] which Coq can infer faster than [Build_pEquiv]. *)

Infix "<~>*" := pEquiv : pointed_scope.

(** Note: because we define [pMap] as a special case of [pForall], we must declare all coercions into [pForall], *not* into [pMap]. *)
Coercion pointed_equiv_fun : pEquiv >-> pForall.

Coercion pointed_equiv_equiv {A B} (f : A <~>* B)
  : A <~> B := Build_Equiv A B f _.

(** The pointed identity is a pointed equivalence *)
Definition pequiv_pmap_idmap {A} : A <~>* A
  := Build_pEquiv pmap_idmap _.

(** Pointed sigma types *)
Definition psigma {A : pType} (P : pFam A) : pType
  := [sig P, (point A; dpoint P)].

(** *** Pointed products *)

(** Pointed pi types; note that the domain is not pointed *)
Definition pproduct {A : Type} (F : A -> pType) : pType
  := [forall (a : A), pointed_type (F a), ispointed_type o F].

Definition pproduct_corec `{Funext} {A : Type} (F : A -> pType)
  (X : pType) (f : forall a, X ->* F a)
  : X ->* pproduct F.
H: Funext
A: Type
F: A -> pType
X: pType
f: forall a : A, X ->* F a
X ->* pproduct F
Proof.
H: Funext
A: Type
F: A -> pType
X: pType
f: forall a : A, X ->* F a
X ->* pproduct F
  snapply Build_pMap.
H: Funext
A: Type
F: A -> pType
X: pType
f: forall a : A, X ->* F a
X -> pproduct F
H: Funext
A: Type
F: A -> pType
X: pType
f: forall a : A, X ->* F a
?f pt = pt
  -
H: Funext
A: Type
F: A -> pType
X: pType
f: forall a : A, X ->* F a
X -> pproduct F intros x a.
H: Funext
A: Type
F: A -> pType
X: pType
f: forall a : A, X ->* F a
x: X
a: A
F a
    exact (f a x).
  -
H: Funext
A: Type
F: A -> pType
X: pType
f: forall a : A, X ->* F a
(fun x : X => (fun a : A => f a x) : pproduct F) pt =
pt cbn.
H: Funext
A: Type
F: A -> pType
X: pType
f: forall a : A, X ->* F a
(fun a : A => f a pt) =
(fun x : A => ispointed_type (F x))
    funext a.
H: Funext
A: Type
F: A -> pType
X: pType
f: forall a : A, X ->* F a
a: A
f a pt = ispointed_type (F a)
    apply point_eq.
Defined.

Definition pproduct_proj {A : Type} {F : A -> pType} (a : A)
  : pproduct F ->* F a.
A: Type
F: A -> pType
a: A
pproduct F ->* F a
Proof.
A: Type
F: A -> pType
a: A
pproduct F ->* F a
  snapply Build_pMap.
A: Type
F: A -> pType
a: A
pproduct F -> F a
A: Type
F: A -> pType
a: A
?f pt = pt
  -
A: Type
F: A -> pType
a: A
pproduct F -> F a intros x.
A: Type
F: A -> pType
a: A
x: pproduct F
F a
    exact (x a).
  -
A: Type
F: A -> pType
a: A
(fun x : pproduct F => x a) pt = pt reflexivity.
Defined.

(** The projections from a pointed product are pointed maps. *)
Definition pfst {A B : pType} : A * B ->* A
  := Build_pMap fst idpath.

Definition psnd {A B : pType} : A * B ->* B
  := Build_pMap snd idpath.

Definition pprod_corec {X Y} (Z : pType) (f : Z ->* X) (g : Z ->* Y)
  : Z ->* (X * Y)
  := Build_pMap (fun z => (f z, g z))
      (path_prod' (point_eq _) (point_eq _)).

Definition pprod_corec_beta_fst {X Y} (Z : pType) (f : Z ->* X) (g : Z ->* Y)
  : pfst o* pprod_corec Z f g ==* f.
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
pfst o* pprod_corec Z f g ==* f
Proof.
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
pfst o* pprod_corec Z f g ==* f
  snapply Build_pHomotopy.
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
pfst o* pprod_corec Z f g == f
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
?p pt =
dpoint_eq (pfst o* pprod_corec Z f g) @ (dpoint_eq f)^
  1: reflexivity.
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
(fun x0 : Z => 1) pt =
dpoint_eq (pfst o* pprod_corec Z f g) @ (dpoint_eq f)^
  apply moveL_pV.
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
1 @ dpoint_eq f =
dpoint_eq (pfst o* pprod_corec Z f g)
  refine (concat_1p _ @ _^ @ (concat_p1 _)^).
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
ap pfst (point_eq (pprod_corec Z f g)) = dpoint_eq f
  apply ap_fst_path_prod'.
Defined.

Definition pprod_corec_beta_snd {X Y} (Z : pType) (f : Z ->* X) (g : Z ->* Y)
  : psnd o* pprod_corec Z f g ==* g.
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
psnd o* pprod_corec Z f g ==* g
Proof.
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
psnd o* pprod_corec Z f g ==* g
  snapply Build_pHomotopy.
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
psnd o* pprod_corec Z f g == g
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
?p pt =
dpoint_eq (psnd o* pprod_corec Z f g) @ (dpoint_eq g)^
  1: reflexivity.
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
(fun x0 : Z => 1) pt =
dpoint_eq (psnd o* pprod_corec Z f g) @ (dpoint_eq g)^
  apply moveL_pV.
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
1 @ dpoint_eq g =
dpoint_eq (psnd o* pprod_corec Z f g)
  refine (concat_1p _ @ _^ @ (concat_p1 _)^).
X, Y, Z: pType
f: Z ->* X
g: Z ->* Y
ap psnd (point_eq (pprod_corec Z f g)) = dpoint_eq g
  apply ap_snd_path_prod'.
Defined.

(** The following tactics often allow us to "pretend" that pointed maps and homotopies preserve basepoints strictly. *)

(** First a version with no rewrites, which leaves some cleanup to be done but which can be used in transparent proofs. *)
Ltac pointed_reduce :=
  (*TODO: are these correct? *)
  unfold pointed_fun, pointed_htpy;
  cbn in *;
  repeat match goal with
           | [ X : pType |- _ ] => destruct X as [X ?point]
           | [ P : pFam ?X |- _ ] => destruct P as [P ?]
           | [ phi : pForall ?X ?Y |- _ ] => destruct phi as [phi ?]
           | [ alpha : pHomotopy ?f ?g |- _ ] => let H := fresh in destruct alpha as [alpha H]; try (apply moveR_pM in H)
           | [ equiv : pEquiv ?X ?Y |- _ ] => destruct equiv as [equiv ?iseq]
         end;
  cbn in *; unfold point in *;
  path_induction; cbn.

(** Next a version that uses [rewrite], and should only be used in opaque proofs. *)
Ltac pointed_reduce_rewrite :=
  pointed_reduce;
  rewrite ?concat_p1, ?concat_1p.

(** Finally, a version that just strictifies a single map or equivalence.  This has the advantage that it leaves the context more readable. *)
Ltac pointed_reduce_pmap f
  := try match type of f with
    | pEquiv ?X ?Y => destruct f as [f ?iseq]
    end;
    match type of f with
    | _ ->* ?Y => let p := fresh in destruct Y as [Y ?], f as [f p]; cbn in *; destruct p; cbn
    end.

(** A general tactic to replace pointedness paths in a [pForall] with reflexivity.  Because it generalizes [f pt], it can usually only be applied once the function itself is not longer needed.  Compared to [pointed_reduce], an advantage is that the pointed types do not need to be destructed. *)
Ltac pelim f :=
  try match type of f with
    | pEquiv ?X ?Y => destruct f as [f ?iseq]; unfold pointed_fun in *
  end;
  destruct f as [f ?ptd];
  cbn in f, ptd |- *;
  match type of ptd with ?fpt = _ => generalize dependent fpt end;
  napply paths_ind_r;
  try clear f.

Tactic Notation "pelim" constr(x0) := pelim x0.
Tactic Notation "pelim" constr(x0) constr(x1) := pelim x0; pelim x1.
Tactic Notation "pelim" constr(x0) constr(x1) constr(x2) := pelim x0; pelim x1 x2.
Tactic Notation "pelim" constr(x0) constr(x1) constr(x2) constr(x3) := pelim x0; pelim x1 x2 x3.
Tactic Notation "pelim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) := pelim x0; pelim x1 x2 x3 x4.
Tactic Notation "pelim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) constr(x5) := pelim x0; pelim x1 x2 x3 x4 x5.
Tactic Notation "pelim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) constr(x5) constr(x6) := pelim x0; pelim x1 x2 x3 x4 x5 x6.

(** ** Equivalences to sigma-types. *)

(** [pType] *)
Definition issig_ptype : { X : Type & X } <~> pType := ltac:(issig).

(** [pForall] *)
Definition issig_pforall (A : pType) (P : pFam A)
  : {f : forall x, P x & f (point A) = dpoint P} <~> (pForall A P)
  := ltac:(issig).

(** [pMap] *)
Definition issig_pmap (A B : pType)
  : {f : A -> B & f (point A) = point B} <~> (A ->* B)
  := ltac:(issig).

(** [pHomotopy] *)
Definition issig_phomotopy {A : pType} {P : pFam A} (f g : pForall A P)
  : {p : f == g & p (point A) = dpoint_eq f @ (dpoint_eq g)^} <~> (f ==* g)
  := ltac:(issig).

(** [pEquiv] *)
Definition issig_pequiv (A B : pType)
  : {f : A ->* B & IsEquiv f} <~> (A <~>* B)
  := ltac:(issig).

(** The record for pointed equivalences is equivalently a different sigma type *)
Definition issig_pequiv' (A B : pType)
  : {f : A <~> B & f (point A) = point B} <~> (A <~>* B)
  := ltac:(make_equiv).

(** [pForall] can also be described as a type of extensions. *)
Definition equiv_extension_along_pforall `{Funext} {A : pType} (P : pFam A)
  : ExtensionAlong@{Set _ _ _} (unit_name (point A)) P (unit_name (dpoint P)) <~> pForall A P.
H: Funext
A: pType
P: pFam A
ExtensionAlong (unit_name pt) P (unit_name (dpoint P)) <~>
pForall A P
Proof.
H: Funext
A: pType
P: pFam A
ExtensionAlong (unit_name pt) P (unit_name (dpoint P)) <~>
pForall A P
  unfold ExtensionAlong.
H: Funext
A: pType
P: pFam A
{s : forall y : A, P y & Unit -> s pt = dpoint P} <~>
pForall A P
  refine (issig_pforall A P oE _).
H: Funext
A: pType
P: pFam A
{s : forall y : A, P y & Unit -> s pt = dpoint P} <~>
{f : forall x : A, P x & f pt = dpoint P}
  apply equiv_functor_sigma_id; intro s.
H: Funext
A: pType
P: pFam A
s: forall y : A, P y
(Unit -> s pt = dpoint P) <~> s pt = dpoint P
  symmetry; apply equiv_unit_rec.
Defined.

(** This is [equiv_prod_coind] for pointed families. *)
Definition equiv_pprod_coind {A : pType} (P Q : pFam A)
  : (pForall A P * pForall A Q) <~>
      (pForall A (Build_pFam (fun a => prod (P a) (Q a)) (dpoint P, dpoint Q))).
A: pType
P, Q: pFam A
pForall A P * pForall A Q <~>
pForall A
  {|
    pfam_pr1 := fun a : A => (P a * Q a)%type;
    dpoint := (dpoint P, dpoint Q)
  |}
Proof.
A: pType
P, Q: pFam A
pForall A P * pForall A Q <~>
pForall A
  {|
    pfam_pr1 := fun a : A => (P a * Q a)%type;
    dpoint := (dpoint P, dpoint Q)
  |}
  transitivity {p : prod (forall a:A, P a) (forall a:A, Q a)
                    & prod (fst p _ = dpoint P) (snd p _ = dpoint Q)}.
A: pType
P, Q: pFam A
pForall A P * pForall A Q <~>
{p : (forall a : A, P a) * (forall a : A, Q a) &
((fst p pt = dpoint P) * (snd p pt = dpoint Q))%type}
A: pType
P, Q: pFam A
{p : (forall a : A, P a) * (forall a : A, Q a) &
((fst p pt = dpoint P) * (snd p pt = dpoint Q))%type} <~>
pForall A
  {|
    pfam_pr1 := fun a : A => (P a * Q a)%type;
    dpoint := (dpoint P, dpoint Q)
  |}
  1: make_equiv.
A: pType
P, Q: pFam A
{p : (forall a : A, P a) * (forall a : A, Q a) &
((fst p pt = dpoint P) * (snd p pt = dpoint Q))%type} <~>
pForall A
  {|
    pfam_pr1 := fun a : A => (P a * Q a)%type;
    dpoint := (dpoint P, dpoint Q)
  |}
  refine (issig_pforall _ _ oE _).
A: pType
P, Q: pFam A
{p : (forall a : A, P a) * (forall a : A, Q a) &
((fst p pt = dpoint P) * (snd p pt = dpoint Q))%type} <~>
{f
: forall x : A,
  {|
    pfam_pr1 := fun a : A => (P a * Q a)%type;
    dpoint := (dpoint P, dpoint Q)
  |} x &
f pt =
dpoint
  {|
    pfam_pr1 := fun a : A => (P a * Q a)%type;
    dpoint := (dpoint P, dpoint Q)
  |}}
  srapply equiv_functor_sigma'.
A: pType
P, Q: pFam A
(forall a : A, P a) * (forall a : A, Q a) <~>
(forall x : A,
 {|
   pfam_pr1 := fun a : A => (P a * Q a)%type;
   dpoint := (dpoint P, dpoint Q)
 |} x)
A: pType
P, Q: pFam A
forall a : (forall a : A, P a) * (forall a : A, Q a),
(fun p : (forall a0 : A, P a0) * (forall a0 : A, Q a0)
 =>
 ((fst p pt = dpoint P) * (snd p pt = dpoint Q))%type)
  a <~>
(fun
   f : forall x : A,
       {|
         pfam_pr1 := fun a0 : A => (P a0 * Q a0)%type;
         dpoint := (dpoint P, dpoint Q)
       |} x =>
 f pt =
 dpoint
   {|
     pfam_pr1 := fun a0 : A => (P a0 * Q a0)%type;
     dpoint := (dpoint P, dpoint Q)
   |}) (?f a)
  1: apply equiv_prod_coind.
A: pType
P, Q: pFam A
forall a : (forall a : A, P a) * (forall a : A, Q a),
(fun p : (forall a0 : A, P a0) * (forall a0 : A, Q a0)
 =>
 ((fst p pt = dpoint P) * (snd p pt = dpoint Q))%type)
  a <~>
(fun
   f : forall x : A,
       {|
         pfam_pr1 := fun a0 : A => (P a0 * Q a0)%type;
         dpoint := (dpoint P, dpoint Q)
       |} x =>
 f pt =
 dpoint
   {|
     pfam_pr1 := fun a0 : A => (P a0 * Q a0)%type;
     dpoint := (dpoint P, dpoint Q)
   |}) (equiv_prod_coind P Q a)
  intro f; cbn.
A: pType
P, Q: pFam A
f: ((forall a : A, P a) * (forall a : A, Q a))%type
(fst f pt = dpoint P) * (snd f pt = dpoint Q) <~>
prod_coind_uncurried f pt = (dpoint P, dpoint Q)
  unfold prod_coind_uncurried.
A: pType
P, Q: pFam A
f: ((forall a : A, P a) * (forall a : A, Q a))%type
(fst f pt = dpoint P) * (snd f pt = dpoint Q) <~>
(fst f pt, snd f pt) = (dpoint P, dpoint Q)
  exact (equiv_path_prod (fst f _, snd f _) (dpoint P, dpoint Q)).
Defined.

Definition functor_pprod {A A' B B' : pType} (f : A ->* A') (g : B ->* B')
  : A * B ->* A' * B'.
A, A', B, B': pType
f: A ->* A'
g: B ->* B'
A * B ->* A' * B'
Proof.
A, A', B, B': pType
f: A ->* A'
g: B ->* B'
A * B ->* A' * B'
  snapply Build_pMap.
A, A', B, B': pType
f: A ->* A'
g: B ->* B'
[A * B, ispointed_prod] -> [A' * B', ispointed_prod]
A, A', B, B': pType
f: A ->* A'
g: B ->* B'
?f pt = pt
  -
A, A', B, B': pType
f: A ->* A'
g: B ->* B'
[A * B, ispointed_prod] -> [A' * B', ispointed_prod] exact (functor_prod f g).
  -
A, A', B, B': pType
f: A ->* A'
g: B ->* B'
functor_prod f g pt = pt apply path_prod; apply point_eq.
Defined.

(** [isequiv_functor_prod] applies, and is an Instance. *)
Definition equiv_functor_pprod {A A' B B' : pType} (f : A <~>* A') (g : B <~>* B')
  : A * B <~>* A' * B'
  := Build_pEquiv (functor_pprod f g) _.

(** ** Various operations with pointed homotopies *)

(** For the following three instances, the typeclass (e.g. [Reflexive]) requires a third universe variable, the maximum of the universe of [A] and the universe of the values of [P].  Because of this, in each case we first prove a version not mentioning the typeclass, which avoids a stray universe variable. *)

(** [pHomotopy] is a reflexive relation *)
Definition phomotopy_reflexive {A : pType} {P : pFam A} (f : pForall A P)
  : f ==* f
  := Build_pHomotopy (fun x => 1) (concat_pV _)^.

Instance phomotopy_reflexive' {A : pType} {P : pFam A}
  : Reflexive (@pHomotopy A P)
  := @phomotopy_reflexive A P.

(** [pHomotopy] is a symmetric relation *)
Definition phomotopy_symmetric {A P} {f g : pForall A P} (p : f ==* g)
  : g ==* f.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
g ==* f
Proof.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
g ==* f
  snrefine (Build_pHomotopy _ _); cbn.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
g == f
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
?Goal pt = dpoint_eq g @ (dpoint_eq f)^
  1: intros x; exact ((p x)^).
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
((fun x : A => (p x)^) : g == f) pt =
dpoint_eq g @ (dpoint_eq f)^
  by pelim p f g.
Defined.

Instance phomotopy_symmetric' {A P}
  : Symmetric (@pHomotopy A P)
  := @phomotopy_symmetric A P.

Notation "p ^*" := (phomotopy_symmetric p) : pointed_scope.

(** [pHomotopy] is a transitive relation *)
Definition phomotopy_transitive {A P} {f g h : pForall A P} (p : f ==* g) (q : g ==* h)
  : f ==* h.
A: pType
P: pFam A
f, g, h: pForall A P
p: f ==* g
q: g ==* h
f ==* h
Proof.
A: pType
P: pFam A
f, g, h: pForall A P
p: f ==* g
q: g ==* h
f ==* h
  snrefine (Build_pHomotopy (fun x => p x @ q x) _).
A: pType
P: pFam A
f, g, h: pForall A P
p: f ==* g
q: g ==* h
(fun x : A => p x @ q x) pt =
dpoint_eq f @ (dpoint_eq h)^
  nrefine (dpoint_eq p @@ dpoint_eq q @ concat_pp_p _ _ _ @ _).
A: pType
P: pFam A
f, g, h: pForall A P
p: f ==* g
q: g ==* h
dpoint_eq f @
((dpoint_eq g)^ @ dpoint (pfam_phomotopy g h)) =
dpoint_eq f @ (dpoint_eq h)^
  napply whiskerL; napply concat_V_pp.
Defined.

Instance phomotopy_transitive' {A P} : Transitive (@pHomotopy A P)
  := @phomotopy_transitive A P.

Notation "p @* q" := (phomotopy_transitive p q) : pointed_scope.

(** ** Whiskering of pointed homotopies by pointed functions *)

Definition pmap_postwhisker {A B C : pType} {f g : A ->* B}
  (h : B ->* C) (p : f ==* g)
  : h o* f ==* h o* g.
A, B, C: pType
f, g: A ->* B
h: B ->* C
p: f ==* g
h o* f ==* h o* g
Proof.
A, B, C: pType
f, g: A ->* B
h: B ->* C
p: f ==* g
h o* f ==* h o* g
  snrefine (Build_pHomotopy _ _); cbn.
A, B, C: pType
f, g: A ->* B
h: B ->* C
p: f ==* g
(fun x : A => h (f x)) == (fun x : A => h (g x))
A, B, C: pType
f, g: A ->* B
h: B ->* C
p: f ==* g
?Goal pt =
(ap h (point_eq f) @ point_eq h) @
(ap h (point_eq g) @ point_eq h)^
  1: exact (fun x => ap h (p x)).
A, B, C: pType
f, g: A ->* B
h: B ->* C
p: f ==* g
(fun x : A => ap h (p x)) pt =
(ap h (point_eq f) @ point_eq h) @
(ap h (point_eq g) @ point_eq h)^
  by pelim p f g h.
Defined.

Definition pmap_prewhisker {A B C : pType} (f : A ->* B)
  {g h : B ->* C} (p : g ==* h)
  : g o* f ==* h o* f.
A, B, C: pType
f: A ->* B
g, h: B ->* C
p: g ==* h
g o* f ==* h o* f
Proof.
A, B, C: pType
f: A ->* B
g, h: B ->* C
p: g ==* h
g o* f ==* h o* f
  snrefine (Build_pHomotopy _ _); cbn.
A, B, C: pType
f: A ->* B
g, h: B ->* C
p: g ==* h
(fun x : A => g (f x)) == (fun x : A => h (f x))
A, B, C: pType
f: A ->* B
g, h: B ->* C
p: g ==* h
?Goal pt =
(ap g (point_eq f) @ point_eq g) @
(ap h (point_eq f) @ point_eq h)^
  1: exact (fun x => p (f x)).
A, B, C: pType
f: A ->* B
g, h: B ->* C
p: g ==* h
(fun x : A => p (f x)) pt =
(ap g (point_eq f) @ point_eq g) @
(ap h (point_eq f) @ point_eq h)^
  by pelim f p g h.
Defined.

(** ** 1-categorical properties of [pType]. *)

(** Composition of pointed maps is associative up to pointed homotopy *)
Definition pmap_compose_assoc {A B C D : pType} (h : C ->* D)
  (g : B ->* C) (f : A ->* B)
  : (h o* g) o* f ==* h o* (g o* f).
A, B, C, D: pType
h: C ->* D
g: B ->* C
f: A ->* B
h o* g o* f ==* h o* (g o* f)
Proof.
A, B, C, D: pType
h: C ->* D
g: B ->* C
f: A ->* B
h o* g o* f ==* h o* (g o* f)
  snapply Build_pHomotopy.
A, B, C, D: pType
h: C ->* D
g: B ->* C
f: A ->* B
h o* g o* f == h o* (g o* f)
A, B, C, D: pType
h: C ->* D
g: B ->* C
f: A ->* B
?p pt =
dpoint_eq (h o* g o* f) @ (dpoint_eq (h o* (g o* f)))^
  1: reflexivity.
A, B, C, D: pType
h: C ->* D
g: B ->* C
f: A ->* B
(fun x0 : A => 1) pt =
dpoint_eq (h o* g o* f) @ (dpoint_eq (h o* (g o* f)))^
  by pelim f g h.
Defined.

(** precomposition of identity pointed map *)
Definition pmap_precompose_idmap {A B : pType} (f : A ->* B)
: f o* pmap_idmap ==* f.
A, B: pType
f: A ->* B
f o* pmap_idmap ==* f
Proof.
A, B: pType
f: A ->* B
f o* pmap_idmap ==* f
  snapply Build_pHomotopy.
A, B: pType
f: A ->* B
f o* pmap_idmap == f
A, B: pType
f: A ->* B
?p pt = dpoint_eq (f o* pmap_idmap) @ (dpoint_eq f)^
  1: reflexivity.
A, B: pType
f: A ->* B
(fun x0 : A => 1) pt =
dpoint_eq (f o* pmap_idmap) @ (dpoint_eq f)^
  by pelim f.
Defined.

(** postcomposition of identity pointed map *)
Definition pmap_postcompose_idmap {A B : pType} (f : A ->* B)
: pmap_idmap o* f ==* f.
A, B: pType
f: A ->* B
pmap_idmap o* f ==* f
Proof.
A, B: pType
f: A ->* B
pmap_idmap o* f ==* f
  snapply Build_pHomotopy.
A, B: pType
f: A ->* B
pmap_idmap o* f == f
A, B: pType
f: A ->* B
?p pt = dpoint_eq (pmap_idmap o* f) @ (dpoint_eq f)^
  1: reflexivity.
A, B: pType
f: A ->* B
(fun x0 : A => 1) pt =
dpoint_eq (pmap_idmap o* f) @ (dpoint_eq f)^
  by pelim f.
Defined.

(** ** 1-categorical properties of [pForall]. *)

Definition phomotopy_postwhisker {A : pType} {P : pFam A}
  {f g h : pForall A P} {p p' : f ==* g} (r : p ==* p') (q : g ==* h)
  : p @* q ==* p' @* q.
A: pType
P: pFam A
f, g, h: pForall A P
p, p': f ==* g
r: p ==* p'
q: g ==* h
p @* q ==* p' @* q
Proof.
A: pType
P: pFam A
f, g, h: pForall A P
p, p': f ==* g
r: p ==* p'
q: g ==* h
p @* q ==* p' @* q
  snapply Build_pHomotopy.
A: pType
P: pFam A
f, g, h: pForall A P
p, p': f ==* g
r: p ==* p'
q: g ==* h
p @* q == p' @* q
A: pType
P: pFam A
f, g, h: pForall A P
p, p': f ==* g
r: p ==* p'
q: g ==* h
?p pt = dpoint_eq (p @* q) @ (dpoint_eq (p' @* q))^
  1: exact (fun x => whiskerR (r x) (q x)).
A: pType
P: pFam A
f, g, h: pForall A P
p, p': f ==* g
r: p ==* p'
q: g ==* h
(fun x : A => whiskerR (r x) (q x)) pt =
dpoint_eq (p @* q) @ (dpoint_eq (p' @* q))^
  by pelim q r p p' f g h.
Defined.

Definition phomotopy_prewhisker {A : pType} {P : pFam A}
  {f g h : pForall A P} (p : f ==* g) {q q' : g ==* h} (s : q ==* q')
  : p @* q ==* p @* q'.
A: pType
P: pFam A
f, g, h: pForall A P
p: f ==* g
q, q': g ==* h
s: q ==* q'
p @* q ==* p @* q'
Proof.
A: pType
P: pFam A
f, g, h: pForall A P
p: f ==* g
q, q': g ==* h
s: q ==* q'
p @* q ==* p @* q'
  snapply Build_pHomotopy.
A: pType
P: pFam A
f, g, h: pForall A P
p: f ==* g
q, q': g ==* h
s: q ==* q'
p @* q == p @* q'
A: pType
P: pFam A
f, g, h: pForall A P
p: f ==* g
q, q': g ==* h
s: q ==* q'
?p pt = dpoint_eq (p @* q) @ (dpoint_eq (p @* q'))^
  1: exact (fun x => whiskerL (p x) (s x)).
A: pType
P: pFam A
f, g, h: pForall A P
p: f ==* g
q, q': g ==* h
s: q ==* q'
(fun x : A => whiskerL (p x) (s x)) pt =
dpoint_eq (p @* q) @ (dpoint_eq (p @* q'))^
  by pelim s q q' p f g h.
Defined.

Definition phomotopy_compose_assoc {A : pType} {P : pFam A}
  {f g h k : pForall A P} (p : f ==* g) (q : g ==* h) (r : h ==* k)
  : p @* (q @* r) ==* (p @* q) @* r.
A: pType
P: pFam A
f, g, h, k: pForall A P
p: f ==* g
q: g ==* h
r: h ==* k
p @* (q @* r) ==* (p @* q) @* r
Proof.
A: pType
P: pFam A
f, g, h, k: pForall A P
p: f ==* g
q: g ==* h
r: h ==* k
p @* (q @* r) ==* (p @* q) @* r
  snapply Build_pHomotopy.
A: pType
P: pFam A
f, g, h, k: pForall A P
p: f ==* g
q: g ==* h
r: h ==* k
p @* (q @* r) == (p @* q) @* r
A: pType
P: pFam A
f, g, h, k: pForall A P
p: f ==* g
q: g ==* h
r: h ==* k
?p pt =
dpoint_eq (p @* (q @* r)) @
(dpoint_eq ((p @* q) @* r))^
  1: exact (fun x => concat_p_pp (p x) (q x) (r x)).
A: pType
P: pFam A
f, g, h, k: pForall A P
p: f ==* g
q: g ==* h
r: h ==* k
(fun x : A => concat_p_pp (p x) (q x) (r x)) pt =
dpoint_eq (p @* (q @* r)) @
(dpoint_eq ((p @* q) @* r))^
  by pelim r q p f g h k.
Defined.

Definition phomotopy_compose_p1 {A : pType} {P : pFam A} {f g : pForall A P}
 (p : f ==* g) : p @* reflexivity g ==* p.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
p @* reflexivity g ==* p
Proof.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
p @* reflexivity g ==* p
  srapply Build_pHomotopy.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
p @* reflexivity g == p
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
?p pt =
dpoint_eq (p @* reflexivity g) @ (dpoint_eq p)^
  1: intro; apply concat_p1.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
((fun x : A => concat_p1 (p x))
 :
 p @* reflexivity g == p) pt =
dpoint_eq (p @* reflexivity g) @ (dpoint_eq p)^
  by pelim p f g.
Defined.

Definition phomotopy_compose_1p {A : pType} {P : pFam A} {f g : pForall A P}
 (p : f ==* g) : reflexivity f @* p ==* p.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
reflexivity f @* p ==* p
Proof.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
reflexivity f @* p ==* p
  srapply Build_pHomotopy.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
reflexivity f @* p == p
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
?p pt =
dpoint_eq (reflexivity f @* p) @ (dpoint_eq p)^
  1: intro x; apply concat_1p.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
((fun x : A => concat_1p (p x))
 :
 reflexivity f @* p == p) pt =
dpoint_eq (reflexivity f @* p) @ (dpoint_eq p)^
  by pelim p f g.
Defined.

Definition phomotopy_compose_pV {A : pType} {P : pFam A} {f g : pForall A P}
 (p : f ==* g) : p @* p ^* ==* phomotopy_reflexive f.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
p @* p^* ==* phomotopy_reflexive f
Proof.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
p @* p^* ==* phomotopy_reflexive f
  srapply Build_pHomotopy.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
p @* p^* == phomotopy_reflexive f
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
?p pt =
dpoint_eq (p @* p^*) @
(dpoint_eq (phomotopy_reflexive f))^
  1: intro x; apply concat_pV.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
((fun x : A => concat_pV (p x))
 :
 p @* p^* == phomotopy_reflexive f) pt =
dpoint_eq (p @* p^*) @
(dpoint_eq (phomotopy_reflexive f))^
  by pelim p f g.
Defined.

Definition phomotopy_compose_Vp {A : pType} {P : pFam A} {f g : pForall A P}
 (p : f ==* g) : p ^* @* p ==* phomotopy_reflexive g.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
p^* @* p ==* phomotopy_reflexive g
Proof.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
p^* @* p ==* phomotopy_reflexive g
  srapply Build_pHomotopy.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
p^* @* p == phomotopy_reflexive g
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
?p pt =
dpoint_eq (p^* @* p) @
(dpoint_eq (phomotopy_reflexive g))^
  1: intro x; apply concat_Vp.
A: pType
P: pFam A
f, g: pForall A P
p: f ==* g
((fun x : A => concat_Vp (p x))
 :
 p^* @* p == phomotopy_reflexive g) pt =
dpoint_eq (p^* @* p) @
(dpoint_eq (phomotopy_reflexive g))^
  by pelim p f g.
Defined.

(** ** The pointed category structure of [pType] *)

(** Pointed types of pointed maps *)

(** A family of pointed types gives rise to a [pFam]. *)
Definition pointed_fam {A : pType} (B : A -> pType) : pFam A
  := Build_pFam (pointed_type o B) (point (B (point A))).

(** The section of a family of pointed types *)
Definition point_pforall {A : pType} (B : A -> pType) : pForall A (pointed_fam B)
  := Build_pForall A (pointed_fam B) (fun x => point (B x)) 1.

(** The pointed type of dependent pointed maps. Note that we need a family of pointed types, not just a family of types with a point over the basepoint of [A]. *)
Definition ppForall (A : pType) (B : A -> pType) : pType
  := [pForall A (pointed_fam B), point_pforall B].

Notation "'ppforall'  x .. y , P"
  := (ppForall _ (fun x => .. (ppForall _ (fun y => P)) ..))
     : pointed_scope.

(** The constant (zero) map *)
Definition pconst {A B : pType} : A ->* B
  := point_pforall (fun _ => B).

(** The pointed type of pointed maps.  This is a special case of [ppForall]. *)
Definition ppMap (A B : pType) : pType
  := [A ->* B, pconst].

Infix "->**" := ppMap : pointed_scope.

Lemma pmap_punit_pconst {A : pType} (f : A ->* pUnit) : pconst ==* f.
A: pType
f: A ->* pUnit
pconst ==* f
Proof.
A: pType
f: A ->* pUnit
pconst ==* f
  srapply Build_pHomotopy.
A: pType
f: A ->* pUnit
pconst == f
A: pType
f: A ->* pUnit
?p pt = dpoint_eq pconst @ (dpoint_eq f)^
  1: intro; apply path_unit.
A: pType
f: A ->* pUnit
((fun x : A => path_unit (pconst x) (f x))
 :
 pconst == f) pt = dpoint_eq pconst @ (dpoint_eq f)^
  apply path_contr.
Defined.

Lemma punit_pmap_pconst {A : pType} (f : pUnit ->* A) : pconst ==* f.
A: pType
f: pUnit ->* A
pconst ==* f
Proof.
A: pType
f: pUnit ->* A
pconst ==* f
  srapply Build_pHomotopy.
A: pType
f: pUnit ->* A
pconst == f
A: pType
f: pUnit ->* A
?p pt = dpoint_eq pconst @ (dpoint_eq f)^
  1: intros []; exact (point_eq f)^.
A: pType
f: pUnit ->* A
((fun x : pUnit =>
  match x as u return (pconst u = f u) with
  | tt => (point_eq f)^
  end)
 :
 pconst == f) pt = dpoint_eq pconst @ (dpoint_eq f)^
  exact (concat_1p _)^.
Defined.

Instance contr_pmap_from_contr `{Funext} {A B : pType} `{C : Contr A}
  : Contr (A ->* B).
H: Funext
A, B: pType
C: Contr A
Contr (A ->* B)
Proof.
H: Funext
A, B: pType
C: Contr A
Contr (A ->* B)
  rapply (contr_equiv' { b : B & b = pt }).
H: Funext
A, B: pType
C: Contr A
{b : B & b = pt} <~> (A ->* B)
  refine (issig_pmap A B oE _).
H: Funext
A, B: pType
C: Contr A
{b : B & b = pt} <~> {f : A -> B & f pt = pt}
  exact (equiv_functor_sigma_pb (equiv_arrow_from_contr A B)^-1%equiv).
Defined.

(** * [pType] and [pForall] as wild categories *)

(** Note that the definitions for [pForall] are also used for the higher structure in [pType]. *)

(** [pType] is a graph *)
Instance isgraph_ptype : IsGraph pType
  := Build_IsGraph pType (fun X Y => X ->* Y).

(** [pForall] is a graph *)
Instance isgraph_pforall (A : pType) (P : pFam A)
  : IsGraph (pForall A P)
  := Build_IsGraph _ pHomotopy.

(** [pType] is a 0-coherent 1-category *)
Instance is01cat_ptype : Is01Cat pType
  := Build_Is01Cat pType _ (@pmap_idmap) (@pmap_compose).

(** [pForall] is a 0-coherent 1-category *)
Instance is01cat_pforall (A : pType) (P : pFam A) : Is01Cat (pForall A P).
A: pType
P: pFam A
Is01Cat (pForall A P)
Proof.
A: pType
P: pFam A
Is01Cat (pForall A P)
  econstructor.
A: pType
P: pFam A
forall a : pForall A P, a $-> a
A: pType
P: pFam A
forall a b c : pForall A P,
(b $-> c) -> (a $-> b) -> a $-> c
  -
A: pType
P: pFam A
forall a : pForall A P, a $-> a exact phomotopy_reflexive.
  -
A: pType
P: pFam A
forall a b c : pForall A P,
(b $-> c) -> (a $-> b) -> a $-> c intros a b c f g.
A: pType
P: pFam A
a, b, c: pForall A P
f: b $-> c
g: a $-> b
a $-> c exact (g @* f).
Defined.

Instance is2graph_ptype : Is2Graph pType := fun f g => _.

Instance is2graph_pforall (A : pType) (P : pFam A)
  : Is2Graph (pForall A P)
  := fun f g => _.

(** [pForall] is a 0-coherent 1-groupoid *)
Instance is0gpd_pforall (A : pType) (P : pFam A) : Is0Gpd (pForall A P).
A: pType
P: pFam A
Is0Gpd (pForall A P)
Proof.
A: pType
P: pFam A
Is0Gpd (pForall A P)
  srapply Build_Is0Gpd.
A: pType
P: pFam A
forall a b : pForall A P, (a $-> b) -> b $-> a intros ? ? h.
A: pType
P: pFam A
a, b: pForall A P
h: a $-> b
b $-> a exact h^*.
Defined.

(** [pType] is a 1-coherent 1-category *)
Instance is1cat_ptype : Is1Cat pType.
Is1Cat pType
Proof.
Is1Cat pType
  snapply Build_Is1Cat'.
forall a b : pType, Is01Cat (a $-> b)
forall a b : pType, Is0Gpd (a $-> b)
forall (a b c : pType) (g : b $-> c),
Is0Functor (cat_postcomp a g)
forall (a b c : pType) (f : a $-> b),
Is0Functor (cat_precomp c f)
forall (a b c d : pType) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f)
forall (a b : pType) (f : a $-> b), Id b $o f $== f
forall (a b : pType) (f : a $-> b), f $o Id a $== f
  1, 2: exact _.
forall (a b c : pType) (g : b $-> c),
Is0Functor (cat_postcomp a g)
forall (a b c : pType) (f : a $-> b),
Is0Functor (cat_precomp c f)
forall (a b c d : pType) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f)
forall (a b : pType) (f : a $-> b), Id b $o f $== f
forall (a b : pType) (f : a $-> b), f $o Id a $== f
  -
forall (a b c : pType) (g : b $-> c),
Is0Functor (cat_postcomp a g) intros A B C h; rapply Build_Is0Functor.
A, B, C: pType
h: B $-> C
forall a b : A $-> B,
(a $-> b) -> cat_postcomp A h a $-> cat_postcomp A h b
    intros f g p; cbn.
A, B, C: pType
h: B $-> C
f, g: A $-> B
p: f $-> g
h o* f ==* h o* g
    apply pmap_postwhisker; assumption.
  -
forall (a b c : pType) (f : a $-> b),
Is0Functor (cat_precomp c f) intros A B C h; rapply Build_Is0Functor.
A, B, C: pType
h: A $-> B
forall a b : B $-> C,
(a $-> b) -> cat_precomp C h a $-> cat_precomp C h b
    intros f g p; cbn.
A, B, C: pType
h: A $-> B
f, g: B $-> C
p: f $-> g
f o* h ==* g o* h
    apply pmap_prewhisker; assumption.
  -
forall (a b c d : pType) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f) intros ? ? ? ? f g h; exact (pmap_compose_assoc h g f).
  -
forall (a b : pType) (f : a $-> b), Id b $o f $== f intros ? ? f; exact (pmap_postcompose_idmap f).
  -
forall (a b : pType) (f : a $-> b), f $o Id a $== f intros ? ? f; exact (pmap_precompose_idmap f).
Defined.

(** [pType] is a pointed category *)
Instance ispointedcat_ptype : IsPointedCat pType.
IsPointedCat pType
Proof.
IsPointedCat pType
  snapply Build_IsPointedCat.
pType
IsInitial ?zero_object
IsTerminal ?zero_object
  +
pType exact pUnit.
  +
IsInitial pUnit intro A.
A: pType
{f : pUnit $-> A & forall g : pUnit $-> A, f $== g}
    exists pconst.
A: pType
forall g : pUnit $-> A, pconst $== g
    exact punit_pmap_pconst.
  +
IsTerminal pUnit intro B.
B: pType
{f : B $-> pUnit & forall g : B $-> pUnit, f $== g}
    exists pconst.
B: pType
forall g : B $-> pUnit, pconst $== g
    exact pmap_punit_pconst.
Defined.

(** The constant map is definitionally equal to the zero_morphism of a pointed category *)
Definition path_zero_morphism_pconst (A B : pType)
  : (@pconst A B) = zero_morphism := idpath.

(** [pForall] is a 1-category *)
Instance is1cat_pforall (A : pType) (P : pFam A) : Is1Cat (pForall A P) | 10.
A: pType
P: pFam A
Is1Cat (pForall A P)
Proof.
A: pType
P: pFam A
Is1Cat (pForall A P)
  snapply Build_Is1Cat'.
A: pType
P: pFam A
forall a b : pForall A P, Is01Cat (a $-> b)
A: pType
P: pFam A
forall a b : pForall A P, Is0Gpd (a $-> b)
A: pType
P: pFam A
forall (a b c : pForall A P) (g : b $-> c),
Is0Functor (cat_postcomp a g)
A: pType
P: pFam A
forall (a b c : pForall A P) (f : a $-> b),
Is0Functor (cat_precomp c f)
A: pType
P: pFam A
forall (a b c d : pForall A P) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f)
A: pType
P: pFam A
forall (a b : pForall A P) (f : a $-> b),
Id b $o f $== f
A: pType
P: pFam A
forall (a b : pForall A P) (f : a $-> b),
f $o Id a $== f
  1, 2: exact _.
A: pType
P: pFam A
forall (a b c : pForall A P) (g : b $-> c),
Is0Functor (cat_postcomp a g)
A: pType
P: pFam A
forall (a b c : pForall A P) (f : a $-> b),
Is0Functor (cat_precomp c f)
A: pType
P: pFam A
forall (a b c d : pForall A P) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f)
A: pType
P: pFam A
forall (a b : pForall A P) (f : a $-> b),
Id b $o f $== f
A: pType
P: pFam A
forall (a b : pForall A P) (f : a $-> b),
f $o Id a $== f
  -
A: pType
P: pFam A
forall (a b c : pForall A P) (g : b $-> c),
Is0Functor (cat_postcomp a g) intros f g h p; rapply Build_Is0Functor.
A: pType
P: pFam A
f, g, h: pForall A P
p: g $-> h
forall a b : f $-> g,
(a $-> b) -> cat_postcomp f p a $-> cat_postcomp f p b
    intros q r s.
A: pType
P: pFam A
f, g, h: pForall A P
p: g $-> h
q, r: f $-> g
s: q $-> r
cat_postcomp f p q $-> cat_postcomp f p r exact (phomotopy_postwhisker s p).
  -
A: pType
P: pFam A
forall (a b c : pForall A P) (f : a $-> b),
Is0Functor (cat_precomp c f) intros f g h p; rapply Build_Is0Functor.
A: pType
P: pFam A
f, g, h: pForall A P
p: f $-> g
forall a b : g $-> h,
(a $-> b) -> cat_precomp h p a $-> cat_precomp h p b
    intros q r s.
A: pType
P: pFam A
f, g, h: pForall A P
p: f $-> g
q, r: g $-> h
s: q $-> r
cat_precomp h p q $-> cat_precomp h p r exact (phomotopy_prewhisker p s).
  -
A: pType
P: pFam A
forall (a b c d : pForall A P) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f) intros ? ? ? ? p q r.
A: pType
P: pFam A
a, b, c, d: pForall A P
p: a $-> b
q: b $-> c
r: c $-> d
r $o q $o p $== r $o (q $o p) simpl.
A: pType
P: pFam A
a, b, c, d: pForall A P
p: a $-> b
q: b $-> c
r: c $-> d
p @* (q @* r) ==* (p @* q) @* r exact (phomotopy_compose_assoc p q r).
  -
A: pType
P: pFam A
forall (a b : pForall A P) (f : a $-> b),
Id b $o f $== f intros ? ? p; exact (phomotopy_compose_p1 p).
  -
A: pType
P: pFam A
forall (a b : pForall A P) (f : a $-> b),
f $o Id a $== f intros ? ? p; exact (phomotopy_compose_1p p).
Defined.

(** [pForall] is a 1-groupoid *)
Instance is1gpd_pforall (A : pType) (P : pFam A) : Is1Gpd (pForall A P) | 10.
A: pType
P: pFam A
Is1Gpd (pForall A P)
Proof.
A: pType
P: pFam A
Is1Gpd (pForall A P)
  econstructor.
A: pType
P: pFam A
forall (a b : pForall A P) (f : a $-> b),
f^$ $o f $== Id a
A: pType
P: pFam A
forall (a b : pForall A P) (f : a $-> b),
f $o f^$ $== Id b
  +
A: pType
P: pFam A
forall (a b : pForall A P) (f : a $-> b),
f^$ $o f $== Id a intros ? ? p.
A: pType
P: pFam A
a, b: pForall A P
p: a $-> b
p^$ $o p $== Id a exact (phomotopy_compose_pV p).
  +
A: pType
P: pFam A
forall (a b : pForall A P) (f : a $-> b),
f $o f^$ $== Id b intros ? ? p.
A: pType
P: pFam A
a, b: pForall A P
p: a $-> b
p $o p^$ $== Id b exact (phomotopy_compose_Vp p).
Defined.

Instance is3graph_ptype : Is3Graph pType
  := fun f g => is2graph_pforall _ _.

Instance is21cat_ptype : Is21Cat pType.
Is21Cat pType
Proof.
Is21Cat pType
  unshelve econstructor.
forall a b : pType, Is1Gpd (a $-> b)
forall (a b c : pType) (g : b $-> c),
Is1Functor (cat_postcomp a g)
forall (a b c : pType) (f : a $-> b),
Is1Functor (cat_precomp c f)
forall (a b c : pType) (f f' : a $-> b)
(g g' : b $-> c) (p : f $== f') (p' : g $== g'),
(p' $@R f) $@ (g' $@L p) $== (g $@L p) $@ (p' $@R f')
forall (a b c d : pType) (f : a $-> b) (g : b $-> c),
Is1Natural
  (fun x : c $-> d =>
   cat_precomp d f (cat_precomp d g x))
  (cat_precomp d (g $o f)) (cat_assoc f g)
forall (a b c d : pType) (f : a $-> b) (h : c $-> d),
Is1Natural
  (fun x : b $-> c =>
   cat_precomp d f (cat_postcomp b h x))
  (fun x : b $-> c =>
   cat_postcomp a h (cat_precomp c f x))
  (fun g : b $-> c => cat_assoc f g h)
forall (a b c d : pType) (g : b $-> c) (h : c $-> d),
Is1Natural (cat_postcomp a (h $o g))
  (fun x : a $-> b =>
   cat_postcomp a h (cat_postcomp a g x))
  (fun f : a $-> b => cat_assoc f g h)
forall a b : pType,
Is1Natural (cat_postcomp a (Id b)) idmap cat_idl
forall a b : pType,
Is1Natural (cat_precomp b (Id a)) idmap cat_idr
forall (a b c d e : pType) (f : a $-> b) (g : b $-> c)
(h : c $-> d) (k : d $-> e),
k $@L cat_assoc f g h $o cat_assoc f (h $o g) k $o
cat_assoc g h k $@R f $==
cat_assoc (g $o f) h k $o cat_assoc f g (k $o h)
forall (a b c : pType) (f : a $-> b) (g : b $-> c),
g $@L cat_idl f $o cat_assoc f (Id b) g $==
cat_idr g $@R f
  -
forall a b : pType, Is1Gpd (a $-> b) exact _.
  -
forall (a b c : pType) (g : b $-> c),
Is1Functor (cat_postcomp a g) intros A B C f; napply Build_Is1Functor.
A, B, C: pType
f: B $-> C
forall (a b : A $-> B) (f0 g : a $-> b),
f0 $== g ->
fmap (cat_postcomp A f) f0 $==
fmap (cat_postcomp A f) g
A, B, C: pType
f: B $-> C
forall a : A $-> B,
fmap (cat_postcomp A f) (Id a) $==
Id (cat_postcomp A f a)
A, B, C: pType
f: B $-> C
forall (a b c : A $-> B) (f0 : a $-> b) (g : b $-> c),
fmap (cat_postcomp A f) (g $o f0) $==
fmap (cat_postcomp A f) g $o
fmap (cat_postcomp A f) f0
    +
A, B, C: pType
f: B $-> C
forall (a b : A $-> B) (f0 g : a $-> b),
f0 $== g ->
fmap (cat_postcomp A f) f0 $==
fmap (cat_postcomp A f) g intros g h p q r.
A, B, C: pType
f: B $-> C
g, h: A $-> B
p, q: g $-> h
r: p $== q
fmap (cat_postcomp A f) p $==
fmap (cat_postcomp A f) q
      srapply Build_pHomotopy.
A, B, C: pType
f: B $-> C
g, h: A $-> B
p, q: g $-> h
r: p $== q
fmap (cat_postcomp A f) p == fmap (cat_postcomp A f) q
A, B, C: pType
f: B $-> C
g, h: A $-> B
p, q: g $-> h
r: p $== q
?p pt =
dpoint_eq (fmap (cat_postcomp A f) p) @
(dpoint_eq (fmap (cat_postcomp A f) q))^
      1: exact (fun _ => ap _ (r _)).
A, B, C: pType
f: B $-> C
g, h: A $-> B
p, q: g $-> h
r: p $== q
(fun x : A => ap (ap f) (r x)) pt =
dpoint_eq (fmap (cat_postcomp A f) p) @
(dpoint_eq (fmap (cat_postcomp A f) q))^
      by pelim r p q g h f.
    +
A, B, C: pType
f: B $-> C
forall a : A $-> B,
fmap (cat_postcomp A f) (Id a) $==
Id (cat_postcomp A f a) intros g.
A, B, C: pType
f: B $-> C
g: A $-> B
fmap (cat_postcomp A f) (Id g) $==
Id (cat_postcomp A f g)
      srapply Build_pHomotopy.
A, B, C: pType
f: B $-> C
g: A $-> B
fmap (cat_postcomp A f) (Id g) ==
Id (cat_postcomp A f g)
A, B, C: pType
f: B $-> C
g: A $-> B
?p pt =
dpoint_eq (fmap (cat_postcomp A f) (Id g)) @
(dpoint_eq (Id (cat_postcomp A f g)))^
      1: reflexivity.
A, B, C: pType
f: B $-> C
g: A $-> B
(fun x0 : A => 1) pt =
dpoint_eq (fmap (cat_postcomp A f) (Id g)) @
(dpoint_eq (Id (cat_postcomp A f g)))^
      by pelim g f.
    +
A, B, C: pType
f: B $-> C
forall (a b c : A $-> B) (f0 : a $-> b) (g : b $-> c),
fmap (cat_postcomp A f) (g $o f0) $==
fmap (cat_postcomp A f) g $o
fmap (cat_postcomp A f) f0 intros g h i p q.
A, B, C: pType
f: B $-> C
g, h, i: A $-> B
p: g $-> h
q: h $-> i
fmap (cat_postcomp A f) (q $o p) $==
fmap (cat_postcomp A f) q $o fmap (cat_postcomp A f) p
      srapply Build_pHomotopy.
A, B, C: pType
f: B $-> C
g, h, i: A $-> B
p: g $-> h
q: h $-> i
fmap (cat_postcomp A f) (q $o p) ==
fmap (cat_postcomp A f) q $o fmap (cat_postcomp A f) p
A, B, C: pType
f: B $-> C
g, h, i: A $-> B
p: g $-> h
q: h $-> i
?p pt =
dpoint_eq (fmap (cat_postcomp A f) (q $o p)) @
(dpoint_eq
   (fmap (cat_postcomp A f) q $o
    fmap (cat_postcomp A f) p))^
      1: cbn; exact (fun _ => ap_pp _ _ _).
A, B, C: pType
f: B $-> C
g, h, i: A $-> B
p: g $-> h
q: h $-> i
((fun x : A => ap_pp f (p x) (q x))
 :
 fmap (cat_postcomp A f) (q $o p) ==
 fmap (cat_postcomp A f) q $o
 fmap (cat_postcomp A f) p) pt =
dpoint_eq (fmap (cat_postcomp A f) (q $o p)) @
(dpoint_eq
   (fmap (cat_postcomp A f) q $o
    fmap (cat_postcomp A f) p))^
      by pelim p q g h i f.
  -
forall (a b c : pType) (f : a $-> b),
Is1Functor (cat_precomp c f) intros A B C f; napply Build_Is1Functor.
A, B, C: pType
f: A $-> B
forall (a b : B $-> C) (f0 g : a $-> b),
f0 $== g ->
fmap (cat_precomp C f) f0 $== fmap (cat_precomp C f) g
A, B, C: pType
f: A $-> B
forall a : B $-> C,
fmap (cat_precomp C f) (Id a) $==
Id (cat_precomp C f a)
A, B, C: pType
f: A $-> B
forall (a b c : B $-> C) (f0 : a $-> b) (g : b $-> c),
fmap (cat_precomp C f) (g $o f0) $==
fmap (cat_precomp C f) g $o fmap (cat_precomp C f) f0
    +
A, B, C: pType
f: A $-> B
forall (a b : B $-> C) (f0 g : a $-> b),
f0 $== g ->
fmap (cat_precomp C f) f0 $== fmap (cat_precomp C f) g intros g h p q r.
A, B, C: pType
f: A $-> B
g, h: B $-> C
p, q: g $-> h
r: p $== q
fmap (cat_precomp C f) p $== fmap (cat_precomp C f) q
      srapply Build_pHomotopy.
A, B, C: pType
f: A $-> B
g, h: B $-> C
p, q: g $-> h
r: p $== q
fmap (cat_precomp C f) p == fmap (cat_precomp C f) q
A, B, C: pType
f: A $-> B
g, h: B $-> C
p, q: g $-> h
r: p $== q
?p pt =
dpoint_eq (fmap (cat_precomp C f) p) @
(dpoint_eq (fmap (cat_precomp C f) q))^
      1: intro; exact (r _).
A, B, C: pType
f: A $-> B
g, h: B $-> C
p, q: g $-> h
r: p $== q
((fun x : A => r (f x))
 :
 fmap (cat_precomp C f) p == fmap (cat_precomp C f) q)
  pt =
dpoint_eq (fmap (cat_precomp C f) p) @
(dpoint_eq (fmap (cat_precomp C f) q))^
      by pelim f r p q g h.
    +
A, B, C: pType
f: A $-> B
forall a : B $-> C,
fmap (cat_precomp C f) (Id a) $==
Id (cat_precomp C f a) intros g.
A, B, C: pType
f: A $-> B
g: B $-> C
fmap (cat_precomp C f) (Id g) $==
Id (cat_precomp C f g)
      srapply Build_pHomotopy.
A, B, C: pType
f: A $-> B
g: B $-> C
fmap (cat_precomp C f) (Id g) ==
Id (cat_precomp C f g)
A, B, C: pType
f: A $-> B
g: B $-> C
?p pt =
dpoint_eq (fmap (cat_precomp C f) (Id g)) @
(dpoint_eq (Id (cat_precomp C f g)))^
      1: reflexivity.
A, B, C: pType
f: A $-> B
g: B $-> C
(fun x0 : A => 1) pt =
dpoint_eq (fmap (cat_precomp C f) (Id g)) @
(dpoint_eq (Id (cat_precomp C f g)))^
      by pelim f g.
    +
A, B, C: pType
f: A $-> B
forall (a b c : B $-> C) (f0 : a $-> b) (g : b $-> c),
fmap (cat_precomp C f) (g $o f0) $==
fmap (cat_precomp C f) g $o fmap (cat_precomp C f) f0 intros g h i p q.
A, B, C: pType
f: A $-> B
g, h, i: B $-> C
p: g $-> h
q: h $-> i
fmap (cat_precomp C f) (q $o p) $==
fmap (cat_precomp C f) q $o fmap (cat_precomp C f) p
      srapply Build_pHomotopy.
A, B, C: pType
f: A $-> B
g, h, i: B $-> C
p: g $-> h
q: h $-> i
fmap (cat_precomp C f) (q $o p) ==
fmap (cat_precomp C f) q $o fmap (cat_precomp C f) p
A, B, C: pType
f: A $-> B
g, h, i: B $-> C
p: g $-> h
q: h $-> i
?p pt =
dpoint_eq (fmap (cat_precomp C f) (q $o p)) @
(dpoint_eq
   (fmap (cat_precomp C f) q $o
    fmap (cat_precomp C f) p))^
      1: reflexivity.
A, B, C: pType
f: A $-> B
g, h, i: B $-> C
p: g $-> h
q: h $-> i
(fun x0 : A => 1) pt =
dpoint_eq (fmap (cat_precomp C f) (q $o p)) @
(dpoint_eq
   (fmap (cat_precomp C f) q $o
    fmap (cat_precomp C f) p))^
      by pelim f p q i g h.
  -
forall (a b c : pType) (f f' : a $-> b)
(g g' : b $-> c) (p : f $== f') (p' : g $== g'),
(p' $@R f) $@ (g' $@L p) $== (g $@L p) $@ (p' $@R f') intros A B C f g h k p q.
A, B, C: pType
f, g: A $-> B
h, k: B $-> C
p: f $== g
q: h $== k
(q $@R f) $@ (k $@L p) $== (h $@L p) $@ (q $@R g)
    snapply Build_pHomotopy.
A, B, C: pType
f, g: A $-> B
h, k: B $-> C
p: f $== g
q: h $== k
(q $@R f) $@ (k $@L p) == (h $@L p) $@ (q $@R g)
A, B, C: pType
f, g: A $-> B
h, k: B $-> C
p: f $== g
q: h $== k
?p pt =
dpoint_eq ((q $@R f) $@ (k $@L p)) @
(dpoint_eq ((h $@L p) $@ (q $@R g)))^
    +
A, B, C: pType
f, g: A $-> B
h, k: B $-> C
p: f $== g
q: h $== k
(q $@R f) $@ (k $@L p) == (h $@L p) $@ (q $@R g) intros x.
A, B, C: pType
f, g: A $-> B
h, k: B $-> C
p: f $== g
q: h $== k
x: A
((q $@R f) $@ (k $@L p)) x =
((h $@L p) $@ (q $@R g)) x
      exact (concat_Ap q _)^.
    +
A, B, C: pType
f, g: A $-> B
h, k: B $-> C
p: f $== g
q: h $== k
((fun x : A => (concat_Ap q (p x))^)
 :
 (q $@R f) $@ (k $@L p) == (h $@L p) $@ (q $@R g)) pt =
dpoint_eq ((q $@R f) $@ (k $@L p)) @
(dpoint_eq ((h $@L p) $@ (q $@R g)))^ by pelim p f g q h k.
  -
forall (a b c d : pType) (f : a $-> b) (g : b $-> c),
Is1Natural
  (fun x : c $-> d =>
   cat_precomp d f (cat_precomp d g x))
  (cat_precomp d (g $o f)) (cat_assoc f g) intros A B C D f g.
A, B, C, D: pType
f: A $-> B
g: B $-> C
Is1Natural
  (fun x : C $-> D =>
   cat_precomp D f (cat_precomp D g x))
  (cat_precomp D (g $o f)) (cat_assoc f g)
    snapply Build_Is1Natural.
A, B, C, D: pType
f: A $-> B
g: B $-> C
forall (a a' : C $-> D) (f0 : a $-> a'),
cat_assoc f g a' $o
fmap (cat_precomp D f o cat_precomp D g) f0 $==
fmap (cat_precomp D (g $o f)) f0 $o cat_assoc f g a
    intros r1 r2 s1.
A, B, C, D: pType
f: A $-> B
g: B $-> C
r1, r2: C $-> D
s1: r1 $-> r2
cat_assoc f g r2 $o
fmap (cat_precomp D f o cat_precomp D g) s1 $==
fmap (cat_precomp D (g $o f)) s1 $o cat_assoc f g r1
    srapply Build_pHomotopy.
A, B, C, D: pType
f: A $-> B
g: B $-> C
r1, r2: C $-> D
s1: r1 $-> r2
cat_assoc f g r2 $o
fmap (cat_precomp D f o cat_precomp D g) s1 ==
fmap (cat_precomp D (g $o f)) s1 $o cat_assoc f g r1
A, B, C, D: pType
f: A $-> B
g: B $-> C
r1, r2: C $-> D
s1: r1 $-> r2
?p pt =
dpoint_eq
  (cat_assoc f g r2 $o
   fmap (cat_precomp D f o cat_precomp D g) s1) @
(dpoint_eq
   (fmap (cat_precomp D (g $o f)) s1 $o
    cat_assoc f g r1))^
    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
A, B, C, D: pType
f: A $-> B
g: B $-> C
r1, r2: C $-> D
s1: r1 $-> r2
(fun x : A =>
 concat_p1
   (fmap (cat_precomp D f o cat_precomp D g) s1 x) @
 (concat_1p
    (fmap (cat_precomp D f o cat_precomp D g) s1 x))^)
  pt =
dpoint_eq
  (cat_assoc f g r2 $o
   fmap (cat_precomp D f o cat_precomp D g) s1) @
(dpoint_eq
   (fmap (cat_precomp D (g $o f)) s1 $o
    cat_assoc f g r1))^
    by pelim f g s1 r1 r2.
  -
forall (a b c d : pType) (f : a $-> b) (h : c $-> d),
Is1Natural
  (fun x : b $-> c =>
   cat_precomp d f (cat_postcomp b h x))
  (fun x : b $-> c =>
   cat_postcomp a h (cat_precomp c f x))
  (fun g : b $-> c => cat_assoc f g h) intros A B C D f g.
A, B, C, D: pType
f: A $-> B
g: C $-> D
Is1Natural
  (fun x : B $-> C =>
   cat_precomp D f (cat_postcomp B g x))
  (fun x : B $-> C =>
   cat_postcomp A g (cat_precomp C f x))
  (fun g0 : B $-> C => cat_assoc f g0 g)
    snapply Build_Is1Natural.
A, B, C, D: pType
f: A $-> B
g: C $-> D
forall (a a' : B $-> C) (f0 : a $-> a'),
(fun g0 : B $-> C => cat_assoc f g0 g) a' $o
fmap (cat_precomp D f o cat_postcomp B g) f0 $==
fmap (cat_postcomp A g o cat_precomp C f) f0 $o
(fun g0 : B $-> C => cat_assoc f g0 g) a
    intros r1 r2 s1.
A, B, C, D: pType
f: A $-> B
g: C $-> D
r1, r2: B $-> C
s1: r1 $-> r2
(fun g0 : B $-> C => cat_assoc f g0 g) r2 $o
fmap (cat_precomp D f o cat_postcomp B g) s1 $==
fmap (cat_postcomp A g o cat_precomp C f) s1 $o
(fun g0 : B $-> C => cat_assoc f g0 g) r1
    srapply Build_pHomotopy.
A, B, C, D: pType
f: A $-> B
g: C $-> D
r1, r2: B $-> C
s1: r1 $-> r2
(fun g0 : B $-> C => cat_assoc f g0 g) r2 $o
fmap (cat_precomp D f o cat_postcomp B g) s1 ==
fmap (cat_postcomp A g o cat_precomp C f) s1 $o
(fun g0 : B $-> C => cat_assoc f g0 g) r1
A, B, C, D: pType
f: A $-> B
g: C $-> D
r1, r2: B $-> C
s1: r1 $-> r2
?p pt =
dpoint_eq
  ((fun g0 : B $-> C => cat_assoc f g0 g) r2 $o
   fmap (cat_precomp D f o cat_postcomp B g) s1) @
(dpoint_eq
   (fmap (cat_postcomp A g o cat_precomp C f) s1 $o
    (fun g0 : B $-> C => cat_assoc f g0 g) r1))^
    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
A, B, C, D: pType
f: A $-> B
g: C $-> D
r1, r2: B $-> C
s1: r1 $-> r2
(fun x : A =>
 concat_p1
   (fmap (cat_precomp D f o cat_postcomp B g) s1 x) @
 (concat_1p
    (fmap (cat_precomp D f o cat_postcomp B g) s1 x))^)
  pt =
dpoint_eq
  ((fun g0 : B $-> C => cat_assoc f g0 g) r2 $o
   fmap (cat_precomp D f o cat_postcomp B g) s1) @
(dpoint_eq
   (fmap (cat_postcomp A g o cat_precomp C f) s1 $o
    (fun g0 : B $-> C => cat_assoc f g0 g) r1))^
    by pelim f s1 r1 r2 g.
  -
forall (a b c d : pType) (g : b $-> c) (h : c $-> d),
Is1Natural (cat_postcomp a (h $o g))
  (fun x : a $-> b =>
   cat_postcomp a h (cat_postcomp a g x))
  (fun f : a $-> b => cat_assoc f g h) intros A B C D f g.
A, B, C, D: pType
f: B $-> C
g: C $-> D
Is1Natural (cat_postcomp A (g $o f))
  (fun x : A $-> B =>
   cat_postcomp A g (cat_postcomp A f x))
  (fun f0 : A $-> B => cat_assoc f0 f g)
    snapply Build_Is1Natural.
A, B, C, D: pType
f: B $-> C
g: C $-> D
forall (a a' : A $-> B) (f0 : a $-> a'),
(fun f1 : A $-> B => cat_assoc f1 f g) a' $o
fmap (cat_postcomp A (g $o f)) f0 $==
fmap (cat_postcomp A g o cat_postcomp A f) f0 $o
(fun f1 : A $-> B => cat_assoc f1 f g) a
    intros r1 r2 s1.
A, B, C, D: pType
f: B $-> C
g: C $-> D
r1, r2: A $-> B
s1: r1 $-> r2
(fun f0 : A $-> B => cat_assoc f0 f g) r2 $o
fmap (cat_postcomp A (g $o f)) s1 $==
fmap (cat_postcomp A g o cat_postcomp A f) s1 $o
(fun f0 : A $-> B => cat_assoc f0 f g) r1
    srapply Build_pHomotopy.
A, B, C, D: pType
f: B $-> C
g: C $-> D
r1, r2: A $-> B
s1: r1 $-> r2
(fun f0 : A $-> B => cat_assoc f0 f g) r2 $o
fmap (cat_postcomp A (g $o f)) s1 ==
fmap (cat_postcomp A g o cat_postcomp A f) s1 $o
(fun f0 : A $-> B => cat_assoc f0 f g) r1
A, B, C, D: pType
f: B $-> C
g: C $-> D
r1, r2: A $-> B
s1: r1 $-> r2
?p pt =
dpoint_eq
  ((fun f0 : A $-> B => cat_assoc f0 f g) r2 $o
   fmap (cat_postcomp A (g $o f)) s1) @
(dpoint_eq
   (fmap (cat_postcomp A g o cat_postcomp A f) s1 $o
    (fun f0 : A $-> B => cat_assoc f0 f g) r1))^
    1: cbn; exact (fun _ => concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^).
A, B, C, D: pType
f: B $-> C
g: C $-> D
r1, r2: A $-> B
s1: r1 $-> r2
((fun x : A =>
  (concat_p1 (ap (g o f) (s1 x)) @
   ap_compose f g (s1 x)) @
  (concat_1p (ap g (ap f (s1 x))))^)
 :
 (fun f0 : A $-> B => cat_assoc f0 f g) r2 $o
 fmap (cat_postcomp A (g $o f)) s1 ==
 fmap (cat_postcomp A g o cat_postcomp A f) s1 $o
 (fun f0 : A $-> B => cat_assoc f0 f g) r1) pt =
dpoint_eq
  ((fun f0 : A $-> B => cat_assoc f0 f g) r2 $o
   fmap (cat_postcomp A (g $o f)) s1) @
(dpoint_eq
   (fmap (cat_postcomp A g o cat_postcomp A f) s1 $o
    (fun f0 : A $-> B => cat_assoc f0 f g) r1))^
    by pelim s1 r1 r2 f g.
  -
forall a b : pType,
Is1Natural (cat_postcomp a (Id b)) idmap cat_idl intros A B.
A, B: pType
Is1Natural (cat_postcomp A (Id B)) idmap cat_idl
    snapply Build_Is1Natural.
A, B: pType
forall (a a' : A $-> B) (f : a $-> a'),
cat_idl a' $o fmap (cat_postcomp A (Id B)) f $==
fmap idmap f $o cat_idl a
    intros r1 r2 s1.
A, B: pType
r1, r2: A $-> B
s1: r1 $-> r2
cat_idl r2 $o fmap (cat_postcomp A (Id B)) s1 $==
fmap idmap s1 $o cat_idl r1
    srapply Build_pHomotopy.
A, B: pType
r1, r2: A $-> B
s1: r1 $-> r2
cat_idl r2 $o fmap (cat_postcomp A (Id B)) s1 ==
fmap idmap s1 $o cat_idl r1
A, B: pType
r1, r2: A $-> B
s1: r1 $-> r2
?p pt =
dpoint_eq
  (cat_idl r2 $o fmap (cat_postcomp A (Id B)) s1) @
(dpoint_eq (fmap idmap s1 $o cat_idl r1))^
    1: exact (fun _ => concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
A, B: pType
r1, r2: A $-> B
s1: r1 $-> r2
(fun x : A =>
 (concat_p1 (ap idmap (s1 x)) @ ap_idmap (s1 x)) @
 (concat_1p (s1 x))^) pt =
dpoint_eq
  (cat_idl r2 $o fmap (cat_postcomp A (Id B)) s1) @
(dpoint_eq (fmap idmap s1 $o cat_idl r1))^
    by pelim s1 r1 r2.
  -
forall a b : pType,
Is1Natural (cat_precomp b (Id a)) idmap cat_idr intros A B.
A, B: pType
Is1Natural (cat_precomp B (Id A)) idmap cat_idr
    snapply Build_Is1Natural.
A, B: pType
forall (a a' : A $-> B) (f : a $-> a'),
cat_idr a' $o fmap (cat_precomp B (Id A)) f $==
fmap idmap f $o cat_idr a
    intros r1 r2 s1.
A, B: pType
r1, r2: A $-> B
s1: r1 $-> r2
cat_idr r2 $o fmap (cat_precomp B (Id A)) s1 $==
fmap idmap s1 $o cat_idr r1
    srapply Build_pHomotopy.
A, B: pType
r1, r2: A $-> B
s1: r1 $-> r2
cat_idr r2 $o fmap (cat_precomp B (Id A)) s1 ==
fmap idmap s1 $o cat_idr r1
A, B: pType
r1, r2: A $-> B
s1: r1 $-> r2
?p pt =
dpoint_eq
  (cat_idr r2 $o fmap (cat_precomp B (Id A)) s1) @
(dpoint_eq (fmap idmap s1 $o cat_idr r1))^
    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
A, B: pType
r1, r2: A $-> B
s1: r1 $-> r2
(fun x : A =>
 concat_p1 (fmap (cat_precomp B (Id A)) s1 x) @
 (concat_1p (fmap (cat_precomp B (Id A)) s1 x))^) pt =
dpoint_eq
  (cat_idr r2 $o fmap (cat_precomp B (Id A)) s1) @
(dpoint_eq (fmap idmap s1 $o cat_idr r1))^
    simpl; by pelim s1 r1 r2.
  -
forall (a b c d e : pType) (f : a $-> b) (g : b $-> c)
(h : c $-> d) (k : d $-> e),
k $@L cat_assoc f g h $o cat_assoc f (h $o g) k $o
cat_assoc g h k $@R f $==
cat_assoc (g $o f) h k $o cat_assoc f g (k $o h) intros A B C D E f g h j.
A, B, C, D, E: pType
f: A $-> B
g: B $-> C
h: C $-> D
j: D $-> E
j $@L cat_assoc f g h $o cat_assoc f (h $o g) j $o
cat_assoc g h j $@R f $==
cat_assoc (g $o f) h j $o cat_assoc f g (j $o h)
    srapply Build_pHomotopy.
A, B, C, D, E: pType
f: A $-> B
g: B $-> C
h: C $-> D
j: D $-> E
j $@L cat_assoc f g h $o cat_assoc f (h $o g) j $o
cat_assoc g h j $@R f ==
cat_assoc (g $o f) h j $o cat_assoc f g (j $o h)
A, B, C, D, E: pType
f: A $-> B
g: B $-> C
h: C $-> D
j: D $-> E
?p pt =
dpoint_eq
  (j $@L cat_assoc f g h $o cat_assoc f (h $o g) j $o
   cat_assoc g h j $@R f) @
(dpoint_eq
   (cat_assoc (g $o f) h j $o cat_assoc f g (j $o h)))^
    1: reflexivity.
A, B, C, D, E: pType
f: A $-> B
g: B $-> C
h: C $-> D
j: D $-> E
(fun x0 : A => 1) pt =
dpoint_eq
  (j $@L cat_assoc f g h $o cat_assoc f (h $o g) j $o
   cat_assoc g h j $@R f) @
(dpoint_eq
   (cat_assoc (g $o f) h j $o cat_assoc f g (j $o h)))^
    by pelim f g h j.
  -
forall (a b c : pType) (f : a $-> b) (g : b $-> c),
g $@L cat_idl f $o cat_assoc f (Id b) g $==
cat_idr g $@R f intros A B C f g.
A, B, C: pType
f: A $-> B
g: B $-> C
g $@L cat_idl f $o cat_assoc f (Id B) g $==
cat_idr g $@R f
    srapply Build_pHomotopy.
A, B, C: pType
f: A $-> B
g: B $-> C
g $@L cat_idl f $o cat_assoc f (Id B) g ==
cat_idr g $@R f
A, B, C: pType
f: A $-> B
g: B $-> C
?p pt =
dpoint_eq (g $@L cat_idl f $o cat_assoc f (Id B) g) @
(dpoint_eq (cat_idr g $@R f))^
    1: reflexivity.
A, B, C: pType
f: A $-> B
g: B $-> C
(fun x0 : A => 1) pt =
dpoint_eq (g $@L cat_idl f $o cat_assoc f (Id B) g) @
(dpoint_eq (cat_idr g $@R f))^
    by pelim f g.
Defined.

(** The forgetful map from [pType] to [Type] is a 0-functor *)
Instance is0functor_pointed_type : Is0Functor pointed_type.
Is0Functor pointed_type
Proof.
Is0Functor pointed_type
  apply Build_Is0Functor.
forall a b : pType, (a $-> b) -> a $-> b intros.
a, b: pType
f: a $-> b
a $-> b exact f.
Defined.

(** The forgetful map from [pType] to [Type] is a 1-functor *)
Instance is1functor_pointed_type : Is1Functor pointed_type.
Is1Functor pointed_type
Proof.
Is1Functor pointed_type
  apply Build_Is1Functor.
forall (a b : pType) (f g : a $-> b),
f $== g -> fmap pointed_type f $== fmap pointed_type g
forall a : pType, fmap pointed_type (Id a) $== Id a
forall (a b c : pType) (f : a $-> b) (g : b $-> c),
fmap pointed_type (g $o f) $==
fmap pointed_type g $o fmap pointed_type f
  +
forall (a b : pType) (f g : a $-> b),
f $== g -> fmap pointed_type f $== fmap pointed_type g intros ? ? ? ? h.
a, b: pType
f, g: a $-> b
h: f $== g
fmap pointed_type f $== fmap pointed_type g exact h.
  +
forall a : pType, fmap pointed_type (Id a) $== Id a intros.
a: pType
fmap pointed_type (Id a) $== Id a reflexivity.
  +
forall (a b c : pType) (f : a $-> b) (g : b $-> c),
fmap pointed_type (g $o f) $==
fmap pointed_type g $o fmap pointed_type f intros.
a, b, c: pType
f: a $-> b
g: b $-> c
fmap pointed_type (g $o f) $==
fmap pointed_type g $o fmap pointed_type f reflexivity.
Defined.

(** [pType] has binary products *)
Instance hasbinaryproducts_ptype : HasBinaryProducts pType.
HasBinaryProducts pType
Proof.
HasBinaryProducts pType
  intros X Y.
X, Y: pType
BinaryProduct X Y
  snapply Build_BinaryProduct.
X, Y: pType
pType
X, Y: pType
?cat_binprod' $-> X
X, Y: pType
?cat_binprod' $-> Y
X, Y: pType
forall z : pType,
(z $-> X) -> (z $-> Y) -> z $-> ?cat_binprod'
X, Y: pType
forall (z : pType) (f : z $-> X) (g : z $-> Y),
?cat_pr1 $o ?cat_binprod_corec z f g $== f
X, Y: pType
forall (z : pType) (f : z $-> X) (g : z $-> Y),
?cat_pr2 $o ?cat_binprod_corec z f g $== g
X, Y: pType
forall (z : pType) (f g : z $-> ?cat_binprod'),
?cat_pr1 $o f $== ?cat_pr1 $o g ->
?cat_pr2 $o f $== ?cat_pr2 $o g -> f $== g
  -
X, Y: pType
pType exact (X * Y).
  -
X, Y: pType
X * Y $-> X exact pfst.
  -
X, Y: pType
X * Y $-> Y exact psnd.
  -
X, Y: pType
forall z : pType,
(z $-> X) -> (z $-> Y) -> z $-> X * Y exact pprod_corec.
  -
X, Y: pType
forall (z : pType) (f : z $-> X) (g : z $-> Y),
pfst $o pprod_corec z f g $== f exact pprod_corec_beta_fst.
  -
X, Y: pType
forall (z : pType) (f : z $-> X) (g : z $-> Y),
psnd $o pprod_corec z f g $== g exact pprod_corec_beta_snd.
  -
X, Y: pType
forall (z : pType) (f g : z $-> X * Y),
pfst $o f $== pfst $o g ->
psnd $o f $== psnd $o g -> f $== g intros Z f g p q.
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
f $== g
    simpl.
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
f ==* g
    snapply Build_pHomotopy.
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
f == g
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
?p pt = dpoint_eq f @ (dpoint_eq g)^
    {
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
f == g intros a.
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
a: Z
f a = g a
      apply path_prod'; cbn.
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
a: Z
fst (f a) = fst (g a)
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
a: Z
snd (f a) = snd (g a)
      -
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
a: Z
fst (f a) = fst (g a) exact (p a).
      -
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
a: Z
snd (f a) = snd (g a) exact (q a). }
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
((fun a : Z =>
  path_prod' (p a : fst (f a) = fst (g a))
    (q a : snd (f a) = snd (g a)))
 :
 f == g) pt = dpoint_eq f @ (dpoint_eq g)^
    simpl.
X, Y, Z: pType
f, g: Z $-> X * Y
p: pfst $o f $== pfst $o g
q: psnd $o f $== psnd $o g
path_prod' (p pt) (q pt) =
dpoint_eq f @ (dpoint_eq g)^
    by pelim p q f g.
Defined.

(** [pType] has I-indexed product. *)
Instance hasallproducts_ptype `{Funext} : HasAllProducts pType.
H: Funext
HasAllProducts pType
Proof.
H: Funext
HasAllProducts pType
  intros I x.
H: Funext
I: Type
x: I -> pType
Product I x
  snapply Build_Product.
H: Funext
I: Type
x: I -> pType
pType
H: Funext
I: Type
x: I -> pType
forall i : I, ?cat_prod $-> x i
H: Funext
I: Type
x: I -> pType
forall z : pType,
(forall i : I, z $-> x i) -> z $-> ?cat_prod
H: Funext
I: Type
x: I -> pType
forall (z : pType) (f : forall i : I, z $-> x i)
(i : I), ?cat_pr i $o ?cat_prod_corec z f $== f i
H: Funext
I: Type
x: I -> pType
forall (z : pType) (f g : z $-> ?cat_prod),
(forall i : I, ?cat_pr i $o f $== ?cat_pr i $o g) ->
f $== g
  -
H: Funext
I: Type
x: I -> pType
pType exact (pproduct x).
  -
H: Funext
I: Type
x: I -> pType
forall i : I, pproduct x $-> x i exact pproduct_proj. 
  -
H: Funext
I: Type
x: I -> pType
forall z : pType,
(forall i : I, z $-> x i) -> z $-> pproduct x exact (pproduct_corec x).
  -
H: Funext
I: Type
x: I -> pType
forall (z : pType) (f : forall i : I, z $-> x i)
(i : I),
pproduct_proj i $o pproduct_corec x z f $== f i intros Z f i.
H: Funext
I: Type
x: I -> pType
Z: pType
f: forall i : I, Z $-> x i
i: I
pproduct_proj i $o pproduct_corec x Z f $== f i
    snapply Build_pHomotopy.
H: Funext
I: Type
x: I -> pType
Z: pType
f: forall i : I, Z $-> x i
i: I
pproduct_proj i $o pproduct_corec x Z f == f i
H: Funext
I: Type
x: I -> pType
Z: pType
f: forall i : I, Z $-> x i
i: I
?p pt =
dpoint_eq (pproduct_proj i $o pproduct_corec x Z f) @
(dpoint_eq (f i))^
    1: reflexivity.
H: Funext
I: Type
x: I -> pType
Z: pType
f: forall i : I, Z $-> x i
i: I
(fun x0 : Z => 1) pt =
dpoint_eq (pproduct_proj i $o pproduct_corec x Z f) @
(dpoint_eq (f i))^
    apply moveL_pV.
H: Funext
I: Type
x: I -> pType
Z: pType
f: forall i : I, Z $-> x i
i: I
1 @ dpoint_eq (f i) =
dpoint_eq (pproduct_proj i $o pproduct_corec x Z f)
    apply equiv_1p_q1.
H: Funext
I: Type
x: I -> pType
Z: pType
f: forall i : I, Z $-> x i
i: I
dpoint_eq (f i) =
ap (pproduct_proj i) (point_eq (pproduct_corec x Z f))
    exact (apD10_path_forall _ _ (fun a => point_eq (f a)) i)^.
  -
H: Funext
I: Type
x: I -> pType
forall (z : pType) (f g : z $-> pproduct x),
(forall i : I,
 pproduct_proj i $o f $== pproduct_proj i $o g) ->
f $== g intros Z f g p.
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
f $== g
    snapply Build_pHomotopy.
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
f == g
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
?p pt = dpoint_eq f @ (dpoint_eq g)^
    1: intros z; funext i; apply p.
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
((fun z : Z =>
  path_forall (f z) (g z)
    ((fun i : I =>
      let X := fun i0 : I => pointed_fun (p i0) in
      X i z)
     :
     f z == g z))
 :
 f == g) pt = dpoint_eq f @ (dpoint_eq g)^
    cbn; apply moveR_equiv_V.
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
(fun i : I => p i pt) =
apD10 (dpoint_eq f @ (dpoint_eq g)^)
    funext i.
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
i: I
p i pt = apD10 (dpoint_eq f @ (dpoint_eq g)^) i
    rhs napply ap_pp.
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
i: I
p i pt =
ap (pproduct_proj i) (dpoint_eq f) @
ap (pproduct_proj i) (dpoint_eq g)^
    lhs exact (dpoint_eq (p i)).
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
i: I
dpoint
  (pfam_phomotopy (pproduct_proj i $o f)
     (pproduct_proj i $o g)) =
ap (pproduct_proj i) (dpoint_eq f) @
ap (pproduct_proj i) (dpoint_eq g)^
    cbn; f_ap.
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
i: I
ap (fun x : forall a : I, x a => x i) (point_eq f) @ 1 =
ap (fun x : forall a : I, x a => x i) (dpoint_eq f)
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
i: I
(ap (fun x : forall a : I, x a => x i) (point_eq g) @
 1)^ =
ap (fun x : forall a : I, x a => x i) (dpoint_eq g)^
    +
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
i: I
ap (fun x : forall a : I, x a => x i) (point_eq f) @ 1 =
ap (fun x : forall a : I, x a => x i) (dpoint_eq f) apply concat_p1.
    +
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
i: I
(ap (fun x : forall a : I, x a => x i) (point_eq g) @
 1)^ =
ap (fun x : forall a : I, x a => x i) (dpoint_eq g)^ rhs napply (ap_V _ (dpoint_eq g)).
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
i: I
(ap (fun x : forall a : I, x a => x i) (point_eq g) @
 1)^ =
(ap (fun x : forall a : I, x a => x i) (dpoint_eq g))^
      apply inverse2.
H: Funext
I: Type
x: I -> pType
Z: pType
f, g: Z $-> pproduct x
p: forall i : I,
pproduct_proj i $o f $== pproduct_proj i $o g
i: I
ap (fun x : forall a : I, x a => x i) (point_eq g) @ 1 =
ap (fun x : forall a : I, x a => x i) (dpoint_eq g)
      apply concat_p1.
Defined.

(** Some higher homotopies *)

(** Horizontal composition of homotopies. *)
Notation "p @@* q" := (p $@@ q).

(** ** Funext for pointed types and direct consequences. *)

(** By funext pointed homotopies are equivalent to paths *)
Definition equiv_path_pforall `{Funext} {A : pType}
  {P : pFam A} (f g : pForall A P)
  : (f ==* g) <~> (f = g).
H: Funext
A: pType
P: pFam A
f, g: pForall A P
f ==* g <~> f = g
Proof.
H: Funext
A: pType
P: pFam A
f, g: pForall A P
f ==* g <~> f = g
  refine (_ oE (issig_phomotopy f g)^-1).
H: Funext
A: pType
P: pFam A
f, g: pForall A P
{p : f == g & p pt = dpoint_eq f @ (dpoint_eq g)^} <~>
f = g
  revert f g; apply (equiv_path_issig_contr (issig_pforall A P)).
H: Funext
A: pType
P: pFam A
forall b : {f : forall x : A, P x & f pt = dpoint P},
{p : issig_pforall A P b == issig_pforall A P b &
p pt =
dpoint_eq (issig_pforall A P b) @
(dpoint_eq (issig_pforall A P b))^}
H: Funext
A: pType
P: pFam A
forall b1 : {f : forall x : A, P x & f pt = dpoint P},
Contr
  {b2 : {f : forall x : A, P x & f pt = dpoint P} &
  {p : issig_pforall A P b1 == issig_pforall A P b2 &
  p pt =
  dpoint_eq (issig_pforall A P b1) @
  (dpoint_eq (issig_pforall A P b2))^}}
  {
H: Funext
A: pType
P: pFam A
forall b : {f : forall x : A, P x & f pt = dpoint P},
{p : issig_pforall A P b == issig_pforall A P b &
p pt =
dpoint_eq (issig_pforall A P b) @
(dpoint_eq (issig_pforall A P b))^} intros [f feq]; cbn.
H: Funext
A: pType
P: pFam A
f: forall x : A, P x
feq: f pt = dpoint P
{p : f == f & p pt = feq @ feq^}
    exists (fun a => 1%path).
H: Funext
A: pType
P: pFam A
f: forall x : A, P x
feq: f pt = dpoint P
1 = feq @ feq^
    exact (concat_pV _)^. }
H: Funext
A: pType
P: pFam A
forall b1 : {f : forall x : A, P x & f pt = dpoint P},
Contr
  {b2 : {f : forall x : A, P x & f pt = dpoint P} &
  {p : issig_pforall A P b1 == issig_pforall A P b2 &
  p pt =
  dpoint_eq (issig_pforall A P b1) @
  (dpoint_eq (issig_pforall A P b2))^}}
  intros [f feq]; cbn.
H: Funext
A: pType
P: pFam A
f: forall x : A, P x
feq: f pt = dpoint P
Contr
  {b2 : {f : forall x : A, P x & f pt = dpoint P} &
  {p : f == b2.1 & p pt = feq @ (b2.2)^}}
  contr_sigsig f (fun a:A => idpath (f a)); cbn.
H: Funext
A: pType
P: pFam A
f: forall x : A, P x
feq: f pt = dpoint P
Contr {y : f pt = dpoint P & 1 = feq @ y^}
  refine (contr_equiv' {feq' : f (point A) = dpoint P & feq = feq'} _).
H: Funext
A: pType
P: pFam A
f: forall x : A, P x
feq: f pt = dpoint P
{feq' : f pt = dpoint P & feq = feq'} <~>
{y : f pt = dpoint P & 1 = feq @ y^}
  refine (equiv_functor_sigma' (equiv_idmap _) _); intros p.
H: Funext
A: pType
P: pFam A
f: forall x : A, P x
feq, p: f pt = dpoint P
feq = p <~> 1 = feq @ (1%equiv p)^
  refine (_^-1 oE equiv_path_inverse _ _).
H: Funext
A: pType
P: pFam A
f: forall x : A, P x
feq, p: f pt = dpoint P
1 = feq @ (1%equiv p)^ <~> p = feq
  apply equiv_moveR_1M.
Defined.

Definition path_pforall `{Funext} {A : pType} {P : pFam A} {f g : pForall A P}
  : (f ==* g) -> (f = g) := equiv_path_pforall f g.

(** We note that the inverse of [path_pforall] computes definitionally on reflexivity, and hence [path_pforall] itself computes typally so. *)
Definition equiv_inverse_path_pforall_1 `{Funext} {A : pType} {P : pFam A} (f : pForall A P)
  : (equiv_path_pforall f f)^-1%equiv 1%path = reflexivity f
  := 1.

Definition path_pforall_1 `{Funext} {A : pType} {P : pFam A} {f : pForall A P}
  : equiv_path_pforall _ _ (reflexivity f) = 1%path
  := moveR_equiv_M _ _ (equiv_inverse_path_pforall_1 f)^.

(** Here is the inverse map without assuming funext *)
Definition phomotopy_path {A : pType} {P : pFam A} {f g : pForall A P}
  : (f = g) -> (f ==* g) := ltac:(by intros []).

(** And we prove that it agrees with the inverse of [equiv_path_pforall] *)
Definition path_equiv_path_pforall_phomotopy_path `{Funext} {A : pType}
  {P : pFam A} {f g : pForall A P}
  : phomotopy_path (f:=f) (g:=g) = (equiv_path_pforall f g)^-1%equiv
  := ltac:(by funext []).

(** TODO: The next few results could be proven for [GpdHom_path] in any WildCat. *)

(** [phomotopy_path] sends concatenation to composition of pointed homotopies.*)
Definition phomotopy_path_pp {A : pType} {P : pFam A}
  {f g h : pForall A P} (p : f = g) (q : g = h)
  : phomotopy_path (p @ q) ==* phomotopy_path p @* phomotopy_path q.
A: pType
P: pFam A
f, g, h: pForall A P
p: f = g
q: g = h
phomotopy_path (p @ q) ==*
phomotopy_path p @* phomotopy_path q
Proof.
A: pType
P: pFam A
f, g, h: pForall A P
p: f = g
q: g = h
phomotopy_path (p @ q) ==*
phomotopy_path p @* phomotopy_path q
  induction p.
A: pType
P: pFam A
f, h: pForall A P
q: f = h
phomotopy_path (1 @ q) ==*
phomotopy_path 1 @* phomotopy_path q induction q.
A: pType
P: pFam A
f: pForall A P
phomotopy_path (1 @ 1) ==*
phomotopy_path 1 @* phomotopy_path 1 symmetry.
A: pType
P: pFam A
f: pForall A P
phomotopy_path 1 @* phomotopy_path 1 ==*
phomotopy_path (1 @ 1) apply phomotopy_compose_p1.
Defined.

(** ** [phomotopy_path] respects 2-cells. *)
Definition phomotopy_path2 {A : pType} {P : pFam A}
  {f g : pForall A P} {p p' : f = g} (q : p = p')
  : phomotopy_path p ==* phomotopy_path p'.
A: pType
P: pFam A
f, g: pForall A P
p, p': f = g
q: p = p'
phomotopy_path p ==* phomotopy_path p'
Proof.
A: pType
P: pFam A
f, g: pForall A P
p, p': f = g
q: p = p'
phomotopy_path p ==* phomotopy_path p'
  induction q.
A: pType
P: pFam A
f, g: pForall A P
p: f = g
phomotopy_path p ==* phomotopy_path p reflexivity.
Defined.

(** [phomotopy_path] sends inverses to inverses.*)
Definition phomotopy_path_V {A : pType} {P : pFam A}
  {f g : pForall A P} (p : f = g)
  : phomotopy_path (p^) ==* (phomotopy_path p)^*.
A: pType
P: pFam A
f, g: pForall A P
p: f = g
phomotopy_path p^ ==* (phomotopy_path p)^*
Proof.
A: pType
P: pFam A
f, g: pForall A P
p: f = g
phomotopy_path p^ ==* (phomotopy_path p)^*
  induction p.
A: pType
P: pFam A
f: pForall A P
phomotopy_path 1^ ==* (phomotopy_path 1)^* simpl.
A: pType
P: pFam A
f: pForall A P
phomotopy_reflexive' f ==* (phomotopy_reflexive' f)^* symmetry.
A: pType
P: pFam A
f: pForall A P
(phomotopy_reflexive' f)^* ==* phomotopy_reflexive' f exact gpd_rev_1.
Defined.

(** Since pointed homotopies are equivalent to equalities, we can act as if they are paths and define a path induction for them. *)
Definition phomotopy_ind `{H0 : Funext} {A : pType} {P : pFam A}
  {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> Type)
  (q : Q k (reflexivity k)) (k' : pForall A P)
  : forall (H : k ==* k'), Q k' H.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P, k ==* k' -> Type
q: Q k (reflexivity k)
k': pForall A P
forall H : k ==* k', Q k' H
Proof.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P, k ==* k' -> Type
q: Q k (reflexivity k)
k': pForall A P
forall H : k ==* k', Q k' H
  equiv_intro (equiv_path_pforall k k')^-1%equiv p.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P, k ==* k' -> Type
q: Q k (reflexivity k)
k': pForall A P
p: k = k'
Q k' ((equiv_path_pforall k k')^-1%equiv p)
  induction p.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P, k ==* k' -> Type
q: Q k (reflexivity k)
Q k ((equiv_path_pforall k k)^-1%equiv 1)
  exact q.
Defined.

(** Sometimes you have a goal with both a pointed homotopy [H] and [path_pforall H].  This is an induction principle that allows us to replace both of them by reflexivity at the same time. *)
Definition phomotopy_ind' `{H0 : Funext} {A : pType} {P : pFam A}
  {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> (k = k') -> Type)
  (q : Q k (reflexivity k) 1 % path) (k' : pForall A P) (H : k ==* k')
  (p : k = k') (r : path_pforall H = p)
  : Q k' H p.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P,
k ==* k' -> k = k' -> Type
q: Q k (reflexivity k) 1
k': pForall A P
H: k ==* k'
p: k = k'
r: path_pforall H = p
Q k' H p
Proof.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P,
k ==* k' -> k = k' -> Type
q: Q k (reflexivity k) 1
k': pForall A P
H: k ==* k'
p: k = k'
r: path_pforall H = p
Q k' H p
  induction r.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P,
k ==* k' -> k = k' -> Type
q: Q k (reflexivity k) 1
k': pForall A P
H: k ==* k'
Q k' H (path_pforall H)
  revert k' H.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P,
k ==* k' -> k = k' -> Type
q: Q k (reflexivity k) 1
forall (k' : pForall A P) (H : k ==* k'),
Q k' H (path_pforall H)
  rapply phomotopy_ind.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P,
k ==* k' -> k = k' -> Type
q: Q k (reflexivity k) 1
Q k (reflexivity k) (path_pforall (reflexivity k))
  exact (transport (Q _ (reflexivity _)) path_pforall_1^ q).
Defined.

Definition phomotopy_ind_1 `{H0 : Funext} {A : pType} {P : pFam A}
  {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> Type)
  (q : Q k (reflexivity k)) :
  phomotopy_ind Q q k (reflexivity k) = q.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P, k ==* k' -> Type
q: Q k (reflexivity k)
phomotopy_ind Q q k (reflexivity k) = q
Proof.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P, k ==* k' -> Type
q: Q k (reflexivity k)
phomotopy_ind Q q k (reflexivity k) = q
  change (reflexivity k) with ((equiv_path_pforall k k)^-1%equiv (idpath k)).
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P, k ==* k' -> Type
q: Q k (reflexivity k)
phomotopy_ind Q q k
  ((equiv_path_pforall k k)^-1%equiv 1) = q
  apply equiv_ind_comp.
Defined.

Definition phomotopy_ind_1' `{H0 : Funext} {A : pType} {P : pFam A}
  {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> (k = k') -> Type)
  (q : Q k (reflexivity k) 1 % path)
  : phomotopy_ind' Q q k (reflexivity k) (path_pforall (reflexivity k)) (1 % path)
  = transport (Q k (reflexivity k)) path_pforall_1^ q.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P,
k ==* k' -> k = k' -> Type
q: Q k (reflexivity k) 1
phomotopy_ind' Q q k (reflexivity k)
  (path_pforall (reflexivity k)) 1 =
transport (Q k (reflexivity k)) path_pforall_1^ q
Proof.
H0: Funext
A: pType
P: pFam A
k: pForall A P
Q: forall k' : pForall A P,
k ==* k' -> k = k' -> Type
q: Q k (reflexivity k) 1
phomotopy_ind' Q q k (reflexivity k)
  (path_pforall (reflexivity k)) 1 =
transport (Q k (reflexivity k)) path_pforall_1^ q
  srapply phomotopy_ind_1.
Defined.

(** Every homotopy between pointed maps of sets is a pointed homotopy. *)
Definition phomotopy_homotopy_hset {X Y : pType} `{IsHSet Y} {f g : X ->* Y} (h : f == g)
  : f ==* g.
X, Y: pType
IsHSet0: IsHSet Y
f, g: X ->* Y
h: f == g
f ==* g
Proof.
X, Y: pType
IsHSet0: IsHSet Y
f, g: X ->* Y
h: f == g
f ==* g
  apply (Build_pHomotopy h).
X, Y: pType
IsHSet0: IsHSet Y
f, g: X ->* Y
h: f == g
h pt = dpoint_eq f @ (dpoint_eq g)^
  apply path_ishprop.
Defined.

(** Pointed homotopies in a set form an HProp. *)
Instance ishprop_phomotopy_hset `{Funext} {X Y : pType} `{IsHSet Y} (f g : X ->* Y)
  : IsHProp (f ==* g)
  := inO_equiv_inO' (O:=Tr (-1)) _ (issig_phomotopy f g).

(** ** Operations on equivalences needed to make [pType] a wild category with equivalences *)

(** The inverse equivalence of a pointed equivalence is again a pointed equivalence *)
Definition pequiv_inverse {A B} (f : A <~>* B) : B <~>* A.
A, B: pType
f: A <~>* B
B <~>* A
Proof.
A, B: pType
f: A <~>* B
B <~>* A
  snapply Build_pEquiv.
A, B: pType
f: A <~>* B
B ->* A
A, B: pType
f: A <~>* B
IsEquiv ?pointed_equiv_fun
  1: apply (Build_pMap f^-1).
A, B: pType
f: A <~>* B
f^-1 pt = pt
A, B: pType
f: A <~>* B
IsEquiv (Build_pMap f^-1 ?Goal)
  1: apply moveR_equiv_V; symmetry; apply point_eq.
A, B: pType
f: A <~>* B
IsEquiv
  (Build_pMap f^-1 (moveR_equiv_V pt pt (point_eq f)^))
  exact _.
Defined.

(* A pointed equivalence is a section of its inverse *)
Definition peissect {A B : pType} (f : A <~>* B)
  : (pequiv_inverse f) o* f ==* pmap_idmap.
A, B: pType
f: A <~>* B
pequiv_inverse f o* f ==* pmap_idmap
Proof.
A, B: pType
f: A <~>* B
pequiv_inverse f o* f ==* pmap_idmap
  srefine (Build_pHomotopy _ _).
A, B: pType
f: A <~>* B
pequiv_inverse f o* f == pmap_idmap
A, B: pType
f: A <~>* B
?p pt =
dpoint_eq (pequiv_inverse f o* f) @
(dpoint_eq pmap_idmap)^
  1: exact (eissect f).
A, B: pType
f: A <~>* B
eissect f pt =
dpoint_eq (pequiv_inverse f o* f) @
(dpoint_eq pmap_idmap)^
  simpl.
A, B: pType
f: A <~>* B
eissect f pt =
(ap f^-1 (point_eq f) @
 moveR_equiv_V pt pt (point_eq f)^) @ 1 unfold moveR_equiv_V.
A, B: pType
f: A <~>* B
eissect f pt =
(ap f^-1 (point_eq f) @
 (ap f^-1 (point_eq f)^ @ eissect f pt)) @ 1
  pointed_reduce.
A: Type
point0: IsPointed A
B: Type
f: A -> B
iseq: IsEquiv f
eissect f point0 = (1 @ (1 @ eissect f point0)) @ 1
  symmetry.
A: Type
point0: IsPointed A
B: Type
f: A -> B
iseq: IsEquiv f
(1 @ (1 @ eissect f point0)) @ 1 = eissect f point0
  exact (concat_p1 _ @ concat_1p _ @ concat_1p _).
Defined.

(* A pointed equivalence is a retraction of its inverse *)
Definition peisretr {A B : pType} (f : A <~>* B)
  : f o* (pequiv_inverse f) ==* pmap_idmap.
A, B: pType
f: A <~>* B
f o* pequiv_inverse f ==* pmap_idmap
Proof.
A, B: pType
f: A <~>* B
f o* pequiv_inverse f ==* pmap_idmap
  srefine (Build_pHomotopy _ _).
A, B: pType
f: A <~>* B
f o* pequiv_inverse f == pmap_idmap
A, B: pType
f: A <~>* B
?p pt =
dpoint_eq (f o* pequiv_inverse f) @
(dpoint_eq pmap_idmap)^
  1: exact (eisretr f).
A, B: pType
f: A <~>* B
eisretr f pt =
dpoint_eq (f o* pequiv_inverse f) @
(dpoint_eq pmap_idmap)^
  pointed_reduce.
A: Type
point0: IsPointed A
B: Type
f: A -> B
iseq: IsEquiv f
eisretr f (f point0) =
(ap f (moveR_equiv_V (f point0) point0 1) @ 1) @ 1
  unfold moveR_equiv_V.
A: Type
point0: IsPointed A
B: Type
f: A -> B
iseq: IsEquiv f
eisretr f (f point0) =
(ap f (ap f^-1 1 @ eissect f point0) @ 1) @ 1
  refine (eisadj f _ @ _).
A: Type
point0: IsPointed A
B: Type
f: A -> B
iseq: IsEquiv f
ap f (eissect f point0) =
(ap f (ap f^-1 1 @ eissect f point0) @ 1) @ 1
  symmetry.
A: Type
point0: IsPointed A
B: Type
f: A -> B
iseq: IsEquiv f
(ap f (ap f^-1 1 @ eissect f point0) @ 1) @ 1 =
ap f (eissect f point0)
  exact (concat_p1 _ @ concat_p1 _ @ ap _ (concat_1p _)).
Defined.

(** Univalence for pointed types *)
Definition equiv_path_ptype `{Univalence} (A B : pType@{u}) : A <~>* B <~> A = B.
H: Univalence
A, B: pType
(A <~>* B) <~> A = B
Proof.
H: Univalence
A, B: pType
(A <~>* B) <~> A = B
  refine (equiv_path_from_contr A (fun C => A <~>* C) pequiv_pmap_idmap _ B).
H: Univalence
A, B: pType
Contr {y : pType & A <~>* y}
  napply (contr_equiv' { X : Type@{u} & { f : A <~> X & {x : X & f pt = x} }}).
H: Univalence
A, B: pType
{X : Type & {f : A <~> X & {x : X & f pt = x}}} <~>
{y : pType & A <~>* y}
H: Univalence
A, B: pType
Contr {X : Type & {f : A <~> X & {x : X & f pt = x}}}
  1: make_equiv.
H: Univalence
A, B: pType
Contr {X : Type & {f : A <~> X & {x : X & f pt = x}}}
  rapply (contr_equiv' { X : Type@{u} &  A <~> X }).
H: Univalence
A, B: pType
{X : Type & A <~> X} <~>
{X : Type & {f : A <~> X & {x : X & f pt = x}}}
  napply equiv_functor_sigma_id; intro X; symmetry.
H: Univalence
A, B: pType
X: Type
{f : A <~> X & {x : X & f pt = x}} <~> (A <~> X)
  rapply equiv_sigma_contr.
  (** If you replace the type in the second line with { Xf : {X : Type & A <~> X} & {x : Xf.1 & Xf.2 pt = x} }, then the third line completes the proof, but that results in an extra universe variable. *)
Defined.

Definition path_ptype `{Univalence} {A B : pType} : (A <~>* B) -> A = B
  := equiv_path_ptype A B.

(** The inverse map can be defined without Univalence. *)
Definition pequiv_path {A B : pType} (p : A = B) : (A <~>* B)
  := match p with idpath => pequiv_pmap_idmap end.

(** This just confirms that it is definitionally the inverse map. *)
Definition pequiv_path_equiv_path_ptype_inverse `{Univalence} {A B : pType}
  : @pequiv_path A B = (equiv_path_ptype A B)^-1
  := idpath.

Instance isequiv_pequiv_path `{Univalence} {A B : pType}
  : IsEquiv (@pequiv_path A B)
  := isequiv_inverse (equiv_path_ptype A B).

(** Two pointed equivalences are equal if their underlying pointed functions are equal. This requires [Funext] for knowing that [IsEquiv] is an [HProp]. *)
Definition equiv_path_pequiv' `{Funext} {A B : pType} (f g : A <~>* B)
  : (f = g :> (A ->* B)) <~> (f = g :> (A <~>* B)).
H: Funext
A, B: pType
f, g: A <~>* B
f = g <~> f = g
Proof.
H: Funext
A, B: pType
f, g: A <~>* B
f = g <~> f = g
  refine ((equiv_ap' (issig_pequiv A B)^-1%equiv f g)^-1%equiv oE _); cbn.
H: Funext
A, B: pType
f, g: A <~>* B
f = g <~>
(f; pointed_isequiv A B f) =
(g; pointed_isequiv A B g)
  match goal with |- _ <~> ?F = ?G => exact (equiv_path_sigma_hprop F G) end.
Defined.

(** Two pointed equivalences are equal if their underlying pointed functions are pointed homotopic. *)
Definition equiv_path_pequiv `{Funext} {A B : pType} (f g : A <~>* B)
  : (f ==* g) <~> (f = g)
  := equiv_path_pequiv' f g oE equiv_path_pforall f g.

Definition path_pequiv `{Funext} {A B : pType} (f g : A <~>* B)
  : (f ==* g) -> (f = g)
  := equiv_path_pequiv f g.

Definition equiv_phomotopy_concat_l `{Funext} {A B : pType}
  (f g h : A ->* B) (K : g ==* f)
  : f ==* h <~> g ==* h.
H: Funext
A, B: pType
f, g, h: A ->* B
K: g ==* f
f ==* h <~> g ==* h
Proof.
H: Funext
A, B: pType
f, g, h: A ->* B
K: g ==* f
f ==* h <~> g ==* h
  refine ((equiv_path_pforall _ _)^-1%equiv oE _ oE equiv_path_pforall _ _).
H: Funext
A, B: pType
f, g, h: A ->* B
K: g ==* f
f = h <~> g = h
  rapply equiv_concat_l.
H: Funext
A, B: pType
f, g, h: A ->* B
K: g ==* f
g = f
  apply equiv_path_pforall.
H: Funext
A, B: pType
f, g, h: A ->* B
K: g ==* f
g ==* f
  exact K.
Defined.

(** Under funext, [pType] has morphism extensionality *)
Instance hasmorext_ptype `{Funext} : HasMorExt pType.
H: Funext
HasMorExt pType
Proof.
H: Funext
HasMorExt pType
  intros A B f g.
H: Funext
A, B: pType
f, g: A $-> B
IsEquiv GpdHom_path
  refine (isequiv_homotopic (equiv_path_pforall f g)^-1%equiv _).
H: Funext
A, B: pType
f, g: A $-> B
(equiv_path_pforall f g)^-1%equiv == GpdHom_path
  intros []; reflexivity.
Defined.

(** [pType] has equivalences *)
Instance hasequivs_ptype : HasEquivs pType.
HasEquivs pType
Proof.
HasEquivs pType
  stapply (
    Build_HasEquivs _ _ _ _ _ pEquiv (fun A B f => IsEquiv f));
  intros A B f; cbn; intros.
A, B: pType
f: A <~>* B
A ->* B
A, B: pType
f: A <~>* B
IsEquiv ?Goal
A, B: pType
f: A $-> B
X: IsEquiv f
A <~>* B
A, B: pType
f: A $-> B
fe: IsEquiv f
?Goal@{f:=(fun H : IsEquiv f => ?Goal4@{X:=H}) fe} ==*
f
A, B: pType
f: A <~>* B
B ->* A
A, B: pType
f: A <~>* B
?Goal1 o* ?Goal ==* pmap_idmap
A, B: pType
f: A <~>* B
?Goal o* ?Goal1 ==* pmap_idmap
A, B: pType
f: A $-> B
g: B ->* A
r: f o* g ==* pmap_idmap
s: g o* f ==* pmap_idmap
IsEquiv f
  -
A, B: pType
f: A <~>* B
A ->* B exact f.
  -
A, B: pType
f: A <~>* B
IsEquiv f exact _.
  -
A, B: pType
f: A $-> B
X: IsEquiv f
A <~>* B exact (Build_pEquiv f _).
  -
A, B: pType
f: A $-> B
fe: IsEquiv f
(fun H : IsEquiv f =>
 {| pointed_equiv_fun := f; pointed_isequiv := H |})
  fe ==* f reflexivity.
  -
A, B: pType
f: A <~>* B
B ->* A exact (pequiv_inverse f).
  -
A, B: pType
f: A <~>* B
pequiv_inverse f o* f ==* pmap_idmap apply peissect.
  -
A, B: pType
f: A <~>* B
f o* pequiv_inverse f ==* pmap_idmap cbn.
A, B: pType
f: A <~>* B
f
o* Build_pMap f^-1 (moveR_equiv_V pt pt (point_eq f)^) ==*
pmap_idmap exact (peisretr f).
  -
A, B: pType
f: A $-> B
g: B ->* A
r: f o* g ==* pmap_idmap
s: g o* f ==* pmap_idmap
IsEquiv f rapply (isequiv_adjointify f g).
A, B: pType
f: A $-> B
g: B ->* A
r: f o* g ==* pmap_idmap
s: g o* f ==* pmap_idmap
(fun x : B => f (g x)) == idmap
A, B: pType
f: A $-> B
g: B ->* A
r: f o* g ==* pmap_idmap
s: g o* f ==* pmap_idmap
(fun x : A => g (f x)) == idmap
    +
A, B: pType
f: A $-> B
g: B ->* A
r: f o* g ==* pmap_idmap
s: g o* f ==* pmap_idmap
(fun x : B => f (g x)) == idmap intros x; exact (r x).
    +
A, B: pType
f: A $-> B
g: B ->* A
r: f o* g ==* pmap_idmap
s: g o* f ==* pmap_idmap
(fun x : A => g (f x)) == idmap intros x; exact (s x).
Defined.

Instance hasmorext_core_ptype `{Funext} : HasMorExt (core pType).
H: Funext
HasMorExt (core pType)
Proof.
H: Funext
HasMorExt (core pType)
  rapply hasmorext_core.
H: Funext
forall (x y : core pType)
(f g : uncore x $<~> uncore y), IsEquiv (ap cate_fun)
  intros A B f g.
H: Funext
A, B: core pType
f, g: uncore A $<~> uncore B
IsEquiv (ap cate_fun)
  snapply isequiv_homotopic'.
H: Funext
A, B: core pType
f, g: uncore A $<~> uncore B
f = g <~> f = g
H: Funext
A, B: core pType
f, g: uncore A $<~> uncore B
?f == ap cate_fun
  1: exact (equiv_path_pequiv' f g)^-1%equiv.
H: Funext
A, B: core pType
f, g: uncore A $<~> uncore B
(equiv_path_pequiv' f g)^-1%equiv == ap cate_fun
  by intros [].
Defined.

(** [pType] is a univalent 1-coherent 1-category *)
Instance isunivalent_ptype `{Univalence} : IsUnivalent1Cat pType.
H: Univalence
IsUnivalent1Cat pType
Proof.
H: Univalence
IsUnivalent1Cat pType
  intros A B.
H: Univalence
A, B: pType
IsEquiv (cat_equiv_path A B)
  (* [cate_equiv_path] is almost definitionally equal to [pequiv_path].  Both are defined by path induction, sending [idpath A] to [id_cate A] and [pequiv_pmap_idmap A], respectively.  [id_cate A] is almost definitionally equal to [pequiv_pmap_idmap A], except that the former uses [catie_adjointify], so the adjoint law is different. However, the underlying pointed maps are definitionally equal. *)
  refine (isequiv_homotopic pequiv_path _).
H: Univalence
A, B: pType
pequiv_path == cat_equiv_path A B
  intros [].
H: Univalence
A, B: pType
pequiv_path 1 = cat_equiv_path A A 1
  apply equiv_path_pequiv'.  (* Change to equality as pointed functions. *)
H: Univalence
A, B: pType
pequiv_path 1 = cat_equiv_path A A 1
  reflexivity.
Defined.

(** The free base point added to a type. This is in fact a functor and left adjoint to the forgetful functor [pType] to [Type]. *)
Definition pointify (S : Type) : pType := [S + Unit, inr tt].

Instance is0functor_pointify : Is0Functor pointify.
Is0Functor pointify
Proof.
Is0Functor pointify
  apply Build_Is0Functor.
forall a b : Type,
(a $-> b) -> pointify a $-> pointify b
  intros A B f.
A, B: Type
f: A $-> B
pointify A $-> pointify B
  srapply Build_pMap.
A, B: Type
f: A $-> B
pointify A -> pointify B
A, B: Type
f: A $-> B
?f pt = pt
  1: exact (functor_sum f idmap).
A, B: Type
f: A $-> B
functor_sum f idmap pt = pt
  reflexivity.
Defined.

(** [pointify] is left adjoint to forgetting the basepoint in the following sense *)
Theorem equiv_pointify_map `{Funext} (A : Type) (X : pType)
  : (pointify A ->* X) <~> (A -> X).
H: Funext
A: Type
X: pType
(pointify A ->* X) <~> (A -> X)
Proof.
H: Funext
A: Type
X: pType
(pointify A ->* X) <~> (A -> X)
  snapply equiv_adjointify.
H: Funext
A: Type
X: pType
(pointify A ->* X) -> A -> X
H: Funext
A: Type
X: pType
(A -> X) -> pointify A ->* X
H: Funext
A: Type
X: pType
?f o ?g == idmap
H: Funext
A: Type
X: pType
?g o ?f == idmap
  1: exact (fun f => f o inl).
H: Funext
A: Type
X: pType
(A -> X) -> pointify A ->* X
H: Funext
A: Type
X: pType
(fun f : pointify A ->* X => f o inl) o ?g == idmap
H: Funext
A: Type
X: pType
?g o (fun f : pointify A ->* X => f o inl) == idmap
  {
H: Funext
A: Type
X: pType
(A -> X) -> pointify A ->* X intros f.
H: Funext
A: Type
X: pType
f: A -> X
pointify A ->* X
    snapply Build_pMap.
H: Funext
A: Type
X: pType
f: A -> X
pointify A -> X
H: Funext
A: Type
X: pType
f: A -> X
?f pt = pt
    {
H: Funext
A: Type
X: pType
f: A -> X
pointify A -> X intros [a|].
H: Funext
A: Type
X: pType
f: A -> X
a: A
X
H: Funext
A: Type
X: pType
f: A -> X
u: Unit
X
      1: exact (f a).
H: Funext
A: Type
X: pType
f: A -> X
u: Unit
X
      exact pt. }
H: Funext
A: Type
X: pType
f: A -> X
(fun X0 : pointify A =>
 match X0 with
 | inl a => (fun a0 : A => f a0) a
 | inr u => unit_name pt u
 end) pt = pt
    reflexivity. }
H: Funext
A: Type
X: pType
(fun f : pointify A ->* X => f o inl)
o (fun f : A -> X =>
   Build_pMap
     (fun X0 : pointify A =>
      match X0 with
      | inl a => (fun a0 : A => f a0) a
      | inr u => unit_name pt u
      end) 1) == idmap
H: Funext
A: Type
X: pType
(fun f : A -> X =>
 Build_pMap
   (fun X0 : pointify A =>
    match X0 with
    | inl a => (fun a0 : A => f a0) a
    | inr u => unit_name pt u
    end) 1) o (fun f : pointify A ->* X => f o inl) ==
idmap
  1: intro x; reflexivity.
H: Funext
A: Type
X: pType
(fun f : A -> X =>
 Build_pMap
   (fun X0 : pointify A =>
    match X0 with
    | inl a => (fun a0 : A => f a0) a
    | inr u => unit_name pt u
    end) 1) o (fun f : pointify A ->* X => f o inl) ==
idmap
  intros f.
H: Funext
A: Type
X: pType
f: pointify A ->* X
Build_pMap
  (fun X0 : pointify A =>
   match X0 with
   | inl a => f (inl a)
   | inr _ => pt
   end) 1 = f
  cbv.
H: Funext
A: Type
X: pType
f: pointify A ->* X
{|
  pointed_fun :=
    fun X0 : A + Unit =>
    match X0 with
    | inl a => f (inl a)
    | inr _ => ispointed_type X
    end;
  dpoint_eq := 1
|} = f
  pointed_reduce.
H: Funext
A, X: Type
f: A + Unit -> X
{|
  pointed_fun :=
    fun X0 : A + Unit =>
    match X0 with
    | inl a => f (inl a)
    | inr _ => f (inr tt)
    end;
  dpoint_eq := 1
|} = {| pointed_fun := f; dpoint_eq := 1 |}
  rapply equiv_path_pforall.
H: Funext
A, X: Type
f: A + Unit -> X
{|
  pointed_fun :=
    fun X0 : A + Unit =>
    match X0 with
    | inl a => f (inl a)
    | inr _ => f (inr tt)
    end;
  dpoint_eq := 1
|} ==* {| pointed_fun := f; dpoint_eq := 1 |}
  snapply Build_pHomotopy.
H: Funext
A, X: Type
f: A + Unit -> X
{|
  pointed_fun :=
    fun X0 : A + Unit =>
    match X0 with
    | inl a => f (inl a)
    | inr _ => f (inr tt)
    end;
  dpoint_eq := 1
|} == {| pointed_fun := f; dpoint_eq := 1 |}
H: Funext
A, X: Type
f: A + Unit -> X
?p pt =
dpoint_eq
  {|
    pointed_fun :=
      fun X0 : A + Unit =>
      match X0 with
      | inl a => f (inl a)
      | inr _ => f (inr tt)
      end;
    dpoint_eq := 1
  |} @
(dpoint_eq {| pointed_fun := f; dpoint_eq := 1 |})^
  1: by intros [a|[]].
H: Funext
A, X: Type
f: A + Unit -> X
((fun x : [A + Unit, inr tt] =>
  match
    x as s
    return
      ({|
         pointed_fun :=
           fun X0 : A + Unit =>
           match X0 with
           | inl a => f (inl a)
           | inr _ => f (inr tt)
           end;
         dpoint_eq := 1
       |} s = {| pointed_fun := f; dpoint_eq := 1 |} s)
  with
  | inl a => (fun a0 : A => 1) a
  | inr u =>
      (fun u0 : Unit =>
       match
         u0 as u1
         return
           ({|
              pointed_fun :=
                fun X0 : A + Unit =>
                match X0 with
                | inl a => f (inl a)
                | inr _ => f (inr tt)
                end;
              dpoint_eq := 1
            |} (inr u1) =
            {| pointed_fun := f; dpoint_eq := 1 |}
              (inr u1))
       with
       | tt => 1
       end) u
  end)
 :
 {|
   pointed_fun :=
     fun X0 : A + Unit =>
     match X0 with
     | inl a => f (inl a)
     | inr _ => f (inr tt)
     end;
   dpoint_eq := 1
 |} == {| pointed_fun := f; dpoint_eq := 1 |}) pt =
dpoint_eq
  {|
    pointed_fun :=
      fun X0 : A + Unit =>
      match X0 with
      | inl a => f (inl a)
      | inr _ => f (inr tt)
      end;
    dpoint_eq := 1
  |} @
(dpoint_eq {| pointed_fun := f; dpoint_eq := 1 |})^
  reflexivity.
Defined.

Lemma natequiv_pointify_r `{Funext} (A : Type)
  : NatEquiv (opyon (pointify A)) (opyon A o pointed_type).
H: Funext
A: Type
NatEquiv (opyon (pointify A)) (opyon A o pointed_type)
Proof.
H: Funext
A: Type
NatEquiv (opyon (pointify A)) (opyon A o pointed_type)
  snapply Build_NatEquiv.
H: Funext
A: Type
forall a : pType,
opyon (pointify A) a $<~>
(fun x : pType => opyon A x) a
H: Funext
A: Type
Is1Natural (opyon (pointify A))
  (fun x : pType => opyon A x) (fun a : pType => ?e a)
  1: rapply equiv_pointify_map.
H: Funext
A: Type
Is1Natural (opyon (pointify A))
  (fun x : pType => opyon A x)
  (fun a : pType => equiv_pointify_map A a)
  snapply Build_Is1Natural.
H: Funext
A: Type
forall (a a' : pType) (f : a $-> a'),
(fun a0 : pType => cate_fun (equiv_pointify_map A a0))
  a' $o fmap (opyon (pointify A)) f $==
fmap (opyon A o pointed_type) f $o
(fun a0 : pType => cate_fun (equiv_pointify_map A a0))
  a
  cbv; reflexivity.
Defined.

(** * Pointed categories give rise to pointed structures *)

(** Pointed categories have pointed hom sets *)
Definition pHom {A : Type} `{IsPointedCat A} (a1 a2 : A)
  := [Hom a1 a2, zero_morphism].

(** Pointed functors give pointed maps on morphisms *)
Definition pfmap {A B : Type} (F : A -> B)
  `{IsPointedCat A, IsPointedCat B, !HasEquivs B, !HasMorExt B}
  `{!Is0Functor F, !Is1Functor F, !IsPointedFunctor F}
  {a1 a2 : A}
  : pHom a1 a2 ->* pHom (F a1) (F a2).
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
HasMorExt0: HasMorExt B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a1, a2: A
pHom a1 a2 ->* pHom (F a1) (F a2)
Proof.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
HasMorExt0: HasMorExt B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a1, a2: A
pHom a1 a2 ->* pHom (F a1) (F a2)
  snapply Build_pMap.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
HasMorExt0: HasMorExt B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a1, a2: A
pHom a1 a2 -> pHom (F a1) (F a2)
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
HasMorExt0: HasMorExt B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a1, a2: A
?f pt = pt
  -
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
HasMorExt0: HasMorExt B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a1, a2: A
pHom a1 a2 -> pHom (F a1) (F a2) exact (fmap F).
  -
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
HasMorExt0: HasMorExt B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a1, a2: A
fmap F pt = pt apply path_hom.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
HasMorExt0: HasMorExt B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a1, a2: A
fmap F pt $== pt
    snapply fmap_zero_morphism; assumption.
Defined.