text:
{-# OPTIONS --cubical --safe --exact-split --without-K #-}

-- this depends mainly on agda/cubical, but also uses the standard library for `Function`
module scratch where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.HLevels
open import Cubical.Relation.Nullary
open import Cubical.HITs.HitInt renaming (abs to absℤ ; Sign to Sign'; sign to sign')
open import Cubical.HITs.Rational
open import Cubical.Data.Bool
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_; _*_ to _*ℕ_)
open import Cubical.Data.Empty
open import Cubical.Data.Unit
open import Cubical.Data.Prod
open import Agda.Primitive
open import Function

private
  variable
    ℓ ℓ' : Level

const₂ : {A B : Set ℓ} {C : Set ℓ'} → C → A → B → C
const₂ c _ _ = c

record FromNat (A : Set ℓ) : Set (lsuc ℓ) where
  field
    Constraint : ℕ → Set ℓ
    fromNat : (n : ℕ) ⦃ _ : Constraint n ⦄ → A
open FromNat ⦃ ... ⦄ public using (fromNat)

{-# BUILTIN FROMNAT fromNat #-}

record FromNeg (A : Set ℓ) : Set (lsuc ℓ) where
  field
    Constraint : ℕ → Set ℓ
    fromNeg : (n : ℕ) ⦃ _ : Constraint n ⦄ → A
open FromNeg ⦃ ... ⦄ public using (fromNeg)

{-# BUILTIN FROMNEG fromNeg #-}

instance
  NatFromNat : FromNat ℕ
  NatFromNat .FromNat.Constraint _ = Unit
  fromNat ⦃ NatFromNat ⦄ n = n

instance
  ℤFromNat : FromNat ℤ
  ℤFromNat .FromNat.Constraint _ = Unit
  fromNat ⦃ ℤFromNat ⦄ n = pos n

instance
  ℤFromNeg : FromNeg ℤ
  ℤFromNeg .FromNeg.Constraint _ = Unit
  fromNeg ⦃ ℤFromNeg ⦄ n = neg n

instance
  ℚFromNat : FromNat ℚ
  ℚFromNat .FromNat.Constraint _ = Unit
  fromNat ⦃ ℚFromNat ⦄ n = int (pos n)

instance
  ℚFromNeg : FromNeg ℚ
  ℚFromNeg .FromNeg.Constraint _ = Unit
  fromNeg ⦃ ℚFromNeg ⦄ n = int (neg n)

record Op< (A B : Set ℓ) (C : A → B → Set ℓ') : Set (ℓ-max ℓ ℓ') where
  infix 5 _<_
  field
    _<_ : (a : A) → (b : B) → C a b
open Op< ⦃ ... ⦄ public

record Op> (A B : Set ℓ) (C : A → B → Set ℓ') : Set (ℓ-max ℓ ℓ') where
  infix 5 _>_
  field
    _>_ : (a : A) → (b : B) → C a b
open Op> ⦃ ... ⦄ public

record Op≥ (A B : Set ℓ) (C : A → B → Set ℓ') : Set (ℓ-max ℓ ℓ') where
  infix 5 _≥_
  field
    _≥_ : (a : A) → (b : B) → C a b
open Op≥ ⦃ ... ⦄ public

record Op≤ (A B : Set ℓ) (C : A → B → Set ℓ') : Set (ℓ-max ℓ ℓ') where
  infix 5 _≤_
  field
    _≤_ : (a : A) → (b : B) → C a b
open Op≤ ⦃ ... ⦄ public

record Op== (A B : Set ℓ) (C : A → B → Set ℓ') : Set (ℓ-max ℓ ℓ') where
  infix 5 _==_
  field
    _==_ : (a : A) → (b : B) → C a b
open Op== ⦃ ... ⦄ public

record Op+ (A B : Set ℓ) (C : A → B → Set ℓ') : Set (ℓ-max ℓ ℓ') where
  infixl 7 _+_
  field
    _+_ : (a : A) → (b : B) → C a b
open Op+ ⦃ ... ⦄ public

record Op- (A B : Set ℓ) (C : A → B → Set ℓ') : Set (ℓ-max ℓ ℓ') where
  infixl 7 _-_
  field
    _-_ : (a : A) → (b : B) → C a b
open Op- ⦃ ... ⦄ public

record Op* (A B : Set ℓ) (C : A → B → Set ℓ') : Set (ℓ-max ℓ ℓ') where
  infixl 8 _*_
  field
    _*_ : (a : A) → (b : B) → C a b
open Op* ⦃ ... ⦄ public

record OpUnary- (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ-max ℓ ℓ') where
  field
    -_ : (a : A) → B a
open OpUnary- ⦃ ... ⦄ public

instance
  ℕ< : Op< ℕ ℕ (const₂ Bool)
  _<_ ⦃ ℕ< ⦄ n m = n less-than m where
    _less-than_ : ℕ → ℕ → Bool
    zero less-than zero = false
    zero less-than suc _ = true
    suc _ less-than zero = false
    suc a less-than suc b = a less-than b

instance
 ℕ> : Op> ℕ ℕ (const₂ Bool)
 _>_ ⦃ ℕ> ⦄ n m = n greater-than m where
   _greater-than_ : ℕ → ℕ → Bool
   zero greater-than zero = false
   zero greater-than suc b = false
   suc a greater-than zero = true
   suc a greater-than suc b = a greater-than b

instance
  ℕ≥ : Op≥ ℕ ℕ (const₂ Bool)
  _≥_ ⦃ ℕ≥ ⦄ a b = not (a < b)

instance
  ℕ≤ : Op≤ ℕ ℕ (const₂ Bool)
  _≤_ ⦃ ℕ≤ ⦄ a b = not (a > b)

instance
  ℕ== : Op== ℕ ℕ (const₂ Bool)
  _==_ ⦃ ℕ== ⦄ a b = a eq b where
    _eq_ : ℕ → ℕ → Bool
    zero eq zero = true
    zero eq suc _ = false
    suc _ eq zero = false
    suc a eq suc b = a eq b

a<b≡¬a≥b : {a b : ℕ} → a < b ≡ not (a ≥ b)
a<b≡¬a≥b {a} {b} = sym (notnot (a < b))

a>b≡¬a≤b : {a b : ℕ} → a > b ≡ not (a ≤ b)
a>b≡¬a≤b {a} {b} = sym (notnot (a > b))

instance
  ℕ+ : Op+ ℕ ℕ (const₂ ℕ)
  _+_ ⦃ ℕ+ ⦄ a b = a +ℕ b

instance
  ℕ- : Op- ℕ ℕ (λ a b → ⦃ _ : a ≥ b ≡ true ⦄ → ℕ)
  _-_ ⦃ ℕ- ⦄ a b = a minus b where
    _minus_ : (a : ℕ) → (b : ℕ) → ⦃ _ : a ≥ b ≡ true ⦄ → ℕ
    n minus zero = n
    _minus_ zero (suc b) ⦃ a≥b ⦄ = ⊥-elim (false≢true a≥b)
    (suc a) minus (suc b) = a minus b

instance
  ℕ* : Op* ℕ ℕ (const₂ ℕ)
  _*_ ⦃ ℕ* ⦄ a b = a *ℕ b

--ℤ---------------

instance
  ℤ< : Op< ℤ ℤ (const₂ Bool)
  _<_ ⦃ ℤ< ⦄ n m = n less-than m where
    _less-than_ : ℤ → ℤ → Bool
    pos n less-than pos m = n < m
    neg n less-than neg m = n > m
    pos _ less-than neg _ = false
    neg zero less-than pos zero = false
    neg zero less-than pos (suc _) = true
    neg (suc _) less-than pos _ = true
    pos zero less-than posneg _ = false
    pos (suc _) less-than posneg _ = false
    neg zero less-than posneg _ = false
    neg (suc _) less-than posneg _ = true
    posneg _ less-than pos zero = false
    posneg _ less-than pos (suc _) = true
    posneg _ less-than neg zero = false
    posneg _ less-than neg (suc _) = false
    posneg _ less-than posneg _ = false

instance
  ℤ> : Op> ℤ ℤ (const₂ Bool)
  _>_ ⦃ ℤ> ⦄ n m = m < n

instance
  ℤ≥ : Op≥ ℤ ℤ (const₂ Bool)
  _≥_ ⦃ ℤ≥ ⦄ a b = not (a < b)

instance
  ℤ≤ : Op≤ ℤ ℤ (const₂ Bool)
  _≤_ ⦃ ℤ≤ ⦄ a b = not (a > b)

instance
  ℤ== : Op== ℤ ℤ (const₂ Bool)
  _==_ ⦃ ℤ== ⦄ a b = a eq b where
    _eq_ : ℤ → ℤ → Bool
    pos n eq pos m = n == m
    neg n eq neg m = n == m
    pos zero eq neg zero = true
    pos zero eq neg (suc _) = false
    pos (suc _) eq neg _ = false
    neg zero eq pos zero = true
    neg zero eq pos (suc _) = false
    neg (suc _) eq pos _ = false
    pos zero eq posneg _ = true
    pos (suc _) eq posneg _ = false
    neg zero eq posneg _ = true
    neg (suc _) eq posneg _ = false
    posneg _ eq pos zero = true
    posneg _ eq pos (suc _) = false
    posneg _ eq neg zero = true
    posneg _ eq neg (suc _) = false
    posneg _ eq posneg _ = true

instance
  ℤ+ : Op+ ℤ ℤ (const₂ ℤ)
  _+_ ⦃ ℤ+ ⦄ a b = a +ℤ b

instance
  ℤ- : Op- ℤ ℤ (const₂ ℤ)
  _-_ ⦃ ℤ- ⦄ a (pos n) = a + (neg n)
  _-_ ⦃ ℤ- ⦄ a (neg n) = a + (pos n)
  _-_ ⦃ ℤ- ⦄ a (posneg _) = a

instance
  ℤ* : Op* ℤ ℤ (const₂ ℤ)
  _*_ ⦃ ℤ* ⦄ a b = a *ℤ b

instance
  ℤunary- : OpUnary- ℤ (const ℤ)
  -_ ⦃ ℤunary- ⦄ (pos n) = neg n
  -_ ⦃ ℤunary- ⦄ (neg n) = pos n
  -_ ⦃ ℤunary- ⦄ (posneg i) = (sym posneg) i

-- use of this lemma could be made automatic by changing `path` in ℚ to take instance arguments instead of implicit arguments.
-- `nonzero-prod` would then be an instance of `¬ (q * r ≡ pos 0)`
-- however currently, since `¬ (q * r ≡ pos 0)` is a function type, it is not allowed as an instance argument type
nonzero-prod : (q r : ℤ) → ¬ (q ≡ 0) → ¬ (r ≡ 0) → ¬ (q * r ≡ 0)
nonzero-prod (pos (suc n)) (pos (suc m)) _ _ q*r≡0 = snotz (cong absℤ q*r≡0)
nonzero-prod (pos (suc n)) (neg (suc m)) _ _ q*r≡0 = snotz (cong absℤ q*r≡0)
nonzero-prod (neg (suc n)) (pos (suc m)) _ _ q*r≡0 = snotz (cong absℤ q*r≡0)
nonzero-prod (neg (suc n)) (neg (suc m)) _ _ q*r≡0 = snotz (cong absℤ q*r≡0)
nonzero-prod (pos zero) _ q≢0 _ _ = q≢0 refl
nonzero-prod (neg zero) _ q≢0 _ _ = q≢0 (sym posneg)
nonzero-prod (pos (suc _)) (pos zero) _ r≢0 _ = r≢0 refl
nonzero-prod (pos (suc _)) (neg zero) _ r≢0 _ = r≢0 (sym posneg)
nonzero-prod (neg (suc _)) (pos zero) _ r≢0 _ = r≢0 refl
nonzero-prod (neg (suc _)) (neg zero) _ r≢0 _ = r≢0 (sym posneg)
nonzero-prod q@(pos (suc _)) (posneg i) _ r≢0 _ = r≢0 λ j → posneg (i ∧ ~ j)
nonzero-prod q@(neg (suc _)) (posneg i) _ r≢0 _ = r≢0 λ j → posneg (i ∧ ~ j)
nonzero-prod (posneg i) _ q≢0 _ _ = q≢0 λ j → posneg (i ∧ ~ j)

0≡m*ℤ0 : (m : ℤ) → 0 ≡ m * 0
0≡m*ℤ0 (pos n) = cong pos $ 0≡m*0 n
0≡m*ℤ0 (neg zero) = refl
0≡m*ℤ0 (neg (suc n)) = posneg ∙ (cong ℤ.neg $ 0≡m*0 n)
0≡m*ℤ0 (posneg i) = refl

0≡0*ℤm : (m : ℤ) → 0 ≡ 0 * m
0≡0*ℤm (pos n) = refl
0≡0*ℤm (neg zero) = refl
0≡0*ℤm (neg (suc n)) = posneg
0≡0*ℤm (posneg i) = refl

m≡0+ℤm : (m : ℤ) → m ≡ 0 + m
m≡0+ℤm (pos zero) = refl
m≡0+ℤm (neg zero) = sym posneg
m≡0+ℤm (posneg i) = λ j → posneg (i ∧ ~ j)
m≡0+ℤm (pos (suc n)) = cong sucℤ $ m≡0+ℤm (pos n)
m≡0+ℤm (neg (suc n)) = cong predℤ $ m≡0+ℤm (neg n)

m≡m*1 : (m : ℕ) → m ≡ m * 1
m≡m*1 zero = refl
m≡m*1 (suc m) = cong suc $ m≡m*1 m

m≡m*ℤ1 : (m : ℤ) → m ≡ m * 1
m≡m*ℤ1 (pos zero) = refl
m≡m*ℤ1 (pos (suc n)) = cong (ℤ.pos ∘ suc) $ m≡m*1 n
m≡m*ℤ1 (neg zero) = sym posneg
m≡m*ℤ1 (neg (suc n)) = cong (ℤ.neg ∘ suc) $ m≡m*1 n
m≡m*ℤ1 (posneg i) = λ j → posneg (i ∧ ~ j)

ℤ+-pred : (m n : ℤ) → m + predℤ n ≡ predℤ (m + n)
ℤ+-pred m (pos zero) = refl
ℤ+-pred m (pos (suc n)) = sym $ predSucℤ (m + pos n)
ℤ+-pred m (neg n) = refl
ℤ+-pred m (posneg i) = refl

ℤ+-suc : (m n : ℤ) → m + sucℤ n ≡ sucℤ (m + n)
ℤ+-suc m (pos zero) = refl
ℤ+-suc m (pos (suc n)) = refl
ℤ+-suc m (neg zero) = refl
ℤ+-suc m (neg (suc n)) = sym $ sucPredℤ (m + neg n)
ℤ+-suc m (posneg i) = refl

ℤ+-comm-0 : (z : ℤ) → (i : I) → posneg i + z ≡ z
ℤ+-comm-0 z i = cong (_+ z) (λ j → posneg (i ∧ ~ j)) ∙ sym (m≡0+ℤm z)

ℤ+-comm-0-0 : (i j : I) → posneg i ≡ posneg j
ℤ+-comm-0-0 i j = λ k → posneg ((~ k ∧ i) ∨ (k ∧ j))

ℤ+-comm : (m n : ℤ) → m + n ≡ n + m
ℤ+-comm (pos zero) (pos zero) = ℤ+-comm-0-0 i0 i0
ℤ+-comm (neg zero) (neg zero) = ℤ+-comm-0-0 i1 i1
ℤ+-comm (pos zero) (neg zero) = ℤ+-comm-0-0 i0 i1
ℤ+-comm (neg zero) (pos zero) = ℤ+-comm-0-0 i1 i0
ℤ+-comm (posneg i) (pos zero) = ℤ+-comm-0-0 i i0
ℤ+-comm (posneg i) (neg zero) = ℤ+-comm-0-0 i i1
ℤ+-comm (pos zero) (posneg j) = ℤ+-comm-0-0 i0 j
ℤ+-comm (neg zero) (posneg j) = ℤ+-comm-0-0 i1 j
ℤ+-comm (posneg i) (posneg j) = ℤ+-comm-0-0 i j
ℤ+-comm (pos zero) (pos (suc n)) = cong sucℤ $ ℤ+-comm-0 (pos n) i0
ℤ+-comm (neg zero) (pos (suc n)) = cong sucℤ $ ℤ+-comm-0 (pos n) i1
ℤ+-comm (posneg i) (pos (suc n)) = cong sucℤ $ ℤ+-comm-0 (pos n) i
ℤ+-comm (pos zero) (neg (suc n)) = cong predℤ $ ℤ+-comm-0 (neg n) i0
ℤ+-comm (neg zero) (neg (suc n)) = cong predℤ $ ℤ+-comm-0 (neg n) i1
ℤ+-comm (posneg i) (neg (suc n)) = cong predℤ $ ℤ+-comm-0 (neg n) i
ℤ+-comm (pos (suc m)) (pos zero) = cong sucℤ $ sym $ ℤ+-comm-0 (pos m) i0
ℤ+-comm (pos (suc m)) (neg zero) = cong sucℤ $ sym $ ℤ+-comm-0 (pos m) i1
ℤ+-comm (pos (suc m)) (posneg i) = cong sucℤ $ sym $ ℤ+-comm-0 (pos m) i
ℤ+-comm (neg (suc m)) (pos zero) = cong predℤ $ sym $ ℤ+-comm-0 (neg m) i0
ℤ+-comm (neg (suc m)) (neg zero) = cong predℤ $ sym $ ℤ+-comm-0 (neg m) i1
ℤ+-comm (neg (suc m)) (posneg i) = cong predℤ $ sym $ ℤ+-comm-0 (neg m) i
ℤ+-comm (pos (suc m)) (pos (suc n)) = cong sucℤ
  ( pos (suc m) + pos n  ≡⟨ ℤ+-comm (pos (suc m)) (pos n) ⟩
    pos n + pos (suc m)  ≡⟨ refl ⟩
    sucℤ (pos n + pos m) ≡⟨ cong sucℤ $ ℤ+-comm (pos n) (pos m) ⟩
    sucℤ (pos m + pos n) ≡⟨ refl ⟩
    pos m + pos (suc n)  ≡⟨ ℤ+-comm (pos m) (pos (suc n)) ⟩
    pos (suc n) + pos m  ∎
  )
ℤ+-comm (neg (suc m)) (pos (suc n)) =
  ( sucℤ (neg (suc m) + pos n)   ≡⟨ cong sucℤ $ ℤ+-comm (neg (suc m)) (pos n) ⟩
    sucℤ (pos n + neg (suc m))   ≡⟨ refl ⟩
    sucℤ (predℤ (pos n + neg m)) ≡⟨ sucPredℤ _ ⟩
    pos n + neg m                ≡⟨ ℤ+-comm (pos n) (neg m) ⟩
    neg m + pos n                ≡⟨ sym $ predSucℤ _ ⟩
    predℤ (sucℤ (neg m + pos n)) ≡⟨ refl ⟩
    predℤ (neg m + pos (suc n))  ≡⟨ cong predℤ $ ℤ+-comm (neg m) (pos (suc n)) ⟩
    predℤ (pos (suc n) + neg m)  ∎
  )
ℤ+-comm (pos (suc m)) (neg (suc n)) =
  ( predℤ (pos (suc m) + neg n)  ≡⟨ cong predℤ $ ℤ+-comm (pos (suc m)) (neg n) ⟩
    predℤ (neg n + pos (suc m))  ≡⟨ refl ⟩
    predℤ (sucℤ (neg n + pos m)) ≡⟨ predSucℤ _ ⟩
    neg n + pos m                ≡⟨ ℤ+-comm (neg n) (pos m) ⟩
    pos m + neg n                ≡⟨ sym $ sucPredℤ _ ⟩
    sucℤ (predℤ (pos m + neg n)) ≡⟨ refl ⟩
    sucℤ (pos m + neg (suc n))   ≡⟨ cong sucℤ $ ℤ+-comm (pos m) (neg (suc n)) ⟩
    sucℤ (neg (suc n) + pos m)   ∎
  )
ℤ+-comm (neg (suc m)) (neg (suc n)) = cong predℤ
  ( neg (suc m) + neg n   ≡⟨ ℤ+-comm (neg (suc m)) (neg n) ⟩
    neg n + neg (suc m)   ≡⟨ refl ⟩
    predℤ (neg n + neg m) ≡⟨ cong predℤ $ ℤ+-comm (neg n) (neg m) ⟩
    predℤ (neg m + neg n) ≡⟨ refl ⟩
    neg m + neg (suc n)   ≡⟨ ℤ+-comm (neg m) (neg (suc n)) ⟩
    neg (suc n) + neg m   ∎
  )

ℤ+-assoc : (m n o : ℤ) → m + (n + o) ≡ m + n + o
ℤ+-assoc m n (pos zero) = refl
ℤ+-assoc m n (pos (suc o)) =
  ( m + sucℤ (n + pos o)   ≡⟨ ℤ+-suc m (n + pos o) ⟩
    sucℤ (m + (n + pos o)) ≡⟨ cong sucℤ $ ℤ+-assoc m n (pos o) ⟩
    sucℤ (m + n + pos o)   ∎
  )
ℤ+-assoc m n (neg zero) = refl
ℤ+-assoc m n (neg (suc o)) =
  ( m + predℤ (n + neg o)   ≡⟨ ℤ+-pred m (n + neg o) ⟩
    predℤ (m + (n + neg o)) ≡⟨ cong predℤ $ ℤ+-assoc m n (neg o) ⟩
    predℤ (m + n + neg o)   ∎
  )
ℤ+-assoc m n (posneg i) = refl

lemma : (m n : ℕ) → n + m * suc n ≡ m + n * suc m
lemma m n =
  ( n + m * suc n   ≡⟨ cong (n +_) $ *-suc m n ⟩
    n + (m + m * n) ≡⟨ +-assoc n m (m * n) ⟩
    n + m + m * n   ≡⟨ cong (_+ m * n) $ +-comm n m ⟩
    m + n + m * n   ≡⟨ cong (m + n +_) $ *-comm m n ⟩
    m + n + n * m   ≡⟨ sym $ +-assoc m n (n * m) ⟩
    m + (n + n * m) ≡⟨ cong (m +_) $ sym $ *-suc n m ⟩
    m + n * suc m   ∎
  )

ℤ*-comm : (m n : ℤ) → m * n ≡ n * m
ℤ*-comm (pos zero) (pos zero) = refl
ℤ*-comm (neg zero) (pos zero) = refl
ℤ*-comm (posneg i) (pos zero) = refl
ℤ*-comm (pos zero) (neg zero) = refl
ℤ*-comm (neg zero) (neg zero) = refl
ℤ*-comm (posneg i) (neg zero) = refl
ℤ*-comm (pos zero) (posneg i) = refl
ℤ*-comm (neg zero) (posneg i) = refl
ℤ*-comm (posneg i) (posneg j) = refl
ℤ*-comm (pos zero) (pos (suc n)) = cong pos $ 0≡m*0 n
ℤ*-comm (neg zero) (pos (suc n)) = cong pos $ 0≡m*0 n
ℤ*-comm (posneg i) (pos (suc n)) = cong pos $ 0≡m*0 n
ℤ*-comm (pos zero) (neg (suc n)) = cong neg $ 0≡m*0 n
ℤ*-comm (neg zero) (neg (suc n)) = cong neg $ 0≡m*0 n
ℤ*-comm (posneg i) (neg (suc n)) = cong neg $ 0≡m*0 n
ℤ*-comm (pos (suc m)) (pos zero) = cong pos $ sym $ 0≡m*0 m
ℤ*-comm (neg (suc m)) (pos zero) = cong neg $ sym $ 0≡m*0 m
ℤ*-comm (pos (suc m)) (neg zero) = cong pos $ sym $ 0≡m*0 m
ℤ*-comm (neg (suc m)) (neg zero) = cong neg $ sym $ 0≡m*0 m
ℤ*-comm (pos (suc m)) (posneg i) = cong pos $ sym $ 0≡m*0 m
ℤ*-comm (neg (suc m)) (posneg i) = cong neg $ sym $ 0≡m*0 m
ℤ*-comm (pos (suc m)) (neg (suc n)) = cong (ℤ.neg ∘ suc) $ lemma m n
ℤ*-comm (neg (suc m)) (neg (suc n)) = cong (ℤ.pos ∘ suc) $ lemma m n
ℤ*-comm (pos (suc m)) (pos (suc n)) = cong (ℤ.pos ∘ suc) $ lemma m n
ℤ*-comm (neg (suc m)) (pos (suc n)) = cong (ℤ.neg ∘ suc) $ lemma m n

neg-distrib-+ : (m n : ℕ) → neg (m + n) ≡ neg m + neg n
neg-distrib-+ m zero = cong neg $ +-zero m
neg-distrib-+ m (suc n) =
  ( neg (m + suc n)       ≡⟨ cong neg $ +-suc m n ⟩
    predℤ (neg (m + n))   ≡⟨ cong predℤ $ neg-distrib-+ m n ⟩
    predℤ (neg m + neg n) ∎
  )

pos-distrib-+ : (m n : ℕ) → pos (m + n) ≡ pos m + pos n
pos-distrib-+ m zero = cong pos $ +-zero m
pos-distrib-+ m (suc n) =
  ( pos (m + suc n)      ≡⟨ cong pos $ +-suc m n ⟩
    sucℤ (pos (m + n))   ≡⟨ cong sucℤ $ pos-distrib-+ m n ⟩
    sucℤ (pos m + pos n) ∎
  )

lemma2 : (m n : ℕ) → suc (n + m * suc (suc n)) ≡ suc m + (n + m * suc n)
lemma2 m n =
  ( suc (n + m * suc (suc n)) ≡⟨ cong (suc ∘ (n +_)) $ *-suc m (suc n) ⟩
    suc (n + (m + m * suc n)) ≡⟨ cong (suc ∘ (n +_)) $ +-comm m (m * suc n) ⟩
    suc (n + (m * suc n + m)) ≡⟨ cong (suc) $ +-assoc n (m * suc n) m ⟩
    suc (n + m * suc n + m)   ≡⟨ sym $ +-suc (n + m * suc n) m ⟩
    n + m * suc n + suc m     ≡⟨ +-comm (n + m * suc n) (suc m) ⟩
    suc m + (n + m * suc n)   ∎
  )

lemma3 : (m : ℤ) → (i : I) → m * 1 ≡ (m + m * posneg i)
lemma3 m i =
  ( m * 1            ≡⟨ sym $ m≡m*ℤ1 m ⟩
    m                ≡⟨ refl ⟩
    m + 0            ≡⟨ cong (m +_) $ 0≡m*ℤ0 m ⟩
    m + m * 0        ≡⟨ cong (λ x → m + m * x) (λ j → posneg (i ∧ j)) ⟩
    m + m * posneg i ∎
  )

ℤ-m+-m≡0 : (m : ℕ) → pos m + neg m ≡ 0
ℤ-m+-m≡0 zero = refl
ℤ-m+-m≡0 (suc m) =
  ( predℤ (pos (suc m) + neg m)  ≡⟨ cong predℤ $ ℤ+-comm (pos (suc m)) (neg m) ⟩
    predℤ (neg m + pos (suc m))  ≡⟨ refl ⟩
    predℤ (sucℤ (neg m + pos m)) ≡⟨ predSucℤ _ ⟩
    neg m + pos m                ≡⟨ ℤ+-comm (neg m) (pos m) ⟩
    pos m + neg m                ≡⟨ ℤ-m+-m≡0 m ⟩
    0                            ∎
  )

ℤ--m+m≡0 : (m : ℕ) → neg m + pos m ≡ 0
ℤ--m+m≡0 m = ℤ+-comm (neg m) (pos m) ∙ ℤ-m+-m≡0 m

ℤ*-suc : (m n : ℤ) → m * sucℤ n ≡ m + m * n
ℤ*-suc m (pos zero) = lemma3 m i0
ℤ*-suc m (neg zero) = lemma3 m i1
ℤ*-suc m (posneg i) = lemma3 m i
ℤ*-suc (pos zero) (pos (suc n)) = refl
ℤ*-suc (neg zero) (pos (suc n)) = posneg
ℤ*-suc (posneg i) (pos (suc n)) = λ j → posneg (i ∧ j)
ℤ*-suc (pos zero) (neg (suc zero)) = refl
ℤ*-suc (pos zero) (neg (suc (suc n))) = sym posneg
ℤ*-suc (neg zero) (neg (suc zero)) = posneg
ℤ*-suc (neg zero) (neg (suc (suc n))) = refl
ℤ*-suc (posneg i) (neg (suc zero)) = λ j → posneg (i ∧ j)
ℤ*-suc (posneg i) (neg (suc (suc n))) =  λ j → posneg (i ∨ ~ j)
ℤ*-suc (pos (suc m)) (neg (suc zero)) =
  ( pos (suc m) * -0 ≡⟨ cong (pos (suc m) *_) $ sym $ posneg ⟩
    pos (suc m) * 0 ≡⟨ sym $ 0≡m*ℤ0 (pos (suc m)) ⟩
    0 ≡⟨ sym $ ℤ--m+m≡0 m ⟩
    neg m + pos m ≡⟨ sym $ predSucℤ _ ⟩
    predℤ (sucℤ (neg m + pos m)) ≡⟨ refl ⟩
    predℤ (neg m + pos (suc m)) ≡⟨ cong predℤ $ ℤ+-comm (neg m) (pos (suc m)) ⟩
    predℤ (pos (suc m) + neg m) ≡⟨ cong (predℤ ∘ (pos (suc m) +_) ∘ ℤ.neg) $ m≡m*1 m ⟩
    predℤ (pos (suc m) + neg (m * 1)) ∎
  )
ℤ*-suc (pos (suc m)) (neg (suc (suc n))) = cong predℤ $ sym
  ( predℤ (pos (suc m) + neg (n + m * suc (suc n)))  ≡⟨ cong predℤ $ ℤ+-comm (pos (suc m)) (neg (n + m * suc (suc n))) ⟩
    predℤ (neg (n + m * suc (suc n)) + pos (suc m))  ≡⟨ refl ⟩
    predℤ (sucℤ (neg (n + m * suc (suc n)) + pos m)) ≡⟨ predSucℤ (neg (n + m * suc (suc n)) + pos m) ⟩
    neg (n + m * suc (suc n)) + pos m                ≡⟨ cong ((_+ pos m) ∘ ℤ.neg ∘ (n +_)) $ *-suc m (suc n) ⟩
    neg (n + (m + m * suc n)) + pos m                ≡⟨ cong ((_+ pos m) ∘ ℤ.neg ∘ (n +_)) $ +-comm m (m * suc n) ⟩
    neg (n + (m * suc n + m)) + pos m                ≡⟨ cong ((_+ pos m) ∘ ℤ.neg) $ +-assoc n (m * suc n) m ⟩
    neg (n + m * suc n + m) + pos m                  ≡⟨ cong (_+ pos m) $ neg-distrib-+ (n + m * suc n) m ⟩
    neg (n + m * suc n) + neg m + pos m              ≡⟨ sym $ ℤ+-assoc (neg (n + m * suc n)) (neg m) (pos m) ⟩
    neg (n + m * suc n) + (neg m + pos m)            ≡⟨ cong (neg (n + m * suc n) +_) $ ℤ--m+m≡0 m ⟩
    neg (n + m * suc n) + 0                          ≡⟨ refl ⟩
    neg (n + m * suc n)                              ∎
  )
ℤ*-suc (neg (suc m)) (neg (suc zero)) =
  ( neg (suc m) * -0 ≡⟨ cong (neg (suc m) *_) $ sym $ posneg ⟩
    neg (suc m) * 0 ≡⟨ sym $ 0≡m*ℤ0 (neg (suc m)) ⟩
    0 ≡⟨ sym $ ℤ-m+-m≡0 m ⟩
    pos m + neg m ≡⟨ sym $ sucPredℤ (pos m + neg m) ⟩
    sucℤ (predℤ (pos m + neg m)) ≡⟨ refl ⟩
    sucℤ (pos m + neg (suc m)) ≡⟨ cong sucℤ $ ℤ+-comm (pos m) (neg (suc m)) ⟩
    sucℤ (neg (suc m) + pos m) ≡⟨ cong (sucℤ ∘ (neg (suc m) +_) ∘ ℤ.pos) $ m≡m*1 m ⟩
    sucℤ (neg (suc m) + pos (m * 1)) ∎
  )
ℤ*-suc (neg (suc m)) (neg (suc (suc n))) = cong sucℤ $ sym
  ( sucℤ (predℤ (neg m) + pos (n + m * suc (suc n))) ≡⟨ cong sucℤ $ ℤ+-comm (predℤ (neg m)) (pos (n + m * suc (suc n))) ⟩
    sucℤ (pos (n + m * suc (suc n)) + predℤ (neg m)) ≡⟨ cong sucℤ $ ℤ+-pred (pos (n + m * suc (suc n))) (neg m) ⟩
    sucℤ (predℤ (pos (n + m * suc (suc n)) + neg m)) ≡⟨ sucPredℤ _ ⟩
    pos (n + m * suc (suc n)) + neg m ≡⟨ cong ((_+ neg m) ∘ ℤ.pos ∘ (n +_)) $ *-suc m (suc n) ⟩
    pos (n + (m + m * suc n)) + neg m ≡⟨ cong ((_+ neg m) ∘ ℤ.pos) $ +-assoc n m (m * suc n) ⟩
    pos (n + m + m * suc n) + neg m ≡⟨ cong ((_+ neg m) ∘ ℤ.pos ∘ (_+ m * suc n)) $ +-comm n m ⟩
    pos (m + n + m * suc n) + neg m ≡⟨ cong ((_+ neg m) ∘ ℤ.pos) $ sym $ +-assoc m n (m * suc n) ⟩
    pos (m + (n + m * suc n)) + neg m ≡⟨ cong (_+ neg m) $ pos-distrib-+ m (n + m * suc n) ⟩
    pos m + pos (n + m * suc n) + neg m ≡⟨ cong (_+ neg m) $ ℤ+-comm (pos m) (pos (n + m * suc n))  ⟩
    pos (n + m * suc n) + pos m + neg m ≡⟨ sym $ ℤ+-assoc (pos (n + m * suc n)) (pos m) (neg m) ⟩
    pos (n + m * suc n) + (pos m + neg m) ≡⟨ cong (pos (n + m * suc n) +_) $ ℤ-m+-m≡0 m ⟩
    pos (n + m * suc n) + 0 ≡⟨ refl ⟩
    pos (n + m * suc n) ∎
  )
ℤ*-suc (pos (suc m)) (pos (suc n)) = cong sucℤ
  ( pos (suc (n + m * suc (suc n)))   ≡⟨ cong ℤ.pos $ lemma2 m n ⟩
    pos (suc m + (n + m * suc n))     ≡⟨ pos-distrib-+ (suc m) (n + m * suc n) ⟩
    pos (suc m) + pos (n + m * suc n) ∎
  )
ℤ*-suc (neg (suc m)) (pos (suc n)) = cong predℤ
  ( neg (suc (n + m * suc (suc n)))   ≡⟨ cong ℤ.neg $ lemma2 m n ⟩
    neg (suc m + (n + m * suc n))     ≡⟨ neg-distrib-+ (suc m) (n + m * suc n) ⟩
    neg (suc m) + neg (n + m * suc n) ∎
  )

lemma4 : (m : ℕ) → neg (suc (m * 1)) ≡ predℤ (pos (m * 0) + neg m)
lemma4 m = cong predℤ
  ( neg (m * 1)         ≡⟨ cong ℤ.neg $ sym $ m≡m*1 m ⟩
    neg m               ≡⟨ m≡0+ℤm _ ⟩
    pos 0 + neg m       ≡⟨ cong ((_+ neg m) ∘ ℤ.pos) $ 0≡m*0 m ⟩
    pos (m * 0) + neg m ∎
  )

lemma5 : (m : ℕ) → pos (suc (m * 1)) ≡ sucℤ (neg (m * 0) + pos m)
lemma5 m = cong sucℤ
  ( pos (m * 1)         ≡⟨ cong ℤ.pos $ sym $ m≡m*1 m ⟩
    pos m               ≡⟨ m≡0+ℤm _ ⟩
    0 + pos m           ≡⟨ cong (_+ pos m) posneg ⟩
    neg 0 + pos m       ≡⟨ cong ((_+ pos m) ∘ ℤ.neg) $ 0≡m*0 m ⟩
    neg (m * 0) + pos m ∎
  )

lemma6 : (m n : ℕ) → n + m * suc (suc n) ≡ m + (n + m * suc n)
lemma6 m n =
  ( n + m * suc (suc n) ≡⟨ cong (n +_) $ *-suc m (suc n) ⟩
    n + (m + m * suc n) ≡⟨ +-assoc n m (m * suc n) ⟩
    n + m + m * suc n   ≡⟨ cong (_+ m * suc n) $ +-comm n m ⟩
    m + n + m * suc n   ≡⟨ sym $ +-assoc m n (m * suc n) ⟩
    m + (n + m * suc n) ∎
  )

lemma7 : (m n : ℕ) → m + (n + m * n) ≡ n + m * suc n
lemma7 m n =
  ( m + (n + m * n) ≡⟨ +-assoc m n (m * n) ⟩
    m + n + m * n   ≡⟨ cong (_+ m * n) $ +-comm m n ⟩
    n + m + m * n   ≡⟨ sym $ +-assoc n m (m * n) ⟩
    n + (m + m * n) ≡⟨ cong (n +_) $ sym $ *-suc m n ⟩
    n + m * suc n   ∎
  )

ℤ*-pred : (m n : ℤ) → m * predℤ n ≡ m * n - m
ℤ*-pred (pos zero) (pos zero) = sym posneg
ℤ*-pred (neg zero) (pos zero) = sym posneg
ℤ*-pred (posneg i) (pos zero) = sym posneg
ℤ*-pred (pos zero) (neg zero) = sym posneg
ℤ*-pred (neg zero) (neg zero) = sym posneg
ℤ*-pred (posneg i) (neg zero) = sym posneg
ℤ*-pred (pos zero) (posneg i) = sym posneg
ℤ*-pred (neg zero) (posneg i) = sym posneg
ℤ*-pred (posneg i) (posneg j) = sym posneg
ℤ*-pred (pos (suc m)) (pos zero) = lemma4 m
ℤ*-pred (pos (suc m)) (neg zero) = lemma4 m
ℤ*-pred (pos (suc m)) (posneg i) = lemma4 m
ℤ*-pred (neg (suc m)) (pos zero) = lemma5 m
ℤ*-pred (neg (suc m)) (neg zero) = lemma5 m
ℤ*-pred (neg (suc m)) (posneg i) = lemma5 m
ℤ*-pred (pos zero) (pos (suc n)) = refl
ℤ*-pred (neg zero) (pos (suc n)) = refl
ℤ*-pred (posneg i) (pos (suc n)) = refl
ℤ*-pred (pos zero) (neg (suc n)) = refl
ℤ*-pred (neg zero) (neg (suc n)) = refl
ℤ*-pred (posneg i) (neg (suc n)) = refl
ℤ*-pred (pos (suc m)) (pos (suc n)) =
  ( pos (n + m * n)                            ≡⟨ m≡0+ℤm _ ⟩
    0 + pos (n + m * n)                        ≡⟨ cong (_+ pos (n + m * n)) $ sym $ ℤ--m+m≡0 m ⟩
    neg m + pos m + pos (n + m * n)            ≡⟨ sym $ ℤ+-assoc (neg m) (pos m) (pos (n + m * n)) ⟩
    neg m + (pos m + pos (n + m * n))          ≡⟨ cong (neg m +_) $ sym $ pos-distrib-+ m (n + m * n) ⟩
    neg m + pos (m + (n + m * n))              ≡⟨ cong ((neg m +_) ∘ ℤ.pos) $ lemma7 m n ⟩
    neg m + pos (n + m * suc n)                ≡⟨ cong (neg m +_) $ sym $ predSucℤ (pos (n + m * suc n)) ⟩
    neg m + predℤ (sucℤ (pos (n + m * suc n))) ≡⟨ ℤ+-pred (neg m) (sucℤ (pos (n + m * suc n))) ⟩
    predℤ (neg m + sucℤ (pos (n + m * suc n))) ≡⟨ cong predℤ $ ℤ+-comm (neg m) (sucℤ (pos (n + m * suc n))) ⟩
    predℤ (sucℤ (pos (n + m * suc n)) + neg m) ∎
  )
ℤ*-pred (neg (suc m)) (pos (suc n)) =
  ( neg (n + m * n)                            ≡⟨ m≡0+ℤm _ ⟩
    0 + neg (n + m * n)                        ≡⟨ cong (_+ neg (n + m * n)) $ sym $ ℤ-m+-m≡0 m ⟩
    pos m + neg m + neg (n + m * n)            ≡⟨ sym $ ℤ+-assoc (pos m) (neg m) (neg (n + m * n)) ⟩
    pos m + (neg m + neg (n + m * n))          ≡⟨ cong (pos m +_) $ sym $ neg-distrib-+ m (n + m * n) ⟩
    pos m + neg (m + (n + m * n))              ≡⟨ cong ((pos m +_) ∘ ℤ.neg) $ lemma7 m n ⟩
    pos m + neg (n + m * suc n)                ≡⟨ cong (pos m +_) $ sym $ sucPredℤ (neg (n + m * suc n)) ⟩
    pos m + sucℤ (predℤ (neg (n + m * suc n))) ≡⟨ ℤ+-suc (pos m) (predℤ (neg (n + m * suc n))) ⟩
    sucℤ (pos m + predℤ (neg (n + m * suc n))) ≡⟨ cong sucℤ $ ℤ+-comm (pos m) (predℤ (neg (n + m * suc n))) ⟩
    sucℤ (predℤ (neg (n + m * suc n)) + pos m) ∎
  )
ℤ*-pred (pos (suc m)) (neg (suc n)) = cong predℤ
  ( predℤ (neg (n + m * suc (suc n)))   ≡⟨ cong (predℤ ∘ ℤ.neg) $ lemma6 m n ⟩
    predℤ (neg (m + (n + m * suc n)))   ≡⟨ cong predℤ $ neg-distrib-+ m (n + m * suc n) ⟩
    predℤ (neg m + neg (n + m * suc n)) ≡⟨ ℤ+-pred (neg m) (neg (n + m * suc n)) ⟩
    neg m + predℤ (neg (n + m * suc n)) ≡⟨ ℤ+-comm (neg m) (predℤ (neg (n + m * suc n))) ⟩
    predℤ (neg (n + m * suc n)) + neg m ∎
  )
ℤ*-pred (neg (suc m)) (neg (suc n)) = cong sucℤ
  ( sucℤ (pos (n + m * suc (suc n)))   ≡⟨ cong (sucℤ ∘ ℤ.pos) $ lemma6 m n ⟩
    sucℤ (pos (m + (n + m * suc n)))   ≡⟨ cong sucℤ $ pos-distrib-+ m (n + m * suc n) ⟩
    sucℤ (pos m + pos (n + m * suc n)) ≡⟨ sym $ ℤ+-suc (pos m) (pos (n + m * suc n)) ⟩
    pos m + sucℤ (pos (n + m * suc n)) ≡⟨ ℤ+-comm (pos m) (sucℤ (pos (n + m * suc n))) ⟩
    sucℤ (pos (n + m * suc n)) + pos m ∎
  )

lemma-ℤ*+-right-distrib : ∀ i → (q r : ℤ) → (q + r) * posneg i ≡ q * posneg i + r * posneg i
lemma-ℤ*+-right-distrib i q r =
  ( (q + r) * 0       ≡⟨ sym $ 0≡m*ℤ0 (q + r) ⟩
    0                 ≡⟨ refl ⟩
    0 + 0             ≡⟨ cong (0 +_) $ 0≡m*ℤ0 r ⟩
    0 + (r * 0)       ≡⟨ cong (_+ (r * 0)) $ 0≡m*ℤ0 q ⟩
    (q * 0) + (r * 0) ∎
  )

ℤ*+-right-distrib : (q r s : ℤ) → (q + r) * s ≡ q * s + r * s
ℤ*+-right-distrib q r (pos zero) = lemma-ℤ*+-right-distrib i0 q r
ℤ*+-right-distrib q r (neg zero) = lemma-ℤ*+-right-distrib i1 q r
ℤ*+-right-distrib q r (posneg i) = lemma-ℤ*+-right-distrib i q r
ℤ*+-right-distrib q r (pos (suc n)) =
  ( (q + r) * sucℤ (pos n)              ≡⟨ ℤ*-suc (q + r) (pos n) ⟩
    q + r + (q + r) * pos n             ≡⟨ cong (q + r +_) $ ℤ*+-right-distrib q r (pos n) ⟩
    q + r + (q * pos n + r * pos n)     ≡⟨ ℤ+-assoc (q + r) (q * pos n) (r * pos n) ⟩
    q + r + q * pos n + r * pos n       ≡⟨ cong (_+ r * pos n) $ sym $ ℤ+-assoc q r (q * pos n) ⟩
    q + (r + q * pos n) + r * pos n     ≡⟨ cong ((_+ r * pos n) ∘ (q +_)) $ ℤ+-comm r (q * pos n) ⟩
    q + (q * pos n + r) + r * pos n     ≡⟨ cong (_+ r * pos n) $ ℤ+-assoc q (q * pos n) r ⟩
    q + q * pos n + r + r * pos n       ≡⟨ sym $ ℤ+-assoc (q + q * pos n) r (r * pos n) ⟩
    q + q * pos n + (r + r * pos n)     ≡⟨ cong (q + q * pos n +_) $ sym $ ℤ*-suc r (pos n) ⟩
    q + q * pos n + r * sucℤ (pos n)    ≡⟨ cong (_+ r * sucℤ (pos n)) $ sym $ ℤ*-suc q (pos n) ⟩
    q * sucℤ (pos n) + r * sucℤ (pos n) ∎
  )
ℤ*+-right-distrib q r (neg (suc n)) =
  ( (q + r) * predℤ (neg n)               ≡⟨ ℤ*-pred (q + r) (neg n) ⟩
    (q + r) * (neg n) - (q + r)           ≡⟨ cong (_- (q + r)) $ ℤ*+-right-distrib q r (neg n) ⟩
    q * neg n + r * neg n - (q + r)       ≡⟨ {!!} ⟩ -- TODO: needs things like a + (- b) = a - b
    q * neg n - q + (r * neg n - r)       ≡⟨ cong (q * neg n - q +_) $ sym $ ℤ*-pred r (neg n) ⟩
    q * neg n - q + r * predℤ (neg n)     ≡⟨ cong (_+ r * predℤ (neg n)) $ sym $ ℤ*-pred q (neg n) ⟩
    q * predℤ (neg n) + r * predℤ (neg n) ∎
  )

ℤ*+-left-distrib : (q r s : ℤ) → q * (r + s) ≡ q * r + q * s
ℤ*+-left-distrib q r s =
  ( q * (r + s) ≡⟨ ℤ*-comm q (r + s) ⟩
    (r + s) * q ≡⟨ ℤ*+-right-distrib r s q ⟩
    r * q + s * q ≡⟨ cong (_+ s * q) $ ℤ*-comm r q ⟩
    q * r + s * q ≡⟨ cong (q * r +_) $ ℤ*-comm s q ⟩
    q * r + q * s ∎
  )

lemma-ℤ*-assoc : ∀ i → (m n : ℤ) → m * (n * posneg i) ≡ m * n * posneg i
lemma-ℤ*-assoc i m n =
  ( m * (n * 0)        ≡⟨ cong (m *_) $ sym $ 0≡m*ℤ0 n ⟩
    m * 0              ≡⟨ sym $ 0≡m*ℤ0 m ⟩
    0                  ≡⟨ 0≡m*ℤ0 (m * n) ⟩
    m * n * 0          ∎
  )

ℤ*-assoc : (m n o : ℤ) → m * (n * o) ≡ m * n * o
ℤ*-assoc m n (pos zero) = lemma-ℤ*-assoc i0 m n
ℤ*-assoc m n (neg zero) = lemma-ℤ*-assoc i1 m n
ℤ*-assoc m n (posneg i) = lemma-ℤ*-assoc i m n
ℤ*-assoc m n (pos (suc o)) =
  ( m * (n * sucℤ (pos o))  ≡⟨ cong (m *_) $ ℤ*-suc n (pos o) ⟩
    m * (n + n * pos o)     ≡⟨ ℤ*+-left-distrib m n (n * pos o) ⟩
    m * n + m * (n * pos o) ≡⟨ cong (m * n +_) $ ℤ*-assoc m n (pos o) ⟩
    m * n + m * n * pos o   ≡⟨ sym $ ℤ*-suc (m * n) (pos o) ⟩
    m * n * sucℤ (pos o)    ∎
  )
ℤ*-assoc m n (neg (suc o)) =
  ( m * (n * predℤ (neg o)) ≡⟨ cong (m *_) $ ℤ*-pred n (neg o) ⟩
    m * (n * neg o - n)     ≡⟨ {!!} ⟩ -- TODO: needs things like a + (- b) = a - b
    m * (n * neg o) - m * n ≡⟨ cong (_- m * n) $ ℤ*-assoc m n (neg o) ⟩
    m * n * neg o - m * n   ≡⟨ sym $ ℤ*-pred (m * n) (neg o) ⟩
    m * n * predℤ (neg o)   ∎
  )

instance
  ℚ+ : Op+ ℚ ℚ (const₂ ℚ)
  _+_ ⦃ ℚ+ ⦄ q r = q plus r where
    plus-lemma1 : (u a v b w c : ℤ)
      (x : ¬ a ≡ 0) (p₁ : ¬ b ≡ 0) (p₂ : ¬ c ≡ 0)
      (y : v * c ≡ w * b)
      → con (u * b + v * a) (a * b) (nonzero-prod a b x p₁) ≡ con (u * c + w * a) (a * c) (nonzero-prod a c x p₂)
    plus-lemma1 u a v b w c x p₁ p₂ y = path _ _ _ _ $
      (u * b + v * a) * (a * c)         ≡⟨ ℤ*+-right-distrib (u * b) (v * a) (a * c) ⟩
      u * b * (a * c) + v * a * (a * c) ≡⟨ cong (_+ (v * a * (a * c))) $
        u * b * (a * c)                   ≡⟨ sym $ ℤ*-assoc u b (a * c) ⟩
        u * (b * (a * c))                 ≡⟨ cong (u *_) $ ℤ*-comm b (a * c) ⟩
        u * (a * c * b)                   ≡⟨ cong ((u *_) ∘ (_* b)) $ ℤ*-comm a c ⟩
        u * (c * a * b)                   ≡⟨ cong (u *_) $ sym $ ℤ*-assoc c a b ⟩
        u * (c * (a * b))                 ≡⟨ ℤ*-assoc u c (a * b) ⟩
        u * c * (a * b)                   ∎
      ⟩
      u * c * (a * b) + v * a * (a * c) ≡⟨ cong (u * c * (a * b) +_) $
        v * a * (a * c)                   ≡⟨ sym $ ℤ*-assoc v a (a * c) ⟩
        v * (a * (a * c))                 ≡⟨ cong (v *_) $ ℤ*-comm a (a * c) ⟩
        v * (a * c * a)                   ≡⟨ cong ((v *_) ∘ (_* a)) $ ℤ*-comm a c ⟩
        v * (c * a * a)                   ≡⟨ cong (v *_) $ sym $ ℤ*-assoc c a a ⟩
        v * (c * (a * a))                 ≡⟨ ℤ*-assoc v c (a * a) ⟩
        v * c * (a * a)                   ≡⟨ cong (_* (a * a)) y ⟩
        w * b * (a * a)                   ≡⟨ sym $ ℤ*-assoc w b (a * a) ⟩
        w * (b * (a * a))                 ≡⟨ cong (w *_) $ ℤ*-assoc b a a ⟩
        w * (b * a * a)                   ≡⟨ cong ((w *_) ∘ (_* a)) $ ℤ*-comm b a ⟩
        w * (a * b * a)                   ≡⟨ cong (w *_) $ ℤ*-comm (a * b) a ⟩
        w * (a * (a * b))                 ≡⟨ ℤ*-assoc w a (a * b) ⟩
        w * a * (a * b)                   ∎
      ⟩
      u * c * (a * b) + w * a * (a * b) ≡⟨ sym $ ℤ*+-right-distrib (u * c) (w * a) (a * b) ⟩
      (u * c + w * a) * (a * b)         ∎

    plus-lemma2 : (u a v b w c : ℤ)
      (x : ¬ a ≡ 0) (p₁ : ¬ b ≡ 0) (p₂ : ¬ c ≡ 0)
      (y : v * c ≡ w * b)
      → con (v * a + u * b) (b * a) (nonzero-prod b a p₁ x) ≡ con (w * a + u * c) (c * a) (nonzero-prod c a p₂ x)
    plus-lemma2 u a v b w c x p₁ p₂ y = -- trying to reuse plus_lemma1 with this proof
      con (v * a + u * b) (b * a) _ ≡⟨ cong (λ nom → con nom (b * a) _) $ ℤ+-comm (v * a) (u * b) ⟩
      con (u * b + v * a) (b * a) _ ≡⟨ cong₂ (λ denom prf → con (u * b + v * a) denom prf) (ℤ*-comm b a) $ {!!} ⟩ -- TODO: not sure if this is the right approach
      con (u * b + v * a) (a * b) (nonzero-prod a b x p₁) ≡⟨ plus-lemma1 u a v b w c x p₁ p₂ y ⟩
      con (u * c + w * a) (a * c) (nonzero-prod a c x p₂) ≡⟨ cong₂ (λ denom prf → con (u * c + w * a) denom prf) (ℤ*-comm a c) $ {!!} ⟩ -- TODO: ditto
      con (u * c + w * a) (c * a) (nonzero-prod c a p₂ x) ≡⟨ cong (λ nom → con nom (c * a) (nonzero-prod c a p₂ x)) $ ℤ+-comm (u * c) (w * a) ⟩
      con (w * a + u * c) (c * a) _ ∎

    _plus_ : ℚ → ℚ → ℚ
    con u a x plus con v b y = con (u * b + v * a) (a * b) (nonzero-prod a b x y)
    con u a x plus path v b w c {p₁} {p₂} y i = plus-lemma1 u a v b w c x p₁ p₂ y i
    path v b w c {p₁} {p₂} y i plus con u a x = plus-lemma2 u a v b w c x p₁ p₂ y i
    path u a v b {p} {q} x i plus path u₁ a₁ v₁ b₁ {p₁} {q₁} x₁ j =
      isSet→isSet' trunc
        (plus-lemma1 u a u₁ a₁ v₁ b₁ p p₁ q₁ x₁)
        (plus-lemma1 v b u₁ a₁ v₁ b₁ q p₁ q₁ x₁)
        (plus-lemma2 u₁ a₁ u a v b p₁ p q x)
        (plus-lemma2 v₁ b₁ u a v b q₁ p q x)
        i j
    q@(path _ _ _ _ _ _) plus trunc r r₁ x y i i₁ = trunc (q plus r) (q plus r₁) (cong (q plus_) x) (cong (q plus_) y) i i₁
    q@(con _ _ _) plus trunc r r₁ x y i i₁ = trunc (q plus r) (q plus r₁) (cong (q plus_) x) (cong (q plus_) y) i i₁
    trunc q q₁ x y i i₁ plus r = trunc (q plus r) (q₁ plus r) (cong (_plus r) x) (cong (_plus r) y) i i₁

neg-assoc* : {a b : ℤ} → - (a * b) ≡ (- a) * b
neg-assoc* {pos zero} {pos n₁} = sym posneg
neg-assoc* {pos (suc n)} {pos n₁} = refl
neg-assoc* {pos zero} {neg zero} = sym posneg
neg-assoc* {pos zero} {neg (suc n₁)} = posneg
neg-assoc* {pos (suc n)} {neg zero} = refl
neg-assoc* {pos (suc n)} {neg (suc n₁)} = refl
neg-assoc* {pos zero} {posneg i} = sym posneg
neg-assoc* {pos (suc n)} {posneg i} = refl
neg-assoc* {neg zero} {pos n₁} = sym posneg
neg-assoc* {neg (suc n)} {pos n₁} = refl
neg-assoc* {neg zero} {neg zero} = sym posneg
neg-assoc* {neg (suc n)} {neg zero} = refl
neg-assoc* {neg zero} {neg (suc n₁)} = posneg
neg-assoc* {neg (suc n)} {neg (suc n₁)} = refl
neg-assoc* {neg zero} {posneg i} = sym posneg
neg-assoc* {neg (suc n)} {posneg i} = refl
neg-assoc* {posneg i} {pos n} = sym posneg
neg-assoc* {posneg i} {neg zero} = sym posneg
neg-assoc* {posneg i} {neg (suc n)} = posneg
neg-assoc* {posneg i} {posneg i₁} = sym posneg

instance
  ℚunary- : OpUnary- ℚ (const ℚ)
  -_ ⦃ ℚunary- ⦄ q = negative q where
    negative : ℚ → ℚ
    negative (con u a x) = con (- u) a x
    negative (path u a v b {p} {q} x i) = path (- u) a (- v) b {p = p} {q = q}
      ( - u * b ≡⟨ sym $ neg-assoc* {a = u} {b = b} ⟩
        - (u * b) ≡⟨ cong -_ x ⟩
        - (v * a) ≡⟨ neg-assoc* {a = v} {b = a} ⟩
        - v * a ∎
      ) i
    negative (trunc q q₁ x y i i₁) = trunc (negative q) (negative q₁) (cong negative x) (cong negative y) i i₁

instance
  ℚ- : Op- ℚ ℚ (const₂ ℚ)
  _-_ ⦃ ℚ- ⦄ q r = q + (- r)

instance
  ℚ< : Op< ℚ ℚ (const₂ Bool)
  _<_ ⦃ ℚ< ⦄ n m = n less-than m where
    _less-than_ : ℚ → ℚ → Bool
    con u a _ less-than con v b _ = u * b < v * a
    q@(con u a x) less-than path v b w c y i = {!!} -- not sure
    path u a v b x i less-than r = {!!}
    q@(con _ _ _) less-than trunc r r₁ x y i i₁ = isSetBool (q less-than r) (q less-than r₁) (cong (q less-than_) x) (cong (q less-than_) y) i i₁
    trunc q q₁ x y i i₁ less-than r = isSetBool (q less-than r) (q₁ less-than r) (cong (_less-than r) x) (cong (_less-than r) y) i i₁

instance
  ℚ> : Op> ℚ ℚ (const₂ Bool)
  _>_ ⦃ ℚ> ⦄ n m = m < n

pabsℤ : ℤ → ℤ
pabsℤ = pos ∘ absℤ

abs-distrib* : {a b : ℤ} → pabsℤ (a * b) ≡ pabsℤ a * pabsℤ b
abs-distrib* {pos n} {pos n₁} = refl
abs-distrib* {pos n} {neg zero} = refl
abs-distrib* {pos n} {neg (suc n₁)} = refl
abs-distrib* {pos n} {posneg i} = refl
abs-distrib* {neg zero} {pos n₁} = refl
abs-distrib* {neg (suc n)} {pos n₁} = refl
abs-distrib* {neg zero} {neg zero} = refl
abs-distrib* {neg zero} {neg (suc n₁)} = refl
abs-distrib* {neg (suc n)} {neg zero} = refl
abs-distrib* {neg (suc n)} {neg (suc n₁)} = refl
abs-distrib* {neg zero} {posneg i} = refl
abs-distrib* {neg (suc n)} {posneg i} = refl
abs-distrib* {posneg i} {pos n} = refl
abs-distrib* {posneg i} {neg zero} = refl
abs-distrib* {posneg i} {neg (suc n)} = refl
abs-distrib* {posneg i} {posneg i₁} = refl

abs-zero : {a : ℤ} → pabsℤ a ≡ 0 → a ≡ 0
abs-zero {pos zero} _ = refl
abs-zero {pos (suc _)} p = p
abs-zero {neg zero} _ = sym posneg
abs-zero {neg (suc _)} p = cong (neg ∘ absℤ) p ∙ (sym posneg)
abs-zero {posneg i} _ = λ j → posneg (i ∧ ~ j)

abs : ℚ → ℚ
abs (con u a x) = con (pabsℤ u) (pabsℤ a) λ y → x (abs-zero y)
abs (path u a v b {p} {q} x i) = path (pabsℤ u) (pabsℤ a) (pabsℤ v) (pabsℤ b)
  {p = λ x → p (abs-zero x)}
  {q = λ x → q (abs-zero x)}
  ((sym $ abs-distrib* {a = u} {b = b}) ∙ cong pabsℤ x ∙ abs-distrib* {a = v} {b = a})
  i
abs (trunc q q₁ x y i i₁) = trunc (abs q) (abs q₁) (cong abs x) (cong abs y) i i₁

infix 10 _~⟨_⟩_

-- The reason for all of the above machinery:
data ℝ : Set
data _~⟨_⟩_ : ℝ → (tol : ℚ) → ⦃ _ : tol > 0 ≡ true ⦄ → ℝ → Set

data ℝ where
  rat : (q : ℚ) → ℝ
  lim : (x : ℚ → ℝ) → ((δ ε : ℚ) ⦃ _ : δ + ε > 0 ≡ true ⦄ → x δ ~⟨ δ + ε ⟩ x ε) → ℝ
  eq : (u v : ℝ) → ((ε : ℚ) ⦃ _ : ε > 0 ≡ true ⦄ → u ~⟨ ε ⟩ v) → u ≡ v

data _~⟨_⟩_ where
  ~-rat-rat : ∀ {q r ε} ⦃ _ : ε > 0 ≡ true ⦄ → abs (q - r) < ε ≡ true → rat q ~⟨ ε ⟩ rat r
  ~-rat-lim : ∀ {q y l δ ε} ⦃ _ : ε - δ > 0 ≡ true ⦄ ⦃ _ : ε > 0 ≡ true ⦄ → rat q ~⟨ ε - δ ⟩ y δ → rat q ~⟨ ε ⟩ lim y l
  ~-lim-rat : ∀ {x l r δ ε} ⦃ _ : ε - δ > 0 ≡ true ⦄ ⦃ _ : ε > 0 ≡ true ⦄ → x δ ~⟨ ε - δ ⟩ rat r → lim x l ~⟨ ε ⟩ rat r
  ~-lim-lim : ∀ {x lₓ y ly ε δ η} ⦃ _ : ε > 0 ≡ true ⦄ ⦃ _ : ε - δ - η > 0 ≡ true ⦄ → x δ ~⟨ ε - δ - η ⟩ y η → lim x lₓ ~⟨ ε ⟩ lim y ly
  ~-isProp : ∀ {u v ε} ⦃ _ : ε > 0 ≡ true ⦄ → isProp (u ~⟨ ε ⟩ v)

max_stars_repo_name: dylanede/cubical-experiments

max_issues_repo_name: dylanede/cubical-experiments

max_forks_repo_name: dylanede/cubical-experiments


text:
data Bool : Set where
  true false : Bool

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

one : Nat
one = suc zero

two : Nat
two = suc one

data Fin : Nat → Set where
  zero : ∀{n} → Fin (suc n)
  suc  : ∀{n} (i : Fin n) → Fin (suc n)

--This part works as expected:

s : ∀ n → (f : (k : Fin n) → Bool) → Fin (suc n)
s n f = zero

t1 : Fin two
t1 = s one (λ { zero → true ; (suc ()) })

-- But Agda is not able to infer the 1 in this case:

ttwo : Fin two
ttwo = s _ (λ { zero → true ; (suc ()) })

-- Warning:
-- _142 : Nat

-- The problem gets worse when i add arguments to the ttwo function. This gives an error:

t3 : Set → Fin two
t3 A = s _ (λ { zero → true ; (suc ()) })

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --rewriting  #-}
open import Reflection hiding (return; _>>=_) renaming (_≟_ to _≟r_)

open import Data.List hiding (_++_)
open import Data.Vec as V using (Vec; updateAt)
open import Data.Unit
open import Data.Nat as N
open import Data.Nat.Properties
open import Data.Fin using (Fin; #_; suc; zero)
open import Data.Maybe hiding (_>>=_; map)
open import Function
open import Data.Bool
open import Data.Product hiding (map)
open import Data.String renaming (_++_ to _++s_; concat to sconc; length to slen)
open import Data.Char renaming (_≈?_ to _c≈?_; show to showChar)

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Decidable hiding (map)
open import Data.Nat.Show renaming (show to showNat)

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

open import Category.Monad using (RawMonad)

open RawMonad {{...}} public

instance
  monadMB : ∀ {f} → RawMonad {f} Maybe
  monadMB = record { return = just ; _>>=_ = Data.Maybe._>>=_ }

  monadTC : ∀ {f} → RawMonad {f} TC
  monadTC = record { return = Reflection.return ; _>>=_ = Reflection._>>=_ }

data Err {a} (A : Set a) : Set a where
  error : String → Err A
  ok : A → Err A

instance
  monadErr : ∀ {f} → RawMonad {f} Err
  monadErr = record {
    return = ok ;
    _>>=_ = λ { (error s) f → error s ; (ok a) f → f a }
    }

record RawMonoid {a}(A : Set a) : Set a where
  field
    _++_ : A → A → A
    ε : A
  ++/_ : List A → A
  ++/ [] = ε
  ++/ (x ∷ a) = x ++ ++/ a

  infixr 5 _++_

open RawMonoid {{...}} public

instance
  monoidLst : ∀ {a}{A : Set a} → RawMonoid (List A)
  monoidLst {A = A} = record {
    _++_ = Data.List._++_;
    ε = []
    }

  monoidErrLst : ∀{a}{A : Set a} → RawMonoid (Err $ List A)
  monoidErrLst = record {
    _++_ =  λ where
      (error s) _ → error s
      _ (error s) → error s
      (ok s₁) (ok s₂) → ok (s₁ ++ s₂)
    ;
    ε = ok []
    }

defToTerm : Name → Definition → List (Arg Term) → Term
defToTerm _ (function cs) as = pat-lam cs as
defToTerm _ (constructor′ d) as = con d as
defToTerm _ _ _ = unknown

derefImmediate : Term → TC Term
derefImmediate (def f args) = getDefinition f >>= λ f' → return (defToTerm f f' args)
derefImmediate x = return x

derefT : Term → TC Term
derefT (def f args) = getType f
derefT (con f args) = getType f
derefT x = return x

Ctx = List $ Arg Type

drop-ctx' : Ctx → ℕ → Ctx
drop-ctx' l zero = l
drop-ctx' [] (suc n) = []
drop-ctx' (x ∷ l) (suc n) = drop-ctx' l n

take-ctx' : Ctx → ℕ → Ctx
take-ctx' [] zero = []
take-ctx' [] (suc p) = [] --error "take-ctx: ctx too short for the prefix"
take-ctx' (x ∷ l) zero = []
take-ctx' (x ∷ l) (suc p) = x ∷ take-ctx' l p

-- FIXME we probably want to error out on these two functions.
pi-to-ctx : Term → Ctx
pi-to-ctx (Π[ s ∶ a ] x) = (a ∷ pi-to-ctx x)
pi-to-ctx _ = []

ctx-to-pi : List (Arg Type) → Type
ctx-to-pi [] = def (quote ⊤) []
ctx-to-pi (a ∷ t) = Π[ "_" ∶  a ] ctx-to-pi t

ty-con-args : Arg Type → List $ Arg Type
ty-con-args (arg _ (con c args)) = args
ty-con-args (arg _ (def c args)) = args
ty-con-args _ = []

con-to-ctx : Term → Term × Ctx
con-to-ctx (Π[ s ∶ a ] x) = let t , args = con-to-ctx x in t , a ∷ args
con-to-ctx x = x , []

record Eq : Set where
  constructor _↦_
  field
    left  : Term
    right : Term

Eqs = List Eq

eqs-shift-vars : Eqs → ℕ → Eqs

mbeqs-eqs : Maybe Eqs → Eqs
mbeqs-eqs (just x) = x
mbeqs-eqs nothing = []

-- stupid name, this generates equalities for two terms being somewhat similar.
unify-eq : Term → Term → Eqs
unify-eq-map : List $ Arg Term → List $ Arg Term → Maybe Eqs

unify-eq (var x [])             y = [ var x [] ↦ y ]
unify-eq (var x args@(_ ∷ _))   t₂ = {!!}

unify-eq (con c args) (con c′ args′) with c ≟-Name c′
... | yes p = mbeqs-eqs $ unify-eq-map args args′
... | no ¬p = []
unify-eq (def f args) (def f′ args′) with f ≟-Name f′
              -- Generally speaking this is a lie of course, as
              -- not all the definitons are injective.  However,
              -- we mainly use these for types such as Vec, Nat, etc
              -- and for these cases it is fine.  How do I check whether
              -- the definition is a data type or not?
... | yes p = mbeqs-eqs $ unify-eq-map args args′
... | no ¬p = []
unify-eq (lam v t) t₂ = {!!}
unify-eq (pat-lam cs args) t₂ = {!!}
unify-eq (pi a b) t₂ = {!!}
unify-eq (sort s) t₂ = {!!}
unify-eq (lit l) y = [ lit l ↦ y ]
unify-eq (meta x x₁) t₂ = {!!}
unify-eq unknown t₂ = {!!}
unify-eq x              (var y []) = [ x ↦ var y [] ]
unify-eq x              (var y args@(_ ∷ _)) =  {!!} --[ x ↦ var y [] ]
unify-eq a b = []

test-unify₁ = unify-eq (var 0 []) (con (quote ℕ.suc) [ vArg $ con (quote ℕ.zero) [] ] )
test-unify₂ = unify-eq (con (quote ℕ.suc) [ vArg $ con (quote ℕ.zero) [] ] )   (var 0 [])

unify-eq-map [] [] = just []
unify-eq-map [] (y ∷ _) = nothing
unify-eq-map (x ∷ _) [] = nothing
unify-eq-map (arg _ x ∷ xs) (arg _ y ∷ ys) = do
  eqs ← unify-eq-map xs ys
  return $ unify-eq x y ++ eqs

eq-find-l : Eqs → Term → Term
eq-find-l [] t = t
eq-find-l (l ↦ r ∷ eqs) t with l ≟r t
... | yes l≡t = r
... | no  l≢t = eq-find-l eqs t

decvar : Term → (min off : ℕ) → Err Term
decvar-map : List $ Arg Term → (min off : ℕ) → Err $ List $ Arg Term

decvar (var x args) m o with x ≥? m
decvar (var x args) m o | yes x≥m with x ≥? o
decvar (var x args) m o | yes x≥m | yes x≥o = do
  args ← decvar-map args m o
  return $ var (x ∸ o) args
decvar (var x args) m o | yes x≥m | no x≱o = error "decvar: variable index is less than decrement"
decvar (var x args) m o | no x≱m = do
  args ← decvar-map args m o
  return $ var x args
decvar (con c args) m o = do
  args ← decvar-map args m o
  return $ con c args
decvar (def f args) m o = do
  args ← decvar-map args m o
  return $ def f args
decvar (lam v t) m o = {!!}
decvar (pat-lam cs args) m o = {!!}
decvar (Π[ s ∶ arg i a ] x) m o = do
  a ← decvar a m o
  x ← decvar x (1 + m) o
  return $ Π[ s ∶ arg i a ] x
decvar (sort (set t)) m o = do
  t ← decvar t m o
  return $ sort $ set t
decvar (sort (lit n)) m o =
  return $ sort $ lit n
decvar (sort unknown) m o =
  return $ sort $ unknown
decvar (lit l) m o = return $ lit l
decvar (meta x args) m o = do
  args ← decvar-map args m o
  return $ meta x args
decvar unknown m o = return unknown

decvar-map [] m o = ok []
decvar-map (arg i x ∷ l) m o = do
   x ← decvar x m o
   l ← decvar-map l m o
   return $ (arg i x) ∷ l

-- Note that we throw away the equality in case it didn't decvar'd correctly.
decvar-eqs : Eqs → (min off : ℕ) → Eqs
decvar-eqs [] m o = []
decvar-eqs (x ↦ y ∷ eqs) m o with (decvar x m o) | (decvar y m o)
decvar-eqs (x ↦ y ∷ eqs) m o | ok x′ | ok y′ = x′ ↦ y′ ∷ decvar-eqs eqs m o
decvar-eqs (x ↦ y ∷ eqs) m o | _     | _       = decvar-eqs eqs m o

check-var-pred : Term → (p : ℕ → Bool) → (min : ℕ) → Bool
check-var-pred-map : List $ Arg Term → (p : ℕ → Bool) (min : ℕ) → Bool
check-var-pred (var x args) p m with x ≥? m
check-var-pred (var x args) p m | yes x≥m with p x
check-var-pred (var x args) p m | yes x≥m | true = true
check-var-pred (var x args) p m | yes x≥m | false = check-var-pred-map args p m
check-var-pred (var x args) p m | no  x≱m = check-var-pred-map args p m
check-var-pred (con c args) p m = check-var-pred-map args p m
check-var-pred (def f args) p m = check-var-pred-map args p m
check-var-pred (lam v t) p m = {!!}
check-var-pred (pat-lam cs args) p m = {!!}
check-var-pred (Π[ s ∶ (arg i a) ] x) p m with check-var-pred a p m
... | true  = true
... | false = check-var-pred x p (1 + m)
check-var-pred (sort (set t)) p m = check-var-pred t p m
check-var-pred (sort (lit n)) p m = false
check-var-pred (sort unknown) p m = false
check-var-pred (lit l) p m = false
check-var-pred (meta x args) p m = check-var-pred-map args p m
check-var-pred unknown p m = false

check-var-pred-map [] p m = false
check-var-pred-map (arg _ x ∷ l) p m with check-var-pred x p m
... | true = true
... | false = check-var-pred-map l p m

-- eliminate equalities where we reverence variables that are greaterh than n
eqs-elim-vars-ge-l : Eqs → (n : ℕ) → Eqs
eqs-elim-vars-ge-l [] n = []
eqs-elim-vars-ge-l (l ↦ r ∷ eqs) n with check-var-pred l (isYes ∘ (_≥? n)) 0
... | true = eqs-elim-vars-ge-l eqs n
... | false = (l ↦ r) ∷ eqs-elim-vars-ge-l eqs n

subst-eq-var : Eqs → Type → (min : ℕ) → Type
subst-eq-var-map : Eqs → List $ Arg Type → (min : ℕ) → List $ Arg Type

-- Iterate over a reversed telescopic context and try to subsitute variables
-- from eqs, if we have some.
subst-eq-vars : Eqs → List $ Arg Type → List $ Arg Type

subst-eq-vars eqs [] = []
subst-eq-vars eqs ((arg i ty) ∷ tys) = let
  eqs = decvar-eqs eqs 0 1
  in (arg i $ subst-eq-var eqs ty 0) ∷ subst-eq-vars eqs tys

subst-eq-var eqs t@(var x []) m with x ≥? m
... | yes p = eq-find-l eqs t
... | no ¬p = t
subst-eq-var eqs (var x (x₁ ∷ args)) m = {!!}
subst-eq-var eqs (con c args) m =
      con c $ subst-eq-var-map eqs args m
subst-eq-var eqs (def f args) m =
      def f $ subst-eq-var-map eqs args m
subst-eq-var eqs (lam v t) m = {!!}
subst-eq-var eqs (pat-lam cs args) m = {!!}
subst-eq-var eqs (Π[ s ∶ (arg i a) ] x) m =
  Π[ s ∶ (arg i $ subst-eq-var eqs a m) ]
   -- We need to increase all the variables in
   -- eqs berfore entering x.
   subst-eq-var (eqs-shift-vars eqs 1) x (1 + m)
subst-eq-var eqs (sort s) m = {!!}
subst-eq-var eqs (lit l) m = lit l
subst-eq-var eqs (meta x x₁) m = {!!}
subst-eq-var eqs unknown m = unknown

subst-eq-var-map eqs [] m = []
subst-eq-var-map eqs (arg i x ∷ l) m =
  arg i (subst-eq-var eqs x m) ∷ subst-eq-var-map eqs l m

-- shift all the variables by n
shift-vars : Type → (min off : ℕ) → Type
shift-vars-map : List $ Arg Type → ℕ → ℕ → List $ Arg Type

shift-vars (var x args) m o with x ≥? m
... | yes p = var (o + x) (shift-vars-map args m o)
... | no ¬p = var x (shift-vars-map args m o)
shift-vars (con c args) m o = con c $ shift-vars-map args m o
shift-vars (def f args) m o = def f $ shift-vars-map args m o
shift-vars (lam v (abs s x)) m o = lam v $ abs s $ shift-vars x (1 + m) o

shift-vars (pat-lam cs args) m o = {!!}
shift-vars (Π[ s ∶ arg i a ] x) m o = Π[ s ∶ arg i (shift-vars a m o) ] shift-vars x (1 + m) o
shift-vars (sort (set t)) m o = sort $ set $ shift-vars t m o
shift-vars (sort (lit n)) m o = sort $ lit n
shift-vars (sort unknown) m o = sort unknown
shift-vars (lit l) m o = lit l
shift-vars (meta x args) m o = meta x $ shift-vars-map args m o
shift-vars unknown m o = unknown

shift-vars-map [] m o = []
shift-vars-map (arg i x ∷ l) m o = arg i (shift-vars x m o) ∷ shift-vars-map l m o

eqs-shift-vars [] n = []
eqs-shift-vars (l ↦ r ∷ eqs) n = let
  l′ = shift-vars l 0 n
  r′ = shift-vars r 0 n
  in l′ ↦ r′ ∷ eqs-shift-vars eqs n

trans-eqs : Eqs → Eq → Eqs
trans-eqs [] (l ↦ r) = []
trans-eqs ((l′ ↦ r′) ∷ eqs) eq@(l ↦ r) with l′ ≟r l
... | yes l′≡l = unify-eq r′ r ++ trans-eqs eqs eq
... | no _ with  l′ ≟r r
... | yes l′≡r = unify-eq r′ l ++ trans-eqs eqs eq
... | no _ with  r′ ≟r l
... | yes r′≡l = unify-eq l′ r ++ trans-eqs eqs eq
... | no _ with  r′ ≟r r
... | yes r′≡r = unify-eq l′ l ++ trans-eqs eqs eq
... | no _ = trans-eqs eqs eq

merge-eqs : (l r : Eqs) → (acc : Eqs) → Eqs
merge-eqs l [] acc = l ++ acc
merge-eqs l (x ∷ r) acc = merge-eqs l r (x ∷ acc ++ trans-eqs l x)

TyPat = Arg Type × Arg Pattern

merge-tys-pats : List $ Arg Type → List $ Arg Pattern → Err $ List TyPat
merge-tys-pats [] [] = ok []
merge-tys-pats [] (x ∷ ps) = error "merge-tys-pats: more patterns than types"
merge-tys-pats (x ∷ tys) [] = error "merge-tys-pats: more types than patterns"
merge-tys-pats (ty ∷ tys) (p ∷ ps) = ok [ ty , p ] ++ merge-tys-pats tys ps

shift-ty-vars-map : List TyPat → (min off : ℕ) → List TyPat
shift-ty-vars-map [] m o = []
shift-ty-vars-map ((arg i ty , p) ∷ l) m o = (arg i (shift-vars ty m o) , p) ∷ shift-ty-vars-map l m o

subst-typats : List TyPat → (min var : ℕ) → Type → List TyPat
subst-typats [] m v x = []
subst-typats ((arg tv ty , p) ∷ l) m v x = let
  ty′ = subst-eq-var [ (var v []) ↦ x ] ty m
  in (arg tv ty′ , p) ∷ subst-typats l (1 + m) (1 + v) (shift-vars x 0 1)

gen-n-vars : (count v : ℕ) → List $ Arg Term
gen-n-vars 0 _ = []
gen-n-vars (suc n) v = vArg (var v []) ∷ gen-n-vars n (1 + v)

{-# TERMINATING #-}
pats-ctx-open-cons : List TyPat → Eqs →  TC $ Eqs × (Err $ List TyPat)
pats-ctx-open-cons [] eqs = return $ eqs , ok []
pats-ctx-open-cons ((arg tv ty , arg pv (con c ps)) ∷ l) eqs = do
   con-type ← getType c
   let con-ret , con-ctx = con-to-ctx con-type
   -- bump indices in x by the length of ps
   let #ps = length ps
   let ty = shift-vars ty 0 #ps
   let con-eqs = unify-eq con-ret ty
   --let con-eqs = mbeqs-eqs $ unify-eq-map con-type-args ty-args
   let ctx = subst-eq-vars con-eqs (take-ctx' (reverse con-ctx) #ps)
   case #ps N.≟ 0 of λ where
     (no #ps≢0) → do
        -- Throw away substitutions that point further than the number
        -- of arguments to the constructor
        let con-eqs′ = eqs-elim-vars-ge-l con-eqs #ps
        let eqs′ = eqs-shift-vars eqs #ps
        let ctxl = merge-tys-pats (reverse ctx) ps
        -- substitute constructor into the rest of the context
        let l′ = subst-typats l 0 0 (con c $ gen-n-vars #ps 0)
        -- We eliminated 0 variable, so bump all the variables greater than 0
        let l′ = shift-ty-vars-map l′ 1 (#ps ∸ 1)
        eqs″ , ctxr ← pats-ctx-open-cons l′ (merge-eqs eqs′ con-eqs′ [])
        return $ eqs″ , ctxl ++ ctxr
     (yes  ps≡0) → do
        let con-eqs′ = eqs-elim-vars-ge-l con-eqs 0
        -- shift con-eqs′ by 1 to account for the newly inserted Dot.
        let con-eqs′ = eqs-shift-vars con-eqs′ 1
        -- Add equality of the newly inserted Dot and shift eqs by 1
        --let eqs′ = (var 0 [] ≜ con c []) ∷ eqs-shift-vars eqs 1
        let eqs′ = eqs-shift-vars eqs 1
        -- substitute constructor into the rest of the context
        let l′ = subst-typats l 0 0 (con c [])
        eqs″ , ctxr ← pats-ctx-open-cons l′ (merge-eqs eqs′ con-eqs′ [])
        return $ eqs″ , ok [ arg tv ty , arg pv dot ] ++ ctxr
pats-ctx-open-cons ((ty , arg i dot) ∷ l) eqs = do
  -- leave the dot and psas the equations further
  let eqs′ = eqs-shift-vars eqs 1
  eqs″ , ctx ← pats-ctx-open-cons l eqs′
  return $ eqs″ , ok [ ty , arg i dot ] ++ ctx
pats-ctx-open-cons ((ty , arg i (var s)) ∷ l) eqs = do
  -- pass the equations further and leave the variable as is
  let eqs′ = eqs-shift-vars eqs 1
  eqs″ , ctx ← pats-ctx-open-cons l eqs′
  return $ eqs″ , ok [ ty , arg i (var s) ] ++ ctx
pats-ctx-open-cons ((ty , arg i (lit x)) ∷ l) eqs = do
  -- we don't get any new equations from the literal so
  -- pass the equations further and insert the dot
  let eqs′ = eqs-shift-vars eqs 1
  let l′ = subst-typats l 0 0 (lit x)
  eqs″ , ctx ← pats-ctx-open-cons l′ eqs′
  return $ eqs″ , ok [ ty , arg i dot ] ++ ctx
pats-ctx-open-cons ((ty , arg i (proj f)) ∷ l) eqs =
  return $ eqs , error "pats-ctx-open-cons: projection found, fixme"
pats-ctx-open-cons ((ty , arg i absurd) ∷ l) eqs =
  return $ eqs , error "pats-ctx-open-cons: absurd pattern found, fixme"

-- Check whether the varibale (var 0) can be found in the tyspats
-- telescopic context.
check-ref : List TyPat → (v : ℕ) → Bool
check-ref [] v = false
check-ref ((arg _ ty , _) ∷ l) v with check-var-pred ty (isYes ∘ (N._≟ v)) 0
... | true  = true
... | false = check-ref l (1 + v)

-- XXX we are going to ignore the errors from the decvar, as we assume that
-- (var 0) is not referenced in the telescopic pattern.
dec-typats : List TyPat → (min : ℕ) → List TyPat
dec-typats [] m = []
dec-typats ((arg ti ty , p) ∷ l) m with decvar ty m 1
... | ok ty′  = (arg ti ty′ , p) ∷ dec-typats l (1 + m)
... | error _ = (arg ti ty , p) ∷ dec-typats l (1 + m)

-- Try to eliminate dots if there is no references in the rhs to this variable
{-# TERMINATING #-}  -- XXX this can be resolved, this function IS terminating
try-elim-dots : List TyPat → List TyPat
try-elim-dots [] = []
try-elim-dots ((ty , arg i dot) ∷ tyspats) with check-ref tyspats 0
... | true = (ty , arg i dot) ∷ try-elim-dots tyspats
... | false = try-elim-dots (dec-typats tyspats 1)
try-elim-dots ((ty , p) ∷ tyspats) = (ty , p) ∷ try-elim-dots tyspats

-- Look at the ctx list in *reverse* and get the list of variables that
-- correspond to dot patterns
get-dots : List TyPat → ℕ → List ℕ
get-dots [] o = []
get-dots ((_ , arg _ dot) ∷ l) o = o ∷ get-dots l (1 + o)
get-dots (_ ∷ l) o = get-dots l (1 + o)

-- Check if a given term contains any variable from the list
check-refs : Term → List ℕ → Bool
check-refs t [] = false
check-refs t (v ∷ vs) with check-var-pred t (isYes ∘ (N._≟ v)) 0
... | true = true
... | false = check-refs t vs

-- Eliminate the rhs of each eq in case it references dot patterns.
eqs-elim-nondots : Eqs → List ℕ → Eqs
eqs-elim-nondots [] _ = []
eqs-elim-nondots (eq@(_ ↦ r) ∷ eqs) vs with check-refs r vs
... | true = eqs-elim-nondots eqs vs
... | false = eq ∷ eqs-elim-nondots eqs vs

-- Substitute the variables from eqs into the *reversed* telescopic
-- context.
subst-eq-typats : Eqs → List TyPat → List TyPat
subst-eq-typats eqs [] = []
subst-eq-typats []  l  = l
subst-eq-typats eqs ((arg ti ty , p) ∷ typats) = let
  eqs = decvar-eqs eqs 0 1
  in (arg ti (subst-eq-var eqs ty 0) , p) ∷ subst-eq-typats eqs typats

check-no-dots : List TyPat → Bool
check-no-dots [] = true
check-no-dots ((_ , arg _ dot) ∷ l) = false
check-no-dots (_ ∷ l) = check-no-dots l

check-all-vars : List TyPat → Bool
check-all-vars [] = true
check-all-vars ((_ , arg _ (var _)) ∷ l) = check-all-vars l
check-all-vars (_ ∷ l) = false

check-conlit : List TyPat → Bool
check-conlit [] = false
check-conlit ((_ , arg _ (con _ _)) ∷ l) = true
check-conlit ((_ , arg _ (lit _)) ∷ l) = true
check-conlit (_ ∷ l) = check-conlit l

{-# TERMINATING #-}
compute-ctx : List TyPat → TC $ Err $ List TyPat
compute-ctx typats with check-no-dots typats ∧ check-all-vars typats
... | true = return $ ok typats
... | false with check-conlit typats
... | true = do
      eqs , typats ← pats-ctx-open-cons typats []
      case typats of λ where
        (error s) → return $ error s
        (ok t) → let
          sub = eqs-elim-nondots (eqs ++ map (λ { (l ↦ r) → r ↦ l}) eqs) (get-dots (reverse t) 0)
          t = subst-eq-typats sub (reverse t)
          t = try-elim-dots (reverse t)
          in compute-ctx t
... | false = return $ error "compute-ctx: can't eliminate dots in the context"

-- try normalising every clause of the pat-lam, given
-- the context passed as an argument.  Propagate error that
-- can be produced by pats-ctx.
pat-lam-norm : Term → Ctx → TC $ Err Term
pat-lam-norm (pat-lam cs args) ctx = do
  cs ← hlpr ctx cs
  case cs of λ where
    (ok cs) → return $ ok (pat-lam cs args)
    (error s) → return $ error s
  --return $ ok (pat-lam cs args)
  where
    hlpr : Ctx → List Clause → TC $ Err (List Clause)
    hlpr ctx [] = return $ ok []
    hlpr ctx (clause ps t ∷ l) = do
      case merge-tys-pats ctx ps of λ where
        (error s) → return $ error s
        (ok typats) → do
           typats ← compute-ctx typats
           case typats of λ where
             (ok typats) → do
               let ctx′ = map proj₁ typats
               t ← inContext (reverse ctx′) (normalise t)
               l ← hlpr ctx l
               return $ ok [ clause ps t ] ++ l
             (error s) →
               --return $ clause ps t ∷ l
               -- Make sure that we properly error out
               -- Uncomment above line, in case you want to skip the error.
               return $ error s
    hlpr ctx (a ∷ l) = do
      l' ← hlpr ctx l
      return (ok [ a ] ++ l')
      --return (a ∷ l')
pat-lam-norm x ctx = return $ error "pat-lam-norm: Shouldn't happen" --return $ ok x

macro
  reflect : Term → Term → TC ⊤
  reflect f a = -- not sure I need this
                --withNormalisation true
                normalise f >>=
                (derefImmediate)
                >>= quoteTC >>= unify a

  reflect-ty : Name → Type → TC ⊤
  reflect-ty f a = getType f >>= quoteTC >>= normalise >>= unify a

  tstctx : Name → Type → TC ⊤
  tstctx f a = do
    t ← getType f
    q ← quoteTC (con-to-ctx t)
    unify a q

  rtest : Term → Term → TC ⊤
  rtest f a = do
     t ← derefT f
     v ← derefImmediate f
     v ← pat-lam-norm v (pi-to-ctx t)
     q ← quoteTC v
     --q ← quoteTC (con-to-ctx t)
     unify a q

  norm-test : Term → Term → TC ⊤
  norm-test tm a = do
    t ← derefT tm
    v ← derefImmediate tm
    --let vec-and'-pat-[] = (hArg dot ∷ vArg (con (quote nil) []) ∷ vArg (var "_") ∷ [])
    {-
    let add-2v-pat = (hArg (var "_") ∷
                      vArg (con (quote imap) (hArg dot ∷ vArg (var "a") ∷ [])) ∷
                      vArg (con (quote imap) (hArg dot ∷ vArg (var "b") ∷ [])) ∷ [])
    -}
    {-
    let vec-sum-pat = (hArg dot ∷
                       vArg
                       (con (quote V._∷_)
                        (hArg (var "_") ∷ vArg (var "x") ∷ vArg (var "a") ∷ []))
                       ∷
                       vArg
                       (con (quote V._∷_)
                        (hArg dot ∷ vArg (var "y") ∷ vArg (var "b") ∷ []))
                       ∷ [])
    -}
    let vec-sum-pat-[] = (hArg dot ∷ vArg (con (quote V.[]) []) ∷ vArg (var "_") ∷ [])

    {-
    let ty-args = args-to-ctx vec-args 0
    t ← getType (quote V._∷_)
    let t = subst-args 2 (reverse $ take-ctx' ty-args 2) 0 t
    -}
    let ctx = pi-to-ctx t
    case merge-tys-pats ctx vec-sum-pat-[] of λ where
      (error s) → unify a (lit (string s))
      (ok typats) → do
         eqs , t ← pats-ctx-open-cons typats []
         --let t = ok typats
         case t of λ where
           (error s) → unify a (lit (string s))
           (ok t) → do
              -- let sub = eqs-elim-nondots (eqs ++ map (λ { (l ≜ r) → r ≜ l}) eqs) (get-dots (reverse t) 0)
              -- let t = subst-eq-typats sub (reverse t)
              -- let t = try-elim-dots (reverse t)
              q ← quoteTC t
              unify a q

    --t ← inferType v -- (vArg n ∷ [ vArg lz ]))
    --let v = plug-new-args v (vArg n ∷ [ vArg lz ])
    --t ← inContext (reverse $ hArg lz ∷ [ hArg n ]) (normalise v)
    --t ← reduce t
    --t ← getType t
    --t ← inContext [] (normalise t)
    --q ← quoteTC (pi-to-ctx t)

  infert : Type → Term → TC ⊤
  infert t a = inferType t >>= quoteTC >>= unify a

-- {-
open import Data.Vec
vec-and : ∀ {n} → Vec Bool n → Vec Bool n → Vec Bool n
vec-and (x ∷ a) (y ∷ b) = x ∧ y ∷ vec-and a b
vec-and [] _ = []

-- explicit length
vec-and-nd : ∀ {n} → Vec Bool n → Vec Bool n → Vec Bool n
vec-and-nd {0}     []      _ = []
vec-and-nd {suc n} (_∷_ {n = n} x a) (_∷_ {n = n} y b) = x ∧ y ∷ vec-and-nd a b

data Vec' {l : Level} (A : Set l) : ℕ → Set l where
  nil  : Vec' A 0
  cons : A → {n : ℕ} → Vec' A n → Vec' A (1 + n)

vec-and' : ∀ {n} → Vec' Bool n → Vec' Bool n → Vec' Bool n
vec-and' nil _ = nil
vec-and' (cons x a) (cons y b) = cons (x ∧ y) (vec-and' a b)

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE +-identityʳ #-}

a = 1 + 0

xx : ℕ → Bool → ℕ → ℕ
xx x true y = let a = x * x in a + y
xx x false y = x + 2 + 0

postulate
  rev-rev : ∀ {a}{X : Set a}{n}{xs : Vec X n} →
            let rev = V.foldl (Vec X) (λ rev x → x ∷ rev) [] in
            rev (rev xs) ≡ xs

{-# REWRITE rev-rev #-}

test-reverse : ∀ {a}{X : Set a}{n} → X → Vec X n → Vec X (suc n)
test-reverse x xs =  x ∷ V.reverse (V.reverse xs)

test-rev-pat : ∀ {a}{X : Set a}{n} → X → Vec X n → Vec X (suc n)
test-rev-pat x [] = x ∷ []
test-rev-pat x xs = x ∷ V.reverse (V.reverse xs)

open import Array
add-2v : ∀ {n} → let X = Ar ℕ 1 (n ∷ []) in X → X → X
add-2v (imap a) (imap b) = imap λ iv → a iv + b iv

postulate
  asum : ∀ {n} → Ar ℕ 1 (n ∷ []) → ℕ

mm : ∀ {m n k} → let Mat a b = Ar ℕ 2 (a ∷ b ∷ []) in
                 Mat m n → Mat n k → Mat m k
mm (imap a) (imap b) = imap λ iv → let i = ix-lookup iv (# 0)
                                       j = ix-lookup iv (# 1)
                                   in asum (imap λ kv → let k = ix-lookup kv (# 0)
                                                        in a (i ∷ k ∷ []) * b (k ∷ j ∷ []))

data P (x : ℕ) : Set where
  c : P x

data TT : ℕ → Set where
  tc : ∀ {n} → P (suc n) → TT (suc n)

foo : ∀ {n} → TT (suc n) → ℕ
foo (tc x) = 5

xxx = 3 N.< 5

max_stars_repo_name: ashinkarov/agda-array

max_issues_repo_name: ashinkarov/agda-array

max_forks_repo_name: ashinkarov/agda-array


text:
open import Structure.Operator.Monoid
open import Structure.Setoid
open import Type

module Numeral.Natural.Oper.Summation {ℓᵢ ℓ ℓₑ} {I : Type{ℓᵢ}} {T : Type{ℓ}} {_▫_ : T → T → T} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ ⦃ monoid : Monoid{T = T}(_▫_) ⦄ where
open Monoid(monoid)

import      Lvl
open import Data.List
open import Data.List.Functions
open import Structure.Function
open import Structure.Operator

∑ : List(I) → (I → T) → T
∑(r) f = foldᵣ(_▫_) id (map f(r))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- Vectors, defined using a recursive function
------------------------------------------------------------------------

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

open import Equality

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

open import Prelude

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
open import Function-universe eq hiding (id; _∘_)
open import List eq using (length)
open import Surjection eq using (_↠_; ↠-≡)

private

  variable
    a b c : Level
    A B   : Type a
    f g   : A → B
    n     : ℕ

------------------------------------------------------------------------
-- The type

-- Vectors.

Vec : Type a → ℕ → Type a
Vec A zero    = ↑ _ ⊤
Vec A (suc n) = A × Vec A n

------------------------------------------------------------------------
-- Some simple functions

-- Finds the element at the given position.

index : Vec A n → Fin n → A
index {n = suc _} (x , _)  fzero    = x
index {n = suc _} (_ , xs) (fsuc i) = index xs i

-- Updates the element at the given position.

infix 3 _[_≔_]

_[_≔_] : Vec A n → Fin n → A → Vec A n
_[_≔_] {n = zero}  _        ()       _
_[_≔_] {n = suc _} (x , xs) fzero    y = y , xs
_[_≔_] {n = suc _} (x , xs) (fsuc i) y = x , (xs [ i ≔ y ])

-- Applies the function to every element in the vector.

map : (A → B) → Vec A n → Vec B n
map {n = zero}  f _        = _
map {n = suc _} f (x , xs) = f x , map f xs

-- Constructs a vector containing a certain number of copies of the
-- given element.

replicate : A → Vec A n
replicate {n = zero}  _ = _
replicate {n = suc _} x = x , replicate x

-- The head of the vector.

head : Vec A (suc n) → A
head = proj₁

-- The tail of the vector.

tail : Vec A (suc n) → Vec A n
tail = proj₂

------------------------------------------------------------------------
-- Conversions to and from lists

-- Vectors can be converted to lists.

to-list : Vec A n → List A
to-list {n = zero}  _        = []
to-list {n = suc n} (x , xs) = x ∷ to-list xs

-- Lists can be converted to vectors.

from-list : (xs : List A) → Vec A (length xs)
from-list []       = _
from-list (x ∷ xs) = x , from-list xs

-- ∃ (Vec A) is isomorphic to List A.

∃Vec↔List : ∃ (Vec A) ↔ List A
∃Vec↔List {A = A} = record
  { surjection = record
    { logical-equivalence = record
      { to   = to-list ∘ proj₂
      ; from = λ xs → length xs , from-list xs
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = uncurry from∘to
  }
  where
  to∘from : (xs : List A) → to-list (from-list xs) ≡ xs
  to∘from []       = refl _
  to∘from (x ∷ xs) = cong (x ∷_) (to∘from xs)

  tail′ : A → ∃ (Vec A) ↠ ∃ (Vec A)
  tail′ y = record
    { logical-equivalence = record
      { to   = λ where
                 (suc n , _ , xs) → n , xs
                 xs@(zero , _)    → xs
      ; from = Σ-map suc (y ,_)
      }
    ; right-inverse-of = refl
    }

  from∘to :
    ∀ n (xs : Vec A n) →
    (length (to-list xs) , from-list (to-list xs)) ≡ (n , xs)
  from∘to zero    _        = refl _
  from∘to (suc n) (x , xs) =                                    $⟨ from∘to n xs ⟩
    (length (to-list xs) , from-list (to-list xs)) ≡ (n , xs)   ↝⟨ _↠_.from $ ↠-≡ (tail′ x) ⟩□

    (length (to-list (x , xs)) , from-list (to-list (x , xs)))
      ≡
    (suc n , x , xs)                                            □

------------------------------------------------------------------------
-- Some properties

-- The map function satisfies the functor laws.

map-id :
  {A : Type a} {xs : Vec A n} → map id xs ≡ xs
map-id {n = zero}  = refl _
map-id {n = suc n} = cong (_ ,_) map-id

map-∘ :
  {A : Type a} {B : Type b} {C : Type c} {f : B → C} {g : A → B}
  {xs : Vec A n} →
  map (f ∘ g) xs ≡ map f (map g xs)
map-∘ {n = zero}  = refl _
map-∘ {n = suc n} = cong (_ ,_) map-∘

-- If f and g are pointwise equal, then map f xs and map g xs are
-- equal.

map-cong :
  ∀ {n} {xs : Vec A n} →
  (∀ x → f x ≡ g x) → map f xs ≡ map g xs
map-cong {n = zero}  _   = refl _
map-cong {n = suc n} hyp = cong₂ _,_ (hyp _) (map-cong hyp)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Signature
import Program

module Observations (Σ : Sig) (V : Set) (P : Program.Program Σ V) where

open import Terms Σ
open import Program Σ V
open import Rewrite Σ V P
open import Function
open import Relation.Nullary
open import Relation.Unary
open import Data.Product as Prod renaming (Σ to ⨿)
open import Streams hiding (_↓_)

-- | We will need _properly refining_ substitutions: σ properly refines t ∈ T V,
-- if ∀ v ∈ fv(t). σ(v) = f(α) for f ∈ Σ.
-- Then an observation step must go along a properly refining substitution,
-- which in turn allows us to construct a converging sequence of terms.

{- |
We can make an observation according to the following rule.

t ↓ s   fv(s) ≠ ∅    ∃ k, σ. s ~[σ]~ Pₕ(k)
--------------------------------------------
              t ----> t[σ]
-}
data _↦_ (t : T V) : T V → Set where
  obs-step : {s : T V} → t ↓ s → -- ¬ Empty (fv s) →
             (cl : dom P) {σ : Subst V V} →
             ProperlyRefining t σ → mgu s (geth P cl) σ →
             t ↦ app σ t

reduct : ∀{t s} → t ↦ s → T V
reduct (obs-step {s} _ _ _ _ ) = s

refining : ∀{t s} → t ↦ s → Subst V V
refining (obs-step _ _ {σ} _ _) = σ

is-refining : ∀{t s} (o : t ↦ s) → ProperlyRefining t (refining o)
is-refining (obs-step _ _ r _) = r

GroundTerm : Pred (T V) _
GroundTerm t = Empty (fv t)

--------
-- FLAW: This does not allow us to distinguish between inductive
-- and coinductive definitions on the clause level.
-- The following definitions are _global_ for a derivation!
-------

data IndDerivable (t : T V) : Set where
  ground : GroundTerm t → Valid t → IndDerivable t
  der-step : (s : T V) → t ↦ s → IndDerivable s → IndDerivable t

record CoindDerivable (t : T V) : Set where
  coinductive
  field
    term-SN : SN t
    der-obs : ⨿ (T V) λ s → t ↦ s × CoindDerivable s
open CoindDerivable public

obs-result : ∀{t} → CoindDerivable t → T V
obs-result = proj₁ ∘ der-obs

get-obs : ∀{t} (d : CoindDerivable t) → t ↦ (obs-result d)
get-obs = proj₁ ∘ proj₂ ∘ der-obs

-- | This should give us convergence to a term in T∞ V, see Terms.agda
coind-deriv-seq : (t : T V) → CoindDerivable t → ProperlyRefiningSeq t
hd-ref (coind-deriv-seq t d) = refining (get-obs d)
hd-is-ref (coind-deriv-seq t d) = is-refining (get-obs d)
tl-ref (coind-deriv-seq t d) with (der-obs d)
tl-ref (coind-deriv-seq t d) | ._ , obs-step red cl {σ} ref _ , d' =
  coind-deriv-seq (app σ t) d'

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module ImportWarnings where

open import ImportWarningsB

-- A warning in the top-level file
{-# REWRITE #-}

-- make sure that this file is long enough to detect if we inherit
-- also the warning highlighting
foooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooo : Set1
foooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooo = Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Type
open import Structure.Setoid

module Structure.Operator.Lattice {ℓ ℓₑ} (L : Type{ℓ}) ⦃ equiv-L : Equiv{ℓₑ}(L) ⦄ where

import      Lvl
open import Functional
import      Function.Names as Names
open import Logic
open import Logic.IntroInstances
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Function.Domain using (Involution ; involution)
open import Structure.Function.Multi
open import Structure.Function
open import Structure.Operator.Monoid
open import Structure.Operator.Properties
open import Structure.Operator.Proofs
open import Structure.Operator
open import Structure.Relator.Ordering
open import Structure.Relator.Properties
open import Syntax.Transitivity

record Semilattice (_▫_ : L → L → L) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ operator ⦄     : BinaryOperator(_▫_)
    ⦃ commutative ⦄  : Commutativity(_▫_)
    ⦃ associative ⦄  : Associativity(_▫_)
    ⦃ idempotent ⦄   : Idempotence(_▫_)

  order : L → L → Stmt
  order x y = (x ▫ y ≡ y)

  partialOrder : Weak.PartialOrder(order)(_≡_)
  Antisymmetry.proof (Weak.PartialOrder.antisymmetry partialOrder) {x}{y} xy yx =
    x     🝖-[ symmetry(_≡_) yx ]
    y ▫ x 🝖-[ commutativity(_▫_) ]
    x ▫ y 🝖-[ xy ]
    y     🝖-end
  Transitivity.proof (Weak.PartialOrder.transitivity partialOrder) {x}{y}{z} xy yz =
    x ▫ z       🝖-[ congruence₂ᵣ(_▫_)(_) (symmetry(_≡_) yz) ]
    x ▫ (y ▫ z) 🝖-[ symmetry(_≡_) (associativity(_▫_)) ]
    (x ▫ y) ▫ z 🝖-[ congruence₂ₗ(_▫_)(_) xy ]
    y ▫ z       🝖-[ yz ]
    z           🝖-end
  Reflexivity.proof  (Weak.PartialOrder.reflexivity  partialOrder) = idempotence(_▫_)

record Lattice (_∨_ : L → L → L) (_∧_ : L → L → L) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ [∨]-operator ⦄ : BinaryOperator(_∨_)
    ⦃ [∧]-operator ⦄ : BinaryOperator(_∧_)

    ⦃ [∨]-commutativity ⦄ : Commutativity(_∨_)
    ⦃ [∧]-commutativity ⦄ : Commutativity(_∧_)

    ⦃ [∨]-associativity ⦄ : Associativity(_∨_)
    ⦃ [∧]-associativity ⦄ : Associativity(_∧_)

    ⦃ [∨][∧]-absorptionₗ ⦄ : Absorptionₗ(_∨_)(_∧_)
    ⦃ [∧][∨]-absorptionₗ ⦄ : Absorptionₗ(_∧_)(_∨_)

  instance
    [∨][∧]-absorptionᵣ : Absorptionᵣ(_∨_)(_∧_)
    [∨][∧]-absorptionᵣ = [↔]-to-[→] OneTypeTwoOp.absorption-equivalence-by-commutativity [∨][∧]-absorptionₗ

  instance
    [∨]-idempotence : Idempotence(_∨_)
    Idempotence.proof [∨]-idempotence {x} =
      x ∨ x             🝖-[ congruence₂ᵣ(_∨_)(_) (symmetry(_≡_) (absorptionₗ(_∧_)(_∨_))) ]
      x ∨ (x ∧ (x ∨ x)) 🝖-[ absorptionₗ(_∨_)(_∧_) ]
      x                 🝖-end

  instance
    [∨]-semilattice : Semilattice(_∨_)
    [∨]-semilattice = intro

  instance
    [∧][∨]-absorptionᵣ : Absorptionᵣ(_∧_)(_∨_)
    [∧][∨]-absorptionᵣ = [↔]-to-[→] OneTypeTwoOp.absorption-equivalence-by-commutativity [∧][∨]-absorptionₗ

  instance
    [∧]-idempotence : Idempotence(_∧_)
    Idempotence.proof [∧]-idempotence {x} =
      x ∧ x             🝖-[ congruence₂ᵣ(_∧_)(_) (symmetry(_≡_) (absorptionₗ(_∨_)(_∧_))) ]
      x ∧ (x ∨ (x ∧ x)) 🝖-[ absorptionₗ(_∧_)(_∨_) ]
      x                 🝖-end

  instance
    [∧]-semilattice : Semilattice(_∧_)
    [∧]-semilattice = intro

  record Bounded (𝟎 : L) (𝟏 : L) : Stmt{ℓ Lvl.⊔ ℓₑ} where
    constructor intro
    field
      ⦃ [∨]-identityₗ ⦄ : Identityₗ(_∨_)(𝟎)
      ⦃ [∧]-identityₗ ⦄ : Identityₗ(_∧_)(𝟏)

    instance
      [∨]-identityᵣ : Identityᵣ(_∨_)(𝟎)
      [∨]-identityᵣ = [↔]-to-[→] One.identity-equivalence-by-commutativity [∨]-identityₗ

    instance
      [∧]-identityᵣ : Identityᵣ(_∧_)(𝟏)
      [∧]-identityᵣ = [↔]-to-[→] One.identity-equivalence-by-commutativity [∧]-identityₗ

    instance
      [∨]-identity : Identity(_∨_)(𝟎)
      [∨]-identity = intro

    instance
      [∧]-identity : Identity(_∧_)(𝟏)
      [∧]-identity = intro

    instance
      [∨]-absorberₗ : Absorberₗ(_∨_)(𝟏)
      [∨]-absorberₗ = OneTypeTwoOp.absorberₗ-by-absorptionₗ-identityₗ

    instance
      [∧]-absorberₗ : Absorberₗ(_∧_)(𝟎)
      [∧]-absorberₗ = OneTypeTwoOp.absorberₗ-by-absorptionₗ-identityₗ

    instance
      [∨]-absorberᵣ : Absorberᵣ(_∨_)(𝟏)
      [∨]-absorberᵣ = [↔]-to-[→] One.absorber-equivalence-by-commutativity [∨]-absorberₗ

    instance
      [∧]-absorberᵣ : Absorberᵣ(_∧_)(𝟎)
      [∧]-absorberᵣ = [↔]-to-[→] One.absorber-equivalence-by-commutativity [∧]-absorberₗ

    instance
      [∨]-absorber : Absorber(_∨_)(𝟏)
      [∨]-absorber = intro

    instance
      [∧]-absorber : Absorber(_∧_)(𝟎)
      [∧]-absorber = intro

    instance
      [∧]-monoid : Monoid(_∧_)
      Monoid.identity-existence [∧]-monoid = [∃]-intro(𝟏)

    instance
      [∨]-monoid : Monoid(_∨_)
      Monoid.identity-existence [∨]-monoid = [∃]-intro(𝟎)

    record Complemented (¬_ : L → L) : Stmt{ℓ Lvl.⊔ ℓₑ} where
      constructor intro
      field
        ⦃ [¬]-function ⦄      : Function(¬_)
        ⦃ excluded-middle   ⦄ : ComplementFunction(_∨_)(¬_)
        ⦃ non-contradiction ⦄ : ComplementFunction(_∧_)(¬_)

  record Distributive : Stmt{ℓ Lvl.⊔ ℓₑ} where
    constructor intro
    field
      ⦃ [∨][∧]-distributivityₗ ⦄ : Distributivityₗ(_∨_)(_∧_)
      ⦃ [∧][∨]-distributivityₗ ⦄ : Distributivityₗ(_∧_)(_∨_)

    instance
      [∨][∧]-distributivityᵣ : Distributivityᵣ(_∨_)(_∧_)
      [∨][∧]-distributivityᵣ = [↔]-to-[→] OneTypeTwoOp.distributivity-equivalence-by-commutativity [∨][∧]-distributivityₗ

    instance
      [∧][∨]-distributivityᵣ : Distributivityᵣ(_∧_)(_∨_)
      [∧][∨]-distributivityᵣ = [↔]-to-[→] OneTypeTwoOp.distributivity-equivalence-by-commutativity [∧][∨]-distributivityₗ

  -- TODO: Is a negatable lattice using one of its operators distributed by a negation a lattice? In other words, Lattice(_∧_)(¬_ ∘₂ (_∧_ on ¬_))?
  record Negatable (¬_ : L → L) : Stmt{ℓ Lvl.⊔ ℓₑ} where
    constructor intro
    field
      ⦃ [¬]-function ⦄   : Function(¬_)
      ⦃ [¬]-involution ⦄ : Involution(¬_)
      ⦃ [¬][∧][∨]-distributivity ⦄ : Preserving₂(¬_)(_∧_)(_∨_)

    instance
      [¬][∨][∧]-distributivity : Preserving₂(¬_)(_∨_)(_∧_)
      Preserving.proof [¬][∨][∧]-distributivity {x}{y} =
        ¬(x ∨ y)               🝖-[ congruence₁(¬_) (congruence₂(_∨_) (symmetry(_≡_) (involution(¬_))) (symmetry(_≡_) (involution(¬_)))) ]
        ¬((¬(¬ x)) ∨ (¬(¬ y))) 🝖-[ congruence₁(¬_) (symmetry(_≡_) (preserving₂(¬_)(_∧_)(_∨_))) ]
        ¬(¬((¬ x) ∧ (¬ y)))    🝖-[ involution(¬_) ]
        (¬ x) ∧ (¬ y)          🝖-end
open Lattice using (intro) public

{- TODO: ?
semilattices-to-lattice : ∀{_∨_ _∧_} → ⦃ _ : Semilattice(_∨_) ⦄ → ⦃ _ : Semilattice(_∧_) ⦄ → Lattice(_∨_)(_∧_)
Lattice.[∨]-operator (semilattices-to-lattice ⦃ join ⦄ ⦃ meet ⦄) = Semilattice.operator join
Lattice.[∧]-operator (semilattices-to-lattice ⦃ join ⦄ ⦃ meet ⦄) = Semilattice.operator meet
Lattice.[∨]-commutativity (semilattices-to-lattice ⦃ join ⦄ ⦃ meet ⦄) = Semilattice.commutative join
Lattice.[∧]-commutativity (semilattices-to-lattice ⦃ join ⦄ ⦃ meet ⦄) = Semilattice.commutative meet
Lattice.[∨]-associativity (semilattices-to-lattice ⦃ join ⦄ ⦃ meet ⦄) = Semilattice.associative join
Lattice.[∧]-associativity (semilattices-to-lattice ⦃ join ⦄ ⦃ meet ⦄) = Semilattice.associative meet
Absorptionₗ.proof (Lattice.[∨][∧]-absorptionₗ (semilattices-to-lattice {_∨_}{_∧_} ⦃ join ⦄ ⦃ meet ⦄)) {x} {y} =
  x ∨ (x ∧ y)    🝖-[ {!!} ]
  x    🝖-end
Absorptionₗ.proof (Lattice.[∧][∨]-absorptionₗ (semilattices-to-lattice {_∨_}{_∧_} ⦃ join ⦄ ⦃ meet ⦄)) {x} {y} =
  x ∧ (x ∨ y)    🝖-[ {!!} ]
  x    🝖-end
-}

-- Also called: De Morgan algebra
record MorganicAlgebra (_∨_ : L → L → L) (_∧_ : L → L → L) (¬_ : L → L) (⊥ : L) (⊤ : L) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ lattice ⦄             : Lattice(_∨_)(_∧_)
    ⦃ boundedLattice ⦄      : Lattice.Bounded(lattice)(⊥)(⊤)
    ⦃ distributiveLattice ⦄ : Lattice.Distributive(lattice)
    ⦃ negatableLattice ⦄    : Lattice.Negatable(lattice)(¬_)

record BooleanAlgebra (_∨_ : L → L → L) (_∧_ : L → L → L) (¬_ : L → L) (⊥ : L) (⊤ : L) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ lattice ⦄             : Lattice(_∨_)(_∧_)
    ⦃ boundedLattice ⦄      : Lattice.Bounded(lattice)(⊥)(⊤)
    ⦃ complementedLattice ⦄ : Lattice.Bounded.Complemented(boundedLattice)(¬_)
    ⦃ distributiveLattice ⦄ : Lattice.Distributive(lattice)

-- TODO: Heyting algebra
-- TODO: Import some proofs from SetAlgebra


text:
open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Bool

-----------------------------------------------------
-- Σ types
-----------------------------------------------------
data Σ {A : Set} (P : A → Set) : Set where
    Σ_intro : ∀ (a : A) → P a → Σ P

-----------------------------------------------------
-- Π type
-----------------------------------------------------
data Π {A : Set} (P : A → Set) : Set where
    Π_intro : (∀ (a : A) → P a) → Π P

-----------------------------------------------------
-- constT
-----------------------------------------------------
constT : ∀ (X : Set) (Y : Set) → Y → Set
constT x _ _ = x

-----------------------------------------------------
-- Tuples using Σ types (const)
-----------------------------------------------------
Σ-pair : ∀ (A B : Set) → Set
Σ-pair a b = Σ (constT b a)

Σ-mkPair : ∀ {A : Set}  {B : Set} → A → B → Σ-pair A B
Σ-mkPair a b = Σ_intro a b

Σ-fst : ∀ {A B : Set} → Σ-pair A B → A
Σ-fst (Σ_intro a _) = a

Σ-snd : ∀ {A B : Set} → Σ-pair A B → B
Σ-snd (Σ_intro _ b) = b

-----------------------------------------------------
-- Exponential using Π type (const)
-----------------------------------------------------
Π-function : ∀ (A B : Set) → Set
Π-function a b = Π (constT b a)

Π-mkFunction : ∀ {A B : Set} → (A → B) → Π-function A B
Π-mkFunction f = Π_intro f

Π-apply : ∀ {A B : Set} → Π-function A B → A → B
Π-apply (Π_intro f) a = f a

-----------------------------------------------------
-- bool
-----------------------------------------------------
bool : ∀ (A B : Set) → Bool → Set
bool a _ true  = a
bool _ b false = b

-----------------------------------------------------
-- Sum type using Σ types
-----------------------------------------------------
Σ-sum : ∀ (A B : Set) → Set
Σ-sum a b = Σ (bool a b)

Σ-sum_left : ∀ {A : Set} (B : Set) → A → Σ-sum A B
Σ-sum_left _ a = Σ_intro true a

Σ-sum_right : ∀ {B : Set} (A : Set) → B → Σ-sum A B
Σ-sum_right _ b = Σ_intro false b

Σ-sum_elim : ∀ {A B R : Set} → (A → R) → (B → R) → Σ-sum A B → R
Σ-sum_elim f _ (Σ_intro true  a) = f a
Σ-sum_elim _ g (Σ_intro false b) = g b

-----------------------------------------------------
-- prodPredicate
-----------------------------------------------------
prodPredicate : ∀ (A B R : Set) → Set
prodPredicate a b r = (a → r) → (b → r) → r

-----------------------------------------------------
-- Sum type using Π types
-----------------------------------------------------
data Π' {a b} {A : Set a} (P : A → Set b) : Set (a ⊔ b) where
    Π'_intro : (∀ (a : A) → P a) → Π' P

Π-sum : ∀ (A B : Set) → Set₁
Π-sum a b = Π' (prodPredicate a b)

Π-sum-left : ∀ {A : Set} (B : Set) → A → Π-sum A B
Π-sum-left _ a = Π'_intro (\_ f _ → f a)

Π-sum-right : ∀ {A : Set} (B : Set) → B → Π-sum A B
Π-sum-right _ b = Π'_intro (\_ _ g → g b)

Π-sum-elim : ∀ {A B R : Set} → (A → R) → (B → R) → Π-sum A B → R
Π-sum-elim f g (Π'_intro elim) = elim _ f g

-----------------------------------------------------
-- Extra: Tuples using Π types
-----------------------------------------------------
Π-pair : ∀ (A B : Set) → Set
Π-pair a b = Π (bool a b)

Π-mkPair : ∀ {A B : Set} → A → B → Π-pair A B
Π-mkPair a b = Π_intro f
    where
    f : (b : Bool) → bool _ _ b
    f true = a
    f false = b

Π-fst : ∀ {A B : Set} → Π-pair A B → A
Π-fst (Π_intro f) = f true

Π-snd : ∀ {A B : Set} → Π-pair A B → B
Π-snd (Π_intro f) = f false

---
-- ??
--

data Σ' {a b} {A : Set a} (P : A → Set b) : Set (a ⊔ b) where
    Σ'_intro : ∀ (a : A) → P a → Σ' P

id : ∀ {A : Set} → A → A
id a = a

x : ∀ (A : Set) → Set1
x a = Σ (\(b : Set1) → (a → b))

mk : ∀ (A B : Set) → A → x A B
mk _ b a' = Σ'_intro b (\f g → f (g a'))

elim : {A B : Set} → (A → B) → x A B → B
elim f (Σ'_intro _ g) = g id f

 -- : ∀ {A : Set} (B : Set) → A → Π-sum A B
--Π-sum-left _ a = Π'_intro (\_ f _ → f a)
--
--Π-sum-right : ∀ {A : Set} (B : Set) → B → Π-sum A B
--Π-sum-right _ b = Π'_intro (\_ _ g → g b)
--
--Π-sum-elim : ∀ {A B R : Set} → (A → R) → (B → R) → Π-sum A B → R
--Π-sum-elim f g (Π'_intro elim) = elim _ f g


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Leftunit
open import Oscar.Class.Reflexivity
open import Oscar.Class.Transitivity

module Oscar.Class.Transrightidentity where

module Transrightidentity
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ)
  (ε : Reflexivity.type _∼_)
  (transitivity : Transitivity.type _∼_)
  = ℭLASS (_∼_ ,, (λ {x y} → _∼̇_ {x} {y}) ,, (λ {x} → ε {x}) ,, (λ {x y z} → transitivity {x} {y} {z}))
          (∀ {x y} {f : x ∼ y} → Leftunit.type _∼̇_ ε transitivity f)

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  {ℓ} {_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ}
  {ε : Reflexivity.type _∼_}
  {transitivity : Transitivity.type _∼_}
  where
  transrightidentity = Transrightidentity.method _∼_ _∼̇_ ε transitivity
  instance
    toLeftunitFromTransrightidentity :
      ⦃ _ : Transrightidentity.class _∼_ _∼̇_ ε transitivity ⦄
      → ∀ {x y} {f : x ∼ y} → Leftunit.class _∼̇_ ε transitivity f
    toLeftunitFromTransrightidentity .⋆ = transrightidentity

module Transrightidentity!
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ)
  ⦃ _ : Reflexivity.class _∼_ ⦄
  ⦃ _ : Transitivity.class _∼_ ⦄
  = Transrightidentity (_∼_) (_∼̇_) reflexivity transitivity


text:
module Types where

import Level
open import Data.Unit as Unit renaming (tt to ∗)
open import Data.List as List
open import Data.Product
open import Categories.Category using (Category)
open import Function

open import Relation.Binary.PropositionalEquality as PE hiding ([_]; subst)
open import Relation.Binary using (module IsEquivalence; Setoid; module Setoid)
open ≡-Reasoning

open import Common.Context as Context
-- open import Categories.Object.BinaryCoproducts ctx-cat

-- Codes
mutual
  data TermCtxCode : Set where
    emptyC : TermCtxCode
    cCtxC : (γ : TermCtxCode) → TypeCode γ → TermCtxCode

  TyCtxCode : Set

  data TypeCode (δ : TyCtxCode) (γ : TermCtxCode) : Set where
    closeAppTyC : TypeCode δ γ

  data TyFormerCode (γ : TermCtxCode) : Set where
    univ : TyFormerCode γ
    abs : (A : TypeCode γ) → (TyFormerCode (cCtxC γ A)) → TyFormerCode γ

  TyCtxCode = Ctx (Σ TermCtxCode TyFormerCode)
  TyVarCode : TyCtxCode → {γ : TermCtxCode} → TyFormerCode γ → Set
  TyVarCode δ {γ} T = Var δ (γ , T)
  emptyTy : TyCtxCode
  emptyTy = []

  {-
  ctxTyFormer : (γ : TermCtxCode) → TyFormerCode γ → TyFormerCode emptyC
  ctxTyFormer = ?
  -}

  data AppTypeCode (δ : TyCtxCode) (γ : TermCtxCode) : Set where
    varC  : (T : TyFormerCode γ) → (x : TyVarCode δ T) → AppTypeCode δ γ
    appTyC : (T : TyFormerCode γ) → AppTypeCode δ γ T
    μC : (γ₁ : TermCtxCode) → (t : TypeCode (ctxTyFormer γ univ ∷ δ) γ₁)
         → AppTypeCode δ γ

  {- (T : TyFormerCode) → (A : TypeCode δ γ univ)
            → (B : TypeCode δ γ (cCtxC γ A T)) → (t : TermCode γ A)
            → Type Δ Γ (subst B t) -}
    {-
    -- Just one constructor/destructor for now
    μ    : (Γ Γ₁ : TermCtx) → (t : Type (ctxTyFormer Γ univ ∷ Δ) Γ₁ univ)
         → Type Δ Γ (ctxTyFormer Γ univ)
    ν    : (Γ Γ₁ : TermCtx) → (t : Type (ctxTyFormer Γ univ ∷ Δ) Γ₁ univ)
         → Type Δ Γ (ctxTyFormer Γ univ)
  -}
{-

mutual
  data TermCtx : Set where
    empty : TermCtx
    cCtx : (Γ : TermCtx) → TypeCode Γ → TermCtx

  data TypeCode (Γ : TermCtx) : Set where
    appTy : TypeCode Γ

  Type : (Γ : TermCtx) → TypeCode Γ → Set

  data Term : (Γ : TermCtx) → TypeCode Γ → Set where

  data TyFormer (Γ : TermCtx) : Set where
    univ : TyFormer Γ
    abs : (A : TypeCode Γ) → (TyFormer (cCtx Γ A)) → TyFormer Γ

  subst : {Γ : TermCtx} → {A : TypeCode Γ}
          → TyFormer (cCtx Γ A) → Term Γ A → TyFormer Γ

  subst = {!!}

  Type Γ appTy = Σ (TypeCode Γ) (λ A →
                 Σ (AppType emptyTy Γ (abs A univ)) (λ B →
                 Term Γ A))

  ctxTyFormer : (Γ : TermCtx) → TyFormer Γ → TyFormer
  ctxTyFormer empty T = T
  ctxTyFormer (cCtx Γ A) T = ctxTyFormer Γ (abs Γ A)

  TyCtx : Set
  TyCtx = Ctx (Σ TermCtx TyFormer)
  TyVar : TyCtx → {Γ : TermCtx} → TyFormer Γ → Set
  TyVar Δ {Γ} T = Var Δ (Γ , T)
  emptyTy : TyCtx
  emptyTy = []

  -- | Type syntax
  data AppType (Δ : TyCtx) : (Γ : TermCtx) → TyFormer Γ → Set where
    var  : (Γ : TermCtx) → (T : TyFormer Γ) → (x : TyVar Δ T) → AppType Δ Γ T
    appTy : (Γ : TermCtx) → (T : TyFormer) → (A : Type Δ Γ univ)
            → (B : Type Δ Γ (cCtx Γ A T)) → (t : Term Γ)
            → Type Δ Γ (subst B t)
    -- Just one constructor/destructor for now
    μ    : (Γ Γ₁ : TermCtx) → (t : Type (ctxTyFormer Γ univ ∷ Δ) Γ₁ univ)
         → Type Δ Γ (ctxTyFormer Γ univ)
    ν    : (Γ Γ₁ : TermCtx) → (t : Type (ctxTyFormer Γ univ ∷ Δ) Γ₁ univ)
         → Type Δ Γ (ctxTyFormer Γ univ)
-}

{-
succ' : ∀{Δ} (x : TyVar Δ) → TyVar (∗ ∷ Δ)
succ' = Context.succ ∗
-}

{-
-- | Congruence for types
data _≅T_  {Γ Γ' : Ctx} : Type Γ → Type Γ' → Set where
  unit : unit ≅T unit
  var  : ∀{x : TyVar Γ} {x' : TyVar Γ'} → (x ≅V x') → var x ≅T var x'
  _⊕_  : ∀{t₁ t₂ : Type Γ} {t₁' t₂' : Type Γ'} →
         (t₁ ≅T t₁') → (t₂ ≅T t₂') →
         (t₁ ⊕ t₂) ≅T (t₁' ⊕ t₂')
  _⊗_  : ∀{t₁ t₂ : Type Γ} {t₁' t₂' : Type Γ'} →
         (t₁ ≅T t₁') → (t₂ ≅T t₂') →
         (t₁ ⊗ t₂) ≅T (t₁' ⊗ t₂')
  μ    : ∀{t : Type (∗ ∷ Γ)} {t' : Type (∗ ∷ Γ')} →
         (t ≅T t') →
         (μ t) ≅T (μ t')
  _⇒_  : ∀{t₁ t₁' : Type []} {t₂ : Type Γ} {t₂' : Type Γ'} →
         (t₁ ≅T t₁') → (t₂ ≅T t₂') →
         (t₁ ⇒ t₂) ≅T (t₁' ⇒ t₂')
  ν    : ∀{t : Type (∗ ∷ Γ)} {t' : Type (∗ ∷ Γ')} →
         (t ≅T t') →
         (ν t) ≅T (ν t')

Trefl : ∀ {Γ : Ctx} {t : Type Γ} → t ≅T t
Trefl {t = unit}    = unit
Trefl {t = var x}   = var e.refl
  where
    module s = Setoid
    module e = IsEquivalence (s.isEquivalence ≅V-setoid)
Trefl {t = t₁ ⊕ t₂} = Trefl ⊕ Trefl
Trefl {t = μ t}     = μ Trefl
Trefl {t = t ⊗ t₁}  = Trefl ⊗ Trefl
Trefl {t = t ⇒ t₁}  = Trefl ⇒ Trefl
Trefl {t = ν t}     = ν Trefl

Tsym : ∀ {Γ Γ' : Ctx} {t : Type Γ} {t' : Type Γ'} → t ≅T t' → t' ≅T t
Tsym unit      = unit
Tsym (var u)   = var (Vsym u)
Tsym (u₁ ⊕ u₂) = Tsym u₁ ⊕ Tsym u₂
Tsym (u₁ ⊗ u₂) = Tsym u₁ ⊗ Tsym u₂
Tsym (μ u)     = μ (Tsym u)
Tsym (u₁ ⇒ u₂) = Tsym u₁ ⇒ Tsym u₂
Tsym (ν u)     = ν (Tsym u)

Ttrans : ∀ {Γ₁ Γ₂ Γ₃ : Ctx} {t₁ : Type Γ₁} {t₂ : Type Γ₂} {t₃ : Type Γ₃} →
         t₁ ≅T t₂ → t₂ ≅T t₃ → t₁ ≅T t₃
Ttrans unit unit           = unit
Ttrans (var u₁) (var u₂)   = var (Vtrans u₁ u₂)
Ttrans (u₁ ⊕ u₂) (u₃ ⊕ u₄) = Ttrans u₁ u₃ ⊕ Ttrans u₂ u₄
Ttrans (u₁ ⊗ u₂) (u₃ ⊗ u₄) = Ttrans u₁ u₃ ⊗ Ttrans u₂ u₄
Ttrans (μ u₁) (μ u₂)       = μ (Ttrans u₁ u₂)
Ttrans (u₁ ⇒ u₂) (u₃ ⇒ u₄) = Ttrans u₁ u₃ ⇒ Ttrans u₂ u₄
Ttrans (ν u₁) (ν u₂)       = ν (Ttrans u₁ u₂)

≡→≅T : ∀ {Γ : Ctx} {t₁ t₂ : Type Γ} →
       t₁ ≡ t₂ → t₁ ≅T t₂
≡→≅T {Γ} {t₁} {.t₁} refl = Trefl

-- Note: makes the equality homogeneous in Γ
≅T-setoid : ∀ {Γ} → Setoid _ _
≅T-setoid {Γ} = record
  { Carrier = Type Γ
  ; _≈_ = _≅T_
  ; isEquivalence = record
    { refl = Trefl ; sym = Tsym ; trans = Ttrans }
  }

-- | Ground type
GType = Type []
unit′ : GType
unit′ = unit

-- | Variable renaming in types
rename : {Γ Δ : TyCtx} → (ρ : Γ ▹ Δ) → Type Γ → Type Δ
rename         ρ unit      = unit
rename         ρ (var x)   = var (ρ ∗ x)
rename         ρ (t₁ ⊕ t₂) = rename ρ t₁ ⊕ rename ρ t₂
rename {Γ} {Δ} ρ (μ t)     = μ (rename ρ' t)
  where
    ρ' : (∗ ∷ Γ) ▹ (∗ ∷ Δ)
    ρ' = ctx-id {[ ∗ ]} ⧻ ρ
rename         ρ (t₁ ⊗ t₂) = rename ρ t₁ ⊗ rename ρ t₂
rename         ρ (t₁ ⇒ t₂) = t₁ ⇒ rename ρ t₂
rename {Γ} {Δ} ρ (ν t)     = ν (rename ρ' t)
  where
    ρ' : (∗ ∷ Γ) ▹ (∗ ∷ Δ)
    ρ' = ctx-id {[ ∗ ]} ⧻ ρ

-------------------------
---- Generating structure on contexts (derived from renaming)

weaken : {Γ : TyCtx} (Δ : TyCtx) → Type Γ -> Type (Δ ∐ Γ)
weaken {Γ} Δ = rename {Γ} {Δ ∐ Γ} (i₂ {Δ} {Γ})

exchange : (Γ Δ : TyCtx) → Type (Γ ∐ Δ) -> Type (Δ ∐ Γ)
exchange Γ Δ = rename [ i₂ {Δ} {Γ} , i₁ {Δ} {Γ} ]

contract : {Γ : TyCtx} → Type (Γ ∐ Γ) -> Type Γ
contract = rename [ ctx-id , ctx-id ]

-- weaken-id-empty-ctx : (Δ : TyCtx) (t : GType) → weaken {[]} Δ t ≡ t
-- weaken-id-empty-ctx = ?

Subst : TyCtx → TyCtx → Set
Subst Γ Δ = TyVar Γ → Type Δ

id-subst : ∀{Γ : TyCtx} → Subst Γ Γ
id-subst x = var x

update : ∀{Γ Δ : TyCtx} → Subst Γ Δ → Type Δ → (Subst (∗ ∷ Γ) Δ)
update σ a zero        = a
update σ _ (succ′ _ x) = σ x

single-subst : ∀{Γ : TyCtx} → Type Γ → (Subst (∗ ∷ Γ) Γ)
single-subst a zero        = a
single-subst _ (succ′ _ x) = var x

lift : ∀{Γ Δ} → Subst Γ Δ → Subst (∗ ∷ Γ) (∗ ∷ Δ)
lift σ = update (weaken [ ∗ ] ∘ σ) (var zero)

-- | Simultaneous substitution
subst : {Γ Δ : TyCtx} → (σ : Subst Γ Δ) → Type Γ → Type Δ
subst         σ unit      = unit
subst         σ (var x)   = σ x
subst         σ (t₁ ⊕ t₂) = subst σ t₁ ⊕ subst σ t₂
subst {Γ} {Δ} σ (μ t)     = μ (subst (lift σ) t)
subst         σ (t₁ ⊗ t₂) = subst σ t₁ ⊗ subst σ t₂
subst         σ (t₁ ⇒ t₂) = t₁ ⇒ subst σ t₂
subst {Γ} {Δ} σ (ν t)     = ν (subst (lift σ) t)

subst₀ : {Γ : TyCtx} → Type Γ → Type (∗ ∷ Γ) → Type Γ
subst₀ {Γ} a = subst (update id-subst a)

rename′ : {Γ Δ : TyCtx} → (ρ : Γ ▹ Δ) → Type Γ → Type Δ
rename′ ρ = subst (var ∘ (ρ ∗))

-- | Unfold lfp
unfold-μ : (Type [ ∗ ]) → GType
unfold-μ a = subst₀ (μ a) a

-- | Unfold gfp
unfold-ν : (Type [ ∗ ]) → GType
unfold-ν a = subst₀ (ν a) a

--------------------------------------------------
---- Examples

Nat : Type []
Nat = μ (unit ⊕ x)
  where x = var zero

Str-Fun : {Γ : TyCtx} → Type Γ → Type (∗ ∷ Γ)
Str-Fun a = (weaken [ ∗ ] a ⊗ x)
  where x = var zero

Str : {Γ : TyCtx} → Type Γ → Type Γ
Str a = ν (Str-Fun a)

lemma : ∀ {Γ : Ctx} {a b : Type Γ} {σ : Subst Γ Γ} →
        subst (update σ b) (weaken [ ∗ ] a) ≅T subst σ a
lemma {a = unit}    = unit
lemma {a = var x}   = Trefl
lemma {a = a₁ ⊕ a₂} = lemma {a = a₁} ⊕ lemma {a = a₂}
lemma {a = μ a}     = μ {!!}
lemma {a = a₁ ⊗ a₂} = lemma {a = a₁} ⊗ lemma {a = a₂}
lemma {a = a₁ ⇒ a₂} = Trefl ⇒ lemma {a = a₂}
lemma {a = ν a}     = ν {!!}

lift-id-is-id-ext : ∀ {Γ : Ctx} (x : TyVar (∗ ∷ Γ)) →
                    (lift (id-subst {Γ})) x ≡ id-subst x
lift-id-is-id-ext zero        = refl
lift-id-is-id-ext (succ′ ∗ x) = refl

lift-id-is-id : ∀ {Γ : Ctx} → lift (id-subst {Γ}) ≡ id-subst
lift-id-is-id = η-≡ lift-id-is-id-ext

id-subst-id : ∀ {Γ : Ctx} {a : Type Γ} →
              subst id-subst a ≅T a
id-subst-id {a = unit}   = unit
id-subst-id {a = var x}  = var Vrefl
id-subst-id {a = a ⊕ a₁} = id-subst-id ⊕ id-subst-id
id-subst-id {a = μ a}    =
  μ (Ttrans (≡→≅T (cong (λ u → subst u a) lift-id-is-id)) id-subst-id)
id-subst-id {a = a ⊗ a₁} = id-subst-id ⊗ id-subst-id
id-subst-id {a = a ⇒ a₁} = Trefl ⇒ id-subst-id
id-subst-id {a = ν a}    =
  ν (Ttrans (≡→≅T (cong (λ u → subst u a) lift-id-is-id)) id-subst-id)

lemma₂ : ∀ {Γ : Ctx} {a b : Type Γ} →
        subst (update id-subst b) (weaken [ ∗ ] a) ≅T a
lemma₂ {Γ} {a} {b} = Ttrans (lemma {Γ} {a} {b} {σ = id-subst}) id-subst-id

unfold-str : ∀{a : Type []} → (unfold-ν (Str-Fun a)) ≅T (a ⊗ Str a)
unfold-str {a} = lemma₂ ⊗ Trefl

LFair : {Γ : TyCtx} → Type Γ → Type Γ → Type Γ
LFair a b = ν (μ ((w a ⊗ x) ⊕ (w b ⊗ y)))
  where
    x = var zero
    y = var (succ zero)
    Δ = ∗ ∷ [ ∗ ]
    w = weaken Δ
-}