forked-from-1kasper/bravo

Castle Bravo: Experimental HoTT Implementation

Castle Bravo

type exp =
  | EPre of Z.t | EKan of Z.t                                                 (* cosmos *)
  | EVar of name | EHole                                                   (* variables *)
  | EPi of exp * (name * exp) | ELam of exp * (name * exp) | EApp of exp * exp     (* Π *)
  | ESig of exp * (name * exp) | EPair of exp * exp | ESigMk of exp * exp * exp    (* Σ *)
  | EFst of exp | ESnd of exp | ESigProd of exp * exp * exp * exp * exp            (* Σ *)
  | EPath of exp * exp * exp | EIdp of exp | ERev of exp | ETrans of exp * exp  (* path *)
  | ECoe of exp * exp | EApd of exp * exp                             (* Kan operations *)
  | EUAWeak of exp * exp * exp * exp * exp * exp                          (* univalence *)
  | EN | EZero | ESucc | ENInd of exp                                              (* N *)
  | EZ | EPos | ENeg | EZInd of exp | EZSucc | EZPred                              (* Z *)
  | ES1 | EBase | ELoop | ES1Ind of exp                                           (* S¹ *)
  | ER | Elem | EGlue | ERInd of exp                                               (* R *)
  | EBot | EBotRec of exp                                                          (* ⊥ *)
  | EId of exp | ERefl of exp | EJ of exp                            (* strict equality *)