0 | module APLAS
  1 |
  2 | import Data.Container
  3 | import Data.Container.Category
  4 | import Data.Container.Morphism
  5 | import Data.Container.Maybe
  6 | import Data.Container.Monad
  7 |
  8 | import Data.Category
  9 | import Data.Category.Functor
 10 | import Data.Category.NaturalTransformation
 11 | import Data.Category.Monad
 12 |
 13 | import Data.Iso
 14 |
 15 | import Syntax.PreorderReasoning
 16 |
 17 | %hide Prelude.Ops.infixl.(*>)
 18 | %default total
 19 |
 20 | namespace Containers
 21 |   namespace Definition1
 22 |
 23 |     Container : Type
 24 |     Container = Σ Type (\req => req -> Type)
 25 |
 26 |   namespace Definition2
 27 |
 28 |     infixr 1 =>>
 29 |     export
 30 |     record (=>>) (c1, c2 : Container) where
 31 |       constructor (<|)
 32 |       fwMap : c1.req -> c2.req
 33 |       bwMap : {x : c1.req} -> c2.res (fwMap x) -> c1.res x
 34 |
 35 |   namespace Definition3
 36 |
 37 |     (⨾) : a =>> b -> b =>> c -> a =>> c
 38 |     (⨾) (q1 <| r1) (q2 <| r2) = q2 . q1 <| r1 . r2
 39 |
 40 |     -- In the rest of the program we are going to use =%> for container
 41 |     -- morphisms, it has an explicit first argument in the bwMap
 42 |
 43 | namespace Definition4
 44 |
 45 |   proposition4 : Category Container
 46 |   proposition4 = Cont
 47 |
 48 | namespace Definition5
 49 |
 50 |   maybeMap : Container -> Container
 51 |   maybeMap (c !> c') = (x : Maybe c) !> All c' x
 52 |
 53 | namespace Proposition6
 54 |
 55 |   maybeMapId : forall t. (v : Maybe t) -> maybeMap (\x => x) v === v
 56 |   maybeMapId Nothing = Refl
 57 |   maybeMapId (Just x) = Refl
 58 |
 59 |   maybeMapComp : forall a, b, c. (v : Maybe a) -> {f : b -> c} -> {g : a -> b} ->
 60 |                  maybeMap (f . g) v === maybeMap f (maybeMap g v)
 61 |   maybeMapComp Nothing = Refl
 62 |   maybeMapComp (Just x) = Refl
 63 |
 64 |   0
 65 |   MaybeAllIdrisPresId : forall a. MaybeAllIdrisFunctor (identity {a}) `DepLensEq` identity {a = MaybeAllIdris a}
 66 |   MaybeAllIdrisPresId = MkDepLensEq maybeMapId maybeMapId'
 67 |     where
 68 |
 69 |       maybeMapId' : (v : Maybe a.req) -> (y : All a.res (maybeMap (\x => x) v)) ->
 70 |                     bwdMaybeAllF {x = a, y = a, mor = identity {a}} v y ===
 71 |                       replace {p = All a.res} (maybeMapId v) y
 72 |       maybeMapId' (Just x) (Aye y) = Refl
 73 |       maybeMapId' (Nothing) Nah = Refl
 74 |
 75 |   public export
 76 |   MaybeAllIdrisPresComp : forall a, b, c. (f : a =%> b) -> (g : b =%> c) ->
 77 |                           MaybeAllIdrisFunctor (f ⨾ g) `DepLensEq`
 78 |                           MaybeAllIdrisFunctor f ⨾ MaybeAllIdrisFunctor g
 79 |   MaybeAllIdrisPresComp f g = MkDepLensEq
 80 |     (\v => maybeMapComp v)
 81 |     (\case Nothing => \Nah => Refl
 82 |            (Just x) => \(Aye y) => Refl)
 83 |
 84 |   public export
 85 |   MaybeIsFunctor : Functor Cont Cont
 86 |   MaybeIsFunctor = MkFunctor
 87 |     MaybeAllIdris
 88 |     (\_, _ => MaybeAllIdrisFunctor)
 89 |     (\_ => depLensEqToEq MaybeAllIdrisPresId)
 90 |     (\_, _, _, f, g => depLensEqToEq (MaybeAllIdrisPresComp f g))
 91 |
 92 | namespace Proposition7
 93 |
 94 |   unit : idF Cont ==>> MaybeIsFunctor
 95 |   unit = MkNT
 96 |     maybeAllPure
 97 |     (\a, b, m => depLensEqToEq $ MkDepLensEq (\_ => Refl) (\v => \(Aye w) => Refl))
 98 |
 99 |   mult : MaybeIsFunctor *> MaybeIsFunctor ==>> MaybeIsFunctor
100 |   mult = MkNT
101 |     maybeAllJoin
102 |     (\a, b, m => depLensEqToEq $ MkDepLensEq
103 |         (\case (Just (Just x)) => Refl ; Just Nothing => Refl ; Nothing => Refl )
104 |         (\case (Just (Just x)) => \(Aye x) => Refl
105 |                          ; Nothing => (\x => Refl)
106 |                          ; Just Nothing => (\x => Refl)))
107 |
108 |   %unbound_implicits off
109 |   joinMapJoin : forall a. (v : Maybe (Maybe (Maybe a))) -> maybeJoin (maybeMap maybeJoin v) = maybeJoin (maybeJoin v)
110 |   joinMapJoin Nothing = Refl
111 |   joinMapJoin (Just Nothing) = Refl
112 |   joinMapJoin (Just (Just Nothing)) = Refl
113 |   joinMapJoin (Just (Just (Just x))) = Refl
114 |
115 |   bwdJoinMapJoin : {0 x : Container} -> (v : Maybe (Maybe (Maybe x.req))) ->
116 |                    (y : All x.res (maybeJoin (maybeMap maybeJoin v))) ->
117 |                    bwdMaybeAllF {mor = maybeAllJoin x} v (maybeAllJoinBwd (maybeMap maybeJoin v) y) ===
118 |                      maybeAllJoinBwd v (maybeAllJoinBwd (maybeJoin v) (replace {p = All x.res} (joinMapJoin v) y))
119 |   bwdJoinMapJoin Nothing Nah = Refl
120 |   bwdJoinMapJoin (Just Nothing) Nah = Refl
121 |   bwdJoinMapJoin (Just (Just Nothing)) Nah = Refl
122 |   bwdJoinMapJoin (Just (Just (Just z))) (Aye y) = Refl
123 |
124 |   monadSquare : (x : Container) -> let
125 |                 left, top : MaybeAllIdris (MaybeAllIdris (MaybeAllIdris x)) =%> MaybeAllIdris (MaybeAllIdris x)
126 |                 top = MaybeAllIdrisFunctor (maybeAllJoin x)
127 |                 left = maybeAllJoin (MaybeAllIdris x)
128 |                 in top ⨾ maybeAllJoin x `DepLensEq` left ⨾ maybeAllJoin x
129 |   monadSquare x = MkDepLensEq
130 |       joinMapJoin
131 |       bwdJoinMapJoin
132 |
133 |   maybeJoinJust : forall a. (v : Maybe a) -> maybeJoin (Just v) = v
134 |   maybeJoinJust Nothing = Refl
135 |   maybeJoinJust (Just x) = Refl
136 |
137 |   bwdMaybeJoinJust : forall x. (v : Maybe (x .req)) -> (y : All x.res (maybeJoin (Just v))) ->
138 |                                Maybe.obtain (maybeAllJoinBwd (Just v) y)
139 |                                = replace {p = All x.res} (maybeJoinJust v) y
140 |   bwdMaybeJoinJust Nothing Nah = Refl
141 |   bwdMaybeJoinJust (Just z) (Aye y) = Refl
142 |
143 |   monadIdLeft : (x : Container) -> maybeAllPure (MaybeAllIdris x) ⨾ maybeAllJoin x
144 |                 `DepLensEq` identity
145 |   monadIdLeft x = MkDepLensEq maybeJoinJust bwdMaybeJoinJust
146 |
147 |   maybeJoinMapJust : forall a. (v : Maybe a) -> maybeJoin (maybeMap Just v) = v
148 |   maybeJoinMapJust Nothing = Refl
149 |   maybeJoinMapJust (Just x) = Refl
150 |
151 |   bwdMaybeJoinMapJust : forall x. (v : Maybe (x .req)) ->
152 |                         (y : All x.res (maybeJoin (maybeMap Just v))) ->
153 |                         bwdMaybeAllF {mor = maybeAllPure x} v (maybeAllJoinBwd (maybeMap Just v) y) ===
154 |                           replace {p = All x.res} (maybeJoinMapJust v) y
155 |   bwdMaybeJoinMapJust Nothing Nah = Refl
156 |   bwdMaybeJoinMapJust (Just z) (Aye y) = Refl
157 |
158 |   monadIdRight : (x : Container) -> MaybeAllIdrisFunctor (maybeAllPure x) ⨾ maybeAllJoin x `DepLensEq` identity {a = MaybeAllIdris x}
159 |   monadIdRight x = MkDepLensEq
160 |       maybeJoinMapJust bwdMaybeJoinMapJust
161 |
162 |   %unbound_implicits on
163 |
164 |   public export
165 |   maybeMonadInCont : Monad Cont
166 |   maybeMonadInCont = MkMonad
167 |       MaybeIsFunctor
168 |       unit
169 |       mult
170 |       (\x => depLensEqToEq $ monadSquare x)
171 |       (\x => depLensEqToEq $ monadIdLeft x)
172 |       (\x => depLensEqToEq $ monadIdRight x)
173 |
174 | namespace Definition8
175 |
176 |   coproduct : Container -> Container -> Container
177 |   coproduct c1 c2 = (x : c1.req + c2.req) !> choice c1.res c2.res x
178 |
179 | namespace Proposition9
180 |
181 |   -- Maybe and 1 + are isomorphic in the category of types
182 |   maybeCoprod : Maybe x -> () + x
183 |   maybeCoprod Nothing = <+ ()
184 |   maybeCoprod (Just p2) = +> p2
185 |
186 |   coprodMaybe : () + x -> Maybe x
187 |   coprodMaybe (<+ y) = Nothing
188 |   coprodMaybe (+> y) = Just y
189 |
190 |   coprodMaybeCoprod : (v : () + x) -> maybeCoprod (coprodMaybe v) === v
191 |   coprodMaybeCoprod (<+ ()) = Refl
192 |   coprodMaybeCoprod (+> y) = Refl
193 |
194 |   maybeCoprodMaybe : (v : Maybe x) -> coprodMaybe (maybeCoprod v) === v
195 |   maybeCoprodMaybe Nothing = Refl
196 |   maybeCoprodMaybe (Just y) = Refl
197 |
198 |   maybeCoprodIso : {0 x : Type} -> Iso (Prelude.Maybe x) (() + x)
199 |   maybeCoprodIso = MkIso maybeCoprod coprodMaybe coprodMaybeCoprod maybeCoprodMaybe
200 |
201 |   -- Maybe and 1 + are isomorphic in the category of containers
202 |   bwd_maybeToCoprod : (x : Maybe v.req) ->
203 |                       choice (\value => Unit) v.res (maybeCoprod x) -> All v.res x
204 |   bwd_maybeToCoprod Nothing y = Nah
205 |   bwd_maybeToCoprod (Just x) y = Aye y
206 |
207 |   bwd_coprodMaybe : (x : () + v.req) -> All v.res (coprodMaybe x) -> choice (\value => Unit) v.res x
208 |   bwd_coprodMaybe (<+ x) y = ()
209 |   bwd_coprodMaybe (+> x) y = obtain y
210 |
211 |   export
212 |   maybeToCoprod : (v : Container) -> MaybeAllIdris v =%> CUnit + v
213 |   maybeToCoprod v = maybeCoprod <| bwd_maybeToCoprod
214 |
215 |   export
216 |   coprodToMaybe : (v : Container) -> CUnit + v =%> MaybeAllIdris v
217 |   coprodToMaybe v = coprodMaybe <| bwd_coprodMaybe
218 |
219 |   %unbound_implicits off
220 |   coprodAndBack : (v : Container) -> coprodToMaybe v ⨾ maybeToCoprod v `DepLensEq` identity {a = CUnit + v}
221 |   coprodAndBack v = MkDepLensEq coprodMaybeCoprod
222 |       (\case (<+ x) => \() => Refl
223 |              (+> x) => \_ => Refl)
224 |
225 |   maybeAndBack : (v : Container) -> maybeToCoprod v ⨾ coprodToMaybe v `DepLensEq` identity {a = MaybeAllIdris v}
226 |   maybeAndBack v = MkDepLensEq maybeCoprodMaybe
227 |       (\case Nothing => \Nah => Refl
228 |              (Just x) => \(Aye y) => Refl)
229 |
230 |   coprodMaybeIsoCont : (x : Container) -> ContIso (MaybeAllIdris x) (CUnit + x)
231 |   coprodMaybeIsoCont x = MkGenIso (maybeToCoprod x) (coprodToMaybe x) (maybeAndBack x) (coprodAndBack x)
232 |
233 | %unbound_implicits on
234 | namespace Definition10
235 |
236 |   dia : a + a =%> a
237 |   dia = dia <| \case (+> r) => id ; (<+ l) => id
238 |
239 | namespace Definition11
240 |
241 |   maybeU : MaybeAllIdris CUnit =%> CUnit
242 |   maybeU = maybeToCoprod CUnit ⨾ dia
243 |
244 | namespace Definition12
245 |
246 |   public export
247 |   (>>) : Container -> Container -> Container
248 |   (>>) c1 c2 = (x : Σ c1.req (\r => c1.res r -> c2.req))
249 |                !> Σ (c1.res x.π1) (\r => c2.res (x.π2 r))
250 |
251 | namespace Definition13
252 |
253 |   public export
254 |   compLUnit : CUnit >> c =%> c
255 |   compLUnit = (\x => x.π2 ()) <| (\x, y => () ## y)
256 |
257 |   public export
258 |   compRUnit : c >> CUnit =%> c
259 |   compRUnit = (\x => x.π1) <| (\x, y => y ## ())
260 |
261 | namespace Definition14
262 |
263 |   public export
264 |   data StarShp : Container -> Type where
265 |     Done : forall c. StarShp c
266 |     More : forall c. Ex c (StarShp c) -> StarShp c
267 |
268 |   public export
269 |   StarPos : (c : Container) -> StarShp c -> Type
270 |   StarPos c Done = Unit
271 |   StarPos c (More x) = Σ (c.res x.ex1) (\y => assert_total $ StarPos c (x.ex2 y))
272 |
273 |   public export
274 |   Kleene : Container -> Container
275 |   Kleene c = (!>) (StarShp c) (StarPos c)
276 |
277 | %unbound_implicits on
278 | namespace Proposition15
279 |
280 |   -- We can map the requests
281 |   public export
282 |   mapStarShp : (a =%> b) -> StarShp a -> StarShp b
283 |   mapStarShp x Done = Done
284 |   mapStarShp x (More p1) = More (MkEx (x.fwd p1.ex1) (\y : b.res (x.fwd p1.ex1) => assert_total $ mapStarShp x (p1.ex2 (x.bwd p1.ex1 y))))
285 |
286 |   -- We can map the responses
287 |   mapStarPos : (mor : a =%> b) -> (x : StarShp a) -> StarPos b (mapStarShp mor x) -> StarPos a x
288 |   mapStarPos y Done z = MkUnit
289 |   mapStarPos y (More (MkEx x1 x2)) (y1 ## y2) = y.bwd x1 y1 ## mapStarPos y (x2 (y.bwd x1 y1)) y2
290 |
291 |   public export
292 |   map_kleene : a =%> b -> Kleene a =%> Kleene b
293 |   map_kleene mor = mapStarShp mor <| mapStarPos mor
294 |
295 |   -- Mapping morphisms preserves identity
296 |   public export 0
297 |   kleene_pres_id : forall a. map_kleene (identity {a}) `DepLensEq` identity {a = Kleene a}
298 |   kleene_pres_id = MkDepLensEq starShpMapId kleene_pres_id_rhs
299 |     where
300 |       starShpMapId : (x : StarShp a) -> mapStarShp Morphism.identity x === x
301 |       starShpMapId Done = Refl
302 |       starShpMapId (More (MkEx x1 x2)) = cong More
303 |           $ exEqToEq $ MkExEq  Refl (\vx => starShpMapId (x2 vx))
304 |
305 |       kleene_pres_id_rhs :
306 |           (vx : StarShp a) ->
307 |           (vy : StarPos a (mapStarShp Morphism.identity vx)) ->
308 |           mapStarPos (Morphism.identity {a}) vx vy = replace {p = StarPos a} (starShpMapId vx) vy
309 |       kleene_pres_id_rhs Done () = Refl
310 |       kleene_pres_id_rhs (More x) (v1 ## v2) with (x.ex2 v1) proof p
311 |         kleene_pres_id_rhs (More (MkEx x1 x2)) (v1 ## ()) | Done = sigEqToEq $ MkSigEq Refl (rewrite p in Refl)
312 |         kleene_pres_id_rhs (More (MkEx x1 x2)) (v1 ## v2) | More pat = sigEqToEq $ MkSigEq Refl (kleene_pres_id_rhs (x2 v1) (rewrite p in v2))
313 |
314 |   -- Mapping morphisms preserves composition
315 |   public export 0
316 |   kleene_pres_comp : forall a, b, c. (f : a =%> b) -> (g : b =%> c) ->
317 |                      map_kleene (f ⨾ g) `DepLensEq` (map_kleene f ⨾ map_kleene g)
318 |   kleene_pres_comp f g = MkDepLensEq starShpComp eqBwd'
319 |     where
320 |       starShpComp : (vs : StarShp a) -> mapStarShp (f ⨾ g) vs = mapStarShp g (mapStarShp f vs)
321 |       starShpComp Done = Refl
322 |       starShpComp (More x) = cong More $
323 |                              exEqToEq $
324 |                              MkExEq Refl
325 |                              (\vx => assert_total $ starShpComp (x .ex2 ((f ⨾ g) .bwd (x .ex1) vx)))
326 |
327 |       eqBwd' : (v : StarShp a) -> (y : StarPos c (mapStarShp (f ⨾ g) v)) ->
328 |           let 0 p1, p2 : StarPos a v
329 |               p1 = mapStarPos (f ⨾ g) v y
330 |               p2 = mapStarPos f v (mapStarPos g (mapStarShp f v) (replace {p = StarPos c} (starShpComp v) y))
331 |           in p1 === p2
332 |       eqBwd' Done y = Refl
333 |       eqBwd' (More (MkEx x1 x2)) (y1 ## y2) = Calc $
334 |         |~ mapStarPos (f ⨾ g) (More (MkEx x1 x2)) (y1 ## y2)
335 |         ~~ (f ⨾ g).bwd x1 y1             ## mapStarPos (f ⨾ g) (x2 ((f ⨾ g).bwd x1 y1)) y2 ...(Refl)
336 |         ~~ f.bwd x1 (g.bwd (f.fwd x1) y1) ## mapStarPos f (x2 (f.bwd x1 (g.bwd (f.fwd x1) y1))) (mapStarPos g (mapStarShp f (x2 (f.bwd x1 (g.bwd (f.fwd x1) y1)))) (replace {p = StarPos c} (starShpComp (x2 (f.bwd x1 (g.bwd (f.fwd x1) y1)))) y2))
337 |             ...(sigEqToEq $ MkSigEq Refl (eqBwd' (x2 (f .bwd x1 (g .bwd (f .fwd x1) y1))) y2))
338 |         ~~ mapStarPos f (More (MkEx x1 x2)) (g.bwd (f.fwd x1) y1 ## mapStarPos g (mapStarShp f (x2 (f.bwd x1 (g.bwd (f.fwd x1) y1)))) (replace {p = StarPos c} (starShpComp (x2 (f.bwd x1 (g.bwd (f.fwd x1) y1)))) y2)) ...(Refl)
339 |         ~~ mapStarPos f (More (MkEx x1 x2)) (mapStarPos g (More (MkEx (f.fwd x1)  (\y : b.res (f.fwd x1) => assert_total $ mapStarShp f (x2 (f.bwd x1 y))))) (replace {p = StarPos c} (starShpComp (More (MkEx x1 x2))) (y1 ## y2))) ...(Refl)
340 |         ~~ mapStarPos f (More (MkEx x1 x2)) (mapStarPos g (mapStarShp f (More (MkEx x1 x2))) (replace {p = StarPos c} (starShpComp (More (MkEx x1 x2))) (y1 ## y2))) ...(Refl)
341 |
342 |   partial
343 |   KleeneFunctor : Functor Cont Cont
344 |   KleeneFunctor = MkFunctor
345 |       Kleene
346 |       (\_, _ => map_kleene)
347 |       (\_ => depLensEqToEq $ kleene_pres_id)
348 |       (\a, b, c, f, g => depLensEqToEq $ kleene_pres_comp f g)
349 |
350 | namespace StateCostateContext
351 |   namespace Definition16
352 |
353 |     public export
354 |     State : Container -> Type
355 |     State c = CUnit =%> c
356 |
357 |     public export
358 |     value : State a -> a.req
359 |     value m = m.fwd ()
360 |
361 |     public export
362 |     state : a.req -> State a
363 |     state x = const x <| (\_, _ => ())
364 |
365 |   namespace Definition17
366 |
367 |     public export
368 |     Costate : Container -> Type
369 |     Costate c = c =%> CUnit
370 |
371 |     public export
372 |     costate : ((x : a.req) -> a.res x) -> Costate a
373 |     costate f = const () <| (\x, _ => f x)
374 |
375 |     public export
376 |     exec : Costate a -> (x : a.req) -> a.res x
377 |     exec m x = m.bwd x ()
378 |
379 |   namespace Definition18
380 |
381 |     Context : (a, b : Container) -> Type
382 |     Context a b = a.req * ((x : b.req) -> b.res x)
383 |
384 |     split : Context a b -> State a * Costate b
385 |     split = bimap state costate
386 |
387 |     run : (i : State a) -> Costate b -> a =%> b -> a.res (value i)
388 |     run st co m = exec (m ⨾ co) (value st)
389 |
390 | namespace Definition19
391 |
392 |   public export
393 |   Lift : (Type -> Type) -> Container -> Container
394 |   Lift f c = (!>) c.req (f . c.res)
395 |
396 | %unbound_implicits off
397 | namespace Proposition20
398 |   parameters (f : Functor Idris Idris)
399 |
400 |     public export
401 |     f_hom : {0 a, b : Container} -> a =%> b ->  Lift f.F a =%> Lift f.F b
402 |     f_hom c = c.fwd <| \x => f.F' _ _ (c.bwd x)
403 |
404 |     public export 0
405 |     f_pres_id : (a : Container) -> f_hom (identity {a}) `DepLensEq` identity {a = Lift f.F a}
406 |     f_pres_id a = MkDepLensEq (\_ => Refl) (\x, y => let hh = f.presId (a.res x) in app _ _ hh y)
407 |
408 |     public export 0
409 |     f_pres_comp : (a, b, c : Container) -> (f1 : a =%> b) -> (f2 : b =%> c) ->
410 |                     f_hom (f1 ⨾ f2) `DepLensEq` f_hom f1 ⨾ f_hom f2
411 |     f_pres_comp a b c f1 f2 = MkDepLensEq
412 |         (\_ => Refl)
413 |         (\v, y => let hh = f.presComp _ _ _ (f2.bwd ((f_hom f1).fwd v)) (f1.bwd v) in app _ _ hh y)
414 |
415 |     public export
416 |     LiftIsFunctor : Functor Cont Cont
417 |     LiftIsFunctor = MkFunctor
418 |       (Lift f.F)
419 |       (\_, _, m => f_hom m)
420 |       (\x => depLensEqToEq $ f_pres_id x)
421 |       (\a, b, c, f, g => depLensEqToEq $ f_pres_comp a b c f g)
422 |
423 | namespace Proposition21
424 |   parameters (m : Monad Idris)
425 |
426 |     Fn : Container -> Container
427 |     Fn = Lift m.endo.F
428 |
429 |     base_counit : (v : Container) -> Fn v =%> v
430 |     base_counit v = id <| (\x, y => m.η.comp (v.res x) y )
432 |     base_comult : (v : Container) -> Fn v =%> Fn (Fn v)
433 |     base_comult v = id <| \x => m.μ.comp (v.res x)
435 |     identity_left : (v : Container) ->
436 |                     base_comult v ⨾ base_counit (Fn v)
437 |                     `DepLensEq`
438 |                     identity {a = Fn v}
439 |     identity_left v = MkDepLensEq (\_ => Refl) (\vx, y => let
440 |                                   m' = m.identityLeft (v.res vx)
441 |                                   in app _ _ m' y)
443 |     identity_right : (v : Container) ->
444 |                      base_comult v ⨾ f_hom m.endo (base_counit v)
445 |                      `DepLensEq`
446 |                     identity {a = Fn v}
447 |     identity_right v = MkDepLensEq (\_ => Refl) (\vx, vy => let
448 |                                    m' = m.identityRight (v.res vx)
449 |                                    in app _ _ m' vy)
451 |     monad_square : (v : Container) ->
452 |                    let top : Fn v =%> Fn (Fn v)
453 |                        top = base_comult v
454 |                        right : Fn (Fn v) =%> Fn (Fn (Fn v))
455 |                        right = f_hom m.endo (base_comult v)
456 |                        left : Fn v =%> Fn (Fn v)
457 |                        left = base_comult v
458 |                        bot : Fn (Fn v) =%> Fn (Fn (Fn v))
459 |                        bot = base_comult (Fn v)
460 |                     in top ⨾ right `DepLensEq` left ⨾ bot
461 |     monad_square v = MkDepLensEq (\_ => Refl)
462 |         (\vx, vy => app _ _ (m.square (v.res vx)) vy)
464 |     comonad : ContainerComonad (LiftIsFunctor m.endo)
465 |     comonad = MkContainerComonad
466 |         base_counit
467 |         base_comult
468 |         monad_square
469 |         identity_left
470 |         identity_right
472 | %unbound_implicits on
473 | namespace Definition22
475 |   distrib_plus : Lift f (a + b) =%> Lift f a + Lift f b
476 |   distrib_plus = id <| \case (<+ x) => id ; (+> x) => id
478 | namespace Definition23
480 |   distrib_maybeAll : Monad m => Lift m (MaybeAllIdris a) =%> MaybeAllIdris (Lift m a)
481 |   distrib_maybeAll = id <| \case Nothing => \x => pure Nah
482 |                                ; (Just x) => \(Aye y) => map Aye y
484 | namespace Definition24
486 |   seq2M : Monad m => Costate (Lift m a) -> Costate (Lift m b) -> Costate (Lift m (a >> b))
487 |   seq2M x y = costate (\xn => do v1 <- extract x xn.π1
488 |                                  v2 <- extract y (xn.π2 v1)
489 |                                  pure (v1 ## v2))