Properties.idr

The extension of containers is a crucial feature making them suitable for generic data programming and has a few very nice propertie we explore here.

Proposition

The extension of containers forms a bifuctor $[[\_]]\_:\mathcal{C}ont\times \mathcal{S}et\to \mathcal{S}et$

exBimap : a =%> a' -> (b -> b') -> Ex a b -> Ex a' b'
exBimap f g x = MkEx (y <- f.fwd x.ex1) | g (x.ex2 (f.bwd x.ex1 y))

ExBifunctor : Bifunctor Cont Set Set
ExBifunctor = MkFunctor
    (uncurry Ex)
    (\x, y, m => exBimap m.π1 m.π2)

Or equivalently, a functor $[[\_]]:\mathcal{C}ont\to [Set,Set]$.

ExFunctor : Cont ->> (FunctorCat Set Set)
ExFunctor = uncurryFunctor ExBifunctor

From this definition we recover functors in $\mathcal{S}et$ indexed by a container

Proposition

The extension functor $[[\_]]:\mathcal{C}ont\to [\mathcal{S}et,\mathcal{S}et]$ is full and faithful.

ExIsFullAndFaithFull : FullyFaithful ExFunctor
ExIsFullAndFaithFull = MkFullFaithful
    (\nt => lensFromExMap nt.component)
    (\x => depLensEqToEq $ MkDepLensEq (\_ => Refl) (\_, _ => Refl))
    (\x, y, (MkNT xc xs) => ntEqToEq $ MkNTEq $ \vx =>
        funExt $ \(MkEx vy vz) => exEqToEq $
        let gg = app (xs vx vx id) (MkEx vy vz)
            qq = app (xs (? .response vy) vx vz) (MkEx vy (\x => x))
            pp = sym $ exP1 gg
            ss = exP1 qq
        in MkExEq
        (trans ss pp)
        (\vy =>
          let vy' = rewrite__impl y.response (sym ss) vy
              pq = exP2 gg vy'
              sq = exP2 qq vy
          in trans sq (cong2Dep (.ex2) Refl (transpUIP ? ?))
        )
    )

Proposition

Extension preserves coproducts

public export
exCoprod : Ex (a + b) c -> Ex a c + Ex b c
exCoprod (MkEx (<+ x) ex2) = <+ MkEx x ex2
exCoprod (MkEx (+> x) ex2) = +> MkEx x ex2

Proposition

Extension preserves composition

public export
exCompose : Ex (a ▷ b) c -> Ex a (Ex b c)
exCompose x = MkEx x.ex1.ex1 (\vx => MkEx (x.ex1.ex2 vx) (x.ex2 . (vx ##)))

Proposition

Extension preserves cartesian product

public export
exProduct : Ex (a * b) c -> Ex a c * Ex b c
exProduct xx = MkEx xx.ex1.π1 (xx.ex2 . (<+)) && MkEx xx.ex1.π2 (xx.ex2 . (+>))

• [?] Can we say that if we have a monad in the extension of the container then we have a monoid in Cont wrt to $⊳$?