(* -*- mode: coq; mode: visual-line -*- *)
Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import PathAny.
Require Import WildCat.
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 *)
Global Instance ispointed_unit : IsPointed Unit := tt.

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

(** A sigma type of pointed components is pointed. *)
Global 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. *)
Global 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 [&] tells Coq to use the context to infer the later arguments (in this case, all of them). *)
Arguments Build_pMap & _ _ _ _.

(** Pointed maps perserve 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 A A idmap 1.

(** Composition of pointed maps *)
Definition pmap_compose {A B C : pType} (g : B ->* C) (f : A ->* B)
  : A ->* C
  := Build_pMap A C (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 presevation 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 ;
}.

(** 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.
Global Existing Instance pointed_isequiv.

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
  snrapply 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
?Goal 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
  snrapply Build_pMap.
A: Type
F: A -> pType
a: A
pproduct F -> F a
A: Type
F: A -> pType
a: A
?Goal 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 (A * B) A fst idpath.

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

Definition pprod_corec {X Y} (Z : pType) (f : Z ->* X) (g : Z ->* Y)
  : Z ->* (X * Y)
  := Build_pMap Z (X * Y) (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
  snrapply 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
  snrapply 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;
  nrapply 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'
  snrapply Build_pMap.
A, A', B, B': pType
f: A ->* A'
g: B ->* B'
[A * B, ispointed_prod] -> A' * B'
A, A', B, B': pType
f: A ->* A'
g: B ->* B'
?Goal pt = pt
  -
A, A', B, B': pType
f: A ->* A'
g: B ->* B'
[A * B, ispointed_prod] -> A' * B' 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 a Global 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 _)^.

Global 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.

Global 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)^
  nrapply whiskerL; nrapply concat_V_pp.
Defined.

Global 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)
  snrapply 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
  snrapply 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
  snrapply 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
  snrapply 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'
  snrapply 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
  snrapply 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.

Global 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 *)
Global Instance isgraph_ptype : IsGraph pType
  := Build_IsGraph pType (fun X Y => X ->* Y).

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

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

(** pForall is a 0-coherent 1-category *)
Global 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.

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

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

(** pForall is a 0-coherent 1-groupoid *)
Global 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 *)
Global Instance is1cat_ptype : Is1Cat pType.
Is1Cat pType
Proof.
Is1Cat pType
  snrapply 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 *)
Global Instance ispointedcat_ptype : IsPointedCat pType.
IsPointedCat pType
Proof.
IsPointedCat pType
  snrapply 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 *)
Global 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)
  snrapply 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 *)
Global 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.

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

Global 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; nrapply 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; nrapply 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)
    snrapply 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 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 r1 r2 s1.
A, B, C, D: pType
f: A $-> B
g: C $-> D
r1, r2: B $-> C
s1: r1 $-> r2
cat_assoc f r2 g $o
fmap (cat_precomp D f o cat_postcomp B g) s1 $==
fmap (cat_postcomp A g o cat_precomp C f) s1 $o
cat_assoc f r1 g
    srapply Build_pHomotopy.
A, B, C, D: pType
f: A $-> B
g: C $-> D
r1, r2: B $-> C
s1: r1 $-> r2
cat_assoc f r2 g $o
fmap (cat_precomp D f o cat_postcomp B g) s1 ==
fmap (cat_postcomp A g o cat_precomp C f) s1 $o
cat_assoc f r1 g
A, B, C, D: pType
f: A $-> B
g: C $-> D
r1, r2: B $-> C
s1: r1 $-> r2
?p pt =
dpoint_eq
  (cat_assoc f r2 g $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
    cat_assoc f r1 g))^
    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
  (cat_assoc f r2 g $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
    cat_assoc f r1 g))^
    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 r1 r2 s1.
A, B, C, D: pType
f: B $-> C
g: C $-> D
r1, r2: A $-> B
s1: r1 $-> r2
cat_assoc r2 f g $o fmap (cat_postcomp A (g $o f)) s1 $==
fmap (cat_postcomp A g o cat_postcomp A f) s1 $o
cat_assoc r1 f g
    srapply Build_pHomotopy.
A, B, C, D: pType
f: B $-> C
g: C $-> D
r1, r2: A $-> B
s1: r1 $-> r2
cat_assoc r2 f g $o fmap (cat_postcomp A (g $o f)) s1 ==
fmap (cat_postcomp A g o cat_postcomp A f) s1 $o
cat_assoc r1 f g
A, B, C, D: pType
f: B $-> C
g: C $-> D
r1, r2: A $-> B
s1: r1 $-> r2
?p pt =
dpoint_eq
  (cat_assoc r2 f g $o
   fmap (cat_postcomp A (g $o f)) s1) @
(dpoint_eq
   (fmap (cat_postcomp A g o cat_postcomp A f) s1 $o
    cat_assoc r1 f g))^
    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))))^)
 :
 cat_assoc r2 f g $o fmap (cat_postcomp A (g $o f)) s1 ==
 fmap (cat_postcomp A g o cat_postcomp A f) s1 $o
 cat_assoc r1 f g) pt =
dpoint_eq
  (cat_assoc r2 f g $o
   fmap (cat_postcomp A (g $o f)) s1) @
(dpoint_eq
   (fmap (cat_postcomp A g o cat_postcomp A f) s1 $o
    cat_assoc r1 f g))^
    by pelim s1 r1 r2 f g.
  -
forall a b : pType,
Is1Natural (cat_postcomp a (Id b)) idmap cat_idl intros A B 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 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 *)
Global 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 *)
Global 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 *)
Global Instance hasbinaryproducts_ptype : HasBinaryProducts pType.
HasBinaryProducts pType
Proof.
HasBinaryProducts pType
  intros X Y.
X, Y: pType
BinaryProduct X Y
  snrapply 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
    snrapply 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. *)
Global 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
  snrapply 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
    snrapply 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
    snrapply 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 nrapply 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 nrapply (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 nrapply (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. *)
Global 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
  snrapply 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 B A f^-1 ?Goal)
  1: apply moveR_equiv_V; symmetry; apply point_eq.
A, B: pType
f: A <~>* B
IsEquiv
  (Build_pMap B A 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: apply (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
  refine (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: apply (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}
  nrapply (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}}}
  nrapply 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.

Global 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 *)
Global Instance hasmorext_ptype `{Funext} : HasMorExt pType.
H: Funext
HasMorExt pType
Proof.
H: Funext
HasMorExt pType
  srapply Build_HasMorExt; 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 *)
Global Instance hasequivs_ptype : HasEquivs pType.
HasEquivs pType
Proof.
HasEquivs pType
  srapply (
    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 B A f^-1
     (moveR_equiv_V pt pt (point_eq f)^) ==*
pmap_idmap refine (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.

Global 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)
  snrapply 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 *)
Global Instance isunivalent_ptype `{Univalence} : IsUnivalent1Cat pType.
H: Univalence
IsUnivalent1Cat pType
Proof.
H: Univalence
IsUnivalent1Cat pType
  srapply Build_IsUnivalent1Cat; 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].

Global 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
?Goal 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)
  snrapply 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
    snrapply Build_pMap.
H: Funext
A: Type
X: pType
f: A -> X
pointify A -> X
H: Funext
A: Type
X: pType
f: A -> X
?Goal 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 (pointify A) X
     (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 (pointify A) X
   (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 (pointify A) X
   (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 (pointify A) X
  (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 |}
  snrapply 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)
  snrapply 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)
  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)
  snrapply 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
?Goal 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
    snrapply fmap_zero_morphism; assumption.
Defined.