Dependent products of pointed types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-13.
Last modified on 2023-09-15.

module structured-types.dependent-products-pointed-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import structured-types.pointed-types

Idea

Given a family of pointed types Mᵢ indexed by i : I, the dependent product Π(i : I), Mᵢ is a pointed type consisting of dependent functions taking i : I to an element of the underlying type of Mᵢ. The base point is given pointwise.

Definition

Π-Pointed-Type :
  {l1 l2 : Level} (I : UU l1) (P : I → Pointed-Type l2) → Pointed-Type (l1 ⊔ l2)
pr1 (Π-Pointed-Type I P) = (x : I) → type-Pointed-Type (P x)
pr2 (Π-Pointed-Type I P) x = point-Pointed-Type (P x)

Recent changes