Module Cubical.CofThy

The CofThy module implements decision procedures for sequents relative to a theory over the interval, stated in the language of cofibrations.

type cof = (Dim.dim[ `L of int | `G of Basis.Symbol.t ]) Cof.cof
module Alg : sig ... end

Algebraic theories over the interval.

module Disj : sig ... end

Disjunctive theories over the interval.