module Cof = Kado.Syntax.Endo
type t =
| Var of int
| Global of Global.t
| Let of t * Ident.t * t
| Ann of t * tp
| Zero
| Suc of t
| NatElim of t * t * t * t
| Base
| Loop of t
| CircleElim of t * t * t * t
| Lam of Ident.t * t
| Ap of t * t
| Pair of t * t
| Fst of t
| Snd of t
| Struct of fields
| Proj of t * Ident.t * int
| Coe of t * t * t * t
| HCom of t * t * t * t * t
| Com of t * t * t * t * t
| SubIn of t
| SubOut of t
| Dim0
| Dim1
| Cof of (t, t) Cof.t
| ForallCof of t
| CofSplit of (t * t) list
| Prf
| ElIn of t
| ElOut of t
| Box of t * t * t * t * t
| Cap of t * t * t * t * t
| VIn of t * t * t * t
| VProj of t * t * t * t * t
| CodeExt of int * t * [ `Global of t ] * t
| CodePi of t * t
| CodeSg of t * t
| CodeSignature of kan_tele
| CodeNat
| CodeUniv
| CodeV of t * t * t * t
| CodeCircle
| ESub of sub * t
and tp =
| Univ
| El of t
| TpVar of int
| TpDim
| TpCof
| TpPrf of t
| TpCofSplit of (t * tp) list
| Sub of tp * t * t
| Pi of tp * Ident.t * tp
| Sg of tp * Ident.t * tp
| Signature of tele
| Nat
| Circle
| TpESub of sub * tp
and sub =
| SbI
| SbC of sub * sub
| Sb1
| SbE of sub * t
| SbP