{A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem R r0} (S : A -> Type) (s0 : S a0) : exists f : pfamMap R S r0 s0, forall g, pfammap_homotopy f g. Proof. pose (to_S := idsys_ind (fun a _ => S a) s0). pose proof (to_S_beta := idsys_ind_beta (fun a _ => S a) s0). snrefine ((to_S; to_S_beta); _). intro g. exists (idsys_ind (fun a r => to_S a r = pr1 g a r) (to_S_beta @ (pr2 g)^)). snrapply idsys_ind_beta. Defined.
Require Import Basics. Require Import Types.Sigma Types.Equiv Types.Paths. Require Import HoTT.Tactics.