{-# OPTIONS --cubical --safe #-}

open import Semirings

module Probability {s} (rng : Semiring s) where

open Semiring rng

open import Cubical.Core.Everything
open import Cubical.Relation.Everything
open import Cubical.Foundations.Prelude hiding (_β‰‘βŸ¨_⟩_)
open import Cubical.HITs.SetTruncation
open import Utils

infixr 5 _&_∷_
data 𝒫 (A : Set a) : Set (a βŠ” s) where
  []  : 𝒫 A
  _&_∷_ : (p : R) β†’ (x : A) β†’ 𝒫 A β†’ 𝒫 A
  dup : βˆ€ p q x xs β†’ p & x ∷ q & x ∷ xs ≑ p + q & x ∷ xs
  com : βˆ€ p x q y xs β†’ p & x ∷ q & y ∷ xs ≑ q & y ∷ p & x ∷ xs
  del : βˆ€ x xs β†’ 0# & x ∷ xs ≑ xs
  trunc : isSet (𝒫 A)

record βŸ…_↝_βŸ† {a β„“} (A : Set a) (P : 𝒫 A β†’ Set β„“) : Set (a βŠ” β„“ βŠ” s) where
  constructor elim
  field
    βŸ…_βŸ†-set : βˆ€ {xs} β†’ isSet (P xs)
    βŸ…_βŸ†[] : P []
    βŸ…_βŸ†_&_∷_ : βˆ€ p x xs β†’ P xs β†’ P (p & x ∷ xs)
  private z = βŸ…_βŸ†[]; f = βŸ…_βŸ†_&_∷_
  field
    βŸ…_βŸ†-dup : (βˆ€ p q x xs pxs β†’ PathP (Ξ» i β†’ P (dup p q x xs i))
              (f p x (q & x ∷ xs) (f q x xs pxs)) (f (p + q) x xs pxs))
    βŸ…_βŸ†-com : (βˆ€ p x q y xs pxs β†’ PathP (Ξ» i β†’ P (com p x q y xs i))
              (f p x (q & y ∷ xs) (f q y xs pxs)) (f q y (p & x ∷ xs) (f p x xs pxs)))
    βŸ…_βŸ†-del : (βˆ€ x xs pxs β†’ PathP (Ξ» i β†’ P (del x xs i))
              (f 0# x xs pxs) pxs)
  βŸ…_βŸ†β‡“ : (xs : 𝒫 A) β†’ P xs
  βŸ… [] βŸ†β‡“ = z
  βŸ… p & x ∷ xs βŸ†β‡“ = f p x xs βŸ… xs βŸ†β‡“
  βŸ… dup p q x xs i βŸ†β‡“ = βŸ…_βŸ†-dup p q x xs βŸ… xs βŸ†β‡“ i
  βŸ… com p x q y xs i βŸ†β‡“ = βŸ…_βŸ†-com p x q y xs βŸ… xs βŸ†β‡“ i
  βŸ… del x xs i βŸ†β‡“ = βŸ…_βŸ†-del x xs βŸ… xs βŸ†β‡“ i
  βŸ… trunc xs ys p q i j βŸ†β‡“ =
    elimSquashβ‚€ (Ξ» xs β†’ βŸ…_βŸ†-set {xs}) (trunc xs ys p q) βŸ… xs βŸ†β‡“ βŸ… ys βŸ†β‡“ (cong βŸ…_βŸ†β‡“ p) (cong βŸ…_βŸ†β‡“ q) i j

open βŸ…_↝_βŸ† public
elim-syntax : βˆ€ {a β„“} β†’ (A : Set a) β†’ (𝒫 A β†’ Set β„“) β†’ Set (a βŠ” β„“ βŠ” s)
elim-syntax = βŸ…_↝_βŸ†

syntax elim-syntax A (Ξ» xs β†’ Pxs) = [ xs βˆˆπ’« A ↝ Pxs ]

record ⟦_β‡’_⟧ {a β„“} (A : Set a) (P : 𝒫 A β†’ Set β„“) : Set (a βŠ” β„“ βŠ” s) where
  constructor elim-prop
  field
    ⟦_⟧-prop : βˆ€ {xs} β†’ isProp (P xs)
    ⟦_⟧[] : P []
    ⟦_⟧_&_∷_⟨_⟩ : βˆ€ p x xs β†’ P xs β†’ P (p & x ∷ xs)
  private z = ⟦_⟧[]; f = ⟦_⟧_&_∷_⟨_⟩
  ⟦_βŸ§β‡‘ = elim
          (isPropβ†’isSet ⟦_⟧-prop)
          z f
          (Ξ» p q x xs pxs β†’
            toPathP (⟦_⟧-prop (transp (Ξ» i β†’ P (dup p q x xs i))
            i0
            (f p x (q & x ∷ xs) (f q x xs pxs))) (f (p + q) x xs pxs) ))
          (Ξ» p x q y xs pxs β†’ toPathP (⟦_⟧-prop (transp (Ξ» i β†’ P (com p x q y xs i)) i0
            (f p x (q & y ∷ xs) (f q y xs pxs))) (f q y (p & x ∷ xs) (f p x xs pxs))))
            Ξ» x xs pxs β†’ toPathP (⟦_⟧-prop (transp (Ξ» i β†’ P (del x xs i)) i0 ((f 0# x xs pxs))) pxs)
  ⟦_βŸ§β‡“ = βŸ… ⟦_βŸ§β‡‘ βŸ†β‡“

open ⟦_β‡’_⟧ public
elim-prop-syntax : βˆ€ {a β„“} β†’ (A : Set a) β†’ (𝒫 A β†’ Set β„“) β†’ Set (a βŠ” β„“ βŠ” s)
elim-prop-syntax = ⟦_β‡’_⟧

syntax elim-prop-syntax A (Ξ» xs β†’ Pxs) = ⟦ xs βˆˆπ’« A β‡’ Pxs ⟧

record [_↦_] {a b} (A : Set a) (B : Set b) : Set (a βŠ” b βŠ” s) where
  constructor rec
  field
    [_]-set  : isSet B
    [_]_&_∷_ : R β†’ A β†’ B β†’ B
    [_][]    : B
  private f = [_]_&_∷_; z = [_][]
  field
    [_]-dup  : βˆ€ p q x xs β†’ f p x (f q x xs) ≑ f (p + q) x xs
    [_]-com : βˆ€ p x q y xs β†’ f p x (f q y xs) ≑ f q y (f p x xs)
    [_]-del : βˆ€ x xs β†’ f 0# x xs ≑ xs
  [_]⇑ = elim
            [_]-set
            z
            (Ξ» p x _ xs β†’ f p x xs)
            (Ξ» p q x xs β†’ [_]-dup p q x)
            (Ξ» p x q y xs β†’ [_]-com p x q y)
            (Ξ» x xs β†’ [_]-del x)
  [_]↓ = βŸ… [_]⇑ βŸ†β‡“
open [_↦_] public

map : (A β†’ B) β†’ 𝒫 A β†’ 𝒫 B
map = Ξ» f β†’ [ mapβ€² f ]↓
  module Map where
  mapβ€² : (A β†’ B) β†’ [ A ↦ 𝒫 B ]
  [ mapβ€² f ] p & x ∷ xs = p & f x ∷ xs
  [ mapβ€² f ][] = []
  [ mapβ€² f ]-set = trunc
  [ mapβ€² f ]-dup p q x xs = dup p q (f x) xs
  [ mapβ€² f ]-com p x q y xs = com p (f x) q (f y) xs
  [ mapβ€² f ]-del x xs = del (f x) xs

infixr 5 _βˆͺ_
_βˆͺ_ : 𝒫 A β†’ 𝒫 A β†’ 𝒫 A
_βˆͺ_ = Ξ» xs ys β†’ [ union ys ]↓ xs
  module Union where
  union : 𝒫 A β†’ [ A ↦ 𝒫 A ]
  [ union ys ]-set = trunc
  [ union ys ] p & x ∷ xs = p & x ∷ xs
  [ union ys ][] = ys
  [ union ys ]-dup = dup
  [ union ys ]-com = com
  [ union ys ]-del = del

infixl 7 _β‹Š_
_β‹Š_ : R β†’ 𝒫 A β†’ 𝒫 A
_β‹Š_ = Ξ» p β†’ [ p β‹Šβ€² ]↓
  module Cond where
  _β‹Šβ€² : R β†’ [ A ↦ 𝒫 A ]
  [ p β‹Šβ€² ]-set = trunc
  [ p β‹Šβ€² ][] = []
  [ p β‹Šβ€² ] q & x ∷ xs = p * q & x ∷ xs
  [ p β‹Šβ€² ]-com q x r y xs = com (p * q) x (p * r) y xs
  [ p β‹Šβ€² ]-dup q r x xs =
    p * q & x ∷ p * r & x ∷ xs β‰‘βŸ¨ dup (p * q) (p * r) x xs ⟩
    p * q + p * r & x ∷ xs     β‰‘Λ˜βŸ¨ cong (_& x ∷ xs) (*⟨+⟩ p q r) ⟩
    p * (q + r) & x ∷ xs       ∎
  [ p β‹Šβ€² ]-del x xs =
    p * 0# & x ∷ xs β‰‘βŸ¨ cong (_& x ∷ xs) (*0 p) ⟩
    0# & x ∷ xs     β‰‘βŸ¨ del x xs ⟩
    xs              ∎

∫ : (A β†’ R) β†’ 𝒫 A β†’ R
∫ = Ξ» f β†’ [ βˆ«β€² f ]↓
  module Expect where
  βˆ«β€² : (A β†’ R) β†’ [ A ↦ R ]
  [ βˆ«β€² f ]-set = sIsSet
  [ βˆ«β€² f ] p & x ∷ xs = p * f x + xs
  [ βˆ«β€² f ][] = 0#
  [ βˆ«β€² f ]-dup p q x xs =
    p * f x + (q * f x + xs) β‰‘Λ˜βŸ¨ +-assoc (p * f x) (q * f x) xs ⟩
    (p * f x + q * f x) + xs β‰‘Λ˜βŸ¨ cong (_+ xs) (⟨+⟩* p q (f x)) ⟩
    (p + q) * f x + xs ∎
  [ βˆ«β€² f ]-com p x q y xs =
    p * f x + (q * f y + xs) β‰‘Λ˜βŸ¨ +-assoc (p * f x) (q * f y) (xs) ⟩
    p * f x + q * f y + xs   β‰‘βŸ¨ cong (_+ xs) (+-comm (p * f x) (q * f y)) ⟩
    q * f y + p * f x + xs   β‰‘βŸ¨ +-assoc (q * f y) (p * f x) (xs) ⟩
    q * f y + (p * f x + xs) ∎
  [ βˆ«β€² f ]-del x xs =
    0# * f x + xs β‰‘βŸ¨ cong (_+ xs) (0* (f x)) ⟩
    0# + xs       β‰‘βŸ¨ 0+ (xs) ⟩
    xs            ∎

syntax ∫ (Ξ» x β†’ e) = ∫ e 𝑑 x

pure : A β†’ 𝒫 A
pure x = 1# & x ∷ []

βˆͺ-cons : βˆ€ p (x : A) xs ys β†’ xs βˆͺ p & x ∷ ys ≑ p & x ∷ xs βˆͺ ys
βˆͺ-cons = Ξ» p x xs ys β†’ ⟦ βˆͺ-consβ€² p x ys βŸ§β‡“ xs
  module UCons where
  βˆͺ-consβ€² : βˆ€ p x ys β†’ ⟦ xs βˆˆπ’« A β‡’ xs βˆͺ p & x ∷ ys ≑ p & x ∷ xs βˆͺ ys ⟧
  ⟦ βˆͺ-consβ€² p x ys ⟧-prop = trunc _ _
  ⟦ βˆͺ-consβ€² p x ys ⟧[] = refl
  ⟦ βˆͺ-consβ€² p x ys ⟧ r & y ∷ xs ⟨ P ⟩ = cong (r & y ∷_) P βˆ™ com r y p x (xs βˆͺ ys)

β‹Š-distribΚ³ : βˆ€ p q β†’ (xs : 𝒫 A) β†’ p β‹Š xs βˆͺ q β‹Š xs ≑ (p + q) β‹Š xs
β‹Š-distribΚ³ = Ξ» p q β†’ ⟦ β‹Š-distribΚ³β€² p q βŸ§β‡“
  module JDistrib where
  β‹Š-distribΚ³β€² : βˆ€ p q β†’ ⟦ xs βˆˆπ’« A β‡’ p β‹Š xs βˆͺ q β‹Š xs ≑ (p + q) β‹Š xs ⟧
  ⟦ β‹Š-distribΚ³β€² p q ⟧-prop = trunc _ _
  ⟦ β‹Š-distribΚ³β€² p q ⟧[] = refl
  ⟦ β‹Š-distribΚ³β€² p q ⟧ r & x ∷ xs ⟨ P ⟩ =
    p β‹Š (r & x ∷ xs) βˆͺ q β‹Š (r & x ∷ xs)   β‰‘βŸ¨ βˆͺ-cons (q * r) x (p β‹Š (r & x ∷ xs)) (q β‹Š xs)  ⟩
    q * r & x ∷ p β‹Š (r & x ∷ xs) βˆͺ q β‹Š xs β‰‘βŸ¨ cong (_βˆͺ q β‹Š xs) (dup (q * r) (p * r) x (p β‹Š xs)) ⟩
    q * r + p * r & x ∷ p β‹Š xs βˆͺ q β‹Š xs   β‰‘Λ˜βŸ¨ cong (_& x ∷ (p β‹Š xs βˆͺ q β‹Š xs)) (⟨+⟩* q p r) ⟩
    (q + p) * r & x ∷ p β‹Š xs βˆͺ q β‹Š xs     β‰‘βŸ¨ cong ((q + p) * r & x ∷_) P ⟩
    (q + p) * r & x ∷ (p + q) β‹Š xs                β‰‘βŸ¨ cong (Ξ» pq β†’ pq * r & x ∷ (p + q) β‹Š xs) (+-comm q p) ⟩
    (p + q) * r & x ∷ (p + q) β‹Š xs                β‰‘βŸ¨βŸ©
    _β‹Š_ (p + q) (r & x ∷ xs) ∎

β‹Š-distribΛ‘ : βˆ€ p β†’ (xs ys : 𝒫 A) β†’ p β‹Š xs βˆͺ p β‹Š ys ≑ p β‹Š (xs βˆͺ ys)
β‹Š-distribΛ‘ = Ξ» p xs ys β†’ ⟦ β‹Š-distribΛ‘β€² p ys βŸ§β‡“ xs
  module JDistribL where
  β‹Š-distribΛ‘β€² : βˆ€ p ys β†’ ⟦ xs βˆˆπ’« A β‡’ p β‹Š xs βˆͺ p β‹Š ys ≑ p β‹Š (xs βˆͺ ys) ⟧
  ⟦ β‹Š-distribΛ‘β€² p ys ⟧-prop = trunc _ _
  ⟦ β‹Š-distribΛ‘β€² p ys ⟧[] = refl
  ⟦ β‹Š-distribΛ‘β€² p ys ⟧ q & x ∷ xs ⟨ P ⟩ =
    p β‹Š (q & x ∷ xs) βˆͺ p β‹Š ys β‰‘βŸ¨βŸ©
    p * q & x ∷ p β‹Š xs βˆͺ p β‹Š ys β‰‘βŸ¨ cong (p * q & x ∷_) P ⟩
    p * q & x ∷ p β‹Š (xs βˆͺ ys) β‰‘βŸ¨βŸ©
    p β‹Š ((q & x ∷ xs) βˆͺ ys) ∎

βˆͺ-assoc : (xs ys zs : 𝒫 A) β†’ xs βˆͺ (ys βˆͺ zs) ≑ (xs βˆͺ ys) βˆͺ zs
βˆͺ-assoc = Ξ» xs ys zs β†’ ⟦ βˆͺ-assocβ€² ys zs βŸ§β‡“ xs
  module UAssoc where
  βˆͺ-assocβ€² : βˆ€ ys zs β†’ ⟦ xs βˆˆπ’« A β‡’ xs βˆͺ (ys βˆͺ zs) ≑ (xs βˆͺ ys) βˆͺ zs ⟧
  ⟦ βˆͺ-assocβ€² ys zs ⟧-prop = trunc _ _
  ⟦ βˆͺ-assocβ€² ys zs ⟧[] = refl
  ⟦ βˆͺ-assocβ€² ys zs ⟧ p & x ∷ xs ⟨ P ⟩ = cong (p & x ∷_) P

βˆͺ-idΚ³ : (xs : 𝒫 A) β†’ xs βˆͺ [] ≑ xs
βˆͺ-idΚ³ = ⟦ βˆͺ-idΚ³β€² βŸ§β‡“
  module UIdR where
  βˆͺ-idΚ³β€² : ⟦ xs βˆˆπ’« A β‡’ xs βˆͺ [] ≑ xs ⟧
  ⟦ βˆͺ-idΚ³β€² ⟧-prop = trunc _ _
  ⟦ βˆͺ-idΚ³β€² ⟧[] = refl
  ⟦ βˆͺ-idΚ³β€² ⟧ p & x ∷ xs ⟨ P ⟩ = cong (p & x ∷_) P

βˆͺ-comm : (xs ys : 𝒫 A) β†’ xs βˆͺ ys ≑ ys βˆͺ xs
βˆͺ-comm = Ξ» xs ys β†’ ⟦ βˆͺ-commβ€² ys βŸ§β‡“ xs
  module UComm where
  βˆͺ-commβ€² : βˆ€ ys β†’ ⟦ xs βˆˆπ’« A β‡’ xs βˆͺ ys ≑ ys βˆͺ xs ⟧
  ⟦ βˆͺ-commβ€² ys ⟧-prop = trunc _ _
  ⟦ βˆͺ-commβ€² ys ⟧[] = sym (βˆͺ-idΚ³ ys)
  ⟦ βˆͺ-commβ€² ys ⟧ p & x ∷ xs ⟨ P ⟩ = cong (p & x ∷_) P βˆ™ sym (βˆͺ-cons p x ys xs)

0β‹Š : (xs : 𝒫 A) β†’ 0# β‹Š xs ≑ []
0β‹Š = ⟦ 0β‹Šβ€² βŸ§β‡“
  module ZeroJ where
  0β‹Šβ€² : ⟦ xs βˆˆπ’« A β‡’ 0# β‹Š xs ≑ [] ⟧
  ⟦ 0β‹Šβ€² ⟧-prop = trunc _ _
  ⟦ 0β‹Šβ€² ⟧[] = refl
  ⟦ 0β‹Šβ€² ⟧ p & x ∷ xs ⟨ P ⟩ =
    0# β‹Š (p & x ∷ xs)    β‰‘βŸ¨βŸ©
    0# * p & x ∷ 0# β‹Š xs β‰‘βŸ¨ cong (_& x ∷ 0# β‹Š xs) (0* p) ⟩
    0# & x ∷ 0# β‹Š xs     β‰‘βŸ¨ del x (0# β‹Š xs) ⟩
    0# β‹Š xs              β‰‘βŸ¨ P ⟩
    [] ∎

_>>=_ : 𝒫 A β†’ (A β†’ 𝒫 B) β†’ 𝒫 B
xs >>= f = [ f =<< ]↓ xs
  module Bind where
  _=<< : (A β†’ 𝒫 B) β†’ [ A ↦ 𝒫 B ]
  [ f =<< ] p & x ∷ xs = p β‹Š (f x) βˆͺ xs
  [ f =<< ][] = []
  [ f =<< ]-set = trunc
  [ f =<< ]-del x xs = cong (_βˆͺ xs) (0β‹Š (f x))
  [ f =<< ]-dup p q x xs =
    p β‹Š (f x) βˆͺ q β‹Š (f x) βˆͺ xs   β‰‘βŸ¨ βˆͺ-assoc (p β‹Š f x) (q β‹Š f x) xs ⟩
    (p β‹Š (f x) βˆͺ q β‹Š (f x)) βˆͺ xs β‰‘βŸ¨ cong (_βˆͺ xs) (β‹Š-distribΚ³ p q (f x) ) ⟩
    _β‹Š_ (p + q) (f x) βˆͺ xs ∎
  [ f =<< ]-com p x q y xs =
    p β‹Š (f x) βˆͺ q β‹Š (f y) βˆͺ xs   β‰‘βŸ¨ βˆͺ-assoc (p β‹Š f x) (q β‹Š f y) xs ⟩
    (p β‹Š (f x) βˆͺ q β‹Š (f y)) βˆͺ xs β‰‘βŸ¨ cong (_βˆͺ xs) (βˆͺ-comm (p β‹Š f x) (q β‹Š f y)) ⟩
    (q β‹Š (f y) βˆͺ p β‹Š (f x)) βˆͺ xs β‰‘Λ˜βŸ¨ βˆͺ-assoc (q β‹Š f y) (p β‹Š f x) xs ⟩
    q β‹Š (f y) βˆͺ p β‹Š (f x) βˆͺ xs ∎

_<*>_ : 𝒫 (A β†’ B) β†’ 𝒫 A β†’ 𝒫 B
fs <*> xs = do
  f ← fs
  x ← xs
  pure (f x)

1β‹Š : (xs : 𝒫 A) β†’ 1# β‹Š xs ≑ xs
1β‹Š = ⟦ 1β‹Šβ€² βŸ§β‡“
  module OneJoin where
  1β‹Šβ€² : ⟦ xs βˆˆπ’« A β‡’ 1# β‹Š xs ≑ xs ⟧
  ⟦ 1β‹Šβ€² ⟧-prop = trunc _ _
  ⟦ 1β‹Šβ€² ⟧[] = refl
  ⟦ 1β‹Šβ€² ⟧ p & x ∷ xs ⟨ P ⟩ =
    1# β‹Š (p & x ∷ xs) β‰‘βŸ¨βŸ©
    1# * p & x ∷ 1# β‹Š xs β‰‘βŸ¨ cong (_& x ∷ 1# β‹Š xs) (1* p) ⟩
    p & x ∷ 1# β‹Š xs β‰‘βŸ¨ cong (p & x ∷_) P ⟩
    p & x ∷ xs ∎

>>=-distrib : (xs ys : 𝒫 A) (g : A β†’ 𝒫 B) β†’ (xs βˆͺ ys) >>= g ≑ (xs >>= g) βˆͺ (ys >>= g)
>>=-distrib = Ξ» xs ys g β†’ ⟦ >>=-distribβ€² ys g βŸ§β‡“ xs
  module BindDistrib where
  >>=-distribβ€² : (ys : 𝒫 A) (g : A β†’ 𝒫 B) β†’ ⟦ xs βˆˆπ’« A β‡’ ((xs βˆͺ ys) >>= g) ≑ (xs >>= g) βˆͺ (ys >>= g) ⟧
  ⟦ >>=-distribβ€² ys g ⟧-prop = trunc _ _
  ⟦ >>=-distribβ€² ys g ⟧[] = refl
  ⟦ >>=-distribβ€² ys g ⟧ p & x ∷ xs ⟨ P ⟩ =
    (((p & x ∷ xs) βˆͺ ys) >>= g) β‰‘βŸ¨βŸ©
    (p & x ∷ xs βˆͺ ys) >>= g β‰‘βŸ¨βŸ©
    p β‹Š g x βˆͺ ((xs βˆͺ ys) >>= g) β‰‘βŸ¨ cong (p β‹Š g x βˆͺ_) P ⟩
    p β‹Š g x βˆͺ ((xs >>= g) βˆͺ (ys >>= g)) β‰‘βŸ¨ βˆͺ-assoc (p β‹Š g x) (xs >>= g) (ys >>= g) ⟩
    (p β‹Š g x βˆͺ (xs >>= g)) βˆͺ (ys >>= g) β‰‘βŸ¨βŸ©
    ((p & x ∷ xs) >>= g) βˆͺ (ys >>= g) ∎

*-assoc-β‹Š : βˆ€ p q (xs : 𝒫 A) β†’ (p * q) β‹Š xs ≑ p β‹Š (q β‹Š xs)
*-assoc-β‹Š = Ξ» p q β†’ ⟦ *-assoc-β‹Šβ€² p q βŸ§β‡“
  module MAssocJ where
  *-assoc-β‹Šβ€² : βˆ€ p q β†’ ⟦ xs βˆˆπ’« A β‡’ (p * q) β‹Š xs ≑ p β‹Š (q β‹Š xs) ⟧
  ⟦ *-assoc-β‹Šβ€² p q ⟧-prop = trunc _ _
  ⟦ *-assoc-β‹Šβ€² p q ⟧[] = refl
  ⟦ *-assoc-β‹Šβ€² p q ⟧ r & x ∷ xs ⟨ P ⟩ =
    p * q β‹Š (r & x ∷ xs) β‰‘βŸ¨βŸ©
    p * q * r & x ∷ (p * q β‹Š xs) β‰‘βŸ¨ cong (_& x ∷ (p * q β‹Š xs)) (*-assoc p q r) ⟩
    p * (q * r) & x ∷ (p * q β‹Š xs) β‰‘βŸ¨ cong (p * (q * r) & x ∷_) P ⟩
    p * (q * r) & x ∷ (p β‹Š (q β‹Š xs)) β‰‘βŸ¨βŸ©
    p β‹Š (q β‹Š (r & x ∷ xs)) ∎

β‹Š-assoc->>= : βˆ€ p (xs : 𝒫 A) (f : A β†’ 𝒫 B) β†’ (p β‹Š xs) >>= f ≑ p β‹Š (xs >>= f)
β‹Š-assoc->>= = Ξ» p xs f β†’ ⟦ β‹Š-assoc->>=β€² p f βŸ§β‡“ xs
  module JDistribB where
  β‹Š-assoc->>=β€² : βˆ€ p (f : A β†’ 𝒫 B) β†’ ⟦ xs βˆˆπ’« A β‡’ (p β‹Š xs) >>= f ≑ p β‹Š (xs >>= f) ⟧
  ⟦ β‹Š-assoc->>=β€² p f ⟧-prop = trunc _ _
  ⟦ β‹Š-assoc->>=β€² p f ⟧[] = refl
  ⟦ β‹Š-assoc->>=β€² p f ⟧ q & x ∷ xs ⟨ P ⟩ =
    (p β‹Š (q & x ∷ xs)) >>= f β‰‘βŸ¨βŸ©
    (p * q & x ∷ p β‹Š xs) >>= f β‰‘βŸ¨βŸ©
    ((p * q) β‹Š f x) βˆͺ ((p β‹Š xs) >>= f) β‰‘βŸ¨ cong (((p * q) β‹Š f x) βˆͺ_) P ⟩
    ((p * q) β‹Š f x) βˆͺ (p β‹Š (xs >>= f)) β‰‘βŸ¨ cong (_βˆͺ (p β‹Š (xs >>= f))) (*-assoc-β‹Š p q (f x)) ⟩
    (p β‹Š (q β‹Š f x)) βˆͺ (p β‹Š (xs >>= f)) β‰‘βŸ¨ β‹Š-distribΛ‘ p (q β‹Š f x) (xs >>= f) ⟩
    p β‹Š ((q & x ∷ xs) >>= f) ∎


module MonadLaws where
  lawΒΉ : (x : A) β†’ (f : A β†’ 𝒫 B)
       β†’ (pure x >>= f) ≑ f x
  lawΒΉ x f =
    pure x >>= f β‰‘βŸ¨βŸ©
    (1# & x ∷ []) >>= f β‰‘βŸ¨βŸ©
    1# β‹Š f x βˆͺ [] >>= f β‰‘βŸ¨βŸ©
    1# β‹Š f x βˆͺ [] β‰‘βŸ¨ βˆͺ-idΚ³ (1# β‹Š f x) ⟩
    1# β‹Š f x β‰‘βŸ¨ 1β‹Š (f x) ⟩
    f x ∎

  lawΒ² : (xs : 𝒫 A) β†’ xs >>= pure ≑ xs
  lawΒ² = ⟦ lawΒ²β€² βŸ§β‡“
    module Law1 where
    lawΒ²β€² : ⟦ xs βˆˆπ’« A β‡’ xs >>= pure ≑ xs ⟧
    ⟦ lawΒ²β€² ⟧-prop = trunc _ _
    ⟦ lawΒ²β€² ⟧[] = refl
    ⟦ lawΒ²β€² ⟧ p & x ∷ xs ⟨ P ⟩ =
      ((p & x ∷ xs) >>= pure) β‰‘βŸ¨βŸ©
      p β‹Š (pure x) βˆͺ (xs >>= pure) β‰‘βŸ¨βŸ©
      p β‹Š (1# & x ∷ []) βˆͺ (xs >>= pure) β‰‘βŸ¨βŸ©
      p * 1# & x ∷ [] βˆͺ (xs >>= pure) β‰‘βŸ¨βŸ©
      p * 1# & x ∷ (xs >>= pure) β‰‘βŸ¨ cong (_& x ∷ (xs >>= pure)) (*1 p) ⟩
      p & x ∷ xs >>= pure β‰‘βŸ¨ cong (p & x ∷_) P ⟩
      p & x ∷ xs ∎

  lawΒ³ : (xs : 𝒫 A) β†’ (f : A β†’ 𝒫 B) β†’ (g : B β†’ 𝒫 C)
       β†’ ((xs >>= f) >>= g) ≑ xs >>= (Ξ» x β†’ f x >>= g)
  lawΒ³ = Ξ» xs f g β†’ ⟦ lawΒ³β€² f g βŸ§β‡“ xs
    module Law3 where
    lawΒ³β€² : (f : A β†’ 𝒫 B) β†’ (g : B β†’ 𝒫 C) β†’ ⟦ xs βˆˆπ’« A β‡’ ((xs >>= f) >>= g) ≑ xs >>= (Ξ» x β†’ f x >>= g) ⟧
    ⟦ lawΒ³β€² f g ⟧-prop = trunc _ _
    ⟦ lawΒ³β€² f g ⟧[] = refl
    ⟦ lawΒ³β€² f g ⟧ p & x ∷ xs ⟨ P ⟩ =
      (((p & x ∷ xs) >>= f) >>= g) β‰‘βŸ¨βŸ©
      ((p β‹Š f x βˆͺ (xs >>= f)) >>= g) β‰‘βŸ¨ >>=-distrib (p β‹Š f x) (xs >>= f) g ⟩
      ((p β‹Š f x) >>= g) βˆͺ ((xs >>= f) >>= g) β‰‘βŸ¨ cong ((p β‹Š f x) >>= g βˆͺ_) P ⟩
      ((p β‹Š f x) >>= g) βˆͺ (xs >>= (Ξ» y β†’ f y >>= g)) β‰‘βŸ¨ cong (_βˆͺ (xs >>= (Ξ» y β†’ f y >>= g))) (β‹Š-assoc->>= p (f x) g) ⟩
      p β‹Š (f x >>= g) βˆͺ (xs >>= (Ξ» y β†’ f y >>= g)) β‰‘βŸ¨βŸ©
      ((p & x ∷ xs) >>= (Ξ» y β†’ f y >>= g)) ∎

open import Lists

fromListΒΉ : List A β†’ 𝒫 A
fromListΒΉ = foldr (Ξ» x xs β†’ 1# & x ∷ xs) []