🧊 Anders
Modal Homotopy Type System.
type exp =
| EPre of Z.t | EKan of Z.t | EVar of name | EHole (* cosmos *)
| EPi of exp * (name * exp) | ELam of exp * (name * exp) | EApp of exp * exp (* pi *)
| ESig of exp * (name * exp) | EPair of tag * exp * exp | EFst of exp | ESnd of exp (* sigma *)
| EId of exp | ERef of exp | EJ of exp | EField of exp * string (* strict equality *)
| EPathP of exp | EPLam of exp | EAppFormula of exp * exp (* path equality *)
| EI | EDir of dir | EAnd of exp * exp | EOr of exp * exp | ENeg of exp (* CCHM interval *)
| ETransp of exp * exp | EHComp of exp * exp * exp * exp (* Kan operations *)
| EPartial of exp | EPartialP of exp * exp | ESystem of exp System.t (* partial functions *)
| ESub of exp * exp * exp | EInc of exp * exp | EOuc of exp (* cubical subtypes *)
| EGlue of exp | EGlueElem of exp * exp * exp | EUnglue of exp (* glueing *)
| EEmpty | EIndEmpty of exp (* 𝟎 *)
| EUnit | EStar | EIndUnit of exp (* 𝟏 *)
| EBool | EFalse | ETrue | EIndBool of exp (* 𝟐 *)
| EW of exp * (name * exp) | ESup of exp * exp | EIndW of exp * exp * exp (* W *)
| EIm of exp | EInf of exp | EIndIm of exp * exp | EJoin of exp (* Infinitesimal Modality *)
| ECoeq of exp | EIota of exp | EResp of exp | EIndCoeq of exp (* Coequalizer *)
| EDisc of exp | EBase of exp | EHub of exp | ESpoke of exp | EIndDisc of exp (* Disc *)