text:
{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}

module Number.Operations.Details where

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Data.Unit.Base -- Unit
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
open import Function.Base using (_$_)

open import Cubical.Data.Nat.Properties
open import Cubical.Data.Nat.Order renaming (zero-≤ to z≤n; suc-≤-suc to s≤s)

open import MoreNatProperties renaming (0≤x to 0≤xⁿ)

open import Number.Postulates
open import Number.Structures
open import Number.Bundles
open import Number.Inclusions
open import Number.Base
open import Number.Coercions

open ℕⁿ
open ℤᶻ
open ℚᶠ
open ℝʳ
open ℂᶜ

infix  9 _⁻¹
infix  8 -_

open import Number.Operations.Specification

open PatternsProp

_⁻¹ : ∀{l p} → (x : Number (l , p)) → ⁻¹-Types x

_⁻¹ {isNat    } {⁇x⁇} (x ,, q) {{h}} = let r = Isℕ↪ℚ.preserves-#0 ℕ↪ℚinc _ h in _⁻¹ᶠ (ℕ↪ℚ x) {{r}} ,, ℚ.⁻¹-preserves-#0 _ r
_⁻¹ {isNat    } {x#0} (x ,, q) {{h}} = let r = Isℕ↪ℚ.preserves-#0 ℕ↪ℚinc _ q in _⁻¹ᶠ (ℕ↪ℚ x) {{r}} ,, ℚ.⁻¹-preserves-#0 _ r
_⁻¹ {isNat    } {0≤x} (x ,, q) {{h}} = let p = Isℕ↪ℚ.preserves-0< ℕ↪ℚinc _ (ℕ.≤-#-implies-< _ _ q (ℕ.#-sym _ _ h))
                                           r = Isℕ↪ℚ.preserves-#0 ℕ↪ℚinc _ h
                                       in  _⁻¹ᶠ (ℕ↪ℚ x) {{r}} ,, ℚ.⁻¹-preserves-0< _ p r
_⁻¹ {isNat    } {0<x} (x ,, q) {{h}} = let p = Isℕ↪ℚ.preserves-0< ℕ↪ℚinc _ q
                                           r = Isℕ↪ℚ.preserves-#0 ℕ↪ℚinc _ (ℕ.#-sym _ _ (ℕ.<-implies-# _ _ q))
                                       in  _⁻¹ᶠ (ℕ↪ℚ x) {{r}} ,, ℚ.⁻¹-preserves-0< _ p r
_⁻¹ {isNat    } {x≤0} (x ,, q) {{h}} = let p = Isℕ↪ℚ.preserves-<0 ℕ↪ℚinc _ (ℕ.≤-#-implies-< _ _ q h)
                                           r = Isℕ↪ℚ.preserves-#0 ℕ↪ℚinc _ h
                                       in  _⁻¹ᶠ (ℕ↪ℚ x) {{r}} ,, ℚ.⁻¹-preserves-<0 _ p r

_⁻¹ {isInt    } {⁇x⁇} (x ,, q) {{h}} = let r = Isℤ↪ℚ.preserves-#0 ℤ↪ℚinc _ h in _⁻¹ᶠ (ℤ↪ℚ x) {{r}} ,, ℚ.⁻¹-preserves-#0 _ r
_⁻¹ {isInt    } {x#0} (x ,, q) {{h}} = let r = Isℤ↪ℚ.preserves-#0 ℤ↪ℚinc _ q in _⁻¹ᶠ (ℤ↪ℚ x) {{r}} ,, ℚ.⁻¹-preserves-#0 _ r
_⁻¹ {isInt    } {0≤x} (x ,, q) {{h}} = let p = Isℤ↪ℚ.preserves-0< ℤ↪ℚinc _ (ℤ.≤-#-implies-< _ _ q (ℤ.#-sym _ _ h))
                                           r = Isℤ↪ℚ.preserves-#0 ℤ↪ℚinc _ h
                                       in  _⁻¹ᶠ (ℤ↪ℚ x) {{r}} ,, ℚ.⁻¹-preserves-0< _ p r
_⁻¹ {isInt    } {0<x} (x ,, q) {{h}} = let p = Isℤ↪ℚ.preserves-0< ℤ↪ℚinc _ q
                                           r = Isℤ↪ℚ.preserves-#0 ℤ↪ℚinc _ (ℤ.#-sym _ _ (ℤ.<-implies-# _ _ q))
                                       in  _⁻¹ᶠ (ℤ↪ℚ x) {{r}} ,, ℚ.⁻¹-preserves-0< _ p r
_⁻¹ {isInt    } {x<0} (x ,, q) {{h}} = let p = Isℤ↪ℚ.preserves-<0 ℤ↪ℚinc _ q
                                           r = Isℤ↪ℚ.preserves-#0 ℤ↪ℚinc _ (ℤ.<-implies-# _ _ q)
                                       in  _⁻¹ᶠ (ℤ↪ℚ x) {{r}} ,,  ℚ.⁻¹-preserves-<0 _ p r
_⁻¹ {isInt    } {x≤0} (x ,, q) {{h}} = let p = Isℤ↪ℚ.preserves-<0 ℤ↪ℚinc _ (ℤ.≤-#-implies-< _ _ q h)
                                           r = Isℤ↪ℚ.preserves-#0 ℤ↪ℚinc _ h
                                       in  _⁻¹ᶠ (ℤ↪ℚ x) {{r}} ,, ℚ.⁻¹-preserves-<0 _ p r

_⁻¹ {isRat    } {⁇x⁇} (x ,, q) {{h}} =  _⁻¹ᶠ x  {{h}} ,, ℚ.⁻¹-preserves-#0 x h
_⁻¹ {isRat    } {x#0} (x ,, q) {{h}} =  _⁻¹ᶠ x  {{q}} ,, ℚ.⁻¹-preserves-#0 x q
_⁻¹ {isRat    } {0≤x} (x ,, q) {{h}} =  _⁻¹ᶠ x  {{h}} ,, ℚ.⁻¹-preserves-0< x (ℚ.≤-#-implies-< _ _ q (ℚ.#-sym _ _ h)) h
_⁻¹ {isRat    } {0<x} (x ,, q) {{h}} = let r = ℚ.#-sym _ _ (ℚ.<-implies-# _ _ q) in _⁻¹ᶠ x  {{r}} ,,  ℚ.⁻¹-preserves-0< _ q r
_⁻¹ {isRat    } {x<0} (x ,, q) {{h}} = let r = ℚ.<-implies-# _ _ q in _⁻¹ᶠ x  {{r}} ,, ℚ.⁻¹-preserves-<0 _ q r
_⁻¹ {isRat    } {x≤0} (x ,, q) {{h}} =  _⁻¹ᶠ x  {{h}} ,,  ℚ.⁻¹-preserves-<0 x (ℚ.≤-#-implies-< _ _ q h) h

_⁻¹ {isReal   } {⁇x⁇} (x ,, q) {{h}} =  _⁻¹ʳ x  {{h}} ,, ℝ.⁻¹-preserves-#0 x h
_⁻¹ {isReal   } {x#0} (x ,, q) {{h}} =  _⁻¹ʳ x  {{q}} ,, ℝ.⁻¹-preserves-#0 x q
_⁻¹ {isReal   } {0≤x} (x ,, q) {{h}} =  _⁻¹ʳ x  {{h}} ,, ℝ.⁻¹-preserves-0< x (ℝ.≤-#-implies-< _ _ q (ℝ.#-sym _ _ h)) h
_⁻¹ {isReal   } {0<x} (x ,, q) {{h}} = let r = ℝ.#-sym _ _ (ℝ.<-implies-# _ _ q) in _⁻¹ʳ x {{r}} ,,  ℝ.⁻¹-preserves-0< _ q r
_⁻¹ {isReal   } {x<0} (x ,, q) {{h}} = let r = ℝ.<-implies-# _ _ q in _⁻¹ʳ x  {{r}} ,, ℝ.⁻¹-preserves-<0 _ q r
_⁻¹ {isReal   } {x≤0} (x ,, q) {{h}} =  _⁻¹ʳ      x  {{h}} ,, ℝ.⁻¹-preserves-<0 x (ℝ.≤-#-implies-< _ _ q h) h

_⁻¹ {isComplex} {⁇x⁇} (x ,, q) {{h}} =  _⁻¹ᶜ      x  {{h}} ,, ℂ.⁻¹-preserves-#0 x h
_⁻¹ {isComplex} {x#0} (x ,, q) {{h}} =  _⁻¹ᶜ      x  {{q}} ,, ℂ.⁻¹-preserves-#0 x q

-_ : ∀{l p} → (x : Number (l , p)) → -Types x
-_ {isNat    } {⁇x⁇} (x ,, p) = (-ᶻ (ℕ↪ℤ x)) ,, (ℤ.-flips-0≤ _ $ Isℕ↪ℤ.preserves-0≤ ℕ↪ℤinc _ (0≤xⁿ x))
-_ {isNat    } {x#0} (x ,, p) = (-ᶻ (ℕ↪ℤ x)) ,, (ℤ.-preserves-#0 _ $ Isℕ↪ℤ.preserves-#0 ℕ↪ℤinc _ p)
-_ {isNat    } {0≤x} (x ,, p) = (-ᶻ (ℕ↪ℤ x)) ,, (ℤ.-flips-0≤ _ $ Isℕ↪ℤ.preserves-0≤ ℕ↪ℤinc _ p)
-_ {isNat    } {0<x} (x ,, p) = (-ᶻ (ℕ↪ℤ x)) ,, (ℤ.-flips-0< _ $ Isℕ↪ℤ.preserves-0< ℕ↪ℤinc _ p)
-_ {isNat    } {x≤0} (x ,, p) = (-ᶻ (ℕ↪ℤ x)) ,, (ℤ.-flips-≤0 _ $ Isℕ↪ℤ.preserves-≤0 ℕ↪ℤinc _ p)
-_ {isInt    } {⁇x⁇} (x ,, p) = (-ᶻ      x ) ,, lift tt
-_ {isInt    } {x#0} (x ,, p) = (-ᶻ      x ) ,, ℤ.-preserves-#0 _ p
-_ {isInt    } {0≤x} (x ,, p) = (-ᶻ      x ) ,, ℤ.-flips-0≤ _ p
-_ {isInt    } {0<x} (x ,, p) = (-ᶻ      x ) ,, ℤ.-flips-0< _ p
-_ {isInt    } {x<0} (x ,, p) = (-ᶻ      x ) ,, ℤ.-flips-<0 _ p
-_ {isInt    } {x≤0} (x ,, p) = (-ᶻ      x ) ,, ℤ.-flips-≤0 _ p
-_ {isRat    } {⁇x⁇} (x ,, p) = (-ᶠ      x ) ,, lift tt
-_ {isRat    } {x#0} (x ,, p) = (-ᶠ      x ) ,, ℚ.-preserves-#0 _ p
-_ {isRat    } {0≤x} (x ,, p) = (-ᶠ      x ) ,, ℚ.-flips-0≤ _ p
-_ {isRat    } {0<x} (x ,, p) = (-ᶠ      x ) ,, ℚ.-flips-0< _ p
-_ {isRat    } {x<0} (x ,, p) = (-ᶠ      x ) ,, ℚ.-flips-<0 _ p
-_ {isRat    } {x≤0} (x ,, p) = (-ᶠ      x ) ,, ℚ.-flips-≤0 _ p
-_ {isReal   } {⁇x⁇} (x ,, p) = (-ʳ      x ) ,, lift tt
-_ {isReal   } {x#0} (x ,, p) = (-ʳ      x ) ,, ℝ.-preserves-#0 _ p
-_ {isReal   } {0≤x} (x ,, p) = (-ʳ      x ) ,, ℝ.-flips-0≤ _ p
-_ {isReal   } {0<x} (x ,, p) = (-ʳ      x ) ,, ℝ.-flips-0< _ p
-_ {isReal   } {x<0} (x ,, p) = (-ʳ      x ) ,, ℝ.-flips-<0 _ p
-_ {isReal   } {x≤0} (x ,, p) = (-ʳ      x ) ,, ℝ.-flips-≤0 _ p
-_ {isComplex} {⁇x⁇} (x ,, p) = (-ᶜ      x ) ,, lift tt
-_ {isComplex} {x#0} (x ,, p) = (-ᶜ      x ) ,, ℂ.-preserves-#0 _ p

_+ʰⁿ_ : ∀{p q} → (x : Number (isNat , p)) → (y : Number (isNat , q)) → PositivityKindInterpretation isNat (+-Positivityʰ isNat p q) (num x +ⁿ num y)
_+ʰⁿ_ {⁇x⁇} {⁇x⁇} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {⁇x⁇} {x#0} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {⁇x⁇} {0≤x} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {⁇x⁇} {0<x} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {⁇x⁇} {x≤0} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {x#0} {⁇x⁇} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {x#0} {x#0} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {x#0} {0≤x} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {x#0} {0<x} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {x#0} {x≤0} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {0≤x} {⁇x⁇} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {0≤x} {x#0} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {0≤x} {0≤x} (a ,, pa) (b ,, pb) = ℕ.+-0≤-0≤-implies-0≤ a b pa pb -- 0 ≤ a → 0 ≤ b → 0 ≤ a + b
_+ʰⁿ_ {0≤x} {0<x} (a ,, pa) (b ,, pb) = ℕ.+-0≤-0<-implies-0< a b pa pb -- 0 ≤ a → 0 < b → 0 < a + b
_+ʰⁿ_ {0≤x} {x≤0} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {0<x} {⁇x⁇} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {0<x} {x#0} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {0<x} {0≤x} (a ,, pa) (b ,, pb) = ℕ.+-0<-0≤-implies-0< a b pa pb -- 0 < a → 0 ≤ b → 0 < a + b
_+ʰⁿ_ {0<x} {0<x} (a ,, pa) (b ,, pb) = ℕ.+-0<-0<-implies-0< a b pa pb -- 0 < a → 0 < b → 0 < a + b
_+ʰⁿ_ {0<x} {x≤0} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {x≤0} {⁇x⁇} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {x≤0} {x#0} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {x≤0} {0≤x} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {x≤0} {0<x} (a ,, pa) (b ,, pb) = tt
_+ʰⁿ_ {x≤0} {x≤0} (a ,, pa) (b ,, pb) = ℕ.+-≤0-≤0-implies-≤0 a b pa pb -- a ≤ 0 → b ≤ 0 → (a + b) ≤ 0

_+ʰᶻ_ : ∀{p q} → (x : Number (isInt , p)) → (y : Number (isInt , q)) → PositivityKindInterpretation isInt (+-Positivityʰ isInt p q) (num x +ᶻ num y)
_+ʰᶻ_ {⁇x⁇} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {⁇x⁇} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {⁇x⁇} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {⁇x⁇} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {⁇x⁇} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {⁇x⁇} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x#0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x#0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x#0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x#0} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x#0} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x#0} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {0≤x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {0≤x} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {0≤x} {0≤x} (a ,, pa) (b ,, pb) = ℤ.+-0≤-0≤-implies-0≤ a b pa pb -- 0 ≤ a → 0 ≤ b → 0 ≤ a + b
_+ʰᶻ_ {0≤x} {0<x} (a ,, pa) (b ,, pb) = ℤ.+-0≤-0<-implies-0< a b pa pb -- 0 ≤ a → 0 < b → 0 < a + b
_+ʰᶻ_ {0≤x} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {0≤x} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {0<x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {0<x} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {0<x} {0≤x} (a ,, pa) (b ,, pb) = ℤ.+-0<-0≤-implies-0< a b pa pb -- 0 < a → 0 ≤ b → 0 < a + b
_+ʰᶻ_ {0<x} {0<x} (a ,, pa) (b ,, pb) = ℤ.+-0<-0<-implies-0< a b pa pb -- 0 < a → 0 < b → 0 < a + b
_+ʰᶻ_ {0<x} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {0<x} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x<0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x<0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x<0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x<0} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x<0} {x<0} (a ,, pa) (b ,, pb) = ℤ.+-<0-<0-implies-<0 a b pa pb -- a < 0 → b < 0 → (a + b) < 0
_+ʰᶻ_ {x<0} {x≤0} (a ,, pa) (b ,, pb) = ℤ.+-<0-≤0-implies-<0 a b pa pb -- a < 0 → b ≤ 0 → (a + b) < 0
_+ʰᶻ_ {x≤0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x≤0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x≤0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x≤0} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶻ_ {x≤0} {x<0} (a ,, pa) (b ,, pb) = ℤ.+-≤0-<0-implies-<0 a b pa pb -- a ≤ 0 → b < 0 → (a + b) < 0
_+ʰᶻ_ {x≤0} {x≤0} (a ,, pa) (b ,, pb) = ℤ.+-≤0-≤0-implies-≤0 a b pa pb -- a ≤ 0 → b ≤ 0 → (a + b) ≤ 0

_+ʰᶠ_ : ∀{p q} → (x : Number (isRat , p)) → (y : Number (isRat , q)) → PositivityKindInterpretation isRat (+-Positivityʰ isRat p q) (num x +ᶠ num y)
_+ʰᶠ_ {⁇x⁇} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {⁇x⁇} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {⁇x⁇} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {⁇x⁇} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {⁇x⁇} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {⁇x⁇} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x#0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x#0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x#0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x#0} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x#0} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x#0} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {0≤x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {0≤x} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {0≤x} {0≤x} (a ,, pa) (b ,, pb) = ℚ.+-0≤-0≤-implies-0≤ a b pa pb -- 0 ≤ a → 0 ≤ b → 0 ≤ a + b
_+ʰᶠ_ {0≤x} {0<x} (a ,, pa) (b ,, pb) = ℚ.+-0≤-0<-implies-0< a b pa pb -- 0 ≤ a → 0 < b → 0 < a + b
_+ʰᶠ_ {0≤x} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {0≤x} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {0<x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {0<x} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {0<x} {0≤x} (a ,, pa) (b ,, pb) = ℚ.+-0<-0≤-implies-0< a b pa pb -- 0 < a → 0 ≤ b → 0 < a + b
_+ʰᶠ_ {0<x} {0<x} (a ,, pa) (b ,, pb) = ℚ.+-0<-0<-implies-0< a b pa pb -- 0 < a → 0 < b → 0 < a + b
_+ʰᶠ_ {0<x} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {0<x} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x<0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x<0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x<0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x<0} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x<0} {x<0} (a ,, pa) (b ,, pb) = ℚ.+-<0-<0-implies-<0 a b pa pb -- a < 0 → b < 0 → (a + b) < 0
_+ʰᶠ_ {x<0} {x≤0} (a ,, pa) (b ,, pb) = ℚ.+-<0-≤0-implies-<0 a b pa pb -- a < 0 → b ≤ 0 → (a + b) < 0
_+ʰᶠ_ {x≤0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x≤0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x≤0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x≤0} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰᶠ_ {x≤0} {x<0} (a ,, pa) (b ,, pb) = ℚ.+-≤0-<0-implies-<0 a b pa pb -- a ≤ 0 → b < 0 → (a + b) < 0
_+ʰᶠ_ {x≤0} {x≤0} (a ,, pa) (b ,, pb) = ℚ.+-≤0-≤0-implies-≤0 a b pa pb -- a ≤ 0 → b ≤ 0 → (a + b) ≤ 0

_+ʰʳ_ : ∀{p q} → (x : Number (isReal , p)) → (y : Number (isReal , q)) → PositivityKindInterpretation isReal (+-Positivityʰ isReal p q) (num x +ʳ num y)
_+ʰʳ_ {⁇x⁇} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {⁇x⁇} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {⁇x⁇} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {⁇x⁇} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {⁇x⁇} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {⁇x⁇} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x#0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x#0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x#0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x#0} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x#0} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x#0} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {0≤x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {0≤x} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {0≤x} {0≤x} (a ,, pa) (b ,, pb) = ℝ.+-0≤-0≤-implies-0≤ a b pa pb -- 0 ≤ a → 0 ≤ b → 0 ≤ a + b
_+ʰʳ_ {0≤x} {0<x} (a ,, pa) (b ,, pb) = ℝ.+-0≤-0<-implies-0< a b pa pb -- 0 ≤ a → 0 < b → 0 < a + b
_+ʰʳ_ {0≤x} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {0≤x} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {0<x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {0<x} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {0<x} {0≤x} (a ,, pa) (b ,, pb) = ℝ.+-0<-0≤-implies-0< a b pa pb -- 0 < a → 0 ≤ b → 0 < a + b
_+ʰʳ_ {0<x} {0<x} (a ,, pa) (b ,, pb) = ℝ.+-0<-0<-implies-0< a b pa pb -- 0 < a → 0 < b → 0 < a + b
_+ʰʳ_ {0<x} {x<0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {0<x} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x<0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x<0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x<0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x<0} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x<0} {x<0} (a ,, pa) (b ,, pb) = ℝ.+-<0-<0-implies-<0 a b pa pb -- a < 0 → b < 0 → (a + b) < 0
_+ʰʳ_ {x<0} {x≤0} (a ,, pa) (b ,, pb) = ℝ.+-<0-≤0-implies-<0 a b pa pb -- a < 0 → b ≤ 0 → (a + b) < 0
_+ʰʳ_ {x≤0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x≤0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x≤0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x≤0} {0<x} (a ,, pa) (b ,, pb) = lift tt
_+ʰʳ_ {x≤0} {x<0} (a ,, pa) (b ,, pb) = ℝ.+-≤0-<0-implies-<0 a b pa pb -- a ≤ 0 → b < 0 → (a + b) < 0
_+ʰʳ_ {x≤0} {x≤0} (a ,, pa) (b ,, pb) = ℝ.+-≤0-≤0-implies-≤0 a b pa pb -- a ≤ 0 → b ≤ 0 → (a + b) ≤ 0

_+ʰᶜ_ : ∀{p q} → (x : Number (isComplex , p)) → (y : Number (isComplex , q)) → PositivityKindInterpretation isComplex (+-Positivityʰ isComplex p q) (num x +ᶜ num y)
_+ʰᶜ_ x y = lift tt

_·ʰⁿ_ : ∀{p q} → (x : Number (isNat , p)) → (y : Number (isNat , q)) → PositivityKindInterpretation isNat (·-Positivityʰ isNat p q) (num x ·ⁿ num y)
_·ʰⁿ_ {⁇x⁇} {⁇x⁇} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {⁇x⁇} {x#0} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {⁇x⁇} {0≤x} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {⁇x⁇} {0<x} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {⁇x⁇} {x≤0} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {x#0} {⁇x⁇} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {x#0} {x#0} (a ,, pa) (b ,, pb) = ℕ.·-#0-#0-implies-#0 a b pa pb -- a # 0 → b # 0 → (a · b) # 0
_·ʰⁿ_ {x#0} {0≤x} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {x#0} {0<x} (a ,, pa) (b ,, pb) = ℕ.·-#0-0<-implies-#0 a b pa pb -- a # 0 → 0 < b → (a · b) # 0
_·ʰⁿ_ {x#0} {x≤0} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {0≤x} {⁇x⁇} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {0≤x} {x#0} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {0≤x} {0≤x} (a ,, pa) (b ,, pb) = ℕ.·-0≤-0≤-implies-0≤ a b pa pb -- 0 ≤ a → 0 ≤ b → 0 ≤ (a · b)
_·ʰⁿ_ {0≤x} {0<x} (a ,, pa) (b ,, pb) = ℕ.·-0≤-0<-implies-0≤ a b pa pb -- 0 ≤ a → 0 < b → 0 ≤ (a · b)
_·ʰⁿ_ {0≤x} {x≤0} (a ,, pa) (b ,, pb) = ℕ.·-0≤-≤0-implies-≤0 a b pa pb -- 0 ≤ a → b ≤ 0 → (a · b) ≤ 0
_·ʰⁿ_ {0<x} {⁇x⁇} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {0<x} {x#0} (a ,, pa) (b ,, pb) = ℕ.·-0<-#0-implies-#0 a b pa pb -- 0 < a → b # 0 → (a · b) # 0
_·ʰⁿ_ {0<x} {0≤x} (a ,, pa) (b ,, pb) = ℕ.·-0<-0≤-implies-0≤ a b pa pb -- 0 < a → 0 ≤ b → 0 ≤ (a · b)
_·ʰⁿ_ {0<x} {0<x} (a ,, pa) (b ,, pb) = ℕ.·-0<-0<-implies-0< a b pa pb -- 0 < a → 0 < b → 0 < (a · b)
_·ʰⁿ_ {0<x} {x≤0} (a ,, pa) (b ,, pb) = ℕ.·-0<-≤0-implies-≤0 a b pa pb -- 0 < a → b ≤ 0 → (a · b) ≤ 0
_·ʰⁿ_ {x≤0} {⁇x⁇} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {x≤0} {x#0} (a ,, pa) (b ,, pb) = tt
_·ʰⁿ_ {x≤0} {0≤x} (a ,, pa) (b ,, pb) = ℕ.·-≤0-0≤-implies-≤0 a b pa pb -- a ≤ 0 → 0 ≤ b → (a · b) ≤ 0
_·ʰⁿ_ {x≤0} {0<x} (a ,, pa) (b ,, pb) = ℕ.·-≤0-0<-implies-≤0 a b pa pb -- a ≤ 0 → 0 < b → (a · b) ≤ 0
_·ʰⁿ_ {x≤0} {x≤0} (a ,, pa) (b ,, pb) = ℕ.·-≤0-≤0-implies-0≤ a b pa pb -- a ≤ 0 → b ≤ 0 → 0 ≤ (a · b)

_·ʰᶻ_ : ∀{p q} → (x : Number (isInt , p)) → (y : Number (isInt , q)) → PositivityKindInterpretation isInt (·-Positivityʰ isInt p q) (num x ·ᶻ num y)
_·ʰᶻ_ {⁇x⁇} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {⁇x⁇} {x#0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {⁇x⁇} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {⁇x⁇} {0<x} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {⁇x⁇} {x<0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {⁇x⁇} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {x#0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {x#0} {x#0} (a ,, pa) (b ,, pb) = ℤ.·-#0-#0-implies-#0 a b pa pb -- a # 0 → b # 0 → (a · b) # 0
_·ʰᶻ_ {x#0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {x#0} {0<x} (a ,, pa) (b ,, pb) = ℤ.·-#0-0<-implies-#0 a b pa pb -- a # 0 → 0 < b → (a · b) # 0
_·ʰᶻ_ {x#0} {x<0} (a ,, pa) (b ,, pb) = ℤ.·-#0-<0-implies-#0 a b pa pb -- a # 0 → b < 0 → (a · b) # 0
_·ʰᶻ_ {x#0} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {0≤x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {0≤x} {x#0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {0≤x} {0≤x} (a ,, pa) (b ,, pb) = ℤ.·-0≤-0≤-implies-0≤ a b pa pb -- 0 ≤ a → 0 ≤ b → 0 ≤ (a · b)
_·ʰᶻ_ {0≤x} {0<x} (a ,, pa) (b ,, pb) = ℤ.·-0≤-0<-implies-0≤ a b pa pb -- 0 ≤ a → 0 < b → 0 ≤ (a · b)
_·ʰᶻ_ {0≤x} {x<0} (a ,, pa) (b ,, pb) = ℤ.·-0≤-<0-implies-≤0 a b pa pb -- 0 ≤ a → b < 0 → (a · b) ≤ 0
_·ʰᶻ_ {0≤x} {x≤0} (a ,, pa) (b ,, pb) = ℤ.·-0≤-≤0-implies-≤0 a b pa pb -- 0 ≤ a → b ≤ 0 → (a · b) ≤ 0
_·ʰᶻ_ {0<x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {0<x} {x#0} (a ,, pa) (b ,, pb) = ℤ.·-0<-#0-implies-#0 a b pa pb -- 0 < a → b # 0 → (a · b) # 0
_·ʰᶻ_ {0<x} {0≤x} (a ,, pa) (b ,, pb) = ℤ.·-0<-0≤-implies-0≤ a b pa pb -- 0 < a → 0 ≤ b → 0 ≤ (a · b)
_·ʰᶻ_ {0<x} {0<x} (a ,, pa) (b ,, pb) = ℤ.·-0<-0<-implies-0< a b pa pb -- 0 < a → 0 < b → 0 < (a · b)
_·ʰᶻ_ {0<x} {x<0} (a ,, pa) (b ,, pb) = ℤ.·-0<-<0-implies-<0 a b pa pb -- 0 < a → b < 0 → (a · b) < 0
_·ʰᶻ_ {0<x} {x≤0} (a ,, pa) (b ,, pb) = ℤ.·-0<-≤0-implies-≤0 a b pa pb -- 0 < a → b ≤ 0 → (a · b) ≤ 0
_·ʰᶻ_ {x<0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {x<0} {x#0} (a ,, pa) (b ,, pb) = ℤ.·-<0-#0-implies-#0 a b pa pb -- a < 0 → b # 0 → (a · b) # 0
_·ʰᶻ_ {x<0} {0≤x} (a ,, pa) (b ,, pb) = ℤ.·-<0-0≤-implies-≤0 a b pa pb -- a < 0 → 0 ≤ b → (a · b) ≤ 0
_·ʰᶻ_ {x<0} {0<x} (a ,, pa) (b ,, pb) = ℤ.·-<0-0<-implies-<0 a b pa pb -- a < 0 → 0 < b → (a · b) < 0
_·ʰᶻ_ {x<0} {x<0} (a ,, pa) (b ,, pb) = ℤ.·-<0-<0-implies-0< a b pa pb -- a < 0 → b < 0 → 0 < (a · b)
_·ʰᶻ_ {x<0} {x≤0} (a ,, pa) (b ,, pb) = ℤ.·-<0-≤0-implies-0≤ a b pa pb -- a < 0 → b ≤ 0 → 0 ≤ (a · b)
_·ʰᶻ_ {x≤0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {x≤0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶻ_ {x≤0} {0≤x} (a ,, pa) (b ,, pb) = ℤ.·-≤0-0≤-implies-≤0 a b pa pb -- a ≤ 0 → 0 ≤ b → (a · b) ≤ 0
_·ʰᶻ_ {x≤0} {0<x} (a ,, pa) (b ,, pb) = ℤ.·-≤0-0<-implies-≤0 a b pa pb -- a ≤ 0 → 0 < b → (a · b) ≤ 0
_·ʰᶻ_ {x≤0} {x<0} (a ,, pa) (b ,, pb) = ℤ.·-≤0-<0-implies-0≤ a b pa pb -- a ≤ 0 → b < 0 → 0 ≤ (a · b)
_·ʰᶻ_ {x≤0} {x≤0} (a ,, pa) (b ,, pb) = ℤ.·-≤0-≤0-implies-0≤ a b pa pb -- a ≤ 0 → b ≤ 0 → 0 ≤ (a · b)

_·ʰᶠ_ : ∀{p q} → (x : Number (isRat , p)) → (y : Number (isRat , q)) → PositivityKindInterpretation isRat (·-Positivityʰ isRat p q) (num x ·ᶠ num y)
_·ʰᶠ_ {⁇x⁇} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {⁇x⁇} {x#0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {⁇x⁇} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {⁇x⁇} {0<x} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {⁇x⁇} {x<0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {⁇x⁇} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {x#0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {x#0} {x#0} (a ,, pa) (b ,, pb) = ℚ.·-#0-#0-implies-#0 a b pa pb -- a # 0 → b # 0 → (a · b) # 0
_·ʰᶠ_ {x#0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {x#0} {0<x} (a ,, pa) (b ,, pb) = ℚ.·-#0-0<-implies-#0 a b pa pb -- a # 0 → 0 < b → (a · b) # 0
_·ʰᶠ_ {x#0} {x<0} (a ,, pa) (b ,, pb) = ℚ.·-#0-<0-implies-#0 a b pa pb -- a # 0 → b < 0 → (a · b) # 0
_·ʰᶠ_ {x#0} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {0≤x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {0≤x} {x#0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {0≤x} {0≤x} (a ,, pa) (b ,, pb) = ℚ.·-0≤-0≤-implies-0≤ a b pa pb -- 0 ≤ a → 0 ≤ b → 0 ≤ (a · b)
_·ʰᶠ_ {0≤x} {0<x} (a ,, pa) (b ,, pb) = ℚ.·-0≤-0<-implies-0≤ a b pa pb -- 0 ≤ a → 0 < b → 0 ≤ (a · b)
_·ʰᶠ_ {0≤x} {x<0} (a ,, pa) (b ,, pb) = ℚ.·-0≤-<0-implies-≤0 a b pa pb -- 0 ≤ a → b < 0 → (a · b) ≤ 0
_·ʰᶠ_ {0≤x} {x≤0} (a ,, pa) (b ,, pb) = ℚ.·-0≤-≤0-implies-≤0 a b pa pb -- 0 ≤ a → b ≤ 0 → (a · b) ≤ 0
_·ʰᶠ_ {0<x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {0<x} {x#0} (a ,, pa) (b ,, pb) = ℚ.·-0<-#0-implies-#0 a b pa pb -- 0 < a → b # 0 → (a · b) # 0
_·ʰᶠ_ {0<x} {0≤x} (a ,, pa) (b ,, pb) = ℚ.·-0<-0≤-implies-0≤ a b pa pb -- 0 < a → 0 ≤ b → 0 ≤ (a · b)
_·ʰᶠ_ {0<x} {0<x} (a ,, pa) (b ,, pb) = ℚ.·-0<-0<-implies-0< a b pa pb -- 0 < a → 0 < b → 0 < (a · b)
_·ʰᶠ_ {0<x} {x<0} (a ,, pa) (b ,, pb) = ℚ.·-0<-<0-implies-<0 a b pa pb -- 0 < a → b < 0 → (a · b) < 0
_·ʰᶠ_ {0<x} {x≤0} (a ,, pa) (b ,, pb) = ℚ.·-0<-≤0-implies-≤0 a b pa pb -- 0 < a → b ≤ 0 → (a · b) ≤ 0
_·ʰᶠ_ {x<0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {x<0} {x#0} (a ,, pa) (b ,, pb) = ℚ.·-<0-#0-implies-#0 a b pa pb -- a < 0 → b # 0 → (a · b) # 0
_·ʰᶠ_ {x<0} {0≤x} (a ,, pa) (b ,, pb) = ℚ.·-<0-0≤-implies-≤0 a b pa pb -- a < 0 → 0 ≤ b → (a · b) ≤ 0
_·ʰᶠ_ {x<0} {0<x} (a ,, pa) (b ,, pb) = ℚ.·-<0-0<-implies-<0 a b pa pb -- a < 0 → 0 < b → (a · b) < 0
_·ʰᶠ_ {x<0} {x<0} (a ,, pa) (b ,, pb) = ℚ.·-<0-<0-implies-0< a b pa pb -- a < 0 → b < 0 → 0 < (a · b)
_·ʰᶠ_ {x<0} {x≤0} (a ,, pa) (b ,, pb) = ℚ.·-<0-≤0-implies-0≤ a b pa pb -- a < 0 → b ≤ 0 → 0 ≤ (a · b)
_·ʰᶠ_ {x≤0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {x≤0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶠ_ {x≤0} {0≤x} (a ,, pa) (b ,, pb) = ℚ.·-≤0-0≤-implies-≤0 a b pa pb -- a ≤ 0 → 0 ≤ b → (a · b) ≤ 0
_·ʰᶠ_ {x≤0} {0<x} (a ,, pa) (b ,, pb) = ℚ.·-≤0-0<-implies-≤0 a b pa pb -- a ≤ 0 → 0 < b → (a · b) ≤ 0
_·ʰᶠ_ {x≤0} {x<0} (a ,, pa) (b ,, pb) = ℚ.·-≤0-<0-implies-0≤ a b pa pb -- a ≤ 0 → b < 0 → 0 ≤ (a · b)
_·ʰᶠ_ {x≤0} {x≤0} (a ,, pa) (b ,, pb) = ℚ.·-≤0-≤0-implies-0≤ a b pa pb -- a ≤ 0 → b ≤ 0 → 0 ≤ (a · b)

_·ʰʳ_ : ∀{p q} → (x : Number (isReal , p)) → (y : Number (isReal , q)) → PositivityKindInterpretation isReal (·-Positivityʰ isReal p q) (num x ·ʳ num y)
_·ʰʳ_ {⁇x⁇} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {⁇x⁇} {x#0} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {⁇x⁇} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {⁇x⁇} {0<x} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {⁇x⁇} {x<0} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {⁇x⁇} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {x#0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {x#0} {x#0} (a ,, pa) (b ,, pb) = ℝ.·-#0-#0-implies-#0 a b pa pb -- a # 0 → b # 0 → (a · b) # 0
_·ʰʳ_ {x#0} {0≤x} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {x#0} {0<x} (a ,, pa) (b ,, pb) = ℝ.·-#0-0<-implies-#0 a b pa pb -- a # 0 → 0 < b → (a · b) # 0
_·ʰʳ_ {x#0} {x<0} (a ,, pa) (b ,, pb) = ℝ.·-#0-<0-implies-#0 a b pa pb -- a # 0 → b < 0 → (a · b) # 0
_·ʰʳ_ {x#0} {x≤0} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {0≤x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {0≤x} {x#0} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {0≤x} {0≤x} (a ,, pa) (b ,, pb) = ℝ.·-0≤-0≤-implies-0≤ a b pa pb -- 0 ≤ a → 0 ≤ b → 0 ≤ (a · b)
_·ʰʳ_ {0≤x} {0<x} (a ,, pa) (b ,, pb) = ℝ.·-0≤-0<-implies-0≤ a b pa pb -- 0 ≤ a → 0 < b → 0 ≤ (a · b)
_·ʰʳ_ {0≤x} {x<0} (a ,, pa) (b ,, pb) = ℝ.·-0≤-<0-implies-≤0 a b pa pb -- 0 ≤ a → b < 0 → (a · b) ≤ 0
_·ʰʳ_ {0≤x} {x≤0} (a ,, pa) (b ,, pb) = ℝ.·-0≤-≤0-implies-≤0 a b pa pb -- 0 ≤ a → b ≤ 0 → (a · b) ≤ 0
_·ʰʳ_ {0<x} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {0<x} {x#0} (a ,, pa) (b ,, pb) = ℝ.·-0<-#0-implies-#0 a b pa pb -- 0 < a → b # 0 → (a · b) # 0
_·ʰʳ_ {0<x} {0≤x} (a ,, pa) (b ,, pb) = ℝ.·-0<-0≤-implies-0≤ a b pa pb -- 0 < a → 0 ≤ b → 0 ≤ (a · b)
_·ʰʳ_ {0<x} {0<x} (a ,, pa) (b ,, pb) = ℝ.·-0<-0<-implies-0< a b pa pb -- 0 < a → 0 < b → 0 < (a · b)
_·ʰʳ_ {0<x} {x<0} (a ,, pa) (b ,, pb) = ℝ.·-0<-<0-implies-<0 a b pa pb -- 0 < a → b < 0 → (a · b) < 0
_·ʰʳ_ {0<x} {x≤0} (a ,, pa) (b ,, pb) = ℝ.·-0<-≤0-implies-≤0 a b pa pb -- 0 < a → b ≤ 0 → (a · b) ≤ 0
_·ʰʳ_ {x<0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {x<0} {x#0} (a ,, pa) (b ,, pb) = ℝ.·-<0-#0-implies-#0 a b pa pb -- a < 0 → b # 0 → (a · b) # 0
_·ʰʳ_ {x<0} {0≤x} (a ,, pa) (b ,, pb) = ℝ.·-<0-0≤-implies-≤0 a b pa pb -- a < 0 → 0 ≤ b → (a · b) ≤ 0
_·ʰʳ_ {x<0} {0<x} (a ,, pa) (b ,, pb) = ℝ.·-<0-0<-implies-<0 a b pa pb -- a < 0 → 0 < b → (a · b) < 0
_·ʰʳ_ {x<0} {x<0} (a ,, pa) (b ,, pb) = ℝ.·-<0-<0-implies-0< a b pa pb -- a < 0 → b < 0 → 0 < (a · b)
_·ʰʳ_ {x<0} {x≤0} (a ,, pa) (b ,, pb) = ℝ.·-<0-≤0-implies-0≤ a b pa pb -- a < 0 → b ≤ 0 → 0 ≤ (a · b)
_·ʰʳ_ {x≤0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {x≤0} {x#0} (a ,, pa) (b ,, pb) = lift tt
_·ʰʳ_ {x≤0} {0≤x} (a ,, pa) (b ,, pb) = ℝ.·-≤0-0≤-implies-≤0 a b pa pb -- a ≤ 0 → 0 ≤ b → (a · b) ≤ 0
_·ʰʳ_ {x≤0} {0<x} (a ,, pa) (b ,, pb) = ℝ.·-≤0-0<-implies-≤0 a b pa pb -- a ≤ 0 → 0 < b → (a · b) ≤ 0
_·ʰʳ_ {x≤0} {x<0} (a ,, pa) (b ,, pb) = ℝ.·-≤0-<0-implies-0≤ a b pa pb -- a ≤ 0 → b < 0 → 0 ≤ (a · b)
_·ʰʳ_ {x≤0} {x≤0} (a ,, pa) (b ,, pb) = ℝ.·-≤0-≤0-implies-0≤ a b pa pb -- a ≤ 0 → b ≤ 0 → 0 ≤ (a · b)

_·ʰᶜ_ : ∀{p q} → (x : Number (isComplex , p)) → (y : Number (isComplex , q)) → PositivityKindInterpretation isComplex (·-Positivityʰ isComplex p q) (num x ·ᶜ num y)
_·ʰᶜ_ {⁇x⁇} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶜ_ {⁇x⁇} {x#0} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶜ_ {x#0} {⁇x⁇} (a ,, pa) (b ,, pb) = lift tt
_·ʰᶜ_ {x#0} {x#0} (a ,, pa) (b ,, pb) = ℂ.·-#0-#0-implies-#0 a b pa pb -- a # 0 → b # 0 → (a · b) # 0

open PatternsType

-- abs x = max x (- x)

abs : ∀{l p} → (x : Number (l , p)) → abs-Types x
abs {isNat    } {X  } (x ,, p) = (absⁿ x ,, 0≤xⁿ x)
abs {isNat    } {X⁺⁻} (x ,, p) = (absⁿ x ,, ℕ.0≤-#0-implies-0< x (0≤xⁿ x) p)
abs {isNat    } {X₀⁺} (x ,, p) = (absⁿ x ,, p)
abs {isNat    } {X⁺ } (x ,, p) = (absⁿ x ,, p)
abs {isNat    } {X₀⁻} (x ,, p) = (absⁿ x ,, (0ⁿ , (sym $ ≤0→≡0 p)))
abs {isInt    } {X  } (x ,, p) = (absᶻ x ,, {!!}) -- ∀ x → 0 ≤ abs x
abs {isInt    } {X⁺⁻} (x ,, p) = (absᶻ x ,, {!!}) -- ∀ x → x # 0 → 0 < abs x
abs {isInt    } {X₀⁺} (x ,, p) = (absᶻ x ,, {!!}) -- ∀ x → 0 ≤ abs x
abs {isInt    } {X⁺ } (x ,, p) = (absᶻ x ,, {!!}) -- ∀ x → 0 < x → 0 < abs x
abs {isInt    } {X⁻ } (x ,, p) = (absᶻ x ,, {!!}) -- ∀ x → x < 0 → 0 < abs x
abs {isInt    } {X₀⁻} (x ,, p) = (absᶻ x ,, {!!}) -- ∀ x → 0 ≤ abs x
abs {isRat    } {X  } (x ,, p) = (absᶠ x ,, {!!}) -- ∀ x → 0 ≤ abs x
abs {isRat    } {X⁺⁻} (x ,, p) = (absᶠ x ,, {!!}) -- ∀ x → x # 0 → 0 < abs x
abs {isRat    } {X₀⁺} (x ,, p) = (absᶠ x ,, {!!}) -- ∀ x → 0 ≤ abs x
abs {isRat    } {X⁺ } (x ,, p) = (absᶠ x ,, {!!}) -- ∀ x → 0 < x → 0 < abs x
abs {isRat    } {X⁻ } (x ,, p) = (absᶠ x ,, {!!}) -- ∀ x → x < 0 → 0 < abs x
abs {isRat    } {X₀⁻} (x ,, p) = (absᶠ x ,, {!!}) -- ∀ x → 0 ≤ abs x
abs {isReal   } {X  } (x ,, p) = (absʳ x ,, {!!}) -- ∀ x → 0 ≤ abs x
abs {isReal   } {X⁺⁻} (x ,, p) = (absʳ x ,, {!!}) -- ∀ x → x # 0 → 0 < abs x
abs {isReal   } {X₀⁺} (x ,, p) = (absʳ x ,, {!!}) -- ∀ x → 0 ≤ abs x
abs {isReal   } {X⁺ } (x ,, p) = (absʳ x ,, {!!}) -- ∀ x → 0 < x → 0 < abs x
abs {isReal   } {X⁻ } (x ,, p) = (absʳ x ,, {!!}) -- ∀ x → x < 0 → 0 < abs x
abs {isReal   } {X₀⁻} (x ,, p) = (absʳ x ,, {!!}) -- ∀ x → 0 ≤ abs x
abs {isComplex} {X  } (x ,, p) = (absᶜ x ,, 0≤abs x)
abs {isComplex} {X⁺⁻} (x ,, p) = (absᶜ x ,, γ) where
  pʳ = ℂ.0≤abs x
  γ : 0ʳ <ʳ absᶜ x
  γ =  ℝ.0≤-#0-implies-0< (absᶜ x) pʳ (ℂ.abs-preserves-#0 x p)

-- a < b → ¬(b ≤ a) = ¬¬(a < b)

-- 0≤abs       : ∀ x → 0ʳ ≤ʳ abs x
-- abs-preserves-0 : ∀ x → x ≡ 0f → abs x ≡ 0ʳ
-- abs-reflects-0  : ∀ x → abs x ≡ 0ʳ → x ≡ 0f
-- abs-preserves-· : ∀ x y → abs (x · y) ≡ (abs x) ·ʳ (abs y)
-- #-tight : ∀ x y → ¬(x # y) → x ≡ y
-- a ≤ b = ¬(b < a)

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
{-# OPTIONS --rewriting #-}
{-# OPTIONS --show-implicit #-}
module NaturalDeduction-PatternLambdaBug
 where

record ⊤ : Set where

data ⊥ : Set where

foo : ⦃ _ : ⊤ ⦄ → ⊥ → Set
foo = λ {x → {!x!}}
{-
  C-c C-c above generates invalid syntax:
    foo = λ { }
      Found an implicit lambda where an explicit lambda was expected
      when checking that the expression λ {} has type ⊥ → Set

  Better would have been
    foo = λ {()}
-}

-- module DelayMishMash where

--   open import Level --public
--     using (Level) renaming (zero to lzero; suc to lsuc)

--   open import Size public

--   open import Prelude.Monad renaming (Monad to RawMonad)
--   --open import Category.Monad public
--   --  using (RawMonad; module RawMonad)

--   open import Data.Empty --public
--     using (⊥; ⊥-elim)

--   open import Data.List --public
--     using (List; []; _∷_; map)

--   open import Data.Maybe --public
--     using (Maybe; just; nothing) renaming (map to fmap)

--   open import Data.Product public
--     using (∃; _×_; _,_) renaming (proj₁ to fst; proj₂ to snd)
--   --infixr 1 _,_

--   open import Data.Sum --public
--     using (_⊎_; [_,_]′) renaming (inj₁ to inl; inj₂ to inr)

--   open import Data.Unit  --public
--     using (⊤)

--   open import Function --public
--     using (_∘_; case_of_)

--   open import Relation.Nullary --public
--     using (Dec; yes; no)

--   open import Relation.Binary --public
--     using (Setoid; module Setoid)

--   import Relation.Binary.PreorderReasoning
--   module Pre = Relation.Binary.PreorderReasoning

--   open import Relation.Binary.PropositionalEquality --public
--     using (_≡_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning)

--   --open ≡-Reasoning renaming (begin_ to proof_) public

--   open import Relation.Binary.HeterogeneousEquality --public
--     using (_≅_; refl; ≡-to-≅; module ≅-Reasoning)
--     renaming (sym to hsym; trans to htrans; cong to hcong;
--               cong₂ to hcong₂; subst to hsubst)

--   hcong₃ : {A : Set}{B : A → Set}{C : ∀ a → B a → Set}{D : ∀ a b → C a b → Set}
--            (f : ∀ a b c → D a b c)
--            {a a′ : A} → a ≅ a′ →
--            {b : B a}{b′ : B a′} → b ≅ b′ →
--            {c : C a b}{c′ : C a′ b′} → c ≅ c′ →
--            f a b c ≅ f a′ b′ c′
--   hcong₃ f refl refl refl = refl

--   ≅-to-≡ : ∀ {a} {A : Set a} {x y : A} → x ≅ y → x ≡ y
--   ≅-to-≡ refl = refl

--   mutual
--     data Delay (i : Size) (A : Set) : Set where
--       now    :  A           → Delay i A
--       later  :  ∞Delay i A  → Delay i A

--     record ∞Delay (i : Size) (A : Set) : Set where
--       coinductive
--       field
--         force : {j : Size< i} → Delay j A

--   open ∞Delay public

--   never                  :  ∀{i A} → ∞Delay i A
--   force (never {i}) {j}  =  later (never {j})

--   module Bind where
--     mutual
--       bindDelay          :  ∀ {i A B} → Delay i A → (A → Delay i B) → Delay i B
--       bindDelay (now    a) f   =  f a
--       bindDelay (later a∞) f   =  later (bind∞Delay a∞ f)

--       bind∞Delay             :  ∀ {i A B} → ∞Delay i A → (A → Delay i B) → ∞Delay i B
--       force (bind∞Delay a∞ f)  =  bindDelay (force a∞) f

--   _d>>=_ : ∀ {i A B} → Delay i A → (A → Delay i B) → Delay i B
--   _d>>=_ {i} = Bind.bindDelay {i}

--   {-
--   open import Prelude.Applicative using (Applicative)
--   instance delayApplicative : ∀ {i} → Applicative (Delay i)
--   Applicative.pure (delayApplicative {i}) x = now x
--   Applicative._<*>_ (delayApplicative {i}) (now f) x = x d>>= (now ∘ f)
--   Applicative._<*>_ (delayApplicative {i}) (later f) x = {!force f {i}!}
--   {-
--   Applicative._<*>_ (delayApplicative {i}) f (now x) = {!x!} -- Bind.bindDelay x (λ x₁ → {!!})
--   Applicative._<*>_ (delayApplicative {i}) (now f) (later x) = {!!} -- Bind.bindDelay x (λ x₁ → {!!})
--   Applicative._<*>_ (delayApplicative {i}) (later f) (later x) = {!!} -- Bind.bindDelay x (λ x₁ → {!!})
--   -}
--   Applicative.super (delayApplicative {i}) = {!!}
--   -}
--   {-
--   instance delayMonad : ∀ {i} → RawMonad (Delay i)
--   delayMonad {i} = record
--     { {-return  =  now
--     ; -}_>>=_   =  bindDelay {i}
--     } where open Bind
--   -}

--   {-
--   module _ {i : Size} where
--     open module DelayMonad = RawMonad (delayMonad {i = i})
--                              public -- renaming (_⊛_ to _<*>_)
--   -}
--   open Bind public using () renaming (bind∞Delay to _∞>>=_)

--   -- Map for Delay

--   dreturn : {i : Size} → {A : Set} → A → Delay i A
--   dreturn {i} = Delay.now {i}

--   _d<$>_ : ∀ {i A B} (f : A → B) (a : Delay i A) → Delay i B
--   f d<$> a = a d>>= λ a → dreturn (f a)

--   -- Map for ∞Delay

--   _∞<$>_ : ∀ {i A B} (f : A → B) (∞a : ∞Delay i A) → ∞Delay i B
--   f ∞<$> ∞a = ∞a ∞>>= λ a → dreturn (f a)
--   -- force (f ∞<$> ∞a) = f <$> force ∞a

--   -- Double bind

--   _=<<2_,_ : ∀ {i A B C} → (A → B → Delay i C) → Delay i A → Delay i B → Delay i C
--   f =<<2 x , y = x d>>= λ a → y d>>= λ b → f a b

--   mutual
--     data _∼_ {i : Size} {A : Set} : (a? b? : Delay ∞ A) → Set where
--       ∼now    :  ∀ a                              →  now a     ∼ now a
--       ∼later  :  ∀ {a∞ b∞} (eq : a∞ ∞∼⟨ i ⟩∼ b∞)  →  later a∞  ∼ later b∞

--     _∼⟨_⟩∼_ = λ {A} a? i b? → _∼_ {i}{A} a? b?

--     record _∞∼⟨_⟩∼_ {A} (a∞ : ∞Delay ∞ A) i (b∞ : ∞Delay ∞ A) : Set where
--       coinductive
--       field
--         ∼force : {j : Size< i} → force a∞ ∼⟨ j ⟩∼ force b∞

--   _∞∼_ = λ {i} {A} a∞ b∞ → _∞∼⟨_⟩∼_ {A} a∞ i b∞

--   open _∞∼⟨_⟩∼_ public

--   ∼never : ∀{i A} → (never {A = A}) ∞∼⟨ i ⟩∼ never
--   ∼force ∼never = ∼later ∼never

--   ∼refl    :  ∀{i A} (a?  : Delay ∞ A)   →  a? ∼⟨ i ⟩∼ a?
--   ∞∼refl   :  ∀{i A} (a∞  : ∞Delay ∞ A)  →  a∞ ∞∼⟨ i ⟩∼ a∞

--   ∼sym     :  ∀{i A}{a?  b?  : Delay ∞ A }  →  a? ∼⟨ i ⟩∼ b?   →  b? ∼⟨ i ⟩∼ a?
--   ∞∼sym    :  ∀{i A}{a∞  b∞  : ∞Delay ∞ A}  →  a∞ ∞∼⟨ i ⟩∼ b∞  →  b∞ ∞∼⟨ i ⟩∼ a∞

--   ∼trans   :  ∀{i A}{a? b? c? : Delay ∞ A} →
--               a? ∼⟨ i ⟩∼ b? →  b? ∼⟨ i ⟩∼ c? → a? ∼⟨ i ⟩∼ c?
--   ∞∼trans  :  ∀{i A}{a∞ b∞ c∞ : ∞Delay ∞ A} →
--               a∞ ∞∼⟨ i ⟩∼ b∞ →  b∞ ∞∼⟨ i ⟩∼ c∞ → a∞ ∞∼⟨ i ⟩∼ c∞

--   ∼refl (now a)    = ∼now a
--   ∼refl (later a∞) = ∼later (∞∼refl a∞)

--   ∼force (∞∼refl a∞) = ∼refl (force a∞)

--   ∼sym (∼now a)    = ∼now a
--   ∼sym (∼later eq) = ∼later (∞∼sym eq)

--   ∼force (∞∼sym eq) = ∼sym (∼force eq)

--   ∼trans (∼now a)    (∼now .a)    = ∼now a
--   ∼trans (∼later eq) (∼later eq′) = ∼later (∞∼trans eq eq′)

--   ∼force (∞∼trans eq eq′) = ∼trans (∼force eq) (∼force eq′)

--   -- Equality reasoning

--   ∼setoid : (i : Size) (A : Set) → Setoid lzero lzero
--   ∼setoid i A = record
--     { Carrier       = Delay ∞ A
--     ; _≈_           = _∼_ {i}
--     ; isEquivalence = record
--       { refl  = λ {a?} → ∼refl a?
--       ; sym   = ∼sym
--       ; trans = ∼trans
--       }
--     }

--   ∞∼setoid : (i : Size) (A : Set) → Setoid lzero lzero
--   ∞∼setoid i A = record
--     { Carrier       = ∞Delay ∞ A
--     ; _≈_           = _∞∼_ {i}
--     ; isEquivalence = record
--       { refl  = λ {a?} → ∞∼refl a?
--       ; sym   = ∞∼sym
--       ; trans = ∞∼trans
--       }
--     }

--   module ∼-Reasoning {i : Size} {A : Set} where
--     open Pre (Setoid.preorder (∼setoid i A)) public
--   --    using (begin_; _∎) (_≈⟨⟩_ to _∼⟨⟩_; _≈⟨_⟩_ to _∼⟨_⟩_)
--       renaming (_≈⟨⟩_ to _≡⟨⟩_; _≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _∼⟨_⟩_; begin_ to proof_)

--   module ∞∼-Reasoning {i : Size} {A : Set} where
--     open Pre (Setoid.preorder (∞∼setoid i A)) public
--   --    using (begin_; _∎) (_≈⟨⟩_ to _∼⟨⟩_; _≈⟨_⟩_ to _∼⟨_⟩_)
--       renaming (_≈⟨⟩_ to _≡⟨⟩_; _≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _∞∼⟨_⟩_; begin_ to proof_)

--   mutual
--     bind-assoc               :  ∀{i A B C} (m : Delay ∞ A)
--                                 {k : A → Delay ∞ B} {l : B → Delay ∞ C} →
--                                 ((m d>>= k) d>>= l) ∼⟨ i ⟩∼ (m d>>= λ a → (k a d>>= l))
--     bind-assoc (now a)       =  ∼refl _
--     bind-assoc (later a∞)    =  ∼later (∞bind-assoc a∞)

--     ∞bind-assoc              :  ∀{i A B C} (a∞ : ∞Delay ∞ A)
--                                 {k : A → Delay ∞ B} {l : B → Delay ∞ C} →
--                                 ((a∞ ∞>>= k) ∞>>= l) ∞∼⟨ i ⟩∼ (a∞ ∞>>= λ a → (k a d>>= l))
--     ∼force (∞bind-assoc a∞)  =  bind-assoc (force a∞)

--   bind-cong-l   :  ∀{i A B}{a? b? : Delay ∞ A} →  a? ∼⟨ i ⟩∼ b? →
--                    (k : A → Delay ∞ B) → (a? d>>= k) ∼⟨ i ⟩∼ (b? d>>= k)

--   ∞bind-cong-l  :  ∀{i A B}{a∞ b∞ : ∞Delay ∞ A} → a∞ ∞∼⟨ i ⟩∼ b∞ →
--                    (k : A → Delay ∞ B) → (a∞ ∞>>= k) ∞∼⟨ i ⟩∼ (b∞ ∞>>= k)

--   bind-cong-r   :  ∀{i A B}(a? : Delay ∞ A){k l : A → Delay ∞ B} →
--                    (∀ a → (k a) ∼⟨ i ⟩∼ (l a)) → (a? d>>= k) ∼⟨ i ⟩∼ (a? d>>= l)

--   ∞bind-cong-r  :  ∀{i A B}(a∞ : ∞Delay ∞ A){k l : A → Delay ∞ B} →
--                    (∀ a → (k a) ∼⟨ i ⟩∼ (l a)) → (a∞ ∞>>= k) ∞∼⟨ i ⟩∼ (a∞ ∞>>= l)

--   bind-cong-l (∼now a)    k = ∼refl _
--   bind-cong-l (∼later eq) k = ∼later (∞bind-cong-l eq k)

--   ∼force (∞bind-cong-l eq k) = bind-cong-l (∼force eq) k

--   bind-cong-r (now a)    h = h a
--   bind-cong-r (later a∞) h = ∼later (∞bind-cong-r a∞ h)

--   ∼force (∞bind-cong-r a∞ h) = bind-cong-r (force a∞) h

--   open import Prelude.Functor using (Functor; _<$>_)
-- {-
--   instance FunctorDelay : {i : Size} → Functor (Delay i)
--   Functor.fmap (FunctorDelay {i}) {A} {B} f (now x) = {!!}
--   Functor.fmap (FunctorDelay {i}) {A} {B} f (later x) = {!!}
-- -}
--   open import Prelude.Function using (_∘′_)

--   map-compose     :  ∀{i A B C} (a? : Delay ∞ A) {f : A → B} {g : B → C} →
--                      (g d<$> (f d<$> a?)) ∼⟨ i ⟩∼ ((g ∘ f) d<$> a?)
--   map-compose a?  =  bind-assoc a?

--   map-cong        :  ∀{i A B}{a? b? : Delay ∞ A} (f : A → B) →
--                      a? ∼⟨ i ⟩∼ b? → (f d<$> a?) ∼⟨ i ⟩∼ (f d<$> b?)
--   map-cong f eq   =  bind-cong-l eq (now ∘ f)

--   data _⇓_ {A : Set} : (a? : Delay ∞ A) (a : A) → Set where
--     now⇓    :  ∀{a}                                   → now a ⇓ a
--     later⇓  :  ∀{a} {a∞ : ∞Delay ∞ A} → force a∞ ⇓ a  → later a∞ ⇓ a

--   _⇓   :  {A : Set} (x : Delay ∞ A) → Set
--   x ⇓  =  ∃ λ a → x ⇓ a

--   map⇓     :  ∀{A B}{a : A}{a? : Delay ∞ A}(f : A → B) → a? ⇓ a → (f d<$> a?) ⇓ f a

--   subst∼⇓  :  ∀{A}{a? a?′ : Delay ∞ A}{a : A} → a? ⇓ a → a? ∼ a?′ → a?′ ⇓ a

--   bind⇓    :  ∀{A B}(f : A → Delay ∞ B){?a : Delay ∞ A}{a : A}{b : B} →
--               ?a ⇓ a → f a ⇓ b → (?a d>>= f) ⇓ b

--   map⇓ f now⇓        = now⇓
--   map⇓ f (later⇓ a⇓) = later⇓ (map⇓ f a⇓)

--   subst∼⇓ now⇓ (∼now a) = now⇓
--   subst∼⇓ (later⇓ p) (∼later eq) = later⇓ (subst∼⇓ p (∼force eq))

--   bind⇓ f now⇓ q = q
--   bind⇓ f (later⇓ p) q = later⇓ (bind⇓ f p q)

--   --infixr 6 _⇒_
--   --infixl 1 _,_

-- module CustomPrelude where

--   open import Prelude public
--     renaming (_==_ to _≟_) -- TODO ask Agda to rename Eq._==_ to Eq._≟_
--     hiding (force) -- needed by ∞Delay

--   {-# BUILTIN REWRITE _≡_ #-}

--   --{-# DISPLAY Eq._==_ _ = _≟_ #-}

--   open import Container.List renaming (_∈_ to _∈C_; lookup∈ to lookup∈C) public

--   _∈C?_ : ∀ {ℓ} {A : Set ℓ} ⦃ _ : Eq A ⦄ (a : A) → (xs : List A) → Dec (a ∈C xs)
--   a ∈C? [] = no λ ()
--   a ∈C? (x ∷ xs) with a ≟ x
--   … | yes a≡x rewrite a≡x = yes (zero refl)
--   … | no a≢x with a ∈C? xs
--   … | yes a∈xs = yes (suc a∈xs)
--   … | no a∉xs = no (λ {(zero a≡x) → a≢x a≡x ; (suc a∈xs) → a∉xs a∈xs})

--   data _∈_ {ℓ} {A : Set ℓ} (a : A) : List A → Set ℓ
--    where
--     here : (as : List A) → a ∈ (a ∷ as)
--     there : (x : A) {as : List A} → a ∈ as → a ∈ (x ∷ as)

--   _∉_ : ∀ {ℓ} {A : Set ℓ} ⦃ _ : Eq A ⦄ (a : A) → (xs : List A) → Set ℓ
--   a ∉ xs = ¬ (a ∈ xs)

--   _∈?_ : ∀ {ℓ} {A : Set ℓ} ⦃ _ : Eq A ⦄ (a : A) → (xs : List A) → Dec (a ∈ xs)
--   a ∈? [] = no λ ()
--   a ∈? (x ∷ xs) with a ≟ x
--   … | yes a≡x rewrite a≡x = yes (here xs)
--   … | no a≢x with a ∈? xs
--   … | yes a∈xs = yes (there x a∈xs)
--   … | no a∉xs = no (λ {(here _) → a≢x refl ; (there _ a∈xs) → a∉xs a∈xs})

--   _⊆_ : ∀ {ℓ} {A : Set ℓ} → List A → List A → Set ℓ
--   R ⊆ S = ∀ {x} → x ∈ R → x ∈ S

--   _≢_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
--   x ≢ y = ¬ (x ≡ y)

--   infix 0 _↔_
--   _↔_ : {ℓ¹ : Level} → Set ℓ¹ → {ℓ² : Level} → Set ℓ² → Set (ℓ¹ ⊔ ℓ²)
--   P ↔ Q = (P → Q) × (Q → P)

--   ∃ : ∀ {ℓᴬ ℓᴮ} {A : Set ℓᴬ} (B : A → Set ℓᴮ) → Set (ℓᴬ ⊔ ℓᴮ)
--   ∃ = Σ _

--   ∄ : ∀ {ℓᴬ ℓᴮ} {A : Set ℓᴬ} (B : A → Set ℓᴮ) → Set (ℓᴬ ⊔ ℓᴮ)
--   ∄ = ¬_ ∘ ∃

--   infixl 4 _⊎_
--   _⊎_ = Either

--   --open import Agda.Builtin.Size public
--   open import Size public

--   open import Control.Monad.State public
--   open import Control.Monad.Identity public
--   open import Container.Traversable public

--   sequence : ∀ {a b} {A : Set a} {F : Set a → Set b} ⦃ _ : Applicative F ⦄ → List (F A) → F ⊤′
--   sequence [] = pure tt
--   sequence (x ∷ xs) = x *> sequence xs

--   open import Tactic.Nat public

--   open import Tactic.Deriving.Eq public

--   mutual

--     data Delay (i : Size) (A : Set) : Set where
--       now    :  A           → Delay i A
--       later  :  ∞Delay i A  → Delay i A

--     record ∞Delay (i : Size) (A : Set) : Set where
--       coinductive
--       field
--         force : {j : Size< i} → Delay j A

--   open ∞Delay public

--   module BindDelay
--    where

--     mutual

--       bindDelay          :  ∀ {i A B} → Delay i A → (A → Delay i B) → Delay i B
--       bindDelay (now    a) f   =  f a
--       bindDelay (later ∞a) f   =  later (bind∞Delay ∞a f)

--       bind∞Delay             :  ∀ {i A B} → ∞Delay i A → (A → Delay i B) → ∞Delay i B
--       force (bind∞Delay ∞a f)  =  bindDelay (force ∞a) f

--   module _
--    where

--     open BindDelay

--     open BindDelay public using () renaming (bind∞Delay to _∞>>=_)

--     instance FunctorDelay : {i : Size} → Functor (Delay i)
--     Functor.fmap FunctorDelay f x = bindDelay x $ now ∘ f

--     instance ApplicativeDelay : {i : Size} → Applicative (Delay i)
--     Applicative.pure ApplicativeDelay x = now x
--     Applicative._<*>_ ApplicativeDelay (now f) x = f <$> x
--     Applicative._<*>_ ApplicativeDelay (later ∞f) x = later ∘ bind∞Delay ∞f $ flip fmap x
--     Applicative.super ApplicativeDelay = FunctorDelay

--     instance MonadDelay : {i : Size} → Monad (Delay i)
--     Monad._>>=_ MonadDelay = bindDelay
--     Monad.super MonadDelay = ApplicativeDelay

--   mutual

--     data _∼_ {i : Size} {A : Set} : (a? b? : Delay ∞ A) → Set where
--       ∼now    :  ∀ a                              →  now a     ∼ now a
--       ∼later  :  ∀ {a∞ b∞} (eq : a∞ ∞∼⟨ i ⟩∼ b∞)  →  later a∞  ∼ later b∞

--     _∼⟨_⟩∼_ = λ {A} a? i b? → _∼_ {i}{A} a? b?

--     record _∞∼⟨_⟩∼_ {A} (a∞ : ∞Delay ∞ A) i (b∞ : ∞Delay ∞ A) : Set where
--       coinductive
--       field
--         ∼force : {j : Size< i} → force a∞ ∼⟨ j ⟩∼ force b∞

--   open _∞∼⟨_⟩∼_ public

--   _∞∼_ = λ {i} {A} a∞ b∞ → _∞∼⟨_⟩∼_ {A} a∞ i b∞

--   mutual

--     ∼refl    :  ∀{i A} (a?  : Delay ∞ A)   →  a? ∼⟨ i ⟩∼ a?
--     ∼refl (now a)    = ∼now a
--     ∼refl (later a∞) = ∼later (∞∼refl a∞)

--     ∞∼refl   :  ∀{i A} (a∞  : ∞Delay ∞ A)  →  a∞ ∞∼⟨ i ⟩∼ a∞
--     ∼force (∞∼refl a∞) = ∼refl (force a∞)

--   mutual

--     ∼sym     :  ∀{i A}{a?  b?  : Delay ∞ A }  →  a? ∼⟨ i ⟩∼ b?   →  b? ∼⟨ i ⟩∼ a?
--     ∼sym (∼now a)    = ∼now a
--     ∼sym (∼later eq) = ∼later (∞∼sym eq)

--     ∞∼sym    :  ∀{i A}{a∞  b∞  : ∞Delay ∞ A}  →  a∞ ∞∼⟨ i ⟩∼ b∞  →  b∞ ∞∼⟨ i ⟩∼ a∞
--     ∼force (∞∼sym eq) = ∼sym (∼force eq)

--   mutual

--     ∼trans   :  ∀{i A}{a? b? c? : Delay ∞ A} →
--                 a? ∼⟨ i ⟩∼ b? →  b? ∼⟨ i ⟩∼ c? → a? ∼⟨ i ⟩∼ c?
--     ∼trans (∼now a)    (∼now .a)    = ∼now a
--     ∼trans (∼later eq) (∼later eq′) = ∼later (∞∼trans eq eq′)

--     ∞∼trans  :  ∀{i A}{a∞ b∞ c∞ : ∞Delay ∞ A} →
--                 a∞ ∞∼⟨ i ⟩∼ b∞ →  b∞ ∞∼⟨ i ⟩∼ c∞ → a∞ ∞∼⟨ i ⟩∼ c∞
--     ∼force (∞∼trans eq eq′) = ∼trans (∼force eq) (∼force eq′)

--   --∼setoid : (i : Size) (A : Set) → Setoid lzero lzero
--   --∞∼setoid : (i : Size) (A : Set) → Setoid lzero lzero

--   mutual

--     bind-assoc               :  ∀{i A B C} (m : Delay ∞ A)
--                                 {k : A → Delay ∞ B} {l : B → Delay ∞ C} →
--                                 ((m >>= k) >>= l) ∼⟨ i ⟩∼ (m >>= λ a → (k a >>= l))
--     bind-assoc (now a)       =  ∼refl _
--     bind-assoc (later a∞)    =  ∼later (∞bind-assoc a∞)

--     ∞bind-assoc              :  ∀{i A B C} (a∞ : ∞Delay ∞ A)
--                                 {k : A → Delay ∞ B} {l : B → Delay ∞ C} →
--                                 ((a∞ ∞>>= k) ∞>>= l) ∞∼⟨ i ⟩∼ (a∞ ∞>>= λ a → (k a >>= l))
--     ∼force (∞bind-assoc a∞)  =  bind-assoc (force a∞)

--   mutual

--     bind-cong-l   :  ∀{i A B}{a? b? : Delay ∞ A} →  a? ∼⟨ i ⟩∼ b? →
--                      (k : A → Delay ∞ B) → (a? >>= k) ∼⟨ i ⟩∼ (b? >>= k)
--     bind-cong-l (∼now a)    k = ∼refl _
--     bind-cong-l (∼later eq) k = ∼later (∞bind-cong-l eq k)

--     ∞bind-cong-l  :  ∀{i A B}{a∞ b∞ : ∞Delay ∞ A} → a∞ ∞∼⟨ i ⟩∼ b∞ →
--                      (k : A → Delay ∞ B) → (a∞ ∞>>= k) ∞∼⟨ i ⟩∼ (b∞ ∞>>= k)
--     ∼force (∞bind-cong-l eq k) = bind-cong-l (∼force eq) k

--   mutual
--     bind-cong-r   :  ∀{i A B}(a? : Delay ∞ A){k l : A → Delay ∞ B} →
--                      (∀ a → (k a) ∼⟨ i ⟩∼ (l a)) → (a? >>= k) ∼⟨ i ⟩∼ (a? >>= l)
--     bind-cong-r (now a)    h = h a
--     bind-cong-r (later a∞) h = ∼later (∞bind-cong-r a∞ h)

--     ∞bind-cong-r  :  ∀{i A B}(a∞ : ∞Delay ∞ A){k l : A → Delay ∞ B} →
--                      (∀ a → (k a) ∼⟨ i ⟩∼ (l a)) → (a∞ ∞>>= k) ∞∼⟨ i ⟩∼ (a∞ ∞>>= l)
--     ∼force (∞bind-cong-r a∞ h) = bind-cong-r (force a∞) h

--   map-compose     :  ∀{i A B C} (a? : Delay ∞ A) {f : A → B} {g : B → C} →
--                      (g <$> (f <$> a?)) ∼⟨ i ⟩∼ ((g ∘ f) <$> a?)
--   map-compose a?  =  bind-assoc a?

--   map-cong        :  ∀{i A B}{a? b? : Delay ∞ A} (f : A → B) →
--                      a? ∼⟨ i ⟩∼ b? → (f <$> a?) ∼⟨ i ⟩∼ (f <$> b?)
--   map-cong f eq   =  bind-cong-l eq (now ∘ f)

--   data _⇓_ {A : Set} : (a? : Delay ∞ A) (a : A) → Set where
--     now⇓    :  ∀{a}                                   → now a ⇓ a
--     later⇓  :  ∀{a} {a∞ : ∞Delay ∞ A} → force a∞ ⇓ a  → later a∞ ⇓ a

--   _⇓   :  {A : Set} (x : Delay ∞ A) → Set
--   x ⇓  =  ∃ λ a → x ⇓ a

--   map⇓     :  ∀{A B}{a : A}{a? : Delay ∞ A}(f : A → B) → a? ⇓ a → (f <$> a?) ⇓ f a
--   map⇓ f now⇓        = now⇓
--   map⇓ f (later⇓ a⇓) = later⇓ (map⇓ f a⇓)

--   bind⇓    :  ∀{A B}(f : A → Delay ∞ B){?a : Delay ∞ A}{a : A}{b : B} →
--               ?a ⇓ a → f a ⇓ b → (?a >>= f) ⇓ b
--   bind⇓ f now⇓ q = q
--   bind⇓ f (later⇓ p) q = later⇓ (bind⇓ f p q)

--   infixl 4 _>>=⇓_
--   _>>=⇓_    :  ∀{A B}{f : A → Delay ∞ B}{?a : Delay ∞ A}{a : A}{b : B} →
--                ?a ⇓ a → f a ⇓ b → (?a >>= f) ⇓ b
--   _>>=⇓_ = bind⇓ _

--   infixl 4 _⇓>>=⇓_
--   _⇓>>=⇓_    :  ∀{A B}{f : A → Delay ∞ B}{?a : Delay ∞ A}{b : B} →
--                 (?a⇓ : ?a ⇓) → f (fst ?a⇓) ⇓ b → (?a >>= f) ⇓ b
--   _⇓>>=⇓_ (_ , a⇓) = bind⇓ _ a⇓

--   _⇓Dec>>=⇓_else⇓_ : ∀{A B}{f-yes : A → Delay ∞ B}{f-no : ¬ A → Delay ∞ B}{?a : Delay ∞ (Dec A)}{b : B} →
--               (?a⇓ : ?a ⇓) →
--               ((a : A) → f-yes a ⇓ b) →
--               ((¬a : ¬ A) → f-no ¬a ⇓ b) →
--               ((?a >>= (λ { (yes y) → f-yes y ; (no n) → f-no n }))) ⇓ b
--   (yes y , y⇓) ⇓Dec>>=⇓ fy⇓ else⇓ fn⇓ = y⇓ >>=⇓ fy⇓ y
--   (no n , n⇓) ⇓Dec>>=⇓ fy⇓ else⇓ fn⇓ = n⇓ >>=⇓ fn⇓ n

--   _⇓DecEq>>=⇓_else⇓_ : ∀{A : Set} {A₁ A₂ : A} {B}{f-yes : A₁ ≡ A₂ → Delay ∞ B}{f-no : A₁ ≢ A₂ → Delay ∞ B}{?a : Delay ∞ (Dec (A₁ ≡ A₂))}{b : B} →
--               (?a⇓ : ?a ⇓) →
--               ((eq : A₁ ≡ A₂) → f-yes eq ⇓ b) →
--               ((¬eq : A₁ ≢ A₂) → f-no ¬eq ⇓ b) →
--               ((?a >>= (λ { (yes refl) → f-yes refl ; (no n) → f-no n }))) ⇓ b
--   (yes refl , y⇓) ⇓DecEq>>=⇓ fy⇓ else⇓ fn⇓ = y⇓ >>=⇓ fy⇓ refl
--   (no n , n⇓) ⇓DecEq>>=⇓ fy⇓ else⇓ fn⇓ = n⇓ >>=⇓ fn⇓ n

--   app⇓ : ∀{A}{B}{f? : Delay ∞ (A → B)}{f : A → B}{x? : Delay ∞ A}{x : A} → f? ⇓ f → x? ⇓ x → (f? <*> x?) ⇓ f x
--   app⇓ now⇓ now⇓ = now⇓
--   app⇓ now⇓ (later⇓ x?) = later⇓ $ map⇓ _ x?
--   app⇓ (later⇓ f?) now⇓ = later⇓ $ bind⇓ _ f? now⇓
--   app⇓ (later⇓ ⇓f) (later⇓ ⇓x) = later⇓ $ bind⇓ _ ⇓f $ later⇓ $ bind⇓ _ ⇓x now⇓

--   subst∼⇓  :  ∀{A}{a? a?′ : Delay ∞ A}{a : A} → a? ⇓ a → a? ∼ a?′ → a?′ ⇓ a
--   subst∼⇓ now⇓ (∼now a) = now⇓
--   subst∼⇓ (later⇓ p) (∼later eq) = later⇓ (subst∼⇓ p (∼force eq))
--   {-
--   traverse⇓' : ∀{A}{B}{f? : A → Delay ∞ B}{T : Set → Set}⦃ _ : Traversable T ⦄{X : T A} → (∀ x → f? x ⇓) → ∀ (x : T A) → traverse f? x ⇓
--   traverse⇓' x₁ x₂ = {!!} , {!!}
--   -}
--   {-
--   traverse⇓ : ∀{A}{B}{f : A → B}{T : Set → Set}⦃ _ : Traversable T ⦄{X : T A} → (∀ x → f? x ⇓) → ∀ (x : T A) → traverse f x ⇓
--   traverse⇓ x₁ x₂ = {!!} , {!!}
--   -}
--   traverse-list⇓ : ∀{A}{B} (f? : A → Delay ∞ B) → (∀ x → f? x ⇓) → (xs : List A) → traverse f? xs ⇓
--   traverse-list⇓ f? f?⇓ [] = [] , now⇓
--   traverse-list⇓ f? f?⇓ (x ∷ xs)
--    with f?⇓ x | traverse-list⇓ f? f?⇓ xs
--   … | y , y⇓ | ys , ys⇓ = y ∷ ys , app⇓ (map⇓ _ y⇓) ys⇓
--   {-
--   traverse-vec⇓' : ∀{A}{B}{𝑎} (f? : A → Delay ∞ B) → (∀ x → f? x ⇓) → (xs : Vector A 𝑎) → traverse f? xs ⇓
--   traverse-vec⇓' f? f?⇓ [] = [] , now⇓
--   traverse-vec⇓' f? f?⇓ (x ∷ xs)
--    with f?⇓ x | traverse-vec⇓' f? f?⇓ xs
--   … | y , y⇓ | ys , ys⇓ = y ∷ ys , app⇓ (map⇓ _ y⇓) ys⇓

--   traverse-vec⇓ : ∀{A}{B}{𝑎} (f : A → B) → (xs : Vector (Delay ∞ A) 𝑎) → traverse {!f!} xs ⇓
--   traverse-vec⇓ = {!!}
--   -}

-- open CustomPrelude

-- -- infix 15 _╱_
-- -- record Sequent (A : Set) ⦃ _ : BeFormula A ⦄ : Set
-- --  where
-- --   constructor _╱_
-- --   field
-- --     statement : A
-- --     suppositions : List A

-- -- open Sequent

-- -- foooo : {A : Set} ⦃ bf : BeFormula A ⦄ {-⦃ hs : HasNegation A ⦄-} {-(x : Sequent A)-} →
-- --       (∃ λ (x : A) → x ∈ List.[]) → ⊥
-- --       {-
-- --       Dec
-- --       (-- Either
-- --        (Σ A
-- --         (λ x₁ →
-- --            --Σ
-- --            ({-BeFormula.formula bf -}x₁ ∈
-- --             {-map (BeFormula.formula bf)-} [] {-(suppositions x)-})
-- --            {-
-- --            (λ _ →
-- --              ⊤
-- --               --BeFormula.formula bf (HasNegation.~ hs x₁) ∈
-- --               --map (BeFormula.formula bf) (suppositions x)
-- --               )-}
-- --            ))
-- --        {-(BeFormula.formula bf (statement x) ∈
-- --         map (BeFormula.formula bf) (suppositions x))-})
-- --       -}
-- -- foooo = λ {x → {!x!}}
-- -- {-
-- -- foooo (statement₁ ╱ []) = λ {x → {!x!}} -- no (λ {x → {!x!}})
-- -- foooo (statement₁ ╱ (x ∷ suppositions₁)) = {!!}
-- -- -}
-- -- -- TruthValue = Bool

-- -- -- -- reification of elements of the domain
-- -- -- Element = Nat

-- -- -- record VariableName : Set
-- -- --  where
-- -- --   constructor ⟨_⟩
-- -- --   field
-- -- --     name : Nat

-- -- -- open VariableName

-- -- -- instance EqVariableName : Eq VariableName
-- -- -- Eq._==_ EqVariableName _ = decEq₁ (cong name) ∘ (_≟_ on name $ _)

-- -- -- record FunctionName : Set
-- -- --  where
-- -- --   constructor ⟨_⟩
-- -- --   field
-- -- --     name : Nat

-- -- -- open FunctionName

-- -- -- instance EqFunctionName : Eq FunctionName
-- -- -- Eq._==_ EqFunctionName _ = decEq₁ (cong name) ∘ (_≟_ on name $ _)

-- -- -- record PredicateName : Set
-- -- --  where
-- -- --   constructor ⟨_⟩
-- -- --   field
-- -- --     name : Nat

-- -- -- open PredicateName

-- -- -- instance EqPredicateName : Eq PredicateName
-- -- -- Eq._==_ EqPredicateName _ = decEq₁ (cong name) ∘ (_≟_ on name $ _)

-- -- -- record Arity : Set
-- -- --  where
-- -- --   constructor ⟨_⟩
-- -- --   field
-- -- --     arity : Nat

-- -- -- open Arity

-- -- -- instance EqArity : Eq Arity
-- -- -- Eq._==_ EqArity _ = decEq₁ (cong arity) ∘ (_≟_ on arity $ _)

-- -- -- Vector : Set → Arity → Set
-- -- -- Vector A = Vec A ∘ arity

-- -- -- record Elements : Set
-- -- --  where
-- -- --   constructor ⟨_⟩
-- -- --   field
-- -- --     {arity} : Arity
-- -- --     elements : Vector Element arity

-- -- -- open Elements

-- -- -- instance EqElements : Eq Elements
-- -- -- Eq._==_ EqElements (⟨_⟩ {𝑎₁} εs₁) (⟨_⟩ {𝑎₂} εs₂)
-- -- --  with 𝑎₁ ≟ 𝑎₂
-- -- -- … | no 𝑎₁≢𝑎₂ = no λ {refl → 𝑎₁≢𝑎₂ refl}
-- -- -- … | yes refl
-- -- --  with εs₁ ≟ εs₂
-- -- -- … | yes refl = yes refl
-- -- -- … | no εs₁≢εs₂ = no λ {refl → εs₁≢εs₂ refl}

-- -- -- record Interpretation : Set
-- -- --  where
-- -- --   field
-- -- --     μ⟦_⟧ : VariableName → Element
-- -- --     𝑓⟦_⟧ : FunctionName → Elements → Element
-- -- --     𝑃⟦_⟧ : PredicateName → Elements → TruthValue

-- -- -- open Interpretation

-- -- -- mutual

-- -- --   data Term : Set
-- -- --    where
-- -- --     variable : VariableName → Term
-- -- --     function : FunctionName → Terms → Term

-- -- --   record Terms : Set
-- -- --    where
-- -- --     constructor ⟨_⟩
-- -- --     inductive
-- -- --     field
-- -- --       {arity} : Arity
-- -- --       terms : Vector Term arity

-- -- -- open Terms

-- -- -- termVariable-inj : ∀ {𝑥₁ 𝑥₂} → Term.variable 𝑥₁ ≡ variable 𝑥₂ → 𝑥₁ ≡ 𝑥₂
-- -- -- termVariable-inj refl = refl

-- -- -- termFunction-inj₁ : ∀ {𝑓₁ 𝑓₂ τ₁s τ₂s} → Term.function 𝑓₁ τ₁s ≡ function 𝑓₂ τ₂s → 𝑓₁ ≡ 𝑓₂
-- -- -- termFunction-inj₁ refl = refl

-- -- -- termFunction-inj₂ : ∀ {𝑓₁ 𝑓₂ τ₁s τ₂s} → Term.function 𝑓₁ τ₁s ≡ function 𝑓₂ τ₂s → τ₁s ≡ τ₂s
-- -- -- termFunction-inj₂ refl = refl

-- -- -- foo : ∀ a → (ts1 ts2 : Vec Term (arity a)) → (τ₁≡τ₂ : Terms.⟨ ts1 ⟩ ≡ (⟨_⟩ {a} ts2)) → _≡_ {lzero} {Vec Term (arity a)} ts1 ts2
-- -- -- foo a ts1 .ts1 refl = refl

-- -- -- mutual

-- -- --   EqTerm⇑ : ∀ {i} → (x y : Term) → Delay i ∘ Dec $ x ≡ y
-- -- --   EqTerm⇑ (variable _) (variable _) = now (decEq₁ termVariable-inj $ _≟_ _ _)
-- -- --   EqTerm⇑ (function 𝑓₁ τ₁s) (function 𝑓₂ τ₂s) = EqTerms⇑ τ₁s τ₂s >>= λ τ₁s≟τ₂s → now $ decEq₂ termFunction-inj₁ termFunction-inj₂ (𝑓₁ ≟ 𝑓₂) τ₁s≟τ₂s
-- -- --   EqTerm⇑ (variable _) (function _ _) = now $ no λ ()
-- -- --   EqTerm⇑ (function _ _) (variable _) = now $ no λ ()

-- -- --   EqTerms⇑ : ∀ {i} → (x y : Terms) → Delay i ∘ Dec $ x ≡ y
-- -- --   EqTerms⇑ (⟨_⟩ {𝑎₁} τ₁s) (⟨_⟩ {𝑎₂} τ₂s)
-- -- --    with 𝑎₁ ≟ 𝑎₂
-- -- --   … | no 𝑎₁≢𝑎₂ = now $ no λ {τ₁≡τ₂ → 𝑎₁≢𝑎₂ (cong arity τ₁≡τ₂)}
-- -- --   … | yes refl = EqVecTerm⇑ τ₁s τ₂s >>= λ { (yes refl) → now $ yes refl ; (no τ₁s≢τ₂s) → now $ no (λ ⟨τ₁s⟩≡⟨τ₂s⟩ → τ₁s≢τ₂s (foo ⟨ arity 𝑎₁ ⟩ τ₁s τ₂s ⟨τ₁s⟩≡⟨τ₂s⟩)) }

-- -- --   EqVecTerm⇑ : ∀ {i} {n} → (x y : Vec Term n) → Delay i ∘ Dec $ x ≡ y
-- -- --   EqVecTerm⇑ [] [] = now (yes refl)
-- -- --   EqVecTerm⇑ (τ₁ ∷ τ₁s) (τ₂ ∷ τ₂s) =
-- -- --     EqTerm⇑ τ₁ τ₂ >>= λ
-- -- --     { (yes refl) → EqVecTerm⇑ τ₁s τ₂s >>= λ
-- -- --                    { (yes refl) → now $ yes refl
-- -- --                    ; (no τ₁s≢τ₂s) → now $ no λ τ₁₁s≡τ₁₂s → τ₁s≢τ₂s $ vcons-inj-tail τ₁₁s≡τ₁₂s }
-- -- --     ; (no τ₁≢τ₂) → now $ no λ τ₁₁s≡τ₂₂s → τ₁≢τ₂ $ vcons-inj-head τ₁₁s≡τ₂₂s }

-- -- -- EqVecTerm⇓ : ∀ {n} → (x y : Vec Term n) → EqVecTerm⇑ x y ⇓
-- -- -- EqVecTerm⇓ [] [] = _ , now⇓
-- -- -- EqVecTerm⇓ (variable 𝑥₁ ∷ τ₁s) (variable 𝑥₂ ∷ τ₂s)
-- -- --  with 𝑥₁ ≟ 𝑥₂
-- -- -- … | yes refl with EqVecTerm⇓ τ₁s τ₂s
-- -- -- EqVecTerm⇓ (variable 𝑥₁ ∷ τ₁s) (variable .𝑥₁ ∷ .τ₁s) | yes refl | (yes refl , snd₁) = _ , snd₁ >>=⇓ now⇓
-- -- -- EqVecTerm⇓ (variable 𝑥₁ ∷ τ₁s) (variable .𝑥₁ ∷ τ₂s) | yes refl | (no x , snd₁) = _ , snd₁ >>=⇓ now⇓
-- -- -- EqVecTerm⇓ (variable 𝑥₁ ∷ τ₁s) (variable 𝑥₂ ∷ τ₂s) | no 𝑥₁≢𝑥₂ = _ , now⇓
-- -- -- EqVecTerm⇓ (variable x ∷ τ₁s) (function x₁ x₂ ∷ τ₂s) = _ , now⇓
-- -- -- EqVecTerm⇓ (function x x₁ ∷ τ₁s) (variable x₂ ∷ τ₂s) = _ , now⇓
-- -- -- EqVecTerm⇓ (function 𝑓₁ (⟨_⟩ {𝑎₁} τ₁s) ∷ τ₁₂s) (function 𝑓₂ (⟨_⟩ {𝑎₂} τ₂s) ∷ τ₂₂s)
-- -- --  with 𝑎₁ ≟ 𝑎₂ | 𝑓₁ ≟ 𝑓₂
-- -- -- … | no 𝑎₁≢𝑎₂ | no 𝑓₁≢𝑓₂  = _ , now⇓
-- -- -- … | no 𝑎₁≢𝑎₂ | yes refl  = _ , now⇓
-- -- -- … | yes refl | no 𝑓₁≢𝑓₂
-- -- --  with EqVecTerm⇓ τ₁s τ₂s
-- -- -- … | (no τ₁s≢τ₂s , τ⇓)  = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ now⇓
-- -- -- … | (yes refl , τ⇓)    = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ now⇓
-- -- -- EqVecTerm⇓ (function 𝑓₁ (⟨_⟩ {𝑎₁} τ₁s) ∷ τ₁₂s) (function 𝑓₂ (⟨_⟩ {𝑎₂} τ₂s) ∷ τ₂₂s) | yes refl | yes refl
-- -- --  with EqVecTerm⇓ τ₁s τ₂s | EqVecTerm⇓ τ₁₂s τ₂₂s
-- -- -- … | (no τ₁s≢τ₂s , τ⇓) | (no τ₁₂s≢τ₂₂s , τs⇓) = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ now⇓
-- -- -- … | (yes refl , τ⇓)   | (no τ₁₂s≢τ₂₂s , τs⇓) = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ (τs⇓ >>=⇓ now⇓)
-- -- -- … | (no τ₁s≢τ₂s , τ⇓) | (yes refl , τs⇓) = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ now⇓
-- -- -- … | (yes refl , τ⇓)   | (yes refl , τs⇓) = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ (τs⇓ >>=⇓ now⇓)

-- -- -- EqTerms⇓ : (x y : Terms) → EqTerms⇑ x y ⇓
-- -- -- EqTerms⇓ (⟨_⟩ {𝑎₁} τ₁s) (⟨_⟩ {𝑎₂} τ₂s)
-- -- --  with 𝑎₁ ≟ 𝑎₂
-- -- -- … | no 𝑎₁≢𝑎₂ = _ , now⇓
-- -- -- … | yes refl
-- -- --  with EqVecTerm⇓ τ₁s τ₂s
-- -- -- … | (yes refl , τ⇓) = _ , τ⇓ >>=⇓ now⇓
-- -- -- … | (no _ , τ⇓) = _ , τ⇓ >>=⇓ now⇓

-- -- -- EqTerm⇓ : (x y : Term) → EqTerm⇑ x y ⇓
-- -- -- EqTerm⇓ (variable x) (variable x₁) = _ , now⇓
-- -- -- EqTerm⇓ (function _ τ₁s) (function _ τ₂s)
-- -- --  with EqTerms⇓ τ₁s τ₂s
-- -- -- … | (_ , τ⇓) = _ , τ⇓ >>=⇓ now⇓
-- -- -- EqTerm⇓ (variable x) (function x₁ x₂) = _ , now⇓
-- -- -- EqTerm⇓ (function x x₁) (variable x₂) = _ , now⇓

-- -- -- instance EqTerm : Eq Term
-- -- -- EqTerm = record { _==_ = λ x y → fst (EqTerm⇓ x y) }

-- -- -- instance EqTerms : Eq Terms
-- -- -- Eq._==_ EqTerms x y = fst (EqTerms⇓ x y)

-- -- -- mutual

-- -- --   τ⇑⟦_⟧ : Interpretation → {i : Size} → Term → Delay i Element
-- -- --   τ⇑⟦ I ⟧ (variable 𝑥) = now $ μ⟦ I ⟧ 𝑥
-- -- --   τ⇑⟦ I ⟧ (function 𝑓 τs) = 𝑓⟦ I ⟧ 𝑓 ∘ ⟨_⟩ <$> τs⇑⟦ I ⟧ τs

-- -- --   τs⇑⟦_⟧ : Interpretation → {i : Size} → (τs : Terms) → Delay i (Vector Element (arity τs))
-- -- --   τs⇑⟦ I ⟧ ⟨ [] ⟩ = now []
-- -- --   τs⇑⟦ I ⟧ ⟨ τ ∷ τs ⟩ = τ⇑⟦ I ⟧ τ >>= (λ t → τs⇑⟦ I ⟧ ⟨ τs ⟩ >>= λ ts → now (t ∷ ts))

-- -- -- τs⇓⟦_⟧ : (I : Interpretation) → (τs : Terms) → τs⇑⟦ I ⟧ τs ⇓
-- -- -- τs⇓⟦ I ⟧ ⟨ [] ⟩ = _ , now⇓
-- -- -- τs⇓⟦ I ⟧ ⟨ variable 𝑥 ∷ τs ⟩ = _ , τs⇓⟦ I ⟧ ⟨ τs ⟩ ⇓>>=⇓ now⇓
-- -- -- τs⇓⟦ I ⟧ ⟨ function 𝑓₁ τs₁ ∷ τs₂ ⟩ =
-- -- --   _ , τs⇓⟦ I ⟧ τs₁ ⇓>>=⇓ now⇓ >>=⇓ (τs⇓⟦ I ⟧ ⟨ τs₂ ⟩ ⇓>>=⇓ now⇓)

-- -- -- τ⇓⟦_⟧ : (I : Interpretation) → (τ : Term) → τ⇑⟦ I ⟧ τ ⇓
-- -- -- τ⇓⟦ I ⟧ (variable 𝑥) = _ , now⇓
-- -- -- τ⇓⟦ I ⟧ (function 𝑓 τs) = _ , τs⇓⟦ I ⟧ τs ⇓>>=⇓ now⇓

-- -- -- τ⟦_⟧ : (I : Interpretation) → {i : Size} → (τ : Term) → Element
-- -- -- τ⟦ I ⟧ τ = fst (τ⇓⟦ I ⟧ τ)

-- -- -- data Formula : Set
-- -- --  where
-- -- --   atomic : PredicateName → Terms → Formula
-- -- --   logical : Formula →
-- -- --             Formula →
-- -- --             Formula
-- -- --   quantified : VariableName → Formula → Formula

-- -- -- formulaAtomic-inj₁ : ∀ {𝑃₁ τs₁ 𝑃₂ τs₂} → Formula.atomic 𝑃₁ τs₁ ≡ atomic 𝑃₂ τs₂ → 𝑃₁ ≡ 𝑃₂
-- -- -- formulaAtomic-inj₁ refl = refl

-- -- -- formulaAtomic-inj₂ : ∀ {𝑃₁ τs₁ 𝑃₂ τs₂} → Formula.atomic 𝑃₁ τs₁ ≡ atomic 𝑃₂ τs₂ → τs₁ ≡ τs₂
-- -- -- formulaAtomic-inj₂ refl = refl

-- -- -- formulaLogical-inj₁ : ∀ {φ₁₁ φ₁₂ φ₂₁ φ₂₂} → Formula.logical φ₁₁ φ₁₂ ≡ logical φ₂₁ φ₂₂ → φ₁₁ ≡ φ₂₁
-- -- -- formulaLogical-inj₁ refl = refl

-- -- -- formulaLogical-inj₂ : ∀ {φ₁₁ φ₁₂ φ₂₁ φ₂₂} → Formula.logical φ₁₁ φ₁₂ ≡ logical φ₂₁ φ₂₂ → φ₁₂ ≡ φ₂₂
-- -- -- formulaLogical-inj₂ refl = refl

-- -- -- formulaQuantified-inj₁ : ∀ {𝑥₁ φ₁ 𝑥₂ φ₂} → Formula.quantified 𝑥₁ φ₁ ≡ quantified 𝑥₂ φ₂ → 𝑥₁ ≡ 𝑥₂
-- -- -- formulaQuantified-inj₁ refl = refl

-- -- -- formulaQuantified-inj₂ : ∀ {𝑥₁ φ₁ 𝑥₂ φ₂} → Formula.quantified 𝑥₁ φ₁ ≡ quantified 𝑥₂ φ₂ → φ₁ ≡ φ₂
-- -- -- formulaQuantified-inj₂ refl = refl

-- -- -- instance EqFormula : Eq Formula
-- -- -- Eq._==_ EqFormula (atomic 𝑃₁ τs₁) (atomic 𝑃₂ τs₂)  = decEq₂ formulaAtomic-inj₁ formulaAtomic-inj₂ (𝑃₁ ≟ 𝑃₂) (τs₁ ≟ τs₂)
-- -- -- Eq._==_ EqFormula (logical φ₁₁ φ₁₂) (logical φ₂₁ φ₂₂)  = decEq₂ formulaLogical-inj₁ formulaLogical-inj₂ (φ₁₁ ≟ φ₂₁) (φ₁₂ ≟ φ₂₂)
-- -- -- Eq._==_ EqFormula (quantified 𝑥₁ φ₁) (quantified 𝑥₂ φ₂)  = decEq₂ formulaQuantified-inj₁ formulaQuantified-inj₂ (𝑥₁ ≟ 𝑥₂) (φ₁ ≟ φ₂)
-- -- -- Eq._==_ EqFormula (atomic _ _) (logical _ _) = no λ ()
-- -- -- Eq._==_ EqFormula (atomic _ _) (quantified _ _) = no λ ()
-- -- -- Eq._==_ EqFormula (logical _ _) (atomic _ _)  = no λ ()
-- -- -- Eq._==_ EqFormula (logical _ _) (quantified _ _)  = no λ ()
-- -- -- Eq._==_ EqFormula (quantified _ _) (atomic _ _)  = no λ ()
-- -- -- Eq._==_ EqFormula (quantified _ _) (logical _ _)  = no λ ()

-- -- -- record HasNegation (A : Set) : Set
-- -- --  where
-- -- --   field
-- -- --     ~ : A → A

-- -- -- open HasNegation ⦃ … ⦄

-- -- -- record BeFormula (A : Set) : Set
-- -- --  where
-- -- --   constructor ⟨_⟩
-- -- --   field
-- -- --     formula : A → Formula

-- -- -- open BeFormula ⦃ … ⦄

-- -- -- record HasSatisfaction (A : Set) : Set₁
-- -- --  where
-- -- --   field
-- -- --     _⊨_ : Interpretation → A → Set

-- -- --   _⊭_ : Interpretation → A → Set
-- -- --   _⊭_ I = ¬_ ∘ I ⊨_

-- -- -- open HasSatisfaction ⦃ … ⦄

-- -- -- record HasDecidableSatisfaction (A : Set) ⦃ _ : HasSatisfaction A ⦄ : Set₁
-- -- --  where
-- -- --   field
-- -- --     _⊨?_ : (I : Interpretation) → (x : A) → Dec (I ⊨ x)

-- -- -- open HasDecidableSatisfaction ⦃ … ⦄

-- -- -- infix 15 _╱_
-- -- -- record Sequent (A : Set) ⦃ _ : BeFormula A ⦄ : Set
-- -- --  where
-- -- --   constructor _╱_
-- -- --   field
-- -- --     statement : A
-- -- --     suppositions : List A

-- -- -- open Sequent

-- -- -- foooo : {A : Set} ⦃ bf : BeFormula A ⦄ {-⦃ hs : HasNegation A ⦄-} (x : Sequent A) →
-- -- --       Dec
-- -- --       (-- Either
-- -- --        (Σ A
-- -- --         (λ x₁ →
-- -- --            --Σ
-- -- --            ({-BeFormula.formula bf -}x₁ ∈
-- -- --             {-map (BeFormula.formula bf)-} (suppositions x))
-- -- --            {-
-- -- --            (λ _ →
-- -- --              ⊤
-- -- --               --BeFormula.formula bf (HasNegation.~ hs x₁) ∈
-- -- --               --map (BeFormula.formula bf) (suppositions x)
-- -- --               )-}
-- -- --            ))
-- -- --        {-(BeFormula.formula bf (statement x) ∈
-- -- --         map (BeFormula.formula bf) (suppositions x))-})
-- -- -- foooo (statement₁ ╱ []) = no (λ {x → {!x!}})
-- -- -- foooo (statement₁ ╱ (x ∷ suppositions₁)) = {!!}

-- -- -- -- record HasValidation (A : Set) : Set₁
-- -- -- --  where
-- -- -- --   field
-- -- -- --     ⊨_ : A → Set

-- -- -- --   ⊭_ : A → Set
-- -- -- --   ⊭_ = ¬_ ∘ ⊨_

-- -- -- -- open HasValidation ⦃ … ⦄

-- -- -- -- 𝑃[_♭_] : PredicateName → Terms → Formula
-- -- -- -- 𝑃[_♭_] = atomic

-- -- -- -- _⊗_ : Formula → Formula → Formula
-- -- -- -- _⊗_ = logical

-- -- -- -- instance

-- -- -- --   HasNegationFormula : HasNegation Formula
-- -- -- --   HasNegation.~ HasNegationFormula φ = φ ⊗ φ

-- -- -- -- data IsLiteral : Formula → Set
-- -- -- --  where
-- -- -- --   atomic : (𝑃 : PredicateName) → (τs : Terms) → IsLiteral $ 𝑃[ 𝑃 ♭ τs ]
-- -- -- --   logical : (𝑃 : PredicateName) → (τs : Terms) → IsLiteral ∘ ~ $ 𝑃[ 𝑃 ♭ τs ]

-- -- -- -- eqIsLiteral : ∀ {φ} → (lf₁ lf₂ : IsLiteral φ) → lf₁ ≡ lf₂
-- -- -- -- eqIsLiteral (atomic 𝑃 τs) (atomic .𝑃 .τs) = refl
-- -- -- -- eqIsLiteral (logical 𝑃 τs) (logical .𝑃 .τs) = refl

-- -- -- -- instance EqIsLiteral : ∀ {φ} → Eq (IsLiteral φ)
-- -- -- -- Eq._==_ EqIsLiteral lf₁ lf₂ = yes (eqIsLiteral lf₁ lf₂)

-- -- -- -- record LiteralFormula : Set
-- -- -- --  where
-- -- -- --   constructor ⟨_⟩
-- -- -- --   field
-- -- -- --     {formula} : Formula
-- -- -- --     isLiteral : IsLiteral formula

-- -- -- -- open LiteralFormula

-- -- -- -- instance EqLiteralFormula : Eq LiteralFormula
-- -- -- -- Eq._==_ EqLiteralFormula (⟨_⟩ {φ₁} lf₁) (⟨_⟩ {φ₂} lf₂)
-- -- -- --  with φ₁ ≟ φ₂
-- -- -- -- … | no φ₁≢φ₂ = no (λ {refl → φ₁≢φ₂ refl})
-- -- -- -- Eq._==_ EqLiteralFormula (⟨_⟩ {φ₁} lf₁) (⟨_⟩ {φ₂} lf₂) | yes refl = case (eqIsLiteral lf₁ lf₂) of λ {refl → yes refl}

-- -- -- -- infix 13 _¶_
-- -- -- -- record Problem (A : Set) ⦃ _ : BeFormula A ⦄ : Set
-- -- -- --  where
-- -- -- --   constructor _¶_
-- -- -- --   field
-- -- -- --     inferences : List (Sequent A)
-- -- -- --     interest : Sequent A

-- -- -- -- open Problem

-- -- -- -- record HasSubstantiveDischarge (+ : Set) (- : Set) : Set₁
-- -- -- --  where
-- -- -- --   field
-- -- -- --     _≽_ : + → - → Set

-- -- -- -- open HasSubstantiveDischarge ⦃ … ⦄

-- -- -- -- record HasVacuousDischarge (+ : Set) : Set₁
-- -- -- --  where
-- -- -- --   field
-- -- -- --     ◁_ : + → Set

-- -- -- -- open HasVacuousDischarge ⦃ … ⦄

-- -- -- -- record HasSalvation (A : Set) : Set₁
-- -- -- --  where
-- -- -- --   field
-- -- -- --     {isVacuouslyDischargable} : Set
-- -- -- --     ⦃ hasVacuousDischarge ⦄ : HasVacuousDischarge isVacuouslyDischargable
-- -- -- --     ▷_ : A → Set

-- -- -- -- open HasSalvation ⦃ … ⦄

-- -- -- -- record HasDecidableSalvation (A : Set) : Set₁
-- -- -- --  where
-- -- -- --   field
-- -- -- --     ⦃ hasSalvation ⦄ : HasSalvation A
-- -- -- --     ▷?_ : (x : A) → Dec $ ▷_ x

-- -- -- -- open HasDecidableSalvation ⦃ … ⦄

-- -- -- -- ∀[_♭_] : VariableName → Formula → Formula
-- -- -- -- ∀[_♭_] = quantified

-- -- -- -- _∧_ : Formula → Formula → Formula
-- -- -- -- φ₁ ∧ φ₂ = ~ φ₁ ⊗ ~ φ₂

-- -- -- -- _∨_ : Formula → Formula → Formula
-- -- -- -- φ₁ ∨ φ₂ = ~ (φ₁ ⊗ φ₂)

-- -- -- -- _⊃_ : Formula → Formula → Formula
-- -- -- -- φ₁ ⊃ φ₂ = ~ φ₁ ∨ φ₂

-- -- -- -- _⟷_ : Formula → Formula → Formula
-- -- -- -- φ₁ ⟷ φ₂ = (φ₁ ⊗ (φ₂ ⊗ φ₂)) ⊗ ((φ₁ ⊗ φ₁) ⊗ φ₂) -- TODO check that this is logically equivalent to the more verbose, (φ₁ ⊃ φ₂) ∧ (φ₂ ⊃ φ₁)

-- -- -- -- record _≞_/_ (𝓘 : Interpretation) (I : Interpretation) (𝑥 : VariableName) : Set
-- -- -- --  where
-- -- -- --   field
-- -- -- --     μEquality : {𝑥′ : VariableName} → 𝑥′ ≢ 𝑥 → μ⟦ 𝓘 ⟧ 𝑥 ≡ μ⟦ I ⟧ 𝑥′
-- -- -- --     𝑓Equality : (𝑓 : FunctionName) (μs : Elements) → 𝑓⟦ 𝓘 ⟧ 𝑓 μs ≡ 𝑓⟦ I ⟧ 𝑓 μs
-- -- -- --     𝑃Equality : (𝑃 : PredicateName) → (μs : Elements) → 𝑃⟦ 𝓘 ⟧ 𝑃 μs ≡ 𝑃⟦ I ⟧ 𝑃 μs

-- -- -- -- instance

-- -- -- --   BeFormulaFormula : BeFormula Formula
-- -- -- --   BeFormula.formula BeFormulaFormula = id

-- -- -- --   BeFormulaLiteralFormula : BeFormula LiteralFormula
-- -- -- --   BeFormula.formula BeFormulaLiteralFormula = formula

-- -- -- -- instance

-- -- -- --   HasNegationLiteralFormula : HasNegation LiteralFormula
-- -- -- --   HasNegation.~ HasNegationLiteralFormula ⟨ atomic 𝑃 τs ⟩ = ⟨ logical 𝑃 τs ⟩
-- -- -- --   HasNegation.~ HasNegationLiteralFormula ⟨ logical 𝑃 τs ⟩ = ⟨ atomic 𝑃 τs ⟩

-- -- -- --   HasNegationSequent : {A : Set} ⦃ _ : HasNegation A ⦄ ⦃ _ : BeFormula A ⦄ → HasNegation $ Sequent A
-- -- -- --   HasNegation.~ HasNegationSequent ( φᵗ ╱ φˢs ) = ~ φᵗ ╱ φˢs

-- -- -- -- instance

-- -- -- --   HasSatisfactionList : {A : Set} ⦃ _ : HasSatisfaction A ⦄ → HasSatisfaction $ List A
-- -- -- --   HasSatisfaction._⊨_ HasSatisfactionList I [] = ⊤
-- -- -- --   HasSatisfaction._⊨_ HasSatisfactionList I (x ∷ xs) = I ⊨ x × I ⊨ xs

-- -- -- --   HasSatisfactionBeFormula : {A : Set} → ⦃ _ : BeFormula A ⦄ → HasSatisfaction A
-- -- -- --   HasSatisfaction._⊨_ (HasSatisfactionBeFormula ⦃ beFormula ⦄) = λ I φ → I ⊨φ formula beFormula φ
-- -- -- --    where
-- -- -- --     _⊨φ_ : Interpretation → Formula → Set
-- -- -- --     I ⊨φ (atomic 𝑃 τs) = 𝑃⟦ I ⟧ 𝑃 ⟨ τ⟦ I ⟧ <$> terms τs ⟩ ≡ true
-- -- -- --     I ⊨φ (logical φ₁ φ₂) = ¬ I ⊨φ φ₁ × ¬ I ⊨φ φ₂
-- -- -- --     I ⊨φ (quantified 𝑥 φ) = (𝓘 : Interpretation) → 𝓘 ≞ I / 𝑥 → 𝓘 ⊨φ φ

-- -- -- --   HasSatisfactionSequent : {A : Set} ⦃ _ : BeFormula A ⦄ → HasSatisfaction $ Sequent A
-- -- -- --   HasSatisfaction._⊨_ HasSatisfactionSequent I (φᵗ ╱ φˢs) = I ⊨ φˢs → I ⊨ φᵗ

-- -- -- -- instance
-- -- -- --   postulate
-- -- -- --     HasDecidableSatisfactionFormula : HasDecidableSatisfaction Formula

-- -- -- -- instance

-- -- -- --   HasValidationBeFormula : {A : Set} ⦃ _ : BeFormula A ⦄ → HasValidation A
-- -- -- --   HasValidation.⊨_ HasValidationBeFormula φ = (I : Interpretation) → I ⊨ φ

-- -- -- --   HasValidationSequent : {A : Set} ⦃ _ : BeFormula A ⦄ → HasValidation $ Sequent A
-- -- -- --   HasValidation.⊨_ HasValidationSequent Φ = (I : Interpretation) → I ⊨ Φ

-- -- -- --   HasValidationProblem : {A : Set} ⦃ _ : BeFormula A ⦄ → HasValidation $ Problem A
-- -- -- --   HasValidation.⊨_ HasValidationProblem (χs ¶ ι) = (I : Interpretation) → I ⊨ χs → I ⊨ ι

-- -- -- -- instance

-- -- -- --   HasSubstantiveDischargeBeFormulaBeFormula : {A : Set} ⦃ _ : BeFormula A ⦄ → HasSubstantiveDischarge A A
-- -- -- --   HasSubstantiveDischarge._≽_ (HasSubstantiveDischargeBeFormulaBeFormula ⦃ ⟨ beFormula ⟩ ⦄) = _≡_ on beFormula -- _≡_ on (formula beFormula) -- _≡_

-- -- -- --   HasSubstantiveDischargeListBeFormulaBeFormula : {A : Set} ⦃ _ : BeFormula A ⦄ → HasSubstantiveDischarge (List A) A
-- -- -- --   HasSubstantiveDischarge._≽_ (HasSubstantiveDischargeListBeFormulaBeFormula ⦃ ⟨ beFormula ⟩ ⦄) +s - = beFormula - ∈ (beFormula <$> +s) -- flip _∈_

-- -- -- --   HasSubstantiveDischargeListFormulaListFormula : {A : Set} ⦃ _ : BeFormula A ⦄ → HasSubstantiveDischarge (List A) (List A)
-- -- -- --   HasSubstantiveDischarge._≽_ (HasSubstantiveDischargeListFormulaListFormula ⦃ ⟨ beFormula ⟩ ⦄) = flip $ _⊆_ on fmap beFormula -- flip _⊆_

-- -- -- --   HasSubstantiveDischargeSequentSequent : ∀ {A : Set} ⦃ _ : BeFormula A ⦄ → HasSubstantiveDischarge (Sequent A) (Sequent A)
-- -- -- --   HasSubstantiveDischarge._≽_ HasSubstantiveDischargeSequentSequent (+ᵗ ╱ +ᵖs) (-ᵗ ╱ -ᵖs) = +ᵗ ≽ -ᵗ × +ᵖs ≽ -ᵖs

-- -- -- --   HasSubstantiveDischargeListSequentSequent : ∀ {A : Set} ⦃ _ : BeFormula A ⦄ → HasSubstantiveDischarge (List $ Sequent A) (Sequent A)
-- -- -- --   HasSubstantiveDischarge._≽_ HasSubstantiveDischargeListSequentSequent χs ι = ∃ λ c → (c ∈ χs) × c ≽ ι

-- -- -- -- instance

-- -- -- --   HasVacuousDischargeList : {A : Set} ⦃ _ : HasSubstantiveDischarge (List A) A ⦄ ⦃ _ : HasNegation A ⦄ → HasVacuousDischarge (List A)
-- -- -- --   HasVacuousDischarge.◁_ (HasVacuousDischargeList {A}) xs = ∃ λ (x : A) → xs ≽ x × xs ≽ ~ x

-- -- -- --   HasVacuousDischargeSequent : {A : Set} ⦃ _ : BeFormula A ⦄ ⦃ _ : HasNegation A ⦄ → HasVacuousDischarge (Sequent A)
-- -- -- --   HasVacuousDischarge.◁_ HasVacuousDischargeSequent (_ ╱ φˢs) = ∃ λ s → (s ∈ φˢs) × (φˢs ≽ s) × (φˢs ≽ ~ s)

-- -- -- -- instance

-- -- -- --   HasSalvationSequent : {A : Set} ⦃ _ : BeFormula A ⦄ ⦃ _ : HasNegation A ⦄ {-⦃ _ : HasVacuousDischarge $ List A ⦄-} → HasSalvation $ Sequent A
-- -- -- --   HasSalvation.isVacuouslyDischargable (HasSalvationSequent {A}) = List A
-- -- -- --   HasSalvation.hasVacuousDischarge HasSalvationSequent = HasVacuousDischargeList
-- -- -- --   HasSalvation.▷_ HasSalvationSequent (φᵗ ╱ φᵖs) = (◁ φᵖs) ⊎ (φᵖs ≽ φᵗ)

-- -- -- -- HasDecidableSalvationSequent : {A : Set} ⦃ bf : BeFormula A ⦄ ⦃ hs : HasNegation A ⦄
-- -- -- --                                → HasDecidableSalvation $ Sequent A
-- -- -- -- HasDecidableSalvation.hasSalvation HasDecidableSalvationSequent = HasSalvationSequent
-- -- -- -- --(HasDecidableSalvation.▷? HasDecidableSalvationSequent) (statement₁ ╱ []) = no (foo2 statement₁)
-- -- -- -- HasDecidableSalvation.▷? HasDecidableSalvationSequent = {!!}
-- -- -- -- --(HasDecidableSalvation.▷? HasDecidableSalvationSequent) (statement₁ ╱ []) = no (λ {x → {!!}})
-- -- -- -- --(HasDecidableSalvation.▷? HasDecidableSalvationSequent) (statement₁ ╱ (x₂ ∷ suppositions₁)) = {!!}

-- -- -- -- -- foo1 : ∀ {A} → ⦃ b : BeFormula A ⦄ ⦃ _ : HasNegation A ⦄ (statement₁ : A) → Σ A
-- -- -- -- --       (λ x →
-- -- -- -- --          Σ (BeFormula.formula b x ∈ [])
-- -- -- -- --          (λ _ → BeFormula.formula b (~ x) ∈ []))
-- -- -- -- --       ⊎ (BeFormula.formula b statement₁ ∈ []) →
-- -- -- -- --       ⊥
-- -- -- -- -- foo1 statement₁ (left (fst₁ , () , snd₁))
-- -- -- -- -- foo1 statement₁ (right ())

-- -- -- -- -- foo2 : ∀ {A} → ⦃ b : BeFormula A ⦄ ⦃ _ : HasNegation A ⦄ (statement₁ : A) → ▷ (statement₁ ╱ []) →
-- -- -- -- --       ⊥
-- -- -- -- -- foo2 statement₁ (left (fst₁ , () , snd₁))
-- -- -- -- -- foo2 statement₁ (right ())

ext: agda


text:
------------------------------------------------------------------------
-- Split surjections
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Equality

module Surjection
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open Derived-definitions-and-properties eq
open import Logical-equivalence
  using (_⇔_; module _⇔_) renaming (_∘_ to _⊙_)
open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)

------------------------------------------------------------------------
-- Split surjections

-- The property of being a split surjection.

Split-surjective :
  ∀ {a b} {A : Type a} {B : Type b} → (A → B) → Type (a ⊔ b)
Split-surjective f = ∀ y → ∃ λ x → f x ≡ y

infix 0 _↠_

-- Split surjections. Note that in this development split surjections
-- are often called simply "surjections".

record _↠_ {f t} (From : Type f) (To : Type t) : Type (f ⊔ t) where
  field
    logical-equivalence : From ⇔ To

  open _⇔_ logical-equivalence

  field
    right-inverse-of : ∀ x → to (from x) ≡ x

  -- A lemma.

  from-to : ∀ {x y} → from x ≡ y → to y ≡ x
  from-to {x} {y} from-x≡y =
    to y         ≡⟨ cong to $ sym from-x≡y ⟩
    to (from x)  ≡⟨ right-inverse-of x ⟩∎
    x            ∎

  -- The to function is split surjective.

  split-surjective : Split-surjective to
  split-surjective = λ y → from y , right-inverse-of y

  -- Every left inverse of to is pointwise equal to from.

  left-inverse-unique :
    (f : To → From) →
    (∀ x → f (to x) ≡ x) →
    (∀ x → f x ≡ from x)
  left-inverse-unique f left x =
    f x              ≡⟨ cong f $ sym $ right-inverse-of _ ⟩
    f (to (from x))  ≡⟨ left _ ⟩∎
    from x           ∎

  -- Every right inverse of from is pointwise equal to to.

  right-inverse-of-from-unique :
    (f : From → To) →
    (∀ x → from (f x) ≡ x) →
    (∀ x → f x ≡ to x)
  right-inverse-of-from-unique _ right x = sym $ from-to (right x)

  open _⇔_ logical-equivalence public

------------------------------------------------------------------------
-- Preorder

-- _↠_ is a preorder.

id : ∀ {a} {A : Type a} → A ↠ A
id = record
  { logical-equivalence = Logical-equivalence.id
  ; right-inverse-of    = refl
  }

infixr 9 _∘_

_∘_ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} →
      B ↠ C → A ↠ B → A ↠ C
f ∘ g = record
  { logical-equivalence = logical-equivalence f ⊙ logical-equivalence g
  ; right-inverse-of    = to∘from
  }
  where
  open _↠_

  to∘from : ∀ x → to f (to g (from g (from f x))) ≡ x
  to∘from = λ x →
    to f (to g (from g (from f x)))  ≡⟨ cong (to f) (right-inverse-of g (from f x)) ⟩
    to f (from f x)                  ≡⟨ right-inverse-of f x ⟩∎
    x                                ∎

-- "Equational" reasoning combinators.

infix  -1 finally-↠
infixr -2 step-↠

-- For an explanation of why step-↠ is defined in this way, see
-- Equality.step-≡.

step-↠ : ∀ {a b c} (A : Type a) {B : Type b} {C : Type c} →
         B ↠ C → A ↠ B → A ↠ C
step-↠ _ = _∘_

syntax step-↠ A B↠C A↠B = A ↠⟨ A↠B ⟩ B↠C

finally-↠ : ∀ {a b} (A : Type a) (B : Type b) → A ↠ B → A ↠ B
finally-↠ _ _ A↠B = A↠B

syntax finally-↠ A B A↠B = A ↠⟨ A↠B ⟩□ B □

------------------------------------------------------------------------
-- Some preservation/respectfulness lemmas

-- ∃ preserves surjections.

∃-cong :
  ∀ {a b₁ b₂} {A : Type a} {B₁ : A → Type b₁} {B₂ : A → Type b₂} →
  (∀ x → B₁ x ↠ B₂ x) → ∃ B₁ ↠ ∃ B₂
∃-cong {B₁ = B₁} {B₂} B₁↠B₂ = record
  { logical-equivalence = record
    { to   = to′
    ; from = from′
    }
  ; right-inverse-of = right-inverse-of′
  }
  where
  open _↠_

  to′ : ∃ B₁ → ∃ B₂
  to′ = Σ-map P.id (to (B₁↠B₂ _))

  from′ : ∃ B₂ → ∃ B₁
  from′ = Σ-map P.id (from (B₁↠B₂ _))

  right-inverse-of′ : ∀ p → to′ (from′ p) ≡ p
  right-inverse-of′ = λ p →
    cong (_,_ (proj₁ p)) (right-inverse-of (B₁↠B₂ (proj₁ p)) _)

-- A preservation lemma involving Σ, _↠_ and _⇔_.

Σ-cong-⇔ :
  ∀ {a₁ a₂ b₁ b₂} {A₁ : Type a₁} {A₂ : Type a₂}
    {B₁ : A₁ → Type b₁} {B₂ : A₂ → Type b₂}
  (A₁↠A₂ : A₁ ↠ A₂) → (∀ x → B₁ x ⇔ B₂ (_↠_.to A₁↠A₂ x)) →
  Σ A₁ B₁ ⇔ Σ A₂ B₂
Σ-cong-⇔ {B₂ = B₂} A₁↠A₂ B₁⇔B₂ = record
  { to   = Σ-map (_↠_.to A₁↠A₂) (_⇔_.to (B₁⇔B₂ _))
  ; from =
     Σ-map
       (_↠_.from A₁↠A₂)
       (λ {x} y → _⇔_.from
                    (B₁⇔B₂ (_↠_.from A₁↠A₂ x))
                    (subst B₂ (sym (_↠_.right-inverse-of A₁↠A₂ x)) y))
  }

-- A generalisation of ∃-cong.

Σ-cong :
  ∀ {a₁ a₂ b₁ b₂} {A₁ : Type a₁} {A₂ : Type a₂}
    {B₁ : A₁ → Type b₁} {B₂ : A₂ → Type b₂}
  (A₁↠A₂ : A₁ ↠ A₂) → (∀ x → B₁ x ↠ B₂ (_↠_.to A₁↠A₂ x)) →
  Σ A₁ B₁ ↠ Σ A₂ B₂
Σ-cong {A₁ = A₁} {A₂} {B₁} {B₂} A₁↠A₂ B₁↠B₂ = record
  { logical-equivalence = logical-equivalence′
  ; right-inverse-of    = right-inverse-of′
  }
  where
  open _↠_

  logical-equivalence′ : Σ A₁ B₁ ⇔ Σ A₂ B₂
  logical-equivalence′ = Σ-cong-⇔ A₁↠A₂ (logical-equivalence ⊚ B₁↠B₂)

  abstract
    right-inverse-of′ :
      ∀ p →
      _⇔_.to logical-equivalence′ (_⇔_.from logical-equivalence′ p) ≡ p
    right-inverse-of′ = λ p → Σ-≡,≡→≡
      (_↠_.right-inverse-of A₁↠A₂ (proj₁ p))
      (subst B₂ (_↠_.right-inverse-of A₁↠A₂ (proj₁ p))
         (to (B₁↠B₂ _) (from (B₁↠B₂ _)
            (subst B₂ (sym (_↠_.right-inverse-of A₁↠A₂ (proj₁ p)))
               (proj₂ p))))                                         ≡⟨ cong (subst B₂ _) $ right-inverse-of (B₁↠B₂ _) _ ⟩
       subst B₂ (_↠_.right-inverse-of A₁↠A₂ (proj₁ p))
         (subst B₂ (sym (_↠_.right-inverse-of A₁↠A₂ (proj₁ p)))
            (proj₂ p))                                              ≡⟨ subst-subst-sym B₂ _ _ ⟩∎
       proj₂ p ∎)

-- Π A preserves surjections (assuming extensionality).

∀-cong :
  ∀ {a b₁ b₂} →
  Extensionality a (b₁ ⊔ b₂) →
  {A : Type a} {B₁ : A → Type b₁} {B₂ : A → Type b₂} →
  (∀ x → B₁ x ↠ B₂ x) →
  ((x : A) → B₁ x) ↠ ((x : A) → B₂ x)
∀-cong {b₁ = b₁} ext B₁↠B₂ = record
  { logical-equivalence = equiv
  ; right-inverse-of    = right-inverse-of
  }
  where
  equiv = record
    { to   = (_↠_.to   ⊚ B₁↠B₂) _ ⊚_
    ; from = (_↠_.from ⊚ B₁↠B₂) _ ⊚_
    }

  abstract
    right-inverse-of : ∀ f → _⇔_.to equiv (_⇔_.from equiv f) ≡ f
    right-inverse-of = λ f →
      apply-ext (lower-extensionality lzero b₁ ext) λ x →
        _↠_.to (B₁↠B₂ x) (_↠_.from (B₁↠B₂ x) (f x))  ≡⟨ _↠_.right-inverse-of (B₁↠B₂ x) (f x) ⟩∎
        f x                                          ∎

-- A lemma relating surjections and equality.

↠-≡ : ∀ {a b} {A : Type a} {B : Type b} (A↠B : A ↠ B) {x y : B} →
      (_↠_.from A↠B x ≡ _↠_.from A↠B y) ↠ (x ≡ y)
↠-≡ A↠B {x} {y} = record
  { logical-equivalence = record
    { from = cong from
    ; to   = to′
    }
  ; right-inverse-of = right-inverse-of′
  }
  where
  open _↠_ A↠B

  to′ : from x ≡ from y → x ≡ y
  to′ = λ from-x≡from-y →
    x            ≡⟨ sym $ right-inverse-of _ ⟩
    to (from x)  ≡⟨ cong to from-x≡from-y ⟩
    to (from y)  ≡⟨ right-inverse-of _ ⟩∎
    y            ∎

  abstract
    right-inverse-of′ : ∀ p → to′ (cong from p) ≡ p
    right-inverse-of′ = elim
      (λ {x y} x≡y → trans (sym (right-inverse-of x)) (
                       trans (cong to (cong from x≡y)) (
                       right-inverse-of y)) ≡
                     x≡y)
      (λ x → trans (sym (right-inverse-of x)) (
               trans (cong to (cong from (refl x))) (
               right-inverse-of x))                                 ≡⟨ cong (λ p → trans (sym (right-inverse-of x))
                                                                                (trans (cong to p) (right-inverse-of x)))
                                                                            (cong-refl from) ⟩
             trans (sym (right-inverse-of x)) (
               trans (cong to (refl (from x))) (
               right-inverse-of x))                                 ≡⟨ cong (λ p → trans (sym (right-inverse-of x))
                                                                                (trans p (right-inverse-of x)))
                                                                            (cong-refl to) ⟩
             trans (sym (right-inverse-of x)) (
               trans (refl (to (from x))) (
               right-inverse-of x))                                 ≡⟨ cong (trans (sym _)) (trans-reflˡ _) ⟩
             trans (sym (right-inverse-of x)) (right-inverse-of x)  ≡⟨ trans-symˡ _ ⟩∎
             refl x                                                 ∎)

-- A "computation rule" for ↠-≡.

to-↠-≡-refl :
  ∀ {a b} {A : Type a} {B : Type b} (A↠B : A ↠ B) {x : B} →
  _↠_.to (↠-≡ A↠B) (refl (_↠_.from A↠B x)) ≡ refl x
to-↠-≡-refl A↠B {x = x} =
  trans (sym $ _↠_.right-inverse-of A↠B x)
    (trans (cong (_↠_.to A↠B) (refl (_↠_.from A↠B x)))
       (_↠_.right-inverse-of A↠B x))                    ≡⟨ cong (λ p → trans _ (trans p _)) $ cong-refl _ ⟩

  trans (sym $ _↠_.right-inverse-of A↠B x)
    (trans (refl (_↠_.to A↠B (_↠_.from A↠B x)))
       (_↠_.right-inverse-of A↠B x))                    ≡⟨ cong (trans _) $ trans-reflˡ _ ⟩

  trans (sym $ _↠_.right-inverse-of A↠B x)
    (_↠_.right-inverse-of A↠B x)                        ≡⟨ trans-symˡ _ ⟩∎

  refl x                                                ∎

-- Decidable-equality respects surjections.

Decidable-equality-respects :
  ∀ {a b} {A : Type a} {B : Type b} →
  A ↠ B → Decidable-equality A → Decidable-equality B
Decidable-equality-respects A↠B _≟A_ x y =
  ⊎-map (to (↠-≡ A↠B))
        (λ from-x≢from-y → from-x≢from-y ⊚ from (↠-≡ A↠B))
        (from A↠B x ≟A from A↠B y)
  where open _↠_

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Homotopy.Whitehead where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.HITs.Susp renaming (toSusp to σ)
open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.Join
open import Cubical.HITs.Wedge
open import Cubical.HITs.SetTruncation

open import Cubical.Homotopy.Group.Base

open Iso
open 3x3-span

joinTo⋁ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
 → join (typ A) (typ B)
 → (Susp (typ A) , north) ⋁ (Susp (typ B) , north)
joinTo⋁ (inl x) = inr north
joinTo⋁ (inr x) = inl north
joinTo⋁ {A = A} {B = B} (push a b i) =
     ((λ i → inr (σ B b i))
  ∙∙ sym (push tt)
  ∙∙ λ i → inl (σ A a i)) i

-- Whitehead product (main definition)
[_∣_] : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
       → (S₊∙ (suc n) →∙ X)
       → (S₊∙ (suc m) →∙ X)
       → S₊∙ (suc (n + m)) →∙ X
fst ([_∣_] {X = X} {n = n} {m = m} f g) x =
  _∨→_ (f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n))
        (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m))
        (joinTo⋁ {A = S₊∙ n} {B = S₊∙ m}
          (inv (IsoSphereJoin n m) x))
snd ([_∣_] {n = n} {m = m} f g) =
  cong (_∨→_ (f ∘∙ (inv (IsoSucSphereSusp n) , IsoSucSphereSusp∙ n))
       (g ∘∙ (inv (IsoSucSphereSusp m) , IsoSucSphereSusp∙ m)))
       (cong (joinTo⋁ {A = S₊∙ n} {B = S₊∙ m}) (IsoSphereJoin⁻Pres∙ n m))
    ∙ cong (fst g) (IsoSucSphereSusp∙ m)
    ∙ snd g

-- For Sⁿ, Sᵐ with n, m ≥ 2, we can avoid some bureaucracy. We make
-- a separate definition and prove it equivalent.
[_∣_]-pre : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
       → (S₊∙ (suc (suc n)) →∙ X)
       → (S₊∙ (suc (suc m)) →∙ X)
       → join (typ (S₊∙ (suc n))) (typ (S₊∙ (suc m))) → fst X
[_∣_]-pre {n = n} {m = m} f g x =
  _∨→_ f g
        (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)}
        x)

[_∣_]₂ : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
       → (S₊∙ (suc (suc n)) →∙ X)
       → (S₊∙ (suc (suc m)) →∙ X)
       → S₊∙ (suc ((suc n) + (suc m))) →∙ X
fst ([_∣_]₂ {n = n} {m = m} f g) x =
  [ f ∣ g ]-pre (inv (IsoSphereJoin (suc n) (suc m)) x)
snd ([_∣_]₂ {n = n} {m = m} f g) =
    cong ([ f ∣ g ]-pre) (IsoSphereJoin⁻Pres∙ (suc n) (suc m))
  ∙ snd g

[]≡[]₂ : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
       → (f : (S₊∙ (suc (suc n)) →∙ X))
       → (g : (S₊∙ (suc (suc m)) →∙ X))
       → [ f ∣ g ] ≡ [ f ∣ g ]₂
[]≡[]₂ {n = n} {m = m} f g =
  ΣPathP (
    (λ i x → _∨→_ (∘∙-idˡ f i)
                    (∘∙-idˡ g i)
                (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)}
                 (inv (IsoSphereJoin (suc n) (suc m)) x)))
  , (cong (cong (_∨→_ (f ∘∙ idfun∙ _)
                       (g ∘∙ idfun∙ _))
       (cong (joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)})
             (IsoSphereJoin⁻Pres∙ (suc n) (suc m))) ∙_)
                (sym (lUnit (snd g)))
  ◁ λ j → (λ i → _∨→_ (∘∙-idˡ f j)
                        (∘∙-idˡ g j)
           ( joinTo⋁ {A = S₊∙ (suc n)} {B = S₊∙ (suc m)}
          ((IsoSphereJoin⁻Pres∙ (suc n) (suc m)) i))) ∙ snd g))

-- Homotopy group version
[_∣_]π' : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
       → π' (suc n) X → π' (suc m) X
       → π' (suc (n + m)) X
[_∣_]π' = elim2 (λ _ _ → squash₂) λ f g → ∣ [ f ∣ g ] ∣₂

-- We prove that the function joinTo⋁ used in the definition of the whitehead
-- product gives an equivalence between (Susp A × Susp B) and the
-- appropriate cofibre of joinTo⋁ (last two theorems in the following
-- module).

module _ (A B : Type) (a₀ : A) (b₀ : B) where
  private
    W = joinTo⋁ {A = (A , a₀)} {B = (B , b₀)}

  A∨B = (Susp A , north) ⋁ (Susp B , north)

  σB = σ (B , b₀)
  σA = σ (A , a₀)

  cofibW = Pushout W λ _ → tt

  whitehead3x3 :  3x3-span
  A00 whitehead3x3 = Susp A
  A02 whitehead3x3 = B
  A04 whitehead3x3 = Unit
  A20 whitehead3x3 = B
  A22 whitehead3x3 = A × B
  A24 whitehead3x3 = A
  A40 whitehead3x3 = B
  A42 whitehead3x3 = B
  A44 whitehead3x3 = Unit
  f10 whitehead3x3 _ = south
  f12 whitehead3x3 = snd
  f14 whitehead3x3 _ = tt
  f30 whitehead3x3 = idfun B
  f32 whitehead3x3 = snd
  f34 whitehead3x3 _ = tt
  f01 whitehead3x3 _ = north
  f21 whitehead3x3 = snd
  f41 whitehead3x3 = idfun B
  f03 whitehead3x3 _ = tt
  f23 whitehead3x3 = fst
  f43 whitehead3x3 _ = tt
  H11 whitehead3x3 x = merid (fst x)
  H13 whitehead3x3 _ = refl
  H31 whitehead3x3 _ = refl
  H33 whitehead3x3 _ = refl

  A0□→A∨B : A0□ whitehead3x3 → A∨B
  A0□→A∨B (inl x) = inl x
  A0□→A∨B (inr x) = inr north
  A0□→A∨B (push a i) = (push tt ∙ λ i → inr (σB a (~ i))) i

  A∨B→A0□ : A∨B → A0□ whitehead3x3
  A∨B→A0□ (inl x) = inl x
  A∨B→A0□ (inr north) = inl north
  A∨B→A0□ (inr south) = inl north
  A∨B→A0□ (inr (merid b i)) = (push b₀ ∙ sym (push b)) i
  A∨B→A0□ (push a i) = inl north

  Iso-A0□-⋁ : Iso (A0□ whitehead3x3) A∨B
  fun Iso-A0□-⋁ = A0□→A∨B
  inv Iso-A0□-⋁ = A∨B→A0□
  rightInv Iso-A0□-⋁ (inl x) = refl
  rightInv Iso-A0□-⋁ (inr north) = push tt
  rightInv Iso-A0□-⋁ (inr south) = push tt ∙ λ i → inr (merid b₀ i)
  rightInv Iso-A0□-⋁ (inr (merid a i)) j = lem j i
    where
    lem : PathP (λ i → push tt i ≡ (push tt ∙ (λ i → inr (merid b₀ i))) i)
              (cong A0□→A∨B (cong A∨B→A0□ λ i → inr (merid a i)))
              (λ i → inr (merid a i))
    lem = (cong-∙ A0□→A∨B (push b₀) (sym (push a))
      ∙ cong₂ _∙_ (cong (push tt ∙_)
                  (λ j i → inr (rCancel (merid b₀) j (~ i)))
                 ∙ sym (rUnit (push tt)))
                  (symDistr (push tt) (λ i → inr (σB a (~ i)))))
      ◁ λ i j → hcomp (λ k →
                  λ { (i = i0) → compPath-filler' (push tt)
                                 (compPath-filler (λ i → inr (σB a i))
                                                  (sym (push tt)) k) k j
                    ; (i = i1) → inr (merid a j)
                    ; (j = i0) → push tt (i ∨ ~ k)
                    ; (j = i1) → compPath-filler' (push tt)
                                                  (λ i → inr (merid b₀ i)) k i})
                        (inr (compPath-filler (merid a)
                                              (sym (merid b₀)) (~ i) j))

  rightInv Iso-A0□-⋁ (push a i) j = push tt (i ∧ j)
  leftInv Iso-A0□-⋁ (inl x) = refl
  leftInv Iso-A0□-⋁ (inr tt) = push b₀
  leftInv Iso-A0□-⋁ (push b i) j = help j i
    where
    help : PathP (λ i → inl north ≡ push b₀ i)
                 (cong A∨B→A0□ (cong A0□→A∨B (push b)))
                 (push b)
    help = (cong-∙ A∨B→A0□ (push tt) (λ i → inr (σB b (~ i)))
         ∙ (λ i → lUnit (sym (cong-∙ (A∨B→A0□ ∘ inr)
                               (merid b) (sym (merid b₀)) i)) (~ i))
         ∙ cong sym (cong ((push b₀ ∙ sym (push b)) ∙_)
                      (cong sym (rCancel (push b₀))))
         ∙ cong sym (sym (rUnit (push b₀ ∙ sym (push b)))))
         ◁ λ i j → compPath-filler' (push b₀) (sym (push b)) (~ i) (~ j)

  Iso-A2□-join : Iso (A2□ whitehead3x3) (join A B)
  fun Iso-A2□-join (inl x) = inr x
  fun Iso-A2□-join (inr x) = inl x
  fun Iso-A2□-join (push (a , b) i) = push a b (~ i)
  inv Iso-A2□-join (inl x) = inr x
  inv Iso-A2□-join (inr x) = inl x
  inv Iso-A2□-join (push a b i) = push (a , b) (~ i)
  rightInv Iso-A2□-join (inl x) = refl
  rightInv Iso-A2□-join (inr x) = refl
  rightInv Iso-A2□-join (push a b i) = refl
  leftInv Iso-A2□-join (inl x) = refl
  leftInv Iso-A2□-join (inr x) = refl
  leftInv Iso-A2□-join (push a i) = refl

  isContrA4□ : isContr (A4□ whitehead3x3)
  fst isContrA4□ = inr tt
  snd isContrA4□ (inl x) = sym (push x)
  snd isContrA4□ (inr x) = refl
  snd isContrA4□ (push a i) j = push a (i ∨ ~ j)

  A4□≃Unit : A4□ whitehead3x3 ≃ Unit
  A4□≃Unit = isContr→≃Unit isContrA4□

  Iso-A□0-Susp : Iso (A□0 whitehead3x3) (Susp A)
  fun Iso-A□0-Susp (inl x) = x
  fun Iso-A□0-Susp (inr x) = north
  fun Iso-A□0-Susp (push a i) = merid a₀ (~ i)
  inv Iso-A□0-Susp x = inl x
  rightInv Iso-A□0-Susp x = refl
  leftInv Iso-A□0-Susp (inl x) = refl
  leftInv Iso-A□0-Susp (inr x) = (λ i → inl (merid a₀ i)) ∙ push x
  leftInv Iso-A□0-Susp (push a i) j =
    hcomp (λ k → λ { (i = i0) → inl (merid a₀ (k ∨ j))
                    ; (i = i1) → compPath-filler
                                   (λ i₁ → inl (merid a₀ i₁))
                                   (push (idfun B a)) k j
                    ; (j = i0) → inl (merid a₀ (~ i ∧ k))
                    ; (j = i1) → push a (i ∧ k)})
          (inl (merid a₀ j))

  Iso-A□2-Susp× : Iso (A□2 whitehead3x3) (Susp A × B)
  fun Iso-A□2-Susp× (inl x) = north , x
  fun Iso-A□2-Susp× (inr x) = south , x
  fun Iso-A□2-Susp× (push a i) = merid (fst a) i , (snd a)
  inv Iso-A□2-Susp× (north , y) = inl y
  inv Iso-A□2-Susp× (south , y) = inr y
  inv Iso-A□2-Susp× (merid a i , y) = push (a , y) i
  rightInv Iso-A□2-Susp× (north , snd₁) = refl
  rightInv Iso-A□2-Susp× (south , snd₁) = refl
  rightInv Iso-A□2-Susp× (merid a i , snd₁) = refl
  leftInv Iso-A□2-Susp× (inl x) = refl
  leftInv Iso-A□2-Susp× (inr x) = refl
  leftInv Iso-A□2-Susp× (push a i) = refl

  Iso-A□4-Susp : Iso (A□4 whitehead3x3) (Susp A)
  fun Iso-A□4-Susp (inl x) = north
  fun Iso-A□4-Susp (inr x) = south
  fun Iso-A□4-Susp (push a i) = merid a i
  inv Iso-A□4-Susp north = inl tt
  inv Iso-A□4-Susp south = inr tt
  inv Iso-A□4-Susp (merid a i) = push a i
  rightInv Iso-A□4-Susp north = refl
  rightInv Iso-A□4-Susp south = refl
  rightInv Iso-A□4-Susp (merid a i) = refl
  leftInv Iso-A□4-Susp (inl x) = refl
  leftInv Iso-A□4-Susp (inr x) = refl
  leftInv Iso-A□4-Susp (push a i) = refl

  Iso-PushSusp×-Susp×Susp :
    Iso (Pushout {A = Susp A × B} fst fst) (Susp A × Susp B)
  Iso-PushSusp×-Susp×Susp = theIso
    where
    F : Pushout {A = Susp A × B} fst fst
     → Susp A × Susp B
    F (inl x) = x , north
    F (inr x) = x , north
    F (push (x , b) i) = x , σB b i

    G : Susp A × Susp B → Pushout {A = Susp A × B} fst fst
    G (a , north) = inl a
    G (a , south) = inr a
    G (a , merid b i) = push (a , b) i

    retr : retract F G
    retr (inl x) = refl
    retr (inr x) = push (x , b₀)
    retr (push (a , b) i) j = help j i
      where
      help : PathP (λ i → Path (Pushout fst fst) (inl a) (push (a , b₀) i))
                   (cong G (λ i → a , σB b i))
                   (push (a , b))
      help = cong-∙ (λ x → G (a , x)) (merid b) (sym (merid b₀))
                  ◁ λ i j → compPath-filler
                               (push (a , b))
                               (sym (push (a , b₀)))
                               (~ i) j

    theIso : Iso (Pushout fst fst) (Susp A × Susp B)
    fun theIso = F
    inv theIso = G
    rightInv theIso (a , north) = refl
    rightInv theIso (a , south) = ΣPathP (refl , merid b₀)
    rightInv theIso (a , merid b i) j =
      a , compPath-filler (merid b) (sym (merid b₀)) (~ j) i
    leftInv theIso = retr

  Iso-A□○-PushSusp× :
    Iso (A□○ whitehead3x3) (Pushout {A = Susp A × B} fst fst)
  Iso-A□○-PushSusp× =
    pushoutIso _ _ fst fst
      (isoToEquiv Iso-A□2-Susp×)
      (isoToEquiv Iso-A□0-Susp)
      (isoToEquiv Iso-A□4-Susp)
      (funExt (λ { (inl x) → refl
                 ; (inr x) → merid a₀
                 ; (push a i) j → help₁ a j i}))
      (funExt λ { (inl x) → refl
                ; (inr x) → refl
                ; (push a i) j
                  → fun Iso-A□4-Susp (rUnit (push (fst a)) (~ j) i)})
    where
    help₁ : (a : A × B)
      → PathP (λ i → north ≡ merid a₀ i)
               (cong (fun Iso-A□0-Susp)
                 (cong (f□1 whitehead3x3) (push a)))
               (merid (fst a))
    help₁ a =
        (cong-∙∙ (fun Iso-A□0-Susp)
                 (λ i → inl (merid (fst a) i))
                 (push (snd a))
                 refl)
      ◁ (λ i j → hcomp (λ k → λ {(i = i1) → merid (fst a) (j ∨ ~ k)
                                 ; (j = i0) → merid (fst a) (~ k)
                                 ; (j = i1) → merid a₀ i})
                        (merid a₀ (i ∨ ~ j)))

  Iso-A□○-Susp×Susp : Iso (A□○ whitehead3x3) (Susp A × Susp B)
  Iso-A□○-Susp×Susp = compIso Iso-A□○-PushSusp× Iso-PushSusp×-Susp×Susp

  Iso-A○□-cofibW : Iso (A○□ whitehead3x3) cofibW
  Iso-A○□-cofibW =
    pushoutIso _ _
      W (λ _ → tt)
      (isoToEquiv Iso-A2□-join) (isoToEquiv Iso-A0□-⋁)
      A4□≃Unit
      (funExt lem)
      λ _ _ → tt
    where
    lem : (x : A2□ whitehead3x3)
      → A0□→A∨B (f1□ whitehead3x3 x) ≡ W (fun Iso-A2□-join x)
    lem (inl x) = (λ i → inl (merid a₀ (~ i)))
    lem (inr x) = refl
    lem (push (a , b) i) j = help j i
      where
      help : PathP (λ i → Path (Pushout (λ _ → north) (λ _ → north))
                                ((inl (merid a₀ (~ i))))
                                (inr north))
                   (cong A0□→A∨B (cong (f1□ whitehead3x3) (push (a , b))))
                   (cong W (cong (fun Iso-A2□-join) (push (a , b))))
      help = (cong-∙∙ A0□→A∨B (λ i → inl (merid a (~ i))) (push b) refl
            ∙ λ j → (λ i₂ → inl (merid a (~ i₂)))
                   ∙∙ compPath-filler (push tt) (λ i → inr (σB b (~ i))) (~ j)
                   ∙∙ λ i → inr (σB b (~ i ∧ j)))
           ◁ (λ j → (λ i → inl (sym (compPath-filler
                                       (merid a) (sym (merid a₀)) j) i))
                   ∙∙ push tt
                   ∙∙ λ i → inr (σB b (~ i)))

  Iso₁-Susp×Susp-cofibW : Iso (Susp A × Susp B) cofibW
  Iso₁-Susp×Susp-cofibW =
    compIso (invIso Iso-A□○-Susp×Susp)
            (compIso (3x3-Iso whitehead3x3) Iso-A○□-cofibW)

  -- Main iso
  Iso-Susp×Susp-cofibJoinTo⋁ : Iso (Susp A × Susp B) cofibW
  Iso-Susp×Susp-cofibJoinTo⋁ =
    compIso (Σ-cong-iso-snd (λ _ → invSuspIso))
            Iso₁-Susp×Susp-cofibW

  -- The induced function A ∨ B → Susp A × Susp B satisfies
  -- the following identity
  Susp×Susp→cofibW≡ : Path (A∨B → Susp A × Susp B)
                      (Iso.inv Iso-Susp×Susp-cofibJoinTo⋁ ∘ inl)
                      ⋁↪
  Susp×Susp→cofibW≡ =
    funExt λ { (inl x) → ΣPathP (refl , (sym (merid b₀)))
             ; (inr north) → ΣPathP (refl , (sym (merid b₀)))
             ; (inr south) → refl
             ; (inr (merid a i)) j → lem₂ a j i
             ; (push a i) j → north , (merid b₀ (~ j))}
    where
    f₁ = fun Iso-PushSusp×-Susp×Susp
    f₂ = fun Iso-A□○-PushSusp×
    f₃ = backward-l whitehead3x3
    f₄ = fun (Σ-cong-iso-snd (λ _ → invSuspIso))

    lem : (b : B)
      → cong (f₁ ∘ f₂ ∘ f₃) (push b)
      ≡ (λ i → north , σB b i)
    lem b = cong (cong f₁) (sym (rUnit (push (north , b))))

    lem₂ : (a : B)
      → PathP (λ i → (north , merid b₀ (~ i)) ≡ (north , south))
               (cong (f₄ ∘ f₁ ∘ f₂ ∘ f₃ ∘ A∨B→A0□ ∘ inr) (merid a))
               λ i → north , merid a i
    lem₂ a =
         cong (cong f₄) (cong-∙ (f₁ ∘ f₂ ∘ f₃) (push b₀) (sym (push a))
      ∙∙ cong₂ _∙_ (lem b₀ ∙ (λ j i → north , rCancel (merid b₀) j i))
                   (cong sym (lem a))
      ∙∙ sym (lUnit (λ i₁ → north , σB a (~ i₁))))
       ∙ (λ i j → north , cong-∙ invSusp (merid a) (sym (merid b₀)) i (~ j) )
        ◁ λ i j → north , compPath-filler (sym (merid a)) (merid b₀) (~ i) (~ j)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical