Pointed dependent functions

module structured-types.pointed-dependent-functions where

Imports

open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.functions
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 of 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-Π =
    fib
      ( 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 *.

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

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