Pointed dependent functions

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-05-07.
Last modified on 2025-10-31.

module structured-types.pointed-dependent-functions where
Imports 
open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.identity-types
open import foundation.universe-levels

open import structured-types.pointed-families-of-types
open import structured-types.pointed-types

Idea

A pointed dependent function into a pointed family B over A is a dependent function of the underlying family taking the base point of A to the base point of B.

module _
  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Fam l2 A)
  where

  pointed-Π : UU (l1 ⊔ l2)
  pointed-Π =
    fiber
      ( ev-point (point-Pointed-Type A) {fam-Pointed-Fam A B})
      ( point-Pointed-Fam A B)

  Π∗ = pointed-Π

Note: the subscript asterisk symbol used for the pointed dependent function type Π∗, and pointed type constructions in general, is the asterisk operator ∗ (agda-input: \ast), not the asterisk *.

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A}
  where

  function-pointed-Π :
    pointed-Π A B → (x : type-Pointed-Type A) → fam-Pointed-Fam A B x
  function-pointed-Π = pr1

  preserves-point-function-pointed-Π :
    (f : pointed-Π A B) →
    function-pointed-Π f (point-Pointed-Type A) ＝ point-Pointed-Fam A B
  preserves-point-function-pointed-Π = pr2

Recent changes