Library MetaCoq.Translations.MiniHoTT

Set Warnings "-notation-overridden".

Local Set Primitive Projections.
Record sigT {A} (P : A → Type) : Type := existT
  { projT1 : A ; projT2 : P projT1 }.
Local Unset Primitive Projections.

Record unit : Type := tt { }.

Generalizable All Variables.

Definition paths : ∀ A, A → A → Type := @eq.
Definition idpath : ∀ A a, paths A a a := @eq_refl.
Definition paths_ind : ∀ A a (P : ∀ y, paths A a y → Type),
    P a (idpath A a) → ∀ y p, P y p.
  intros A a P X y p. destruct p; assumption.
Defined.
Definition paths_ind_beta : ∀ A a P u, paths _ (paths_ind A a P u a (idpath A a)) u.
  reflexivity.
Defined.

Arguments sigT {A}%type P%type.
Arguments existT {A}%type P%type _ _.
Arguments projT1 {A P} _ / .
Arguments projT2 {A P} _ / .
Notation "'exists' x .. y , p" := (sigT (fun x ⇒ .. (sigT (fun y ⇒ p)) ..))
  (at level 200, x binder, right associativity,
   format "'[' 'exists' '/ ' x .. y , '/ ' p ']'")
  : type_scope.
Notation "{ x : A & P }" := (sigT (fun x:A ⇒ P)) : type_scope.

Definition relation (A : Type) := A → A → Type.

Class Reflexive {A} (R : relation A) :=
  reflexivity : ∀ x : A, R x x.

Class Symmetric {A} (R : relation A) :=
  symmetry : ∀ x y, R x y → R y x.

Class Transitive {A} (R : relation A) :=
  transitivity : ∀ x y z, R x y → R y z → R x z.

Class PreOrder {A} (R : relation A) :=
  { PreOrder_Reflexive : Reflexive R | 2 ;
    PreOrder_Transitive : Transitive R | 2 }.

Global Existing Instance PreOrder_Reflexive.
Global Existing Instance PreOrder_Transitive.

Arguments reflexivity {A R _} / _.
Arguments symmetry {A R _} / _ _ _.
Arguments transitivity {A R _} / {_ _ _} _ _.

Ltac reflexivity :=
  Coq.Init.Ltac.reflexivity
  || (intros;
      let R := match goal with |- ?R ?x ?y ⇒ constr:(R) end in
      let pre_proof_term_head := constr:(@reflexivity _ R _) in
      let proof_term_head := (eval cbn in pre_proof_term_head) in
      apply (pre_proof_term_head : ∀ x, R x x)).

Ltac symmetry :=
  let R := match goal with |- ?R ?x ?y ⇒ constr:(R) end in
  let x := match goal with |- ?R ?x ?y ⇒ constr:(x) end in
  let y := match goal with |- ?R ?x ?y ⇒ constr:(y) end in
  let pre_proof_term_head := constr:(@symmetry _ R _) in
  let proof_term_head := (eval cbn in pre_proof_term_head) in
  refine (proof_term_head y x _); change (R y x).

Tactic Notation "etransitivity" open_constr(y) :=
  let R := match goal with |- ?R ?x ?z ⇒ constr:(R) end in
  let x := match goal with |- ?R ?x ?z ⇒ constr:(x) end in
  let z := match goal with |- ?R ?x ?z ⇒ constr:(z) end in
  let pre_proof_term_head := constr:(@transitivity _ R _) in
  let proof_term_head := (eval cbn in pre_proof_term_head) in
  refine (proof_term_head x y z _ _); [ change (R x y) | change (R y z) ].

Tactic Notation "etransitivity" := etransitivity _.

Ltac transitivity x := etransitivity x.

Notation idmap := (fun x ⇒ x).

Declare Scope equiv_scope.
Declare Scope path_scope.
Declare Scope fibration_scope.
Declare Scope trunc_scope.

Delimit Scope equiv_scope with equiv.
Delimit Scope function_scope with function.
Delimit Scope path_scope with path.
Delimit Scope fibration_scope with fibration.
Delimit Scope trunc_scope with trunc.

Open Scope trunc_scope.
Open Scope equiv_scope.
Open Scope path_scope.
Open Scope fibration_scope.
Open Scope nat_scope.
Open Scope function_scope.
Open Scope type_scope.
Open Scope core_scope.

Definition const {A B} (b : B) := fun x : A ⇒ b.

Notation "( x ; y )" := (existT _ x y) : fibration_scope.
Bind Scope fibration_scope with sigT.
Notation pr1 := projT1.
Notation pr2 := projT2.
Notation "x .1" := (pr1 x) (at level 2, left associativity, format "x .1") : fibration_scope.
Notation "x .2" := (pr2 x) (at level 2, left associativity, format "x .2") : fibration_scope.

Notation compose := (fun g f x ⇒ g (f x)).
Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.

Definition composeD {A B C} (g : ∀ b, C b) (f : A → B) := fun x : A ⇒ g (f x).
Global Arguments composeD {A B C}%type_scope (g f)%function_scope x.
#[global]
Hint Unfold composeD : core.
Notation "g 'oD' f" := (composeD g f) (at level 40, left associativity) : function_scope.

Notation "x = y :> A" := (paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.

Bind Scope path_scope with paths.
Open Scope path_scope.

Arguments paths {A} _ _.
Arguments idpath {A a} , [A] a.
Arguments paths_ind [A] a P f y p.

Global Instance reflexive_paths {A} : Reflexive (@paths A) | 0 := @idpath A.
Arguments reflexive_paths / .
Notation "1" := (idpath _) : path_scope.

Definition transport {A : Type} (P : A → Type) {x y : A} (p : x = y) (u : P x) : P y := paths_ind x (fun y _ ⇒ P y) u y p.

Arguments transport {A}%type_scope P%function_scope {x y} p%path_scope u : simpl nomatch.

Definition transport_beta {A} (P : A → Type) {x : A} (u : P x)
  : transport P 1 u = u
  := paths_ind_beta A x (fun y _ ⇒ P y) u.

Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.

Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
  := transport (fun x' ⇒ x' = x) p 1.

Global Instance symmetric_paths {A} : Symmetric (@paths A) | 0 := @inverse A.
Arguments symmetric_paths / .

Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z.
  now destruct p, q.
Defined.

Arguments concat {A x y z} p q : simpl nomatch.

Global Instance transitive_paths {A} : Transitive (@paths A) | 0 := @concat A.
Arguments transitive_paths / .

Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope.

Definition ap {A B:Type} (f:A → B) {x y:A} (p:x = y) : f x = f y
  := transport (fun y ⇒ f x = f y) p 1.

Global Arguments ap {A B}%type_scope f%function_scope {x y} p%path_scope.

Definition pointwise_paths {A} {P:A →Type} (f g:∀ x:A, P x)
  := ∀ x:A, f x = g x.

Global Arguments pointwise_paths {A}%type_scope {P} (f g)%function_scope.

#[global]
Hint Unfold pointwise_paths : typeclass_instances.

Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.

Definition apD10 {A} {B:A →Type} {f g : ∀ x, B x} (h:f =g)
  : f == g
  := fun x ⇒ transport (fun g ⇒ f x = g x) h 1.

Global Arguments apD10 {A%type_scope B} {f g}%function_scope h%path_scope _.

Definition ap10 {A B} {f g:A →B} (h:f =g) : f == g
  := apD10 h.

Global Arguments ap10 {A B}%type_scope {f g}%function_scope h%path_scope _.

Definition ap11 {A B} {f g:A →B} (h:f =g) {x y:A} (p:x =y) : f x = g y
  := ap10 h x @ ap g p.

Global Arguments ap11 {A B}%type_scope {f g}%function_scope h%path_scope {x y} p%path_scope.

Arguments ap {A B} f {x y} p : simpl nomatch.

Definition apD {A:Type} {B:A →Type} (f:∀ a:A, B a) {x y:A} (p:x =y):
  p # (f x ) = f y
  := paths_ind x (fun y p ⇒ p # (f x ) = f y) (transport_beta _ _) y p.

Arguments apD {A%type_scope B} f%function_scope {x y} p%path_scope : simpl nomatch.

Definition Sect {A B : Type} (s : A → B) (r : B → A) :=
  ∀ x : A, r (s x) = x.

Global Arguments Sect {A B}%type_scope (s r)%function_scope.

Class IsEquiv {A B : Type} (f : A → B) := BuildIsEquiv {
                                               equiv_inv : B → A ;
                                               eisretr : Sect equiv_inv f;
                                               eissect : Sect f equiv_inv;
                                               eisadj : ∀ x : A, eisretr (f x) = ap f (eissect x)
                                             }.

Arguments eisretr {A B}%type_scope f%function_scope {_} _.
Arguments eissect {A B}%type_scope f%function_scope {_} _.
Arguments eisadj {A B}%type_scope f%function_scope {_} _.
Arguments IsEquiv {A B}%type_scope f%function_scope.

Record Equiv A B := BuildEquiv {
                        equiv_fun : A → B ;
                        equiv_isequiv : IsEquiv equiv_fun
                      }.

Coercion equiv_fun : Equiv >-> Funclass.

Global Existing Instance equiv_isequiv.

Arguments equiv_fun {A B} _ _.
Arguments equiv_isequiv {A B} _.

Bind Scope equiv_scope with Equiv.

Notation "A <~> B" := (Equiv A B) (at level 90) : type_scope.

Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.

Definition ap10_equiv {A B : Type} {f g : A <~> B} (h : f = g) : f == g
  := ap10 (ap equiv_fun h).

Class Contr (A : Type) :=
  BuildContr { center : A ;
               contr : (∀ y : A, center = y) }.

Arguments center A {_}.

Class Funext := { isequiv_apD10 : ∀ (A : Type) (P : A → Type) f g, IsEquiv (@apD10 A P f g) }.

Global Existing Instance isequiv_apD10.

Definition path_forall `{Funext} {A : Type} {P : A → Type} (f g : ∀ x : A, P x) : f == g → f = g
  := (@apD10 A P f g )^-1.

Global Arguments path_forall {_ A%type_scope P} (f g)%function_scope _.

Definition path_forall2 `{Funext} {A B : Type} {P : A → B → Type} (f g : ∀ x y, P x y) :
  (∀ x y, f x y = g x y ) → f = g
  :=
    (fun E ⇒ path_forall f g (fun x ⇒ path_forall (f x) (g x) (E x))).

Global Arguments path_forall2 {_} {A B}%type_scope {P} (f g)%function_scope _.

Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
  p @ 1 = p.
  now destruct p.
Defined.

Definition concat_1p {A : Type} {x y : A} (p : x = y) :
  1 @ p = p.
  now destruct p.
Defined.

Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
  p @ (q @ r ) = (p @ q ) @ r.
  now destruct p, q, r.
Defined.

Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
  (p @ q ) @ r = p @ (q @ r ).
  now destruct p, q, r.
Defined.

Definition concat_pV {A : Type} {x y : A} (p : x = y) :
  p @ p ^ = 1.
  now destruct p.
Defined.

Definition concat_Vp {A : Type} {x y : A} (p : x = y) :
  p ^ @ p = 1.
  now destruct p.
Defined.

Definition concat_V_pp {A : Type} {x y z : A} (p : x = y) (q : y = z) :
  p ^ @ (p @ q ) = q.
  now destruct p, q.
Defined.

Definition concat_p_Vp {A : Type} {x y z : A} (p : x = y) (q : x = z) :
  p @ (p ^ @ q ) = q.
  now destruct p, q.
Defined.

Definition concat_pp_V {A : Type} {x y z : A} (p : x = y) (q : y = z) :
  (p @ q ) @ q ^ = p.
  now destruct p, q.
Defined.

Definition concat_pV_p {A : Type} {x y z : A} (p : x = z) (q : y = z) :
  (p @ q ^) @ q = p.
  now destruct p, q.
Defined.

Definition inv_pp {A : Type} {x y z : A} (p : x = y) (q : y = z) :
  (p @ q )^ = q ^ @ p ^.
  now destruct p, q.
Defined.

Definition inv_Vp {A : Type} {x y z : A} (p : y = x) (q : y = z) :
  (p ^ @ q )^ = q ^ @ p.
  now destruct p, q.
Defined.

Definition inv_pV {A : Type} {x y z : A} (p : x = y) (q : z = y) :
  (p @ q ^)^ = q @ p ^.
  now destruct p, q.
Defined.

Definition inv_VV {A : Type} {x y z : A} (p : y = x) (q : z = y) :
  (p ^ @ q ^)^ = q @ p.
  now destruct p, q.
Defined.

Definition inv_V {A : Type} {x y : A} (p : x = y) :
  p ^^ = p.
  now destruct p.
Defined.

Definition moveR_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  p = r ^ @ q → r @ p = q.
Proof.
  destruct r.
  intro h. exact (concat_1p _ @ h @ concat_1p _).
Defined.

Definition moveR_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  r = q @ p ^ → r @ p = q.
Proof.
  destruct p.
  intro h. exact (concat_p1 _ @ h @ concat_p1 _).
Defined.

Definition moveR_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
  p = r @ q → r ^ @ p = q.
Proof.
  destruct r.
  intro h. exact (concat_1p _ @ h @ concat_1p _).
Defined.

Definition moveR_pV {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) :
  r = q @ p → r @ p ^ = q.
Proof.
  destruct p.
  intro h. exact (concat_p1 _ @ h @ concat_p1 _).
Defined.

Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  r ^ @ q = p → q = r @ p.
Proof.
  destruct r.
  intro h. exact ((concat_1p _)^ @ h @ (concat_1p _)^).
Defined.

Definition moveL_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  q @ p ^ = r → q = r @ p.
Proof.
  destruct p.
  intro h. exact ((concat_p1 _)^ @ h @ (concat_p1 _)^).
Defined.

Definition moveL_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
  r @ q = p → q = r ^ @ p.
Proof.
  destruct r.
  intro h. exact ((concat_1p _)^ @ h @ (concat_1p _)^).
Defined.

Definition moveL_pV {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) :
  q @ p = r → q = r @ p ^.
Proof.
  destruct p.
  intro h. exact ((concat_p1 _)^ @ h @ (concat_p1 _)^).
Defined.

Definition moveL_1M {A : Type} {x y : A} (p q : x = y) :
  p @ q ^ = 1 → p = q.
Proof.
  destruct q.
  intro h. exact ((concat_p1 _)^ @ h).
Defined.

Definition moveL_M1 {A : Type} {x y : A} (p q : x = y) :
  q ^ @ p = 1 → p = q.
Proof.
  destruct q.
  intro h. exact ((concat_1p _)^ @ h).
Defined.

Definition moveL_1V {A : Type} {x y : A} (p : x = y) (q : y = x) :
  p @ q = 1 → p = q ^.
Proof.
  destruct q.
  intro h. exact ((concat_p1 _)^ @ h).
Defined.

Definition moveL_V1 {A : Type} {x y : A} (p : x = y) (q : y = x) :
  q @ p = 1 → p = q ^.
Proof.
  destruct q.
  intro h. exact ((concat_1p _)^ @ h).
Defined.

Definition moveR_M1 {A : Type} {x y : A} (p q : x = y) :
  1 = p ^ @ q → p = q.
Proof.
  destruct p.
  intro h. exact (h @ (concat_1p _)).
Defined.

Definition moveR_1M {A : Type} {x y : A} (p q : x = y) :
  1 = q @ p ^ → p = q.
Proof.
  destruct p.
  intro h. exact (h @ (concat_p1 _)).
Defined.

Definition moveR_1V {A : Type} {x y : A} (p : x = y) (q : y = x) :
  1 = q @ p → p ^ = q.
Proof.
  destruct p.
  intro h. exact (h @ (concat_p1 _)).
Defined.

Definition moveR_V1 {A : Type} {x y : A} (p : x = y) (q : y = x) :
  1 = p @ q → p ^ = q.
Proof.
  destruct p.
  intro h. exact (h @ (concat_1p _)).
Defined.

Definition moveR_transport_p {A : Type} (P : A → Type) {x y : A}
  (p : x = y) (u : P x) (v : P y)
  : u = p ^ # v → p # u = v.
Proof.
  destruct p.
  exact idmap.
Defined.

Definition moveR_transport_V {A : Type} (P : A → Type) {x y : A}
  (p : y = x) (u : P x) (v : P y)
  : u = p # v → p ^ # u = v.
Proof.
  destruct p.
  exact idmap.
Defined.

Definition moveL_transport_V {A : Type} (P : A → Type) {x y : A}
  (p : x = y) (u : P x) (v : P y)
  : p # u = v → u = p ^ # v.
Proof.
  destruct p.
  exact idmap.
Defined.

Definition moveL_transport_p {A : Type} (P : A → Type) {x y : A}
  (p : y = x) (u : P x) (v : P y)
  : p ^ # u = v → u = p # v.
Proof.
  destruct p.
  exact idmap.
Defined.

Definition moveR_transport_p_V {A : Type} (P : A → Type) {x y : A}
           (p : x = y) (u : P x) (v : P y) (q : u = p ^ # v)
  : (moveR_transport_p P p u v q )^ = moveL_transport_p P p v u q ^.
Proof.
  destruct p; reflexivity.
Defined.

Definition moveR_transport_V_V {A : Type} (P : A → Type) {x y : A}
           (p : y = x) (u : P x) (v : P y) (q : u = p # v)
  : (moveR_transport_V P p u v q )^ = moveL_transport_V P p v u q ^.
Proof.
  destruct p; reflexivity.
Defined.

Definition moveL_transport_V_V {A : Type} (P : A → Type) {x y : A}
           (p : x = y) (u : P x) (v : P y) (q : p # u = v)
  : (moveL_transport_V P p u v q )^ = moveR_transport_V P p v u q ^.
Proof.
  destruct p; reflexivity.
Defined.

Definition moveL_transport_p_V {A : Type} (P : A → Type) {x y : A}
           (p : y = x) (u : P x) (v : P y) (q : p ^ # u = v)
  : (moveL_transport_p P p u v q )^ = moveR_transport_p P p v u q ^.
Proof.
  destruct p; reflexivity.
Defined.

Definition ap_1 {A B : Type} (x : A) (f : A → B) :
  ap f 1 = 1 :> (f x = f x )
  := 1.

Definition apD_1 {A B} (x : A) (f : ∀ x : A, B x) :
  apD f 1 = 1 :> (f x = f x )
  := 1.

Definition ap_pp {A B : Type} (f : A → B) {x y z : A} (p : x = y) (q : y = z) :
  ap f (p @ q) = (ap f p ) @ (ap f q ).
  now destruct p, q.
Defined.

Definition ap_p_pp {A B : Type} (f : A → B) {w : B} {x y z : A}
  (r : w = f x) (p : x = y) (q : y = z) :
  r @ (ap f (p @ q)) = (r @ ap f p ) @ (ap f q ).
Proof.
  destruct p, q. simpl. exact (concat_p_pp r 1 1).
Defined.

Definition ap_pp_p {A B : Type} (f : A → B) {x y z : A} {w : B}
  (p : x = y) (q : y = z) (r : f z = w) :
  (ap f (p @ q)) @ r = (ap f p ) @ (ap f q @ r ).
Proof.
  destruct p, q. simpl. exact (concat_pp_p 1 1 r).
Defined.

Definition inverse_ap {A B : Type} (f : A → B) {x y : A} (p : x = y) :
  (ap f p )^ = ap f (p ^).
  now destruct p.
Defined.

Definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x = y) :
  ap f (p ^) = (ap f p )^.
  now destruct p.
Defined.

Definition ap_idmap {A : Type} {x y : A} (p : x = y) :
  ap idmap p = p.
  now destruct p.
Defined.

Definition ap_compose {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x = y) :
  ap (g o f) p = ap g (ap f p).
  now destruct p.
Defined.

Definition ap_compose' {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x = y) :
  ap (fun a ⇒ g (f a)) p = ap g (ap f p).
  now destruct p.
Defined.

Definition ap_const {A B : Type} {x y : A} (p : x = y) (z : B) :
  ap (fun _ ⇒ z) p = 1.
  now destruct p.
Defined.

Definition concat_Ap {A B : Type} {f g : A → B} (p : ∀ x, f x = g x) {x y : A} (q : x = y) :
  (ap f q ) @ (p y ) = (p x ) @ (ap g q ).
  destruct q. cbn. now rewrite concat_p1, concat_1p.
Defined.

Definition concat_A1p {A : Type} {f : A → A} (p : ∀ x, f x = x) {x y : A} (q : x = y) :
  (ap f q ) @ (p y ) = (p x ) @ q.
  destruct q. cbn. now rewrite concat_p1, concat_1p.
Defined.

Definition concat_pA1 {A : Type} {f : A → A} (p : ∀ x, x = f x) {x y : A} (q : x = y) :
  (p x ) @ (ap f q ) = q @ (p y ).
  destruct q. cbn. now rewrite concat_p1, concat_1p.
Defined.

Definition concat_pA_pp {A B : Type} {f g : A → B} (p : ∀ x, f x = g x)
  {x y : A} (q : x = y)
  {w z : B} (r : w = f x) (s : g y = z)
  :
  (r @ ap f q ) @ (p y @ s ) = (r @ p x ) @ (ap g q @ s ).
Proof.
  destruct q, s; simpl.
  repeat rewrite concat_p1.
  reflexivity.
Defined.

Definition concat_pA_p {A B : Type} {f g : A → B} (p : ∀ x, f x = g x)
  {x y : A} (q : x = y)
  {w : B} (r : w = f x)
  :
  (r @ ap f q ) @ p y = (r @ p x ) @ ap g q.
Proof.
  destruct q; simpl.
  repeat rewrite concat_p1.
  reflexivity.
Defined.

Definition concat_A_pp {A B : Type} {f g : A → B} (p : ∀ x, f x = g x)
  {x y : A} (q : x = y)
  {z : B} (s : g y = z)
  :
  (ap f q ) @ (p y @ s ) = (p x ) @ (ap g q @ s ).
Proof.
  destruct q, s; cbn.
  repeat rewrite concat_p1, concat_1p.
  reflexivity.
Defined.

Definition concat_pA1_pp {A : Type} {f : A → A} (p : ∀ x, f x = x)
  {x y : A} (q : x = y)
  {w z : A} (r : w = f x) (s : y = z)
  :
  (r @ ap f q ) @ (p y @ s ) = (r @ p x ) @ (q @ s ).
Proof.
  destruct q, s; simpl.
  repeat rewrite concat_p1.
  reflexivity.
Defined.

Definition concat_pp_A1p {A : Type} {g : A → A} (p : ∀ x, x = g x)
  {x y : A} (q : x = y)
  {w z : A} (r : w = x) (s : g y = z)
  :
  (r @ p x ) @ (ap g q @ s ) = (r @ q ) @ (p y @ s ).
Proof.
  destruct q, s; simpl.
  repeat rewrite concat_p1.
  reflexivity.
Defined.

Definition concat_pA1_p {A : Type} {f : A → A} (p : ∀ x, f x = x)
  {x y : A} (q : x = y)
  {w : A} (r : w = f x)
  :
  (r @ ap f q ) @ p y = (r @ p x ) @ q.
Proof.
  destruct q; simpl.
  repeat rewrite concat_p1.
  reflexivity.
Defined.

Definition concat_A1_pp {A : Type} {f : A → A} (p : ∀ x, f x = x)
  {x y : A} (q : x = y)
  {z : A} (s : y = z)
  :
  (ap f q ) @ (p y @ s ) = (p x ) @ (q @ s ).
Proof.
  destruct q, s; cbn.
  repeat rewrite concat_p1, concat_1p.
  reflexivity.
Defined.

Definition concat_pp_A1 {A : Type} {g : A → A} (p : ∀ x, x = g x)
  {x y : A} (q : x = y)
  {w : A} (r : w = x)
  :
  (r @ p x ) @ ap g q = (r @ q ) @ p y.
Proof.
  destruct q; simpl.
  repeat rewrite concat_p1.
  reflexivity.
Defined.

Definition concat_p_A1p {A : Type} {g : A → A} (p : ∀ x, x = g x)
  {x y : A} (q : x = y)
  {z : A} (s : g y = z)
  :
  p x @ (ap g q @ s ) = q @ (p y @ s ).
Proof.
  destruct q, s; simpl.
  repeat rewrite concat_p1, concat_1p.
  reflexivity.
Defined.

Lemma concat_1p_1 {A} {x : A} (p : x = x) (q : p = 1)
: concat_1p p @ q = ap (fun p' ⇒ 1 @ p') q.
Proof.
  rewrite <- (inv_V q).
  set (r := q^). clearbody r; clear q; destruct r.
  reflexivity.
Defined.

Lemma concat_p1_1 {A} {x : A} (p : x = x) (q : p = 1)
: concat_p1 p @ q = ap (fun p' ⇒ p' @ 1) q.
Proof.
  rewrite <- (inv_V q).
  set (r := q^). clearbody r; clear q; destruct r.
  reflexivity.
Defined.

Definition apD10_1 {A} {B:A →Type} (f : ∀ x, B x) (x:A)
  : apD10 (idpath f) x = 1
:= 1.

Definition apD10_pp {A} {B:A →Type} {f f' f'' : ∀ x, B x}
  (h:f =f') (h':f'=f'') (x:A)
: apD10 (h @ h') x = apD10 h x @ apD10 h' x.
Proof.
  case h, h'; reflexivity.
Defined.

Definition apD10_V {A} {B:A →Type} {f g : ∀ x, B x} (h:f =g) (x:A)
  : apD10 (h ^) x = (apD10 h x )^.
  now destruct h.
Defined.

Definition ap10_1 {A B} {f:A →B} (x:A) : ap10 (idpath f) x = 1
  := 1.

Definition ap10_pp {A B} {f f' f'':A →B} (h:f =f') (h':f'=f'') (x:A)
  : ap10 (h @ h') x = ap10 h x @ ap10 h' x
:= apD10_pp h h' x.

Definition ap10_V {A B} {f g : A →B} (h : f = g) (x:A)
  : ap10 (h ^) x = (ap10 h x )^
:= apD10_V h x.

Definition apD10_ap_precompose {A B C} (f : A → B) {g g' : ∀ x:B, C x} (p : g = g') a
: apD10 (ap (fun h : ∀ x:B, C x ⇒ h oD f) p) a = apD10 p (f a).
Proof.
  destruct p; reflexivity.
Defined.

Definition ap10_ap_precompose {A B C} (f : A → B) {g g' : B → C} (p : g = g') a
: ap10 (ap (fun h : B → C ⇒ h o f) p) a = ap10 p (f a)
  := apD10_ap_precompose f p a.

Definition apD10_ap_postcompose {A B C} (f : ∀ x, B x → C) {g g' : ∀ x:A, B x} (p : g = g') a
: apD10 (ap (fun h : ∀ x:A, B x ⇒ fun x ⇒ f x (h x)) p) a = ap (f a) (apD10 p a).
Proof.
  destruct p; reflexivity.
Defined.

Definition ap10_ap_postcompose {A B C} (f : B → C) {g g' : A → B} (p : g = g') a
: ap10 (ap (fun h : A → B ⇒ f o h) p) a = ap f (ap10 p a)
:= apD10_ap_postcompose (fun a ⇒ f) p a.

Definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x)
  : 1 # u = u
:= 1.

Definition transport_pp {A : Type} (P : A → Type) {x y z : A} (p : x = y) (q : y = z) (u : P x) :
  p @ q # u = q # p # u.
  now destruct p, q.
Defined.

Definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x = y) (z : P y)
  : p # p ^ # z = z
  := (transport_pp P p ^ p z )^
  @ ap (fun r ⇒ transport P r z) (concat_Vp p).

Definition transport_Vp {A : Type} (P : A → Type) {x y : A} (p : x = y) (z : P x)
  : p ^ # p # z = z
  := (transport_pp P p p ^ z )^
  @ ap (fun r ⇒ transport P r z) (concat_pV p).

Definition transport_p_pp {A : Type} (P : A → Type)
  {x y z w : A} (p : x = y) (q : y = z) (r : z = w)
  (u : P x)
  : ap (fun e ⇒ e # u) (concat_p_pp p q r)
    @ (transport_pp P (p@q) r u ) @ ap (transport P r) (transport_pp P p q u)
  = (transport_pp P p (q@r) u ) @ (transport_pp P q r (p #u))
  :> ((p @ (q @ r )) # u = r # q # p # u ) .
Proof.
  destruct p, q, r. simpl. exact 1.
Defined.

Definition transport_pVp {A} (P : A → Type) {x y:A} (p:x =y) (z:P x)
  : transport_pV P p (transport P p z)
  = ap (transport P p) (transport_Vp P p z).
Proof.
  destruct p; reflexivity.
Defined.

Definition transport_VpV {A} (P : A → Type) {x y : A} (p : x = y) (z : P y)
  : transport_Vp P p (transport P p ^ z)
    = ap (transport P p ^) (transport_pV P p z).
Proof.
  destruct p; reflexivity.
Defined.

Definition ap_transport_transport_pV {A} (P : A → Type) {x y : A}
           (p : x = y) (u : P x) (v : P y) (e : transport P p u = v)
  : ap (transport P p) (moveL_transport_V P p u v e)
       @ transport_pV P p v = e.
Proof.
    now destruct e, p.
Defined.

Definition moveL_transport_V_1 {A} (P : A → Type) {x y : A}
           (p : x = y) (u : P x)
  : moveL_transport_V P p u (p # u) 1 = (transport_Vp P p u )^.
Proof.
  destruct p; reflexivity.
Defined.

Definition ap11_is_ap10_ap01 {A B} {f g:A →B} (h:f =g) {x y:A} (p:x =y)
: ap11 h p = ap10 h x @ ap g p.
  now destruct h, p.
Defined.

Definition transportD {A : Type} (B : A → Type) (C : ∀ a:A, B a → Type)
  {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1 y)
  : C x2 (p # y).
  now destruct p.
Defined.

Definition transportD2 {A : Type} (B C : A → Type) (D : ∀ a:A, B a → C a → Type)
  {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z)
  : D x2 (p # y) (p # z).
  now destruct p.
Defined.

Definition ap011 {A B C} (f : A → B → C) {x x' y y'} (p : x = x') (q : y = y')
: f x y = f x' y'
:= ap11 (ap f p) q.

Definition ap011D {A B C} (f : ∀ (a:A), B a → C)
           {x x'} (p : x = x') {y y'} (q : p # y = y')
: f x y = f x' y'.
Proof.
  destruct p, q; reflexivity.
Defined.

Definition ap01D1 {A B C} (f : ∀ (a:A), B a → C a)
           {x x'} (p : x = x') {y y'} (q : p # y = y')
: transport C p (f x y) = f x' y'.
Proof.
  destruct p, q; reflexivity.
Defined.

Definition apD011 {A B C} (f : ∀ (a:A) (b:B a), C a b)
           {x x'} (p : x = x') {y y'} (q : p # y = y')
: transport (C x') q (transportD B C p y (f x y)) = f x' y'.
Proof.
  destruct p, q; reflexivity.
Defined.

Definition transport2 {A : Type} (P : A → Type) {x y : A} {p q : x = y}
  (r : p = q) (z : P x)
  : p # z = q # z
  := ap (fun p' ⇒ p' # z) r.

Definition transport2_is_ap10 {A : Type} (Q : A → Type) {x y : A} {p q : x = y}
  (r : p = q) (z : Q x)
  : transport2 Q r z = ap10 (ap (transport Q) r) z.
  now destruct r.
Defined.

Definition transport2_p2p {A : Type} (P : A → Type) {x y : A} {p1 p2 p3 : x = y}
  (r1 : p1 = p2) (r2 : p2 = p3) (z : P x)
  : transport2 P (r1 @ r2) z = transport2 P r1 z @ transport2 P r2 z.
Proof.
  destruct r1, r2; reflexivity.
Defined.

Definition transport2_V {A : Type} (Q : A → Type) {x y : A} {p q : x = y}
  (r : p = q) (z : Q x)
  : transport2 Q (r ^) z = (transport2 Q r z )^.
  now destruct r.
Defined.

Definition concat_AT {A : Type} (P : A → Type) {x y : A} {p q : x = y}
  {z w : P x} (r : p = q) (s : z = w)
  : ap (transport P p) s @ transport2 P r w
    = transport2 P r z @ ap (transport P q) s.
  now destruct r, s.
Defined.

Lemma ap_transport {A} {P Q : A → Type} {x y : A} (p : x = y) (f : ∀ x, P x → Q x) (z : P x) :
  f y (p # z) = (p # (f x z )).
  now destruct p.
Defined.

Lemma ap_transportD {A : Type}
      (B : A → Type) (C1 C2 : ∀ a : A, B a → Type)
      (f : ∀ a b, C1 a b → C2 a b)
      {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C1 x1 y)
: f x2 (p # y) (transportD B C1 p y z)
  = transportD B C2 p y (f x1 y z).
Proof.
  now destruct p.
Defined.

Lemma ap_transportD2 {A : Type}
      (B C : A → Type) (D1 D2 : ∀ a, B a → C a → Type)
      (f : ∀ a b c, D1 a b c → D2 a b c)
      {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D1 x1 y z)
: f x2 (p # y) (p # z) (transportD2 B C D1 p y z w)
  = transportD2 B C D2 p y z (f x1 y z w).
Proof.
  now destruct p.
Defined.

Lemma ap_transport_pV {X} (Y : X → Type) {x1 x2 : X} (p : x1 = x2)
      {y1 y2 : Y x2} (q : y1 = y2)
: ap (transport Y p) (ap (transport Y p ^) q) =
  transport_pV Y p y1 @ q @ (transport_pV Y p y2 )^.
Proof.
  destruct p, q; reflexivity.
Defined.

Definition transport_pV_ap {X} (P : X → Type) (f : ∀ x, P x)
      {x1 x2 : X} (p : x1 = x2)
: ap (transport P p) (apD f p ^) @ apD f p = transport_pV P p (f x2).
Proof.
  destruct p; reflexivity.
Defined.

Definition apD_pp {A} {P : A → Type} (f : ∀ x, P x)
           {x y z : A} (p : x = y) (q : y = z)
  : apD f (p @ q)
    = transport_pp P p q (f x) @ ap (transport P q) (apD f p) @ apD f q.
Proof.
  destruct p, q; reflexivity.
Defined.

Definition apD_V {A} {P : A → Type} (f : ∀ x, P x)
           {x y : A} (p : x = y)
  : apD f p ^ = moveR_transport_V _ _ _ _ (apD f p )^.
Proof.
  destruct p; reflexivity.
Defined.
Definition transport_const {A B : Type} {x1 x2 : A} (p : x1 = x2) (y : B)
  : transport (fun x ⇒ B) p y = y.
Proof.
  destruct p. exact 1.
Defined.

Definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 = x2}
  (r : p = q) (y : B)
  : transport_const p y = transport2 (fun _ ⇒ B) r y @ transport_const q y.
  destruct r. symmetry; apply concat_1p.
Defined.

Lemma transport_compose {A B} {x y : A} (P : B → Type) (f : A → B)
  (p : x = y) (z : P (f x))
  : transport (fun x ⇒ P (f x)) p z = transport P (ap f p) z.
Proof.
  destruct p; reflexivity.
Defined.

Lemma transportD_compose {A A'} B {x x' : A} (C : ∀ x : A', B x → Type) (f : A → A')
      (p : x = x') y (z : C (f x) y)
: transportD (B o f) (C oD f) p y z
  = transport (C (f x')) (transport_compose B f p y )^ (transportD B C (ap f p) y z).
Proof.
  destruct p; reflexivity.
Defined.

Lemma transport_apD_transportD {A} B (f : ∀ x : A, B x) (C : ∀ x, B x → Type)
      {x1 x2 : A} (p : x1 = x2) (z : C x1 (f x1))
: apD f p # transportD B C p _ z
  = transport (fun x ⇒ C x (f x)) p z.
Proof.
  destruct p; reflexivity.
Defined.

Lemma transport_precompose {A B C} (f : A → B) (g g' : B → C) (p : g = g')
: transport (fun h : B → C ⇒ g o f = h o f) p 1 =
  ap (fun h ⇒ h o f) p.
Proof.
  destruct p; reflexivity.
Defined.

Definition transport_idmap_ap A (P : A → Type) x y (p : x = y) (u : P x)
: transport P p u = transport idmap (ap P p) u.
  now destruct p.
Defined.

Sometimes, it's useful to have the goal be in terms of ap, so we can use lemmas about ap. However, we can't just rewrite !transport_idmap_ap, as that's likely to loop. So, instead, we provide a tactic transport_to_ap, that replaces all transport P p u with transport idmap (ap P p) u for non-idmap P.

Ltac transport_to_ap :=
  repeat match goal with
           | [ |- context[transport ?P ?p ?u] ]
             ⇒ match P with
                  | idmap ⇒ fail 1
                  | _ ⇒ idtac
                end;
               progress rewrite (transport_idmap_ap _ P _ _ p u)
         end.

Definition transport_transport {A B} (C : A → B → Type)
           {x1 x2 : A} (p : x1 = x2) {y1 y2 : B} (q : y1 = y2)
           (c : C x1 y1)
: transport (C x2) q (transport (fun x ⇒ C x y1) p c)
  = transport (fun x ⇒ C x y2) p (transport (C x1) q c).
Proof.
  destruct p, q; reflexivity.
Defined.

Lemma apD_const {A B} {x y : A} (f : A → B) (p: x = y) :
  apD f p = transport_const p (f x) @ ap f p.
Proof.
  destruct p; reflexivity.
Defined.

Definition concat2 {A} {x y z : A} {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
  : p @ q = p' @ q'.
  now destruct h, h'.
Defined.

Notation "p @@ q" := (concat2 p q)%path (at level 20) : path_scope.

Arguments concat2 : simpl nomatch.

Lemma concat2_ap_ap {A B : Type} {x' y' z' : B}
           (f : A → (x' = y')) (g : A → (y' = z'))
           {x y : A} (p : x = y)
: (ap f p ) @@ (ap g p ) = ap (fun u ⇒ f u @ g u) p.
Proof.
    now destruct p.
Defined.

Definition inverse2 {A : Type} {x y : A} {p q : x = y} (h : p = q)
  : p ^ = q ^
:= ap inverse h.

Lemma ap_pp_concat_pV {A B} (f : A → B) {x y : A} (p : x = y)
: ap_pp f p p ^ @ ((1 @@ ap_V f p ) @ concat_pV (ap f p))
  = ap (ap f) (concat_pV p).
Proof.
  destruct p; reflexivity.
Defined.

Lemma ap_pp_concat_Vp {A B} (f : A → B) {x y : A} (p : x = y)
: ap_pp f p ^ p @ ((ap_V f p @@ 1) @ concat_Vp (ap f p))
  = ap (ap f) (concat_Vp p).
Proof.
  destruct p; reflexivity.
Defined.

Lemma concat_pV_inverse2 {A} {x y : A} (p q : x = y) (r : p = q)
: (r @@ inverse2 r ) @ concat_pV q = concat_pV p.
Proof.
  destruct r, p; reflexivity.
Defined.

Lemma concat_Vp_inverse2 {A} {x y : A} (p q : x = y) (r : p = q)
: (inverse2 r @@ r ) @ concat_Vp q = concat_Vp p.
Proof.
  destruct r, p; reflexivity.
Defined.

Definition whiskerL {A : Type} {x y z : A} (p : x = y)
  {q r : y = z} (h : q = r) : p @ q = p @ r
:= 1 @@ h.

Definition whiskerR {A : Type} {x y z : A} {p q : x = y}
  (h : p = q) (r : y = z) : p @ r = q @ r
:= h @@ 1.

Definition cancelL {A} {x y z : A} (p : x = y) (q r : y = z)
: (p @ q = p @ r ) → (q = r )
:= fun h ⇒ (concat_V_pp p q )^ @ whiskerL p ^ h @ (concat_V_pp p r ).

Definition cancelR {A} {x y z : A} (p q : x = y) (r : y = z)
: (p @ r = q @ r ) → (p = q )
:= fun h ⇒ (concat_pp_V p r )^ @ whiskerR h r ^ @ (concat_pp_V q r ).

Definition whiskerR_p1 {A : Type} {x y : A} {p q : x = y} (h : p = q) :
  (concat_p1 p ) ^ @ whiskerR h 1 @ concat_p1 q = h.
  now destruct h, p.
Defined.

Definition whiskerR_1p {A : Type} {x y z : A} (p : x = y) (q : y = z) :
  whiskerR 1 q = 1 :> (p @ q = p @ q ).
  reflexivity.
Defined.

Definition whiskerL_p1 {A : Type} {x y z : A} (p : x = y) (q : y = z) :
  whiskerL p 1 = 1 :> (p @ q = p @ q ).
  reflexivity.
Defined.

Definition whiskerL_1p {A : Type} {x y : A} {p q : x = y} (h : p = q) :
  (concat_1p p ) ^ @ whiskerL 1 h @ concat_1p q = h.
  now destruct h, p.
Defined.

Definition whiskerR_p1_1 {A} {x : A} (h : idpath x = idpath x)
: whiskerR h 1 = h.
Proof.
  refine (_ @ whiskerR_p1 h); simpl.
  symmetry; refine (concat_p1 _ @ concat_1p _).
Defined.

Definition whiskerL_1p_1 {A} {x : A} (h : idpath x = idpath x)
: whiskerL 1 h = h.
Proof.
  refine (_ @ whiskerL_1p h); simpl.
  symmetry; refine (concat_p1 _ @ concat_1p _).
Defined.

Definition concat2_p1 {A : Type} {x y : A} {p q : x = y} (h : p = q) :
  h @@ 1 = whiskerR h 1 :> (p @ 1 = q @ 1).
  now destruct h.
Defined.

Definition concat2_1p {A : Type} {x y : A} {p q : x = y} (h : p = q) :
  1 @@ h = whiskerL 1 h :> (1 @ p = 1 @ q ).
  now destruct h.
Defined.

Definition cancel2L {A : Type} {x y z : A} {p p' : x = y} {q q' : y = z}
           (g : p = p') (h k : q = q')
: (g @@ h = g @@ k ) → (h = k ).
Proof.
  intro r. destruct g, p, q.
  refine ((whiskerL_1p h)^ @ _). refine (_ @ (whiskerL_1p k)).
  refine (whiskerR _ _). refine (whiskerL _ _).
  apply r.
Defined.

Definition cancel2R {A : Type} {x y z : A} {p p' : x = y} {q q' : y = z}
           (g h : p = p') (k : q = q')
: (g @@ k = h @@ k ) → (g = h ).
Proof.
  intro r. destruct k, p, q.
  refine ((whiskerR_p1 g)^ @ _). refine (_ @ (whiskerR_p1 h)).
  refine (whiskerR _ _). refine (whiskerL _ _).
  apply r.
Defined.

Definition whiskerL_pp {A} {x y z : A} (p : x = y) {q q' q'' : y = z}
           (r : q = q') (s : q' = q'')
: whiskerL p (r @ s) = whiskerL p r @ whiskerL p s.
Proof.
  destruct p, r, s; reflexivity.
Defined.

Definition whiskerR_pp {A} {x y z : A} {p p' p'' : x = y} (q : y = z)
           (r : p = p') (s : p' = p'')
: whiskerR (r @ s) q = whiskerR r q @ whiskerR s q.
Proof.
  destruct q, r, s; reflexivity.
Defined.

Definition whiskerL_VpL {A} {x y z : A} (p : x = y)
           {q q' : y = z} (r : q = q')
: (concat_V_pp p q )^ @ whiskerL p ^ (whiskerL p r) @ concat_V_pp p q'
  = r.
Proof.
  destruct p, r, q. reflexivity.
Defined.

Definition whiskerL_pVL {A} {x y z : A} (p : y = x)
           {q q' : y = z} (r : q = q')
: (concat_p_Vp p q )^ @ whiskerL p (whiskerL p ^ r) @ concat_p_Vp p q'
  = r.
Proof.
  destruct p, r, q. reflexivity.
Defined.

Definition whiskerR_pVR {A} {x y z : A} {p p' : x = y}
           (r : p = p') (q : y = z)
: (concat_pp_V p q )^ @ whiskerR (whiskerR r q) q ^ @ concat_pp_V p' q
  = r.
Proof.
  destruct p, r, q. reflexivity.
Defined.

Definition whiskerR_VpR {A} {x y z : A} {p p' : x = y}
           (r : p = p') (q : z = y)
: (concat_pV_p p q )^ @ whiskerR (whiskerR r q ^) q @ concat_pV_p p' q
  = r.
Proof.
  destruct p, r, q. reflexivity.
Defined.

Definition concat_concat2 {A : Type} {x y z : A} {p p' p'' : x = y} {q q' q'' : y = z}
  (a : p = p') (b : p' = p'') (c : q = q') (d : q' = q'') :
  (a @@ c ) @ (b @@ d ) = (a @ b ) @@ (c @ d ).
Proof.
  case d.
  case c.
  case b.
  case a.
  reflexivity.
Defined.

Definition concat_whisker {A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') :
  (whiskerR a q ) @ (whiskerL p' b ) = (whiskerL p b ) @ (whiskerR a q').
  destruct b, a; symmetry; eapply concat_1p.
Defined.

Definition pentagon {A : Type} {v w x y z : A} (p : v = w) (q : w = x) (r : x = y) (s : y = z)
  : whiskerL p (concat_p_pp q r s)
      @ concat_p_pp p (q@r) s
      @ whiskerR (concat_p_pp p q r) s
  = concat_p_pp p q (r@s) @ concat_p_pp (p@q) r s.
Proof.
  case p, q, r, s. reflexivity.
Defined.

Definition triangulator {A : Type} {x y z : A} (p : x = y) (q : y = z)
  : concat_p_pp p 1 q @ whiskerR (concat_p1 p) q
  = whiskerL p (concat_1p q).
Proof.
  case p, q. reflexivity.
Defined.

Definition eckmann_hilton {A : Type} {x:A} (p q : 1 = 1 :> (x = x )) : p @ q = q @ p :=
  (whiskerR_p1 p @@ whiskerL_1p q )^
  @ (concat_p1 _ @@ concat_p1 _)
  @ (concat_1p _ @@ concat_1p _)
  @ (concat_whisker _ _ _ _ p q )
  @ (concat_1p _ @@ concat_1p _)^
  @ (concat_p1 _ @@ concat_p1 _)^
  @ (whiskerL_1p q @@ whiskerR_p1 p ).

Definition ap02 {A B : Type} (f:A →B) {x y:A} {p q:x =y} (r:p =q) : ap f p = ap f q.
  now destruct r.
Defined.

Definition ap02_pp {A B} (f:A →B) {x y:A} {p p' p'':x =y} (r:p =p') (r':p'=p'')
  : ap02 f (r @ r') = ap02 f r @ ap02 f r'.
Proof.
  case r, r'; reflexivity.
Defined.

Definition ap02_p2p {A B} (f:A →B) {x y z:A} {p p':x =y} {q q':y =z} (r:p =p') (s:q =q')
  : ap02 f (r @@ s) = ap_pp f p q
                      @ (ap02 f r @@ ap02 f s )
                      @ (ap_pp f p' q')^.
Proof.
  case r, s, p, q. reflexivity.
Defined.

Definition apD02 {A : Type} {B : A → Type} {x y : A} {p q : x = y}
  (f : ∀ x, B x) (r : p = q)
  : apD f p = transport2 B r (f x) @ apD f q.
  destruct r; symmetry; eapply concat_1p.
Defined.

Definition apD02_const {A B : Type} (f : A → B) {x y : A} {p q : x = y} (r : p = q)
: apD02 f r = (apD_const f p )
              @ (transport2_const r (f x) @@ ap02 f r )
              @ (concat_p_pp _ _ _)^
              @ (whiskerL (transport2 _ r (f x)) (apD_const f q )^).
  now destruct r, p.
Defined.

Definition apD02_pp {A} (B : A → Type) (f : ∀ x:A, B x) {x y : A}
  {p1 p2 p3 : x = y} (r1 : p1 = p2) (r2 : p2 = p3)
  : apD02 f (r1 @ r2)
  = apD02 f r1
  @ whiskerL (transport2 B r1 (f x)) (apD02 f r2)
  @ concat_p_pp _ _ _
  @ (whiskerR (transport2_p2p B r1 r2 (f x))^ (apD f p3)).
Proof.
  destruct r1, r2. destruct p1. reflexivity.
Defined.

Definition ap_transport_Vp_idmap {A B} (p q : A = B) (r : q = p) (z : A)
: ap (transport idmap q ^) (ap (fun s ⇒ transport idmap s z) r)
  @ ap (fun s ⇒ transport idmap s (p # z)) (inverse2 r)
  @ transport_Vp idmap p z
  = transport_Vp idmap q z.
Proof.
  now destruct r, q.
Defined.

Definition ap_transport_pV_idmap {A B} (p q : A = B) (r : q = p) (z : B)
: ap (transport idmap q) (ap (fun s ⇒ transport idmap s ^ z) r)
  @ ap (fun s ⇒ transport idmap s (p ^ # z)) r
  @ transport_pV idmap p z
  = transport_pV idmap q z.
Proof.
  now destruct r, q.
Defined.

Notation concatR := (fun p q ⇒ concat q p).

#[global]
Hint Resolve
  concat_1p concat_p1 concat_p_pp
  inv_pp inv_V
: path_hints.

#[global]
Hint Rewrite
@concat_p1
@concat_1p
@concat_p_pp
@concat_pV
@concat_Vp
@concat_V_pp
@concat_p_Vp
@concat_pp_V
@concat_pV_p

@inv_V
@moveR_Mp
@moveR_pM
@moveL_Mp
@moveL_pM
@moveL_1M
@moveL_M1
@moveR_M1
@moveR_1M
@ap_1

@inverse_ap
@ap_idmap

@ap_const

@apD10_1
:paths.

Ltac hott_simpl :=
  autorewrite with paths in × |- × ; auto with path_hints.

If a space is contractible, then any two points in it are connected by a path in a canonical way.

Definition path_contr `{Contr A} (x y : A) : x = y
:= (contr x )^ @ (contr y ).

Similarly, any two parallel paths in a contractible space are homotopic, which is just the principle UIP.

Definition path2_contr `{Contr A} {x y : A} (p q : x = y) : p = q.
Proof.
  assert (K : ∀ (r : x = y), r = path_contr x y).
    intro r; destruct r; symmetry; now apply concat_Vp.
  transitivity (path_contr x y). apply K. symmetry; apply K.
Defined.

It follows that any space of paths in a contractible space is contractible. Because Contr is a notation, and Contr_internal is the record, we need to iota expand to fool Coq's typeclass machinery into accepting supposedly "mismatched" contexts.

Global Instance contr_paths_contr `{Contr A} (x y : A) : Contr (x = y) | 10000 := let c := {|
center := (contr x)^ @ contr y;
contr := path2_contr ((contr x)^ @ contr y)
|} in c.

Also, the total space of any based path space is contractible. We define the contr fields as separate definitions, so that we can give them simpl nomatch annotations.

Definition path_basedpaths {X : Type} {x y : X} (p : x = y)
: (x ;1) = (y ;p ) :> {z :X & x =z }.
Proof.
  destruct p; reflexivity.
Defined.

Arguments path_basedpaths {X x y} p : simpl nomatch.

Global Instance contr_basedpaths {X : Type} (x : X) : Contr {y : X & x = y } | 100.
Proof.
  ∃ (x ; 1).
  intros [y p]; apply path_basedpaths.
Defined.

Definition path_basedpaths' {X : Type} {x y : X} (p : y = x)
: @existT _ (fun z ⇒ @paths X z x) x 1 = (y ; p ).
Proof.
  destruct p; reflexivity.
Defined.

Global Instance contr_basedpaths' {X : Type} (x : X) : Contr {y : X & y = x } | 100.
Proof.
  refine (BuildContr _ (@existT _ (fun z ⇒ @paths X z x) x 1) _).
  intros [y p]; apply path_basedpaths'.
Defined.

Arguments path_basedpaths' {X x y} p : simpl nomatch.

Definition ap_pr1_path_contr_basedpaths {X : Type}
           {x y z : X} (p : x = y) (q : x = z)
: ap pr1 (path_contr ((y ;p ):{y':X & x = y'}) (z ;q )) = p ^ @ q.
Proof.
  destruct p,q; reflexivity.
Defined.

Definition ap_pr1_path_contr_basedpaths' {X : Type}
           {x y z : X} (p : y = x) (q : z = x)
: ap pr1 (path_contr ((y ;p ):{y':X & y' = x }) (z ;q )) = p @ q ^.
Proof.
  destruct p,q; reflexivity.
Defined.

Definition ap_pr1_path_basedpaths {X : Type}
           {x y : X} (p : x = y)
: ap pr1 (path_basedpaths p) = p.
Proof.
  destruct p; reflexivity.
Defined.

Definition ap_pr1_path_basedpaths' {X : Type}
           {x y : X} (p : y = x)
: ap pr1 (path_basedpaths' p) = p ^.
Proof.
  destruct p; reflexivity.
Defined.

If the domain is contractible, the function is propositionally constant.

Definition contr_dom_equiv {A B} (f : A → B) `{Contr A} : ∀ x y : A, f x = f y
:= fun x y ⇒ ap f ((contr x )^ @ contr y).

Global Instance isequiv_idmap (A : Type) : IsEquiv idmap | 0 :=
BuildIsEquiv A A idmap idmap (fun _ ⇒ 1) (fun _ ⇒ 1) (fun _ ⇒ 1).

Definition equiv_idmap (A : Type) : A <~> A := BuildEquiv A A idmap _.

Arguments equiv_idmap {A} , A.

Notation "1" := equiv_idmap : equiv_scope.

Global Instance reflexive_equiv : Reflexive Equiv | 0 := @equiv_idmap.

The composition of equivalences is an equivalence.

Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g}
  : IsEquiv (compose g f) | 1000
  := BuildIsEquiv A C (compose g f)
    (compose f^-1 g^-1)
    (fun c ⇒ ap g (eisretr f (g^-1 c)) @ eisretr g c)
    (fun a ⇒ ap (f^-1) (eissect g (f a)) @ eissect f a)
    (fun a ⇒
      (whiskerL _ (eisadj g (f a))) @
      (ap_pp g _ _)^ @
      ap02 g
      ( (concat_A1p (eisretr f) (eissect g (f a)))^ @
        (ap_compose f^-1 f _ @@ eisadj f a ) @
        (ap_pp f _ _)^
      ) @
      (ap_compose f g _)^
    ).

Definition isequiv_compose'
  {A B : Type} (f : A → B) (_ : IsEquiv f)
  {C : Type} (g : B → C) (_ : IsEquiv g)
  : IsEquiv (g o f)
  := isequiv_compose.

Definition equiv_compose {A B C : Type} (g : B → C) (f : A → B)
  `{IsEquiv B C g} `{IsEquiv A B f}
  : A <~> C
  := BuildEquiv A C (compose g f) _.

Definition equiv_compose' {A B C : Type} (g : B <~> C) (f : A <~> B)
  : A <~> C
  := equiv_compose g f.

We put g and f in equiv_scope explcitly. This is a partial work-around for https://coq.inria.fr/bugs/show_bug.cgi?id=3990, which is that implicitly bound scopes don't nest well.

Notation "g 'oE' f" := (equiv_compose' g%equiv f%equiv) (at level 40, left associativity) : equiv_scope.

Global Instance transitive_equiv : Transitive Equiv | 0 :=
fun _ _ _ f g ⇒ equiv_compose g f.

Anything homotopic to an equivalence is an equivalence.

Section IsEquivHomotopic.

  Context {A B : Type} (f : A → B) {g : A → B}.
  Context `{IsEquiv A B f}.
  Hypothesis h : f == g.

  Let sect := (fun b:B ⇒ (h (f ^-1 b))^ @ eisretr f b).
  Let retr := (fun a:A ⇒ (ap f ^-1 (h a))^ @ eissect f a).

  Let adj (a : A) : sect (g a) = ap g (retr a).
  Proof.
    unfold sect, retr.
    rewrite ap_pp. apply moveR_Vp.
    rewrite concat_p_pp, <- concat_Ap, concat_pp_p, <- concat_Ap.
    rewrite ap_V; apply moveL_Vp.
    rewrite <- ap_compose; rewrite (concat_A1p (eisretr f) (h a)).
    apply whiskerR, eisadj.
  Qed.

  Definition isequiv_homotopic : IsEquiv g
    := BuildIsEquiv _ _ g (f ^-1) sect retr adj.

  Definition equiv_homotopic : A <~> B
    := BuildEquiv _ _ g isequiv_homotopic.

End IsEquivHomotopic.

The inverse of an equivalence is an equivalence.

Section EquivInverse.

  Context {A B : Type} (f : A → B) {feq : IsEquiv f}.

  Theorem other_adj (b : B) : eissect f (f ^-1 b) = ap f ^-1 (eisretr f b).
  Proof.
    rewrite <- (concat_1p (eissect _ _)).
    rewrite <- (concat_Vp (ap f ^-1 (eisretr f (f (f ^-1 b))))).
    rewrite (whiskerR (inverse2 (ap02 f ^-1 (eisadj f (f ^-1 b)))) _).
    refine (whiskerL _ (concat_1p (eissect _ _))^ @ _).
    rewrite <- (concat_Vp (eissect f (f ^-1 (f (f ^-1 b ))))).
    rewrite <- (whiskerL _ (concat_1p (eissect f (f ^-1 (f (f ^-1 b )))))).
    rewrite <- (concat_pV (ap f ^-1 (eisretr f (f (f ^-1 b))))).
    apply moveL_M1.
    repeat rewrite concat_p_pp.
    rewrite <- (concat_pp_A1 (fun a ⇒ (eissect f a )^) _ _).
    rewrite (ap_compose' f f ^-1).
    rewrite <- (ap_p_pp _ _ (ap f (ap f ^-1 (eisretr f (f (f ^-1 b))))) _).
    rewrite <- (ap_compose f ^-1 f).
    rewrite (concat_A1p (eisretr f) _).
    rewrite ap_pp, concat_p_pp.
    rewrite (concat_pp_V _ (ap f ^-1 (eisretr f (f (f ^-1 b))))).
    repeat rewrite <- ap_V; rewrite <- ap_pp.
    rewrite <- (concat_pA1 (fun y ⇒ (eissect f y )^) _).
    rewrite ap_compose', <- (ap_compose f ^-1 f).
    rewrite <- ap_p_pp.
    rewrite (concat_A1p (eisretr f) _).
    rewrite concat_p_Vp.
    rewrite <- ap_compose.
    rewrite (concat_pA1_p (eissect f) _).
    rewrite concat_pV_p; apply concat_Vp.
  Qed.

  Global Instance isequiv_inverse : IsEquiv f ^-1 | 10000
    := BuildIsEquiv B A f ^-1 f (eissect f) (eisretr f) other_adj.
End EquivInverse.

If the goal is IsEquiv _^-1, then use isequiv_inverse; otherwise, don't pretend worry about if the goal is an evar and we want to add a ^-1.

#[global]
Hint Extern 0 (IsEquiv _^-1) ⇒ apply @isequiv_inverse : typeclass_instances.

Equiv A B is a symmetric relation.

Theorem equiv_inverse {A B : Type} : (A <~> B ) → (B <~> A ).
Proof.
  intro e.
  ∃ (e^-1).
  apply isequiv_inverse.
Defined.

Notation "e ^-1" := (@equiv_inverse _ _ e) : equiv_scope.

Global Instance symmetric_equiv : Symmetric Equiv | 0 := @equiv_inverse.

If g \o f and f are equivalences, so is g. This is not an Instance because it would require Coq to guess f.

Definition cancelR_isequiv {A B C} (f : A → B) {g : B → C}
  `{IsEquiv A B f} `{IsEquiv A C (g o f )}
  : IsEquiv g
  := isequiv_homotopic (compose (compose g f) f ^-1)
       (fun b ⇒ ap g (eisretr f b)).

Definition cancelR_equiv {A B C} (f : A → B) {g : B → C}
  `{IsEquiv A B f} `{IsEquiv A C (g o f )}
  : B <~> C
  := BuildEquiv B C g (cancelR_isequiv f).

If g \o f and g are equivalences, so is f.

Definition cancelL_isequiv {A B C} (g : B → C) {f : A → B}
  `{IsEquiv B C g} `{IsEquiv A C (g o f )}
  : IsEquiv f
  := isequiv_homotopic (compose g ^-1 (compose g f))
       (fun a ⇒ eissect g (f a)).

Definition cancelL_equiv {A B C} (g : B → C) {f : A → B}
  `{IsEquiv B C g} `{IsEquiv A C (g o f )}
  : A <~> B
  := BuildEquiv _ _ f (cancelL_isequiv g).

Combining these with isequiv_compose, we see that equivalences can be transported across commutative squares.

Definition isequiv_commsq {A B C D}
           (f : A → B) (g : C → D) (h : A → C) (k : B → D)
           (p : k o f == g o h)
           `{IsEquiv _ _ f} `{IsEquiv _ _ h} `{IsEquiv _ _ k}
: IsEquiv g.
Proof.
  refine (@cancelR_isequiv _ _ _ h g _ _).
  refine (isequiv_homotopic _ p).
Defined.

Definition isequiv_commsq' {A B C D}
           (f : A → B) (g : C → D) (h : A → C) (k : B → D)
           (p : g o h == k o f)
           `{IsEquiv _ _ g} `{IsEquiv _ _ h} `{IsEquiv _ _ k}
: IsEquiv f.
Proof.
  refine (@cancelL_isequiv _ _ _ k f _ _).
  refine (isequiv_homotopic _ p).
Defined.

Transporting is an equivalence.

Section EquivTransport.

  Context {A : Type} (P : A → Type) (x y : A) (p : x = y).

  Global Instance isequiv_transport : IsEquiv (transport P p) | 0
    := BuildIsEquiv (P x) (P y) (transport P p) (transport P p ^)
    (transport_pV P p) (transport_Vp P p) (transport_pVp P p).

  Definition equiv_transport : P x <~> P y
    := BuildEquiv _ _ (transport P p) _.

End EquivTransport.

In all the above cases, we were able to directly construct all the structure of an equivalence. However, as is evident, sometimes it is quite difficult to prove the adjoint law.

The following adjointification theorem allows us to be lazy about this if we wish. It says that if we have all the data of an (adjoint) equivalence except the triangle identity, then we can always obtain the triangle identity by modifying the datum equiv_is_section (or equiv_is_retraction). The proof is the same as the standard categorical argument that any equivalence can be improved to an adjoint equivalence.

As a stylistic matter, we try to avoid using adjointification in the library whenever possible, to preserve the homotopies specified by the user.

Section Adjointify.

  Context {A B : Type} (f : A → B) (g : B → A).
  Context (isretr : Sect g f) (issect : Sect f g).

  Let issect' := fun x ⇒
    ap g (ap f (issect x )^) @ ap g (isretr (f x)) @ issect x.

  Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a).
  Proof.
    unfold issect'.
    apply moveR_M1.
    repeat rewrite ap_pp, concat_p_pp; rewrite <- ap_compose.
    rewrite (concat_pA1 (fun b ⇒ (isretr b )^) (ap f (issect a)^)).
    repeat rewrite concat_pp_p; rewrite ap_V; apply moveL_Vp; rewrite concat_p1.
    rewrite concat_p_pp, <- ap_compose.
    rewrite (concat_pA1 (fun b ⇒ (isretr b )^) (isretr (f a))).
    rewrite concat_pV, concat_1p; reflexivity.
  Qed.

We don't make this a typeclass instance, because we want to control when we are applying it.

  Definition isequiv_adjointify : IsEquiv f
    := BuildIsEquiv A B f g isretr issect' is_adjoint'.

  Definition equiv_adjointify : A <~> B
    := BuildEquiv A B f isequiv_adjointify.

End Adjointify.

Arguments isequiv_adjointify {A B}%type_scope (f g)%function_scope isretr issect.
Arguments equiv_adjointify {A B}%type_scope (f g)%function_scope isretr issect.

An involution is an endomap that is its own inverse.

Definition isequiv_involution {X : Type} (f : X → X) (isinvol : Sect f f)
: IsEquiv f
:= isequiv_adjointify f f isinvol isinvol.

Definition equiv_involution {X : Type} (f : X → X) (isinvol : Sect f f)
: X <~> X
:= equiv_adjointify f f isinvol isinvol.

Several lemmas useful for rewriting.

Definition moveR_equiv_M `{IsEquiv A B f} (x : A) (y : B) (p : x = f ^-1 y)
  : (f x = y)
  := ap f p @ eisretr f y.

Definition moveL_equiv_M `{IsEquiv A B f} (x : A) (y : B) (p : f ^-1 y = x)
  : (y = f x)
  := (eisretr f y )^ @ ap f p.

Definition moveR_equiv_V `{IsEquiv A B f} (x : B) (y : A) (p : x = f y)
  : (f ^-1 x = y)
  := ap (f ^-1) p @ eissect f y.

Definition moveL_equiv_V `{IsEquiv A B f} (x : B) (y : A) (p : f y = x)
  : (y = f ^-1 x)
  := (eissect f y )^ @ ap (f ^-1) p.

Equivalence preserves contractibility (which of course is trivial under univalence).

Lemma contr_equiv A {B} (f : A → B) `{IsEquiv A B f} `{Contr A}
  : Contr B.
Proof.
  ∃ (f (center A)).
  intro y.
  apply moveR_equiv_M.
  apply contr.
Qed.

Definition contr_equiv' A {B} `(f : A <~> B) `{Contr A}
  : Contr B
  := contr_equiv A f.

Any two contractible types are equivalent.

Global Instance isequiv_contr_contr {A B : Type}
       `{Contr A} `{Contr B} (f : A → B)
  : IsEquiv f
  := BuildIsEquiv _ _ f (fun _ ⇒ (center A))
                  (fun x ⇒ path_contr _ _)
                  (fun x ⇒ path_contr _ _)
                  (fun x ⇒ path_contr _ _).

Lemma equiv_contr_contr {A B : Type} `{Contr A} `{Contr B}
  : (A <~> B).
Proof.
  apply equiv_adjointify with (fun _ ⇒ center B) (fun _ ⇒ center A);
  intros ?; apply contr.
Defined.

Assuming function extensionality, composing with an equivalence is itself an equivalence

Global Instance isequiv_precompose `{Funext} {A B C : Type}
  (f : A → B) `{IsEquiv A B f}
  : IsEquiv (fun (g:B →C) ⇒ g o f) | 1000
  := isequiv_adjointify (fun (g:B→C) ⇒ g o f)
    (fun h ⇒ h o f^-1)
    (fun h ⇒ path_forall _ _ (fun x ⇒ ap h (eissect f x)))
    (fun g ⇒ path_forall _ _ (fun y ⇒ ap g (eisretr f y))).

Definition equiv_precompose `{Funext} {A B C : Type}
  (f : A → B) `{IsEquiv A B f}
  : (B → C ) <~> (A → C )
  := BuildEquiv _ _ (fun (g:B →C) ⇒ g o f) _.

Definition equiv_precompose' `{Funext} {A B C : Type} (f : A <~> B)
  : (B → C ) <~> (A → C )
  := BuildEquiv _ _ (fun (g:B →C) ⇒ g o f) _.

Global Instance isequiv_postcompose `{Funext} {A B C : Type}
  (f : B → C) `{IsEquiv B C f}
  : IsEquiv (fun (g:A →B) ⇒ f o g) | 1000
  := isequiv_adjointify (fun (g:A→B) ⇒ f o g)
    (fun h ⇒ f^-1 o h)
    (fun h ⇒ path_forall _ _ (fun x ⇒ eisretr f (h x)))
    (fun g ⇒ path_forall _ _ (fun y ⇒ eissect f (g y))).

Definition equiv_postcompose `{Funext} {A B C : Type}
  (f : B → C) `{IsEquiv B C f}
  : (A → B ) <~> (A → C )
  := BuildEquiv _ _ (fun (g:A →B) ⇒ f o g) _.

Definition equiv_postcompose' `{Funext} {A B C : Type} (f : B <~> C)
  : (A → B ) <~> (A → C )
  := BuildEquiv _ _ (fun (g:A →B) ⇒ f o g) _.

Conversely, if pre- or post-composing with a function is always an equivalence, then that function is also an equivalence. It's convenient to know that we only need to assume the equivalence when the other type is the domain or the codomain.

Definition isequiv_isequiv_precompose {A B : Type} (f : A → B)
  (precomp := (fun (C : Type) (h : B → C) ⇒ h o f))
  (Aeq : IsEquiv (precomp A)) (Beq : IsEquiv (precomp B))
  : IsEquiv f.
Proof.
  assert (H : ∀ (C D : Type)
                     (Ceq : IsEquiv (precomp C)) (Deq : IsEquiv (precomp D))
                     (k : C → D) (h : A → C),
                k o (precomp C )^-1 h = (precomp D )^-1 (k o h )).
  { intros C D ? ? k h.
    transitivity ((precomp D)^-1 (k o (precomp C ((precomp C )^-1 h )))).
    - transitivity ((precomp D)^-1 (precomp D (k o ((precomp C )^-1 h )))).
      + rewrite (eissect (precomp D) _); reflexivity.
      + reflexivity.
    - rewrite (eisretr (precomp C) h); reflexivity. }
  refine (isequiv_adjointify f ((precomp A)^-1 idmap) _ _).
  - intros x.
    change ((f o (precomp A)^-1 idmap ) x = idmap x).
    apply ap10.
    rewrite (H A B Aeq Beq).
    change ((precomp B)^-1 (precomp B idmap ) = idmap).
    apply eissect.
  - intros x.
    change ((precomp A ((precomp A)^-1 idmap)) x = idmap x).
    apply ap10, eisretr.
Qed.

If f is an equivalence, then so is ap f. We are lazy and use adjointify.

Global Instance isequiv_ap `{IsEquiv A B f} (x y : A)
: