Module Core.TermBuilder

A language for building terms without doing De Bruijn arithmetic. This module contains constructors * not only for the primitives of cubical type theory, but also for the more complex derived forms -- * for instance, the algorithm of coercion and composition in various type connectives.

include Basis.Monad.S
type 'a m
val ret : 'a -> 'a m
val bind : 'a m -> ('a -> 'b m) -> 'b m
module S := CodeUnit.Syntax
type t := S.t
type tp := S.tp
type tele := S.tele
type 'a b = t m -> 'a m
val scope : 'a b -> 'a m
val run : tplen:int -> conlen:int -> 'a m -> 'a
val lvl : int -> t m
val tplvl : int -> tp m
val lam : ?ident:Ident.t -> t b -> t m
val ap : t m -> t m list -> t m
val coe : t m -> t m -> t m -> t m -> t m
val hcom : t m -> t m -> t m -> t m -> t m -> t m
val com : t m -> t m -> t m -> t m -> t m -> t m
val let_ : ?ident:Ident.t -> t m -> t b -> t m
val pair : t m -> t m -> t m
val fst : t m -> t m
val snd : t m -> t m
val lams : Ident.t list -> (t m list -> t m) -> t m
val struct_ : S.fields m -> t m
val proj : t m -> Ident.t -> int -> t m
val zero : t m
val suc : t m -> t m
val base : t m
val loop : t m -> t m
val prf : t m
val cap : t m -> t m -> t m -> t m -> t m -> t m
val box : t m -> t m -> t m -> t m -> t m -> t m
val cof_split : (t m * t m) list -> t m
val tp_cof_split : (t m * tp m) list -> tp m
val tm_abort : t m
val sub_out : t m -> t m
val sub_in : t m -> t m
val el_in : t m -> t m
val el_out : t m -> t m
val univ : tp m
val nat : tp m
val code_nat : t m
val nat_elim : t m -> t m -> t m -> t m -> t m
val circle : tp m
val code_circle : t m
val circle_elim : t m -> t m -> t m -> t m -> t m
val pi : ?ident:Ident.t -> tp m -> tp b -> tp m
val sg : ?ident:Ident.t -> tp m -> tp b -> tp m
val signature : tele m -> tp m
val sub : tp m -> t m -> t b -> tp m
val tp_prf : t m -> tp m
val tp_dim : tp m
val tp_cof : tp m
val el : t m -> tp m
val pis : ?idents:Ident.t list -> t m list -> (t m list -> tp m) -> tp m
val cube : int -> (t m list -> tp m) -> tp m
val code_pi : t m -> t m -> t m
val code_sg : t m -> t m -> t m
val code_path : t m -> t m -> t m

A specialization of code_path that performs a cof_split.

val code_path' : t m -> t m -> t m -> t m

A specialization of code_path that performs a cof_split.

val code_v : t m -> t m -> t m -> t m -> t m
val code_ext : int -> t m -> t m -> t m -> t m
val vproj : t m -> t m -> t m -> t m -> t m -> t m
val code_pis : t m list -> (t m list -> t m) -> t m
val dim0 : t m
val dim1 : t m
val eq : t m -> t m -> t m
val join : t m list -> t m
val meet : t m list -> t m
val top : t m
val bot : t m
val boundary : t m -> t m
val forall : t b -> t m
module Equiv : sig ... end
module Kan : sig ... end
module Test : sig ... end