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
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import structured-types.pointed-types


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.


Π-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