Frexlet.Monoid.Involutive.Frex

Cosntructing the involutive monoid frex.

This implementation uses the fact that if `a` is an involutive
monoid, then `Frex a s` can be represented by `Frex a.monoid (Bool, s)`.

Definitions

0 AuxExtensionType : InvolutiveMonoid -> Setoid -> Type

Totality: total
Visibility: public export

0 AuxFrexType : InvolutiveMonoid -> Setoid -> Type

  Type of auxiliary monoid frex used to construct the involutive monoid frex

Totality: total
Visibility: public export

AuxFrex : (a : InvolutiveMonoid) -> (s : Setoid) -> AuxFrexType a s

  Auxiliary monoid frex used to construct the involutive monoid frex

Totality: total
Visibility: public export

AuxFrexExtension : (a : InvolutiveMonoid) -> (s : Setoid) -> AuxExtensionType a s

Totality: total
Visibility: public export

AuxFrexMonoid : InvolutiveMonoid -> Setoid -> Monoid

  The monoid part of the involutive monoid frex

Totality: total
Visibility: public export

FrexInvolutionExtension : (a : InvolutiveMonoid) -> (s : Setoid) -> AuxExtensionType a s

  We use the following extension to define the involution on the frex
  
  a                                      (Bool, s)
  | a.inv                                    | bimap not id
  v                                          v
  a.rev --> (AuxFrexMonoid a s).rev <--- (Bool, s)
      sta.rev                        dyn

Totality: total
Visibility: public export

FrexInvolutionExtensionMorphism : (a : InvolutiveMonoid) -> (s : Setoid) -> AuxFrexExtension a s ~> FrexInvolutionExtension a s

  The involution on the frex is given by the universal property:
  
  a ------> FrexInvMonoid a s  <------- (Bool, s)
  | a.inv   =      | FrexInvolution a s     | bimap not id
  v  (in Monoids)  v        =   (in Set)    v
  a.rev --> (FrexInvMonoid a s).rev <--- (Bool, s)
      sta.rev                        dyn

Totality: total
Visibility: public export

FrexInvolution : (a : InvolutiveMonoid) -> (s : Setoid) -> AuxFrexMonoid a s ~> (AuxFrexMonoid a s) .rev

  The involution homomorphism for the frex

Totality: total
Visibility: public export

FrexInvolutionIsInvolution : (a : InvolutiveMonoid) -> (s : Setoid) -> (AuxFrexMonoid a s) .Involution (FrexInvolution a s)

  The involution axiom boils down to this equation:
  
   FrexInvMonoid a s  ---------------------
          |                               |
          | FrexInvolution a s            | cast (cast a).revInvolution
          |                               |
          V                               V
  (FrexInvMonoid a s).rev -------> (FrexInvMonoid a s).rev.rev
                  (FrexInvolution a s).rev

Totality: total
Visibility: public export

FrexInvolutionInvolution : (a : InvolutiveMonoid) -> (s : Setoid) -> Involution (AuxFrexMonoid a s)

Totality: total
Visibility: public export

FrexInvolutiveMonoid : InvolutiveMonoid -> Setoid -> InvolutiveMonoid

Totality: total
Visibility: public export

data InvolutiveExtension : InvolutiveMonoid -> Setoid -> Type

  The reason the involutive frex works is that we can decompose an
  InvolutiveExtension into a monoid extension with the following
  extra data

Totality: total
Visibility: public export
Constructor: 

MkInvolutiveExtension : (MonoidExtension : AuxExtensionType a s) -> (ModelInvolution : Involution (MonoidExtension .Model)) -> ((i : U a) -> ((MonoidExtension .Model) .equivalence) .relation (((MonoidExtension .Embed) .H) .H (a .Sem Involute [i])) (((ModelInvolution .H) .H) .H (((MonoidExtension .Embed) .H) .H i))) -> ((Pair (cast Bool) s ~~> cast (MonoidExtension .Model)) .equivalence) .relation ((ModelInvolution .H) .H . MonoidExtension .Var) (MonoidExtension .Var . bimap (mate not) (id s)) -> InvolutiveExtension a s

.MonoidExtension : InvolutiveExtension a s -> AuxExtensionType a s

Totality: total
Visibility: public export

.ModelInvolution : (ext : InvolutiveExtension a s) -> Involution ((ext .MonoidExtension) .Model)

Totality: total
Visibility: public export

.PreserveInvolute : (ext : InvolutiveExtension a s) -> (i : U a) -> (((ext .MonoidExtension) .Model) .equivalence) .relation ((((ext .MonoidExtension) .Embed) .H) .H (a .Sem Involute [i])) ((((ext .ModelInvolution) .H) .H) .H ((((ext .MonoidExtension) .Embed) .H) .H i))

Totality: total
Visibility: public export

.VarCompatibility : (ext : InvolutiveExtension a s) -> ((Pair (cast Bool) s ~~> cast ((ext .MonoidExtension) .Model)) .equivalence) .relation (((ext .ModelInvolution) .H) .H . (ext .MonoidExtension) .Var) ((ext .MonoidExtension) .Var . bimap (mate not) (id s))

Totality: total
Visibility: public export

InvolutiveExtensionToExtension : InvolutiveExtension a s -> Extension a s

Totality: total
Visibility: public export

ExtensionToInvolutiveExtension : Extension a s -> InvolutiveExtension a s

Totality: total
Visibility: public export

InvMonoidExtension : (a : InvolutiveMonoid) -> (s : Setoid) -> Extension a s

Totality: total
Visibility: public export

.Env : (ext : InvolutiveExtension a s) -> Env s ((ext .MonoidExtension) .Model) (ext .ModelInvolution)

Totality: total
Visibility: public export

ExtenderHomomorphism : (a : InvolutiveMonoid) -> (s : Setoid) -> ExtenderHomomorphism (InvMonoidExtension a s)

Totality: total
Visibility: public export

InvExtender : (a : InvolutiveMonoid) -> (s : Setoid) -> Extender (InvMonoidExtension a s)

Totality: total
Visibility: public export

Uniqueness : (a : InvolutiveMonoid) -> (s : Setoid) -> Uniqueness (InvMonoidExtension a s)

Totality: total
Visibility: public export

Frex : (a : InvolutiveMonoid) -> Frex a s

Totality: total
Visibility: public export