mu_eq_mu' : transport (fun A : Type => A -> V) path^ mu = mu'. Proof. apply path_forall. intro a'. transitivity (transport (fun X => V) path^ (mu (transport (fun X : Type => X) path^^ a'))). - apply (@transport_arrow Type (fun X : Type => X) (fun X => V) Au Au' path^ mu a'). - transitivity (mu (transport idmap path^^ a')). + apply transport_const. + transitivity (mu (inv_e a')). 2: apply (pr2 (snd eq_img_untrunc a')). refine (ap mu _). transitivity (transport idmap path a'). * exact (ap (fun x => transport idmap x a') (inv_V path)). * apply transport_path_universe. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.