Dependent products of subtypes

Content created by Egbert Rijke, Fredrik Bakke and Louis Wasserman.

Created on 2025-08-30.
Last modified on 2026-05-02.

module foundation.dependent-products-subtypes where
Imports 
open import foundation.dependent-products-propositions
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

Idea

Given an indexing type I, a type Aᵢ for each i : I, and a subtype Sᵢ ⊆ Aᵢ for each i : I, a function f : (i : I) → Aᵢ is in the dependent product of the subtypes S if for each i, f i ∈ Sᵢ.

Definition

Π-subtype :
  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} →
  ((i : I) → subtype l3 (A i)) →
  subtype (l1 ⊔ l3) ((i : I) → A i)
Π-subtype {I = I} S f = Π-Prop I (λ i → S i (f i))

Recent changes