Frexlet.Monoid.Involutive.Theory

The syntax and axioms for involutive monoids

Reexports

Definitions

data Operation : Nat -> Type

Totality: total
Visibility: public export
Constructors:

Mono : Operation n -> Operation n

Involution : Operation 1

Signature : Signature

Totality: total
Visibility: public export

castOp : Signature ~> Signature

Totality: total
Visibility: public export

data Axiom : Type

Totality: total
Visibility: public export
Constructors:

Mon : Axiom -> Axiom

Involutivity : Axiom

Antidistributivity : Axiom

InvolutiveMonoidTheory : Presentation

Totality: total
Visibility: public export

InvolutiveMonoidStructure : Type

Totality: total
Visibility: public export

InvolutiveMonoid : Type

Totality: total
Visibility: public export

MkInvolutiveMonoidStructure : (monoid : MonoidStructure) -> cast monoid ~> cast monoid -> InvolutiveMonoidStructure

  Smart constructor for involutive monoid structures

Totality: total
Visibility: public export

MkInvolutiveMonoid : (monoid : Monoid) -> (involution : cast monoid ~> cast monoid) -> (let 0 invMonoid = MkInvolutiveMonoidStructure (monoid .Algebra) involution in ValidatesEquation (involutivity Involution) invMonoid -> ValidatesEquation (antidistributivity Involution (Mono Product)) invMonoid -> InvolutiveMonoid)

  Smart constructor for involutive monoids

Totality: total
Visibility: public export

cast : a ~> b -> cast a ~> cast b

Totality: total
Visibility: public export

Mon : Op (MonoidTheory .signature) -> Op (InvolutiveMonoidTheory .signature)

Totality: total
Visibility: public export

Involute : Op (InvolutiveMonoidTheory .signature)

Totality: total
Visibility: public export