text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.DiffInt.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Data.DiffInt.Base
open import Cubical.Data.Nat as ℕ using (suc; zero; isSetℕ; discreteℕ; ℕ) renaming (_+_ to _+ⁿ_; _·_ to _·ⁿ_)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool

open import Cubical.Data.Int as Int using (Int; sucInt)
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism

open import Cubical.Relation.Binary.Base
open import Cubical.Relation.Nullary

open import Cubical.HITs.SetQuotients

open BinaryRelation

relIsEquiv : isEquivRel rel
relIsEquiv = equivRel {A = ℕ × ℕ} relIsRefl relIsSym relIsTrans
  where
    open import Cubical.Data.Nat
    relIsRefl : isRefl rel
    relIsRefl (a0 , a1) = refl

    relIsSym : isSym rel
    relIsSym (a0 , a1) (b0 , b1) p = sym p

    relIsTrans : isTrans rel
    relIsTrans (a0 , a1) (b0 , b1) (c0 , c1) p0 p1 =
      inj-m+ {m = (b0 + b1)} ((b0 + b1) + (a0 + c1) ≡⟨ +-assoc (b0 + b1) a0 c1  ⟩
            ((b0 + b1) + a0) + c1 ≡[ i ]⟨ +-comm b0 b1 i + a0   + c1 ⟩
            ((b1 + b0) + a0) + c1 ≡[ i ]⟨ +-comm (b1 + b0) a0 i + c1 ⟩
            (a0 + (b1 + b0)) + c1 ≡[ i ]⟨ +-assoc a0 b1 b0 i    + c1 ⟩
            (a0 + b1) + b0 + c1 ≡⟨ sym (+-assoc (a0 + b1) b0 c1) ⟩
            (a0 + b1) + (b0 + c1) ≡⟨ cong (λ p → p . fst + p .snd) (transport ΣPath≡PathΣ (p0 , p1))⟩
            (b0 + a1) + (c0 + b1) ≡⟨ sym (+-assoc b0 a1 (c0 + b1))⟩
            b0 + (a1 + (c0 + b1)) ≡[ i ]⟨ b0 + (a1 + +-comm c0 b1 i) ⟩
            b0 + (a1 + (b1 + c0)) ≡[ i ]⟨ b0 + +-comm a1 (b1 + c0) i ⟩
            b0 + ((b1 + c0) + a1) ≡[ i ]⟨ b0 + +-assoc b1 c0 a1 (~ i) ⟩
            b0 + (b1 + (c0 + a1)) ≡⟨ +-assoc b0 b1 (c0 + a1)⟩
            (b0 + b1) + (c0 + a1) ∎ )

relIsProp : BinaryRelation.isPropValued rel
relIsProp a b x y = isSetℕ _ _ _ _

discreteℤ : Discrete ℤ
discreteℤ = discreteSetQuotients (discreteΣ discreteℕ λ _ → discreteℕ) relIsProp relIsEquiv (λ _ _ → discreteℕ _ _)

isSetℤ : isSet ℤ
isSetℤ = Discrete→isSet discreteℤ

sucℤ' : ℕ × ℕ -> ℤ
sucℤ' (a⁺ , a⁻) = [ suc a⁺ , a⁻ ]

sucℤ'-respects-rel : (a b : ℕ × ℕ) → rel a b → sucℤ' a ≡ sucℤ' b
sucℤ'-respects-rel a@(a⁺ , a⁻) b@(b⁺ , b⁻) a~b = eq/ (suc a⁺ , a⁻) (suc b⁺ , b⁻) λ i → suc (a~b i)

sucℤ : ℤ -> ℤ
sucℤ = elim {R = rel} {B = λ _ → ℤ} (λ _ → isSetℤ) sucℤ' sucℤ'-respects-rel

predℤ' : ℕ × ℕ -> ℤ
predℤ' (a⁺ , a⁻) = [ a⁺ , suc a⁻ ]

⟦_⟧ : Int -> ℤ
⟦_⟧ (Int.pos n) = [ n , 0 ]
⟦_⟧ (Int.negsuc n) = [ 0 , suc n ]

fwd = ⟦_⟧

bwd' : ℕ × ℕ -> Int
bwd' (zero   , a⁻) = Int.neg a⁻
bwd' (suc a⁺ , a⁻) = sucInt (bwd' (a⁺ , a⁻))

rel-suc : ∀ a⁺ a⁻ → rel (a⁺ , a⁻) (suc a⁺ , suc a⁻)
rel-suc a⁺ a⁻ = ℕ.+-suc a⁺ a⁻

bwd'-suc : ∀ a⁺ a⁻ → bwd' (a⁺ , a⁻) ≡ bwd' (suc a⁺ , suc a⁻)
bwd'-suc zero zero = refl
bwd'-suc zero (suc a⁻) = refl
bwd'-suc (suc a⁺) a⁻ i = sucInt (bwd'-suc a⁺ a⁻ i)

bwd'+ : ∀ m n → bwd' (m , m +ⁿ n) ≡ bwd' (0 , n)
bwd'+ zero n = refl
bwd'+ (suc m) n = sym (bwd'-suc m (m +ⁿ n)) ∙ bwd'+ m n

bwd'-respects-rel : (a b : ℕ × ℕ) → rel a b → bwd' a ≡ bwd' b
bwd'-respects-rel (zero   , a⁻) (    b⁺ , b⁻) a~b = sym (bwd'+ b⁺ a⁻) ∙ (λ i → bwd' (b⁺ , a~b (~ i)))
bwd'-respects-rel (suc a⁺ , a⁻) (zero   , b⁻) a~b = (λ i → bwd' (suc a⁺ , a~b (~ i))) ∙ sym (bwd'-suc a⁺ (a⁺ +ⁿ b⁻)) ∙ bwd'+ a⁺ b⁻
bwd'-respects-rel (suc a⁺ , a⁻) (suc b⁺ , b⁻) a~b i = sucInt (bwd'-respects-rel (a⁺ , a⁻) (b⁺ , b⁻) (ℕ.inj-m+ {1} {a⁺ +ⁿ b⁻} {b⁺ +ⁿ a⁻} a~b) i)

bwd : ℤ -> Int
bwd = elim {R = rel} {B = λ _ → Int} (λ _ → Int.isSetInt) bwd' bwd'-respects-rel

bwd-fwd : ∀ (x : Int) -> bwd (fwd x) ≡ x
bwd-fwd (Int.pos zero) = refl
bwd-fwd (Int.pos (suc n)) i = sucInt (bwd-fwd (Int.pos n) i)
bwd-fwd (Int.negsuc n) = refl

suc-⟦⟧ : ∀ x → sucℤ ⟦ x ⟧ ≡ ⟦ sucInt x ⟧
suc-⟦⟧ (Int.pos n) = refl
suc-⟦⟧ (Int.negsuc zero) = eq/ {R = rel} (1 , 1) (0 , 0) refl
suc-⟦⟧ (Int.negsuc (suc n)) = eq/ {R = rel} (1 , 2 +ⁿ n) (0 , 1 +ⁿ n) refl

fwd-bwd' : (a : ℕ × ℕ) → fwd (bwd [ a ]) ≡ [ a ]
fwd-bwd' a@(zero , zero) = refl
fwd-bwd' a@(zero , suc a⁻) = refl
fwd-bwd' a@(suc a⁺ , a⁻) = sym (suc-⟦⟧ (bwd [ a⁺ , a⁻ ])) ∙ (λ i → sucℤ (fwd-bwd' (a⁺ , a⁻) i))

fwd-bwd : ∀ (z : ℤ) -> fwd (bwd z) ≡ z
fwd-bwd = elimProp {R = rel} (λ _  → isSetℤ _ _) fwd-bwd'

Int≡ℤ : Int ≡ ℤ
Int≡ℤ = isoToPath (iso fwd bwd fwd-bwd bwd-fwd)

infix  8 -_
infixl 7 _·_
infixl 6 _+_

_+'_ : (a b : ℕ × ℕ) → ℤ
(a⁺ , a⁻) +' (b⁺ , b⁻) = [ a⁺ +ⁿ b⁺ , a⁻ +ⁿ b⁻ ]

private
  commˡⁿ : ∀ a b c → a +ⁿ b +ⁿ c ≡ a +ⁿ c +ⁿ b
  commˡⁿ a b c = sym (ℕ.+-assoc a b c) ∙ (λ i → a +ⁿ ℕ.+-comm b c i) ∙ ℕ.+-assoc a c b

  lem0 : ∀ a b c d → (a +ⁿ b) +ⁿ (c +ⁿ d) ≡ (a +ⁿ c) +ⁿ (b +ⁿ d)
  lem0 a b c d = ℕ.+-assoc (a +ⁿ b) c d ∙ (λ i → commˡⁿ a b c i +ⁿ d) ∙ sym (ℕ.+-assoc (a +ⁿ c) b d)

+ⁿ-creates-rel-≡ : ∀ a⁺ a⁻ x → _≡_ {A = ℤ} [ a⁺ , a⁻ ] [ a⁺ +ⁿ x , a⁻ +ⁿ x ]
+ⁿ-creates-rel-≡ a⁺ a⁻ x = eq/ (a⁺ , a⁻) (a⁺ +ⁿ x , a⁻ +ⁿ x) ((λ i → a⁺ +ⁿ ℕ.+-comm a⁻ x i) ∙ ℕ.+-assoc a⁺ x a⁻)

+-respects-relʳ : (a b c : ℕ × ℕ) → rel a b → (a +' c) ≡ (b +' c)
+-respects-relʳ a@(a⁺ , a⁻) b@(b⁺ , b⁻) c@(c⁺ , c⁻) p = eq/ {R = rel} (a⁺ +ⁿ c⁺ , a⁻ +ⁿ c⁻) (b⁺ +ⁿ c⁺ , b⁻ +ⁿ c⁻) (
  (a⁺ +ⁿ c⁺) +ⁿ (b⁻ +ⁿ c⁻) ≡⟨ lem0 a⁺ c⁺ b⁻ c⁻ ⟩
  (a⁺ +ⁿ b⁻) +ⁿ (c⁺ +ⁿ c⁻) ≡[ i ]⟨ p i +ⁿ (c⁺ +ⁿ c⁻) ⟩
  (b⁺ +ⁿ a⁻) +ⁿ (c⁺ +ⁿ c⁻) ≡⟨ sym (lem0 b⁺ c⁺ a⁻ c⁻) ⟩
  (b⁺ +ⁿ c⁺) +ⁿ (a⁻ +ⁿ c⁻) ∎)

+-respects-relˡ : (a b c : ℕ × ℕ) → rel b c → (a +' b) ≡ (a +' c)
+-respects-relˡ a@(a⁺ , a⁻) b@(b⁺ , b⁻) c@(c⁺ , c⁻) p = eq/ {R = rel} (a⁺ +ⁿ b⁺ , a⁻ +ⁿ b⁻) (a⁺ +ⁿ c⁺ , a⁻ +ⁿ c⁻) (
  (a⁺ +ⁿ b⁺) +ⁿ (a⁻ +ⁿ c⁻) ≡⟨ lem0 a⁺ b⁺ a⁻ c⁻ ⟩
  (a⁺ +ⁿ a⁻) +ⁿ (b⁺ +ⁿ c⁻) ≡[ i ]⟨ (a⁺ +ⁿ a⁻) +ⁿ p i ⟩
  (a⁺ +ⁿ a⁻) +ⁿ (c⁺ +ⁿ b⁻) ≡⟨ sym (lem0 a⁺ c⁺ a⁻ b⁻) ⟩
  (a⁺ +ⁿ c⁺) +ⁿ (a⁻ +ⁿ b⁻) ∎)

_+''_ : ℤ → ℤ → ℤ
_+''_ = rec2 {R = rel} {B = ℤ} φ _+'_ +-respects-relʳ +-respects-relˡ
  where abstract φ = isSetℤ

-- normalization of isSetℤ explodes. Therefore we wrap this with expanded cases
_+_ : ℤ → ℤ → ℤ
x@([ _ ])               + y@([ _ ])               = x +'' y
x@([ _ ])               + y@(eq/ _ _ _ _)         = x +'' y
x@(eq/ _ _ _ _)         + y@([ _ ])               = x +'' y
x@(eq/ _ _ _ _)         + y@(eq/ _ _ _ _)         = x +'' y
x@(eq/ _ _ _ _)         + y@(squash/ a b p q i j) = isSetℤ _ _ (cong (x +_) p) (cong (x +_) q) i j
x@([ _ ])               + y@(squash/ a b p q i j) = isSetℤ _ _ (cong (x +_) p) (cong (x +_) q) i j
x@(squash/ a b p q i j) + y                       = isSetℤ _ _ (cong (_+ y) p) (cong (_+ y) q) i j

-'_ : ℕ × ℕ → ℤ
-' (a⁺ , a⁻) = [ a⁻ , a⁺ ]

neg-respects-rel'-≡ : (a b : ℕ × ℕ) → rel a b → (-' a) ≡ (-' b)
neg-respects-rel'-≡ a@(a⁺ , a⁻) b@(b⁺ , b⁻) p = eq/ {R = rel} (a⁻ , a⁺) (b⁻ , b⁺) (ℕ.+-comm a⁻ b⁺ ∙ sym p ∙ ℕ.+-comm a⁺ b⁻)

-_ : ℤ → ℤ
-_ = rec {R = rel} {B = ℤ} isSetℤ -'_ neg-respects-rel'-≡

_·'_ : (a b : ℕ × ℕ) → ℤ
(a⁺ , a⁻) ·' (b⁺ , b⁻) = [ a⁺ ·ⁿ b⁺ +ⁿ a⁻ ·ⁿ b⁻ , a⁺ ·ⁿ b⁻ +ⁿ a⁻ ·ⁿ b⁺ ]

private
  lem1 : ∀ a b c d → (a +ⁿ b) +ⁿ (c +ⁿ d) ≡ (a +ⁿ d) +ⁿ (b +ⁿ c)
  lem1 a b c d = (λ i → (a +ⁿ b) +ⁿ ℕ.+-comm c d i) ∙ ℕ.+-assoc (a +ⁿ b) d c ∙ (λ i → commˡⁿ a b d i +ⁿ c) ∙ sym (ℕ.+-assoc (a +ⁿ d) b c)

·-respects-relʳ : (a b c : ℕ × ℕ) → rel a b → (a ·' c) ≡ (b ·' c)
·-respects-relʳ a@(a⁺ , a⁻) b@(b⁺ , b⁻) c@(c⁺ , c⁻) p = eq/ {R = rel} (a⁺ ·ⁿ c⁺ +ⁿ a⁻ ·ⁿ c⁻ , a⁺ ·ⁿ c⁻ +ⁿ a⁻ ·ⁿ c⁺) (b⁺ ·ⁿ c⁺ +ⁿ b⁻ ·ⁿ c⁻ , b⁺ ·ⁿ c⁻ +ⁿ b⁻ ·ⁿ c⁺) (
  (a⁺ ·ⁿ c⁺ +ⁿ a⁻ ·ⁿ c⁻) +ⁿ (b⁺ ·ⁿ c⁻ +ⁿ b⁻ ·ⁿ c⁺) ≡⟨ lem1 (a⁺ ·ⁿ c⁺) (a⁻ ·ⁿ c⁻) (b⁺ ·ⁿ c⁻) (b⁻ ·ⁿ c⁺) ⟩
  (a⁺ ·ⁿ c⁺ +ⁿ b⁻ ·ⁿ c⁺) +ⁿ (a⁻ ·ⁿ c⁻ +ⁿ b⁺ ·ⁿ c⁻) ≡[ i ]⟨ ℕ.·-distribʳ a⁺ b⁻ c⁺ i +ⁿ ℕ.·-distribʳ a⁻ b⁺ c⁻ i ⟩
  ((a⁺ +ⁿ b⁻) ·ⁿ c⁺) +ⁿ ((a⁻ +ⁿ b⁺) ·ⁿ c⁻)         ≡[ i ]⟨ p i ·ⁿ c⁺ +ⁿ (ℕ.+-comm a⁻ b⁺ ∙ sym p ∙ ℕ.+-comm a⁺ b⁻) i ·ⁿ c⁻ ⟩
  ((b⁺ +ⁿ a⁻) ·ⁿ c⁺) +ⁿ ((b⁻ +ⁿ a⁺) ·ⁿ c⁻)         ≡[ i ]⟨ ℕ.·-distribʳ b⁺ a⁻ c⁺ (~ i) +ⁿ ℕ.·-distribʳ b⁻ a⁺ c⁻ (~ i) ⟩
  (b⁺ ·ⁿ c⁺ +ⁿ a⁻ ·ⁿ c⁺) +ⁿ (b⁻ ·ⁿ c⁻ +ⁿ a⁺ ·ⁿ c⁻) ≡⟨ sym (lem1 (b⁺ ·ⁿ c⁺) (b⁻ ·ⁿ c⁻) (a⁺ ·ⁿ c⁻) (a⁻ ·ⁿ c⁺)) ⟩
  (b⁺ ·ⁿ c⁺ +ⁿ b⁻ ·ⁿ c⁻) +ⁿ (a⁺ ·ⁿ c⁻ +ⁿ a⁻ ·ⁿ c⁺) ∎)

·-respects-relˡ : (a b c : ℕ × ℕ) → rel b c → (a ·' b) ≡ (a ·' c)
·-respects-relˡ a@(a⁺ , a⁻) b@(b⁺ , b⁻) c@(c⁺ , c⁻) p = eq/ {R = rel} (a⁺ ·ⁿ b⁺ +ⁿ a⁻ ·ⁿ b⁻ , a⁺ ·ⁿ b⁻ +ⁿ a⁻ ·ⁿ b⁺) (a⁺ ·ⁿ c⁺ +ⁿ a⁻ ·ⁿ c⁻ , a⁺ ·ⁿ c⁻ +ⁿ a⁻ ·ⁿ c⁺) (
  (a⁺ ·ⁿ b⁺ +ⁿ a⁻ ·ⁿ b⁻) +ⁿ (a⁺ ·ⁿ c⁻ +ⁿ a⁻ ·ⁿ c⁺) ≡⟨ lem0 (a⁺ ·ⁿ b⁺) (a⁻ ·ⁿ b⁻) (a⁺ ·ⁿ c⁻) (a⁻ ·ⁿ c⁺) ⟩
  (a⁺ ·ⁿ b⁺ +ⁿ a⁺ ·ⁿ c⁻) +ⁿ (a⁻ ·ⁿ b⁻ +ⁿ a⁻ ·ⁿ c⁺) ≡[ i ]⟨ ℕ.·-distribˡ a⁺ b⁺ c⁻ i +ⁿ ℕ.·-distribˡ a⁻ b⁻ c⁺ i ⟩
  (a⁺ ·ⁿ (b⁺ +ⁿ c⁻)) +ⁿ (a⁻ ·ⁿ (b⁻ +ⁿ c⁺))         ≡[ i ]⟨ a⁺ ·ⁿ p i +ⁿ a⁻ ·ⁿ (ℕ.+-comm b⁻ c⁺ ∙ sym p ∙ ℕ.+-comm b⁺ c⁻) i ⟩
  (a⁺ ·ⁿ (c⁺ +ⁿ b⁻)) +ⁿ (a⁻ ·ⁿ (c⁻ +ⁿ b⁺))         ≡[ i ]⟨ ℕ.·-distribˡ a⁺ c⁺ b⁻ (~ i) +ⁿ ℕ.·-distribˡ a⁻ c⁻ b⁺ (~ i) ⟩
  (a⁺ ·ⁿ c⁺ +ⁿ a⁺ ·ⁿ b⁻) +ⁿ (a⁻ ·ⁿ c⁻ +ⁿ a⁻ ·ⁿ b⁺) ≡⟨ sym (lem0 (a⁺ ·ⁿ c⁺) (a⁻ ·ⁿ c⁻) (a⁺ ·ⁿ b⁻) (a⁻ ·ⁿ b⁺)) ⟩
  (a⁺ ·ⁿ c⁺ +ⁿ a⁻ ·ⁿ c⁻) +ⁿ (a⁺ ·ⁿ b⁻ +ⁿ a⁻ ·ⁿ b⁺) ∎)

_·''_ : ℤ → ℤ → ℤ
_·''_ = rec2 {R = rel} {B = ℤ} isSetℤ _·'_ ·-respects-relʳ ·-respects-relˡ

-- normalization of isSetℤ explodes. Therefore we wrap this with expanded cases
_·_ : ℤ → ℤ → ℤ
x@([ _ ])               · y@([ _ ])               = x ·'' y
x@([ _ ])               · y@(eq/ _ _ _ _)         = x ·'' y
x@(eq/ _ _ _ _)         · y@([ _ ])               = x ·'' y
x@(eq/ _ _ _ _)         · y@(eq/ _ _ _ _)         = x ·'' y
x@(eq/ _ _ _ _)         · y@(squash/ a b p q i j) = isSetℤ _ _ (cong (x ·_) p) (cong (x ·_) q) i j
x@([ _ ])               · y@(squash/ a b p q i j) = isSetℤ _ _ (cong (x ·_) p) (cong (x ·_) q) i j
x@(squash/ a b p q i j) · y                       = isSetℤ _ _ (cong (_· y) p) (cong (_· y) q) i j

+-identityʳ : (x : ℤ) → x + 0 ≡ x
+-identityʳ = elimProp {R = rel} (λ _ → isSetℤ _ _)
  λ{ (a⁺ , a⁻) i → [ ℕ.+-comm a⁺ 0 i , ℕ.+-comm a⁻ 0 i ] }

+-comm : (x y : ℤ) → x + y ≡ y + x
+-comm = elimProp2 {R = rel} (λ _ _ → isSetℤ _ _)
  λ{ (a⁺ , a⁻) (b⁺ , b⁻) i → [ ℕ.+-comm a⁺ b⁺ i , ℕ.+-comm a⁻ b⁻ i ] }

+-inverseʳ : (x : ℤ) → x + (- x) ≡ 0
+-inverseʳ = elimProp {R = rel} (λ _ → isSetℤ _ _)
  λ{ (a⁺ , a⁻) → eq/ {R = rel} (a⁺ +ⁿ a⁻ , a⁻ +ⁿ a⁺) (0 , 0) (ℕ.+-zero (a⁺ +ⁿ a⁻) ∙ ℕ.+-comm a⁺ a⁻) }

+-assoc : (x y z : ℤ) → x + (y + z) ≡ x + y + z
+-assoc = elimProp3 {R = rel} (λ _ _ _ → isSetℤ _ _)
  λ{ (a⁺ , a⁻) (b⁺ , b⁻) (c⁺ , c⁻) i → [ ℕ.+-assoc a⁺ b⁺ c⁺ i , ℕ.+-assoc a⁻ b⁻ c⁻ i ] }

·-identityʳ : (x : ℤ) → x · 1 ≡ x
·-identityʳ = elimProp {R = rel} (λ _ → isSetℤ _ _) γ
  where
  γ : (a : ℕ × ℕ) → _
  γ (a⁺ , a⁻) i = [ p i , q i ]
    where
    p : a⁺ ·ⁿ 1 +ⁿ a⁻ ·ⁿ 0 ≡ a⁺
    p i = ℕ.+-comm (ℕ.·-identityʳ a⁺ i) (ℕ.0≡m·0 a⁻ (~ i)) i
    q : a⁺ ·ⁿ 0 +ⁿ a⁻ ·ⁿ 1 ≡ a⁻
    q i = ℕ.0≡m·0 a⁺ (~ i) +ⁿ ℕ.·-identityʳ a⁻ i

·-comm : (x y : ℤ) → x · y ≡ y · x
·-comm = elimProp2 {R = rel} (λ _ _ → isSetℤ _ _)
  λ{ (a⁺ , a⁻) (b⁺ , b⁻) i → [ ℕ.·-comm a⁺ b⁺ i +ⁿ ℕ.·-comm a⁻ b⁻ i , ℕ.+-comm (ℕ.·-comm a⁺ b⁻ i) (ℕ.·-comm a⁻ b⁺ i) i ] }

·-distribˡ : (x y z : ℤ) → x · (y + z) ≡ x · y + x · z
·-distribˡ = elimProp3 {R = rel} (λ _ _ _ → isSetℤ _ _)
  λ{ (a⁺ , a⁻) (b⁺ , b⁻) (c⁺ , c⁻) →
    [ a⁺ ·ⁿ (b⁺ +ⁿ c⁺) +ⁿ a⁻ ·ⁿ (b⁻ +ⁿ c⁻)
    , a⁺ ·ⁿ (b⁻ +ⁿ c⁻) +ⁿ a⁻ ·ⁿ (b⁺ +ⁿ c⁺)
    ] ≡[ i ]⟨ [ ℕ.·-distribˡ a⁺ b⁺ c⁺ (~ i) +ⁿ ℕ.·-distribˡ a⁻ b⁻ c⁻ (~ i) , ℕ.·-distribˡ a⁺ b⁻ c⁻ (~ i) +ⁿ ℕ.·-distribˡ a⁻ b⁺ c⁺ (~ i) ] ⟩
    [ (a⁺ ·ⁿ b⁺ +ⁿ a⁺ ·ⁿ c⁺) +ⁿ (a⁻ ·ⁿ b⁻ +ⁿ a⁻ ·ⁿ c⁻)
    , (a⁺ ·ⁿ b⁻ +ⁿ a⁺ ·ⁿ c⁻) +ⁿ (a⁻ ·ⁿ b⁺ +ⁿ a⁻ ·ⁿ c⁺)
    ] ≡[ i ]⟨ [ lem0 (a⁺ ·ⁿ b⁺) (a⁻ ·ⁿ b⁻) (a⁺ ·ⁿ c⁺) (a⁻ ·ⁿ c⁻) (~ i), lem0 (a⁺ ·ⁿ b⁻) (a⁺ ·ⁿ c⁻) (a⁻ ·ⁿ b⁺) (a⁻ ·ⁿ c⁺) i ] ⟩
    [ a⁺ ·ⁿ b⁺ +ⁿ a⁻ ·ⁿ b⁻ +ⁿ (a⁺ ·ⁿ c⁺ +ⁿ a⁻ ·ⁿ c⁻)
    , a⁺ ·ⁿ b⁻ +ⁿ a⁻ ·ⁿ b⁺ +ⁿ (a⁺ ·ⁿ c⁻ +ⁿ a⁻ ·ⁿ c⁺)
    ] ∎
   }

·-assoc : (x y z : ℤ) → x · (y · z) ≡ x · y · z
·-assoc = elimProp3 {R = rel} (λ _ _ _ → isSetℤ _ _)
  λ{ (a⁺ , a⁻) (b⁺ , b⁻) (c⁺ , c⁻) →
    [ a⁺ ·ⁿ (b⁺ ·ⁿ c⁺ +ⁿ b⁻ ·ⁿ c⁻) +ⁿ a⁻ ·ⁿ (b⁺ ·ⁿ c⁻ +ⁿ b⁻ ·ⁿ c⁺)
    , a⁺ ·ⁿ (b⁺ ·ⁿ c⁻ +ⁿ b⁻ ·ⁿ c⁺) +ⁿ a⁻ ·ⁿ (b⁺ ·ⁿ c⁺ +ⁿ b⁻ ·ⁿ c⁻)
    ] ≡[ i ]⟨ [ ℕ.·-distribˡ a⁺ (b⁺ ·ⁿ c⁺) (b⁻ ·ⁿ c⁻) (~ i) +ⁿ ℕ.·-distribˡ a⁻ (b⁺ ·ⁿ c⁻) (b⁻ ·ⁿ c⁺) (~ i)
              , ℕ.·-distribˡ a⁺ (b⁺ ·ⁿ c⁻) (b⁻ ·ⁿ c⁺) (~ i) +ⁿ ℕ.·-distribˡ a⁻ (b⁺ ·ⁿ c⁺) (b⁻ ·ⁿ c⁻) (~ i) ] ⟩
    [ (a⁺ ·ⁿ (b⁺ ·ⁿ c⁺) +ⁿ a⁺ ·ⁿ (b⁻ ·ⁿ c⁻)) +ⁿ (a⁻ ·ⁿ (b⁺ ·ⁿ c⁻) +ⁿ a⁻ ·ⁿ (b⁻ ·ⁿ c⁺))
    , (a⁺ ·ⁿ (b⁺ ·ⁿ c⁻) +ⁿ a⁺ ·ⁿ (b⁻ ·ⁿ c⁺)) +ⁿ (a⁻ ·ⁿ (b⁺ ·ⁿ c⁺) +ⁿ a⁻ ·ⁿ (b⁻ ·ⁿ c⁻))
    ] ≡[ i ]⟨ [ (ℕ.·-assoc a⁺ b⁺ c⁺ i +ⁿ ℕ.·-assoc a⁺ b⁻ c⁻ i) +ⁿ (ℕ.·-assoc a⁻ b⁺ c⁻ i +ⁿ ℕ.·-assoc a⁻ b⁻ c⁺ i)
              , (ℕ.·-assoc a⁺ b⁺ c⁻ i +ⁿ ℕ.·-assoc a⁺ b⁻ c⁺ i) +ⁿ (ℕ.·-assoc a⁻ b⁺ c⁺ i +ⁿ ℕ.·-assoc a⁻ b⁻ c⁻ i) ] ⟩
    [ (a⁺ ·ⁿ b⁺ ·ⁿ c⁺ +ⁿ a⁺ ·ⁿ b⁻ ·ⁿ c⁻) +ⁿ (a⁻ ·ⁿ b⁺ ·ⁿ c⁻ +ⁿ a⁻ ·ⁿ b⁻ ·ⁿ c⁺)
    , (a⁺ ·ⁿ b⁺ ·ⁿ c⁻ +ⁿ a⁺ ·ⁿ b⁻ ·ⁿ c⁺) +ⁿ (a⁻ ·ⁿ b⁺ ·ⁿ c⁺ +ⁿ a⁻ ·ⁿ b⁻ ·ⁿ c⁻)
    ] ≡[ i ]⟨ [ lem1 (a⁺ ·ⁿ b⁺ ·ⁿ c⁺) (a⁺ ·ⁿ b⁻ ·ⁿ c⁻) (a⁻ ·ⁿ b⁺ ·ⁿ c⁻) (a⁻ ·ⁿ b⁻ ·ⁿ c⁺) i
              , lem1 (a⁺ ·ⁿ b⁺ ·ⁿ c⁻) (a⁺ ·ⁿ b⁻ ·ⁿ c⁺) (a⁻ ·ⁿ b⁺ ·ⁿ c⁺) (a⁻ ·ⁿ b⁻ ·ⁿ c⁻) i ] ⟩
    [ (a⁺ ·ⁿ b⁺ ·ⁿ c⁺ +ⁿ a⁻ ·ⁿ b⁻ ·ⁿ c⁺) +ⁿ (a⁺ ·ⁿ b⁻ ·ⁿ c⁻ +ⁿ a⁻ ·ⁿ b⁺ ·ⁿ c⁻)
    , (a⁺ ·ⁿ b⁺ ·ⁿ c⁻ +ⁿ a⁻ ·ⁿ b⁻ ·ⁿ c⁻) +ⁿ (a⁺ ·ⁿ b⁻ ·ⁿ c⁺ +ⁿ a⁻ ·ⁿ b⁺ ·ⁿ c⁺)
    ] ≡[ i ]⟨ [ ℕ.·-distribʳ (a⁺ ·ⁿ b⁺) (a⁻ ·ⁿ b⁻) c⁺ i +ⁿ ℕ.·-distribʳ (a⁺ ·ⁿ b⁻) (a⁻ ·ⁿ b⁺) c⁻ i
              , ℕ.·-distribʳ (a⁺ ·ⁿ b⁺) (a⁻ ·ⁿ b⁻) c⁻ i +ⁿ ℕ.·-distribʳ (a⁺ ·ⁿ b⁻) (a⁻ ·ⁿ b⁺) c⁺ i ] ⟩
    [ (a⁺ ·ⁿ b⁺ +ⁿ a⁻ ·ⁿ b⁻) ·ⁿ c⁺ +ⁿ (a⁺ ·ⁿ b⁻ +ⁿ a⁻ ·ⁿ b⁺) ·ⁿ c⁻
    , (a⁺ ·ⁿ b⁺ +ⁿ a⁻ ·ⁿ b⁻) ·ⁿ c⁻ +ⁿ (a⁺ ·ⁿ b⁻ +ⁿ a⁻ ·ⁿ b⁺) ·ⁿ c⁺
    ] ∎
   }

private
  _ : Dec→Bool (discreteℤ [ (3 , 5) ] [ (4 , 6) ]) ≡ true
  _ = refl

  _ : Dec→Bool (discreteℤ [ (3 , 5) ] [ (4 , 7) ]) ≡ false
  _ = refl

max_stars_repo_name: mchristianl/cubical

max_issues_repo_name: mchristianl/cubical

max_forks_repo_name: mchristianl/cubical


text:
open import Class.Listable
open import Data.List.Relation.Unary.All
open import Data.List.Relation.Unary.AllPairs
open import Data.List.Relation.Unary.Any
import Data.Vec.Recursive
import Data.Vec.Recursive.Categorical

open import Prelude

module Theory.PrimMeta where

private
  variable
    A B C : Set
    M : Set → Set

data PrimMeta : Set where
  EvalStmt      : PrimMeta
  ShellCmd      : PrimMeta
  CheckTerm     : PrimMeta
  Parse         : PrimMeta
  Normalize     : PrimMeta
  HeadNormalize : PrimMeta
  InferType     : PrimMeta

private
  variable
    m : PrimMeta

instance
  PrimMeta-Eq : Eq PrimMeta
  PrimMeta-Eq = Listable.Listable→Eq record
    { listing = EvalStmt ∷ ShellCmd ∷ CheckTerm ∷ Parse ∷ Normalize ∷ HeadNormalize ∷ InferType ∷ []
    ; unique = ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ (λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) ∷
                 ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) ∷
                 ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) ∷
                 ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) ∷
                 ((λ ()) ∷ (λ ()) ∷ []) ∷ ((λ ()) ∷ []) ∷ [] ∷ []
    ; complete = λ where
        EvalStmt      → here refl
        ShellCmd      → there (here refl)
        CheckTerm     → there (there (here refl))
        Parse         → there (there (there (here refl)))
        Normalize     → there (there (there (there (here refl))))
        HeadNormalize → there (there (there (there (there (here refl)))))
        InferType     → there (there (there (there (there (there (here refl)))))) }

  PrimMeta-EqB : EqB PrimMeta
  PrimMeta-EqB = Eq→EqB

  PrimMeta-Show : Show PrimMeta
  PrimMeta-Show = record { show = helper }
    where
      helper : PrimMeta → String
      helper EvalStmt      = "EvalStmt"
      helper ShellCmd      = "ShellCmd"
      helper CheckTerm     = "CheckTerm"
      helper Parse         = "Parse"
      helper Normalize     = "Normalize"
      helper HeadNormalize = "HeadNormalize"
      helper InferType     = "InferType"

primMetaArity : PrimMeta → ℕ
primMetaArity EvalStmt      = 1
primMetaArity ShellCmd      = 2
primMetaArity CheckTerm     = 2
primMetaArity Parse         = 3
primMetaArity Normalize     = 1
primMetaArity HeadNormalize = 1
primMetaArity InferType     = 1

primMetaArgs : Set → PrimMeta → Set
primMetaArgs A m  = A Data.Vec.Recursive.^ (primMetaArity m)

mapPrimMetaArgs : (A → B) → primMetaArgs A m → primMetaArgs B m
mapPrimMetaArgs f = Data.Vec.Recursive.map f _

traversePrimMetaArgs : {{Monad M}} → (A → M B) → primMetaArgs A m → M (primMetaArgs B m)
traversePrimMetaArgs {{mon}} = Data.Vec.Recursive.Categorical.mapM mon

primMetaArgs-Show : (A → String) → primMetaArgs A m → String
primMetaArgs-Show showA = Data.Vec.Recursive.foldr "" showA (λ _ a s → showA a + s) _

primMetaArgsZipWith : (A → B → C) → primMetaArgs A m → primMetaArgs B m → primMetaArgs C m
primMetaArgsZipWith f x y = Data.Vec.Recursive.zipWith f _ x y

primMetaArgsSequence : {{Monad M}} → primMetaArgs (M A) m → M (primMetaArgs A m)
primMetaArgsSequence {{mon}} = Data.Vec.Recursive.Categorical.sequenceM mon

primMetaArgsAnd : primMetaArgs Bool m → Bool
primMetaArgsAnd = Data.Vec.Recursive.foldr {P = const Bool} true id (const _∧_) _

ext: agda

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
module UniDB.Spec where

open import UniDB.Core public

record Vr (T : STX) : Set where
  field
    vr     : {γ : Dom} → Ix γ → T γ
    vr-inj : {γ : Dom} → Inj (vr {γ})
open Vr {{...}} public

record Wk (X : STX) : Set where
  field
    wk₁     : {γ : Dom} (x : X γ) → X (suc γ)
    wk      : {γ : Dom} (δ : Dom) (x : X γ) → X (γ ∪ δ)
    wk-zero : {γ : Dom} (x : X γ) → wk 0 x ≡ x
    wk-suc  : {γ : Dom} (δ : Dom) (x : X γ) → wk (suc δ) x ≡ wk₁ (wk δ x)

  wk1-wk₁ : {γ : Dom} (x : X γ) →
    wk 1 x ≡ wk₁ x
  wk1-wk₁ x = trans (wk-suc 0 x) (cong wk₁ (wk-zero x))
open Wk {{...}} public

instance
  iVrIx : Vr Ix
  vr     {{iVrIx}} i = i
  vr-inj {{iVrIx}} p = p

  iWkIx : Wk Ix
  wk₁     {{iWkIx}}           = suc
  wk      {{iWkIx}} zero    i = i
  wk      {{iWkIx}} (suc δ) i = suc (wk δ i)
  wk-zero {{iWkIx}} x         = refl
  wk-suc  {{iWkIx}} δ x       = refl

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

record WkVr (T : STX) {{vrT : Vr T}} {{wkT : Wk T}} : Set where
  field
    wk₁-vr  : {γ : Dom} (i : Ix γ) →
      wk₁ (vr {T} i) ≡ vr {T} (wk₁ i)
    wk-vr  : {γ : Dom} (δ : Dom) (i : Ix γ) →
      wk δ (vr {T} i) ≡ vr {T} (wk δ i)
open WkVr {{...}} public

instance
  iWkVrIx : WkVr Ix
  wk₁-vr {{iWkVrIx}} i = refl
  wk-vr {{iWkVrIx}} δ i = refl

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

record Lk (T : STX) (Ξ : MOR) : Set where
  field
    lk : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (i : Ix γ₁) → T γ₂
open Lk {{...}} public

record Up (Ξ : MOR) : Set where
  infixl 9 _↑₁ _↑_
  field
    _↑₁ : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) → Ξ (suc γ₁) (suc γ₂)
    _↑_ : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (δ : Dom) → Ξ (γ₁ ∪ δ) (γ₂ ∪ δ)
    ↑-zero : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) → ξ ↑ zero ≡ ξ
    ↑-suc : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (δ : Dom) → ξ ↑ suc δ ≡ ξ ↑ δ ↑₁

record Comp (Ξ : MOR) : Set where
  infixl 8 _⊙_
  field
    _⊙_ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Ξ γ₁ γ₂) (ξ₂ : Ξ γ₂ γ₃) → Ξ γ₁ γ₃

record Idm (Ξ : MOR) : Set where
  field
    idm : (γ : Dom) → Ξ γ γ

record Wkm (Ξ : MOR) : Set where
  field
    wkm : {γ : Dom} (δ : Dom) → Ξ γ (γ ∪ δ)

record Snoc (T : STX) (Ξ : MOR) : Set where
  field
    snoc : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (t : T γ₂) → Ξ (suc γ₁) γ₂

record Beta (T : STX) (Ξ : MOR) : Set where
  field
    beta : {γ : Dom} (t : T γ) → Ξ (suc γ) γ

open Idm {{...}} public
open Wkm {{...}} public
open Up {{...}} public
open Comp {{...}} public
open Snoc {{...}} public
open Beta {{...}} public

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

record LkRen
  (T : STX) {{vrT : Vr T}}
  (Ξ : MOR) {{lkIxΞ : Lk Ix Ξ}} {{lkTΞ : Lk T Ξ}} : Set where
  field
    lk-ren : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (i : Ix γ₁) →
      lk {T} ξ i ≡ vr (lk ξ i)
open LkRen {{...}} public

record LkUp
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}}
  (Ξ : MOR) {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} : Set where
  field
    lk-↑₁-zero : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) →
      lk {T} (ξ ↑₁) zero ≡ vr zero
    lk-↑₁-suc : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (i : Ix γ₁) →
      lk {T} (ξ ↑₁) (suc i) ≡ wk₁ (lk ξ i)

  lk-↑-∪ : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (i : Ix γ₁) (δ : Dom) →
    lk {T} (ξ ↑ δ) (wk δ i) ≡ wk δ (lk ξ i)
  lk-↑-∪ ξ i zero    = begin
    lk (ξ ↑ 0) i                  ≡⟨ cong₂ lk ((↑-zero ξ)) refl ⟩
    lk ξ i                        ≡⟨ sym (wk-zero (lk ξ i)) ⟩
    wk 0 (lk ξ i)                 ∎
  lk-↑-∪ ξ i (suc δ) = begin
    lk (ξ ↑ suc δ) (suc (wk δ i)) ≡⟨ cong₂ lk (↑-suc ξ δ) refl ⟩
    lk (ξ ↑ δ ↑₁) (suc (wk δ i))  ≡⟨ lk-↑₁-suc (ξ ↑ δ) (wk δ i) ⟩
    wk₁ (lk (ξ ↑ δ) (wk δ i))     ≡⟨ cong wk₁ (lk-↑-∪ ξ i δ) ⟩
    wk₁ (wk δ (lk ξ i))           ≡⟨ sym (wk-suc δ (lk ξ i)) ⟩
    wk (suc δ) (lk ξ i)           ∎
open LkUp {{...}} public

record LkRenComp
  (T : STX) {{vrT : Vr T}}
  (Ξ : MOR) {{lkIxΞ : Lk Ix Ξ}} {{lkTΞ : Lk T Ξ}} {{compΞ : Comp Ξ}}
  {{lkRenTΞ : LkRen T Ξ}} : Set where
  field
    lk-ren-comp : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Ξ γ₁ γ₂) (ξ₂ : Ξ γ₂ γ₃)
      (i : Ix γ₁) → lk {T} (ξ₁ ⊙ ξ₂) i ≡ lk {T} ξ₂ (lk {Ix} ξ₁ i)
open LkRenComp {{...}} public

record LkIdm
  (T : STX) {{vrT : Vr T}}
  (Ξ : MOR) {{lkTΞ : Lk T Ξ}} {{idmΞ : Idm Ξ}} : Set where
  field
    lk-idm : {γ : Dom} (i : Ix γ) → lk {T} (idm {Ξ} γ) i ≡ vr i
open LkIdm {{...}} public

record LkWkm
  (T : STX) {{vrT : Vr T}}
  (Ξ : MOR) {{lkTΞ : Lk T Ξ}} {{wkmΞ : Wkm Ξ}} : Set where
  field
    lk-wkm : {γ : Dom} (δ : Dom) (i : Ix γ) →
      lk {T} (wkm {Ξ} δ) i ≡ vr (wk δ i)
open LkWkm {{...}} public

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

record UpIdm (Ξ : MOR) {{upΞ : Up Ξ}} {{idmΞ : Idm Ξ}} : Set where
  field
    idm-↑₁ : {γ : Dom} → idm {Ξ} γ ↑₁ ≡ idm {Ξ} (suc γ)

  idm-↑ : {γ : Dom} (δ : Dom) → idm {Ξ} γ ↑ δ ≡ idm {Ξ} (γ ∪ δ)
  idm-↑ zero    = ↑-zero (idm {Ξ} _)
  idm-↑ (suc δ) = begin
    idm _ ↑ suc δ     ≡⟨ ↑-suc (idm _) δ ⟩
    idm _ ↑ δ ↑₁      ≡⟨ cong _↑₁ (idm-↑ δ) ⟩
    idm _ ↑₁          ≡⟨ idm-↑₁ ⟩
    idm (suc (_ ∪ δ)) ∎
open UpIdm {{...}} public

record UpComp (Ξ : MOR) {{upΞ : Up Ξ}} {{compΞ : Comp Ξ}} : Set where
  field
    ⊙-↑₁ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Ξ γ₁ γ₂) (ξ₂ : Ξ γ₂ γ₃) →
      (ξ₁ ⊙ ξ₂) ↑₁ ≡ (ξ₁ ↑₁) ⊙ (ξ₂ ↑₁)

  ⊙-↑ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Ξ γ₁ γ₂) (ξ₂ : Ξ γ₂ γ₃) (δ : Dom) →
    (ξ₁ ⊙ ξ₂) ↑ δ ≡ (ξ₁ ↑ δ) ⊙ (ξ₂ ↑ δ)
  ⊙-↑ ξ₁ ξ₂ zero    = begin
    (ξ₁ ⊙ ξ₂) ↑ 0       ≡⟨ ↑-zero (ξ₁ ⊙ ξ₂) ⟩
    ξ₁       ⊙ ξ₂       ≡⟨ sym (cong₂ _⊙_ (↑-zero ξ₁) (↑-zero ξ₂)) ⟩
    (ξ₁ ↑ 0) ⊙ (ξ₂ ↑ 0) ∎
  ⊙-↑ ξ₁ ξ₂ (suc δ) = begin
    (ξ₁ ⊙ ξ₂) ↑ suc δ           ≡⟨ ↑-suc (ξ₁ ⊙ ξ₂) δ ⟩
    (ξ₁ ⊙ ξ₂) ↑ δ ↑₁            ≡⟨ cong _↑₁ (⊙-↑ ξ₁ ξ₂ δ) ⟩
    ((ξ₁ ↑ δ) ⊙ (ξ₂ ↑ δ)) ↑₁    ≡⟨ ⊙-↑₁ (ξ₁ ↑ δ) (ξ₂ ↑ δ) ⟩
    (ξ₁ ↑ δ ↑₁) ⊙ (ξ₂ ↑ δ ↑₁)   ≡⟨ sym (cong₂ _⊙_ (↑-suc ξ₁ δ) (↑-suc ξ₂ δ)) ⟩
    (ξ₁ ↑ suc δ) ⊙ (ξ₂ ↑ suc δ) ∎
open UpComp {{...}} public

record CompIdm (Ξ : MOR) {{idmΞ : Idm Ξ}} {{compΞ : Comp Ξ}} : Set where
  field
    ⊙-idm : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) → ξ ⊙ idm {Ξ} γ₂ ≡ ξ
    idm-⊙ : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) → idm {Ξ} γ₁ ⊙ ξ ≡ ξ
open CompIdm {{...}} public

record CompAssoc (Ξ : MOR) {{compΞ : Comp Ξ}} : Set where
  field
    ⊙-assoc : {γ₁ γ₂ γ₃ γ₄ : Dom} (ξ₁ : Ξ γ₁ γ₂) (ξ₂ : Ξ γ₂ γ₃) (ξ₃ : Ξ γ₃ γ₄) →
      ξ₁ ⊙ (ξ₂ ⊙ ξ₃) ≡ (ξ₁ ⊙ ξ₂) ⊙ ξ₃
open CompAssoc {{...}} public

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

record WkmBeta
  (T : STX) (Ξ : MOR) {{idmΞ : Idm Ξ}} {{wkmΞ : Wkm Ξ}}
  {{compΞ : Comp Ξ}} {{betaTΞ : Beta T Ξ}} : Set where
  field
    wkm-beta : {γ : Dom} (t : T γ) → wkm {Ξ} 1 ⊙ beta {T} {Ξ} t ≡ idm {Ξ} γ
open WkmBeta {{...}} public

record WkmHom
  (Ξ : MOR) {{idmΞ : Idm Ξ}} {{wkmΞ : Wkm Ξ}} {{compΞ : Comp Ξ}} : Set where
  field
    wkm-zero : {γ : Dom} → wkm {Ξ} 0 ≡ idm {Ξ} γ
    wkm-suc  : {γ : Dom} (δ : Dom) → wkm {Ξ} {γ} (suc δ) ≡ wkm {Ξ} δ ⊙ wkm {Ξ} 1
open WkmHom {{...}} public

record WkmComm
  (Ξ : MOR) {{upΞ : Up Ξ}} {{wkmΞ : Wkm Ξ}} {{compΞ : Comp Ξ}} : Set where
  field
    wkm₁-comm : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) →
      ξ ⊙ wkm {Ξ} 1 ≡ wkm {Ξ} 1 ⊙ ξ ↑₁

  wkm-comm : {{idmΞ : Idm Ξ}} {{wkmHomΞ : WkmHom Ξ}}
    {{compIdmΞ : CompIdm Ξ}} {{compAssocΞ : CompAssoc Ξ}}
    {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (δ : Dom) →
    ξ ⊙ wkm {Ξ} δ ≡ wkm {Ξ} δ ⊙ ξ ↑ δ
  wkm-comm {{iWkmCommReg}} ξ zero  = begin
    ξ ⊙ wkm 0       ≡⟨ cong (_⊙_ ξ) wkm-zero ⟩
    ξ ⊙ idm _       ≡⟨ ⊙-idm ξ ⟩
    ξ               ≡⟨ sym (idm-⊙ ξ) ⟩
    idm _ ⊙ ξ       ≡⟨ sym (cong₂ _⊙_ wkm-zero (↑-zero ξ)) ⟩
    wkm 0 ⊙ (ξ ↑ 0) ∎
  wkm-comm {{iWkmCommReg}} ξ (suc δ) = begin
    ξ ⊙ wkm (suc δ)                ≡⟨ cong (_⊙_ ξ) (wkm-suc δ) ⟩
    ξ ⊙ (wkm δ ⊙ wkm 1)           ≡⟨ ⊙-assoc ξ (wkm δ) (wkm 1) ⟩
    (ξ ⊙ wkm δ) ⊙ wkm 1           ≡⟨ cong (λ ξ → ξ ⊙ wkm 1) (wkm-comm ξ δ) ⟩
    (wkm δ ⊙ (ξ ↑ δ)) ⊙ wkm 1     ≡⟨ sym (⊙-assoc (wkm δ) (ξ ↑ δ) (wkm 1)) ⟩
    wkm δ ⊙ ((ξ ↑ δ) ⊙ wkm 1)     ≡⟨ cong (_⊙_ (wkm δ)) (wkm₁-comm (ξ ↑ δ)) ⟩
    wkm δ ⊙ (wkm 1 ⊙ (ξ ↑ δ ↑₁))  ≡⟨ ⊙-assoc (wkm δ) (wkm 1) (ξ ↑ δ ↑₁) ⟩
    (wkm δ ⊙ wkm 1) ⊙ (ξ ↑ δ ↑₁)  ≡⟨ cong (λ ρ → (wkm δ ⊙ wkm 1) ⊙ ρ) (sym (↑-suc ξ δ)) ⟩
    (wkm δ ⊙ wkm 1) ⊙ (ξ ↑ suc δ) ≡⟨ cong (λ ρ → ρ ⊙ (ξ ↑ suc δ)) (sym (wkm-suc δ)) ⟩
    wkm (suc δ) ⊙ (ξ ↑ suc δ) ∎
open WkmComm {{...}} public

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

infix 1 [_]_≃_
record [_]_≃_
  (T : STX)
  {Ξ : MOR} {{lkTΞ : Lk T Ξ}}
  {Ζ : MOR} {{lkTΖ : Lk T Ζ}}
  {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₁ γ₂) : Set where
  field
    lk≃ : (i : Ix γ₁) → lk {T} {Ξ} ξ i ≡ lk {T} {Ζ} ζ i
open [_]_≃_ public

module _
  {T : STX} {{vrT : Vr T}} {{wkT : Wk T}}
  {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{lkUpTΞ : LkUp T Ξ}}
  {Ζ : MOR} {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}} {{lkUpTΖ : LkUp T Ζ}}
  where

  ≃-↑₁ : {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂}
    (hyp : [ T ] ξ ≃ ζ) → [ T ] ξ ↑₁ ≃ ζ ↑₁
  lk≃ (≃-↑₁ {γ₁} {γ₂} {ξ} {ζ} hyp) zero = begin
    lk (ξ ↑₁) zero     ≡⟨ lk-↑₁-zero ξ ⟩
    vr zero            ≡⟨ sym (lk-↑₁-zero ζ) ⟩
    lk (ζ ↑₁) zero     ∎
  lk≃ (≃-↑₁ {γ₁} {γ₂} {ξ} {ζ} hyp) (suc i) = begin
    lk (ξ ↑₁) (suc i)  ≡⟨ lk-↑₁-suc ξ i ⟩
    wk₁ (lk ξ i)       ≡⟨ cong wk₁ (lk≃ hyp i) ⟩
    wk₁ (lk ζ i)       ≡⟨ sym (lk-↑₁-suc ζ i) ⟩
    lk (ζ ↑₁) (suc i)  ∎

  ≃-↑ : {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂}
    (hyp : [ T ] ξ ≃ ζ) (δ : Dom) → [ T ] ξ ↑ δ ≃ ζ ↑ δ
  ≃-↑ {ξ = ξ} {ζ} hyp zero
    rewrite ↑-zero {Ξ} ξ | ↑-zero {Ζ} ζ = hyp
  ≃-↑ {ξ = ξ} {ζ} hyp (suc δ)
    rewrite ↑-suc {Ξ} ξ δ | ↑-suc {Ζ} ζ δ = ≃-↑₁ (≃-↑ hyp δ)

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

infix 1 [_]_≅_
data [_]_≅_ (T : STX)
  {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
  {Ζ : MOR} {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}} :
  {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₁ γ₂) → Set where
  ≃-to-≅ : {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂}
    (hyp : (δ' : Dom) → [ T ] ξ ↑ δ' ≃ ζ ↑ δ') (δ : Dom) →
    [ T ] ξ ↑ δ ≅ ζ ↑ δ

module _
  {T : STX}
  {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
  {Ζ : MOR} {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}} where

  ≃-to-≅` : {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂}
    (hyp : (δ' : Dom) → [ T ] ξ ↑ δ' ≃ ζ ↑ δ') → [ T ] ξ ≅ ζ
  ≃-to-≅` {ξ = ξ} {ζ} hyp = lem₂
    where
      lem : [ T ] ξ ↑ 0 ≅ ζ ↑ 0
      lem = ≃-to-≅ hyp 0
      lem₂ : [ T ] ξ ≅ ζ
      lem₂ rewrite sym (↑-zero {Ξ} ξ) | sym (↑-zero {Ζ} ζ) = lem

  ≅-to-≃ : {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂}
    (hyp : [ T ] ξ ≅ ζ) → [ T ] ξ ≃ ζ
  ≅-to-≃ (≃-to-≅ hyp δ) = hyp δ

  ≅-↑₁ : {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂}
    (hyp : [ T ] ξ ≅ ζ) → [ T ] ξ ↑₁ ≅ ζ ↑₁
  ≅-↑₁ (≃-to-≅ {ξ = ξ} {ζ} hyp δ)
    rewrite sym (↑-suc {Ξ} ξ δ) | sym (↑-suc {Ζ} ζ δ)
    = ≃-to-≅ hyp (suc δ)

  ≅-↑ : {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂}
    (hyp : [ T ] ξ ≅ ζ) (δ : Dom) → [ T ] ξ ↑ δ ≅ ζ ↑ δ
  ≅-↑ {ξ = ξ} {ζ} hyp zero
    rewrite ↑-zero ξ | ↑-zero ζ
    = hyp
  ≅-↑ {ξ = ξ} {ζ} hyp (suc δ)
    rewrite ↑-suc ξ δ | ↑-suc ζ δ
    = ≅-↑₁ (≅-↑ hyp δ)

module _
  {T : STX} {{vrT : Vr T}}
  {Ξ : MOR} {{lkIxΞ : Lk Ix Ξ}} {{lkTΞ : Lk T Ξ}} {{lkRenTΞ : LkRen T Ξ}} {{upΞ : Up Ξ}}
  {Ζ : MOR} {{lkIxΖ : Lk Ix Ζ}} {{lkTΖ : Lk T Ζ}} {{lkRenTΖ : LkRen T Ζ}} {{upΖ : Up Ζ}} where

  Ix≅-to-≅ : {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂} → [ Ix ] ξ ≅ ζ → [ T ] ξ ≅ ζ
  Ix≅-to-≅ (≃-to-≅ {ξ = ξ} {ζ} hyp δ) = ≃-to-≅ (λ δ' → record { lk≃ = λ i → begin
    lk {T} (ξ ↑ δ') i       ≡⟨ lk-ren {T} {Ξ} (ξ ↑ δ') i ⟩
    vr (lk {Ix} (ξ ↑ δ') i) ≡⟨ cong vr (lk≃ (hyp δ') i) ⟩
    vr (lk {Ix} (ζ ↑ δ') i) ≡⟨ sym (lk-ren {T} {Ζ} (ζ ↑ δ') i) ⟩
    lk {T} (ζ ↑ δ') i ∎}) δ

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

record HComp (Ξ Ζ Θ : MOR) : Set where
  infixl 8 _⊡_
  field
    _⊡_ : {γ₁ γ₂ γ₃ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₂ γ₃) → Θ γ₁ γ₃
open HComp {{...}} public

record UpHComp
  (Ξ : MOR) {{upΞ : Up Ξ}}
  (Ζ : MOR) {{upΖ : Up Ζ}}
  (Θ : MOR) {{upΘ : Up Θ}}
  {{hcompΞΖΘ : HComp Ξ Ζ Θ}} : Set where

  field
    ⊡-↑₁ : {γ₁ γ₂ γ₃ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₂ γ₃) →
      (_⊡_ {Θ = Θ} ξ ζ) ↑₁ ≡ (ξ ↑₁) ⊡ (ζ ↑₁)

  ⊡-↑ : {γ₁ γ₂ γ₃ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₂ γ₃) (δ : Dom) →
    _↑_ {Θ} (ξ ⊡ ζ) δ ≡ (ξ ↑ δ) ⊡ (ζ ↑ δ)
  ⊡-↑ ξ ζ zero = begin
    (ξ ⊡ ζ) ↑ 0           ≡⟨ ↑-zero {Θ} (_⊡_ {Ξ} {Ζ} {Θ} ξ ζ) ⟩
    (ξ ⊡ ζ)               ≡⟨ sym (cong₂ (_⊡_ {Ξ} {Ζ} {Θ}) (↑-zero ξ) (↑-zero ζ)) ⟩
    (ξ ↑ 0) ⊡ (ζ ↑ 0)     ∎
  ⊡-↑ ξ ζ (suc δ) = begin
    (ξ ⊡ ζ) ↑ suc δ       ≡⟨ ↑-suc (ξ ⊡ ζ) δ ⟩
    (ξ ⊡ ζ) ↑ δ ↑₁        ≡⟨ cong _↑₁ ((⊡-↑ ξ ζ δ)) ⟩
    (ξ ↑ δ ⊡ ζ ↑ δ) ↑₁    ≡⟨ ⊡-↑₁ (ξ ↑ δ) (ζ ↑ δ) ⟩
    ξ ↑ δ ↑₁ ⊡ ζ ↑ δ ↑₁   ≡⟨ sym (cong₂ (_⊡_ {Ξ} {Ζ} {Θ}) (↑-suc ξ δ) (↑-suc ζ δ)) ⟩
    ξ ↑ suc δ ⊡ ζ ↑ suc δ ∎
open UpHComp {{...}} public

record HCompIdmLeft
  (Ξ : MOR) {{idmΞ : Idm Ξ}}
  (Ζ : MOR) {{hcompΞΖΖ : HComp Ξ Ζ Ζ}} : Set where
  field
    idm-⊡ : {γ₁ γ₂ : Dom} (ζ : Ζ γ₁ γ₂) → idm {Ξ} γ₁ ⊡ ζ ≡ ζ
open HCompIdmLeft {{...}} public

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


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

module Light.Implementation.Data.These where

open import Light.Library.Data.These using (Library ; Dependencies)
open import Light.Variable.Levels
open import Light.Level using (_⊔_)

dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record { Implementation }
      where
      module Implementation where
            data These (𝕒 : Set aℓ) (𝕓 : Set bℓ) : Set (aℓ ⊔ bℓ) where
                  this : 𝕒 → These 𝕒 𝕓
                  that : 𝕓 → These 𝕒 𝕓
                  these : 𝕒 → 𝕓 → These 𝕒 𝕓

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib