Frexlet.Monoid.Frex.Properties

Properties of the monoid frexlet and its operations

Definitions

multUnitNeutral : (a : Monoid) -> (s : Setoid) -> (is : FrexCarrier a s) -> ((FrexSetoid a s) .equivalence) .relation (the (U a) I1 *. is) is

Totality: total
Visibility: public export

multAssociative : (a : Monoid) -> (s : Setoid) -> (i0 : U a) -> (i1 : U a) -> (is : FrexCarrier a s) -> ((FrexSetoid a s) .equivalence) .relation (i0 *. (i1 *. is)) ((i0 .*. i1) *. is)

Totality: total
Visibility: public export

multMultAssociative : (a : Monoid) -> (s : Setoid) -> (i0 : U a) -> (is : FrexCarrier a s) -> (js : FrexCarrier a s) -> ((FrexSetoid a s) .equivalence) .relation (i0 *. (is .*. js)) ((i0 *. is) .*. js)

Totality: total
Visibility: public export

appendUnitLftNeutral : (a : Monoid) -> (s : Setoid) -> (is : FrexCarrier a s) -> ((FrexSetoid a s) .equivalence) .relation (I1 .*. is) is

Totality: total
Visibility: public export

appendUnitRgtNeutral : (a : Monoid) -> (s : Setoid) -> (is : FrexCarrier a s) -> ((FrexSetoid a s) .equivalence) .relation (is .*. I1) is

Totality: total
Visibility: public export

appendAssociative : (a : Monoid) -> (s : Setoid) -> (is : FrexCarrier a s) -> (js : FrexCarrier a s) -> (ks : FrexCarrier a s) -> ((FrexSetoid a s) .equivalence) .relation (is .*. (js .*. ks)) ((is .*. js) .*. ks)

Totality: total
Visibility: public export

FrexValidatesAxioms : (a : Monoid) -> (s : Setoid) -> Validates MonoidTheory (FrexStructure a s)

Totality: total
Visibility: public export

FrexMonoid : Monoid -> Setoid -> Monoid

Totality: total
Visibility: public export