text:
------------------------------------------------------------------------
-- Some definitions related to and properties of natural numbers
------------------------------------------------------------------------

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

open import Equality

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

import Agda.Builtin.Bool
import Agda.Builtin.Nat

open import Logical-equivalence using (_⇔_)
open import Prelude

open Derived-definitions-and-properties eq

------------------------------------------------------------------------
-- A helper function

private

  -- Converts builtin booleans to Bool.

  Bool→Bool : Agda.Builtin.Bool.Bool → Bool
  Bool→Bool Agda.Builtin.Bool.true  = true
  Bool→Bool Agda.Builtin.Bool.false = false

------------------------------------------------------------------------
-- Equality of natural numbers is decidable

-- Inhabited only for zero.

Zero : ℕ → Type
Zero zero    = ⊤
Zero (suc n) = ⊥

-- Predecessor (except if the argument is zero).

pred : ℕ → ℕ
pred zero    = zero
pred (suc n) = n

abstract

  -- Zero is not equal to the successor of any number.

  0≢+ : {n : ℕ} → zero ≢ suc n
  0≢+ 0≡+ = subst Zero 0≡+ tt

-- The suc constructor is cancellative.

cancel-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n
cancel-suc = cong pred

-- Equality of natural numbers is decidable.

infix 4 _≟_

_≟_ : Decidable-equality ℕ
zero  ≟ zero  = yes (refl _)
suc m ≟ suc n = ⊎-map (cong suc) (λ m≢n → m≢n ∘ cancel-suc) (m ≟ n)
zero  ≟ suc n = no 0≢+
suc m ≟ zero  = no (0≢+ ∘ sym)

-- An equality test that is likely to be more efficient.

infix 4 _==_

_==_ : ℕ → ℕ → Bool
m == n = Bool→Bool (m Agda.Builtin.Nat.== n)

------------------------------------------------------------------------
-- Inequality

-- Inequality.

Distinct : ℕ → ℕ → Type
Distinct zero    zero    = ⊥
Distinct zero    (suc _) = ⊤
Distinct (suc _) zero    = ⊤
Distinct (suc m) (suc n) = Distinct m n

-- Distinct is pointwise logically equivalent to _≢_.

Distinct⇔≢ : {m n : ℕ} → Distinct m n ⇔ m ≢ n
Distinct⇔≢ = record { to = to _ _; from = from _ _ }
  where
  to : ∀ m n → Distinct m n → m ≢ n
  to zero    zero    ()
  to zero    (suc n) _   = 0≢+
  to (suc m) zero    _   = 0≢+ ∘ sym
  to (suc m) (suc n) m≢n = to m n m≢n ∘ cancel-suc

  from : ∀ m n → m ≢ n → Distinct m n
  from zero    zero    0≢0     = 0≢0 (refl 0)
  from zero    (suc n) _       = _
  from (suc m) zero    _       = _
  from (suc m) (suc n) 1+m≢1+n = from m n (1+m≢1+n ∘ cong suc)

-- Two natural numbers are either equal or distinct.

≡⊎Distinct : ∀ m n → m ≡ n ⊎ Distinct m n
≡⊎Distinct m n = ⊎-map id (_⇔_.from Distinct⇔≢) (m ≟ n)

------------------------------------------------------------------------
-- Properties related to _+_

-- Addition is associative.

+-assoc : ∀ m {n o} → m + (n + o) ≡ (m + n) + o
+-assoc zero    = refl _
+-assoc (suc m) = cong suc (+-assoc m)

-- Zero is a right additive unit.

+-right-identity : ∀ {n} → n + 0 ≡ n
+-right-identity {zero}  = refl 0
+-right-identity {suc _} = cong suc +-right-identity

-- The successor constructor can be moved from one side of _+_ to the
-- other.

suc+≡+suc : ∀ m {n} → suc m + n ≡ m + suc n
suc+≡+suc zero    = refl _
suc+≡+suc (suc m) = cong suc (suc+≡+suc m)

-- Addition is commutative.

+-comm : ∀ m {n} → m + n ≡ n + m
+-comm zero        = sym +-right-identity
+-comm (suc m) {n} =
  suc (m + n)  ≡⟨ cong suc (+-comm m) ⟩
  suc (n + m)  ≡⟨ suc+≡+suc n ⟩∎
  n + suc m    ∎

-- A number is not equal to a strictly larger number.

≢1+ : ∀ m {n} → ¬ m ≡ suc (m + n)
≢1+ zero    p = 0≢+ p
≢1+ (suc m) p = ≢1+ m (cancel-suc p)

-- Addition is left cancellative.

+-cancellativeˡ : ∀ {m n₁ n₂} → m + n₁ ≡ m + n₂ → n₁ ≡ n₂
+-cancellativeˡ {zero}  = id
+-cancellativeˡ {suc m} = +-cancellativeˡ ∘ cancel-suc

-- Addition is right cancellative.

+-cancellativeʳ : ∀ {m₁ m₂ n} → m₁ + n ≡ m₂ + n → m₁ ≡ m₂
+-cancellativeʳ {m₁} {m₂} {n} hyp = +-cancellativeˡ (
  n + m₁  ≡⟨ +-comm n ⟩
  m₁ + n  ≡⟨ hyp ⟩
  m₂ + n  ≡⟨ +-comm m₂ ⟩∎
  n + m₂  ∎)

------------------------------------------------------------------------
-- Properties related to _*_

-- Zero is a right zero for multiplication.

*-right-zero : ∀ n → n * 0 ≡ 0
*-right-zero zero    = refl 0
*-right-zero (suc n) = *-right-zero n

-- Multiplication is commutative.

*-comm : ∀ m {n} → m * n ≡ n * m
*-comm zero    {n}     = sym (*-right-zero n)
*-comm (suc m) {zero}  = *-right-zero m
*-comm (suc m) {suc n} =
  suc (n + m * suc n)    ≡⟨ cong (suc ∘ (n +_)) (*-comm m) ⟩
  suc (n + suc n * m)    ≡⟨⟩
  suc (n + (m + n * m))  ≡⟨ cong suc (+-assoc n) ⟩
  suc (n + m + n * m)    ≡⟨ cong₂ (λ x y → suc (x + y)) (+-comm n) (sym (*-comm m)) ⟩
  suc (m + n + m * n)    ≡⟨ cong suc (sym (+-assoc m)) ⟩
  suc (m + (n + m * n))  ≡⟨⟩
  suc (m + suc m * n)    ≡⟨ cong (suc ∘ (m +_)) (*-comm (suc m) {n}) ⟩∎
  suc (m + n * suc m)    ∎

-- One is a left identity for multiplication.

*-left-identity : ∀ {n} → 1 * n ≡ n
*-left-identity {n} =
  1 * n     ≡⟨⟩
  n + zero  ≡⟨ +-right-identity ⟩∎
  n         ∎

-- One is a right identity for multiplication.

*-right-identity : ∀ n → n * 1 ≡ n
*-right-identity n =
  n * 1 ≡⟨ *-comm n ⟩
  1 * n ≡⟨ *-left-identity ⟩∎
  n     ∎

-- Multiplication distributes from the left over addition.

*-+-distribˡ : ∀ m {n o} → m * (n + o) ≡ m * n + m * o
*-+-distribˡ zero            = refl _
*-+-distribˡ (suc m) {n} {o} =
  n + o + m * (n + o)        ≡⟨ cong ((n + o) +_) (*-+-distribˡ m) ⟩
  n + o + (m * n + m * o)    ≡⟨ sym (+-assoc n) ⟩
  n + (o + (m * n + m * o))  ≡⟨ cong (n +_) (+-assoc o) ⟩
  n + (o + m * n + m * o)    ≡⟨ cong ((n +_) ∘ (_+ m * o)) (+-comm o) ⟩
  n + (m * n + o + m * o)    ≡⟨ cong (n +_) (sym (+-assoc (m * _))) ⟩
  n + (m * n + (o + m * o))  ≡⟨ +-assoc n ⟩∎
  n + m * n + (o + m * o)    ∎

-- Multiplication distributes from the right over addition.

*-+-distribʳ : ∀ m {n o} → (m + n) * o ≡ m * o + n * o
*-+-distribʳ m {n} {o} =
  (m + n) * o    ≡⟨ *-comm (m + _) ⟩
  o * (m + n)    ≡⟨ *-+-distribˡ o ⟩
  o * m + o * n  ≡⟨ cong₂ _+_ (*-comm o) (*-comm o) ⟩∎
  m * o + n * o  ∎

-- Multiplication is associative.

*-assoc : ∀ m {n k} → m * (n * k) ≡ (m * n) * k
*-assoc zero                    = refl _
*-assoc (suc m) {n = n} {k = k} =
  n * k + m * (n * k)  ≡⟨ cong (n * k +_) $ *-assoc m ⟩
  n * k + (m * n) * k  ≡⟨ sym $ *-+-distribʳ n ⟩∎
  (n + m * n) * k      ∎

-- Multiplication is right cancellative for positive numbers.

*-cancellativeʳ : ∀ {m₁ m₂ n} → m₁ * suc n ≡ m₂ * suc n → m₁ ≡ m₂
*-cancellativeʳ {zero}   {zero}   = λ _ → zero  ∎
*-cancellativeʳ {zero}   {suc _}  = ⊥-elim ∘ 0≢+
*-cancellativeʳ {suc _}  {zero}   = ⊥-elim ∘ 0≢+ ∘ sym
*-cancellativeʳ {suc m₁} {suc m₂} =
  cong suc ∘
  *-cancellativeʳ ∘
  +-cancellativeˡ

-- Multiplication is left cancellative for positive numbers.

*-cancellativeˡ : ∀ m {n₁ n₂} → suc m * n₁ ≡ suc m * n₂ → n₁ ≡ n₂
*-cancellativeˡ m {n₁} {n₂} hyp = *-cancellativeʳ (
  n₁ * suc m  ≡⟨ *-comm n₁ ⟩
  suc m * n₁  ≡⟨ hyp ⟩
  suc m * n₂  ≡⟨ *-comm (suc m) ⟩∎
  n₂ * suc m  ∎)

-- Even numbers are not equal to odd numbers.

even≢odd : ∀ m n → 2 * m ≢ 1 + 2 * n
even≢odd zero    n eq = 0≢+ eq
even≢odd (suc m) n eq =
  even≢odd n m (
    2 * n            ≡⟨ sym $ cancel-suc eq ⟩
    m + 1 * (1 + m)  ≡⟨ sym $ suc+≡+suc m ⟩∎
    1 + 2 * m        ∎)

------------------------------------------------------------------------
-- Properties related to _^_

-- One is a right identity for exponentiation.

^-right-identity : ∀ {n} → n ^ 1 ≡ n
^-right-identity {n} =
  n ^ 1  ≡⟨⟩
  n * 1  ≡⟨ *-right-identity _ ⟩∎
  n      ∎

-- One is a left zero for exponentiation.

^-left-zero : ∀ n → 1 ^ n ≡ 1
^-left-zero zero    = refl _
^-left-zero (suc n) =
  1 ^ suc n  ≡⟨⟩
  1 * 1 ^ n  ≡⟨ *-left-identity ⟩
  1 ^ n      ≡⟨ ^-left-zero n ⟩∎
  1          ∎

-- Some rearrangement lemmas for exponentiation.

^+≡^*^ : ∀ {m} n {k} → m ^ (n + k) ≡ m ^ n * m ^ k
^+≡^*^ {m} zero {k} =
  m ^ k          ≡⟨ sym *-left-identity ⟩
  1 * m ^ k      ≡⟨⟩
  m ^ 0 * m ^ k  ∎
^+≡^*^ {m} (suc n) {k} =
  m ^ (1 + n + k)      ≡⟨⟩
  m * m ^ (n + k)      ≡⟨ cong (m *_) $ ^+≡^*^ n ⟩
  m * (m ^ n * m ^ k)  ≡⟨ *-assoc m ⟩
  m * m ^ n * m ^ k    ≡⟨⟩
  m ^ (1 + n) * m ^ k  ∎

*^≡^*^ : ∀ {m n} k → (m * n) ^ k ≡ m ^ k * n ^ k
*^≡^*^ {m} {n} zero = refl _
*^≡^*^ {m} {n} (suc k) =
  (m * n) ^ suc k            ≡⟨⟩
  m * n * (m * n) ^ k        ≡⟨ cong (m * n *_) $ *^≡^*^ k ⟩
  m * n * (m ^ k * n ^ k)    ≡⟨ sym $ *-assoc m ⟩
  m * (n * (m ^ k * n ^ k))  ≡⟨ cong (m *_) $ *-assoc n ⟩
  m * (n * m ^ k * n ^ k)    ≡⟨ cong (λ x → m * (x * n ^ k)) $ *-comm n ⟩
  m * (m ^ k * n * n ^ k)    ≡⟨ cong (m *_) $ sym $ *-assoc (m ^ k) ⟩
  m * (m ^ k * (n * n ^ k))  ≡⟨ *-assoc m ⟩
  m * m ^ k * (n * n ^ k)    ≡⟨⟩
  m ^ suc k * n ^ suc k      ∎

^^≡^* : ∀ {m} n {k} → (m ^ n) ^ k ≡ m ^ (n * k)
^^≡^* {m} zero    {k} = ^-left-zero k
^^≡^* {m} (suc n) {k} =
  (m ^ (1 + n)) ^ k    ≡⟨⟩
  (m * m ^ n) ^ k      ≡⟨ *^≡^*^ k ⟩
  m ^ k * (m ^ n) ^ k  ≡⟨ cong (m ^ k *_) $ ^^≡^* n ⟩
  m ^ k * m ^ (n * k)  ≡⟨ sym $ ^+≡^*^ k ⟩
  m ^ (k + n * k)      ≡⟨⟩
  m ^ ((1 + n) * k)    ∎

------------------------------------------------------------------------
-- The usual ordering of the natural numbers, along with some
-- properties

-- The ordering.

infix 4 _≤_ _<_

data _≤_ (m n : ℕ) : Type where
  ≤-refl′ : m ≡ n → m ≤ n
  ≤-step′ : ∀ {k} → m ≤ k → suc k ≡ n → m ≤ n

-- Strict inequality.

_<_ : ℕ → ℕ → Type
m < n = suc m ≤ n

-- Some abbreviations.

≤-refl : ∀ {n} → n ≤ n
≤-refl = ≤-refl′ (refl _)

≤-step : ∀ {m n} → m ≤ n → m ≤ suc n
≤-step m≤n = ≤-step′ m≤n (refl _)

-- _≤_ is transitive.

≤-trans : ∀ {m n o} → m ≤ n → n ≤ o → m ≤ o
≤-trans p (≤-refl′ eq)   = subst (_ ≤_) eq p
≤-trans p (≤-step′ q eq) = ≤-step′ (≤-trans p q) eq

-- If m is strictly less than n, then m is less than or equal to n.

<→≤ : ∀ {m n} → m < n → m ≤ n
<→≤ m<n = ≤-trans (≤-step ≤-refl) m<n

-- "Equational" reasoning combinators.

infix  -1 finally-≤ _∎≤
infixr -2 step-≤ step-≡≤ _≡⟨⟩≤_ step-< _<⟨⟩_

_∎≤ : ∀ n → n ≤ n
_ ∎≤ = ≤-refl

-- For an explanation of why step-≤, step-≡≤ and step-< are defined in
-- this way, see Equality.step-≡.

step-≤ : ∀ m {n o} → n ≤ o → m ≤ n → m ≤ o
step-≤ _ n≤o m≤n = ≤-trans m≤n n≤o

syntax step-≤ m n≤o m≤n = m ≤⟨ m≤n ⟩ n≤o

step-≡≤ : ∀ m {n o} → n ≤ o → m ≡ n → m ≤ o
step-≡≤ _ n≤o m≡n = subst (_≤ _) (sym m≡n) n≤o

syntax step-≡≤ m n≤o m≡n = m ≡⟨ m≡n ⟩≤ n≤o

_≡⟨⟩≤_ : ∀ m {n} → m ≤ n → m ≤ n
_ ≡⟨⟩≤ m≤n = m≤n

finally-≤ : ∀ m n → m ≤ n → m ≤ n
finally-≤ _ _ m≤n = m≤n

syntax finally-≤ m n m≤n = m ≤⟨ m≤n ⟩∎ n ∎≤

step-< : ∀ m {n o} → n ≤ o → m < n → m ≤ o
step-< m {n} {o} n≤o m<n =
  m  ≤⟨ <→≤ m<n ⟩
  n  ≤⟨ n≤o ⟩∎
  o  ∎≤

syntax step-< m n≤o m<n = m <⟨ m<n ⟩ n≤o

_<⟨⟩_ : ∀ m {n} → m < n → m ≤ n
_<⟨⟩_ _ = <→≤

-- Some simple lemmas.

zero≤ : ∀ n → zero ≤ n
zero≤ zero    = ≤-refl
zero≤ (suc n) = ≤-step (zero≤ n)

suc≤suc : ∀ {m n} → m ≤ n → suc m ≤ suc n
suc≤suc (≤-refl′ eq)     = ≤-refl′ (cong suc eq)
suc≤suc (≤-step′ m≤n eq) = ≤-step′ (suc≤suc m≤n) (cong suc eq)

suc≤suc⁻¹ : ∀ {m n} → suc m ≤ suc n → m ≤ n
suc≤suc⁻¹ (≤-refl′ eq)   = ≤-refl′ (cancel-suc eq)
suc≤suc⁻¹ (≤-step′ p eq) =
  ≤-trans (≤-step ≤-refl) (subst (_ ≤_) (cancel-suc eq) p)

m≤m+n : ∀ m n → m ≤ m + n
m≤m+n zero    n = zero≤ n
m≤m+n (suc m) n = suc≤suc (m≤m+n m n)

m≤n+m : ∀ m n → m ≤ n + m
m≤n+m m zero    = ≤-refl
m≤n+m m (suc n) = ≤-step (m≤n+m m n)

pred≤ : ∀ n → pred n ≤ n
pred≤ zero    = ≤-refl
pred≤ (suc _) = ≤-step ≤-refl

-- A decision procedure for _≤_.

infix 4 _≤?_

_≤?_ : Decidable _≤_
zero  ≤? n     = inj₁ (zero≤ n)
suc m ≤? zero  = inj₂ λ { (≤-refl′ eq)   → 0≢+ (sym eq)
                        ; (≤-step′ _ eq) → 0≢+ (sym eq)
                        }
suc m ≤? suc n = ⊎-map suc≤suc (λ m≰n → m≰n ∘ suc≤suc⁻¹) (m ≤? n)

-- A comparison operator that is likely to be more efficient than
-- _≤?_.

infix 4 _<=_

_<=_ : ℕ → ℕ → Bool
m <= n = Bool→Bool (m Agda.Builtin.Nat.< suc n)

-- If m is not less than or equal to n, then n is strictly less
-- than m.

≰→> : ∀ {m n} → ¬ m ≤ n → n < m
≰→> {zero}  {n}     p = ⊥-elim (p (zero≤ n))
≰→> {suc m} {zero}  p = suc≤suc (zero≤ m)
≰→> {suc m} {suc n} p = suc≤suc (≰→> (p ∘ suc≤suc))

-- If m is not less than or equal to n, then n is less than or
-- equal to m.

≰→≥ : ∀ {m n} → ¬ m ≤ n → n ≤ m
≰→≥ p = ≤-trans (≤-step ≤-refl) (≰→> p)

-- If m is less than or equal to n, but not equal to n, then m is
-- strictly less than n.

≤≢→< : ∀ {m n} → m ≤ n → m ≢ n → m < n
≤≢→< (≤-refl′ eq)     m≢m   = ⊥-elim (m≢m eq)
≤≢→< (≤-step′ m≤n eq) m≢1+n = subst (_ <_) eq (suc≤suc m≤n)

-- If m is less than or equal to n, then m is strictly less than n or
-- equal to n.

≤→<⊎≡ : ∀ {m n} → m ≤ n → m < n ⊎ m ≡ n
≤→<⊎≡         (≤-refl′ m≡n)               = inj₂ m≡n
≤→<⊎≡ {m} {n} (≤-step′ {k = k} m≤k 1+k≡n) = inj₁ (
  suc m  ≤⟨ suc≤suc m≤k ⟩
  suc k  ≡⟨ 1+k≡n ⟩≤
  n      ∎≤)

-- _≤_ is total.

total : ∀ m n → m ≤ n ⊎ n ≤ m
total m n = ⊎-map id ≰→≥ (m ≤? n)

-- A variant of total.

infix 4 _≤⊎>_

_≤⊎>_ : ∀ m n → m ≤ n ⊎ n < m
m ≤⊎> n = ⊎-map id ≰→> (m ≤? n)

-- Another variant of total.

infix 4 _<⊎≡⊎>_

_<⊎≡⊎>_ : ∀ m n → m < n ⊎ m ≡ n ⊎ n < m
m <⊎≡⊎> n = case m ≤⊎> n of λ where
  (inj₂ n<m) → inj₂ (inj₂ n<m)
  (inj₁ m≤n) → ⊎-map id inj₁ (≤→<⊎≡ m≤n)

-- A number is not strictly greater than a smaller (strictly or not)
-- number.

+≮ : ∀ m {n} → ¬ m + n < n
+≮ m {n}     (≤-refl′ q)           = ≢1+ n (n            ≡⟨ sym q ⟩
                                            suc (m + n)  ≡⟨ cong suc (+-comm m) ⟩∎
                                            suc (n + m)  ∎)
+≮ m {zero}  (≤-step′ {k = k} p q) = 0≢+ (0      ≡⟨ sym q ⟩∎
                                          suc k  ∎)
+≮ m {suc n} (≤-step′ {k = k} p q) = +≮ m {n} (suc m + n  ≡⟨ suc+≡+suc m ⟩≤
                                               m + suc n  <⟨ p ⟩
                                               k          ≡⟨ cancel-suc q ⟩≤
                                               n          ∎≤)

-- No number is strictly less than zero.

≮0 : ∀ n → ¬ n < zero
≮0 n = +≮ n ∘ subst (_< 0) (sym +-right-identity)

-- _<_ is irreflexive.

<-irreflexive : ∀ {n} → ¬ n < n
<-irreflexive = +≮ 0

-- If m is strictly less than n, then m is not equal to n.

<→≢ : ∀ {m n} → m < n → m ≢ n
<→≢ m<n m≡n = <-irreflexive (subst (_< _) m≡n m<n)

-- Antisymmetry.

≤-antisymmetric : ∀ {m n} → m ≤ n → n ≤ m → m ≡ n
≤-antisymmetric         (≤-refl′ q₁)             _                        = q₁
≤-antisymmetric         _                        (≤-refl′ q₂)             = sym q₂
≤-antisymmetric {m} {n} (≤-step′ {k = k₁} p₁ q₁) (≤-step′ {k = k₂} p₂ q₂) =
  ⊥-elim (<-irreflexive (
    suc k₁  ≡⟨ q₁ ⟩≤
    n       ≤⟨ p₂ ⟩
    k₂      <⟨⟩
    suc k₂  ≡⟨ q₂ ⟩≤
    m       ≤⟨ p₁ ⟩
    k₁      ∎≤))

-- If n is less than or equal to pred n, then n is equal to zero.

≤pred→≡zero : ∀ {n} → n ≤ pred n → n ≡ zero
≤pred→≡zero {zero}  _   = refl _
≤pred→≡zero {suc n} n<n = ⊥-elim (+≮ 0 n<n)

-- The pred function is monotone.

pred-mono : ∀ {m n} → m ≤ n → pred m ≤ pred n
pred-mono         (≤-refl′ m≡n)               = ≤-refl′ (cong pred m≡n)
pred-mono {m} {n} (≤-step′ {k = k} m≤k 1+k≡n) =
  pred m  ≤⟨ pred-mono m≤k ⟩
  pred k  ≤⟨ pred≤ _ ⟩
  k       ≡⟨ cong pred 1+k≡n ⟩≤
  pred n  ∎≤

-- _+_ is monotone.

infixl 6 _+-mono_

_+-mono_ : ∀ {m₁ m₂ n₁ n₂} → m₁ ≤ m₂ → n₁ ≤ n₂ → m₁ + n₁ ≤ m₂ + n₂
_+-mono_ {m₁} {m₂} {n₁} {n₂} (≤-refl′ eq) q =
  m₁ + n₁  ≡⟨ cong (_+ _) eq ⟩≤
  m₂ + n₁  ≤⟨ lemma m₂ q ⟩∎
  m₂ + n₂  ∎≤
  where
  lemma : ∀ m {n k} → n ≤ k → m + n ≤ m + k
  lemma zero    p = p
  lemma (suc m) p = suc≤suc (lemma m p)
_+-mono_ {m₁} {m₂} {n₁} {n₂} (≤-step′ {k = k} p eq) q =
  m₁ + n₁     ≤⟨ p +-mono q ⟩
  k + n₂      ≤⟨ ≤-step (_ ∎≤) ⟩
  suc k + n₂  ≡⟨ cong (_+ _) eq ⟩≤
  m₂ + n₂     ∎≤

-- _*_ is monotone.

infixl 7 _*-mono_

_*-mono_ : ∀ {m₁ m₂ n₁ n₂} → m₁ ≤ m₂ → n₁ ≤ n₂ → m₁ * n₁ ≤ m₂ * n₂
_*-mono_ {zero}          _ _ = zero≤ _
_*-mono_ {suc _} {zero}  p q = ⊥-elim (≮0 _ p)
_*-mono_ {suc _} {suc _} p q = q +-mono suc≤suc⁻¹ p *-mono q

-- 1 is less than or equal to positive natural numbers raised to any
-- power.

1≤+^ : ∀ {m} n → 1 ≤ suc m ^ n
1≤+^ {m} zero    = ≤-refl
1≤+^ {m} (suc n) =
  1                          ≡⟨⟩≤
  1 + 0                      ≤⟨ 1≤+^ n +-mono zero≤ _ ⟩
  suc m ^ n + m * suc m ^ n  ∎≤

private

  -- _^_ is not monotone.

  ¬-^-mono : ¬ (∀ {m₁ m₂ n₁ n₂} → m₁ ≤ m₂ → n₁ ≤ n₂ → m₁ ^ n₁ ≤ m₂ ^ n₂)
  ¬-^-mono mono = ≮0 _ (
    1      ≡⟨⟩≤
    0 ^ 0  ≤⟨ mono (≤-refl {n = 0}) (zero≤ 1) ⟩
    0 ^ 1  ≡⟨⟩≤
    0      ∎≤)

-- _^_ is monotone for positive bases.

infixr 8 _⁺^-mono_

_⁺^-mono_ : ∀ {m₁ m₂ n₁ n₂} →
            suc m₁ ≤ m₂ → n₁ ≤ n₂ → suc m₁ ^ n₁ ≤ m₂ ^ n₂
_⁺^-mono_ {m₁} {m₂ = suc m₂} {n₁ = zero} {n₂} _ _ =
  suc m₁ ^ 0   ≡⟨⟩≤
  1            ≤⟨ 1≤+^ n₂ ⟩
  suc m₂ ^ n₂  ∎≤
_⁺^-mono_ {m₁} {m₂} {suc n₁} {suc n₂} p q =
  suc m₁ * suc m₁ ^ n₁  ≤⟨ p *-mono p ⁺^-mono suc≤suc⁻¹ q ⟩
  m₂     * m₂     ^ n₂  ∎≤
_⁺^-mono_ {m₂ = zero}              p _ = ⊥-elim (≮0 _ p)
_⁺^-mono_ {n₁ = suc _} {n₂ = zero} _ q = ⊥-elim (≮0 _ q)

-- _^_ is monotone for positive exponents.

infixr 8 _^⁺-mono_

_^⁺-mono_ : ∀ {m₁ m₂ n₁ n₂} →
            m₁ ≤ m₂ → suc n₁ ≤ n₂ → m₁ ^ suc n₁ ≤ m₂ ^ n₂
_^⁺-mono_ {zero}  _ _ = zero≤ _
_^⁺-mono_ {suc _} p q = p ⁺^-mono q

-- A natural number raised to a positive power is greater than or
-- equal to the number.

≤^+ : ∀ {m} n → m ≤ m ^ suc n
≤^+ {m} n =
  m          ≡⟨ sym ^-right-identity ⟩≤
  m ^ 1      ≤⟨ ≤-refl {n = m} ^⁺-mono suc≤suc (zero≤ n) ⟩
  m ^ suc n  ∎≤

-- The result of _! is always positive.

1≤! : ∀ n → 1 ≤ n !
1≤! zero    = ≤-refl
1≤! (suc n) =
  1            ≡⟨⟩≤
  1     * 1    ≤⟨ suc≤suc (zero≤ n) *-mono 1≤! n ⟩
  suc n * n !  ≡⟨⟩≤
  suc n !      ∎≤

-- _! is monotone.

infix 9 _!-mono

_!-mono : ∀ {m n} → m ≤ n → m ! ≤ n !
_!-mono {zero}  {n}     _ = 1≤! n
_!-mono {suc m} {zero}  p = ⊥-elim (≮0 _ p)
_!-mono {suc m} {suc n} p =
  suc m * m !  ≤⟨ p *-mono suc≤suc⁻¹ p !-mono ⟩
  suc n * n !  ∎≤

-- An eliminator corresponding to well-founded induction.

well-founded-elim :
  ∀ {p}
  (P : ℕ → Type p) →
  (∀ m → (∀ {n} → n < m → P n) → P m) →
  ∀ m → P m
well-founded-elim P p m = helper (suc m) ≤-refl
  where
  helper : ∀ m {n} → n < m → P n
  helper zero    n<0                           = ⊥-elim (≮0 _ n<0)
  helper (suc m) (≤-step′ {k = k} n<k 1+k≡1+m) =
    helper m (subst (_ <_) (cancel-suc 1+k≡1+m) n<k)
  helper (suc m) (≤-refl′ 1+n≡1+m) =
    subst P (sym (cancel-suc 1+n≡1+m)) (p m (helper m))

-- The accessibility relation for _<_.

data Acc (n : ℕ) : Type where
  acc : (∀ {m} → m < n → Acc m) → Acc n

-- Every natural number is accessible.

accessible : ∀ n → Acc n
accessible = well-founded-elim _ λ _ → acc

------------------------------------------------------------------------
-- An alternative definition of the ordering

-- The following ordering can be used to define a function by
-- recursion up to some bound (see the example below).

infix 4 _≤↑_

data _≤↑_ (m n : ℕ) : Type where
  ≤↑-refl : m ≡ n → m ≤↑ n
  ≤↑-step : suc m ≤↑ n → m ≤↑ n

-- The successor function preserves _≤↑_.

suc≤↑suc : ∀ {m n} → m ≤↑ n → suc m ≤↑ suc n
suc≤↑suc (≤↑-refl m≡n)    = ≤↑-refl (cong suc m≡n)
suc≤↑suc (≤↑-step 1+m≤↑n) = ≤↑-step (suc≤↑suc 1+m≤↑n)

-- Functions that convert between _≤_ and _≤↑_.

≤→≤↑ : ∀ {m n} → m ≤ n → m ≤↑ n
≤→≤↑ (≤-refl′ m≡n)               = ≤↑-refl m≡n
≤→≤↑ (≤-step′ {k = k} m≤k 1+k≡n) =
  subst (_ ≤↑_) 1+k≡n (≤↑-step (suc≤↑suc (≤→≤↑ m≤k)))

≤↑→≤ : ∀ {m n} → m ≤↑ n → m ≤ n
≤↑→≤ (≤↑-refl m≡n)    = ≤-refl′ m≡n
≤↑→≤ (≤↑-step 1+m≤↑n) = <→≤ (≤↑→≤ 1+m≤↑n)

private

  -- An example: The list up-to n consists of all natural numbers from
  -- 0 to n, inclusive.

  up-to : ℕ → List ℕ
  up-to bound = helper 0 (≤→≤↑ (zero≤ bound))
    where
    helper : ∀ n → n ≤↑ bound → List ℕ
    helper n (≤↑-refl _) = n ∷ []
    helper n (≤↑-step p) = n ∷ helper _ p

-- An eliminator wrapping up the technique used in the example above.

up-to-elim :
  ∀ {p}
  (P : ℕ → Type p) →
  ∀ n →
  P n →
  (∀ m → m < n → P (suc m) → P m) →
  P 0
up-to-elim P n Pn P<n = helper 0 (≤→≤↑ (zero≤ n))
  where
  helper : ∀ m → m ≤↑ n → P m
  helper m (≤↑-refl m≡n) = subst P (sym m≡n) Pn
  helper m (≤↑-step m<n) = P<n m (≤↑→≤ m<n) (helper (suc m) m<n)

private

  -- The example, expressed using the eliminator.

  up-to′ : ℕ → List ℕ
  up-to′ bound =
    up-to-elim (const _) bound (bound ∷ []) (λ n _ → n ∷_)

------------------------------------------------------------------------
-- Another alternative definition of the ordering

-- This ordering relation is defined by recursion on the numbers.

infix 4 _≤→_

_≤→_ : ℕ → ℕ → Type
zero  ≤→ _     = ⊤
suc m ≤→ zero  = ⊥
suc m ≤→ suc n = m ≤→ n

-- Functions that convert between _≤_ and _≤→_.

≤→≤→ : ∀ m n → m ≤ n → m ≤→ n
≤→≤→ zero    _       _ = _
≤→≤→ (suc m) zero    p = ≮0 _ p
≤→≤→ (suc m) (suc n) p = ≤→≤→ m n (suc≤suc⁻¹ p)

≤→→≤ : ∀ m n → m ≤→ n → m ≤ n
≤→→≤ zero    n       _  = zero≤ n
≤→→≤ (suc m) zero    ()
≤→→≤ (suc m) (suc n) p  = suc≤suc (≤→→≤ m n p)

------------------------------------------------------------------------
-- Properties related to _∸_

-- Zero is a left zero of truncated subtraction.

∸-left-zero : ∀ n → 0 ∸ n ≡ 0
∸-left-zero zero    = refl _
∸-left-zero (suc _) = refl _

-- A form of associativity for _∸_.

∸-∸-assoc : ∀ {m} n {k} → (m ∸ n) ∸ k ≡ m ∸ (n + k)
∸-∸-assoc         zero            = refl _
∸-∸-assoc {zero}  (suc _) {zero}  = refl _
∸-∸-assoc {zero}  (suc _) {suc _} = refl _
∸-∸-assoc {suc _} (suc n)         = ∸-∸-assoc n

-- A limited form of associativity for _+_ and _∸_.

+-∸-assoc : ∀ {m n k} → k ≤ n → (m + n) ∸ k ≡ m + (n ∸ k)
+-∸-assoc {m} {n} {zero} _ =
  m + n ∸ 0    ≡⟨⟩
  m + n        ≡⟨⟩
  m + (n ∸ 0)  ∎
+-∸-assoc {m} {zero}  {suc k} <0      = ⊥-elim (≮0 _ <0)
+-∸-assoc {m} {suc n} {suc k} 1+k≤1+n =
  m + suc n ∸ suc k    ≡⟨ cong (_∸ suc k) (sym (suc+≡+suc m)) ⟩
  suc m + n ∸ suc k    ≡⟨⟩
  m + n ∸ k            ≡⟨ +-∸-assoc (suc≤suc⁻¹ 1+k≤1+n) ⟩
  m + (n ∸ k)          ≡⟨⟩
  m + (suc n ∸ suc k)  ∎

-- A special case of +-∸-assoc.

∸≡suc∸suc : ∀ {m n} → n < m → m ∸ n ≡ suc (m ∸ suc n)
∸≡suc∸suc = +-∸-assoc

-- If you add a number and then subtract it again, then you get back
-- what you started with.

+∸≡ : ∀ {m} n → (m + n) ∸ n ≡ m
+∸≡ {m} zero =
  m + 0  ≡⟨ +-right-identity ⟩∎
  m      ∎
+∸≡ {zero}  (suc n) = +∸≡ n
+∸≡ {suc m} (suc n) =
  m + suc n ∸ n  ≡⟨ cong (_∸ n) (sym (suc+≡+suc m))  ⟩
  suc m + n ∸ n  ≡⟨ +∸≡ n ⟩∎
  suc m          ∎

-- If you subtract a number from itself, then the answer is zero.

∸≡0 : ∀ n → n ∸ n ≡ 0
∸≡0 = +∸≡

-- If you subtract a number and then add it again, then you get back
-- what you started with if the number is less than or equal to the
-- number that you started with.

∸+≡ : ∀ {m n} → n ≤ m → (m ∸ n) + n ≡ m
∸+≡ {m} {n} (≤-refl′ n≡m) =
  (m ∸ n) + n  ≡⟨ cong (λ n → m ∸ n + n) n≡m ⟩
  (m ∸ m) + m  ≡⟨ cong (_+ m) (∸≡0 m) ⟩
  0 + m        ≡⟨⟩
  m            ∎
∸+≡ {m} {n} (≤-step′ {k = k} n≤k 1+k≡m) =
  (m ∸ n) + n        ≡⟨ cong (λ m → m ∸ n + n) (sym 1+k≡m) ⟩
  (1 + k ∸ n) + n    ≡⟨ cong (_+ n) (∸≡suc∸suc (suc≤suc n≤k)) ⟩
  1 + ((k ∸ n) + n)  ≡⟨ cong (1 +_) (∸+≡ n≤k) ⟩
  1 + k              ≡⟨ 1+k≡m ⟩∎
  m                  ∎

-- If you subtract a number and then add it again, then you get
-- something that is greater than or equal to what you started with.

≤∸+ : ∀ m n → m ≤ (m ∸ n) + n
≤∸+ m zero =
  m      ≡⟨ sym +-right-identity ⟩≤
  m + 0  ∎≤
≤∸+ zero    (suc n) = zero≤ _
≤∸+ (suc m) (suc n) =
  suc m            ≤⟨ suc≤suc (≤∸+ m n) ⟩
  suc (m ∸ n + n)  ≡⟨ suc+≡+suc _ ⟩≤
  m ∸ n + suc n    ∎≤

-- If you subtract something from a number you get a number that is
-- less than or equal to the one you started with.

∸≤ : ∀ m n → m ∸ n ≤ m
∸≤ _       zero    = ≤-refl
∸≤ zero    (suc _) = ≤-refl
∸≤ (suc m) (suc n) = ≤-step (∸≤ m n)

-- A kind of commutativity for _+ n and _∸ k.

+-∸-comm : ∀ {m n k} → k ≤ m → (m + n) ∸ k ≡ (m ∸ k) + n
+-∸-comm {m} {n} {k = zero}  = const (m + n  ∎)
+-∸-comm {zero}  {k = suc k} = ⊥-elim ∘ ≮0 k
+-∸-comm {suc _} {k = suc _} = +-∸-comm ∘ suc≤suc⁻¹

-- _∸_ is monotone in its first argument and antitone in its second
-- argument.

infixl 6 _∸-mono_

_∸-mono_ : ∀ {m₁ m₂ n₁ n₂} → m₁ ≤ m₂ → n₂ ≤ n₁ → m₁ ∸ n₁ ≤ m₂ ∸ n₂
_∸-mono_              {n₁ = zero}   {zero}  p _ = p
_∸-mono_              {n₁ = zero}   {suc _} _ q = ⊥-elim (≮0 _ q)
_∸-mono_ {zero}       {n₁ = suc n₁}         _ _ = zero≤ _
_∸-mono_ {suc _}  {zero}   {suc _}          p _ = ⊥-elim (≮0 _ p)
_∸-mono_ {suc m₁} {suc m₂} {suc n₁} {zero}  p _ = m₁ ∸ n₁  ≤⟨ ∸≤ _ n₁ ⟩
                                                  m₁       ≤⟨ pred≤ _ ⟩
                                                  suc m₁   ≤⟨ p ⟩∎
                                                  suc m₂   ∎≤
_∸-mono_ {suc _}  {suc _}  {suc _}  {suc _} p q =
  suc≤suc⁻¹ p ∸-mono suc≤suc⁻¹ q

-- The predecessor function can be expressed using _∸_.

pred≡∸1 : ∀ n → pred n ≡ n ∸ 1
pred≡∸1 zero    = refl _
pred≡∸1 (suc _) = refl _

------------------------------------------------------------------------
-- Minimum and maximum

-- Minimum.

min : ℕ → ℕ → ℕ
min zero    n       = zero
min m       zero    = zero
min (suc m) (suc n) = suc (min m n)

-- Maximum.

max : ℕ → ℕ → ℕ
max zero    n       = n
max m       zero    = m
max (suc m) (suc n) = suc (max m n)

-- The min operation can be expressed using repeated truncated
-- subtraction.

min≡∸∸ : ∀ m n → min m n ≡ m ∸ (m ∸ n)
min≡∸∸ zero n =
  0            ≡⟨ sym (∸-left-zero (0 ∸ n)) ⟩∎
  0 ∸ (0 ∸ n)  ∎
min≡∸∸ (suc m) zero =
  0      ≡⟨ sym (∸≡0 m) ⟩∎
  m ∸ m  ∎
min≡∸∸ (suc m) (suc n) =
  suc (min m n)      ≡⟨ cong suc (min≡∸∸ m n) ⟩
  suc (m ∸ (m ∸ n))  ≡⟨ sym (+-∸-assoc (∸≤ _ n)) ⟩∎
  suc m ∸ (m ∸ n)    ∎

-- The max operation can be expressed using addition and truncated
-- subtraction.

max≡+∸ : ∀ m n → max m n ≡ m + (n ∸ m)
max≡+∸ zero    _       = refl _
max≡+∸ (suc m) zero    = suc m        ≡⟨ cong suc (sym +-right-identity) ⟩∎
                         suc (m + 0)  ∎
max≡+∸ (suc m) (suc n) = cong suc (max≡+∸ m n)

-- The _≤_ relation can be expressed in terms of the min function.

≤⇔min≡ : ∀ {m n} → m ≤ n ⇔ min m n ≡ m
≤⇔min≡ = record { to = to _ _ ∘ ≤→≤→ _ _; from = from _ _ }
  where
  to : ∀ m n → m ≤→ n → min m n ≡ m
  to zero    n       = const (refl zero)
  to (suc m) zero    = λ ()
  to (suc m) (suc n) = cong suc ∘ to m n

  from : ∀ m n → min m n ≡ m → m ≤ n
  from zero    n       = const (zero≤ n)
  from (suc m) zero    = ⊥-elim ∘ 0≢+
  from (suc m) (suc n) = suc≤suc ∘ from m n ∘ cancel-suc

-- The _≤_ relation can be expressed in terms of the max function.

≤⇔max≡ : ∀ {m n} → m ≤ n ⇔ max m n ≡ n
≤⇔max≡ {m} = record { to = to m _ ∘ ≤→≤→ _ _; from = from _ _ }
  where
  to : ∀ m n → m ≤→ n → max m n ≡ n
  to zero    n       = const (refl n)
  to (suc m) zero    = λ ()
  to (suc m) (suc n) = cong suc ∘ to m n

  from : ∀ m n → max m n ≡ n → m ≤ n
  from zero    n       = const (zero≤ n)
  from (suc m) zero    = ⊥-elim ∘ 0≢+ ∘ sym
  from (suc m) (suc n) = suc≤suc ∘ from m n ∘ cancel-suc

-- Given two numbers one is the minimum and the other is the maximum.

min-and-max :
  ∀ m n → min m n ≡ m × max m n ≡ n ⊎ min m n ≡ n × max m n ≡ m
min-and-max zero    _       = inj₁ (refl _ , refl _)
min-and-max (suc _) zero    = inj₂ (refl _ , refl _)
min-and-max (suc m) (suc n) =
  ⊎-map (Σ-map (cong suc) (cong suc))
        (Σ-map (cong suc) (cong suc))
        (min-and-max m n)

-- The min operation is idempotent.

min-idempotent : ∀ n → min n n ≡ n
min-idempotent n = case min-and-max n n of [ proj₁ , proj₁ ]

-- The max operation is idempotent.

max-idempotent : ∀ n → max n n ≡ n
max-idempotent n = case min-and-max n n of [ proj₂ , proj₂ ]

-- The min operation is commutative.

min-comm : ∀ m n → min m n ≡ min n m
min-comm zero    zero    = refl _
min-comm zero    (suc _) = refl _
min-comm (suc _) zero    = refl _
min-comm (suc m) (suc n) = cong suc (min-comm m n)

-- The max operation is commutative.

max-comm : ∀ m n → max m n ≡ max n m
max-comm zero    zero    = refl _
max-comm zero    (suc _) = refl _
max-comm (suc _) zero    = refl _
max-comm (suc m) (suc n) = cong suc (max-comm m n)

-- The min operation is associative.

min-assoc : ∀ m {n o} → min m (min n o) ≡ min (min m n) o
min-assoc zero                            = refl _
min-assoc (suc m) {n = zero}              = refl _
min-assoc (suc m) {n = suc n} {o = zero}  = refl _
min-assoc (suc m) {n = suc n} {o = suc o} = cong suc (min-assoc m)

-- The max operation is associative.

max-assoc : ∀ m {n o} → max m (max n o) ≡ max (max m n) o
max-assoc zero                            = refl _
max-assoc (suc m) {n = zero}              = refl _
max-assoc (suc m) {n = suc n} {o = zero}  = refl _
max-assoc (suc m) {n = suc n} {o = suc o} = cong suc (max-assoc m)

-- The minimum is less than or equal to both arguments.

min≤ˡ : ∀ m n → min m n ≤ m
min≤ˡ zero    _       = ≤-refl
min≤ˡ (suc _) zero    = zero≤ _
min≤ˡ (suc m) (suc n) = suc≤suc (min≤ˡ m n)

min≤ʳ : ∀ m n → min m n ≤ n
min≤ʳ m n =
  min m n  ≡⟨ min-comm _ _ ⟩≤
  min n m  ≤⟨ min≤ˡ _ _ ⟩∎
  n        ∎≤

-- The maximum is greater than or equal to both arguments.

ˡ≤max : ∀ m n → m ≤ max m n
ˡ≤max zero    _       = zero≤ _
ˡ≤max (suc _) zero    = ≤-refl
ˡ≤max (suc m) (suc n) = suc≤suc (ˡ≤max m n)

ʳ≤max : ∀ m n → n ≤ max m n
ʳ≤max m n =
  n        ≤⟨ ˡ≤max _ _ ⟩
  max n m  ≡⟨ max-comm n _ ⟩≤
  max m n  ∎≤

-- A kind of distributivity property for max and _∸_.

max-∸ : ∀ m n o → max (m ∸ o) (n ∸ o) ≡ max m n ∸ o
max-∸ m       n       zero    = refl _
max-∸ zero    n       (suc o) = refl _
max-∸ (suc m) (suc n) (suc o) = max-∸ m n o
max-∸ (suc m) zero    (suc o) =
  max (m ∸ o) 0  ≡⟨ max-comm _ 0 ⟩
  m ∸ o          ∎

------------------------------------------------------------------------
-- Division by two

-- Division by two, rounded upwards.

⌈_/2⌉ : ℕ → ℕ
⌈ zero        /2⌉ = zero
⌈ suc zero    /2⌉ = suc zero
⌈ suc (suc n) /2⌉ = suc ⌈ n /2⌉

-- Division by two, rounded downwards.

⌊_/2⌋ : ℕ → ℕ
⌊ zero        /2⌋ = zero
⌊ suc zero    /2⌋ = zero
⌊ suc (suc n) /2⌋ = suc ⌊ n /2⌋

-- Some simple lemmas related to division by two.

⌈/2⌉+⌊/2⌋ : ∀ n → ⌈ n /2⌉ + ⌊ n /2⌋ ≡ n
⌈/2⌉+⌊/2⌋ zero          = refl _
⌈/2⌉+⌊/2⌋ (suc zero)    = refl _
⌈/2⌉+⌊/2⌋ (suc (suc n)) =
  suc ⌈ n /2⌉ + suc ⌊ n /2⌋      ≡⟨ cong suc (sym (suc+≡+suc _)) ⟩
  suc (suc (⌈ n /2⌉ + ⌊ n /2⌋))  ≡⟨ cong (suc ∘ suc) (⌈/2⌉+⌊/2⌋ n) ⟩∎
  suc (suc n)                    ∎

⌊/2⌋≤⌈/2⌉ : ∀ n → ⌊ n /2⌋ ≤ ⌈ n /2⌉
⌊/2⌋≤⌈/2⌉ zero          = ≤-refl
⌊/2⌋≤⌈/2⌉ (suc zero)    = zero≤ 1
⌊/2⌋≤⌈/2⌉ (suc (suc n)) = suc≤suc (⌊/2⌋≤⌈/2⌉ n)

⌈/2⌉≤ : ∀ n → ⌈ n /2⌉ ≤ n
⌈/2⌉≤ zero          = ≤-refl
⌈/2⌉≤ (suc zero)    = ≤-refl
⌈/2⌉≤ (suc (suc n)) =
  suc ⌈ n /2⌉  ≤⟨ suc≤suc (⌈/2⌉≤ n) ⟩
  suc n        ≤⟨ m≤n+m _ 1 ⟩∎
  suc (suc n)  ∎≤

⌈/2⌉< : ∀ n → ⌈ 2 + n /2⌉ < 2 + n
⌈/2⌉< n =
  2 + ⌈ n /2⌉  ≤⟨ ≤-refl +-mono ⌈/2⌉≤ n ⟩∎
  2 + n        ∎≤

⌊/2⌋< : ∀ n → ⌊ 1 + n /2⌋ < 1 + n
⌊/2⌋< zero    = ≤-refl
⌊/2⌋< (suc n) =
  2 + ⌊ n /2⌋  ≤⟨ ≤-refl +-mono ⌊/2⌋≤⌈/2⌉ n ⟩
  2 + ⌈ n /2⌉  ≤⟨ ⌈/2⌉< n ⟩∎
  2 + n        ∎≤

⌈2*+/2⌉≡ : ∀ m {n} → ⌈ 2 * m + n /2⌉ ≡ m + ⌈ n /2⌉
⌈2*+/2⌉≡ zero            = refl _
⌈2*+/2⌉≡ (suc m) {n = n} =
  ⌈ 2 * (1 + m) + n /2⌉  ≡⟨ cong (λ m → ⌈ m + n /2⌉) (*-+-distribˡ 2 {n = 1}) ⟩
  ⌈ 2 + 2 * m + n /2⌉    ≡⟨⟩
  1 + ⌈ 2 * m + n /2⌉    ≡⟨ cong suc (⌈2*+/2⌉≡ m) ⟩∎
  1 + m + ⌈ n /2⌉        ∎

⌊2*+/2⌋≡ : ∀ m {n} → ⌊ 2 * m + n /2⌋ ≡ m + ⌊ n /2⌋
⌊2*+/2⌋≡ zero            = refl _
⌊2*+/2⌋≡ (suc m) {n = n} =
  ⌊ 2 * (1 + m) + n /2⌋  ≡⟨ cong (λ m → ⌊ m + n /2⌋) (*-+-distribˡ 2 {n = 1}) ⟩
  ⌊ 2 + 2 * m + n /2⌋    ≡⟨⟩
  1 + ⌊ 2 * m + n /2⌋    ≡⟨ cong suc (⌊2*+/2⌋≡ m) ⟩∎
  1 + m + ⌊ n /2⌋        ∎

⌈2*/2⌉≡ : ∀ n → ⌈ 2 * n /2⌉ ≡ n
⌈2*/2⌉≡ n =
  ⌈ 2 * n /2⌉      ≡⟨ cong ⌈_/2⌉ $ sym +-right-identity ⟩
  ⌈ 2 * n + 0 /2⌉  ≡⟨ ⌈2*+/2⌉≡ n ⟩
  n + ⌈ 0 /2⌉      ≡⟨⟩
  n + 0            ≡⟨ +-right-identity ⟩∎
  n                ∎

⌈1+2*/2⌉≡ : ∀ n → ⌈ 1 + 2 * n /2⌉ ≡ 1 + n
⌈1+2*/2⌉≡ n =
  ⌈ 1 + 2 * n /2⌉  ≡⟨ cong ⌈_/2⌉ $ +-comm 1 ⟩
  ⌈ 2 * n + 1 /2⌉  ≡⟨ ⌈2*+/2⌉≡ n ⟩
  n + ⌈ 1 /2⌉      ≡⟨⟩
  n + 1            ≡⟨ +-comm n ⟩∎
  1 + n            ∎

⌊2*/2⌋≡ : ∀ n → ⌊ 2 * n /2⌋ ≡ n
⌊2*/2⌋≡ n =
  ⌊ 2 * n /2⌋      ≡⟨ cong ⌊_/2⌋ $ sym +-right-identity ⟩
  ⌊ 2 * n + 0 /2⌋  ≡⟨ ⌊2*+/2⌋≡ n ⟩
  n + ⌊ 0 /2⌋      ≡⟨⟩
  n + 0            ≡⟨ +-right-identity ⟩∎
  n                ∎

⌊1+2*/2⌋≡ : ∀ n → ⌊ 1 + 2 * n /2⌋ ≡ n
⌊1+2*/2⌋≡ n =
  ⌊ 1 + 2 * n /2⌋  ≡⟨ cong ⌊_/2⌋ $ +-comm 1 ⟩
  ⌊ 2 * n + 1 /2⌋  ≡⟨ ⌊2*+/2⌋≡ n ⟩
  n + ⌊ 1 /2⌋      ≡⟨⟩
  n + 0            ≡⟨ +-right-identity ⟩∎
  n                ∎

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.Algebra.GradedRing.Instances.TrivialGradedRing where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv

open import Cubical.Data.Unit
open import Cubical.Data.Nat using (ℕ ; zero ; suc ; +-assoc ; +-zero)
open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Monoid.Instances.Nat
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.AbGroup.Instances.Unit
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.GradedRing.Base
open import Cubical.Algebra.GradedRing.DirectSumHIT

private variable
  ℓ : Level

open Iso
open GradedRing-⊕HIT-index
open GradedRing-⊕HIT-⋆

module _
  (ARing@(A , Astr) : Ring ℓ)
  where

  open RingStr Astr
  open RingTheory ARing

  private

    G : ℕ → Type ℓ
    G zero = A
    G (suc k) = Unit*

    Gstr : (k : ℕ) → AbGroupStr (G k)
    Gstr zero = snd (Ring→AbGroup ARing)
    Gstr (suc k) = snd UnitAbGroup

    ⋆ : {k l : ℕ} → G k → G l → G (k Cubical.Data.Nat.+ l)
    ⋆ {zero} {zero} x y = x · y
    ⋆ {zero} {suc l} x y = tt*
    ⋆ {suc k} {l} x y = tt*

    0-⋆ : {k l : ℕ} (b : G l) → ⋆ (AbGroupStr.0g (Gstr k)) b ≡ AbGroupStr.0g (Gstr (k Cubical.Data.Nat.+ l))
    0-⋆ {zero} {zero} b = 0LeftAnnihilates _
    0-⋆ {zero} {suc l} b = refl
    0-⋆ {suc k} {l} b = refl

    ⋆-0 : {k l : ℕ} (a : G k) → ⋆ a (AbGroupStr.0g (Gstr l)) ≡ AbGroupStr.0g (Gstr (k Cubical.Data.Nat.+ l))
    ⋆-0 {zero} {zero} a = 0RightAnnihilates _
    ⋆-0 {zero} {suc l} a = refl
    ⋆-0 {suc k} {l} a = refl

    ⋆Assoc : {k l m : ℕ} (a : G k) (b : G l) (c : G m) →
             _≡_ {A = Σ[ k ∈ ℕ ] G k}
             (k Cubical.Data.Nat.+ (l Cubical.Data.Nat.+ m) , ⋆ a (⋆ b c))
             (k Cubical.Data.Nat.+ l Cubical.Data.Nat.+ m , ⋆ (⋆ a b) c)
    ⋆Assoc {zero} {zero} {zero} a b c =  ΣPathTransport→PathΣ _ _ (+-assoc _ _ _ , transportRefl _ ∙ ·Assoc _ _ _)
    ⋆Assoc {zero} {zero} {suc m} a b c = ΣPathTransport→PathΣ _ _ (+-assoc _ _ _ , transportRefl _)
    ⋆Assoc {zero} {suc l} {m} a b c =  ΣPathTransport→PathΣ _ _ (+-assoc _ _ _ , transportRefl _)
    ⋆Assoc {suc k} {l} {m} a b c = ΣPathTransport→PathΣ _ _ (+-assoc _ _ _ , transportRefl _)

    ⋆IdR : {k : ℕ} (a : G k) → _≡_ {A = Σ[ k ∈ ℕ ] G k} (k Cubical.Data.Nat.+ 0 , ⋆ a 1r) (k , a)
    ⋆IdR {zero} a = ΣPathTransport→PathΣ _ _ (refl , (transportRefl _ ∙ ·IdR _))
    ⋆IdR {suc k} a = ΣPathTransport→PathΣ _ _ ((+-zero _) , (transportRefl _))

    ⋆IdL : {l : ℕ} (b : G l) → _≡_ {A = Σ[ k ∈ ℕ ] G k} (l , ⋆ 1r b) (l , b)
    ⋆IdL {zero} b = ΣPathTransport→PathΣ _ _ (refl , (transportRefl _ ∙ ·IdL _))
    ⋆IdL {suc l} b = ΣPathTransport→PathΣ _ _ (refl , (transportRefl _))

    ⋆DistR+ : {k l : ℕ} (a : G k) (b c : G l) →
              ⋆ a (Gstr l .AbGroupStr._+_ b c) ≡ Gstr (k Cubical.Data.Nat.+ l) .AbGroupStr._+_ (⋆ a b) (⋆ a c)
    ⋆DistR+ {zero} {zero} a b c = ·DistR+ _ _ _
    ⋆DistR+ {zero} {suc l} a b c = refl
    ⋆DistR+ {suc k} {l} a b c = refl

    ⋆DistL+ : {k l : ℕ} (a b : G k) (c : G l) →
              ⋆ (Gstr k .AbGroupStr._+_ a b) c ≡ Gstr (k Cubical.Data.Nat.+ l) .AbGroupStr._+_ (⋆ a c) (⋆ b c)
    ⋆DistL+ {zero} {zero} a b c = ·DistL+ _ _ _
    ⋆DistL+ {zero} {suc l} a b c = refl
    ⋆DistL+ {suc k} {l} a b c = refl

  trivialGradedRing : GradedRing ℓ-zero ℓ
  trivialGradedRing = makeGradedRing ARing NatMonoid
                      G Gstr 1r ⋆  0-⋆ ⋆-0
                      ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+
                      equivRing
    where
    equivRing : RingEquiv ARing (⊕HITgradedRing-Ring
                                 NatMonoid G Gstr 1r ⋆ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+)
    fst equivRing = isoToEquiv is
      where
      is : Iso A (⊕HIT ℕ G Gstr)
      fun is a = base 0 a
      inv is = DS-Rec-Set.f _ _ _ _ is-set
               0r (λ {zero a → a ; (suc k) a → 0r }) _+_ +Assoc +IdR +Comm
               (λ { zero → refl ; (suc k) → refl}) (λ {zero a b → refl ; (suc n) a b → +IdR _})
      rightInv is = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
                    (base-neutral _)
                    (λ { zero a → refl ; (suc k) a → base-neutral _ ∙ sym (base-neutral _)} )
                    λ {U V} ind-U ind-V → sym (base-add _ _ _) ∙ cong₂ _add_ ind-U ind-V
      leftInv is = λ _ → refl
    snd equivRing = makeIsRingHom
                    -- issue agda have trouble infering the Idx, G, Gstr
                    {R = ARing}
                    {S = ⊕HITgradedRing-Ring NatMonoid G Gstr 1r ⋆ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+}
                    {f = λ a → base 0 a}
                    refl (λ _ _ → sym (base-add _ _ _)) λ _ _ → refl

ext: agda

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Oscar.Class
open import Oscar.Class.Reflexivity
open import Oscar.Class.Symmetry
open import Oscar.Class.Transitivity
open import Oscar.Class.Transleftidentity
open import Oscar.Prelude

module Test.ProblemWithDerivation-5 where

module Map
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  {𝔯₁₂} {𝔯₁₂'}
  (ℜ₁₂ : 𝔛₁ → 𝔛₂ → Ø 𝔯₁₂)
  (ℜ₁₂' : 𝔛₁ → 𝔛₂ → Ø 𝔯₁₂')
  = ℭLASS (ℜ₁₂ , ℜ₁₂')
          (∀ P₁ P₂
           → ℜ₁₂ P₁ P₂ → ℜ₁₂' P₁ P₂)

module _
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  {𝔯₁₂} {ℜ₁₂ : 𝔛₁ → 𝔛₂ → Ø 𝔯₁₂}
  {𝔯₁₂'} {ℜ₁₂' : 𝔛₁ → 𝔛₂ → Ø 𝔯₁₂'}
  where
  map = Map.method ℜ₁₂ ℜ₁₂'

module _
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔯₁₂} {ℜ₁₂ : 𝔛₁ → 𝔛₁ → Ø 𝔯₁₂}
  {𝔯₁₂'} {ℜ₁₂' : 𝔛₁ → 𝔛₁ → Ø 𝔯₁₂'}
  where
  smap = Map.method ℜ₁₂ ℜ₁₂' -- FIXME this looks like a viable solution; but what if `-MapFromTransleftidentity` builds something addressable by smap (i.e., where 𝔛₁ ≡ 𝔛₂)?

module _
  {𝔵₁} {𝔛₁ : Ø 𝔵₁}
  {𝔵₂} {𝔛₂ : Ø 𝔵₂}
  {𝔯₁₂} {ℜ₁₂ : 𝔛₁ → 𝔛₂ → Ø 𝔯₁₂}
  where
  hmap = Map.method ℜ₁₂ ℜ₁₂

postulate
  A : Set
  B : Set
  _~A~_ : A → A → Set
  _~B~_ : B → B → Set
  s1 : A → B
  f1 : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y

instance
  𝓢urjectivity1 : Map.class
                    {𝔛₁ = A}
                    {𝔛₂ = A}
                    _~A~_ (λ x y → s1 x ~B~ s1 y)
  𝓢urjectivity1 .⋆ _ _ = f1

-- Oscar.Class.Hmap.Transleftidentity
instance
  postulate
    -MapFromTransleftidentity : ∀
      {𝔵} {𝔛 : Ø 𝔵}
      {𝔞} {𝔄 : 𝔛 → Ø 𝔞}
      {𝔟} {𝔅 : 𝔛 → Ø 𝔟}
      (let _∼_ = Arrow 𝔄 𝔅)
      {ℓ̇} {_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ̇}
      {transitivity : Transitivity.type _∼_}
      {reflexivity : Reflexivity.type _∼_}
      {ℓ}
      ⦃ _ : Transleftidentity.class _∼_ _∼̇_ reflexivity transitivity ⦄
      → ∀ {m n}
      → Map.class {𝔛₁ = Arrow 𝔄 𝔅 m n}
                  {𝔛₂ = LeftExtensionṖroperty ℓ (Arrow 𝔄 𝔅) _∼̇_ m}
                  (λ f P → π₀ (π₀ P) f)
                  (λ f P → π₀ (π₀ P) (transitivity f reflexivity))

test-before : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y
test-before = map _ _

postulate
  XX : Set
  BB : XX → Set
  EQ : ∀ {x y} → Arrow BB BB x y → Arrow BB BB x y → Set

instance
  postulate
    -transleftidentity : Transleftidentity.class (Arrow BB BB) EQ (λ x₁ → magic) (λ x₁ x₂ x₃ → magic)

test-after : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y
test-after {x} {y} = map _ _ -- FIXME yellow

test-after-s : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y
test-after-s {x} {y} = smap _ _

testr : ∀ {m n ℓ}
          (P₁ : Arrow BB BB m n)
          (P₂ : LeftExtensionṖroperty ℓ (Arrow BB BB) EQ m)
          → π₀ (π₀ P₂) P₁ → π₀ (π₀ P₂) (flip {∅̂} {∅̂} {∅̂}
                                         {Arrow (λ z → BB z) (λ z → BB z) m n}
                                         {Arrow (λ z → BB z) (λ z → BB z) n n}
                                         {λ _ _ → Arrow BB BB m n}
                                         (λ _ _ _ → magic) (λ _ → magic) P₁)
testr = map


text:
module CS410-Vec where

open import CS410-Prelude
open import CS410-Nat

data Vec (X : Set) : Nat -> Set where
  []   : Vec X 0
  _::_ : forall {n} ->
         X -> Vec X n -> Vec X (suc n)
infixr 3 _::_

_+V_ : forall {X m n} -> Vec X m -> Vec X n -> Vec X (m +N n)
[] +V ys = ys
(x :: xs) +V ys = x :: xs +V ys
infixr 3 _+V_

data Choppable {X : Set}(m n : Nat) : Vec X (m +N n) -> Set where
  chopTo : (xs : Vec X m)(ys : Vec X n) -> Choppable m n (xs +V ys)

chop : {X : Set}(m n : Nat)(xs : Vec X (m +N n)) -> Choppable m n xs
chop zero n xs = chopTo [] xs
chop (suc m) n (x :: xs) with chop m n xs
chop (suc m) n (x :: .(xs +V ys)) | chopTo xs ys = chopTo (x :: xs) ys

chopParts : {X : Set}(m n : Nat)(xs : Vec X (m +N n)) -> Vec X m * Vec X n
chopParts m n xs with chop m n xs
chopParts m n .(xs +V ys) | chopTo xs ys = xs , ys

vec : forall {n X} -> X -> Vec X n
vec {zero}   x = []
vec {suc n}  x = x :: vec x

vapp : forall {n X Y} -> Vec (X -> Y) n -> Vec X n -> Vec Y n
vapp [] [] = []
vapp (f :: fs) (x :: xs) = f x :: vapp fs xs


text:
-- Andreas, issue 2349

-- Andreas, 2016-12-20, issue #2350

-- {-# OPTIONS -v tc.term.con:50 #-}

postulate A : Set

data D {{a : A}} : Set where
  c : D

test : {{a b : A}} → D
test {{a}} = c {{a}}

-- WAS: complaint about unsolvable instance

-- Should succeed

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Discussion about the inductive approach
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- Peter: If you take away the proof objects (as you do when you go to
-- predicate logic) the K axiom doesn't give you any extra power.

module FOT.FOTC.InductiveApproach.ProofTerm where

open import FOTC.Base

------------------------------------------------------------------------------

foo : (∃ λ x → ∃ λ y → x ≡ y) → (∃ λ x → ∃ λ y → y ≡ x)
foo (x , .x , refl) = x , x , refl

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Agda.Builtin.Equality

postulate
  Ty Cxt : Set
  Var Tm : Ty → Cxt → Set
  _≤_ : (Γ Δ : Cxt) → Set

variable
  Γ Δ Φ : Cxt
  A B C : Ty
  x : Var A Γ

Mon : (P : Cxt → Set) → Set
Mon P = ∀{Δ Γ} (ρ : Δ ≤ Γ) → P Γ → P Δ

postulate
  _•_ : Mon (_≤ Φ)
  monVar : Mon (Var A)
  monTm : Mon (Tm A)

postulate
  refl-ish : {A : Set} {x y : A} → x ≡ y

variable
  ρ ρ' : Δ ≤ Γ

monVar-comp : monVar ρ (monVar ρ' x) ≡ monVar (ρ • ρ') x
monVar-comp {ρ = ρ} {ρ' = ρ'} {x = x} = refl-ish

variable
  t : Tm A Γ

monTm-comp : monTm ρ (monTm ρ' t) ≡ monTm (ρ • ρ') t
monTm-comp {ρ = ρ} {ρ' = ρ'} {t = t} = refl-ish

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Prelude.List.Properties where

open import Prelude.Function

open import Prelude.Bool
open import Prelude.Bool.Properties

open import Prelude.Nat
open import Prelude.Nat.Properties

open import Prelude.Semiring

open import Prelude.List.Base

open import Prelude.Decidable

open import Prelude.Monoid
open import Prelude.Semigroup

open import Prelude.Equality
open import Prelude.Equality.Inspect
open import Prelude.Variables

open import Prelude.Strict

foldr-map-fusion : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
                     (f : B → C → C) (g : A → B) (z : C) (xs : List A) →
                     foldr f z (map g xs) ≡ foldr (f ∘ g) z xs
foldr-map-fusion f g z [] = refl
foldr-map-fusion f g z (x ∷ xs)
  rewrite foldr-map-fusion f g z xs
        = refl

foldl-map-fusion : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
                     (f : C → B → C) (g : A → B) (z : C) (xs : List A) →
                     foldl f z (map g xs) ≡ foldl (λ x y → f x (g y)) z xs
foldl-map-fusion f g z [] = refl
foldl-map-fusion f g z (x ∷ xs)
  rewrite foldl-map-fusion f g (f z (g x)) xs
        = refl

foldl-assoc : ∀ {a} {A : Set a} (f : A → A → A) →
                (∀ x y z → f x (f y z) ≡ f (f x y) z) →
                ∀ y z xs → foldl f (f y z) xs ≡ f y (foldl f z xs)
foldl-assoc f assoc y z [] = refl
foldl-assoc f assoc y z (x ∷ xs)
  rewrite sym (assoc y z x)
        = foldl-assoc f assoc y (f z x) xs

foldl-foldr : ∀ {a} {A : Set a} (f : A → A → A) (z : A) →
                (∀ x y z → f x (f y z) ≡ f (f x y) z) →
                (∀ x → f z x ≡ x) → (∀ x → f x z ≡ x) →
                ∀ xs → foldl f z xs ≡ foldr f z xs
foldl-foldr f z assoc idl idr [] = refl
foldl-foldr f z assoc idl idr (x ∷ xs)
  rewrite sym (foldl-foldr f z assoc idl idr xs)
        | idl x ⟨≡⟩ʳ idr x
        = foldl-assoc f assoc x z xs

foldl!-foldl : ∀ {a b} {A : Set a} {B : Set b} (f : B → A → B) z (xs : List A) →
                 foldl! f z xs ≡ foldl f z xs
foldl!-foldl f z [] = refl
foldl!-foldl f z (x ∷ xs) = forceLemma (f z x) (λ z′ → foldl! f z′ xs) ⟨≡⟩
                            foldl!-foldl f (f z x) xs

-- Properties of _++_

map-++ : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (xs ys : List A) →
           map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++ f []       ys = refl
map-++ f (x ∷ xs) ys = f x ∷_ $≡ map-++ f xs ys

product-++ : (xs ys : List Nat) → productR (xs ++ ys) ≡ productR xs * productR ys
product-++ []       ys = sym (add-zero-r _)
product-++ (x ∷ xs) ys = x *_ $≡ product-++ xs ys ⟨≡⟩ mul-assoc x _ _

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- M-types (the dual of W-types)
------------------------------------------------------------------------

module Data.M where

open import Level
open import Coinduction

-- The family of M-types.

data M {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  inf : (x : A) (f : B x → ∞ (M A B)) → M A B

-- Projections.

head : ∀ {a b} {A : Set a} {B : A → Set b} →
       M A B → A
head (inf x f) = x

tail : ∀ {a b} {A : Set a} {B : A → Set b} →
       (x : M A B) → B (head x) → M A B
tail (inf x f) b = ♭ (f b)


text:
module UnifyMguPair where

open import UnifyTerm
open import UnifyMgu
open import UnifyMguCorrect

open import Data.Fin using (Fin; suc; zero)
open import Data.Nat hiding (_≤_)
open import Relation.Binary.PropositionalEquality renaming ([_] to [[_]])
open import Function using (_∘_; id; case_of_; _$_)
open import Relation.Nullary
open import Data.Product
open import Data.Empty
open import Data.Maybe
open import Data.Sum

l1 : ∀ m → Data.Fin.toℕ (Data.Fin.fromℕ m) ≡ m
l1 zero = refl
l1 (suc m) = cong suc (l1 m)

l2 : ∀ m → m ≡ m + 0
l2 zero = refl
l2 (suc m) = cong suc (l2 m)

fixup : ∀ m → Fin (Data.Fin.toℕ (Data.Fin.fromℕ m) + m) → Fin (m + (m + 0))
fixup m x rewrite l1 m | sym (l2 m) = x

revise-down : ∀ {m} → Fin m → Fin (2 * m)
revise-down {m} x = Data.Fin.inject+ (m + 0) x

revise-up : ∀ {m} → Fin m → Fin (2 * m)
revise-up {m} x = fixup m (Data.Fin.fromℕ m Data.Fin.+ x)

write-variable-down : ∀ {m} → Term m → Term (2 * m)
write-variable-down {m} (i l) = i $ revise-down l
write-variable-down {m} leaf = leaf
write-variable-down {m} (s fork t) = write-variable-down s fork write-variable-down t

write-variable-up : ∀ {m} → Term m → Term (2 * m)
write-variable-up {m} (i r) = i (revise-up r)
write-variable-up {m} leaf = leaf
write-variable-up {m} (s fork t) = write-variable-up s fork write-variable-up t

write-variables-apart : ∀ {m} (s t : Term m) → Term (2 * m) × Term (2 * m)
write-variables-apart s t = write-variable-down s , write-variable-up t

separate-substitutions-down : ∀ {m n} → (Fin (2 * m) → Term n) → Fin m → Term n
separate-substitutions-down {m} f x = f $ revise-down x

separate-substitutions-up : ∀ {m n} → (Fin (2 * m) → Term n) → Fin m → Term n
separate-substitutions-up {m} f x = f $ revise-up x

separate-substitutions : ∀ {m n} → (Fin (2 * m) → Term n) → (Fin m → Term n) × (Fin m → Term n)
separate-substitutions {m} x = separate-substitutions-down {m} x , separate-substitutions-up {m} x

write≡separate : ∀ {m n} (σ : AList (2 * m) n) (t : Term m) → (sub σ ◃_) (write-variable-down t) ≡ ((separate-substitutions-down $ sub σ) ◃_) t
write≡separate {zero} {.0} anil (i x) = refl
write≡separate {suc m} {.(suc (m + suc (m + 0)))} anil (i x) = refl
write≡separate {suc m} {n} (σ asnoc t' / x) (i x₁) = refl
write≡separate σ leaf = refl
write≡separate σ (t₁ fork t₂) = cong₂ _fork_ (write≡separate σ t₁) (write≡separate σ t₂)

write≡separate' : ∀ {m n} (σ : AList (2 * m) n) (t : Term m) → (sub σ ◃_) (write-variable-down t) ≡ ((separate-substitutions-down $ sub σ) ◃_) t
write≡separate' {zero} {.0} anil (i x) = refl
write≡separate' {suc m} {.(suc (m + suc (m + 0)))} anil (i x) = refl
write≡separate' {suc m} {n} (σ asnoc t' / x) (i x₁) = refl
write≡separate' σ leaf = refl
write≡separate' σ (t₁ fork t₂) = cong₂ _fork_ (write≡separate σ t₁) (write≡separate σ t₂)

Property'2 : (m : ℕ) -> Set1
Property'2 m = ∀ {n} -> (Fin (2 * m) -> Term n) -> Set

Nothing'2 : ∀{m} -> (P : Property'2 m) -> Set
Nothing'2 P = ∀{n} f -> P {n} f -> ⊥

Unifies'2 : ∀ {m} (s t : Term m) -> Property'2 m
Unifies'2 s t f =
  let --s' , t' = write-variables-apart s t
      f₁ , f₂ = separate-substitutions f
  in f₁ ◃ s ≡ f₂ ◃ t

pair-mgu' : ∀ {m} -> (s t : Term m) -> Maybe (∃ (AList (2 * m)))
pair-mgu' {m} s t =
  let s' , t' = write-variables-apart s t
      mgu' = mgu s' t'
  in
    mgu'

up-equality : ∀ {m n} {f : (2 * m) ~> n} (t : Term m) → (f ∘ revise-up) ◃ t ≡ f ◃ write-variable-up t
up-equality (i x) = refl
up-equality leaf = refl
up-equality (t₁ fork t₂) = cong₂ _fork_ (up-equality t₁) (up-equality t₂)

down-equality : ∀ {m n} {f : (2 * m) ~> n} (t : Term m) → (f ∘ revise-down) ◃ t ≡ f ◃ write-variable-down t
down-equality (i x) = refl
down-equality leaf = refl
down-equality (t₁ fork t₂) = cong₂ _fork_ (down-equality t₁) (down-equality t₂)

revise-to-write : ∀ {m n} {f : (2 * m) ~> n} (s t : Term m) → (f ∘ revise-down) ◃ s ≡ (f ∘ revise-up) ◃ t → f ◃ write-variable-down s ≡ f ◃ write-variable-up t
revise-to-write (i x) (i x₁) x₂ = x₂
revise-to-write (i x) leaf x₁ = x₁
revise-to-write (i x) (t fork t₁) x₁ = trans x₁ (up-equality (t fork t₁))
revise-to-write leaf (i x) x₁ = x₁
revise-to-write leaf leaf x = refl
revise-to-write leaf (t₁ fork t₂) x = trans x (up-equality (t₁ fork t₂))
revise-to-write (s₁ fork s₂) (i x) x₁ = trans (sym (down-equality (s₁ fork s₂))) x₁
revise-to-write (s₁ fork s₂) leaf x = trans (sym (down-equality (s₁ fork s₂))) x
revise-to-write (s₁ fork s₂) (t₁ fork t₂) x = trans (trans (sym (down-equality (s₁ fork s₂))) x) (up-equality (t₁ fork t₂))

write-to-revise : ∀ {m n} {f : (2 * m) ~> n} (s t : Term m) → f ◃ write-variable-down s ≡ f ◃ write-variable-up t → (f ∘ revise-down) ◃ s ≡ (f ∘ revise-up) ◃ t
write-to-revise (i x) (i x₁) x₂ = x₂
write-to-revise (i x) leaf x₁ = x₁
write-to-revise (i x) (t fork t₁) x₁ = trans x₁ (sym (up-equality (t fork t₁)))
write-to-revise leaf (i x) x₁ = x₁
write-to-revise leaf leaf x = refl
write-to-revise leaf (t fork t₁) x = trans x (sym (up-equality (t fork t₁)))
write-to-revise (s₁ fork s₂) (i x) x₁ = trans ((down-equality (s₁ fork s₂))) x₁
write-to-revise (s₁ fork s₂) leaf x = trans ((down-equality (s₁ fork s₂))) x
write-to-revise (s₁ fork s₂) (t fork t₁) x = trans (trans ((down-equality (s₁ fork s₂))) x) (sym (up-equality (t fork t₁)))

pair-mgu-c' : ∀ {m} (s t : Term m) ->
                (∃ λ n → ∃ λ σ → (Max⋆ (Unifies'2 s t)) (sub σ) × pair-mgu' s t ≡ just (n , σ))
                ⊎ (Nothing⋆ (Unifies'2 s t)                     × pair-mgu' s t ≡ nothing)
pair-mgu-c' {m} s t with write-variable-down s | write-variable-up t | inspect write-variable-down s | inspect write-variable-up t
… | s' | t' | [[ refl ]] | [[ refl ]] with mgu-c s' t'
… | (inj₁ (n , σ , (σ◃s'=σ◃t' , max-σ) , amgu=just)) =
  inj₁ $
  n ,
  σ ,
  ( write-to-revise s t σ◃s'=σ◃t' ,
    ( λ {n'} f f◃s≡f◃t → (proj₁ $ max-σ f (revise-to-write s t f◃s≡f◃t)) ,
      (λ x → proj₂ (max-σ f (revise-to-write s t f◃s≡f◃t)) x) ) ) ,
  amgu=just
… | (inj₂ (notunified , amgu=nothing)) = inj₂ ((λ {n} f x → notunified f (revise-to-write s t x)) , amgu=nothing)


text: open import TakeDropDec


text:
{-# OPTIONS --omega-in-omega --no-termination-check #-}

module Light.Variable.Sets where

open import Light.Variable.Levels

variable
      𝕒 𝕒₀ 𝕒₁ 𝕒₂ 𝕒₃ 𝕒₄ 𝕒₅ : Set aℓ
      𝕓 𝕓₀ 𝕓₁ 𝕓₂ 𝕓₃ 𝕓₄ 𝕓₅ : Set bℓ
      𝕔 𝕔₀ 𝕔₁ 𝕔₂ 𝕔₃ 𝕔₄ 𝕔₅ : Set cℓ
      𝕕 𝕕₀ 𝕕₁ 𝕕₂ 𝕕₃ 𝕕₄ 𝕕₅ : Set dℓ
      𝕖 𝕖₀ 𝕖₁ 𝕖₂ 𝕖₃ 𝕖₄ 𝕖₅ : Set eℓ
      𝕗 𝕗₀ 𝕗₁ 𝕗₂ 𝕗₃ 𝕗₄ 𝕗₅ : Set fℓ
      𝕘 𝕘₀ 𝕘₁ 𝕘₂ 𝕘₃ 𝕘₄ 𝕘₅ : Set gℓ
      𝕙 𝕙₀ 𝕙₁ 𝕙₂ 𝕙₃ 𝕙₄ 𝕙₅ : Set hℓ

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
------------------------------------------------------------------------
-- Some Vec-related properties
------------------------------------------------------------------------

module Data.Vec.Properties where

open import Algebra
open import Data.Vec
open import Data.Nat
import Data.Nat.Properties as Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Function
open import Relation.Binary

module UsingVectorEquality (S : Setoid) where

  private module SS = Setoid S
  open SS using () renaming (carrier to A)
  import Data.Vec.Equality as VecEq
  open VecEq.Equality S

  replicate-lemma : ∀ {m} n x (xs : Vec A m) →
                    replicate {n = n}     x ++ (x ∷ xs) ≈
                    replicate {n = 1 + n} x ++      xs
  replicate-lemma zero    x xs = refl (x ∷ xs)
  replicate-lemma (suc n) x xs = SS.refl ∷-cong replicate-lemma n x xs

  xs++[]=xs : ∀ {n} (xs : Vec A n) → xs ++ [] ≈ xs
  xs++[]=xs []       = []-cong
  xs++[]=xs (x ∷ xs) = SS.refl ∷-cong xs++[]=xs xs

  map-++-commute : ∀ {B m n} (f : B → A) (xs : Vec B m) {ys : Vec B n} →
                   map f (xs ++ ys) ≈ map f xs ++ map f ys
  map-++-commute f []       = refl _
  map-++-commute f (x ∷ xs) = SS.refl ∷-cong map-++-commute f xs

open import Relation.Binary.PropositionalEquality as PropEq
open import Relation.Binary.HeterogeneousEquality as HetEq

-- lookup is natural.

lookup-natural : ∀ {A B n} (f : A → B) (i : Fin n) →
                 lookup i ∘ map f ≗ f ∘ lookup i
lookup-natural f zero    (x ∷ xs) = refl
lookup-natural f (suc i) (x ∷ xs) = lookup-natural f i xs

-- map is a congruence.

map-cong : ∀ {A B n} {f g : A → B} →
           f ≗ g → _≗_ {Vec A n} (map f) (map g)
map-cong f≗g []       = refl
map-cong f≗g (x ∷ xs) = PropEq.cong₂ _∷_ (f≗g x) (map-cong f≗g xs)

-- map is functorial.

map-id : ∀ {A n} → _≗_ {Vec A n} (map id) id
map-id []       = refl
map-id (x ∷ xs) = PropEq.cong (_∷_ x) (map-id xs)

map-∘ : ∀ {A B C n} (f : B → C) (g : A → B) →
        _≗_ {Vec A n} (map (f ∘ g)) (map f ∘ map g)
map-∘ f g []       = refl
map-∘ f g (x ∷ xs) = PropEq.cong (_∷_ (f (g x))) (map-∘ f g xs)

-- sum commutes with _++_.

sum-++-commute : ∀ {m n} (xs : Vec ℕ m) {ys : Vec ℕ n} →
                 sum (xs ++ ys) ≡ sum xs + sum ys
sum-++-commute []            = refl
sum-++-commute (x ∷ xs) {ys} = begin
  x + sum (xs ++ ys)
    ≡⟨ PropEq.cong (λ p → x + p) (sum-++-commute xs) ⟩
  x + (sum xs + sum ys)
    ≡⟨ PropEq.sym (+-assoc x (sum xs) (sum ys)) ⟩
  sum (x ∷ xs) + sum ys
    ∎
  where
  open ≡-Reasoning
  open CommutativeSemiring Nat.commutativeSemiring hiding (_+_; sym)

-- foldr is a congruence.

foldr-cong : ∀ {A} {B₁} {f₁ : ∀ {n} → A → B₁ n → B₁ (suc n)} {e₁}
                   {B₂} {f₂ : ∀ {n} → A → B₂ n → B₂ (suc n)} {e₂} →
             (∀ {n x} {y₁ : B₁ n} {y₂ : B₂ n} →
                y₁ ≅ y₂ → f₁ x y₁ ≅ f₂ x y₂) →
             e₁ ≅ e₂ →
             ∀ {n} (xs : Vec A n) →
             foldr B₁ f₁ e₁ xs ≅ foldr B₂ f₂ e₂ xs
foldr-cong           _     e₁=e₂ []       = e₁=e₂
foldr-cong {B₁ = B₁} f₁=f₂ e₁=e₂ (x ∷ xs) =
  f₁=f₂ (foldr-cong {B₁ = B₁} f₁=f₂ e₁=e₂ xs)

-- foldl is a congruence.

foldl-cong : ∀ {A} {B₁} {f₁ : ∀ {n} → B₁ n → A → B₁ (suc n)} {e₁}
                   {B₂} {f₂ : ∀ {n} → B₂ n → A → B₂ (suc n)} {e₂} →
             (∀ {n x} {y₁ : B₁ n} {y₂ : B₂ n} →
                y₁ ≅ y₂ → f₁ y₁ x ≅ f₂ y₂ x) →
             e₁ ≅ e₂ →
             ∀ {n} (xs : Vec A n) →
             foldl B₁ f₁ e₁ xs ≅ foldl B₂ f₂ e₂ xs
foldl-cong           _     e₁=e₂ []       = e₁=e₂
foldl-cong {B₁ = B₁} f₁=f₂ e₁=e₂ (x ∷ xs) =
  foldl-cong {B₁ = B₁ ∘₀ suc} f₁=f₂ (f₁=f₂ e₁=e₂) xs

-- The (uniqueness part of the) universality property for foldr.

foldr-universal : ∀ {A} (B : ℕ → Set)
                  (f : ∀ {n} → A → B n → B (suc n)) {e}
                  (h : ∀ {n} → Vec A n → B n) →
                  h [] ≡ e →
                  (∀ {n} x → h ∘ _∷_ x ≗ f {n} x ∘ h) →
                  ∀ {n} → h ≗ foldr B {n} f e
foldr-universal B f     h base step []       = base
foldr-universal B f {e} h base step (x ∷ xs) = begin
  h (x ∷ xs)
    ≡⟨ step x xs ⟩
  f x (h xs)
    ≡⟨ PropEq.cong (f x) (foldr-universal B f h base step xs) ⟩
  f x (foldr B f e xs)
    ∎
  where open ≡-Reasoning

-- A fusion law for foldr.

foldr-fusion : ∀ {A} {B : ℕ → Set} {f : ∀ {n} → A → B n → B (suc n)} e
                     {C : ℕ → Set} {g : ∀ {n} → A → C n → C (suc n)}
               (h : ∀ {n} → B n → C n) →
               (∀ {n} x → h ∘ f {n} x ≗ g x ∘ h) →
               ∀ {n} → h ∘ foldr B {n} f e ≗ foldr C g (h e)
foldr-fusion {B = B} {f} e {C} h fuse =
  foldr-universal C _ _ refl (λ x xs → fuse x (foldr B f e xs))

-- The identity function is a fold.

idIsFold : ∀ {A n} → id ≗ foldr (Vec A) {n} _∷_ []
idIsFold = foldr-universal _ _ id refl (λ _ _ → refl)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module Issue1691 where

open import Common.Equality
open import Issue1691.Nat  -- works if we inline this module

∸1≗pred :  ∀ n → n ∸ suc 0 ≡ pred n  -- works if zero is replaced by 0
∸1≗pred zero    = refl
∸1≗pred (suc _) = refl


text:
-- Agda supports full unicode everywhere. An Agda file should be written using
-- the UTF-8 encoding.

module Introduction.Unicode where

module ユーニコード where

  data _∧_ (P Q : Prop) : Prop where
    ∧-intro : P -> Q -> P ∧ Q

  ∧-elim₁ : {P Q : Prop} -> P ∧ Q -> P
  ∧-elim₁ (∧-intro p _) = p

  ∧-elim₂ : {P Q : Prop} -> P ∧ Q -> Q
  ∧-elim₂ (∧-intro _ q) = q

  data _∨_ (P Q : Prop) : Prop where
    ∨-intro₁ : P -> P ∨ Q
    ∨-intro₂ : Q -> P ∨ Q

  ∨-elim : {P Q R : Prop} -> (P -> R) -> (Q -> R) -> P ∨ Q -> R
  ∨-elim f g (∨-intro₁ p) = f p
  ∨-elim f g (∨-intro₂ q) = g q

  data ⊥ : Prop where

  data ⊤ : Prop where
    ⊤-intro : ⊤

  data ¬_ (P : Prop) : Prop where
    ¬-intro : (P -> ⊥) -> ¬ P

  data ∏ {A : Set}(P : A -> Prop) : Prop where
    ∏-intro : ((x : A) -> P x) -> ∏ P


text:
------------------------------------------------------------------------
-- Abstract grammars
------------------------------------------------------------------------

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

module Grammar.Abstract where

open import Data.Bool
open import Data.Char
open import Data.Empty
open import Data.List
open import Data.Product
open import Data.Sum
open import Function
open import Relation.Binary.PropositionalEquality using (_≡_)

------------------------------------------------------------------------
-- Grammars

-- I use an abstract and general definition of grammars: a grammar is
-- a predicate that relates strings with parse results.

Grammar : Set → Set₁
Grammar A = A → List Char → Set

------------------------------------------------------------------------
-- Grammar combinators

-- A grammar for no strings.

fail : ∀ {A} → Grammar A
fail = λ _ _ → ⊥

-- Symmetric choice.

infixl 10 _∣_

_∣_ : ∀ {A} → Grammar A → Grammar A → Grammar A
g₁ ∣ g₂ = λ x s → g₁ x s ⊎ g₂ x s

-- Grammars for the empty string.

return : ∀ {A} → A → Grammar A
return x = λ y s → y ≡ x × s ≡ []

-- Map.

infixl 20 _<$>_ _<$_

_<$>_ : ∀ {A B} → (A → B) → Grammar A → Grammar B
f <$> g = λ x s → ∃ λ y → g y s × x ≡ f y

_<$_ : ∀ {A B} → A → Grammar B → Grammar A
x <$ g = const x <$> g

-- A sequencing combinator for partially applied grammars.

seq : (List Char → Set) → (List Char → Set) → (List Char → Set)
seq p₁ p₂ = λ s → ∃₂ λ s₁ s₂ → p₁ s₁ × p₂ s₂ × s ≡ s₁ ++ s₂

-- Monadic bind.

infixl 15 _>>=_ _>>_

_>>=_ : ∀ {A B} → Grammar A → (A → Grammar B) → Grammar B
g₁ >>= g₂ = λ y s → ∃ λ x → seq (g₁ x) (g₂ x y) s

_>>_ : ∀ {A B} → Grammar A → Grammar B → Grammar B
g₁ >> g₂ = g₁ >>= λ _ → g₂

-- "Applicative" sequencing.

infixl 20 _⊛_ _<⊛_ _⊛>_

_⊛_ : ∀ {A B} → Grammar (A → B) → Grammar A → Grammar B
g₁ ⊛ g₂ = g₁ >>= λ f → f <$> g₂

_<⊛_ : ∀ {A B} → Grammar A → Grammar B → Grammar A
g₁ <⊛ g₂ = λ x s → ∃ λ y → seq (g₁ x) (g₂ y) s

_⊛>_ : ∀ {A B} → Grammar A → Grammar B → Grammar B
_⊛>_ = _>>_

-- Kleene star.

infix 30 _⋆ _+

_⋆ : ∀ {A} → Grammar A → Grammar (List A)
(g ⋆) []       s = s ≡ []
(g ⋆) (x ∷ xs) s = seq (g x) ((g ⋆) xs) s

_+ : ∀ {A} → Grammar A → Grammar (List A)
(g +) []       s = ⊥
(g +) (x ∷ xs) s = (g ⋆) (x ∷ xs) s

-- Elements separated by something.

infixl 18 _sep-by_

_sep-by_ : ∀ {A B} → Grammar A → Grammar B → Grammar (List A)
g sep-by sep = _∷_ <$> g ⊛ (sep >> g) ⋆

-- A grammar for an arbitrary token.

token : Grammar Char
token = λ c s → s ≡ [ c ]

-- A grammar for a given token.

tok : Char → Grammar Char
tok c = λ c′ s → c′ ≡ c × token c′ s

-- A grammar for tokens satisfying a given predicate.

sat : (p : Char → Bool) → Grammar (∃ λ t → T (p t))
sat _ = λ { (c , _) s → token c s }

-- A grammar for whitespace.

whitespace : Grammar Char
whitespace = tok ' ' ∣ tok '\n'

-- A grammar for a given string.

string : List Char → Grammar (List Char)
string s = λ s′ s″ → s′ ≡ s × s″ ≡ s

-- A grammar for the given string, possibly followed by some
-- whitespace.

symbol : List Char → Grammar (List Char)
symbol s = string s <⊛ whitespace ⋆

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module Number.Instances.QuoQ where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)

open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool as Bool using (Bool; not; true; false)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_; inl to inlᵖ; inr to inrᵖ)
open import Function.Base using (it; _∋_; _$_)
open import Cubical.Foundations.Isomorphism

open import Cubical.HITs.PropositionalTruncation --.Properties

open import Utils using (!_; !!_)
open import MoreLogic.Reasoning
open import MoreLogic.Definitions
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Structures
open import MorePropAlgebra.Bundles
open import MorePropAlgebra.Consequences
open import Number.Structures2
open import Number.Bundles2

open import Cubical.Data.Nat using (suc; zero; ℕ) renaming
  ( _*_ to _*ⁿ_
  ; +-comm to +ⁿ-comm
  ; +-assoc to +ⁿ-assoc
  ; *-comm to *ⁿ-comm
  ; *-suc to *ⁿ-suc
  ; *-assoc to *ⁿ-assoc
  ; +-suc to +ⁿ-suc
  ; *-distribˡ to *ⁿ-distribˡ
  ; *-distribʳ to *ⁿ-distribʳ
  ; *-identityʳ to *ⁿ-identityʳ
  ; snotz to snotzⁿ
  ; injSuc to injSucⁿ
  )
open import Cubical.Data.NatPlusOne using (HasFromNat; 1+_; ℕ₊₁; ℕ₊₁→ℕ)
open import Cubical.HITs.Ints.QuoInt using (HasFromNat; signed) renaming
  ( abs to absᶻ
  ; pos to pos
  ; neg to neg
  )

open import Number.Instances.QuoInt using (ℤbundle) renaming
  ( _<ᶠ_ to _<ᶻ_
  ; ·-reflects-<ᶠ to ·ᶻ-reflects-<ᶻ
  )

open import Cubical.Data.Nat.Order using () renaming
  ( ¬-<-zero to ¬-<ⁿ-zero )

module Definitions where
  open import Cubical.HITs.Ints.QuoInt hiding (_+_; -_; +-assoc; +-comm)
  open LinearlyOrderedCommRing ℤbundle
  -- open IsLinearlyOrderedCommRing is-LinearlyOrderedCommRing
  open import Cubical.HITs.Rationals.QuoQ using
    ( ℚ
    ; onCommonDenom
    ; onCommonDenomSym
    ; eq/
    ; _//_
    ; _∼_
    )
    renaming
    ( [_] to [_]ᶠ
    ; ℕ₊₁→ℤ to [1+_ⁿ]ᶻ
    )

  abstract
    0<1 : [ 0 < 1 ]
    0<1 = 0 , refl

    -- TODO: import these properties from somewhere else
    +-reflects-<      : ∀ x y z → [ (x + z < y + z) ⇒ (    x < y    ) ]
    +-preserves-<     : ∀ x y z → [ (    x < y    ) ⇒ (x + z < y + z) ]
    +-creates-<       : ∀ x y z → [ (    x < y    ) ⇔ (x + z < y + z) ]

    +-preserves-< a b x = snd (
      ( a            <  b           ) ⇒ᵖ⟨ transport (λ i → [ sym (fst (+-identity a)) i < sym (fst (+-identity b)) i ]) ⟩
      ( a +    0f    <  b +    0f   ) ⇒ᵖ⟨ transport (λ i → [ a + sym (+-rinv x) i < b + sym (+-rinv x) i ]) ⟩
      ( a + (x  - x) <  b + (x  - x)) ⇒ᵖ⟨ transport (λ i → [ +-assoc a x (- x) i < +-assoc b x (- x) i ]) ⟩
      ((a +  x) - x  < (b +  x) - x ) ⇒ᵖ⟨ +-<-ext (a + x) (- x) (b + x) (- x) ⟩
      ((a + x < b + x) ⊔ (- x < - x)) ⇒ᵖ⟨ (λ q → case q as (a + x < b + x) ⊔ (- x < - x) ⇒ a + x < b + x of λ
                                          { (inl a+x<b+x) → a+x<b+x -- somehow ⊥-elim needs a hint in the next line
                                          ; (inr  -x<-x ) → ⊥-elim {A = λ _ → [ a + x < b + x ]} (<-irrefl (- x) -x<-x)
                                          }) ⟩
       a + x < b + x ◼ᵖ)

    +-reflects-< x y z = snd
      ( x + z < y + z              ⇒ᵖ⟨ +-preserves-< (x + z) (y + z) (- z) ⟩
        (x + z) - z  < (y + z) - z ⇒ᵖ⟨ transport (λ i → [ +-assoc x z (- z) (~ i) < +-assoc y z (- z) (~ i) ]) ⟩
        x + (z - z) < y + (z - z)  ⇒ᵖ⟨ transport (λ i → [ x + +-rinv z i < y + +-rinv z i ]) ⟩
        x + 0f < y + 0f            ⇒ᵖ⟨ transport (λ i → [ fst (+-identity x) i < fst (+-identity y) i ]) ⟩
        x < y                      ◼ᵖ)

    +-creates-< x y z .fst = +-preserves-< x y z
    +-creates-< x y z .snd = +-reflects-<  x y z

    suc-creates-< : ∀ x y → [ (x < y) ⇔ (sucℤ x < sucℤ y) ]
    suc-creates-< x y .fst p = substₚ (λ p → sucℤ x < p) (∣ +-comm y (pos 1) ∣) $ substₚ (λ p → p < y + pos 1) (∣ +-comm x (pos 1) ∣) (+-preserves-< x y (pos 1) p)
    suc-creates-< x y .snd p = +-reflects-< x y (pos 1) $ substₚ (λ p → p < y + pos 1) (∣ +-comm (pos 1) x ∣) $ substₚ (λ p → sucℤ x < p) (∣ +-comm (pos 1) y ∣) p

    +-creates-≤ : ∀ a b x → [ (a ≤ b) ⇔ ((a + x) ≤ (b + x)) ]
    +-creates-≤ a b x = {!   !}

    ·-creates-< : ∀ a b x → [ 0 < x ] → [ (a < b) ⇔ ((a * x) < (b * x)) ]
    ·-creates-< a b x p .fst q = ·-preserves-< a b x p q
    ·-creates-< a b x p .snd q = ·ᶻ-reflects-<ᶻ a b x p q

    ·-creates-≤ : ∀ a b x → [ 0f ≤ x ] → [ (a ≤ b) ⇔ ((a · x) ≤ (b · x)) ]
    ·-creates-≤ a b x 0≤x .fst p = {!   !}
    ·-creates-≤ a b x 0≤x .snd p = {!   !}

    ·-creates-≤-≡ : ∀ a b x → [ 0f ≤ x ] → (a ≤ b) ≡ ((a · x) ≤ (b · x))
    ·-creates-≤-≡ a b x 0≤x = uncurry ⇔toPath $ ·-creates-≤ a b x 0≤x

  ℤlattice : Lattice {ℓ-zero} {ℓ-zero}
  ℤlattice = record { LinearlyOrderedCommRing ℤbundle renaming (≤-Lattice to is-Lattice) }

  open import MorePropAlgebra.Properties.Lattice ℤlattice
  open OnSet is-set hiding (+-min-distribʳ; ·-min-distribʳ; +-max-distribʳ; ·-max-distribʳ)

  abstract
    ≤-dicho : ∀ x y → [ (x ≤ y) ⊔ (y ≤ x) ]
    ≤-dicho x y with <-tricho x y
    ... | inl (inl x<y) = inlᵖ $ <-asym x y x<y
    ... | inl (inr y<x) = inrᵖ $ <-asym y x y<x
    ... | inr      x≡y  = inlᵖ $ subst (λ p → [ ¬(p <ᶻ x) ]) x≡y (<-irrefl x)

    ≤-min-+ : ∀ a b c w → [ w ≤ (a + c) ] → [ w ≤ (b + c) ] → [ w ≤ (min a b + c) ]
    ≤-max-+ : ∀ a b c w → [ (a + c) ≤ w ] → [ (b + c) ≤ w ] → [ (max a b + c) ≤ w ]
    ≤-min-· : ∀ a b c w → [ w ≤ (a · c) ] → [ w ≤ (b · c) ] → [ w ≤ (min a b · c) ]
    ≤-max-· : ∀ a b c w → [ (a · c) ≤ w ] → [ (b · c) ≤ w ] → [ (max a b · c) ≤ w ]

    ≤-min-+ = OnType.≤-dicho⇒+.≤-min-+ _+_ ≤-dicho
    ≤-max-+ = OnType.≤-dicho⇒+.≤-max-+ _+_ ≤-dicho
    ≤-min-· = OnType.≤-dicho⇒·.≤-min-· _·_ ≤-dicho
    ≤-max-· = OnType.≤-dicho⇒·.≤-max-· _·_ ≤-dicho

    +-min-distribʳ : ∀ x y z              → (min x y + z) ≡ min (x + z) (y + z)
    ·-min-distribʳ : ∀ x y z → [ 0f ≤ z ] → (min x y · z) ≡ min (x · z) (y · z)
    +-max-distribʳ : ∀ x y z              → (max x y + z) ≡ max (x + z) (y + z)
    ·-max-distribʳ : ∀ x y z → [ 0f ≤ z ] → (max x y · z) ≡ max (x · z) (y · z)
    +-min-distribˡ : ∀ x y z              → (z + min x y) ≡ min (z + x) (z + y)
    ·-min-distribˡ : ∀ x y z → [ 0f ≤ z ] → (z · min x y) ≡ min (z · x) (z · y)
    +-max-distribˡ : ∀ x y z              → (z + max x y) ≡ max (z + x) (z + y)
    ·-max-distribˡ : ∀ x y z → [ 0f ≤ z ] → (z · max x y) ≡ max (z · x) (z · y)

    +-min-distribʳ = OnSet.+-min-distribʳ is-set _+_ +-creates-≤ ≤-min-+
    ·-min-distribʳ = OnSet.·-min-distribʳ is-set 0f _·_ ·-creates-≤ ≤-min-·
    +-max-distribʳ = OnSet.+-max-distribʳ is-set _+_ +-creates-≤ ≤-max-+
    ·-max-distribʳ = OnSet.·-max-distribʳ is-set 0f _·_ ·-creates-≤ ≤-max-·

    +-min-distribˡ x y z   = +-comm z (min x y) ∙ +-min-distribʳ x y z   ∙ (λ i → min (+-comm x z i) (+-comm y z i))
    ·-min-distribˡ x y z p = ·-comm z (min x y) ∙ ·-min-distribʳ x y z p ∙ (λ i → min (·-comm x z i) (·-comm y z i))
    +-max-distribˡ x y z   = +-comm z (max x y) ∙ +-max-distribʳ x y z   ∙ (λ i → max (+-comm x z i) (+-comm y z i))
    ·-max-distribˡ x y z p = ·-comm z (max x y) ∙ ·-max-distribʳ x y z p ∙ (λ i → max (·-comm x z i) (·-comm y z i))

    pos<pos[suc] : ∀ x → [ pos x < pos (suc x) ]
    pos<pos[suc] 0 = 0<1
    pos<pos[suc] (suc x) = suc-creates-< (pos x) (pos (suc x)) .fst (pos<pos[suc] x)

    0<ᶻpos[suc] : ∀ x → [ 0 < pos (suc x) ]
    0<ᶻpos[suc]      0  = 0<1
    0<ᶻpos[suc] (suc x) = <-trans 0 (pos (suc x)) (pos (suc (suc x))) (0<ᶻpos[suc] x) (suc-creates-< (pos x) (pos (suc x)) .fst (pos<pos[suc] x))

    -- *-nullifiesʳ : ∀(x : ℤ) → x * 0 ≡ 0
    -- *-nullifiesʳ (pos zero) = refl
    -- *-nullifiesʳ (pos (suc n)) = {! *-nullifiesʳ (pos n)  !}
    -- *-nullifiesʳ (neg zero) = refl
    -- *-nullifiesʳ (neg (suc n)) = {! *-nullifiesʳ (neg n)  !}
    -- *-nullifiesʳ (posneg i) = refl

    *-nullifiesˡ : ∀(x : ℤ) → 0 * x ≡ 0
    *-nullifiesˡ x = {!   !}

    *-preserves-<0 : ∀ a b → [ 0 < a ] → [ 0 < b ] → [ 0 < a * b ]
    *-preserves-<0 a b p q = subst (λ p → [ p < a * b ]) (*-nullifiesˡ b) (·-preserves-< 0 a b q p)

    -- data Trichotomy

    ·-creates-<-≡ : ∀ a b x → [ 0 < x ] → (a < b) ≡ ((a * x) < (b * x))
    ·-creates-<-≡ a b x p = ⇔toPath (·-creates-< a b x p .fst) (·-creates-< a b x p .snd)

  open import Cubical.HITs.SetQuotients as SetQuotient using () renaming (_/_ to _//_)

  abstract
    lemma1 : ∀ a b₁ b₂ c → (a * b₁) * (b₂ * c) ≡ (a * c) * (b₂ * b₁)
    lemma1 a b₁ b₂ c =
      (a * b₁) * (b₂ * c) ≡⟨ sym $ ·-assoc a b₁ (b₂ * c) ⟩
      a * (b₁ * (b₂ * c)) ≡⟨ (λ i → a * ·-assoc b₁ b₂ c i) ⟩
      a * ((b₁ * b₂) * c) ≡⟨ (λ i → a * ·-comm (b₁ * b₂) c i) ⟩
      a * (c * (b₁ * b₂)) ≡⟨ ·-assoc a c (b₁ * b₂) ⟩
      (a * c) * (b₁ * b₂) ≡⟨ (λ i → (a * c) * ·-comm b₁ b₂ i) ⟩
      (a * c) * (b₂ * b₁) ∎

  -- TODO: we might extract definition and properties in the where clauses upfront
  infixl 4 _<ᶠ_
  _<ᶠ_ : hPropRel ℚ ℚ ℓ-zero
  a <ᶠ b = SetQuotient.rec2 {R = _∼_} {B = hProp ℓ-zero} isSetHProp _<'_ <'-respects-∼ˡ <'-respects-∼ʳ a b where
    _<'_ : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → hProp ℓ-zero
    (aᶻ , aⁿ) <' (bᶻ , bⁿ) =
      let aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
          bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
      in (aᶻ * bⁿᶻ) < (bᶻ * aⁿᶻ)
    abstract
      <'-respects-∼ˡ : ∀ a b x → a ∼ b → a <' x ≡ b <' x
      <'-respects-∼ˡ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) x@(xᶻ , xⁿ) a~b = γ where
        aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
        bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
        xⁿᶻ = [1+ xⁿ ⁿ]ᶻ
        0<aⁿᶻ : [ 0 < aⁿᶻ ]
        0<aⁿᶻ = 0<ᶻpos[suc] _
        0<bⁿᶻ : [ 0 < bⁿᶻ ]
        0<bⁿᶻ = 0<ᶻpos[suc] _
        p : aᶻ * bⁿᶻ ≡ bᶻ * aⁿᶻ
        p = a~b
        γ : ((aᶻ * xⁿᶻ) < (xᶻ * aⁿᶻ)) ≡ ((bᶻ * xⁿᶻ) < (xᶻ * bⁿᶻ))
        γ with <-tricho 0 aᶻ
        ... | inl (inl 0<aᶻ) =
          (aᶻ * xⁿᶻ)              < (xᶻ * aⁿᶻ)              ≡⟨ ·-creates-<-≡ (aᶻ * xⁿᶻ) (xᶻ * aⁿᶻ) (aᶻ * bⁿᶻ) (*-preserves-<0 aᶻ bⁿᶻ 0<aᶻ 0<bⁿᶻ) ⟩
          (aᶻ * xⁿᶻ) * (aᶻ * bⁿᶻ) < (xᶻ * aⁿᶻ) * (aᶻ * bⁿᶻ) ≡⟨ (λ i → (aᶻ * xⁿᶻ) * p i < (xᶻ * aⁿᶻ) * (aᶻ * bⁿᶻ)) ⟩
          (aᶻ * xⁿᶻ) * (bᶻ * aⁿᶻ) < (xᶻ * aⁿᶻ) * (aᶻ * bⁿᶻ) ≡⟨ (λ i → ·-comm (aᶻ * xⁿᶻ) (bᶻ * aⁿᶻ) i < (xᶻ * aⁿᶻ) * (aᶻ * bⁿᶻ)) ⟩
          (bᶻ * aⁿᶻ) * (aᶻ * xⁿᶻ) < (xᶻ * aⁿᶻ) * (aᶻ * bⁿᶻ) ≡⟨ (λ i → lemma1 bᶻ aⁿᶻ aᶻ xⁿᶻ i < lemma1 xᶻ aⁿᶻ aᶻ bⁿᶻ i) ⟩
          (bᶻ * xⁿᶻ) * (aᶻ * aⁿᶻ) < (xᶻ * bⁿᶻ) * (aᶻ * aⁿᶻ) ≡⟨ sym $ ·-creates-<-≡ (bᶻ * xⁿᶻ) (xᶻ * bⁿᶻ) (aᶻ * aⁿᶻ) (*-preserves-<0 aᶻ aⁿᶻ 0<aᶻ 0<aⁿᶻ) ⟩
          (bᶻ * xⁿᶻ)              < (xᶻ * bⁿᶻ)              ∎
        ... | inl (inr aᶻ<0) = {!   !}
        ... | inr      0≡aᶻ  =
          (aᶻ * xⁿᶻ) < (xᶻ * aⁿᶻ) ≡⟨ {!   !} ⟩
          ( 0 * xⁿᶻ) < (xᶻ * aⁿᶻ) ≡⟨ {!   !} ⟩
            0        < (xᶻ * aⁿᶻ) ≡⟨ {! κ   !} ⟩
            0        < (xᶻ * bⁿᶻ) ≡⟨ {!   !} ⟩
          ( 0 * xⁿᶻ) < (xᶻ * bⁿᶻ) ≡⟨ {!   !} ⟩
          (bᶻ * xⁿᶻ) < (xᶻ * bⁿᶻ) ∎ where
            bᶻ≡0 : bᶻ ≡ 0
            bᶻ≡0 = {!   !}
            κ : ∀ x y z → [ 0 < y ] → [ 0 < z ] → (0 < (x * y)) ≡ (0 < (x * z))
            κ x y z p q =
               0      < (x * y) ≡⟨ {!   !} ⟩
              (0 * y) < (x * y) ≡⟨ {!   !} ⟩
               0      <  x      ≡⟨ {!   !} ⟩
              (0 * z) < (x * z) ≡⟨ {!   !} ⟩
               0      < (x * z) ∎
        -- in (aᶻ * xⁿᶻ)              < (xᶻ * aⁿᶻ)              ≡⟨ {!   !} ⟩
        --    (aᶻ * xⁿᶻ) / (aᶻ * bⁿᶻ) < (xᶻ * aⁿᶻ) / (bᶻ * aⁿᶻ) ≡⟨ {!   !} ⟩
        --          xⁿᶻ  /       bⁿᶻ  <  xᶻ        /  bᶻ        ≡⟨ {!   !} ⟩
        --    (bᶻ * xⁿᶻ) < (xᶻ * bⁿᶻ) ∎

        -- aᶻ > 0:
    abstract
      <'-respects-∼ʳ : ∀ x a b → a ∼ b → x <' a ≡ x <' b
      <'-respects-∼ʳ x@(xᶻ , xⁿ) a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) a~b =
        let aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
            bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
            xⁿᶻ = [1+ xⁿ ⁿ]ᶻ
            p : aᶻ * bⁿᶻ ≡ bᶻ * aⁿᶻ
            p = a~b
        in (xᶻ * aⁿᶻ)              < (aᶻ * xⁿᶻ)              ≡⟨ {!   !} ⟩
           (xᶻ * aⁿᶻ) * (aᶻ * bⁿᶻ) < (aᶻ * xⁿᶻ) * (aᶻ * bⁿᶻ) ≡⟨ {!   !} ⟩
           (xᶻ * aⁿᶻ) * (aᶻ * bⁿᶻ) < (aᶻ * xⁿᶻ) * (bᶻ * aⁿᶻ) ≡⟨ {!   !} ⟩
           (xᶻ * aⁿᶻ) * (aᶻ * bⁿᶻ) < (bᶻ * aⁿᶻ) * (aᶻ * xⁿᶻ) ≡⟨ {!   !} ⟩
           (xᶻ * bⁿᶻ) * (aᶻ * aⁿᶻ) < (bᶻ * xⁿᶻ) * (aᶻ * aⁿᶻ) ≡⟨ {!   !} ⟩
           (xᶻ * bⁿᶻ)              < (bᶻ * xⁿᶻ)              ∎

  _≤ᶠ_ : hPropRel ℚ ℚ ℓ-zero
  x ≤ᶠ y = ¬ᵖ (y <ᶠ x)

  minᶠ : ℚ → ℚ → ℚ
  minᶠ a b = onCommonDenomSym min' min'-sym min'-respects-∼ a b where
    min' : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → ℤ
    min' (aᶻ , aⁿ) (bᶻ , bⁿ) =
      let aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
          bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
      in min (aᶻ * bⁿᶻ) (bᶻ * aⁿᶻ)
    abstract
      min'-sym : ∀ x y → min' x y ≡ min' y x
      min'-sym (aᶻ , aⁿ) (bᶻ , bⁿ) = min-comm (aᶻ * [1+ bⁿ ⁿ]ᶻ) (bᶻ * [1+ aⁿ ⁿ]ᶻ)
      min'-respects-∼ : (a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) x@(xᶻ , xⁿ) : ℤ × ℕ₊₁)
        → a ∼ b
        → [1+ bⁿ ⁿ]ᶻ * min' a x ≡ [1+ aⁿ ⁿ]ᶻ * min' b x
      min'-respects-∼ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) x@(xᶻ , xⁿ) a~b =
        bⁿᶻ * min (aᶻ * xⁿᶻ) (xᶻ * aⁿᶻ)           ≡⟨ ·-min-distribˡ (aᶻ * xⁿᶻ) (xᶻ * aⁿᶻ) bⁿᶻ 0≤bⁿᶻ ⟩
        min (bⁿᶻ * (aᶻ * xⁿᶻ)) (bⁿᶻ * (xᶻ * aⁿᶻ)) ≡⟨ (λ i → min (·-assoc bⁿᶻ aᶻ xⁿᶻ i) (bⁿᶻ * (xᶻ * aⁿᶻ))) ⟩
        min ((bⁿᶻ * aᶻ) * xⁿᶻ) (bⁿᶻ * (xᶻ * aⁿᶻ)) ≡⟨ (λ i → min ((·-comm bⁿᶻ aᶻ i) * xⁿᶻ) (bⁿᶻ * (xᶻ * aⁿᶻ))) ⟩
        min ((aᶻ * bⁿᶻ) * xⁿᶻ) (bⁿᶻ * (xᶻ * aⁿᶻ)) ≡⟨ (λ i → min (p i * xⁿᶻ) (bⁿᶻ * (xᶻ * aⁿᶻ))) ⟩
        min ((bᶻ * aⁿᶻ) * xⁿᶻ) (bⁿᶻ * (xᶻ * aⁿᶻ)) ≡⟨ (λ i → min (·-comm bᶻ aⁿᶻ i * xⁿᶻ) (·-assoc bⁿᶻ xᶻ aⁿᶻ i)) ⟩
        min ((aⁿᶻ * bᶻ) * xⁿᶻ) ((bⁿᶻ * xᶻ) * aⁿᶻ) ≡⟨ (λ i → min (·-assoc aⁿᶻ bᶻ xⁿᶻ (~ i)) (·-comm (bⁿᶻ * xᶻ) aⁿᶻ i)) ⟩
        min (aⁿᶻ * (bᶻ * xⁿᶻ)) (aⁿᶻ * (bⁿᶻ * xᶻ)) ≡⟨ sym $ ·-min-distribˡ (bᶻ * xⁿᶻ) (bⁿᶻ * xᶻ) aⁿᶻ 0≤aⁿᶻ ⟩
        aⁿᶻ * min (bᶻ * xⁿᶻ) (bⁿᶻ * xᶻ)           ≡⟨ (λ i → aⁿᶻ * min (bᶻ * xⁿᶻ) (·-comm bⁿᶻ xᶻ i)) ⟩
        aⁿᶻ * min (bᶻ * xⁿᶻ) (xᶻ * bⁿᶻ)           ∎
        where
          aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
          bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
          xⁿᶻ = [1+ xⁿ ⁿ]ᶻ
          p : aᶻ * bⁿᶻ ≡ bᶻ * aⁿᶻ
          p = a~b
          0≤aⁿᶻ : [ 0 ≤ aⁿᶻ ]
          0≤aⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p
          0≤bⁿᶻ : [ 0 ≤ bⁿᶻ ]
          0≤bⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p

  -- same proof as for min
  maxᶠ : ℚ → ℚ → ℚ
  maxᶠ a b = onCommonDenomSym max' max'-sym max'-respects-∼ a b where
    max' : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → ℤ
    max' (aᶻ , aⁿ) (bᶻ , bⁿ) =
      let aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
          bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
      in max (aᶻ * bⁿᶻ) (bᶻ * aⁿᶻ)
    abstract
      max'-sym : ∀ x y → max' x y ≡ max' y x
      max'-sym (aᶻ , aⁿ) (bᶻ , bⁿ) = max-comm (aᶻ * [1+ bⁿ ⁿ]ᶻ) (bᶻ * [1+ aⁿ ⁿ]ᶻ)
      max'-respects-∼ : (a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) x@(xᶻ , xⁿ) : ℤ × ℕ₊₁)
        → a ∼ b
        → [1+ bⁿ ⁿ]ᶻ * max' a x ≡ [1+ aⁿ ⁿ]ᶻ * max' b x
      max'-respects-∼ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) x@(xᶻ , xⁿ) a~b =
        bⁿᶻ * max (aᶻ * xⁿᶻ) (xᶻ * aⁿᶻ)           ≡⟨ ·-max-distribˡ (aᶻ * xⁿᶻ) (xᶻ * aⁿᶻ) bⁿᶻ 0≤bⁿᶻ ⟩
        max (bⁿᶻ * (aᶻ * xⁿᶻ)) (bⁿᶻ * (xᶻ * aⁿᶻ)) ≡⟨ (λ i → max (·-assoc bⁿᶻ aᶻ xⁿᶻ i) (bⁿᶻ * (xᶻ * aⁿᶻ))) ⟩
        max ((bⁿᶻ * aᶻ) * xⁿᶻ) (bⁿᶻ * (xᶻ * aⁿᶻ)) ≡⟨ (λ i → max ((·-comm bⁿᶻ aᶻ i) * xⁿᶻ) (bⁿᶻ * (xᶻ * aⁿᶻ))) ⟩
        max ((aᶻ * bⁿᶻ) * xⁿᶻ) (bⁿᶻ * (xᶻ * aⁿᶻ)) ≡⟨ (λ i → max (p i * xⁿᶻ) (bⁿᶻ * (xᶻ * aⁿᶻ))) ⟩
        max ((bᶻ * aⁿᶻ) * xⁿᶻ) (bⁿᶻ * (xᶻ * aⁿᶻ)) ≡⟨ (λ i → max (·-comm bᶻ aⁿᶻ i * xⁿᶻ) (·-assoc bⁿᶻ xᶻ aⁿᶻ i)) ⟩
        max ((aⁿᶻ * bᶻ) * xⁿᶻ) ((bⁿᶻ * xᶻ) * aⁿᶻ) ≡⟨ (λ i → max (·-assoc aⁿᶻ bᶻ xⁿᶻ (~ i)) (·-comm (bⁿᶻ * xᶻ) aⁿᶻ i)) ⟩
        max (aⁿᶻ * (bᶻ * xⁿᶻ)) (aⁿᶻ * (bⁿᶻ * xᶻ)) ≡⟨ sym $ ·-max-distribˡ (bᶻ * xⁿᶻ) (bⁿᶻ * xᶻ) aⁿᶻ 0≤aⁿᶻ ⟩
        aⁿᶻ * max (bᶻ * xⁿᶻ) (bⁿᶻ * xᶻ)           ≡⟨ (λ i → aⁿᶻ * max (bᶻ * xⁿᶻ) (·-comm bⁿᶻ xᶻ i)) ⟩
        aⁿᶻ * max (bᶻ * xⁿᶻ) (xᶻ * bⁿᶻ)           ∎
        where
          aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
          bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
          xⁿᶻ = [1+ xⁿ ⁿ]ᶻ
          p : aᶻ * bⁿᶻ ≡ bᶻ * aⁿᶻ
          p = a~b
          0≤aⁿᶻ : [ 0 ≤ aⁿᶻ ]
          0≤aⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p
          0≤bⁿᶻ : [ 0 ≤ bⁿᶻ ]
          0≤bⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p

  -- maxᶠ : ℚ → ℚ → ℚ
  -- maxᶠ a b = onCommonDenom f g h a b where
  --   f : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → ℤ
  --   f (aᶻ , aⁿ) (bᶻ , bⁿ) = max (aᶻ * [1+ bⁿ ⁿ]ᶻ) (bᶻ * [1+ aⁿ ⁿ]ᶻ)
  --   g : (a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) c@(cᶻ , cⁿ) : ℤ × ℕ₊₁)
  --     → aᶻ * [1+ bⁿ ⁿ]ᶻ         ≡ bᶻ * [1+ aⁿ ⁿ]ᶻ
  --     →      [1+ bⁿ ⁿ]ᶻ * f a c ≡      [1+ aⁿ ⁿ]ᶻ * f b c
  --   g a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) c@(cᶻ , cⁿ) aᶻ*bⁿ'≡bᶻ*aⁿ' = let
  --     aⁿ' = [1+ aⁿ ⁿ]ᶻ
  --     bⁿ' = [1+ bⁿ ⁿ]ᶻ
  --     cⁿ' = [1+ cⁿ ⁿ]ᶻ
  --     0<aⁿ' : [ 0 < aⁿ' ]
  --     0<aⁿ' = 0<ᶻpos[suc] _
  --     0<bⁿ' : [ 0 < bⁿ' ]
  --     0<bⁿ' = 0<ᶻpos[suc] _
  --     0<cⁿ' : [ 0 < cⁿ' ]
  --     0<cⁿ' = 0<ᶻpos[suc] _
  --     γ : bⁿ' * max (aᶻ * cⁿ') (cᶻ * aⁿ')
  --       ≡ aⁿ' * max (bᶻ * cⁿ') (cᶻ * bⁿ')
  --     γ = {!   !}
  --     in γ
  --   h : (a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) c@(cᶻ , cⁿ) : ℤ × ℕ₊₁)
  --     →     bᶻ * [1+ cⁿ ⁿ]ᶻ ≡     cᶻ * [1+ bⁿ ⁿ]ᶻ
  --     → f a b  * [1+ cⁿ ⁿ]ᶻ ≡ f a c  * [1+ bⁿ ⁿ]ᶻ
  --   h a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) c@(cᶻ , cⁿ) bᶻ*cⁿ≡cᶻ*bⁿ = {!   !}

open Definitions public renaming
  ( _<ᶠ_ to _<_
  ; _≤ᶠ_ to _≤_
  ; minᶠ to min
  ; maxᶠ to max
  )

open LinearlyOrderedCommRing ℤbundle using () renaming
  ( min to minᶻ
  ; max to maxᶻ
  -- ; _<_ to _<ᶻ_
  ; _≤_ to _≤ᶻ_
  ; <-irrefl to <ᶻ-irrefl
  ; <-trans to <ᶻ-trans
  ; is-min to is-minᶻ
  ; is-max to is-maxᶻ
  ; ·-assoc to ·ᶻ-assoc
  ; ·-comm to ·ᶻ-comm
  ; <-tricho to <ᶻ-tricho
  ; -_ to -ᶻ_
  )

open import Cubical.HITs.Rationals.QuoQ renaming
  ( [_] to [_]ᶠ
  ; eq/ to eq/ᶠ
  ; ℕ₊₁→ℤ to [1+_ⁿ]ᶻ
  )

open import Cubical.HITs.SetQuotients as SetQuotient using () renaming (_/_ to _//_)
open import Cubical.HITs.Ints.QuoInt using (ℤ) renaming (_*_ to _*ᶻ_; sign to signᶻ)
open import Cubical.HITs.PropositionalTruncation renaming (elim to ∣∣-elim)

abstract
  <-irrefl : ∀ a → [ ¬(a < a) ]
  <-irrefl = SetQuotient.elimProp {R = _∼_} (λ a → isProp[] (¬(a < a))) γ where
    γ : (a : ℤ × ℕ₊₁) → [ ¬([ a ]ᶠ < [ a ]ᶠ) ]
    γ a@(aᶻ , aⁿ) = κ where
      aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
      κ : [ ¬((aᶻ *ᶻ aⁿᶻ) <ᶻ (aᶻ *ᶻ aⁿᶻ)) ]
      κ = <ᶻ-irrefl (aᶻ *ᶻ aⁿᶻ)

  <-trans : (a b c : ℚ) → [ a < b ] → [ b < c ] → [ a < c ]
  <-trans = SetQuotient.elimProp3 {R = _∼_} (λ a b c → isProp[] ((a < b) ⇒ (b < c) ⇒ (a < c))) γ where
    γ : (a b c : ℤ × ℕ₊₁) → [ [ a ]ᶠ < [ b ]ᶠ ] → [ [ b ]ᶠ < [ c ]ᶠ ] → [ [ a ]ᶠ < [ c ]ᶠ ]
    γ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) c@(cᶻ , cⁿ) = κ where
      aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
      bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
      cⁿᶻ = [1+ cⁿ ⁿ]ᶻ
      κ : [ (aᶻ *ᶻ bⁿᶻ) <ᶻ (bᶻ *ᶻ aⁿᶻ) ] → [ (bᶻ *ᶻ cⁿᶻ) <ᶻ (cᶻ *ᶻ bⁿᶻ) ] → [ (aᶻ *ᶻ cⁿᶻ) <ᶻ (cᶻ *ᶻ aⁿᶻ) ]
      -- strategy: multiply with xⁿᶻ and then use <ᶻ-trans
      κ = {!!}

  <-asym : ∀ a b → [ a < b ] → [ ¬(b < a) ]
  <-asym a b a<b b<a = <-irrefl a (<-trans a b a a<b b<a)

  <-irrefl'' : ∀ a b → [ a < b ] ⊎ [ b < a ] → [ ¬(a ≡ₚ b) ]
  <-irrefl'' a b (inl a<b) a≡b = <-irrefl b (substₚ (λ p → p < b) a≡b a<b)
  <-irrefl'' a b (inr b<a) a≡b = <-irrefl b (substₚ (λ p → b < p) a≡b b<a)

  <-tricho : (a b : ℚ) → ([ a < b ] ⊎ [ b < a ]) ⊎ [ a ≡ₚ b ] -- TODO: insert trichotomy definition here
  <-tricho = SetQuotient.elimProp2 {R = _∼_} (λ a b → isProp[] ([ <-irrefl'' a b ] ([ <-asym a b ] (a < b) ⊎ᵖ (b < a)) ⊎ᵖ (a ≡ₚ b))) γ where
    γ : (a b : ℤ × ℕ₊₁) → ([ [ a ]ᶠ < [ b ]ᶠ ] ⊎ [ [ b ]ᶠ < [ a ]ᶠ ]) ⊎ [ [ a ]ᶠ ≡ₚ [ b ]ᶠ ]
    γ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) = κ where
      aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
      bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
      κ : ([ (aᶻ *ᶻ bⁿᶻ) <ᶻ (bᶻ *ᶻ aⁿᶻ) ] ⊎ [ (bᶻ *ᶻ aⁿᶻ) <ᶻ (aᶻ *ᶻ bⁿᶻ) ]) ⊎ [ [ aᶻ , aⁿ ]ᶠ ≡ₚ [ bᶻ , bⁿ ]ᶠ ]
      κ with <ᶻ-tricho (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ)
      ... | inl p = inl p
      ... | inr p = inr ∣ eq/ᶠ {R = _∼_} a b p ∣

  <ᶻ-asym : ∀ a b → [ a <ᶻ b ] → [ ¬(b <ᶻ a) ]
  <ᶻ-asym a b a<b b<a = <ᶻ-irrefl a (<ᶻ-trans a b a a<b b<a)

_#ᶻ_ : hPropRel ℤ ℤ ℓ-zero
x #ᶻ y = [ <ᶻ-asym x y ] (x <ᶻ y) ⊎ᵖ (y <ᶻ x)

_#_ : hPropRel ℚ ℚ ℓ-zero
x # y = [ <-asym x y ] (x < y) ⊎ᵖ (y < x)

injᶻⁿ⁺¹ : ∀ x → [ 0 <ᶻ x ] → Σ[ y ∈ ℕ₊₁ ] x ≡ [1+ y ⁿ]ᶻ
injᶻⁿ⁺¹ (signed false zero) p = ⊥-elim {A = λ _ → Σ[ y ∈ ℕ₊₁ ] ℤ.posneg i0 ≡ [1+ y ⁿ]ᶻ}  (¬-<ⁿ-zero p)
injᶻⁿ⁺¹ (signed true  zero) p = ⊥-elim {A = λ _ → Σ[ y ∈ ℕ₊₁ ] ℤ.posneg i1 ≡ [1+ y ⁿ]ᶻ}  (¬-<ⁿ-zero p)
injᶻⁿ⁺¹ (ℤ.posneg i)        p = ⊥-elim {A = λ _ → Σ[ y ∈ ℕ₊₁ ] ℤ.posneg i  ≡ [1+ y ⁿ]ᶻ}  (¬-<ⁿ-zero p)
injᶻⁿ⁺¹ (signed false (suc n)) p =  1+ n , refl

abstract
  -flips-<ᶻ0 : ∀ x → [ (x <ᶻ 0) ⇔ (0 <ᶻ (-ᶻ x)) ]
  -flips-<ᶻ0 (signed false zero) = (λ x → x) , (λ x → x)
  -flips-<ᶻ0 (signed true  zero) = (λ x → x) , (λ x → x)
  -flips-<ᶻ0 (ℤ.posneg i)        = (λ x → x) , (λ x → x)
  -flips-<ᶻ0 (signed false (suc n)) .fst p  = ¬-<ⁿ-zero p
  -flips-<ᶻ0 (signed true  (suc n)) .fst tt = n , +ⁿ-comm n 1
  -flips-<ᶻ0 (signed true  (suc n)) .snd p  = tt

-- -flips-< : ∀ x y → [ x <ᶻ y ⇔ - y <ᶻ - x ]

-- #-Dichotomyˢ : {A : Type ℓ} (is-set : isSet A) (_#_ : hPropRel A A ℓ) )(#-tight : ∀ x y → [ x # y ⇔ ¬([ is-set ] x ≡ˢ y) ] ) (x : A) → hProp ℓ
-- #-Dichotomyˢ x = [ #-tight x 0 .fst ] x # 0 ⊎ᵖ (x ≡ 0)

#ᶻ-dicho : ∀ x → [ x #ᶻ 0 ] ⊎ (x ≡ 0)
#ᶻ-dicho x = <ᶻ-tricho x 0

⊕-identityʳ : ∀ s → (s Bool.⊕ false) ≡ s
⊕-identityʳ false = refl
⊕-identityʳ true  = refl

abstract
  *ᶻ-preserves-signˡ : ∀ x y → [ 0 <ᶻ y ] → signᶻ (x *ᶻ y) ≡ signᶻ x
  *ᶻ-preserves-signˡ x (signed false zero) p = ⊥-elim {A = λ _ → signᶻ (x *ᶻ ℤ.posneg i0) ≡ signᶻ x} (¬-<ⁿ-zero p)
  *ᶻ-preserves-signˡ x (signed true  zero) p = ⊥-elim {A = λ _ → signᶻ (x *ᶻ ℤ.posneg i1) ≡ signᶻ x} (¬-<ⁿ-zero p)
  *ᶻ-preserves-signˡ x (ℤ.posneg i)        p = ⊥-elim {A = λ _ → signᶻ (x *ᶻ ℤ.posneg i ) ≡ signᶻ x} (¬-<ⁿ-zero p)
  *ᶻ-preserves-signˡ (signed false zero) (signed false (suc n)) p = refl
  *ᶻ-preserves-signˡ (signed true  zero) (signed false (suc n)) p = refl
  *ᶻ-preserves-signˡ (ℤ.posneg i)        (signed false (suc n)) p = refl
  *ᶻ-preserves-signˡ (signed s (suc n₁)) (signed false (suc n)) p = ⊕-identityʳ s

absⁿ⁺¹' : ℤ → ℕ₊₁
absⁿ⁺¹' xᶻ with <ᶻ-tricho 0 xᶻ
... | inl (inl 0<xᶻ) = injᶻⁿ⁺¹ xᶻ 0<xᶻ .fst
... | inl (inr xᶻ<0) = injᶻⁿ⁺¹ (-ᶻ xᶻ) ( -flips-<ᶻ0 xᶻ .fst xᶻ<0) .fst
... | inr      0≡xᶻ  = 1+ 0 -- this case will be excluded lateron, but we keep it here to omit the definition of a nonzero ℚ

-- absⁿ⁺¹'-identity⁺ : ∀ x → signed false (ℕ₊₁→ℕ x) ≡ [1+ absⁿ⁺¹' x ⁿ]ᶻ
-- absⁿ⁺¹'-identity⁺ x = ?

absⁿ⁺¹'-identity⁺ : ∀ x → [1+ absⁿ⁺¹' (pos x) ⁿ]ᶻ ≡ pos x
absⁿ⁺¹'-identity⁺ x with <ᶻ-tricho 0 (pos x)
... | inl (inl 0<xᶻ) = {!!}
... | inl (inr xᶻ<0) = {!!}
... | inr      0≡xᶻ  = {!!}

_⁻¹''' : (x : ℚ) → [ x # 0 ] → ℚ
_⁻¹''' = {! SetQuotient.elim {R = _∼_} {B = λ x → [ x # 0 ] → ℚ} φ _⁻¹'' ⁻¹''-respects-∼   !} where
  φ : ∀ x → isSet ([ x # 0 ] → ℚ)
  φ x = isSetΠ (λ _ → isSetℚ)
  _⁻¹''  : (a : ℤ × ℕ₊₁) → [ [ a ]ᶠ # 0 ] → ℚ
  x ⁻¹'' = {!!}
  ⁻¹''-respects-∼ : (a b : ℤ × ℕ₊₁) (r : a ∼ b)
                  → PathP (λ i → [ eq/ᶠ a b r i # 0 ] → ℚ) (a ⁻¹'') (b ⁻¹'')
  ⁻¹''-respects-∼ a b r = {!!}

isSet→ : ∀{ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (isSet B) → isSet (A → B)
isSet→ {B = B} isset = isSetΠ λ _ → isset

_⁻¹' : ℚ → ℚ
_⁻¹' = SetQuotient.rec {R = _∼_} isSetℚ _⁻¹'' ⁻¹''-respects-∼  where
  _⁻¹'' : ℤ × ℕ₊₁ → ℚ
  (xᶻ , xⁿ) ⁻¹'' = [ signed (signᶻ xᶻ) (ℕ₊₁→ℕ xⁿ) , absⁿ⁺¹' xᶻ ]ᶠ
  ⁻¹''-respects-∼ : (a b : ℤ × ℕ₊₁) → a ∼ b → (a ⁻¹'') ≡ (b ⁻¹'')
  ⁻¹''-respects-∼ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) p = κ where
    aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
    bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
    0<aⁿᶻ : [ 0 <ᶻ aⁿᶻ ]
    0<aⁿᶻ = ℕ₊₁.n aⁿ , +ⁿ-comm (ℕ₊₁.n aⁿ) 1
    0<bⁿᶻ : [ 0 <ᶻ bⁿᶻ ]
    0<bⁿᶻ = ℕ₊₁.n bⁿ , +ⁿ-comm (ℕ₊₁.n bⁿ) 1
    q : aᶻ *ᶻ bⁿᶻ ≡ bᶻ *ᶻ aⁿᶻ
    q = p
    sign≡ =
      signᶻ aᶻ          ≡⟨ sym $ *ᶻ-preserves-signˡ aᶻ bⁿᶻ 0<bⁿᶻ ⟩
      signᶻ (aᶻ *ᶻ bⁿᶻ) ≡⟨ (λ i → signᶻ (q i)) ⟩
      signᶻ (bᶻ *ᶻ aⁿᶻ) ≡⟨ *ᶻ-preserves-signˡ bᶻ aⁿᶻ 0<aⁿᶻ ⟩
      signᶻ bᶻ          ∎
    cᶻ dᶻ : ℤ
    cᶻ = signed (signᶻ aᶻ) (ℕ₊₁→ℕ aⁿ)
    dᶻ = signed (signᶻ bᶻ) (ℕ₊₁→ℕ bⁿ)
    cⁿ dⁿ : ℕ₊₁
    cⁿ = absⁿ⁺¹' aᶻ
    dⁿ = absⁿ⁺¹' bᶻ
    t : ∀ s → (signed s (ℕ₊₁→ℕ aⁿ) *ᶻ [1+ absⁿ⁺¹' bᶻ ⁿ]ᶻ) ≡ (signed s (ℕ₊₁→ℕ bⁿ) *ᶻ [1+ absⁿ⁺¹' aᶻ ⁿ]ᶻ)
    t false = {!!}
    t true  = {!!}
    r : (signed (signᶻ aᶻ) (ℕ₊₁→ℕ aⁿ) *ᶻ [1+ absⁿ⁺¹' bᶻ ⁿ]ᶻ) ≡ (signed (signᶻ bᶻ) (ℕ₊₁→ℕ bⁿ) *ᶻ [1+ absⁿ⁺¹' aᶻ ⁿ]ᶻ)
    r = {!!}
    κ : ([ cᶻ , cⁿ  ]ᶠ) ≡ ([ dᶻ  , dⁿ  ]ᶠ)
    κ = eq/ᶠ {R = _∼_} (cᶻ , cⁿ) (dᶻ  , dⁿ) r

·-inv'' : ∀ x → [ (∃[ y ] ([ isSetℚ ] (x * y) ≡ˢ 1)) ⇔ (x # 0) ]
-- ·-inv'' x .fst p = {!   !}
-- ·-inv'' x .snd p = {!   !}
·-inv'' = SetQuotient.elimProp {R = _∼_} φ {!   !} where
  φ : (x : ℚ) → _
  φ x = isProp[] ((∃[ y ] ([ isSetℚ ] (x * y) ≡ˢ 1)) ⇔ (x # 0))
  κ₁ : ∀ x → [ ∃[ y ] ([ isSetℚ ] (x * y) ≡ˢ 1) ] → [ x # 0 ]
  κ₁ x p = ∣∣-elim (λ _ → φ') (λ{ (y , q) → γ y q } ) p    where
    φ' = isProp[] (x # 0)
    γ : ∀ y → [ [ isSetℚ ] (x * y) ≡ˢ 1 ] → [ x # 0 ]
    γ y q = {!!}
  κ₂ : ∀ x → [ x # 0 ] → [ ∃[ y ] ([ isSetℚ ] (x * y) ≡ˢ 1) ]
  κ₂ x (inl x<0) = {!   !}
  -- well.. we would need ℚ⁺ here
  κ₂ x (inr 0<x) =  ∣ SetQuotient.rec {R = _∼_} isSetℚ {!!} {!!} x , {!!} ∣ where
    _⁻¹⁺ : ℤ × ℕ₊₁ → ℚ
    _⁻¹⁺ (aᶻ , aⁿ) = {!!}

+-Semigroup : [ isSemigroup _+_ ]
+-Semigroup .IsSemigroup.is-set   = isSetℚ
+-Semigroup .IsSemigroup.is-assoc = +-assoc

·-Semigroup : [ isSemigroup _*_ ]
·-Semigroup .IsSemigroup.is-set   = isSetℚ
·-Semigroup .IsSemigroup.is-assoc = *-assoc

+-Monoid : [ isMonoid 0 _+_ ]
+-Monoid .IsMonoid.is-Semigroup  = +-Semigroup
+-Monoid .IsMonoid.is-identity x = +-identityʳ x , +-identityˡ x

·-Monoid : [ isMonoid 1 _*_ ]
·-Monoid .IsMonoid.is-Semigroup  = ·-Semigroup
·-Monoid .IsMonoid.is-identity x = *-identityʳ x , *-identityˡ x

is-Semiring : [ isSemiring 0 1 _+_ _*_ ]
is-Semiring .IsSemiring.+-Monoid = +-Monoid
is-Semiring .IsSemiring.·-Monoid = ·-Monoid
is-Semiring .IsSemiring.+-comm   = +-comm
is-Semiring .IsSemiring.is-dist x y z = sym (*-distribˡ x y z) , sym (*-distribʳ x y z)

is-CommSemiring : [ isCommSemiring 0 1 _+_ _*_ ]
is-CommSemiring .IsCommSemiring.is-Semiring = is-Semiring
is-CommSemiring .IsCommSemiring.·-comm      = *-comm

<-StrictLinearOrder : [ isStrictLinearOrder _<_ ]
<-StrictLinearOrder .IsStrictLinearOrder.is-irrefl = <-irrefl
<-StrictLinearOrder .IsStrictLinearOrder.is-trans  = <-trans
<-StrictLinearOrder .IsStrictLinearOrder.is-tricho = <-tricho

open import Cubical.Data.NatPlusOne using (_*₊₁_)

⇔toPath' : ∀{ℓ} {P Q : hProp ℓ} → [ P ⇔ Q ] → P ≡ Q
⇔toPath' = uncurry ⇔toPath

pathTo⇔ : ∀{ℓ} {P Q : hProp ℓ} → P ≡ Q → [ P ⇔ Q ]
pathTo⇔ p≡q = (pathTo⇒ p≡q , pathTo⇐ p≡q)

⊓⇔⊓ : ∀{ℓ ℓ' ℓ'' ℓ'''} {P : hProp ℓ} {Q : hProp ℓ'} {R : hProp ℓ''} {S : hProp ℓ'''}
   → [ (P ⇔ R) ⊓ (Q ⇔ S) ] → [ (P ⊓ Q) ⇔ (R ⊓ S) ]
⊓⇔⊓ (p⇔r , q⇔s) .fst (p , q) = p⇔r .fst p , q⇔s .fst q
⊓⇔⊓ (p⇔r , q⇔s) .snd (r , s) = p⇔r .snd r , q⇔s .snd s

⊓≡⊓ : ∀{ℓ} {P Q R S : hProp ℓ} → P ≡ R → Q ≡ S → (P ⊓ Q) ≡ (R ⊓ S)
⊓≡⊓ p≡r q≡s i = p≡r i ⊓ q≡s i

abstract
  is-min : (x y z : ℚ) → [ (z ≤ min x y) ⇔ (z ≤ x) ⊓ (z ≤ y) ]
  is-min = SetQuotient.elimProp3  {R = _∼_} (λ x y z → isProp[] ((z ≤ min x y) ⇔ (z ≤ x) ⊓ (z ≤ y))) γ where
    γ : (a b c : ℤ × ℕ₊₁) → [ ([ c ]ᶠ ≤ min [ a ]ᶠ [ b ]ᶠ) ⇔ ([ c ]ᶠ ≤ [ a ]ᶠ) ⊓ ([ c ]ᶠ ≤ [ b ]ᶠ) ]
    γ a@(aᶻ , aⁿ) b@(bᶻ , bⁿ) c@(cᶻ , cⁿ) = pathTo⇔ (sym κ) where
      aⁿᶻ = [1+ aⁿ ⁿ]ᶻ
      bⁿᶻ = [1+ bⁿ ⁿ]ᶻ
      cⁿᶻ = [1+ cⁿ ⁿ]ᶻ
      0≤aⁿᶻ : [ 0 ≤ᶻ aⁿᶻ ]
      0≤aⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p
      0≤bⁿᶻ : [ 0 ≤ᶻ bⁿᶻ ]
      0≤bⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p
      0≤cⁿᶻ : [ 0 ≤ᶻ cⁿᶻ ]
      0≤cⁿᶻ (k , p) = snotzⁿ $ sym (+ⁿ-suc k _) ∙ p
      -- -- note, that the following holds definitionally (TODO: put this at the definition of `min`)
      -- _ =    min [ aᶻ , aⁿ ]ᶠ [ bᶻ , bⁿ ]ᶠ                 ≡⟨ refl ⟩
      --     [ (minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) , aⁿ *₊₁ bⁿ) ]ᶠ  ∎
      -- -- and we also have definitionally
      -- _ : [1+ aⁿ *₊₁ bⁿ ⁿ]ᶻ ≡ aⁿᶻ *ᶻ bⁿᶻ
      -- _ = refl
      -- -- therefore, we have for the LHS:
      -- _ = ([ cᶻ , cⁿ ]ᶠ ≤ min [ aᶻ , aⁿ ]ᶠ [ bᶻ , bⁿ ]ᶠ)                      ≡⟨ refl ⟩
      --     ([ cᶻ , cⁿ ]ᶠ ≤ [ (minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) , aⁿ *₊₁ bⁿ) ]ᶠ)    ≡⟨ refl ⟩
      --     (¬([ (minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) , aⁿ *₊₁ bⁿ) ]ᶠ < [ cᶻ , cⁿ ]ᶠ)) ≡⟨ refl ⟩
      --     ¬((minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) *ᶻ cⁿᶻ) <ᶻ (cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)))    ≡⟨ refl ⟩
      --     ((cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)) ≤ᶻ (minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) *ᶻ cⁿᶻ))     ∎
      -- -- similar for the RHS:
      -- _ =  ([ cᶻ , cⁿ ]ᶠ ≤ [ aᶻ , aⁿ ]ᶠ) ⊓  ([ cᶻ , cⁿ ]ᶠ ≤ [ bᶻ , bⁿ ]ᶠ) ≡⟨ refl ⟩
      --     ¬([ aᶻ , aⁿ ]ᶠ < [ cᶻ , cⁿ ]ᶠ) ⊓ ¬([ bᶻ , bⁿ ]ᶠ < [ cᶻ , cⁿ ]ᶠ) ≡⟨ refl ⟩
      --     ¬((aᶻ *ᶻ cⁿᶻ)  <ᶻ (cᶻ *ᶻ aⁿᶻ)) ⊓ ¬((bᶻ *ᶻ cⁿᶻ)  <ᶻ (cᶻ *ᶻ bⁿᶻ)) ≡⟨ refl ⟩
      --      ((cᶻ *ᶻ aⁿᶻ)  ≤ᶻ (aᶻ *ᶻ cⁿᶻ)) ⊓  ((cᶻ *ᶻ bⁿᶻ)  ≤ᶻ (bᶻ *ᶻ cⁿᶻ)) ∎
      -- -- therfore, only properties on ℤ remain
      -- RHS = [ ((cᶻ *ᶻ aⁿᶻ)  ≤ᶻ (aᶻ *ᶻ cⁿᶻ)) ⊓  ((cᶻ *ᶻ bⁿᶻ)  ≤ᶻ (bᶻ *ᶻ cⁿᶻ)) ]
      -- LHS = [ ((cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)) ≤ᶻ (minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) *ᶻ cⁿᶻ)) ]
      -- strategy: multiply everything with aⁿᶻ, bⁿᶻ, cⁿᶻ
      κ = (
        ((cᶻ *ᶻ aⁿᶻ)         ≤ᶻ (aᶻ *ᶻ cⁿᶻ)        ) ⊓ ((cᶻ *ᶻ bⁿᶻ)         ≤ᶻ (bᶻ *ᶻ cⁿᶻ)        ) ≡⟨ ⊓≡⊓ (Definitions.·-creates-≤-≡ (cᶻ *ᶻ aⁿᶻ) (aᶻ *ᶻ cⁿᶻ) bⁿᶻ 0≤bⁿᶻ) (Definitions.·-creates-≤-≡ (cᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ cⁿᶻ) aⁿᶻ 0≤aⁿᶻ) ⟩
        ((cᶻ *ᶻ aⁿᶻ) *ᶻ bⁿᶻ  ≤ᶻ (aᶻ *ᶻ cⁿᶻ) *ᶻ bⁿᶻ ) ⊓ ((cᶻ *ᶻ bⁿᶻ) *ᶻ aⁿᶻ  ≤ᶻ (bᶻ *ᶻ cⁿᶻ) *ᶻ aⁿᶻ ) ≡⟨ ⊓≡⊓ (λ i → ·ᶻ-assoc cᶻ aⁿᶻ bⁿᶻ (~ i) ≤ᶻ ·ᶻ-assoc aᶻ cⁿᶻ bⁿᶻ (~ i)) (λ i → ·ᶻ-assoc cᶻ bⁿᶻ aⁿᶻ (~ i) ≤ᶻ ·ᶻ-assoc bᶻ cⁿᶻ aⁿᶻ (~ i)) ⟩
        ( cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ) ≤ᶻ  aᶻ *ᶻ (cⁿᶻ *ᶻ bⁿᶻ)) ⊓ ( cᶻ *ᶻ (bⁿᶻ *ᶻ aⁿᶻ) ≤ᶻ  bᶻ *ᶻ (cⁿᶻ *ᶻ aⁿᶻ)) ≡⟨ ⊓≡⊓ (λ i → cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ) ≤ᶻ  aᶻ *ᶻ (·ᶻ-comm cⁿᶻ bⁿᶻ i)) (λ i → cᶻ *ᶻ (·ᶻ-comm bⁿᶻ aⁿᶻ i) ≤ᶻ  bᶻ *ᶻ (·ᶻ-comm cⁿᶻ aⁿᶻ i)) ⟩
        ( cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ) ≤ᶻ  aᶻ *ᶻ (bⁿᶻ *ᶻ cⁿᶻ)) ⊓ ( cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ) ≤ᶻ  bᶻ *ᶻ (aⁿᶻ *ᶻ cⁿᶻ)) ≡⟨ sym $ ⇔toPath' $ is-minᶻ (aᶻ *ᶻ (bⁿᶻ *ᶻ cⁿᶻ)) (bᶻ *ᶻ (aⁿᶻ *ᶻ cⁿᶻ)) (cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)) ⟩
        ((cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)) ≤ᶻ minᶻ (aᶻ *ᶻ (bⁿᶻ *ᶻ cⁿᶻ)) (bᶻ *ᶻ (aⁿᶻ *ᶻ cⁿᶻ)))                    ≡⟨ (λ i → ((cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)) ≤ᶻ minᶻ (·ᶻ-assoc aᶻ bⁿᶻ cⁿᶻ i) (·ᶻ-assoc bᶻ aⁿᶻ cⁿᶻ i))) ⟩
        ((cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)) ≤ᶻ minᶻ ((aᶻ *ᶻ bⁿᶻ) *ᶻ cⁿᶻ) ((bᶻ *ᶻ aⁿᶻ) *ᶻ cⁿᶻ))                    ≡⟨ (λ i → (cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)) ≤ᶻ Definitions.·-min-distribʳ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) cⁿᶻ 0≤cⁿᶻ (~ i)) ⟩
        ((cᶻ *ᶻ (aⁿᶻ *ᶻ bⁿᶻ)) ≤ᶻ (minᶻ (aᶻ *ᶻ bⁿᶻ) (bᶻ *ᶻ aⁿᶻ) *ᶻ cⁿᶻ))                             ∎)

≤-Lattice : [ isLattice _≤_ min max ]
≤-Lattice .IsLattice.≤-PartialOrder = linearorder⇒partialorder _ (≤'-isLinearOrder <-StrictLinearOrder)
≤-Lattice .IsLattice.is-min         = is-min
≤-Lattice .IsLattice.is-max         = {!   !}

is-LinearlyOrderedCommSemiring : [ isLinearlyOrderedCommSemiring 0 1 _+_ _*_ _<_ min max ]
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.is-CommSemiring     = is-CommSemiring
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.<-StrictLinearOrder = <-StrictLinearOrder
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.≤-Lattice           = ≤-Lattice
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.+-<-ext             = {!   !}
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.·-preserves-<       = {!   !}

+-inverse : (x : ℚ) → (x + (- x) ≡ 0) × ((- x) + x ≡ 0)
+-inverse x .fst = +-inverseʳ x
+-inverse x .snd = +-inverseˡ x

is-LinearlyOrderedCommRing : [ isLinearlyOrderedCommRing 0 1 _+_ _*_ -_ _<_ min max ]
is-LinearlyOrderedCommRing. IsLinearlyOrderedCommRing.is-LinearlyOrderedCommSemiring = is-LinearlyOrderedCommSemiring
is-LinearlyOrderedCommRing. IsLinearlyOrderedCommRing.+-inverse                      = +-inverse

is-LinearlyOrderedField : [ isLinearlyOrderedField 0 1 _+_ _*_ -_ _<_ min max ]
is-LinearlyOrderedField .IsLinearlyOrderedField.is-LinearlyOrderedCommRing = is-LinearlyOrderedCommRing
is-LinearlyOrderedField .IsLinearlyOrderedField.·-inv''                    = ·-inv''

ℚbundle : LinearlyOrderedField {ℓ-zero} {ℓ-zero}
ℚbundle .LinearlyOrderedField.Carrier                  = ℚ
ℚbundle .LinearlyOrderedField.0f                       = 0
ℚbundle .LinearlyOrderedField.1f                       = 1
ℚbundle .LinearlyOrderedField._+_                      = _+_
ℚbundle .LinearlyOrderedField.-_                       = -_
ℚbundle .LinearlyOrderedField._·_                      = _*_
ℚbundle .LinearlyOrderedField.min                      = min
ℚbundle .LinearlyOrderedField.max                      = max
ℚbundle .LinearlyOrderedField._<_                      = _<_
ℚbundle .LinearlyOrderedField.is-LinearlyOrderedField  = is-LinearlyOrderedField

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
postulate
  id : {t : Set} → t → t
  _≡_ : {t : Set} → t → t → Set
  ⊤ : Set

record FunctorOp (f : Set → Set) : Set₁ where
record FunctorLaws (f : Set → Set) {{op : FunctorOp f}} : Set₁ where

-- demand functor laws to access <*>, but promise we won't use them in our definition
record ApplyOp (A : Set → Set) {{_ : FunctorOp A}} .{{_ : FunctorLaws A}} : Set₁ where
  field
    _<*>_ : ∀ {t₁ t₂} → A (t₁ → t₂) → A t₁ → A t₂

open ApplyOp {{...}}

record ApplyLaws₂ (A : Set → Set) {{_ : FunctorOp A}} .{{_ : FunctorLaws A}} {{i : ApplyOp A}} : Set₁ where
  -- but if we try to do anything in here...
  -- resolution fails, even though our instance `i` is already resolved and in scope!

  field
    blah : ∀ (f : A (⊤ → ⊤)) → (x : A ⊤) → (f <*> x) ≡ x


text:
module SystemF.Substitutions.Types where

open import Prelude
open import SystemF.Syntax.Type
open import Data.Fin.Substitution
open import Data.Star hiding (map)
open import Data.Vec

module TypeSubst where
  module TypeApp {T} (l : Lift T Type) where
    open Lift l hiding (var)

    infixl 8 _/_

    _/_ : ∀ {m n} → Type m → Sub T m n → Type n
    tc c     / σ = tc c
    tvar x   / σ = lift (lookup x σ)
    (a →' b) / σ = (a / σ) →' (b / σ)
    (a ⟶ b) / σ = (a / σ) ⟶ (b / σ)
    ∀' a     / σ = ∀' (a / σ ↑)

    open Application (record { _/_ = _/_ }) using (_/✶_)

    →'-/✶-↑✶ : ∀ k {m n a b} (ρs : Subs T m n) →
               (a →' b) /✶ ρs ↑✶ k ≡ (a /✶ ρs ↑✶ k) →' (b /✶ ρs ↑✶ k)
    →'-/✶-↑✶ k ε        = refl
    →'-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (→'-/✶-↑✶ k ρs) refl

    ⟶-/✶-↑✶ : ∀ k {m n a b} (ρs : Subs T m n) →
               (a ⟶ b) /✶ ρs ↑✶ k ≡ (a /✶ ρs ↑✶ k) ⟶ (b /✶ ρs ↑✶ k)
    ⟶-/✶-↑✶ k ε        = refl
    ⟶-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (⟶-/✶-↑✶ k ρs) refl

    ∀'-/✶-↑✶ : ∀ k {m n a} (ρs : Subs T m n) →
               (∀' a) /✶ ρs ↑✶ k ≡ ∀' (a /✶ ρs ↑✶ (1 + k))
    ∀'-/✶-↑✶ k ε        = refl
    ∀'-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (∀'-/✶-↑✶ k ρs) refl

    tc-/✶-↑✶ : ∀ k {c m n} (ρs : Subs T m n) →
               (tc c) /✶ ρs ↑✶ k ≡ tc c
    tc-/✶-↑✶ k ε        = refl
    tc-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (tc-/✶-↑✶ k ρs) refl

  typeSubst : TermSubst Type
  typeSubst = record { var = tvar; app = TypeApp._/_ }

  open TermSubst typeSubst public hiding (var)

  infix 8 _[/_]

  -- Shorthand for single-variable type substitutions
  _[/_] : ∀ {n} → Type (suc n) → Type n → Type n
  a [/ b ] = a / sub b

open TypeSubst public using ()
  renaming (_/_ to _tp/tp_; _[/_] to _tp[/tp_]; weaken to tp-weaken)