Frex.Axiom

Definitions and functions dealing with single-sorted finitary signatures

Reexports

Definitions

(=-=) : Term sig a -> Term sig a -> (Term sig a, Term sig a)

  Smart constructor for making equations look nicer

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 1

MkEquation : (n : Nat) -> (Term sig (Fin n), Term sig (Fin n)) -> Equation sig

  Smart constructor for equations over finitely many variables

Totality: total
Visibility: public export

additiveNotation : OpWithArity sig 0 -> OpWithArity sig 2 -> Additive1 (Term sig (Fin k))

  Auxiliary: extract additive notation for two given operations

Totality: total
Visibility: public export

EqSpec : Signature -> Vect n Nat -> Type

  Metaprogramming: the type of an equation parameterised by
  operations of the given arity vecotr

Totality: total
Visibility: public export

lftNeutrality : EqSpec sig [0, 2]

  O + x = x

Totality: total
Visibility: public export

rgtNeutrality : EqSpec sig [0, 2]

  x + O = x

Totality: total
Visibility: public export

associativity : EqSpec sig [2]

  x + (y + z) = (x + y) + z

Totality: total
Visibility: public export

commutativity : EqSpec sig [2]

  x + y = y + x

Totality: total
Visibility: public export

rgtInverse : EqSpec sig [0, 1, 2]

  x + - x = 0

Totality: total
Visibility: public export

lftInverse : EqSpec sig [0, 1, 2]

  - x + x = 0

Totality: total
Visibility: public export

lftAnnihilation : EqSpec sig [0, 2]

  0 * x = 0

Totality: total
Visibility: public export

rgtAnnihilation : EqSpec sig [0, 2]

  x * 0 = 0

Totality: total
Visibility: public export

lftDistributivity : EqSpec sig [2, 2]

  x * (y + z) = x * y + x * z

Totality: total
Visibility: public export

rgtDistributivity : EqSpec sig [2, 2]

  (x + y) * z = x * z + y * z

Totality: total
Visibility: public export

involutivity : EqSpec sig [1]

Totality: total
Visibility: public export

antidistributivity : EqSpec sig [1, 2]

Totality: total
Visibility: public export