Require Import HoTT FunextAxiom.

Definition f : Bool -> Bool -> Bool :=
  fun x y => if x then y else false.

Definition g : Bool -> Bool -> Bool :=
  fun x y => if y then x else false.

Definition e : f = g.
  apply path_forall; intros x; apply path_forall; intros y.
  destruct x, y; reflexivity.
Defined.

Definition Phi : Bool -> Type :=
  fun x => match x with true => Bool | false => Unit end.

Definition Psi : (Bool->Bool->Bool)->Type :=
  fun u => Phi (u true true) * Phi (u true false) * Phi (u false true) * Phi (u false false).

Definition X : Psi f := (true,tt,tt,tt).

Definition Y : Psi g := transport Psi e X.

(* Binary products in Coq associate to the left *)
Definition puzzle : fst (fst (fst Y)) = true.
Proof.
  unfold Y, X, Psi.
  rewrite !transport_prod; cbn.
  rewrite transport_compose.
  rewrite (ap_compose (fun u => u true) (fun v => v true) e).
  rewrite !ap_apply_l.
  unfold e.
  rewrite !ap10_path_forall.
  reflexivity.
Defined.