`{H0 : Funext} {A : Type} {B : A -> pType} (P : forall (C : A -> pType) (g : forall a, B a ->* C a), Type) (H : forall (C : A -> Type) (g : forall a, B a -> C a), P _ (fun a => pmap_from_pointed (g a))) : forall (C : A -> pType) (g : forall a, B a ->* C a), P C g. Proof. equiv_intros (equiv_functor_arrow' (equiv_idmap A) issig_ptype oE equiv_sig_coind _ _) C. destruct C as [C c0]. equiv_intros (@equiv_functor_forall_id _ A _ _ (fun a => issig_pmap (B a) [C a, c0 a]) oE equiv_sig_coind _ _) g. simpl in *. destruct g as [g g0]. unfold point in g0. unfold functor_forall, sig_coind_uncurried. simpl. pose (path_forall _ c0 g0). assert (p = path_forall (fun x : A => g x (ispointed_type (B x))) c0 g0). 1: reflexivity. induction p. apply moveR_equiv_V in X. induction X. apply H. Defined.
Require Import Basics Types. Require Import Pointed.Core.