Sharp codiscrete maps

Content created by Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2024-09-06.

{-# OPTIONS --cohesion --flat-split #-}

module modal-type-theory.sharp-codiscrete-maps where
Imports 
open import foundation.fibers-of-maps
open import foundation.propositions
open import foundation.universe-levels

open import modal-type-theory.sharp-codiscrete-types

Idea

A map is said to be sharp codiscrete if its fibers are sharp codiscrete.

Definition

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
  where

  is-sharp-codiscrete-map : UU (l1 ⊔ l2)
  is-sharp-codiscrete-map = is-sharp-codiscrete-family (fiber f)

  is-sharp-codiscrete-map-Prop : Prop (l1 ⊔ l2)
  is-sharp-codiscrete-map-Prop = is-sharp-codiscrete-family-Prop (fiber f)

  is-prop-is-sharp-codiscrete-map : is-prop is-sharp-codiscrete-map
  is-prop-is-sharp-codiscrete-map =
    is-prop-type-Prop is-sharp-codiscrete-map-Prop

Recent changes