Sharp codiscrete types

Content created by Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2023-11-24.

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

module where
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.function-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.transport-along-equivalences
open import foundation.universe-levels

open import

open import orthogonal-factorization-systems.higher-modalities


A type is said to be (sharp) codiscrete if it is sharp modal, i.e. if the sharp unit is an equivalence at that type.

We postulate that codiscrete types are closed under

  • the formation of identity types
  • the formation of dependent function types
  • the formation of the subuniverse of codiscrete types.

Please note that there is some redundancy between the axioms that are assumed here and in the files on the flat-sharp adjunction, and the file on the sharp modality, and they may be subject to change in the future.


is-sharp-codiscrete : {l : Level} (A : UU l)  UU l
is-sharp-codiscrete {l} A = is-equiv (unit-sharp {l} {A})

is-sharp-codiscrete-family :
  {l1 l2 : Level} {A : UU l1} (B : A  UU l2)  UU (l1  l2)
is-sharp-codiscrete-family {A = A} B = (x : A)  is-sharp-codiscrete (B x)

Sharp-Codiscrete : (l : Level)  UU (lsuc l)
Sharp-Codiscrete l = Σ (UU l) (is-sharp-codiscrete)


The identity types of are codiscrete

  is-sharp-codiscrete-Id-sharp :
    {l1 : Level} {A : UU l1} (x y :  A)  is-sharp-codiscrete (x  y)

is-sharp-codiscrete-Id :
  {l1 : Level} {A : UU l1} (x y : A) 
  is-sharp-codiscrete A  is-sharp-codiscrete (x  y)
is-sharp-codiscrete-Id x y is-sharp-codiscrete-A =
    ( is-sharp-codiscrete)
    ( inv-equiv-ap-is-emb (is-emb-is-equiv is-sharp-codiscrete-A))
    ( is-sharp-codiscrete-Id-sharp (unit-sharp x) (unit-sharp y))

A Π-type is codiscrete if its codomain is

  is-sharp-codiscrete-Π :
    {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
    ((x : A)  is-sharp-codiscrete (B x)) 
    is-sharp-codiscrete ((x : A)  B x)

The universe of codiscrete types is codiscrete

  is-sharp-codiscrete-Sharp-Codiscrete :
    (l : Level)  is-sharp-codiscrete (Sharp-Codiscrete l)


Being codiscrete is a property

module _
  {l : Level} (A : UU l)

  is-sharp-codiscrete-Prop : Prop l
  is-sharp-codiscrete-Prop = is-equiv-Prop (unit-sharp {l} {A})

  is-property-is-sharp-codiscrete : is-prop (is-sharp-codiscrete A)
  is-property-is-sharp-codiscrete = is-prop-type-Prop is-sharp-codiscrete-Prop

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

  is-sharp-codiscrete-family-Prop : Prop (l1  l2)
  is-sharp-codiscrete-family-Prop = Π-Prop A (is-sharp-codiscrete-Prop  B)

  is-property-is-sharp-codiscrete-family :
    is-prop (is-sharp-codiscrete-family B)
  is-property-is-sharp-codiscrete-family =
    is-prop-type-Prop is-sharp-codiscrete-family-Prop

Codiscreteness is a higher modality

module _
  (l : Level)

  is-higher-modality-sharp :
    is-higher-modality (sharp-locally-small-operator-modality l) (unit-sharp)
  pr1 is-higher-modality-sharp = induction-principle-sharp
  pr2 is-higher-modality-sharp X = is-sharp-codiscrete-Id-sharp

  sharp-higher-modality : higher-modality l l
  pr1 sharp-higher-modality = sharp-locally-small-operator-modality l
  pr1 (pr2 sharp-higher-modality) = unit-sharp
  pr2 (pr2 sharp-higher-modality) = is-higher-modality-sharp

Types in the image of are codiscrete

is-sharp-codiscrete-sharp : {l : Level} (X : UU l)  is-sharp-codiscrete ( X)
is-sharp-codiscrete-sharp {l} =
  is-modal-operator-type-higher-modality (sharp-higher-modality l)

See also

Recent changes