fact: Fixpoint map_family_prod {F G : I → Type} {ℓ : list I} (f : ∀ i, F i → G i) : FamilyProd F ℓ → FamilyProd G ℓ := match ℓ with | nil => const_tt _ | i :: ℓ' => λ '(x,s), (f i x, map_family_prod f s) end.
imports: HoTT.Utf8Minimal HoTT.Basics.Overture Types.Unit HoTT.Classes.implementations.list