Library MetaCoq.Translations.MiniHoTT_paths

Record sigT {A} (P : A → Type) : Type := existT
  { projT1 : A ; projT2 : P projT1 }.

Definition sigT_ind {A} (B : A → Type) (P : @sigT A B → Type)
           (H : ∀ x y, P (existT _ _ x y))
  : ∀ s, P s.

Record unit : Type := tt { }.


Inductive paths (A : Type) (a : A) : A → Type := idpath : paths A a a.
Definition paths_ind : ∀ A a (P : ∀ y, paths A a y → Type),
    P a (idpath A a) → ∀ y p, P y p.
Defined.
Definition paths_ind_beta : ∀ A a P u, paths _ (paths_ind A a P u a (idpath A a)) u.
Defined.


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





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


Notation idmap := (fun x ⇒ x).



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

Notation "( x ; y )" := (existT _ x y) : fibration_scope.
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).
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.



Global Instance reflexive_paths {A} : Reflexive (@paths A) | 0 := @idpath A.
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.


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.

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


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

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.


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



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.


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


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.



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.


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


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)
                                             }.


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

Coercion equiv_fun : Equiv >-> Funclass.




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) }.


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


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.


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



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

Definition concat_1p {A : Type} {x y : A} (p : x = y) :
  1 @ p = 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.
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).
Defined.

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

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

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

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

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

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

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

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

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

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

Definition inv_V {A : Type} {x y : A} (p : x = y) :
  p^^ = 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.

Definition moveR_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  r = q @ p^ → r @ p = q.

Definition moveR_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
  p = r @ q → r^ @ p = q.

Definition moveR_pV {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) :
  r = q @ p → r @ p^ = q.

Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  r^ @ q = p → q = r @ p.

Definition moveL_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  q @ p^ = r → q = r @ p.

Definition moveL_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
  r @ q = p → q = r^ @ p.

Definition moveL_pV {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) :
  q @ p = r → q = r @ p^.

Definition moveL_1M {A : Type} {x y : A} (p q : x = y) :
  p @ q^ = 1 → p = q.

Definition moveL_M1 {A : Type} {x y : A} (p q : x = y) :
  q^ @ p = 1 → p = q.

Definition moveL_1V {A : Type} {x y : A} (p : x = y) (q : y = x) :
  p @ q = 1 → p = q^.

Definition moveL_V1 {A : Type} {x y : A} (p : x = y) (q : y = x) :
  q @ p = 1 → p = q^.

Definition moveR_M1 {A : Type} {x y : A} (p q : x = y) :
  1 = p^ @ q → p = q.

Definition moveR_1M {A : Type} {x y : A} (p q : x = y) :
  1 = q @ p^ → p = q.

Definition moveR_1V {A : Type} {x y : A} (p : x = y) (q : y = x) :
  1 = q @ p → p^ = q.

Definition moveR_V1 {A : Type} {x y : A} (p : x = y) (q : y = x) :
  1 = p @ q → p^ = q.

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.

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.

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.

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.

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

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

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

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

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

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

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

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

Definition ap_idmap {A : Type} {x y : A} (p : x = y) :
  ap idmap p = 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).
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).
Defined.

Definition ap_const {A B : Type} {x y : A} (p : x = y) (z : B) :
  ap (fun _ ⇒ z) p = 1.
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).
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.
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).
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).

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.

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

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

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

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.

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

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.

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

Lemma concat_1p_1 {A} {x : A} (p : x = x) (q : p = 1)
: concat_1p p @ q = ap (fun p' ⇒ 1 @ p') q.

Lemma concat_p1_1 {A} {x : A} (p : x = x) (q : p = 1)
: concat_p1 p @ q = ap (fun p' ⇒ p' @ 1) q.

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.

Definition apD10_V {A} {B:A→Type} {f g : ∀ x, B x} (h:f=g) (x:A)
  : apD10 (h^) x = (apD10 h x)^.
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).

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

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

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

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

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.

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)^.

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

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

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

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

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)^.
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.
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)).

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

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

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)^.

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

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.

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)^.
Definition transport_const {A B : Type} {x1 x2 : A} (p : x1 = x2) (y : B)
  : transport (fun x ⇒ B) p y = y.

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

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

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.

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.

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