Faithful pointed maps

module structured-types.faithful-pointed-maps where

Imports

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

Idea

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

Definition

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 A B f))

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

  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 A B 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 A B pointed-map-faithful-pointed-map

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