Untrusted helpers for building equality transport terms.
These helpers only construct core terms. Callers still need to pass the result
through Theoria.Kernel before trusting it as a proof.
Summary
Functions
Builds congruence for a unary function.
Builds congruence for applying equal functions to the same argument.
Builds nondependent equality transport by using a constant motive.
Builds an equality-recursion transport term.
Builds a substitution proof from base : motive left and proof : left = right.
Builds a symmetry proof from proof : x = y.
Builds a transitivity proof from left = middle and middle = right.
Functions
@spec congr( Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t() ) :: Theoria.Term.EqRec.t()
Builds congruence for a unary function.
@spec congr_fun( Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t() ) :: Theoria.Term.EqRec.t()
Builds congruence for applying equal functions to the same argument.
@spec ndrec(Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t()) :: Theoria.Term.EqRec.t()
Builds nondependent equality transport by using a constant motive.
@spec rewrite(Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t()) :: Theoria.Term.EqRec.t()
Builds an equality-recursion transport term.
@spec subst(Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t()) :: Theoria.Term.EqRec.t()
Builds a substitution proof from base : motive left and proof : left = right.
@spec symm(Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t()) :: Theoria.Term.EqRec.t()
Builds a symmetry proof from proof : x = y.
@spec trans( Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t(), Theoria.Term.t() ) :: Theoria.Term.EqRec.t()
Builds a transitivity proof from left = middle and middle = right.