Module Globular.Theory

module Theory: sig .. end

A globular theory, the typical example being weak omega-categories.

module Var: sig .. end

module Cons: sig .. end

type term =

`\|`	`Var of Var.t`
`\|`	`Cons of Cons.t * context`	`(*`	A context contains terms with their source and target.	`*)`

type context = (term * (term * term)) list