# Pointed dependent functions

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

Created on 2022-05-07.

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 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-Π =
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) →
Id (function-pointed-Π f (point-Pointed-Type A)) (point-Pointed-Fam A B)
preserves-point-function-pointed-Π = pr2