Isomorphisms.idr

• finish proof that maybe + and maybe ▷ are isomorphic

Lemma

$Mayb{e}_{1+}$ and $Mayb{e}_{▷}$ are isomorphic.

AnySeqIso : {a : Container} -> ContIso (MaybeCont ▷ a) (One + a)
AnySeqIso = CalcWith {dom = Container} {leq = ContIso} @{ContIsoPre} $
    |~ (MaybeCont ▷ a)
    <~ ((One + I) ▷ a)
    ...(congSeqRight maybeContDef)
    <~ ((One ▷ a) + (I ▷ a))
    ...(plusSeqDistrib)
    <~ ((One ▷ a) + a)
    ...(congCoprodLeft {c = One ▷ a, a = I ▷ a, b = a}
            leftUnitor')
    <~ (One + a)
    ...(congCoprodRight leftOneSeq)

• complete proof maybe all is functor