FLAT CODISCRETE MODALITY

The modality in cohesive type theory maps a type to its codiscrete version, preserving its grade. For a type , forgets discrete structure, modeling codiscrete spaces in differential cohomology.

In Urs, operates on types in graded universes from , with applications in smooth geometry and differential cohomology .

Formation

(Flat Modality Formation). The modality is a type operator on graded universes, preserving the grade.

def flat (i : Nat) (g : Grade) (A : U i g) : U i g
(* Flat codiscrete modality *)

Introduction

(Flat Modality Introduction). The modality is applied to a type , producing with the same grade.

(* Applied via flat i g A *)
(* Flat modality introduction *)

Elimination

(Flat Modality Elimination). The eliminator for maps codiscrete types to properties in .

def flat_ind (i : Nat) (g : Grade) (A : U i g)
    (phi : (flat i g A) -> U_0)
    (h : Π (a : flat i g A), phi a)
  : Π (a : flat i g A), phi a

Theorems

(Idempotence of Flat). The modality is idempotent, reflecting its role as a codiscrete projection.

def flat_idem (i : Nat) (g : Grade) (A : U i g) : (flat i g (flat i g A)) = (flat i g A)
(* Idempotence: flat (flat A) = flat A *)

(Flat on Smooth Sets). For , models the codiscrete topology on .

def flat_smthset (i : Nat) (g : Grade) (X : SmthSet) : U i g := flat i g X
(* Flat on smooth sets: codiscrete topology *)