This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Fibers of pointed maps

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

open import structured-types.pointed-maps
open import structured-types.pointed-types

Definition

fiber-Pointed-Type :
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} →
  (A →∗ B) → Pointed-Type (l1 ⊔ l2)
pr1 (fiber-Pointed-Type f) = fiber (map-pointed-map f) (point-Pointed-Type _)
pr1 (pr2 (fiber-Pointed-Type f)) = point-Pointed-Type _
pr2 (pr2 (fiber-Pointed-Type f)) = preserves-point-pointed-map f