Module Cubical

The Cubical library implements the syntax and semantics of the Cartesian interval as well as a logic of cofibrations as described by ABCFHL.

Syntax

module Dim : module type of Dim

The abstract syntax of the Cartesian interval.

module Cof : module type of Cof

The abstract syntax of the restricted predicate logic of cofibrations.

Semantics

module CofThy : sig ... end

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