module foundations.pi-type-distributes-over-sigma-type where
open import foundations.universe open import foundations.identity-type open import foundations.sigma-type
private variable ℓ : Level A : Type ℓ B : A → Type ℓ C : (a : A) → B a → Type ℓ Π-dist-Σ : ((a : A) → Σ (B a) (C a)) → Σ[ f ∈ ((a : A) → B a) ] ((a : A) → C a (f a)) Π-dist-Σ g .fst a = g a .fst Π-dist-Σ g .snd a = g a .snd