{A : Type} {a0 : A} (R S : A -> Type) (r0 : R a0) (s0 : S a0) := {f : forall a : A, R a -> S a & f a0 r0 = s0}.
Require Import Basics. Require Import Types.Sigma Types.Equiv Types.Paths. Require Import HoTT.Tactics.