SHARP DISCRETE MODALITY

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

In Urs, operates on types in graded universes from , with applications in discrete gauge groups and smooth geometry .

Formation

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

def sharp (i : Nat) (g : Grade) (A : U i g) : U i g

Introduction

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

(* Applied via sharp i g A *)
(* Sharp modality introduction *)

Elimination

(Sharp Modality Elimination). The eliminator for maps discrete types to properties in .

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

Theorems

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

def sharp_idem (i : Nat) (g : Grade) (A : U i g) : (sharp i g (sharp i g A)) = (sharp i g A)
(* Idempotence: sharp (sharp A) = sharp A *)

(Sharp on Smooth Sets). For , models the discrete topology on .

def sharp_smthset (i : Nat) (g : Grade) (X : SmthSet) : U i g := sharp i g X
(* Sharp on smooth sets: discrete topology *)