Sharp codiscrete maps
Content created by Fredrik Bakke.
Created on 2023-11-24.
Last modified on 2023-11-24.
{-# 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
is-sharp-codiscrete-map : {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) is-sharp-codiscrete-map f = is-sharp-codiscrete-family (fiber f)
Properties
Being codiscrete is a property
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) where 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 f) is-prop-is-sharp-codiscrete-map = is-prop-type-Prop is-sharp-codiscrete-map-Prop
Recent changes
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).