Monoid.idr

Maybe Monoids

Proposition

$MaybeCont$ is a monoid in $\mathcal{C}ont$ with regards to $(\ast )$

MaybeMonoidOr : MonoidObject {o = Container} {cat = Cont} CartesianMonoidal
-- Proof in Appendix

This fact is actually the same as stating that $Maybea\in \mathcal{S}et$ is a monoid in $\mathcal{S}et$ with Nothing as the neutral and (<|>) as the multiplication.

Proposition

$MaybeCont$ is a monoid in $\mathcal{C}ont$ with regards to $(\otimes )$

MaybeMonoidTensor : MonoidObject {o = Container, cat = Cont} TensorMonoidal

Proposition

$MaybeCont$ is a monoid in $\mathcal{C}ont$ with regards to $⊳$

  MaybeMonoidCompose : MonoidObject {o = Container} {cat = Cont} SequenceMonoidal
  -- Proof in Appendix

This fact is actually the same as stating that $Maybe\in \mathcal{S}et\to \mathcal{S}et$ is a monad in $\mathcal{S}et$.

• complete proof maybe is a monoid wrt composition

Proposition

$MaybeCont$ is a monoid in $\mathcal{C}on{t}^{\#}$ with regards to $⊳$

nothing : I =#> MaybeCont
nothing = MkCartDepLens (\_ => True) (\_ => MkIso (\_ => ()) (\_ => TT)
                        (\x => unitUniq x)
                        (\x => isTrueUniq x)
                        )
 
joinInhabited : Ex MaybeCont Bool -> Bool
joinInhabited (MkEx False ex2) = False
joinInhabited (MkEx True ex2) = ex2 TT
 
joinInhabitedBw :
  (m : Ex MaybeCont Bool) ->
  IsTrue (joinInhabited m)
  ≅ Σ (IsTrue m.ex1) (IsTrue . m.ex2)
joinInhabitedBw (MkEx False ex2) = IsoVoid
joinInhabitedBw (MkEx True ex2) = MkIso
    (\xx => TT ## xx)
    (\xx => transport (IsTrue . ex2) (sym (isTrueUniq xx.π1)) xx.π2 )
    (\xx => sigEqToEqS $ MkSigEqS (isTrueUniq xx.π1) Refl)
    (\xx => applyRefl ? ?)
 
join : MaybeCont ▷ MaybeCont =#> MaybeCont
join = MkCartDepLens
    joinInhabited
    joinInhabitedBw
 
joinInhabitedEx1 :
   (xx : Ex MaybeCont ()) ->
   joinInhabited (MkEx xx.ex1 (\x => True)) = xx.ex1
joinInhabitedEx1 (MkEx False x2) = Refl
joinInhabitedEx1 (MkEx True x2) = Refl
 
joinInhabitedCartBwd :
    (x : Ex MaybeCont ()) ->
    let
        0 topMorphism : MaybeCont ▷ I  =#> MaybeCont ▷ MaybeCont
        topMorphism = identity MaybeCont ~▷#~ Monoid.nothing
        0 a : MaybeCont ▷ I  =#> MaybeCont
        a = topMorphism |#> Monoid.join
        0 p1, p2 : MaybeCont .res (a.cfwd x) ≅ (MaybeCont ▷ I).res x
        p1 = a.cbwd x
        p2 = transport
                 (\arg => MaybeCont .res arg ≅ (MaybeCont ▷ I).res x)
                 ?hu
                 (Cart.unitR1.cbwd x)
 
    in IsoEq p1 p2
joinInhabitedCartBwd (MkEx False x2)
    = MkIsoEq (\x => ?uhu) (\x => absurd x.π1)
joinInhabitedCartBwd (MkEx True x2)
    = MkIsoEq (\xx => believe_me ())
        (\xx => believe_me ())
 
0
left : let 0 η_id_μ, λ : I ▷ MaybeCont =#> MaybeCont
           0 topMorphism : I ▷ MaybeCont =#> MaybeCont ▷ MaybeCont
           topMorphism = Monoid.nothing ~▷#~ identity MaybeCont
           η_id_μ = topMorphism |#> join
           λ = unitL1
        in η_id_μ === λ
left = cartEqToEq
    $ MkCartDepLensEq
      (\_ => believe_me ())
      (\xx => MkIsoEq
          (\_ => believe_me ())
          (\_ => believe_me ())
      )
 
0
right : let 0 id_η_μ, ρ : MaybeCont ▷ I  =#> MaybeCont
            0 topMorphism : MaybeCont ▷ I  =#> MaybeCont ▷ MaybeCont
            topMorphism = identity MaybeCont ~▷#~ Monoid.nothing
            id_η_μ = topMorphism |#> Monoid.join
            ρ  = Cart.unitR1 {a = MaybeCont}
         in id_η_μ `CartDepLensEqTr` ρ
-- right = MkCartDepLensEqTr
--   joinInhabitedEx1
--   joinInhabitedCartBwd
 
0
botLeft : (MaybeCont ▷ MaybeCont) ▷ MaybeCont =#> MaybeCont
botLeft = Monoid.join ~▷#~ identity MaybeCont |#> Monoid.join
0
topRight : ((MaybeCont ▷ MaybeCont) ▷ MaybeCont) =#> MaybeCont
topRight = Monoidal.alphaL {a = MaybeCont, b = MaybeCont, c = MaybeCont}
    |#> identity MaybeCont ~▷#~ Monoid.join |#> Monoid.join
 
0
assocFwdEq :
    (x : ((MaybeCont ▷ MaybeCont) ▷ MaybeCont).req) ->
    botLeft.cfwd x === topRight.cfwd x
-- assocFwdEq (MkEx (MkEx False ex2) ex3) = Refl
-- assocFwdEq (MkEx (MkEx True ex2) ex3) with (ex2 TT)
--   assocFwdEq (MkEx (MkEx True ex2) ex3) | False = Refl
--   assocFwdEq (MkEx (MkEx True ex2) ex3) | True = Refl
 
assocBwdEq :
    (x : ((MaybeCont ▷ MaybeCont) ▷ MaybeCont).req) ->
    let 0 p1 : MaybeCont .res (botLeft.cfwd x) ≅ ((MaybeCont ▷ MaybeCont) ▷ MaybeCont).res x
        p1 = botLeft.cbwd x
        0 p2 : MaybeCont .res (botLeft.cfwd x) ≅ ((MaybeCont ▷ MaybeCont) ▷ MaybeCont).res x
        p2 = transport (\arg => MaybeCont .res arg ≅ ((MaybeCont ▷ MaybeCont) ▷ MaybeCont).res x) (sym $ assocFwdEq x) (topRight.cbwd x)
    in IsoEq p1 p2
assocBwdEq aa = ?oo
-- assocBwdEq (MkEx (MkEx False ex2) ex3)
--   = MkIsoEq (\x => believe_me x) (\x => absurd x.π1.π1)
-- assocBwdEq (MkEx (MkEx True ex2) ex3) with (ex2 TT) proof pt
--   assocBwdEq (MkEx (MkEx True ex2) ex3) | False
--     = MkIsoEq (\x => believe_me x)
--     (\((TT ## x1) ## x2) => absurd (replace {p = IsTrue} pt x1))
--   assocBwdEq (MkEx (MkEx True ex2) ex3) | True with (ex3 (TT ## (replace {p = IsTrue} (sym pt) TT))) proof qt
--     assocBwdEq (MkEx (MkEx True ex2) ex3) | True | False
--       = MkIsoEq (\x => believe_me x)
--           (\((TT ## x1) ## x2) => believe_me ())
--     assocBwdEq (MkEx (MkEx True ex2) ex3) | True | True
--       = MkIsoEq (\xx => believe_me ())(\xx => believe_me ())
 
0
assoc : Monoid.botLeft `CartDepLensEqTr` Monoid.topRight
assoc = MkCartDepLensEqTr
    assocFwdEq
    assocBwdEq
 
namespace Cart
    public export
    MaybeMonoidCompose : MonoidObject {o = Container} {cat = ContCart} SequenceMonoidal
    MaybeMonoidCompose = MkMonObj
        MaybeCont
        nothing
        join
        left
        (cartEqToEqTr right)
        (believe_me ()) --(cartEqToEqTr assoc)