Faithful pointed maps

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

Created on 2022-07-09.
Last modified on 2023-07-19.

module structured-types.faithful-pointed-maps where
open import foundation.dependent-pair-types
open import foundation.faithful-maps
open import foundation.identity-types
open import foundation.universe-levels

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


A faithful pointed map from A to B is a pointed map from A to B of which the underlying map is faithful.


faithful-pointed-map :
  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)  UU (l1  l2)
faithful-pointed-map A B =
  Σ (A →∗ B)  f  is-faithful (map-pointed-map f))

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
  (f : faithful-pointed-map A B)

  pointed-map-faithful-pointed-map : A →∗ B
  pointed-map-faithful-pointed-map = pr1 f

  map-faithful-pointed-map : type-Pointed-Type A  type-Pointed-Type B
  map-faithful-pointed-map =
    map-pointed-map pointed-map-faithful-pointed-map

  preserves-point-faithful-pointed-map :
    map-faithful-pointed-map (point-Pointed-Type A)  point-Pointed-Type B
  preserves-point-faithful-pointed-map =
    preserves-point-pointed-map pointed-map-faithful-pointed-map

  is-faithful-faithful-pointed-map : is-faithful map-faithful-pointed-map
  is-faithful-faithful-pointed-map = pr2 f

Recent changes