(A : Type) (B : A -> Type) (C : A -> Type) (D : forall a, B a -> C a -> Type) {cac : Contr {x:A & C x} } (a : A) (c : C a) {ccd : Contr {y:B a & D a y c } } : Contr {ab : {x:A & B x} & {y:C ab.1 & D ab.1 ab.2 y} }. Proof. pose (d := (center {y:B a & D a y c}).2). set (b := (center {y:B a & D a y c}).1) in *. apply (Build_Contr _ ((a;b);(c;d))). intros [[a' b'] [c' d']]; cbn in *. pose (ac' := (a';c')). pose (bd' := (b';d') : {y:B ac'.1 & D ac'.1 y ac'.2}). change (((a;b);(c;d)) = ((ac'.1;bd'.1);(ac'.2;bd'.2)) :> {ab : {x:A & B x} & {y:C ab.1 & D ab.1 ab.2 y} }). clearbody ac' bd'; clear a' b' c' d'. destruct (@path_contr {x:A & C x} _ (a;c) ac'). destruct (@path_contr {y:B a & D a y c} _ (b;d) bd'). reflexivity. Defined.
Require Import Basics. Require Import Types.Sigma Types.Equiv Types.Paths. Require Import HoTT.Tactics.