Theory errorMonad

⊢ (∀v f. bind (return v) f = f v) ∧ ∀e f. bind (error e) f = error e

⊢ (∀v m. choice (return v) m = return v) ∧ ∀e m. choice (error e) m = m

⊢ ∀f1 f2. errorMAP f1 f2 = error_ABS ∘ SUM_MAP f1 f2 ∘ error_REP

⊢ errorREL =
  (λR1 R2 x y.
     ∃z. (∀p. p ∈ errorSET1 z ⇒ R1 (FST p) (SND p)) ∧
         (∀p. p ∈ errorSET2 z ⇒ R2 (FST p) (SND p)) ∧
         errorMAP FST FST z = x ∧ errorMAP SND SND z = y)

⊢ errorSET1 = S ($UNION ∘ BIMG $= ∘ setL) (BIMG (K ∅) ∘ setR) ∘ error_REP

⊢ errorSET2 = S ($UNION ∘ BIMG (K ∅) ∘ setL) (BIMG $= ∘ setR) ∘ error_REP

⊢ (∀a. error_ABS (error_REP a) = a) ∧
  ∀r. (λx. T) r ⇔ error_REP (error_ABS r) = r

⊢ error_CONS = error_ABS

⊢ ∃rep. TYPE_DEFINITION (λx. T) rep

⊢ (∀a0 f f0. error_CASE (return a0) f f0 = f a0) ∧
  ∀a0 f f0. error_CASE (error a0) f f0 = f0 a0

⊢ ∀f0 f1.
    (∀a0. error_size f0 f1 (return a0) = 1 + f0 a0) ∧
    ∀a0. error_size f0 f1 (error a0) = 1 + f1 a0

⊢ ∀e b. guard e b = if b then return () else error e

⊢ (∀v f. try (return v) f = return v) ∧ ∀e f. try (error e) f = f e

⊢ (∃e. P e) ⇔ (∃a. P (return a)) ∨ ∃e. P (error e)

⊢ (∀e. P e) ⇔ (∀a. P (return a)) ∧ ∀e. P (error e)

⊢ bind m f = error e ⇔ m = error e ∨ ∃u. m = return u ∧ f u = error e

⊢ bind m f = return v ⇔ ∃u. m = return u ∧ f u = return v

⊢ bind m return = m

⊢ DATATYPE (error return error)

⊢ (∀a0 a0'. return a0 = return a0' ⇔ a0 = a0') ∧
  ∀a0 a0'. error a0 = error a0' ⇔ a0 = a0'

⊢ ∀f0 f1. ∃h. (∀a0. h (return a0) = f0 a0) ∧ ∀a0. h (error a0) = f1 a0

⊢ ∀f1 f2 g1 g2 x.
    (∀a. a ∈ errorSET1 x ⇒ f1 a = g1 a) ∧
    (∀a. a ∈ errorSET2 x ⇒ f2 a = g2 a) ⇒
    errorMAP f1 f2 x = errorMAP g1 g2 x

⊢ errorMAP I I = I

⊢ ∀f1 f2 x. errorSET1 (errorMAP f1 f2 x) = IMAGE f1 (errorSET1 x)

⊢ ∀f1 f2 x. errorSET2 (errorMAP f1 f2 x) = IMAGE f2 (errorSET2 x)

⊢ errorMAP g1 g2 ∘ errorMAP f1 f2 = errorMAP (g1 ∘ f1) (g2 ∘ f2)

⊢ ∀x. cardleq (errorSET1 x) 𝕌(:num)

⊢ ∀x. cardleq (errorSET2 x) 𝕌(:num)

⊢ ∀M M' f f0.
    M = M' ∧ (∀a0. M' = return a0 ⇒ f a0 = f' a0) ∧
    (∀a0. M' = error a0 ⇒ f0 a0 = f0' a0) ⇒
    error_CASE M f f0 = error_CASE M' f' f0'

⊢ error_CASE x f f0 = v ⇔
  (∃a. x = return a ∧ f a = v) ∨ ∃e. x = error e ∧ f0 e = v

⊢ ∀a0' a0. return a0 ≠ error a0'

⊢ ∀P. (∀a. P (return a)) ∧ (∀e. P (error e)) ⇒ ∀e. P e

⊢ ∀a1. a1 ∈ errorSET1 ((λa1. error_ABS ((λa1. INL a1) a1)) a1)

⊢ ∀a2. a2 ∈ errorSET2 ((λa2. error_ABS ((λa2. INR a2) a2)) a2)

⊢ ∀ee. (∃a. ee = return a) ∨ ∃e. ee = error e

⊢ ∀a1 a2.
    errorSET1
      ((λa1 a2. error_ABS ((λa1 a2. (K ∘ INL) a1 ARB) a1 a2)) a1 a2) ⊆ {a1} ∧
    errorSET2
      ((λa1 a2. error_ABS ((λa1 a2. (K ∘ INL) a1 ARB) a1 a2)) a1 a2) ⊆ ∅

⊢ ∀a1 a2.
    errorSET1 ((λa1 a2. error_ABS ((λa1 a2. K INR ARB a2) a1 a2)) a1 a2) ⊆
    ∅ ∧
    errorSET2 ((λa1 a2. error_ABS ((λa1 a2. K INR ARB a2) a1 a2)) a1 a2) ⊆
    {a2}