Frexlet.Monoid.Involutive.Notation

Notation for working with involutive monoids (mostly boilerplate)

Definitions

interface Involutive : Type -> Type

Parameters: a
Constructor: 

MkInvolutive

Methods:

.inv : a -> a

Implementations:

(Involutive a, {_:8320}) -> Involutive a

({_:8334}, Involutive a) -> Involutive a

.inv : Involutive a => a -> a

Totality: total
Visibility: public export

.Involutive : (monoid : InvolutiveMonoid) -> Involutive (U monoid)

Totality: total
Visibility: public export

fstInvulotive : (Involutive a, {_:8320}) -> Involutive a

Totality: total
Visibility: public export

sndInvolutive : ({_:8334}, Involutive a) -> Involutive a

Totality: total
Visibility: public export

InvMult1 : Type -> Type

Totality: total
Visibility: public export

InvMult2 : Type -> Type

Totality: total
Visibility: public export

InvMult3 : Type -> Type

Totality: total
Visibility: public export

.Notation1 : (monoid : InvolutiveMonoid) -> InvMult1 (U monoid)

Totality: total
Visibility: public export

.Notation2 : (monoid : InvolutiveMonoid) -> InvMult2 (U monoid)

Totality: total
Visibility: public export

.Notation3 : (monoid : InvolutiveMonoid) -> InvMult3 (U monoid)

Totality: total
Visibility: public export

notationSyntax : Involutive (Term (InvolutiveMonoidTheory .signature) x)

Totality: total
Visibility: public export

notation1 : InvMult1 (Term (InvolutiveMonoidTheory .signature) (Either a (Fin n)))

Totality: total
Visibility: public export

multiplicative1 : (0 n : Nat) -> InvMult1 (Term (InvolutiveMonoidTheory .signature) (Fin n))

Totality: total
Visibility: public export