Frexlet.Monoid.Involutive.Involution

We have an involution functor `.rev : Monoid -> Monoid`
that sends a monoid `a : Monoid` to the monoid with the same
carrier, but with reversed multiplication:
a.rev.Sem Prod [x,y] = a.Sem Prod [y,x]

We can use this functor to characterise involutions as
self-inverse homomorphisms, and this characterisation allows us to
treat involutive monoids quite abstractly.

For a more general set-up, see Bar Jacobs "Involutive Categories
and Monoids, with a GNS-correspondence", QPL'10,
https://arxiv.org/abs/1003.4552

Reexports

Definitions

.rev : MonoidStructure -> MonoidStructure

  Same monoid structure with the order of multiplication reversed:
  
  a.rev.Sem Prod [x,y] = a.Sem Prod [y,x]

Totality: total
Visibility: public export

.rev : Monoid -> Monoid

  Same monoid with the order of multiplication reversed:
  
  a.rev.Sem Prod [x,y] = a.Sem Prod [y,x]

Totality: total
Visibility: public export

.rev : a ~> b -> a .rev ~> b .rev

  Functorial action of .rev on monoid structure homomorphisms

Totality: total
Visibility: public export

.revInvolution : (a : Monoid) -> a .Algebra <~> ((a .Algebra) .rev) .rev

  .rev is an Involution on the category of monoids

Totality: total
Visibility: public export

.revInvolutionAxiom : (a : Monoid) -> (((a .Algebra) .rev ~~> (((a .Algebra) .rev) .rev) .rev) .equivalence) .relation ((cast (a .revInvolution)) .rev) (cast ((a .rev) .revInvolution))

  Jacobs's axiom for the involution on the category of monoids

Totality: total
Visibility: public export

0 .Involution : (a : Monoid) -> a ~> a .rev -> Type

  Characterises the involution axiom abstractly.

Totality: total
Visibility: public export

record Involution : Monoid -> Type

  A characterisation of the structure and properties of an
  involution over a monoid.

Totality: total
Visibility: public export
Constructor: 

MkInvolution : (H : a ~> a .rev) -> a .Involution H -> Involution a

Projections:

.H : Involution a -> a ~> a .rev

.involutive : ({rec:0} : Involution a) -> a .Involution (H {rec:0})

.H : Involution a -> a ~> a .rev

Totality: total
Visibility: public export

H : Involution a -> a ~> a .rev

Totality: total
Visibility: public export

.involutive : ({rec:0} : Involution a) -> a .Involution (H {rec:0})

Totality: total
Visibility: public export

involutive : ({rec:0} : Involution a) -> a .Involution (H {rec:0})

Totality: total
Visibility: public export

InvolutiveMonoidToInvolution : (a : InvolutiveMonoid) -> Involution (cast a)

  Repackage the data and properties in an involutive monoid abstractly

Totality: total
Visibility: public export

InvolutionToInvolutiveMonoid : (a : Monoid) -> Involution (cast a) -> InvolutiveMonoid

Totality: total
Visibility: public export

revFunctorialityCompose : (f : b ~> c) -> (g : a ~> b) -> ((a .rev ~~> c .rev) .equivalence) .relation ((f . g) .rev) (f .rev . g .rev)

  Composition is preserved by (.ev) : (a ~> b) -> a.rev ~> b.rev

Totality: total
Visibility: public export

revFunctorialityId : ((a .rev ~~> a .rev) .equivalence) .relation ((id a) .rev) (id (a .rev))

  Identities are preserved by (.ev) : (a ~> b) -> a.rev ~> b.rev

Totality: total
Visibility: public export

data Env : Setoid -> (a : Monoid) -> Involution a -> Type

  a setoid homomorphism `H : (Bool, s) ~> U a` satisfying:
           H
    U a <---- (Bool, s)
     | inv       | bimap not id
     v           v
    U a <---- (Bool, s)
           H

Totality: total
Visibility: public export
Constructor: 

MkEnv : (H : Pair (cast Bool) s ~> cast a) -> ((Pair (cast Bool) s ~~> cast a) .equivalence) .relation ((inv .H) .H . H) (H . bimap (mate not) (id s)) -> Env s a inv

.H : Env s a inv -> Pair (cast Bool) s ~> cast a

Totality: total
Visibility: public export

.compatibility : (env : Env s a inv) -> ((Pair (cast Bool) s ~~> cast a) .equivalence) .relation ((inv .H) .H . env .H) (env .H . bimap (mate not) (id s))

Totality: total
Visibility: public export

cast : s ~> cast c -> Env s (cast c) (InvolutiveMonoidToInvolution c)

Totality: total
Visibility: public export

cast : Env s c inv -> s ~> cast c

Totality: total
Visibility: public export