theorem2_6_5.v

Require Import HoTT.

Theorem theorem2_6_5' {A A'} {P : A -> Type} {P' : A' -> Type} (g : A -> A') (h : forall a, P a -> P' (g a)) (x y : sigT P) (p : x.1 = y.1)\
 (q : transport _ p x.2 = y.2) :  Type.

  pose (fun z => (g z.1 ; h z.1 z.2)) as f.
  refine (ap f (path_sigma P x y p q) = path_sigma P' (f x) (f y) (ap g p) _).
  subst f; simpl.
  destruct q.
  destruct p.
  reflexivity.

  Eval simpl in (fun (A A' : Type) (P : A -> Type) (P' : A' -> Type)
   (g : A -> A') (h : forall a : A, P a -> P' (g a))
   (x : exists x, P x) (y : exists x, P x) (p : x .1 = y .1)
   (q : transport P p x .2 = y .2) =>
 let f := fun z : exists x, P x => (g z .1; h z .1 z .2) in
 ap f (path_sigma P x y p q) =
 path_sigma P' (f x) (f y) (ap g p)
   (match
      q in (_ = y0) return (transport P' (ap g p) (h x .1 x .2) = h y .1 y0)
    with
    | 1%path =>
        match
          p as p1 in (_ = y0)
          return
            (transport P' (ap g p1) (h x .1 x .2) =
             h y0 (transport P p1 x .2))
        with
        | 1%path => 1%path
        end
    end)).