text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Functions.Fibration where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Path
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓb : Level
    B : Type ℓb

module FiberIso {ℓ} (p⁻¹ : B → Type ℓ) (x : B) where

  p : Σ B p⁻¹ → B
  p = fst

  fwd : fiber p x → p⁻¹ x
  fwd ((x' , y) , q) = subst (λ z → p⁻¹ z) q y

  bwd : p⁻¹ x → fiber p x
  bwd y = (x , y) , refl

  fwd-bwd : ∀ x → fwd (bwd x) ≡ x
  fwd-bwd y = transportRefl y

  bwd-fwd : ∀ x → bwd (fwd x) ≡ x
  bwd-fwd ((x' , y) , q) i = h (r i)
    where h : Σ[ s ∈ singl x ] p⁻¹ (s .fst) → fiber p x
          h ((x , p) , y) = (x , y) , sym p
          r : Path (Σ[ s ∈ singl x ] p⁻¹ (s .fst))
                   ((x  , refl ) , subst p⁻¹ q y)
                   ((x' , sym q) , y                            )
          r = ΣPathP (isContrSingl x .snd (x' , sym q)
                     , toPathP (transport⁻Transport (λ i → p⁻¹ (q i)) y))

  -- HoTT Lemma 4.8.1
  fiberEquiv : fiber p x ≃ p⁻¹ x
  fiberEquiv = isoToEquiv (iso fwd bwd fwd-bwd bwd-fwd)

open FiberIso using (fiberEquiv) public

module _ {ℓ} {E : Type ℓ} (p : E → B) where

  -- HoTT Lemma 4.8.2
  totalEquiv : E ≃ Σ B (fiber p)
  totalEquiv = isoToEquiv isom
    where isom : Iso E (Σ B (fiber p))
          Iso.fun isom x           = p x , x , refl
          Iso.inv isom (b , x , q) = x
          Iso.leftInv  isom x           i = x
          Iso.rightInv isom (b , x , q) i = q i , x , λ j → q (i ∧ j)

module _ (B : Type ℓb) (ℓ : Level) where
  private
    ℓ' = ℓ-max ℓb ℓ

  -- HoTT Theorem 4.8.3
  fibrationEquiv : (Σ[ E ∈ Type ℓ' ] (E → B)) ≃ (B → Type ℓ')
  fibrationEquiv = isoToEquiv isom
    where isom : Iso (Σ[ E ∈ Type ℓ' ] (E → B)) (B → Type ℓ')
          Iso.fun isom (E , p) = fiber p
          Iso.inv isom p⁻¹     = Σ B p⁻¹ , fst
          Iso.rightInv isom p⁻¹ i x = ua (fiberEquiv p⁻¹ x) i
          Iso.leftInv  isom (E , p) i = ua e (~ i) , fst ∘ ua-unglue e (~ i)
            where e = totalEquiv p

-- The path type in a fiber of f is equivalent to a fiber of (cong f)
open import Cubical.Foundations.Function

fiberPath : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {b : B} (h h' : fiber f b) →
             (Σ[ p ∈ (fst h ≡ fst h') ] (PathP (λ i → f (p i) ≡ b) (snd h) (snd h')))
           ≡ fiber (cong f) (h .snd ∙∙ refl ∙∙ sym (h' .snd))
fiberPath h h' = cong (Σ (h .fst ≡ h' .fst)) (funExt λ p → flipSquarePath ∙ PathP≡doubleCompPathʳ _ _ _ _)

fiber≡ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {b : B} (h h' : fiber f b)
  → (h ≡ h') ≡ fiber (cong f) (h .snd ∙∙ refl ∙∙ sym (h' .snd))
fiber≡ {f = f} {b = b} h h' =
  ΣPath≡PathΣ ⁻¹ ∙
  fiberPath h h'

FibrationStr : (B : Type ℓb) → Type ℓ → Type (ℓ-max ℓ ℓb)
FibrationStr B A = A → B

Fibration : (B : Type ℓb) → (ℓ : Level) → Type (ℓ-max ℓb (ℓ-suc ℓ))
Fibration {ℓb = ℓb} B ℓ = Σ[ A ∈ Type ℓ ] FibrationStr B A


text:
module Numeral.Natural.Relation.ModuloCongruence where

open import Data.Boolean.Stmt
open import Functional
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.Modulo
open import Relator.Equals
open import Type

private variable m n x y : ℕ

_≡_[mod_] : ℕ → ℕ → (m : ℕ) → .⦃ pos : IsTrue(positive? m) ⦄ → Type
a ≡ b [mod m ] = ((_≡_) on₂ (_mod m)) a b

open import Relator.Equals.Proofs.Equiv
open import Structure.Relator.Equivalence
open import Structure.Relator.Equivalence.Proofs
open import Structure.Setoid using (Equiv ; intro)

instance
  mod-congruence-equivalence : ⦃ pos : IsTrue(positive? m) ⦄ → Equivalence(_≡_[mod m ])
  mod-congruence-equivalence {m} = on₂-equivalence {f = _mod m} ⦃ [≡]-equivalence ⦄

mod-congruence-equiv : (m : ℕ) → ⦃ pos : IsTrue(positive? m) ⦄ → Equiv(ℕ)
mod-congruence-equiv m = intro(_≡_[mod m ]) ⦃ mod-congruence-equivalence {m} ⦄

open import Lang.Instance
open import Logic.Propositional
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Modulo.Proofs
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Relation.Order
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Proofs
open import Structure.Operator
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Syntax.Implication
open import Syntax.Transitivity

mod-congruence-loose-linear-map : ∀{f g₁ g₂ h : ℕ → ℕ} (add : ∀{a b} → (f(a + b) ≡ g₁(a) + g₂(b))) → (mul : ∀{a b} → (g₂(a ⋅ b) ≡ a ⋅ h(b))) → ∀{m} ⦃ pos : IsTrue(positive? m) ⦄ → Function ⦃ mod-congruence-equiv m ⦄ ⦃ mod-congruence-equiv m ⦄ f
Function.congruence (mod-congruence-loose-linear-map {f}{g₁}{g₂}{h} add mul {𝐒 m}) {a}{b} = mod-intro₂(\{a}{b} am bm → (am ≡ bm) → (f(a) mod 𝐒(m) ≡ f(b) mod 𝐒(m))) {𝐒 m} (\{a}{b}{n₁}{n₂} → p{a}{b}{n₁}{n₂}) {a}{b} where
  p : ∀{a b n₁ n₂} → (a < 𝐒(m)) → (b < 𝐒(m)) → (a ≡ b) → (f(a + (n₁ ⋅ 𝐒(m))) mod 𝐒(m)) ≡ (f(b + (n₂ ⋅ 𝐒(m))) mod 𝐒(m))
  p {a}{b}{n₁}{n₂} am bm ab =
    f(a + (n₁ ⋅ 𝐒(m))) mod 𝐒(m)       🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(m)) (add{a}{n₁ ⋅ 𝐒(m)}) ]
    (g₁(a) + g₂(n₁ ⋅ 𝐒(m))) mod 𝐒(m)  🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(m)) (congruence₂ᵣ(_+_)(g₁(a)) (congruence₁(g₂) (commutativity(_⋅_) {n₁}{𝐒 m}))) ]
    (g₁(a) + g₂(𝐒(m) ⋅ n₁)) mod 𝐒(m)  🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(m)) (congruence₂ᵣ(_+_)(g₁(a)) (mul{𝐒(m)}{n₁})) ]
    (g₁(a) + (𝐒(m) ⋅ h(n₁))) mod 𝐒(m) 🝖[ _≡_ ]-[ mod-of-modulus-sum-multiple{g₁(a)}{𝐒 m}{h(n₁)} ]
    g₁(a) mod 𝐒(m)                    🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(m)) (congruence₁(g₁) ab) ]
    g₁(b) mod 𝐒(m)                    🝖[ _≡_ ]-[ mod-of-modulus-sum-multiple{g₁(b)}{𝐒 m}{h(n₂)} ]-sym
    (g₁(b) + (𝐒(m) ⋅ h(n₂))) mod 𝐒(m) 🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(m)) (congruence₂ᵣ(_+_)(g₁(b)) (mul{𝐒(m)}{n₂})) ]-sym
    (g₁(b) + g₂(𝐒(m) ⋅ n₂)) mod 𝐒(m)  🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(m)) (congruence₂ᵣ(_+_)(g₁(b)) (congruence₁(g₂) (commutativity(_⋅_) {n₂}{𝐒 m}))) ]-sym
    (g₁(b) + g₂(n₂ ⋅ 𝐒(m))) mod 𝐒(m)  🝖[ _≡_ ]-[ congruence₁(_mod 𝐒(m)) (add{b}{n₂ ⋅ 𝐒(m)}) ]-sym
    f(b + (n₂ ⋅ 𝐒(m))) mod 𝐒(m)       🝖-end

module _ {m} ⦃ pos : IsTrue(positive?(m)) ⦄ where
  instance
    mod-congruence-𝐒-function : Function ⦃ mod-congruence-equiv m ⦄ ⦃ mod-congruence-equiv m ⦄ 𝐒
    mod-congruence-𝐒-function = mod-congruence-loose-linear-map {𝐒}{𝐒}{id}{id} (reflexivity(_≡_)) (reflexivity(_≡_)) {m}

  instance
    mod-congruence-[+]-operator : BinaryOperator ⦃ mod-congruence-equiv m ⦄ ⦃ mod-congruence-equiv m ⦄ ⦃ mod-congruence-equiv m ⦄ (_+_)
    mod-congruence-[+]-operator = binaryOperator-from-function ⦃ _ ⦄ ⦃ _ ⦄ ⦃ _ ⦄ {_▫_ = _+_}
      ⦃ \{x} → functionₗ-from-commutative-functionᵣ ⦃ _ ⦄ ⦃ _ ⦄ {_+_} ⦃ r ⦄ ⦃ intro (\{x} → congruence₁(_mod m) (commutativity(_+_) {x})) ⦄ {x} ⦄
      ⦃ r ⦄
      where
        r : ∀{c} → Function ⦃ mod-congruence-equiv m ⦄ ⦃ mod-congruence-equiv m ⦄ (_+ c)
        r{c} = mod-congruence-loose-linear-map {_+ c}{_+ c}{id}{id} (\{a}{b} → One.commuteᵣ-assocₗ{_▫_ = _+_} {a}{b}{c}) (reflexivity(_≡_)) {m}
        -- r {_}{_}{𝟎}  {_} p = p
        -- r {a}{b}{𝐒 c}{m} p = mod-congruence-with-𝐒 {a + c}{b + c}{m} (r {a}{b}{c}{m} p)

  instance
    mod-congruence-[⋅]-operator : BinaryOperator ⦃ mod-congruence-equiv m ⦄ ⦃ mod-congruence-equiv m ⦄ ⦃ mod-congruence-equiv m ⦄ (_⋅_)
    mod-congruence-[⋅]-operator = binaryOperator-from-function ⦃ _ ⦄ ⦃ _ ⦄ ⦃ _ ⦄ {_▫_ = _⋅_}
      ⦃ \{x} → functionₗ-from-commutative-functionᵣ ⦃ _ ⦄ ⦃ _ ⦄ {_⋅_} ⦃ \{c} → r{c} ⦄ ⦃ intro (\{x}{y} → congruence₁(_mod m) (commutativity(_⋅_) {x}{y})) ⦄ {x} ⦄
      ⦃ \{c} → r{c} ⦄
      where
        r : ∀{c} → Function ⦃ mod-congruence-equiv m ⦄ ⦃ mod-congruence-equiv m ⦄ (_⋅ c)
        r{c} = mod-congruence-loose-linear-map {_⋅ c}{_⋅ c}{_⋅ c}{_⋅ c} (\{a}{b} → distributivityᵣ(_⋅_)(_+_) {a}{b}{c}) (\{a}{b} → associativity(_⋅_) {a}{b}{c}) {m}

  mod-congruence-[^]ₗ-function : ∀{n} → Function ⦃ mod-congruence-equiv m ⦄ ⦃ mod-congruence-equiv m ⦄ (_^ n)
  Function.congruence (mod-congruence-[^]ₗ-function {𝟎})           _ = reflexivity(_≡_)
  Function.congruence (mod-congruence-[^]ₗ-function {𝐒 n}) {a} {b} p = BinaryOperator.congruence ⦃ _ ⦄ ⦃ _ ⦄ ⦃ _ ⦄ mod-congruence-[⋅]-operator {a}{b}{a ^ n}{b ^ n} p (Function.congruence ⦃ _ ⦄ ⦃ _ ⦄ (mod-congruence-[^]ₗ-function {n}) p)

instance
  mod-congruence-𝐒-injective : ⦃ pos : IsTrue(positive?(m)) ⦄ → Injective ⦃ mod-congruence-equiv m ⦄ ⦃ mod-congruence-equiv m ⦄ 𝐒
  Injective.proof (mod-congruence-𝐒-injective {𝐒 m}) {a}{b} =
    𝐒(a) mod 𝐒(m) ≡ 𝐒(b) mod 𝐒(m)             ⇒-[ swap (BinaryOperator.congruence ⦃ _ ⦄ ⦃ _ ⦄ ⦃ _ ⦄ (mod-congruence-[+]-operator {𝐒 m}) {𝐒 a}{𝐒 b}{m}{m}) (reflexivity(_≡_)) ]
    (𝐒(a) + m) mod 𝐒(m) ≡ (𝐒(b) + m) mod 𝐒(m) ⇒-[]
    (a + 𝐒(m)) mod 𝐒(m) ≡ (b + 𝐒(m)) mod 𝐒(m) ⇒-[ (p ↦ symmetry(_≡_) (mod-of-modulus-addᵣ{a}{m}) 🝖 p 🝖 mod-of-modulus-addᵣ{b}{m}) ]
    a mod 𝐒(m) ≡ b mod 𝐒(m)                   ⇒-end

mod-congruence-[𝄩] : ∀{a b m} → ⦃ pos : IsTrue(positive?(m)) ⦄ → (a ≡ b [mod m ]) ↔ (m ∣ (a 𝄩 b))
mod-congruence-[𝄩] {a} {b} {𝐒 m} = [↔]-intro (l{a}{b}) (r{a}{b}) where
  l : ∀{a b} → (a mod 𝐒(m) ≡ b mod 𝐒(m)) ← (𝐒(m) ∣ (a 𝄩 b))
  l {𝟎}   {𝟎}   div = [≡]-intro
  l {𝟎}   {𝐒 b} div = symmetry(_≡_) ([↔]-to-[←] mod-divisibility div)
  l {𝐒 a} {𝟎}   div = [↔]-to-[←] mod-divisibility div
  l {𝐒 a} {𝐒 b} div = congruence₁ ⦃ mod-congruence-equiv _ ⦄ ⦃ mod-congruence-equiv _ ⦄ (𝐒) {a}{b} (l{a}{b} div)

  r : ∀{a b} → (a mod 𝐒(m) ≡ b mod 𝐒(m)) → (𝐒(m) ∣ (a 𝄩 b))
  r {𝟎}   {𝟎}   eq = Div𝟎
  r {𝟎}   {𝐒 b} eq = [↔]-to-[→] mod-divisibility (symmetry(_≡_) eq)
  r {𝐒 a} {𝟎}   eq = [↔]-to-[→] mod-divisibility eq
  r {𝐒 a} {𝐒 b} eq = r{a}{b} (injective ⦃ mod-congruence-equiv _ ⦄ ⦃ mod-congruence-equiv _ ⦄ (𝐒) {a}{b} eq)

open import Logic.Propositional.Theorems
open import Numeral.Natural.Function.GreatestCommonDivisor
open import Numeral.Natural.Function.GreatestCommonDivisor.Proofs
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.FlooredDivision.Proofs
open import Numeral.Natural.Oper.FlooredDivision.Proofs.Inverse
open import Numeral.Natural.Coprime
open import Numeral.Natural.Coprime.Proofs
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Relation.Divisibility.Proofs.Product
open import Structure.Relator

-- TODO: Move the postulates below
postulate divides-[⌊/⌋] : ∀{a b c} ⦃ pos : Positive(c) ⦄ → (c ∣ a) → (a ∣ b) → ((a ⌊/⌋ c) ∣ (b ⌊/⌋ c))
postulate [⋅]-positive : ∀{a b} → ⦃ Positive(a) ⦄ → ⦃ Positive(b) ⦄ → Positive(a ⋅ b)
postulate [⌊/⌋][⋅]ₗ-compatibility : ∀{a b c} ⦃ pos : Positive(c) ⦄ → (c ∣ a) → (((a ⋅ b) ⌊/⌋ c) ≡ (a ⌊/⌋ c) ⋅ b)
postulate [⌊/⌋][⋅]ᵣ-compatibility : ∀{a b c} ⦃ pos : Positive(c) ⦄ → (c ∣ a) → (((a ⋅ b) ⌊/⌋ c) ≡ a ⋅ (b ⌊/⌋ c))

mod-congruence-scale-modulus : ∀{m} → ⦃ pos : Positive(m) ⦄ → ∀{a b c} → (c ⋅ a ≡ c ⋅ b [mod m ]) ↔ (a ≡ b [mod((m ⌊/⌋ gcd c m) ⦃ _ ⦄)]) ⦃ _ ⦄
mod-congruence-scale-modulus {m} ⦃ pos ⦄ {a}{b}{c} = [↔]-transitivity  ([↔]-transitivity mod-congruence-[𝄩] ([↔]-intro l r)) ([↔]-symmetry (mod-congruence-[𝄩] ⦃ [⌊/⌋]-positive ⦃ pos ⦄ ⦃ pgcd ⦄ ⦄)) where
  instance
    pgcd : Positive(gcd c m)
    pgcd = [↔]-to-[→] gcd-positive ([∨]-introᵣ pos)

  l : (m ∣ ((c ⋅ a) 𝄩 (c ⋅ b))) ← ((m ⌊/⌋ gcd c m) ⦃ _ ⦄ ∣ (a 𝄩 b))
  l =
    (m ⌊/⌋ gcd c m) ∣ (a 𝄩 b)                         ⇒-[ divides-with-[⋅]ᵣ-both {z = gcd c m} ]
    ((m ⌊/⌋ gcd c m) ⋅ gcd c m) ∣ ((a 𝄩 b) ⋅ gcd c m) ⇒-[ substitute₂ₗ(_∣_) ([⋅][⌊/⌋]-inverseOperatorᵣ (Gcd.divisorᵣ Gcd-gcd)) ]
    m ∣ ((a 𝄩 b) ⋅ gcd c m)                           ⇒-[ divides-with-[⋅] {c = (c ⌊/⌋ gcd c m) ⦃ _ ⦄} ∘ [∨]-introₗ ]
    m ∣ ((a 𝄩 b) ⋅ gcd c m) ⋅ (c ⌊/⌋ gcd c m)         ⇒-[ substitute₂ᵣ(_∣_) (associativity(_⋅_) {a 𝄩 b}{gcd c m}{(c ⌊/⌋ gcd c m) ⦃ _ ⦄}) ]
    m ∣ (a 𝄩 b) ⋅ (gcd c m ⋅ (c ⌊/⌋ gcd c m))         ⇒-[ substitute₂ᵣ(_∣_) (congruence₂ᵣ(_⋅_)(a 𝄩 b) (symmetry(_≡_) ([⌊/⌋][⋅]ᵣ-compatibility {gcd c m}{c}{gcd c m} (reflexivity(_∣_))))) ]
    m ∣ (a 𝄩 b) ⋅ ((gcd c m ⋅ c) ⌊/⌋ gcd c m)         ⇒-[ substitute₂ᵣ(_∣_) (congruence₂ᵣ(_⋅_)(a 𝄩 b) ([⌊/⌋][swap⋅]-inverseOperatorᵣ {gcd c m}{c})) ]
    m ∣ (a 𝄩 b) ⋅ c                                   ⇒-[ substitute₂ᵣ(_∣_) (commutativity(_⋅_) {a 𝄩 b}{c}) ]
    m ∣ c ⋅ (a 𝄩 b)                                   ⇒-[ substitute₂ᵣ(_∣_) (distributivityₗ(_⋅_)(_𝄩_) {c}{a}{b}) ]
    m ∣ ((c ⋅ a) 𝄩 (c ⋅ b))                           ⇒-end

  r : (m ∣ ((c ⋅ a) 𝄩 (c ⋅ b))) → ((m ⌊/⌋ gcd c m) ⦃ _ ⦄ ∣ (a 𝄩 b))
  r =
    (m ∣ (c ⋅ a 𝄩 c ⋅ b))                                        ⇒-[ substitute₂ᵣ(_∣_) (symmetry(_≡_) (distributivityₗ(_⋅_)(_𝄩_) {c}{a}{b})) ]
    (m ∣ c ⋅ (a 𝄩 b))                                            ⇒-[ divides-[⌊/⌋] {m}{c ⋅ (a 𝄩 b)}{gcd c m} (Gcd.divisorᵣ Gcd-gcd) ]
    (m ⌊/⌋ gcd c m) ⦃ _ ⦄ ∣ ((c ⋅ (a 𝄩 b)) ⌊/⌋ gcd c m) ⦃ _ ⦄    ⇒-[ substitute₂ᵣ(_∣_) ([⌊/⌋][⋅]ₗ-compatibility {c}{a 𝄩 b}{gcd c m} ⦃ pgcd ⦄ (Gcd.divisorₗ {c}{m} Gcd-gcd)) ]
    (m ⌊/⌋ gcd c m) ⦃ _ ⦄ ∣ ((c ⌊/⌋ gcd c m) ⦃ pgcd ⦄ ⋅ (a 𝄩 b)) ⇒-[ swap(coprime-divides-of-[⋅] {(m ⌊/⌋ gcd c m) ⦃ _ ⦄}{(c ⌊/⌋ gcd c m) ⦃ _ ⦄}{a 𝄩 b}) (symmetry(Coprime) ([⌊/⌋]-gcd-coprime{c}{m} ([∨]-introᵣ pos))) ]
    ((m ⌊/⌋ gcd c m) ⦃ _ ⦄ ∣ (a 𝄩 b))                            ⇒-end

postulate mod-congruence-scale : ∀{m} ⦃ pos-m : Positive(m) ⦄ {c} ⦃ pos-c : Positive(c) ⦄ → ∀{a b} → (a ≡ b [mod m ]) → (c ⋅ a ≡ c ⋅ b [mod(c ⋅ m)]) ⦃ [⋅]-positive {c}{m} ⦄

postulate mod-congruence-divide : ∀{m} ⦃ pos-m : Positive(m) ⦄ {c} ⦃ pos-c : Positive(c) ⦄ → (c ∣ m) → ∀{a b} → (c ∣ a) → (c ∣ b) → (a ≡ b [mod m ]) → (a ⌊/⌋ c ≡ b ⌊/⌋ c [mod(m ⌊/⌋ c)]) ⦃ [⌊/⌋]-positive {m}{c} ⦄

postulate mod-congruence-smaller-modulus : ∀{m₁} ⦃ pos-m₁ : Positive(m₁) ⦄ {m₂} ⦃ pos-m₂ : Positive(m₂) ⦄ → (m₂ ∣ m₁) → ∀{a b} → (a ≡ b [mod m₁ ]) → (a ≡ b [mod m₂ ])

postulate mod-congruence-to-gcd-equality : ∀{m} ⦃ pos-m : Positive(m) ⦄ → ∀{a b} → (a ≡ b [mod m ]) → (gcd a m ≡ gcd b m)

postulate mod-congruence-[−₀]-operator : ∀{m} ⦃ pos-m : Positive(m) ⦄ → ∀{a₁ a₂ b₁ b₂} → (a₁ ≥ b₁) → (a₂ ≥ b₂) → (a₁ ≡ a₂ [mod m ]) → (b₁ ≡ b₂ [mod m ]) → (a₁ −₀ b₁ ≡ a₂ −₀ b₂ [mod m ])

postulate mod-congruence-[⌊/⌋]-operator : ∀{m} ⦃ pos-m : Positive(m) ⦄ → ∀{a₁ a₂ b₁ b₂} ⦃ pos-b₁ : Positive(b₁) ⦄ ⦃ pos-b₂ : Positive(b₂) ⦄ → (a₁ ∣ b₁) → (a₂ ∣ b₂) → (a₁ ≡ a₂ [mod m ]) → (b₁ ≡ b₂ [mod m ]) → (a₁ ⌊/⌋ b₁ ≡ a₂ ⌊/⌋ b₂ [mod m ])

ext: agda

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:
{-# OPTIONS --cubical #-}
module Cubical.Codata.Conat where

open import Cubical.Codata.Conat.Base public

open import Cubical.Codata.Conat.Properties public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong; cong₂; subst; trans)
open import Relation.Nullary.Decidable using (True; from-yes)
open import Relation.Nullary.Negation using (¬?; contradiction)
open Relation.Binary.PropositionalEquality.≡-Reasoning
open import Function using (_∘_)
open import Relation.Nullary using (yes; no)

open import Data.Empty using (⊥)
open import Data.Product using (_×_; _,_; Σ-syntax; proj₁; proj₂)
open import Data.Fin.Base as Fin using (Fin; zero; suc)
open import Data.Unit using (⊤; tt)

open import Data.List.Base as List using (List; []; _∷_; [_])
import Data.List.Properties as Listₚ
import Data.Char.Properties as Charₚ
import Data.Digit as Digit
import Data.List.Membership.Propositional as ∈ₗ
import Data.List.Membership.Propositional.Properties as ∈ₗₚ
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
import Data.Nat.Properties as ℕₚ
import Data.Nat.Show as ℕₛ
import Data.Nat.Show.Properties as ℕₛₚ
open import Data.String.Base as String using (String)
import Data.Product.Properties as Productₚ
open import Data.Vec.Base as Vec using ([]; _∷_; Vec)
import Data.Vec.Properties as Vecₚ
open import Data.Vec.Relation.Unary.Any as Any using (here; there)
import Data.Vec.Membership.Propositional as ∈ᵥ
import Data.Vec.Membership.Propositional.Properties as ∈ᵥₚ

open import PiCalculus.Syntax
open Raw
open Scoped
open Conversion

open import PiCalculus.Utils

module PiCalculus.Syntax.Properties where

module _ where
  private
    variable
      n : ℕ
      P Q R S : Scoped n
      x y : Fin n
      namex namey : Name

  fromName∘toName : (i : Fin n) (ctx : Ctx n) → ∈toFin (∈ᵥₚ.∈-lookup i ctx) ≡ i
  fromName∘toName zero (x ∷ ctx) = refl
  fromName∘toName (suc i) (x ∷ ctx) rewrite fromName∘toName i ctx = refl

  toName∘fromName : ∀ {x} {ctx : Ctx n} (x∈ctx : x ∈ᵥ.∈ ctx) → Vec.lookup ctx (∈toFin x∈ctx) ≡ x
  toName∘fromName (here px) = sym px
  toName∘fromName (there x∈ctx) = toName∘fromName x∈ctx

  -- The circum (^) is not a decimal character
  ^∉DECIMALS : '^' ∈ᵥ.∉ Digit.digitChars
  ^∉DECIMALS = from-yes (¬? (Any.any? ('^' Charₚ.≟_) Digit.digitChars))

  module _ (base : ℕ) {2≤base : True (2 ℕₚ.≤? base)} {base≤16 : True (base ℕₚ.≤? 16)} where
    charsInBase∈digitChars : ∀ n c → c ∈ₗ.∈ ℕₛ.charsInBase base {2≤base} {base≤16} n → c ∈ᵥ.∈ Digit.digitChars
    charsInBase∈digitChars n c i with ∈ₗₚ.∈-map⁻ Digit.showDigit i
    charsInBase∈digitChars n c i | d , _ , refl = ∈ᵥₚ.∈-lookup (Fin.inject≤ d _) Digit.digitChars

  -- In <name>^<natural> the <natural> does not contain ^, therefore toChars is injective
  toChars-injective : (x y : Name × ℕ) → toChars x ≡ toChars y → x ≡ y
  toChars-injective (nx , cx) (ny , cy) eq = cong₂ _,_ cancel-names (ℕₛₚ.charsInBase-injective 10 cx cy count-repr)
    where
      count-repr = ListInv.inv-++ʳ nx ny '^'
                                   (^∉DECIMALS ∘ charsInBase∈digitChars 10 cx '^')
                                   (^∉DECIMALS ∘ charsInBase∈digitChars 10 cy '^')
                                   eq
      cancel-names = Listₚ.++-cancelʳ nx ny
                                      (subst (λ ● → nx List.++ ('^' ∷ ●) ≡ _)
                                            count-repr eq)

  -- A fresh variable name created from inspecting a context cannot be in that context
  fresh-∉' : ∀ m name (xs : Ctx n) → toChars (name , m ℕ.+ (count name xs)) ∈ᵥ.∉ apply xs
  fresh-∉' m name (x ∷ xs) (here seq) with Listₚ.≡-dec Charₚ._≟_ name x
  fresh-∉' m name (x ∷ xs) (here seq) | yes refl = ℕₚ.m≢1+n+m _ (begin
    count name xs
      ≡˘⟨ Productₚ.,-injectiveʳ (toChars-injective (name , m ℕ.+ suc (count name xs)) (name , count name xs) seq) ⟩
    m ℕ.+ suc (count name xs)
      ≡⟨ ℕₚ.+-suc m _ ⟩
    suc m ℕ.+ count name xs
      ∎)
  fresh-∉' m name (x ∷ xs) (here seq) | no ¬q = contradiction
    (Productₚ.,-injectiveˡ (toChars-injective (name , m ℕ.+ count name xs) (x , count x xs) seq)) ¬q
  fresh-∉' m name (x ∷ xs) (there ∈ps) with Listₚ.≡-dec Charₚ._≟_ name x
  fresh-∉' m name (x ∷ xs) (there ∈ps) | yes refl rewrite ℕₚ.+-suc m (count name xs) = fresh-∉' (suc m) name _ ∈ps
  fresh-∉' m name (x ∷ xs) (there ∈ps) | no ¬q = fresh-∉' m name _ ∈ps

  fresh-∉ : ∀ name (xs : Ctx n) → toChars (name , count name xs) ∈ᵥ.∉ apply xs
  fresh-∉ name xs = fresh-∉' zero name xs

  -- Translating from de Bruijn to names results in a well-scoped process

  toRaw-WellScoped : (ctx : Ctx n) (P : Scoped n) → WellScoped (apply ctx) (toRaw ctx P)
  toRaw-WellScoped ctx 𝟘 = tt
  toRaw-WellScoped ctx (ν P ⦃ name ⦄) = toRaw-WellScoped (name ∷ ctx) P
  toRaw-WellScoped ctx (P ∥ Q) = toRaw-WellScoped ctx P , toRaw-WellScoped ctx Q
  toRaw-WellScoped ctx ((x ⦅⦆ P) ⦃ name ⦄) = ∈ᵥₚ.∈-lookup _ _ , toRaw-WellScoped (name ∷ ctx) P
  toRaw-WellScoped ctx (x ⟨ y ⟩ P) = ∈ᵥₚ.∈-lookup _ _ , ∈ᵥₚ.∈-lookup _ _ , toRaw-WellScoped ctx P

  -- Translating from de Bruijn to names results in no shadowed variables

  toRaw-NotShadowed : (ctx : Ctx n) (P : Scoped n) → NotShadowed (apply ctx) (toRaw ctx P)
  toRaw-NotShadowed ctx 𝟘 = tt
  toRaw-NotShadowed ctx (ν P ⦃ name ⦄) = fresh-∉ name ctx , (toRaw-NotShadowed (_ ∷ ctx) P)
  toRaw-NotShadowed ctx (P ∥ Q) = toRaw-NotShadowed ctx P , toRaw-NotShadowed ctx Q
  toRaw-NotShadowed ctx ((x ⦅⦆ P) ⦃ name ⦄) = fresh-∉ name ctx , toRaw-NotShadowed (name ∷ ctx) P
  toRaw-NotShadowed ctx (x ⟨ y ⟩ P) = toRaw-NotShadowed ctx P

  -- Translating from de Bruijn to names and back results in the same process modulo name hints

  data _α-≡_ {n} : Scoped n → Scoped n → Set where
    inaction : 𝟘 α-≡ 𝟘
    scope    : P α-≡ Q → ν P ⦃ namex ⦄ α-≡ ν Q ⦃ namey ⦄
    comp     : P α-≡ Q → R α-≡ S → (P ∥ R) α-≡ (Q ∥ S)
    input    : P α-≡ Q → (x ⦅⦆ P) ⦃ namex ⦄ α-≡ (x ⦅⦆ Q) ⦃ namey ⦄
    output   : P α-≡ Q → (x ⟨ y ⟩ P) α-≡ (x ⟨ y ⟩ Q)

  fromRaw∘toRaw : (ctx : Ctx n) (P : Scoped n)
                → fromRaw' (apply ctx) (toRaw ctx P) (toRaw-WellScoped ctx P) α-≡ P
  fromRaw∘toRaw ctx 𝟘 = inaction
  fromRaw∘toRaw ctx (ν P ⦃ name ⦄) =
    scope (fromRaw∘toRaw (name ∷ ctx) P)
  fromRaw∘toRaw ctx (P ∥ Q) =
    comp (fromRaw∘toRaw ctx P) (fromRaw∘toRaw ctx Q)
  fromRaw∘toRaw ctx ((x ⦅⦆ P) ⦃ name ⦄)
    rewrite fromName∘toName x (apply ctx) =
    input (fromRaw∘toRaw (name ∷ ctx) P)
  fromRaw∘toRaw ctx (x ⟨ y ⟩ P)
    rewrite fromName∘toName x (apply ctx) | fromName∘toName y (apply ctx) =
    output (fromRaw∘toRaw ctx P)

module _ where
  private
    variable
      n : ℕ
      P Q R S : Raw
      x y w z : Name
      ks vs : Ctx n

  _∈²_ : ∀ {n} → (Name × Name) → (Ctx n × Ctx n) → Set
  (x , y ) ∈² (xs , ys) = Σ[ i ∈ Fin _ ] (Vec.lookup xs i ≡ x × Vec.lookup ys i ≡ y)

  infix 5 _α[_↦_]≡_
  data _α[_↦_]≡_ : Raw → ∀ {n} → Ctx n → Ctx n → Raw → Set where
    inaction : 𝟘 α[ ks ↦ vs ]≡ 𝟘
    scope    : P α[ x ∷ ks ↦ y ∷ vs ]≡ Q
             → ⦅ν x ⦆ P α[ ks ↦ vs ]≡ ⦅ν y ⦆ Q
    comp     : P α[ ks ↦ vs ]≡ Q
             → R α[ ks ↦ vs ]≡ S
             → P ∥ R α[ ks ↦ vs ]≡ Q ∥ S
    input    : (x , y) ∈² (ks , vs)
             → P α[ w ∷ ks ↦ z ∷ vs ]≡ Q
             → x ⦅ w ⦆ P α[ ks ↦ vs ]≡ y ⦅ z ⦆ Q
    output   : (x , y) ∈² (ks , vs)
             → (w , z) ∈² (ks , vs)
             → P α[ ks ↦ vs ]≡ Q
             → x ⟨ w ⟩ P α[ ks ↦ vs ]≡ (y ⟨ z ⟩ Q)

  -- Translating a well-scoped process to de Bruijn and back results in the same process
  -- modulo alpha renaming, where the new names in `apply isf` map to the old in `ctx`

  toRaw∘fromRaw : (ctx : Ctx n) (P : Raw) (wsP : WellScoped ctx P)
                → toRaw ctx (fromRaw' ctx P wsP) α[ apply ctx ↦ ctx ]≡ P
  toRaw∘fromRaw ctx 𝟘 wsP = inaction
  toRaw∘fromRaw ctx (⦅ν x ⦆ P) wsP
    = scope (toRaw∘fromRaw (x ∷ ctx) P wsP)
  toRaw∘fromRaw ctx (P ∥ Q) (wsP , wsQ)
    = comp (toRaw∘fromRaw ctx P wsP)
           (toRaw∘fromRaw ctx Q wsQ)
  toRaw∘fromRaw ctx (x ⦅ y ⦆ P) (x∈ctx , wsP)
    = input (_ , refl , toName∘fromName x∈ctx)
            (toRaw∘fromRaw (y ∷ ctx) P wsP)
  toRaw∘fromRaw ctx (x ⟨ y ⟩ P) (x∈ctx , y∈ctx , wsP)
    = output (_ , refl , toName∘fromName x∈ctx)
             (_ , refl , toName∘fromName y∈ctx)
             (toRaw∘fromRaw ctx P wsP)

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
{-# OPTIONS --warning=error --safe --without-K #-}

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Numbers.Naturals.Order.WellFounded
open import Orders.WellFounded.Induction
open import Orders.Total.Definition
open import Semirings.Definition

module Numbers.Naturals.EuclideanAlgorithm where

open TotalOrder ℕTotalOrder
open Semiring ℕSemiring
open import Decidable.Lemmas ℕDecideEquality

record divisionAlgResult (a : ℕ) (b : ℕ) : Set where
  field
    quot : ℕ
    rem : ℕ
    pr : a *N quot +N rem ≡ b
    remIsSmall : (rem <N a) || (a ≡ 0)
    quotSmall : (0 <N a) || ((0 ≡ a) && (quot ≡ 0))

record divisionAlgResult' (a : ℕ) (b : ℕ) : Set where
  field
    quot : ℕ
    rem : ℕ
    .pr : a *N quot +N rem ≡ b
    remIsSmall : (rem <N' a) || (a =N' 0)
    quotSmall : (0 <N' a) || ((0 =N' a) && (quot =N' 0))

collapseDivAlgResult : {a b : ℕ} → (divisionAlgResult a b) → divisionAlgResult' a b
collapseDivAlgResult record { quot = q ; rem = r ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inl y) } = record { quot = q ; rem = r ; pr = pr ; remIsSmall = inl (<NTo<N' x) ; quotSmall = inl (<NTo<N' y) }
collapseDivAlgResult record { quot = q ; rem = r ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inr y) } = record { quot = q ; rem = r ; pr = pr ; remIsSmall = inl (<NTo<N' x) ; quotSmall = inr (collapseN (_&&_.fst y) ,, collapseN (_&&_.snd y)) }
collapseDivAlgResult record { quot = q ; rem = r ; pr = pr ; remIsSmall = (inr x) ; quotSmall = inl y } = record { quot = q ; rem = r ; pr = pr ; remIsSmall = inr (collapseN x) ; quotSmall = inl (<NTo<N' y) }
collapseDivAlgResult record { quot = q ; rem = r ; pr = pr ; remIsSmall = (inr x) ; quotSmall = inr y } = record { quot = q ; rem = r ; pr = pr ; remIsSmall = inr (collapseN x) ; quotSmall = inr (collapseN (_&&_.fst y) ,, collapseN (_&&_.snd y)) }

squashDivAlgResult : {a b : ℕ} → divisionAlgResult' a b → divisionAlgResult a b
squashDivAlgResult record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inl y) } = record { quot = quot ; rem = rem ; pr = squash pr ; remIsSmall = inl (<N'To<N x) ; quotSmall = inl (<N'To<N y) }
squashDivAlgResult record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inr y) } = record { quot = quot ; rem = rem ; pr = squash pr ; remIsSmall = inl (<N'To<N x) ; quotSmall = inr (squashN (_&&_.fst y) ,, squashN (_&&_.snd y)) }
squashDivAlgResult record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr x) ; quotSmall = (inl y) } = record { quot = quot ; rem = rem ; pr = squash pr ; remIsSmall = inr (squashN x) ; quotSmall = inl (<N'To<N y) }
squashDivAlgResult record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr x) ; quotSmall = (inr y) } = record { quot = quot ; rem = rem ; pr = squash pr ; remIsSmall = inr (squashN x) ; quotSmall = inr (squashN (_&&_.fst y) ,, squashN (_&&_.snd y)) }

squashPreservesRem : {a b : ℕ} → (p : divisionAlgResult' a b) → divisionAlgResult.rem (squashDivAlgResult p) ≡ divisionAlgResult'.rem p
squashPreservesRem record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inl x₁) } = refl
squashPreservesRem record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inr x₁) } = refl
squashPreservesRem record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr x) ; quotSmall = (inl x₁) } = refl
squashPreservesRem record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr x) ; quotSmall = (inr x₁) } = refl

squashPreservesQuot : {a b : ℕ} → (p : divisionAlgResult' a b) → divisionAlgResult.quot (squashDivAlgResult p) ≡ divisionAlgResult'.quot p
squashPreservesQuot record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inl x₁) } = refl
squashPreservesQuot record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inr x₁) } = refl
squashPreservesQuot record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr x) ; quotSmall = (inl x₁) } = refl
squashPreservesQuot record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr x) ; quotSmall = (inr x₁) } = refl

collapsePreservesRem : {a b : ℕ} → (p : divisionAlgResult a b) → divisionAlgResult'.rem (collapseDivAlgResult p) ≡ divisionAlgResult.rem p
collapsePreservesRem record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inl x₁) } = refl
collapsePreservesRem record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inr x₁) } = refl
collapsePreservesRem record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr x) ; quotSmall = (inl x₁) } = refl
collapsePreservesRem record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr x) ; quotSmall = (inr x₁) } = refl

collapsePreservesQuot : {a b : ℕ} → (p : divisionAlgResult a b) → divisionAlgResult'.quot (collapseDivAlgResult p) ≡ divisionAlgResult.quot p
collapsePreservesQuot record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inl x₁) } = refl
collapsePreservesQuot record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) ; quotSmall = (inr x₁) } = refl
collapsePreservesQuot record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr x) ; quotSmall = (inl x₁) } = refl
collapsePreservesQuot record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr x) ; quotSmall = (inr x₁) } = refl

divAlgLessLemma : (a b : ℕ) → (0 <N a) → (r : divisionAlgResult a b) → (divisionAlgResult.quot r ≡ 0) || (divisionAlgResult.rem r <N b)
divAlgLessLemma zero b pr _ = exFalso (TotalOrder.irreflexive ℕTotalOrder pr)
divAlgLessLemma (succ a) b _ record { quot = zero ; rem = a%b ; pr = pr ; remIsSmall = remIsSmall } = inl refl
divAlgLessLemma (succ a) b _ record { quot = (succ a/b) ; rem = a%b ; pr = pr ; remIsSmall = remIsSmall } = inr record { x = a/b +N a *N succ (a/b) ; proof = pr }

modUniqueLemma : {rem1 rem2 a : ℕ} → (quot1 quot2 : ℕ) → rem1 <N a → rem2 <N a → a *N quot1 +N rem1 ≡ a *N quot2 +N rem2 → rem1 ≡ rem2
modUniqueLemma {rem1} {rem2} {a} zero zero rem1<a rem2<a pr rewrite Semiring.productZeroRight ℕSemiring a = pr
modUniqueLemma {rem1} {rem2} {a} zero (succ quot2) rem1<a rem2<a pr rewrite Semiring.productZeroRight ℕSemiring a | pr | multiplicationNIsCommutative a (succ quot2) | equalityCommutative (Semiring.+Associative ℕSemiring a (quot2 *N a) rem2) = exFalso (cannotAddAndEnlarge' {a} {quot2 *N a +N rem2} rem1<a)
modUniqueLemma {rem1} {rem2} {a} (succ quot1) zero rem1<a rem2<a pr rewrite Semiring.productZeroRight ℕSemiring a | equalityCommutative pr | multiplicationNIsCommutative a (succ quot1) | equalityCommutative (Semiring.+Associative ℕSemiring a (quot1 *N a) rem1) = exFalso (cannotAddAndEnlarge' {a} {quot1 *N a +N rem1} rem2<a)
modUniqueLemma {rem1} {rem2} {a} (succ quot1) (succ quot2) rem1<a rem2<a pr rewrite multiplicationNIsCommutative a (succ quot1) | multiplicationNIsCommutative a (succ quot2) | equalityCommutative (Semiring.+Associative ℕSemiring a (quot1 *N a) rem1) | equalityCommutative (Semiring.+Associative ℕSemiring a (quot2 *N a) rem2) = modUniqueLemma {rem1} {rem2} {a} quot1 quot2 rem1<a rem2<a (go {a}{quot1}{rem1}{quot2}{rem2} pr)
  where
    go : {a quot1 rem1 quot2 rem2 : ℕ} → (a +N (quot1 *N a +N rem1) ≡ a +N (quot2 *N a +N rem2)) → a *N quot1 +N rem1 ≡ a *N quot2 +N rem2
    go {a} {quot1} {rem1} {quot2} {rem2} pr rewrite multiplicationNIsCommutative quot1 a | multiplicationNIsCommutative quot2 a = canSubtractFromEqualityLeft {a} pr

modIsUnique : {a b : ℕ} → (div1 div2 : divisionAlgResult a b) → divisionAlgResult.rem div1 ≡ divisionAlgResult.rem div2
modIsUnique {zero} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = remIsSmall1 } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = remIsSmall } = transitivity pr1 (equalityCommutative pr)
modIsUnique {succ a} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = (inl y) } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) } = modUniqueLemma {rem1} {rem} {succ a} quot1 quot y x (transitivity pr1 (equalityCommutative pr))
modIsUnique {succ a} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = (inr ()) } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inl x) }
modIsUnique {succ a} {b} record { quot = quot1 ; rem = rem1 ; pr = pr1 ; remIsSmall = remIsSmall1 } record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = (inr ()) }

transferAddition : (a b c : ℕ) → (a +N b) +N c ≡ (a +N c) +N b
transferAddition a b c rewrite equalityCommutative (Semiring.+Associative ℕSemiring a b c) = p a b c
  where
    p : (a b c : ℕ) → a +N (b +N c) ≡ (a +N c) +N b
    p a b c = transitivity (applyEquality (a +N_) (Semiring.commutative ℕSemiring b c)) (Semiring.+Associative ℕSemiring a c b)

divisionAlgLemma : (x b : ℕ) → x *N zero +N b ≡ b
divisionAlgLemma x b rewrite (Semiring.productZeroRight ℕSemiring x) = refl

divisionAlgLemma2 : (x b : ℕ) → (x ≡ b) → x *N succ zero +N zero ≡ b
divisionAlgLemma2 x b pr rewrite (Semiring.productOneRight ℕSemiring x) = equalityCommutative (transitivity (equalityCommutative pr) (equalityCommutative (Semiring.sumZeroRight ℕSemiring x)))

divisionAlgLemma3 : {a x : ℕ} → (p : succ a <N succ x) → (subtractionNResult.result (-N (inl p))) <N (succ x)
divisionAlgLemma3 {a} {x} p = -NIsDecreasing {a} {succ x} p

divisionAlgLemma4 : (p a q : ℕ) → ((p +N a *N p) +N q) +N succ a ≡ succ ((p +N a *N succ p) +N q)
divisionAlgLemma4 p a q = ans
  where
    r   : ((p +N a *N p) +N q) +N succ a ≡ succ (((p +N a *N p) +N q) +N a)
    ans : ((p +N a *N p) +N q) +N succ a ≡ succ ((p +N a *N succ p) +N q)
    s : ((p +N a *N p) +N q) +N a ≡ (p +N a *N succ p) +N q
    t : (p +N a *N p) +N a ≡ p +N a *N succ p
    s = transitivity (transferAddition (p +N a *N p) q a) (applyEquality (λ i → i +N q) t)
    ans = identityOfIndiscernablesRight _≡_ r (applyEquality succ s)
    r = succExtracts ((p +N a *N p) +N q) a
    t = transitivity (equalityCommutative (Semiring.+Associative ℕSemiring p (a *N p) a)) (applyEquality (λ n → p +N n) (equalityCommutative (transitivity (multiplicationNIsCommutative a (succ p)) (transitivity (Semiring.commutative ℕSemiring a _) (applyEquality (_+N a) (multiplicationNIsCommutative p _))))))

divisionAlg : (a : ℕ) → (b : ℕ) → divisionAlgResult a b
divisionAlg zero = λ b → record { quot = zero ; rem = b ; pr = refl ; remIsSmall = inr refl ; quotSmall = inr (record { fst = refl ; snd = refl }) }
divisionAlg (succ a) = rec <NWellfounded (λ n → divisionAlgResult (succ a) n) go
  where
    go : (x : ℕ) (indHyp : (y : ℕ) (y<x : y <N x) → divisionAlgResult (succ a) y) →
            divisionAlgResult (succ a) x
    go zero prop = record { quot = zero ; rem = zero ; pr = divisionAlgLemma (succ a) zero ; remIsSmall = inl (succIsPositive a) ; quotSmall = inl (succIsPositive a) }
    go (succ x) indHyp with totality (succ a) (succ x)
    go (succ x) indHyp | inl (inl sa<sx) with indHyp (subtractionNResult.result (-N (inl sa<sx))) (divisionAlgLemma3 sa<sx)
    ... | record { quot = prevQuot ; rem = prevRem ; pr = prevPr ; remIsSmall = smallRem } = p
      where
        p : divisionAlgResult (succ a) (succ x)
        addedA : (succ a *N prevQuot +N prevRem) +N (succ a) ≡ subtractionNResult.result (-N (inl sa<sx)) +N (succ a)
        addedA' : (succ a *N prevQuot +N prevRem) +N succ a ≡ succ x
        addedA'' : (succ a *N succ prevQuot) +N prevRem ≡ succ x
        addedA''' : succ ((prevQuot +N a *N succ prevQuot) +N prevRem) ≡ succ x
        addedA''' = identityOfIndiscernablesLeft _≡_ addedA'' refl
        p = record { quot = succ prevQuot ; rem = prevRem ; pr = addedA''' ; remIsSmall = smallRem ; quotSmall = inl (succIsPositive a) }
        addedA = applyEquality (λ n → n +N succ a) prevPr
        addedA' = identityOfIndiscernablesRight _≡_ addedA (addMinus {succ a} {succ x} (inl sa<sx))
        addedA'' = identityOfIndiscernablesLeft _≡_ addedA' (divisionAlgLemma4 prevQuot a prevRem)
    go (succ x) indHyp | inr (sa=sx) = record { quot = succ zero ; rem = zero ; pr = divisionAlgLemma2 (succ a) (succ x) sa=sx ; remIsSmall = inl (succIsPositive a) ; quotSmall = inl (succIsPositive a) }
    go (succ x) indHyp | inl (inr (sx<sa)) = record { quot = zero ; rem = succ x ; pr = divisionAlgLemma (succ a) (succ x) ; remIsSmall = inl sx<sa ; quotSmall = inl (succIsPositive a) }

data _∣_ : ℕ → ℕ → Set where
  divides : {a b : ℕ} → (res : divisionAlgResult a b) → divisionAlgResult.rem res ≡ zero → a ∣ b

data _∣'_ : ℕ → ℕ → Set where
  divides' : {a b : ℕ} → (res : divisionAlgResult' a b) → .(divisionAlgResult'.rem res ≡ zero) → a ∣' b

divToDiv' : {a b : ℕ} → a ∣ b → a ∣' b
divToDiv' (divides res x) = divides' (collapseDivAlgResult res) (transitivity (collapsePreservesRem res) x)

div'ToDiv : {a b : ℕ} → a ∣' b → a ∣ b
div'ToDiv (divides' res x) = divides (squashDivAlgResult res) (transitivity (squashPreservesRem res) (squashN record { eq = x }))

zeroDividesNothing : (a : ℕ) → zero ∣ succ a → False
zeroDividesNothing a (divides record { quot = quot ; rem = rem ; pr = pr } x) = naughtE p
  where
    p : zero ≡ succ a
    p = transitivity (equalityCommutative x) pr

record hcfData (a b : ℕ) : Set where
  field
    c : ℕ
    c|a : c ∣ a
    c|b : c ∣ b
    hcf : ∀ x → x ∣ a → x ∣ b → x ∣ c

positiveTimes : {a b : ℕ} → (succ a *N succ b <N succ a) → False
positiveTimes {a} {b} pr = zeroNeverGreater f'
  where
    g : succ a *N succ b <N succ a *N succ 0
    g rewrite multiplicationNIsCommutative a 1 | Semiring.commutative ℕSemiring a 0 = pr
    f : succ b <N succ 0
    f = cancelInequalityLeft {succ a} {succ b} g
    f' : b <N 0
    f' = canRemoveSuccFrom<N f

biggerThanCantDivideLemma : {a b : ℕ} → (a <N b) → (b ∣ a) → a ≡ 0
biggerThanCantDivideLemma {zero} {b} a<b b|a = refl
biggerThanCantDivideLemma {succ a} {zero} a<b (divides record { quot = quot ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = (inl (le x ())) } refl)
biggerThanCantDivideLemma {succ a} {zero} a<b (divides record { quot = quot ; rem = .0 ; pr = () ; remIsSmall = remIsSmall ; quotSmall = (inr x) } refl)
biggerThanCantDivideLemma {succ a} {succ b} a<b (divides record { quot = zero ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } refl) rewrite Semiring.commutative ℕSemiring (b *N zero) 0 | multiplicationNIsCommutative b 0 = exFalso (naughtE pr)
biggerThanCantDivideLemma {succ a} {succ b} a<b (divides record { quot = (succ quot) ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } refl) rewrite Semiring.commutative ℕSemiring (quot +N b *N succ quot) 0 | equalityCommutative pr = exFalso (positiveTimes {b} {quot} a<b)

biggerThanCantDivide : {a b : ℕ} → (x : ℕ) → (TotalOrder.max ℕTotalOrder a b) <N x → (x ∣ a) → (x ∣ b) → (a ≡ 0) && (b ≡ 0)
biggerThanCantDivide {a} {b} x pr x|a x|b with totality a b
biggerThanCantDivide {a} {b} x pr x|a x|b | inl (inl a<b) = exFalso (zeroNeverGreater f')
  where
    f : b ≡ 0
    f = biggerThanCantDivideLemma pr x|b
    f' : a <N 0
    f' rewrite equalityCommutative f = a<b
biggerThanCantDivide {a} {b} x pr x|a x|b | inl (inr b<a) = exFalso (zeroNeverGreater f')
  where
    f : a ≡ 0
    f = biggerThanCantDivideLemma pr x|a
    f' : b <N 0
    f' rewrite equalityCommutative f = b<a
biggerThanCantDivide {a} {b} x pr x|a x|b | inr a=b = (transitivity a=b f ,, f)
  where
    f : b ≡ 0
    f = biggerThanCantDivideLemma pr x|b

aDivA : (a : ℕ) → a ∣ a
aDivA zero = divides (record { quot = 0 ; rem = 0 ; pr = equalityCommutative (oneTimesPlusZero zero) ; remIsSmall = inr refl ; quotSmall = inr (refl ,, refl) }) refl
aDivA (succ a) = divides (record { quot = 1 ; rem = 0 ; pr = equalityCommutative (oneTimesPlusZero (succ a)) ; remIsSmall = inl (succIsPositive a) ; quotSmall = inl (succIsPositive a) }) refl

aDivZero : (a : ℕ) → a ∣ zero
aDivZero zero = aDivA zero
aDivZero (succ a) = divides (record { quot = zero ; rem = zero ; pr = lemma (succ a) ; remIsSmall = inl (succIsPositive a) ; quotSmall = inl (succIsPositive a) }) refl
  where
    lemma : (b : ℕ) → b *N zero +N zero ≡ zero
    lemma b rewrite (Semiring.sumZeroRight ℕSemiring (b *N zero)) = Semiring.productZeroRight ℕSemiring b

record extendedHcf (a b : ℕ) : Set where
  field
    hcf : hcfData a b
  c : ℕ
  c = hcfData.c hcf
  field
    extended1 : ℕ
    extended2 : ℕ
    extendedProof : (a *N extended1 ≡ b *N extended2 +N c) || (a *N extended1 +N c ≡ b *N extended2)

divEqualityLemma1 : {a b c : ℕ} → b ≡ zero → b *N c +N 0 ≡ a → a ≡ b
divEqualityLemma1 {a} {.0} {c} refl pr = equalityCommutative pr

divEquality : {a b : ℕ} → a ∣ b → b ∣ a → a ≡ b
divEquality {a} {b} (divides record { quot = quotAB ; rem = .0 ; pr = prAB ; remIsSmall = _ ; quotSmall = quotSmallAB } refl) (divides record { quot = quot ; rem = .0 ; pr = pr ; remIsSmall = _ ; quotSmall = (inl x) } refl) rewrite Semiring.commutative ℕSemiring (b *N quot) 0 | Semiring.commutative ℕSemiring (a *N quotAB) 0 | equalityCommutative pr | equalityCommutative (Semiring.*Associative ℕSemiring b quot quotAB) = res
  where
    lem : {b r : ℕ} → b *N r ≡ b → (0 <N b) → r ≡ 1
    lem {zero} {r} pr ()
    lem {succ b} {zero} pr _ rewrite multiplicationNIsCommutative b 0 = exFalso (naughtE pr)
    lem {succ b} {succ zero} pr _ = refl
    lem {succ b} {succ (succ r)} pr _ rewrite multiplicationNIsCommutative b (succ (succ r)) | Semiring.commutative ℕSemiring (succ r) (b +N (b +N r *N b)) | equalityCommutative (Semiring.+Associative ℕSemiring b (b +N r *N b) (succ r)) | Semiring.commutative ℕSemiring (b +N r *N b) (succ r) = exFalso (cannotAddAndEnlarge'' {succ b} pr)
    p : quot *N quotAB ≡ 1
    p = lem prAB x
    q : quot ≡ 1
    q = _&&_.fst (productOneImpliesOperandsOne p)
    res : b *N quot ≡ b
    res rewrite q | multiplicationNIsCommutative b 1 | Semiring.commutative ℕSemiring b 0 = refl
divEquality {.0} {.0} (divides record { quot = quotAB ; rem = .0 ; pr = prAB ; remIsSmall = _ ; quotSmall = quotSmallAB } refl) (divides record { quot = quot ; rem = .0 ; pr = refl ; remIsSmall = _ ; quotSmall = (inr (refl ,, snd)) } refl) = refl

hcfWelldefined : {a b : ℕ} → (ab : hcfData a b) → (ab' : hcfData a b) → (hcfData.c ab ≡ hcfData.c ab')
hcfWelldefined {a} {b} record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } record { c = c' ; c|a = c|a' ; c|b = c|b' ; hcf = hcf' } with hcf c' c|a' c|b'
... | c'DivC with hcf' c c|a c|b
... | cDivC' = divEquality cDivC' c'DivC

reverseHCF : {a b : ℕ} → (ab : extendedHcf a b) → extendedHcf b a
reverseHCF {a} {b} record { hcf = record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } ; extended1 = extended1 ; extended2 = extended2 ; extendedProof = (inl x) } = record { hcf = record { c = c ; c|a = c|b ; c|b = c|a ; hcf = λ x z z₁ → hcf x z₁ z } ; extended1 = extended2 ; extended2 = extended1 ; extendedProof = inr (equalityCommutative x) }
reverseHCF {a} {b} record { hcf = record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } ; extended1 = extended1 ; extended2 = extended2 ; extendedProof = (inr x) } = record { hcf = record { c = c ; c|a = c|b ; c|b = c|a ; hcf = λ x z z₁ → hcf x z₁ z } ; extended1 = extended2 ; extended2 = extended1 ; extendedProof = inl (equalityCommutative x) }

oneDivN : (a : ℕ) → 1 ∣ a
oneDivN a = divides (record { quot = a ; rem = zero ; pr = pr ; remIsSmall = inl (succIsPositive zero) ; quotSmall = inl (le zero refl) }) refl
  where
    pr : (a +N zero) +N zero ≡ a
    pr rewrite Semiring.sumZeroRight ℕSemiring (a +N zero) = Semiring.sumZeroRight ℕSemiring a

hcfZero : (a : ℕ) → extendedHcf zero a
hcfZero a = record { hcf = record { c = a ; c|a = aDivZero a ; c|b = aDivA a ; hcf = λ _ _ p → p } ; extended1 = 0 ; extended2 = 1 ; extendedProof = inr (equalityCommutative (Semiring.productOneRight ℕSemiring a))}

hcfOne : (a : ℕ) → extendedHcf 1 a
hcfOne a = record { hcf = record { c = 1 ; c|a = aDivA 1 ; c|b = oneDivN a ; hcf = λ _ z _ → z } ; extended1 = 1 ; extended2 = 0 ; extendedProof = inl g }
  where
    g : 1 ≡ a *N 0 +N 1
    g rewrite multiplicationNIsCommutative a 0 = refl

zeroIsValidRem : (a : ℕ) → (0 <N a) || (a ≡ 0)
zeroIsValidRem zero = inr refl
zeroIsValidRem (succ a) = inl (succIsPositive a)

dividesBothImpliesDividesSum : {a x y : ℕ} → a ∣ x → a ∣ y → a ∣ (x +N y)
dividesBothImpliesDividesSum {a} {x} {y} (divides record { quot = xDivA ; rem = .0 ; pr = prA ; quotSmall = qsm1 } refl) (divides record { quot = quot ; rem = .0 ; pr = pr ; quotSmall = qsm2 } refl) = divides (record { quot = xDivA +N quot ; rem = 0 ; pr = go {a} {x} {y} {xDivA} {quot} pr prA ; remIsSmall = zeroIsValidRem a ; quotSmall = (quotSmall qsm1 qsm2) }) refl
  where
    go : {a x y quot quot2 : ℕ} → (a *N quot2 +N zero ≡ y) → (a *N quot +N zero ≡ x) → a *N (quot +N quot2) +N zero ≡ x +N y
    go {a} {x} {y} {quot} {quot2} pr1 pr2 rewrite Semiring.sumZeroRight ℕSemiring (a *N quot) = identityOfIndiscernablesLeft _≡_ t (equalityCommutative (Semiring.sumZeroRight ℕSemiring (a *N (quot +N quot2))))
      where
        t : a *N (quot +N quot2) ≡ x +N y
        t rewrite Semiring.sumZeroRight ℕSemiring (a *N quot2) = transitivity (Semiring.+DistributesOver* ℕSemiring a quot quot2) p
          where
            s : a *N quot +N a *N quot2 ≡ x +N a *N quot2
            s = applyEquality (λ n → n +N a *N quot2) pr2
            r : x +N a *N quot2 ≡ x +N y
            r = applyEquality (λ n → x +N n) pr1
            p : a *N quot +N a *N quot2 ≡ x +N y
            p = transitivity s r
    quotSmall : ((0 <N a) || ((0 ≡ a) && (xDivA ≡ 0))) → ((0 <N a) || ((0 ≡ a) && (quot ≡ 0))) → (0 <N a) || ((0 ≡ a) && (xDivA +N quot ≡ 0))
    quotSmall (inl x1) (inl x2) = inl x1
    quotSmall (inl x1) (inr x2) = inl x1
    quotSmall (inr x1) (inl x2) = inl x2
    quotSmall (inr (a=0 ,, bl)) (inr (_ ,, bl2)) = inr (a=0 ,, ans)
      where
        ans : xDivA +N quot ≡ 0
        ans rewrite bl | bl2 = refl

dividesBothImpliesDividesDifference : {a b c : ℕ} → a ∣ b → a ∣ c → (c<b : c <N b) → a ∣ (subtractionNResult.result (-N (inl c<b)))
dividesBothImpliesDividesDifference {zero} {b} {.0} prab (divides record { quot = quot ; rem = .0 ; pr = refl } refl) c<b = prab
dividesBothImpliesDividesDifference {succ a} {b} {c} (divides record { quot = bDivSA ; rem = .0 ; pr = pr } refl) (divides record { quot = cDivSA ; rem = .0 ; pr = pr2 } refl) c<b rewrite (Semiring.sumZeroRight ℕSemiring (succ a *N cDivSA)) | (Semiring.sumZeroRight ℕSemiring (succ a *N bDivSA)) = divides (record { quot = subtractionNResult.result bDivSA-cDivSA ; rem = 0 ; pr = identityOfIndiscernablesLeft _≡_ (identityOfIndiscernablesLeft _≡_ s (equalityCommutative q)) (equalityCommutative (Semiring.sumZeroRight ℕSemiring _)) ; remIsSmall = inl (succIsPositive a) ; quotSmall = inl (succIsPositive a) }) refl
  where
    p : cDivSA <N bDivSA
    p rewrite (equalityCommutative pr2) | (equalityCommutative pr) = cancelInequalityLeft {succ a} {cDivSA} {bDivSA} c<b
    bDivSA-cDivSA : subtractionNResult cDivSA bDivSA (inl p)
    bDivSA-cDivSA = -N {cDivSA} {bDivSA} (inl p)
    la-ka = subtractionNResult.result (-N {succ a *N cDivSA} {succ a *N bDivSA} (inl (lessRespectsMultiplicationLeft cDivSA bDivSA (succ a) p (succIsPositive a))))
    q : (succ a *N (subtractionNResult.result bDivSA-cDivSA)) ≡ la-ka
    q = subtractProduct {succ a} {cDivSA} {bDivSA} (succIsPositive a) p
    s : la-ka ≡ subtractionNResult.result (-N {c} {b} (inl c<b))
    s = equivalentSubtraction (succ a *N cDivSA) b (succ a *N bDivSA) c (lessRespectsMultiplicationLeft cDivSA bDivSA (succ a) p (succIsPositive a)) c<b g
      where
        g : (succ a *N cDivSA) +N b ≡ (succ a *N bDivSA) +N c
        g rewrite equalityCommutative pr2 | equalityCommutative pr = Semiring.commutative ℕSemiring (cDivSA +N a *N cDivSA) (bDivSA +N a *N bDivSA)

euclidLemma1 : {a b : ℕ} → (a<b : a <N b) → (t : ℕ) → a +N b <N t → a +N (subtractionNResult.result (-N (inl a<b))) <N t
euclidLemma1 {zero} {b} zero<b t b<t = b<t
euclidLemma1 {succ a} {b} sa<b t sa+b<t = identityOfIndiscernablesLeft _<N_ q (Semiring.commutative ℕSemiring (subtractionNResult.result (-N (inl sa<b))) (succ a))
  where
    p : b <N t
    p = TotalOrder.<Transitive ℕTotalOrder (le a refl) sa+b<t
    q : (subtractionNResult.result (-N (inl sa<b))) +N succ a <N t
    q = identityOfIndiscernablesLeft _<N_ p (equalityCommutative (addMinus (inl sa<b)))

euclidLemma2 : {a b max : ℕ} → (succ (a +N b) <N max) → b <N max
euclidLemma2 {a} {b} {max} pr = lessTransitive {b} {succ (a +N b)} {max} (lemma a b) pr
  where
    lemma : (a b : ℕ) → b <N succ (a +N b)
    lemma a b rewrite Semiring.commutative ℕSemiring (succ a) b = addingIncreases b a

euclidLemma3 : {a b max : ℕ} → (succ (succ (a +N b)) <N max) → succ b <N max
euclidLemma3 {a} {b} {max} pr = euclidLemma2 {a} {succ b} {max} (identityOfIndiscernablesLeft _<N_ pr (applyEquality succ (equalityCommutative (succExtracts a b))))

euclidLemma4 : (a b c d h : ℕ) → (sa<b : (succ a) <N b) → (pr : subtractionNResult.result (-N (inl sa<b)) *N c ≡ (succ a) *N d +N h) → b *N c ≡ (succ a) *N (d +N c) +N h
euclidLemma4 a b zero d h sa<b pr rewrite Semiring.sumZeroRight ℕSemiring d | Semiring.productZeroRight ℕSemiring b | Semiring.productZeroRight ℕSemiring (subtractionNResult.result (-N (inl sa<b))) = pr
euclidLemma4 a b (succ c) d h sa<b pr rewrite subtractProduct' (succIsPositive c) sa<b = transitivity q' r'
  where
    q : (succ c) *N b ≡ succ (a +N c *N succ a) +N ((succ a) *N d +N h)
    q = moveOneSubtraction {succ (a +N c *N succ a)} {b +N c *N b} {(succ a) *N d +N h} {inl _} pr
    q' : b *N succ c ≡ succ (a +N c *N succ a) +N ((succ a) *N d +N h)
    q' rewrite multiplicationNIsCommutative b (succ c) = q
    r' : ((succ c) *N succ a) +N (((succ a) *N d) +N h) ≡ ((succ a) *N (d +N succ c)) +N h
    r' rewrite Semiring.+Associative ℕSemiring ((succ c) *N succ a) ((succ a) *N d) h = applyEquality (λ t → t +N h) {((succ c) *N succ a) +N ((succ a) *N d)} {(succ a) *N (d +N succ c)} (go (succ c) (succ a) d)
      where
        go' : (a b c : ℕ) → b *N a +N b *N c ≡ b *N (c +N a)
        go : (a b c : ℕ) → a *N b +N b *N c ≡ b *N (c +N a)
        go a b c rewrite multiplicationNIsCommutative a b = go' a b c
        go' a b c rewrite Semiring.commutative ℕSemiring (b *N a) (b *N c) = equalityCommutative (Semiring.+DistributesOver* ℕSemiring b c a)

euclidLemma5 : (a b c d h : ℕ) → (sa<b : (succ a) <N b) → (pr : subtractionNResult.result (-N (inl sa<b)) *N c +N h ≡ (succ a) *N d) → (succ a) *N (d +N c) ≡ b *N c +N h
euclidLemma5 a b c d h sa<b pr with (-N (inl sa<b))
euclidLemma5 a b zero d h sa<b pr | record { result = result ; pr = sub } rewrite Semiring.sumZeroRight ℕSemiring d | Semiring.productZeroRight ℕSemiring b | Semiring.productZeroRight ℕSemiring result = equalityCommutative pr
euclidLemma5 a b (succ c) d h sa<b pr | record { result = result ; pr = sub } rewrite subtractProduct' (succIsPositive c) sa<b | equalityCommutative sub = pv''
  where
    p : succ a *N d ≡ result *N succ c +N h
    p = equalityCommutative pr
    p' : a *N succ c +N succ a *N d ≡ (a *N succ c) +N ((result *N succ c) +N h)
    p' = applyEquality (λ t → a *N succ c +N t) p
    p'' : a *N succ c +N succ a *N d ≡ (a *N succ c +N result *N succ c) +N h
    p'' rewrite equalityCommutative (Semiring.+Associative ℕSemiring (a *N succ c) (result *N succ c) h) = p'
    p''' : a *N succ c +N succ a *N d ≡ (a +N result) *N succ c +N h
    p''' rewrite multiplicationNIsCommutative (a +N result) (succ c) | Semiring.+DistributesOver* ℕSemiring (succ c) a result | multiplicationNIsCommutative (succ c) a | multiplicationNIsCommutative (succ c) result = p''
    pv : c +N (a *N succ c +N succ a *N d) ≡ (c +N (a +N result) *N succ c) +N h
    pv rewrite equalityCommutative (Semiring.+Associative ℕSemiring c ((a +N result) *N succ c) h) = applyEquality (λ t → c +N t) p'''
    pv' : (succ c) +N (a *N succ c +N succ a *N d) ≡ succ ((c +N (a +N result) *N succ c) +N h)
    pv' = applyEquality succ pv
    pv'' : (succ a) *N (d +N succ c) ≡ succ ((c +N (a +N result) *N succ c) +N h)
    pv'' = identityOfIndiscernablesLeft _≡_ pv' (go a c d)
      where
        go : (a c d : ℕ) → (succ c) +N (a *N succ c +N ((succ a) *N d)) ≡ (succ a) *N (d +N succ c)
        go a c d rewrite Semiring.+Associative ℕSemiring (succ c) (a *N succ c) ((succ a) *N d) = go'
          where
            go' : (succ a) *N (succ c) +N (succ a) *N d ≡ (succ a) *N (d +N succ c)
            go' rewrite Semiring.commutative ℕSemiring d (succ c) = equalityCommutative (Semiring.+DistributesOver* ℕSemiring (succ a) (succ c) d)

euclid : (a b : ℕ) → extendedHcf a b
euclid a b = inducted (succ a +N b) a b (a<SuccA (a +N b))
  where
    P : ℕ → Set
    P sum = ∀ (a b : ℕ) → a +N b <N sum → extendedHcf a b
    go'' : {a b : ℕ} → (maxsum : ℕ) → (a <N b) → (a +N b <N maxsum) → (∀ y → y <N maxsum → P y) → extendedHcf a b
    go'' {zero} {b} maxSum zero<b b<maxsum indHyp = hcfZero b
    go'' {1} {b} maxSum 1<b b<maxsum indHyp = hcfOne b
    go'' {succ (succ a)} {b} maxSum ssa<b ssa+b<maxsum indHyp with (indHyp (succ b) (euclidLemma3 {a} {b} {maxSum} ssa+b<maxsum)) (subtractionNResult.result (-N (inl ssa<b))) (succ (succ a)) (identityOfIndiscernablesLeft _<N_ (a<SuccA b) (equalityCommutative (addMinus (inl ssa<b))))
    go'' {succ (succ a)} {b} maxSum ssa<b ssa+b<maxsum indHyp | record { hcf = record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } ; extended1 = extended1 ; extended2 = extended2 ; extendedProof = inl extendedProof } = record { hcf = record { c = c ; c|a = c|b ; c|b = hcfDivB'' ; hcf = λ div prDivSSA prDivB → hcf div (dividesBothImpliesDividesDifference prDivB prDivSSA ssa<b) prDivSSA } ; extended2 = extended1; extended1 = extended2 +N extended1 ; extendedProof = inr (equalityCommutative (euclidLemma4 (succ a) b extended1 extended2 c ssa<b extendedProof)) }
      where
        hcfDivB : c ∣ ((succ (succ a)) +N (subtractionNResult.result (-N (inl ssa<b))))
        hcfDivB = dividesBothImpliesDividesSum {c} {succ (succ a)} { subtractionNResult.result (-N (inl ssa<b))} c|b c|a
        hcfDivB' : c ∣ ((subtractionNResult.result (-N (inl ssa<b))) +N (succ (succ a)))
        hcfDivB' = identityOfIndiscernablesRight _∣_ hcfDivB (Semiring.commutative ℕSemiring (succ (succ a)) ( subtractionNResult.result (-N (inl ssa<b))))
        hcfDivB'' : c ∣ b
        hcfDivB'' = identityOfIndiscernablesRight _∣_ hcfDivB' (addMinus (inl ssa<b))
    go'' {succ (succ a)} {b} maxSum ssa<b ssa+b<maxsum indHyp | record { hcf = record { c = c ; c|a = c|a ; c|b = c|b ; hcf = hcf } ; extended1 = extended1 ; extended2 = extended2 ; extendedProof = inr extendedProof } = record { hcf = record { c = c ; c|a = c|b ; c|b = hcfDivB'' ; hcf = λ div prDivSSA prDivB → hcf div (dividesBothImpliesDividesDifference prDivB prDivSSA ssa<b) prDivSSA } ; extended2 = extended1; extended1 = extended2 +N extended1 ; extendedProof = inl (euclidLemma5 (succ a) b extended1 extended2 c ssa<b extendedProof) }
      where
        hcfDivB : c ∣ ((succ (succ a)) +N (subtractionNResult.result (-N (inl ssa<b))))
        hcfDivB = dividesBothImpliesDividesSum {c} {succ (succ a)} { subtractionNResult.result (-N (inl ssa<b))} c|b c|a
        hcfDivB' : c ∣ ((subtractionNResult.result (-N (inl ssa<b))) +N (succ (succ a)))
        hcfDivB' = identityOfIndiscernablesRight _∣_ hcfDivB (Semiring.commutative ℕSemiring (succ (succ a)) (subtractionNResult.result (-N (inl ssa<b))))
        hcfDivB'' : c ∣ b
        hcfDivB'' = identityOfIndiscernablesRight _∣_ hcfDivB' (addMinus (inl ssa<b))
    go' : (maxSum a b : ℕ) → (a +N b <N maxSum) → (∀ y → y <N maxSum → P y) → extendedHcf a b
    go' maxSum a b a+b<maxsum indHyp with totality a b
    go' maxSum a b a+b<maxsum indHyp | inl (inl a<b) = go'' maxSum a<b a+b<maxsum indHyp
    go' maxSum a b a+b<maxsum indHyp | inl (inr b<a) = reverseHCF (go'' maxSum b<a (identityOfIndiscernablesLeft _<N_ a+b<maxsum (Semiring.commutative ℕSemiring a b)) indHyp)
    go' maxSum a .a _ indHyp | inr refl = record { hcf = record { c = a ; c|a = aDivA a ; c|b = aDivA a ; hcf = λ _ _ z → z } ; extended1 = 0 ; extended2 = 1 ; extendedProof = inr s}
      where
        s : a *N zero +N a ≡ a *N 1
        s rewrite multiplicationNIsCommutative a zero | Semiring.productOneRight ℕSemiring a = refl
    go : ∀ x → (∀ y → y <N x → P y) → P x
    go maxSum indHyp = λ a b a+b<maxSum → go' maxSum a b a+b<maxSum indHyp
    inducted : ∀ x → P x
    inducted = rec <NWellfounded P go

divOneImpliesOne : {a : ℕ} → a ∣ 1 → a ≡ 1
divOneImpliesOne {zero} a|1 = exFalso (zeroDividesNothing _ a|1)
divOneImpliesOne {succ zero} a|1 = refl
divOneImpliesOne {succ (succ a)} (divides record { quot = zero ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } refl) rewrite Semiring.sumZeroRight ℕSemiring (a *N zero) | multiplicationNIsCommutative a 0 = exFalso (naughtE pr)
divOneImpliesOne {succ (succ a)} (divides record { quot = (succ quot) ; rem = .0 ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } refl) rewrite Semiring.commutative ℕSemiring quot (succ (quot +N a *N succ quot)) = exFalso (naughtE (equalityCommutative (succInjective pr)))


text:
{-# OPTIONS --cubical #-}

open import Agda.Builtin.Cubical.Path

data I : Set where
  zero one : I
  zero≡one : zero ≡ one

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Theory T from the paper
------------------------------------------------------------------------------

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

module T where

infixl 9 _·_  -- The symbol is '\cdot'.
infix  7 _≡_

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

postulate
  T        : Set
  zero K S : T
  succ     : T → T
  _·_      : T → T → T

-- The identity type on the universe of discourse.
data _≡_ (x : T) : T → Set where
  refl : x ≡ x

-- Conversion rules
postulate
  cK : ∀ x y → K · x · y         ≡ x
  cS : ∀ x y z → S · x ·  y ·  z ≡ x ·  z ·  (y ·  z)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --rewriting #-}

module Properties.Subtyping where

open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_)
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src; tgt)
open import Properties.Contradiction using (CONTRADICTION; ¬)
open import Properties.Equality using (_≢_)
open import Properties.Functions using (_∘_)
open import Properties.Product using (_×_; _,_)

-- Language membership is decidable
dec-language : ∀ T t → Either (¬Language T t) (Language T t)
dec-language nil (scalar number) = Left (scalar-scalar number nil (λ ()))
dec-language nil (scalar boolean) = Left (scalar-scalar boolean nil (λ ()))
dec-language nil (scalar string) = Left (scalar-scalar string nil (λ ()))
dec-language nil (scalar nil) = Right (scalar nil)
dec-language nil function = Left (scalar-function nil)
dec-language nil (function-ok t) = Left (scalar-function-ok nil)
dec-language nil (function-err t) = Right (scalar-function-err nil)
dec-language boolean (scalar number) = Left (scalar-scalar number boolean (λ ()))
dec-language boolean (scalar boolean) = Right (scalar boolean)
dec-language boolean (scalar string) = Left (scalar-scalar string boolean (λ ()))
dec-language boolean (scalar nil) = Left (scalar-scalar nil boolean (λ ()))
dec-language boolean function = Left (scalar-function boolean)
dec-language boolean (function-ok t) = Left (scalar-function-ok boolean)
dec-language boolean (function-err t) = Right (scalar-function-err boolean)
dec-language number (scalar number) = Right (scalar number)
dec-language number (scalar boolean) = Left (scalar-scalar boolean number (λ ()))
dec-language number (scalar string) = Left (scalar-scalar string number (λ ()))
dec-language number (scalar nil) = Left (scalar-scalar nil number (λ ()))
dec-language number function = Left (scalar-function number)
dec-language number (function-ok t) = Left (scalar-function-ok number)
dec-language number (function-err t) = Right (scalar-function-err number)
dec-language string (scalar number) = Left (scalar-scalar number string (λ ()))
dec-language string (scalar boolean) = Left (scalar-scalar boolean string (λ ()))
dec-language string (scalar string) = Right (scalar string)
dec-language string (scalar nil) = Left (scalar-scalar nil string (λ ()))
dec-language string function = Left (scalar-function string)
dec-language string (function-ok t) = Left (scalar-function-ok string)
dec-language string (function-err t) = Right (scalar-function-err string)
dec-language (T₁ ⇒ T₂) (scalar s) = Left (function-scalar s)
dec-language (T₁ ⇒ T₂) function = Right function
dec-language (T₁ ⇒ T₂) (function-ok t) = mapLR function-ok function-ok (dec-language T₂ t)
dec-language (T₁ ⇒ T₂) (function-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t))
dec-language never t = Left never
dec-language unknown t = Right unknown
dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t)
dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t)

-- ¬Language T is the complement of Language T
language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t)
language-comp t (p₁ , p₂) (left q) = language-comp t p₁ q
language-comp t (p₁ , p₂) (right q) = language-comp t p₂ q
language-comp t (left p) (q₁ , q₂) = language-comp t p q₁
language-comp t (right p) (q₁ , q₂) = language-comp t p q₂
language-comp (scalar s) (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl
language-comp (scalar s) (function-scalar s) (scalar s) = language-comp function (scalar-function s) function
language-comp (scalar s) never (scalar ())
language-comp function (scalar-function ()) function
language-comp (function-ok t) (scalar-function-ok ()) (function-ok q)
language-comp (function-ok t) (function-ok p) (function-ok q) = language-comp t p q
language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p

-- ≮: is the complement of <:
¬≮:-impl-<: : ∀ {T U} → ¬(T ≮: U) → (T <: U)
¬≮:-impl-<: {T} {U} p t q with dec-language U t
¬≮:-impl-<: {T} {U} p t q | Left r = CONTRADICTION (p (witness t q r))
¬≮:-impl-<: {T} {U} p t q | Right r = r

<:-impl-¬≮: : ∀ {T U} → (T <: U) → ¬(T ≮: U)
<:-impl-¬≮: p (witness t q r) = language-comp t r (p t q)

-- reflexivity
≮:-refl : ∀ {T} → ¬(T ≮: T)
≮:-refl (witness t p q) = language-comp t q p

<:-refl : ∀ {T} → (T <: T)
<:-refl = ¬≮:-impl-<: ≮:-refl

-- transititivity
≮:-trans-≡ : ∀ {S T U} → (S ≮: T) → (T ≡ U) → (S ≮: U)
≮:-trans-≡ p refl = p

≡-trans-≮: : ∀ {S T U} → (S ≡ T) → (T ≮: U) → (S ≮: U)
≡-trans-≮: refl p = p

≮:-trans : ∀ {S T U} → (S ≮: U) → Either (S ≮: T) (T ≮: U)
≮:-trans {T = T} (witness t p q) = mapLR (witness t p) (λ z → witness t z q) (dec-language T t)

<:-trans : ∀ {S T U} → (S <: T) → (T <: U) → (S <: U)
<:-trans p q = ¬≮:-impl-<: (cond (<:-impl-¬≮: p) (<:-impl-¬≮: q) ∘ ≮:-trans)

-- Properties of scalars
skalar = number ∪ (string ∪ (nil ∪ boolean))

function-≮:-scalar : ∀ {S T U} → (Scalar U) → ((S ⇒ T) ≮: U)
function-≮:-scalar s = witness function function (scalar-function s)

scalar-≮:-function : ∀ {S T U} → (Scalar U) → (U ≮: (S ⇒ T))
scalar-≮:-function s = witness (scalar s) (scalar s) (function-scalar s)

unknown-≮:-scalar : ∀ {U} → (Scalar U) → (unknown ≮: U)
unknown-≮:-scalar s = witness (function-ok (scalar s)) unknown (scalar-function-ok s)

scalar-≮:-never : ∀ {U} → (Scalar U) → (U ≮: never)
scalar-≮:-never s = witness (scalar s) (scalar s) never

scalar-≢-impl-≮: : ∀ {T U} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ≮: U)
scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-scalar s₁ s₂ p)

-- Properties of tgt
tgt-function-ok : ∀ {T t} → (Language (tgt T) t) → Language T (function-ok t)
tgt-function-ok {T = nil} (scalar ())
tgt-function-ok {T = T₁ ⇒ T₂} p = function-ok p
tgt-function-ok {T = never} (scalar ())
tgt-function-ok {T = unknown} p = unknown
tgt-function-ok {T = boolean} (scalar ())
tgt-function-ok {T = number} (scalar ())
tgt-function-ok {T = string} (scalar ())
tgt-function-ok {T = T₁ ∪ T₂} (left p) = left (tgt-function-ok p)
tgt-function-ok {T = T₁ ∪ T₂} (right p) = right (tgt-function-ok p)
tgt-function-ok {T = T₁ ∩ T₂} (p₁ , p₂) = (tgt-function-ok p₁ , tgt-function-ok p₂)

function-ok-tgt : ∀ {T t} → Language T (function-ok t) → (Language (tgt T) t)
function-ok-tgt (function-ok p) = p
function-ok-tgt (left p) = left (function-ok-tgt p)
function-ok-tgt (right p) = right (function-ok-tgt p)
function-ok-tgt (p₁ , p₂) = (function-ok-tgt p₁ , function-ok-tgt p₂)
function-ok-tgt unknown = unknown

skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t))
skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean)))

skalar-scalar : ∀ {T} (s : Scalar T) → (Language skalar (scalar s))
skalar-scalar number = left (scalar number)
skalar-scalar boolean = right (right (right (scalar boolean)))
skalar-scalar string = right (left (scalar string))
skalar-scalar nil = right (right (left (scalar nil)))

tgt-never-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (never ⇒ U)))
tgt-never-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q)

never-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (never ⇒ U))) → (tgt T ≮: U)
never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁))
never-tgt-≮: (witness function p (q₁ , scalar-function ()))
never-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂
never-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ())))

-- Properties of src
function-err-src : ∀ {T t} → (¬Language (src T) t) → Language T (function-err t)
function-err-src {T = nil} never = scalar-function-err nil
function-err-src {T = T₁ ⇒ T₂} p = function-err p
function-err-src {T = never} (scalar-scalar number () p)
function-err-src {T = never} (scalar-function-ok ())
function-err-src {T = unknown} never = unknown
function-err-src {T = boolean} p = scalar-function-err boolean
function-err-src {T = number} p = scalar-function-err number
function-err-src {T = string} p = scalar-function-err string
function-err-src {T = T₁ ∪ T₂} (left p) = left (function-err-src p)
function-err-src {T = T₁ ∪ T₂} (right p) = right (function-err-src p)
function-err-src {T = T₁ ∩ T₂} (p₁ , p₂) = function-err-src p₁ , function-err-src p₂

¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t)
¬function-err-src {T = nil} (scalar ())
¬function-err-src {T = T₁ ⇒ T₂} p = function-err p
¬function-err-src {T = never} unknown = never
¬function-err-src {T = unknown} (scalar ())
¬function-err-src {T = boolean} (scalar ())
¬function-err-src {T = number} (scalar ())
¬function-err-src {T = string} (scalar ())
¬function-err-src {T = T₁ ∪ T₂} (p₁ , p₂) = (¬function-err-src p₁ , ¬function-err-src p₂)
¬function-err-src {T = T₁ ∩ T₂} (left p) = left (¬function-err-src p)
¬function-err-src {T = T₁ ∩ T₂} (right p) = right (¬function-err-src p)

src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t)
src-¬function-err {T = nil} p = never
src-¬function-err {T = T₁ ⇒ T₂} (function-err p) = p
src-¬function-err {T = never} (scalar-function-err ())
src-¬function-err {T = unknown} p = never
src-¬function-err {T = boolean} p = never
src-¬function-err {T = number} p = never
src-¬function-err {T = string} p = never
src-¬function-err {T = T₁ ∪ T₂} (left p) = left (src-¬function-err p)
src-¬function-err {T = T₁ ∪ T₂} (right p) = right (src-¬function-err p)
src-¬function-err {T = T₁ ∩ T₂} (p₁ , p₂) = (src-¬function-err p₁ , src-¬function-err p₂)

src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t)
src-¬scalar number (scalar number) = never
src-¬scalar boolean (scalar boolean) = never
src-¬scalar string (scalar string) = never
src-¬scalar nil (scalar nil) = never
src-¬scalar s (left p) = left (src-¬scalar s p)
src-¬scalar s (right p) = right (src-¬scalar s p)
src-¬scalar s (p₁ , p₂) = (src-¬scalar s p₁ , src-¬scalar s p₂)
src-¬scalar s unknown = never

src-unknown-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ unknown))
src-unknown-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p)

unknown-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ unknown)) → (U ≮: src T)
unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p)
unknown-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q)))
unknown-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ())))
unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)

-- Properties of unknown and never
unknown-≮: : ∀ {T U} → (T ≮: U) → (unknown ≮: U)
unknown-≮: (witness t p q) = witness t unknown q

never-≮: : ∀ {T U} → (T ≮: U) → (T ≮: never)
never-≮: (witness t p q) = witness t p never

unknown-≮:-never : (unknown ≮: never)
unknown-≮:-never = witness (scalar nil) unknown never

function-≮:-never : ∀ {T U} → ((T ⇒ U) ≮: never)
function-≮:-never = witness function function never

-- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf)
-- defines a "set-theoretic" model (sec 2.5)
-- Unfortunately we don't quite have this property, due to uninhabited types,
-- for example (never -> T) is equivalent to (never -> U)
-- when types are interpreted as sets of syntactic values.

_⊆_ : ∀ {A : Set} → (A → Set) → (A → Set) → Set
(P ⊆ Q) = ∀ a → (P a) → (Q a)

_⊗_ : ∀ {A B : Set} → (A → Set) → (B → Set) → ((A × B) → Set)
(P ⊗ Q) (a , b) = (P a) × (Q b)

Comp : ∀ {A : Set} → (A → Set) → (A → Set)
Comp P a = ¬(P a)

set-theoretic-if : ∀ {S₁ T₁ S₂ T₂} →

  -- This is the "if" part of being a set-theoretic model
  (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)) →
  (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Language T₁)) → Q ⊆ Comp((Language S₂) ⊗ Comp(Language T₂)))

set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , u) Qtu (S₂t , ¬T₂u) = q (t , u) Qtu (S₁t , ¬T₁u) where

  S₁t : Language S₁ t
  S₁t with dec-language S₁ t
  S₁t | Left ¬S₁t with p (function-err t) (function-err ¬S₁t)
  S₁t | Left ¬S₁t | function-err ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t)
  S₁t | Right r = r

  ¬T₁u : ¬(Language T₁ u)
  ¬T₁u T₁u with p (function-ok u) (function-ok T₁u)
  ¬T₁u T₁u | function-ok T₂u = ¬T₂u T₂u

not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →

  -- We don't quite have that this is a set-theoretic model
  -- it's only true when Language T₁ and ¬Language T₂ t₂ are inhabited
  -- in particular it's not true when T₁ is never, or T₂ is unknown.
  ∀ s₂ t₂ → Language S₂ s₂ → ¬Language T₂ t₂ →

  -- This is the "only if" part of being a set-theoretic model
  (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Language T₁)) → Q ⊆ Comp((Language S₂) ⊗ Comp(Language T₂))) →
  (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂))

not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ ¬T₂t₂ p = r where

  Q : (Tree × Tree) → Set
  Q (t , u) = Either (¬Language S₁ t) (Language T₁ u)

  q : Q ⊆ Comp((Language S₁) ⊗ Comp(Language T₁))
  q (t , u) (Left ¬S₁t) (S₁t , ¬T₁u) = language-comp t ¬S₁t S₁t
  q (t , u) (Right T₂u) (S₁t , ¬T₁u) = ¬T₁u T₂u

  r : Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)
  r function function = function
  r (function-err t) (function-err ¬S₁t) with dec-language S₂ t
  r (function-err t) (function-err ¬S₁t) | Left ¬S₂t = function-err ¬S₂t
  r (function-err t) (function-err ¬S₁t) | Right S₂t = CONTRADICTION (p Q q (t , t₂) (Left ¬S₁t) (S₂t , language-comp t₂ ¬T₂t₂))
  r (function-ok t) (function-ok T₁t) with dec-language T₂ t
  r (function-ok t) (function-ok T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , t) (Right T₁t) (S₂s₂ ,  language-comp t ¬T₂t))
  r (function-ok t) (function-ok T₁t) | Right T₂t = function-ok T₂t

-- A counterexample when the argument type is empty.

set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Comp(Language number)) → Q ⊆ Comp((Language never) ⊗ Comp(Language string)))
set-theoretic-counterexample-one Q q ((scalar s) , u) Qtu (scalar () , p)
set-theoretic-counterexample-one Q q ((function-err t) , u) Qtu (scalar-function-err () , p)

set-theoretic-counterexample-two : (never ⇒ number) ≮: (never ⇒ string)
set-theoretic-counterexample-two = witness
  (function-ok (scalar number)) (function-ok (scalar number))
  (function-ok (scalar-scalar number string (λ ())))

-- At some point we may deal with overloaded function resolution, which should fix this problem...
-- The reason why this is connected to overloaded functions is that currently we have that the type of
-- f(x) is (tgt T) where f:T. Really we should have the type depend on the type of x, that is use (tgt T U),
-- where U is the type of x. In particular (tgt (S => T) (U & V)) should be the same as (tgt ((S&U) => T) V)
-- and tgt(never => T) should be unknown. For example
--
-- tgt((number => string) & (string => bool))(number)
-- is tgt(number => string)(number) & tgt(string => bool)(number)
-- is tgt(number => string)(number) & tgt(string => bool)(number&unknown)
-- is tgt(number => string)(number) & tgt(string&number => bool)(unknown)
-- is tgt(number => string)(number) & tgt(never => bool)(unknown)
-- is string & unknown
-- is string
--
-- there's some discussion of this in the Gentle Introduction paper.

max_stars_repo_name: MeltzDev/luau

max_issues_repo_name: MeltzDev/luau

max_forks_repo_name: MeltzDev/luau


text:
------------------------------------------------------------------------------
-- The first-order theory of combinators (FOTC) base
------------------------------------------------------------------------------

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

{-
FOTC                                  The logical framework (Agda)

* Logical constants                   * Curry-Howard isomorphism
* Equality                            * Identity type
* Term language and conversion rules  * Postulates
* Inductively defined predicates      * Inductive families
* Co-inductively defined predicates   * Greatest fixed-points
-}

module FOTC.Base where

-- First-order logic with equality.
open import Common.FOL.FOL-Eq public

-- Common definitions.
open import Common.DefinitionsATP public

infixl 7 _·_
infix  0 if_then_else_

------------------------------------------------------------------------------
-- The term language of FOTC

--   t ::= x   | t · t |
--      | true | false | if
--      | 0    | succ  | pred | iszero

postulate
  _·_                    : D → D → D  -- FOTC application.
  true false if          : D          -- FOTC partial Booleans.
  zero succ pred iszero  : D          -- FOTC partial natural numbers.

------------------------------------------------------------------------------
-- Definitions

-- We define some function symbols for convenience in writing and
-- looking for an optimization for the ATPs.

-- 2012-03-20. The definitions are inside an abstract block because
-- the conversion rules (see below) are based on them, so we want to
-- avoid their expansion.

abstract
  if_then_else_ : D → D → D → D
  if b then t else t' = if · b · t · t'
  -- {-# ATP definition if_then_else_ #-}

  succ₁ : D → D
  succ₁ n = succ · n
  -- {-# ATP definition succ₁ #-}

  pred₁ : D → D
  pred₁ n = pred · n
  -- {-# ATP definition pred₁ #-}

  iszero₁ : D → D
  iszero₁ n = iszero · n
  -- {-# ATP definition iszero₁ #-}

------------------------------------------------------------------------------
-- Conversion rules

-- The conversion relation _conv_ satifies (Aczel 1977, p. 8)
--
-- x conv y <=> FOTC ⊢ x ≡ y,
--
-- therefore, we introduce the conversion rules as non-logical axioms.

-- N.B. Looking for an optimization for the ATPs, we write the
-- conversion rules on the defined function symbols instead of on the
-- term constants.

-- Conversion rules for Booleans.
-- if-true  : ∀ t {t'} → if · true  · t · t' ≡ t
-- if-false : ∀ {t} t' → if · false · t · t' ≡ t'
postulate
  if-true  : ∀ t {t'} → (if true then t else t')  ≡ t
  if-false : ∀ {t} t' → (if false then t else t') ≡ t'
{-# ATP axioms if-true if-false #-}

-- Conversion rules for pred.
-- pred-0 :       pred · zero     ≡ zero
-- pred-S : ∀ n → pred · (succ · n) ≡ n
postulate
  pred-0 : pred₁ zero            ≡ zero
  pred-S : ∀ n → pred₁ (succ₁ n) ≡ n
{-# ATP axioms pred-0 pred-S #-}

-- Conversion rules for iszero.
-- iszero-0 :       iszero · zero       ≡ true
-- iszero-S : ∀ n → iszero · (succ · n) ≡ false
postulate
  iszero-0 : iszero₁ zero            ≡ true
  iszero-S : ∀ n → iszero₁ (succ₁ n) ≡ false
{-# ATP axioms iszero-0 iszero-S #-}

------------------------------------------------------------------------------
-- Discrimination rules

--  0≢S : ∀ {n} → zero ≢ succ · n
postulate
  t≢f : true ≢ false
  0≢S : ∀ {n} → zero ≢ succ₁ n
{-# ATP axioms t≢f 0≢S #-}

------------------------------------------------------------------------------
-- References
--
-- Aczel, Peter (1977). The Strength of MartinLöf’s Intuitionistic
-- Type Theory with One Universe. In: Proc. of the Symposium on
-- Mathematical Logic (Oulu, 1974). Ed. by Miettinen, S. and Väänanen,
-- J. Report No. 2, Department of Philosophy, University of Helsinki,
-- Helsinki, pp. 1–32.


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Escape {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties

open import Definition.Typed

open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties

open import Tools.Product

-- Valid types are well-formed.
escapeᵛ : ∀ {A l Γ} ([Γ] : ⊩ᵛ Γ) → Γ ⊩ᵛ⟨ l ⟩ A / [Γ] → Γ ⊢ A
escapeᵛ [Γ] [A] =
  let ⊢Γ = soundContext [Γ]
      idSubst = idSubstS [Γ]
  in  escape (irrelevance′ (subst-id _) (proj₁ ([A] ⊢Γ idSubst)))

-- Valid type equality respects the equality relation.
escapeEqᵛ : ∀ {A B l Γ} ([Γ] : ⊩ᵛ Γ) ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
              → Γ ⊩ᵛ⟨ l ⟩ A ≡ B / [Γ] / [A] → Γ ⊢ A ≅ B
escapeEqᵛ [Γ] [A] [A≡B] =
  let ⊢Γ = soundContext [Γ]
      idSubst = idSubstS [Γ]
      [idA]  = proj₁ ([A] ⊢Γ idSubst)
      [idA]′ = irrelevance′ (subst-id _) [idA]
  in  escapeEq [idA]′ (irrelevanceEq″ (subst-id _) (subst-id _)
                                           [idA] [idA]′ ([A≡B] ⊢Γ idSubst))

-- Valid terms are well-formed.
escapeTermᵛ : ∀ {t A l Γ} ([Γ] : ⊩ᵛ Γ) ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
               → Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A] → Γ ⊢ t ∷ A
escapeTermᵛ [Γ] [A] [t] =
  let ⊢Γ = soundContext [Γ]
      idSubst = idSubstS [Γ]
      [idA]  = proj₁ ([A] ⊢Γ idSubst)
      [idA]′ = irrelevance′ (subst-id _) (proj₁ ([A] ⊢Γ idSubst))
  in  escapeTerm [idA]′
                    (irrelevanceTerm″ (subst-id _) (subst-id _)
                                       [idA] [idA]′ (proj₁ ([t] ⊢Γ idSubst)))

-- Valid term equality respects the equality relation.
escapeEqTermᵛ : ∀ {t u A l Γ} ([Γ] : ⊩ᵛ Γ) ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
               → Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A / [Γ] / [A] → Γ ⊢ t ≅ u ∷ A
escapeEqTermᵛ [Γ] [A] [t≡u] =
  let ⊢Γ = soundContext [Γ]
      idSubst = idSubstS [Γ]
      [idA]  = proj₁ ([A] ⊢Γ idSubst)
      [idA]′ = irrelevance′ (subst-id _) (proj₁ ([A] ⊢Γ idSubst))
  in  escapeTermEq [idA]′
                       (irrelevanceEqTerm″ (subst-id _) (subst-id _)
                                            (subst-id _)
                                            [idA] [idA]′ ([t≡u] ⊢Γ idSubst))


text:
{-# OPTIONS --safe #-}

module Cubical.HITs.SetQuotients.EqClass where

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

open import Cubical.HITs.PropositionalTruncation as Prop
open import Cubical.HITs.SetQuotients as SetQuot

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

open import Cubical.Functions.Embedding
open import Cubical.Functions.Surjection

private
  variable
    ℓ ℓ' ℓ'' : Level

-- another definition using equivalence classes

open BinaryRelation
open isEquivRel

open Iso

module _
  {ℓ ℓ' : Level}
  (X : Type ℓ) where

  ℙ : Type (ℓ-max ℓ (ℓ-suc ℓ'))
  ℙ = X → hProp ℓ'

  ℙDec : Type (ℓ-max ℓ (ℓ-suc ℓ'))
  ℙDec = Σ[ P ∈ ℙ ] ((x : X) → Dec (P x .fst))

  isSetℙ : isSet ℙ
  isSetℙ = isSetΠ λ x → isSetHProp

  isSetℙDec : isSet ℙDec
  isSetℙDec = isOfHLevelΣ 2 isSetℙ (λ P → isSetΠ (λ x → isProp→isSet (isPropDec (P x .snd))))

  module _
    (R : X → X → Type ℓ'') where

    isEqClass : ℙ → Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
    isEqClass P = ∥ Σ[ x ∈ X ] ((a : X) → P a .fst ≃ ∥ R a x ∥) ∥

    isPropIsEqClass : (P : ℙ) → isProp (isEqClass P)
    isPropIsEqClass P = isPropPropTrunc

    _∥_ : Type (ℓ-max (ℓ-max ℓ (ℓ-suc ℓ')) ℓ'')
    _∥_ = Σ[ P ∈ ℙ ] isEqClass P

    isSet∥ : isSet _∥_
    isSet∥ = isOfHLevelΣ 2 isSetℙ (λ _ → isProp→isSet isPropPropTrunc)

    module _
      (dec : (x x' : X) → Dec (R x x')) where

      _∥Dec_ : Type (ℓ-max (ℓ-max ℓ (ℓ-suc ℓ')) ℓ'')
      _∥Dec_ = Σ[ P ∈ ℙDec ] isEqClass (P .fst)

      isDecEqClass : (P : _∥_) → (x : X) → Dec (P .fst x .fst)
      isDecEqClass (P , h) a =
        Prop.rec (isPropDec (P a .snd)) (λ (x , p) → EquivPresDec (invEquiv (p a)) (Dec∥∥ (dec a x))) h

      Iso-∥Dec-∥ : Iso _∥Dec_ _∥_
      Iso-∥Dec-∥ .fun P = P .fst .fst , P .snd
      Iso-∥Dec-∥ .inv P = (P .fst , isDecEqClass P) , P .snd
      Iso-∥Dec-∥ .rightInv P = refl
      Iso-∥Dec-∥ .leftInv P i .fst .fst = P .fst .fst
      Iso-∥Dec-∥ .leftInv P i .fst .snd x =
        isProp→PathP {B = λ i → Dec (P .fst .fst x .fst)}
          (λ i → isPropDec (P .fst .fst x .snd))
          (isDecEqClass (Iso-∥Dec-∥ .fun P) x) (P .fst .snd x) i
      Iso-∥Dec-∥ .leftInv P i .snd = P .snd

      ∥Dec≃∥ : _∥Dec_ ≃ _∥_
      ∥Dec≃∥ = isoToEquiv Iso-∥Dec-∥

module _
  {ℓ ℓ' ℓ'' : Level}
  (X : Type ℓ)
  (R : X → X → Type ℓ'')
  (h : isEquivRel R) where

  ∥Rx∥Iso : (x x' : X)(r : R x x') → (a : X) → Iso ∥ R a x ∥ ∥ R a x' ∥
  ∥Rx∥Iso x x' r a .fun = Prop.rec isPropPropTrunc (λ r' → ∣ h .transitive _ _ _ r' r ∣)
  ∥Rx∥Iso x x' r a .inv = Prop.rec isPropPropTrunc (λ r' → ∣ h .transitive _ _ _ r' (h .symmetric _ _ r) ∣)
  ∥Rx∥Iso x x' r a .leftInv _ = isPropPropTrunc _ _
  ∥Rx∥Iso x x' r a .rightInv _ = isPropPropTrunc _ _

  isEqClass∥Rx∥ : (x : X) → isEqClass X R (λ a → ∥ R a x ∥ , isPropPropTrunc)
  isEqClass∥Rx∥ x = ∣ x , (λ _ → idEquiv _) ∣

  ∥R∥ : (x : X) → X ∥ R
  ∥R∥ x = (λ a → ∥ R a x ∥ , isPropPropTrunc) , isEqClass∥Rx∥ x

  ∥Rx∥Path : (x x' : X)(r : R x x') → ∥R∥ x ≡ ∥R∥ x'
  ∥Rx∥Path x x' r i .fst a .fst = ua (isoToEquiv (∥Rx∥Iso x x' r a)) i
  ∥Rx∥Path x x' r i .fst a .snd =
    isProp→PathP {B = λ i → isProp (∥Rx∥Path x x' r i .fst a .fst)}
                 (λ i → isPropIsProp) isPropPropTrunc isPropPropTrunc i
  ∥Rx∥Path x x' r i .snd =
    isProp→PathP {B = λ i → isEqClass X R (∥Rx∥Path x x' r i .fst)}
                 (λ i → isPropIsEqClass X R (∥Rx∥Path x x' r i .fst))
                 (isEqClass∥Rx∥ x) (isEqClass∥Rx∥ x') i

  /→∥ : X / R → X ∥ R
  /→∥ = SetQuot.rec (isSet∥ X R) ∥R∥ (λ x x' r → ∥Rx∥Path x x' r)

  inj/→∥' : (x x' : X) → ∥R∥ x ≡ ∥R∥ x' → ∥ R x x' ∥
  inj/→∥' x x' p = transport (λ i → p i .fst x .fst) ∣ h .reflexive x ∣

  inj/→∥ : (x y : X / R) → /→∥ x ≡ /→∥ y → x ≡ y
  inj/→∥ =
    SetQuot.elimProp2 {P = λ x y → /→∥ x ≡ /→∥ y → x ≡ y}
      (λ _ _ → isPropΠ (λ _ → squash/ _ _))
      (λ x y q → Prop.rec (squash/ _ _) (λ r → eq/ _ _ r) (inj/→∥' x y q))

  isEmbedding/→∥ : isEmbedding /→∥
  isEmbedding/→∥ = injEmbedding squash/ (isSet∥ X R) (λ {x} {y} → inj/→∥ x y)

  surj/→∥ : (P : X ∥ R) → ((x , _) : Σ[ x ∈ X ] ((a : X) → P .fst a .fst ≃ ∥ R a x ∥)) → ∥R∥ x ≡ P
  surj/→∥ P (x , p) i .fst a .fst = ua (p a) (~ i)
  surj/→∥ P (x , p) i .fst a .snd =
    isProp→PathP {B = λ i → isProp (surj/→∥ P (x , p) i .fst a .fst)}
                 (λ i → isPropIsProp) isPropPropTrunc (P .fst a .snd) i
  surj/→∥ P (x , p) i .snd =
    isProp→PathP {B = λ i → isEqClass X R (surj/→∥ P (x , p) i .fst)}
                 (λ i → isPropIsEqClass X R (surj/→∥ P (x , p) i .fst))
                 (isEqClass∥Rx∥ x) (P .snd) i

  isSurjection/→∥ : isSurjection /→∥
  isSurjection/→∥ P = Prop.rec isPropPropTrunc (λ p → ∣ [ p .fst ] , surj/→∥ P p ∣) (P .snd)

  -- both definitions are equivalent
  equivQuot : X / R ≃ X ∥ R
  equivQuot = /→∥ , isEmbedding×isSurjection→isEquiv (isEmbedding/→∥ , isSurjection/→∥)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module constructs the unit of the monoidal structure on
-- R-modules, and similar for weaker module-like structures.
-- The intended universal property is that the maps out of the tensor
-- unit into M are isomorphic to the elements of M.
------------------------------------------------------------------------

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

module Algebra.Module.Construct.TensorUnit where

open import Algebra.Bundles
open import Algebra.Module.Bundles
open import Level

private
  variable
    c ℓ : Level

leftSemimodule : {R : Semiring c ℓ} → LeftSemimodule R c ℓ
leftSemimodule {R = semiring} = record
  { Carrierᴹ = Carrier
  ; _≈ᴹ_ = _≈_
  ; _+ᴹ_ = _+_
  ; _*ₗ_ = _*_
  ; 0ᴹ = 0#
  ; isLeftSemimodule = record
    { +ᴹ-isCommutativeMonoid = +-isCommutativeMonoid
    ; isPreleftSemimodule = record
      { *ₗ-cong = *-cong
      ; *ₗ-zeroˡ = zeroˡ
      ; *ₗ-distribʳ = distribʳ
      ; *ₗ-identityˡ = *-identityˡ
      ; *ₗ-assoc = *-assoc
      ; *ₗ-zeroʳ = zeroʳ
      ; *ₗ-distribˡ = distribˡ
      }
    }
  } where open Semiring semiring

rightSemimodule : {R : Semiring c ℓ} → RightSemimodule R c ℓ
rightSemimodule {R = semiring} = record
  { Carrierᴹ = Carrier
  ; _≈ᴹ_ = _≈_
  ; _+ᴹ_ = _+_
  ; _*ᵣ_ = _*_
  ; 0ᴹ = 0#
  ; isRightSemimodule = record
    { +ᴹ-isCommutativeMonoid = +-isCommutativeMonoid
    ; isPrerightSemimodule = record
      { *ᵣ-cong = *-cong
      ; *ᵣ-zeroʳ = zeroʳ
      ; *ᵣ-distribˡ = distribˡ
      ; *ᵣ-identityʳ = *-identityʳ
      ; *ᵣ-assoc = *-assoc
      ; *ᵣ-zeroˡ = zeroˡ
      ; *ᵣ-distribʳ = distribʳ
      }
    }
  } where open Semiring semiring

bisemimodule : {R : Semiring c ℓ} → Bisemimodule R R c ℓ
bisemimodule {R = semiring} = record
  { isBisemimodule = record
    { +ᴹ-isCommutativeMonoid = +-isCommutativeMonoid
    ; isPreleftSemimodule =
      LeftSemimodule.isPreleftSemimodule leftSemimodule
    ; isPrerightSemimodule =
      RightSemimodule.isPrerightSemimodule rightSemimodule
    ; *ₗ-*ᵣ-assoc = *-assoc
    }
  } where open Semiring semiring

semimodule : {R : CommutativeSemiring c ℓ} → Semimodule R c ℓ
semimodule {R = commutativeSemiring} = record
  { isSemimodule = record
    { isBisemimodule = Bisemimodule.isBisemimodule bisemimodule
    }
  } where open CommutativeSemiring commutativeSemiring

leftModule : {R : Ring c ℓ} → LeftModule R c ℓ
leftModule {R = ring} = record
  { -ᴹ_ = -_
  ; isLeftModule = record
    { isLeftSemimodule = LeftSemimodule.isLeftSemimodule leftSemimodule
    ; -ᴹ‿cong = -‿cong
    ; -ᴹ‿inverse = -‿inverse
    }
  } where open Ring ring

rightModule : {R : Ring c ℓ} → RightModule R c ℓ
rightModule {R = ring} = record
  { -ᴹ_ = -_
  ; isRightModule = record
    { isRightSemimodule = RightSemimodule.isRightSemimodule rightSemimodule
    ; -ᴹ‿cong = -‿cong
    ; -ᴹ‿inverse = -‿inverse
    }
  } where open Ring ring

bimodule : {R : Ring c ℓ} → Bimodule R R c ℓ
bimodule {R = ring} = record
  { isBimodule = record
    { isBisemimodule = Bisemimodule.isBisemimodule bisemimodule
    ; -ᴹ‿cong = -‿cong
    ; -ᴹ‿inverse = -‿inverse
    }
  } where open Ring ring

⟨module⟩ : {R : CommutativeRing c ℓ} → Module R c ℓ
⟨module⟩ {R = commutativeRing} = record
  { isModule = record
    { isBimodule = Bimodule.isBimodule bimodule
    }
  } where open CommutativeRing commutativeRing


text:
-- Andreas, 2019-06-26, issue #3855
-- Mark erased hypotheses as such in a non-erased goal.
-- Same for irrelevance.

Goal :
  (        A : Set)
  (@0      B : Set)
  (@irr    C : Set)
  (@0 @irr D : Set)
  (        A : Set)
  (@0      B : Set)
  (@irr    C : Set)
  (@0 @irr D : Set)
  → Set
Goal A B C D = λ A B C D → {!!}

-- Goal: Set
-- ————————————————————————————————————————————————————————————
-- D      : Set  (erased, irrelevant)
-- C      : Set  (irrelevant)
-- B      : Set  (erased)
-- A      : Set
-- D = D₁ : Set  (not in scope, erased, irrelevant)
-- C = C₁ : Set  (not in scope, irrelevant)
-- B = B₁ : Set  (not in scope, erased)
-- A = A₁ : Set  (not in scope)

-- Don't show erasure in erased goal!

@0 ErasedGoal :
  (        A : Set)
  (@0      B : Set)
  (@irr    C : Set)
  (@0 @irr D : Set)
  (        A : Set)
  (@0      B : Set)
  (@irr    C : Set)
  (@0 @irr D : Set)
  → Set
ErasedGoal A B C D = λ A B C D → {!!}

-- Goal: Set
-- ————————————————————————————————————————————————————————————
-- D      : Set  (irrelevant)
-- C      : Set  (irrelevant)
-- B      : Set
-- A      : Set
-- D = D₁ : Set  (not in scope, irrelevant)
-- C = C₁ : Set  (not in scope, irrelevant)
-- B = B₁ : Set  (not in scope)
-- A = A₁ : Set  (not in scope)

-- Don't show irrelevance in irrelevant goal!

@irr IrrGoal :
  (        A : Set)
  (@0      B : Set)
  (@irr    C : Set)
  (@0 @irr D : Set)
  (        A : Set)
  (@0      B : Set)
  (@irr    C : Set)
  (@0 @irr D : Set)
  → Set
IrrGoal A B C D = λ A B C D → {!!}

-- Goal: Set
-- ————————————————————————————————————————————————————————————
-- D      : Set  (erased)
-- C      : Set
-- B      : Set  (erased)
-- A      : Set
-- D = D₁ : Set  (not in scope, erased)
-- C = C₁ : Set  (not in scope)
-- B = B₁ : Set  (not in scope, erased)
-- A = A₁ : Set  (not in scope)


text:
{-# OPTIONS --without-K --cubical #-}

module combinatorial-objects where

import 14-univalence
open 14-univalence public

{- The type ℍ of hereditarily finite types is introduces as an inductive type.

   Note that this is the type of 'planar' combinatorial objects, because Fin n
   is a linearly ordered finite set with n elements.

   For a non-planar type of hereditarily finite types, we need to use the type
   𝔽, which is the image of (Fin : ℕ → UU lzero). This latter type probably has
   the correct identity type, and is more interesting from the perspective of
   homotopy type theory.

   Planar hereditarily finite types are easier to handle though, so we study
   them first.
   -}

data ℍ : UU lzero where
  join-ℍ : (n : ℕ) → (Fin n → ℍ) → ℍ

width-ℍ : ℍ → ℕ
width-ℍ (join-ℍ n x) = n

branch-ℍ : (x : ℍ) → (Fin (width-ℍ x) → ℍ)
branch-ℍ (join-ℍ n x) = x

empty-ℍ : ℍ
empty-ℍ = join-ℍ zero-ℕ ind-empty

Fin-ℍ : ℕ → ℍ
Fin-ℍ n = join-ℍ n (const (Fin n) ℍ empty-ℍ)

unit-ℍ : ℍ
unit-ℍ = Fin-ℍ one-ℕ

{- Logical morphisms of hereditarily finite types. -}

hom-ℍ : ℍ → ℍ → UU lzero
hom-ℍ (join-ℍ m x) (join-ℍ n y) =
  Σ (Fin m → Fin n) (λ h → (i : Fin m) → hom-ℍ (x i) (y (h i)))

map-base-hom-ℍ : (x y : ℍ) (f : hom-ℍ x y) →
  Fin (width-ℍ x) → Fin (width-ℍ y)
map-base-hom-ℍ (join-ℍ m x) (join-ℍ n y) = pr1

hom-branch-hom-ℍ : (x y : ℍ) (f : hom-ℍ x y) (i : Fin (width-ℍ x)) →
  hom-ℍ (branch-ℍ x i) (branch-ℍ y (map-base-hom-ℍ x y f i))
hom-branch-hom-ℍ (join-ℍ m x) (join-ℍ n y) = pr2

htpy-hom-ℍ : {x y : ℍ} (f g : hom-ℍ x y) → UU lzero
htpy-hom-ℍ {join-ℍ m x} {join-ℍ n y} (pair f F) g =
  Σ ( f ~ (map-base-hom-ℍ (join-ℍ m x) (join-ℍ n y) g))
    ( λ H →
      ( i : Fin m) →
        htpy-hom-ℍ
          ( tr (λ t → hom-ℍ (x i) (y t)) (H i) (F i))
          ( hom-branch-hom-ℍ (join-ℍ m x) (join-ℍ n y) g i))

refl-htpy-hom-ℍ : {x y : ℍ} {f : hom-ℍ x y} → htpy-hom-ℍ f f
refl-htpy-hom-ℍ {join-ℍ m x} {join-ℍ n y} {pair f F} =
  pair refl-htpy (λ i → refl-htpy-hom-ℍ)

htpy-hom-ℍ-eq : {x y : ℍ} {f g : hom-ℍ x y} → (Id f g) → htpy-hom-ℍ f g
htpy-hom-ℍ-eq refl = refl-htpy-hom-ℍ

is-contr-total-htpy-hom-ℍ : {x y : ℍ} (f : hom-ℍ x y) →
  is-contr (Σ (hom-ℍ x y) (htpy-hom-ℍ f))
is-contr-total-htpy-hom-ℍ {join-ℍ m x} {join-ℍ n y} (pair f F) =
  is-contr-total-Eq-structure
    ( λ g G (H : f ~ g) →
      ( i : Fin m) →
        htpy-hom-ℍ
          ( tr (λ t → hom-ℍ (x i) (y t)) (H i) (F i))
          ( G i))
    ( is-contr-total-htpy f)
    ( pair f refl-htpy)
    ( is-contr-total-Eq-Π
      ( λ i G → htpy-hom-ℍ (F i) G)
      ( λ i → is-contr-total-htpy-hom-ℍ (F i))
      ( λ i → F i))

is-equiv-htpy-hom-ℍ-eq : {x y : ℍ} (f g : hom-ℍ x y) →
  is-equiv (htpy-hom-ℍ-eq {x} {y} {f} {g})
is-equiv-htpy-hom-ℍ-eq f =
  fundamental-theorem-id f
    ( refl-htpy-hom-ℍ)
    ( is-contr-total-htpy-hom-ℍ f)
    ( λ g → htpy-hom-ℍ-eq)

eq-htpy-hom-ℍ : {x y : ℍ} {f g : hom-ℍ x y} → htpy-hom-ℍ f g → Id f g
eq-htpy-hom-ℍ {x} {y} {f} {g} =
  inv-is-equiv (is-equiv-htpy-hom-ℍ-eq f g)

id-ℍ : {x : ℍ} → hom-ℍ x x
id-ℍ {join-ℍ n x} = pair id (λ i → id-ℍ)

comp-ℍ :
  {x y z : ℍ} (g : hom-ℍ y z) (f : hom-ℍ x y) → hom-ℍ x z
comp-ℍ {join-ℍ m x} {join-ℍ n y} {join-ℍ k z} (pair g G) (pair f F) =
  pair (g ∘ f) (λ i → comp-ℍ (G (f i)) (F i))

left-unit-law-htpy-hom-ℍ :
  {x y : ℍ} (f : hom-ℍ x y) → htpy-hom-ℍ (comp-ℍ id-ℍ f) f
left-unit-law-htpy-hom-ℍ {join-ℍ m x} {join-ℍ n y} (pair f F) =
  pair refl-htpy (λ i → left-unit-law-htpy-hom-ℍ (F i))

left-unit-law-hom-ℍ :
  {x y : ℍ} (f : hom-ℍ x y) → Id (comp-ℍ id-ℍ f) f
left-unit-law-hom-ℍ f = eq-htpy-hom-ℍ (left-unit-law-htpy-hom-ℍ f)

right-unit-law-htpy-hom-ℍ :
  {x y : ℍ} (g : hom-ℍ x y) → htpy-hom-ℍ (comp-ℍ g id-ℍ) g
right-unit-law-htpy-hom-ℍ {join-ℍ m x} {join-ℍ n y} (pair g G) =
  pair refl-htpy (λ i → right-unit-law-htpy-hom-ℍ (G i))

right-unit-law-hom-ℍ :
  {x y : ℍ} (g : hom-ℍ x y) → Id (comp-ℍ g id-ℍ) g
right-unit-law-hom-ℍ g = eq-htpy-hom-ℍ (right-unit-law-htpy-hom-ℍ g)

associative-htpy-comp-ℍ :
  {x y z w : ℍ} (h : hom-ℍ z w) (g : hom-ℍ y z) (f : hom-ℍ x y) →
  htpy-hom-ℍ (comp-ℍ (comp-ℍ h g) f) (comp-ℍ h (comp-ℍ g f))
associative-htpy-comp-ℍ
  {join-ℍ n1 x1} {join-ℍ n2 x2} {join-ℍ n3 x3} {join-ℍ n4 x4} (pair h H) (pair g G) (pair f F) =
  pair refl-htpy (λ i → associative-htpy-comp-ℍ (H (g (f i))) (G (f i)) (F i))

associative-comp-ℍ :
  {x y z w : ℍ} (h : hom-ℍ z w) (g : hom-ℍ y z) (f : hom-ℍ x y) →
  Id (comp-ℍ (comp-ℍ h g) f) (comp-ℍ h (comp-ℍ g f))
associative-comp-ℍ h g f = eq-htpy-hom-ℍ (associative-htpy-comp-ℍ h g f)

{-
{- Union of planar hereditarily finite sets -}

{-
map-add-Fin : {m n : ℕ} → Fin (add-ℕ m n) → coprod (Fin m) (Fin n)
map-add-Fin {zero-ℕ} {n} x = inr x
map-add-Fin {succ-ℕ m} {n} (inl x) = {!!}
map-add-Fin {succ-ℕ m} {n} (inr star) = ?
-}

{-
union-ℍ : ℍ → ℍ → ℍ
union-ℍ (join-ℍ n f) (join-ℍ m g) = join-ℍ (add-ℕ n m) ((ind-coprod (λ x → ℍ) f g) ∘ map-add-Fin)
-}

{- We define the Rado graph to be the graph with set of vertices ℍ, and for each   (f : Fin n → ℍ) and each (i : Fin n), an edge from (join-ℍ n f) to (f i).

   Note that in this definition of the Rado graph, there can be multiple edges
   from x to y. -}

data Rado-ℍ : ℍ → ℍ → UU lzero where
  edge-Rado-ℍ : (n : ℕ) (f : Fin n → ℍ) (i : Fin n) → Rado-ℍ (join-ℍ n f) (f i)

{- Next, we define the Ackermann bijection from ℍ to ℕ. -}

finite-sum-ℕ : (n : ℕ) → (f : Fin n → ℕ) → ℕ
finite-sum-ℕ zero-ℕ f = zero-ℕ
finite-sum-ℕ (succ-ℕ n) f = add-ℕ (f (inr star)) (finite-sum-ℕ n (f ∘ inl))

map-Ackermann-ℍ : ℍ → ℕ
map-Ackermann-ℍ (join-ℍ n f) =
  finite-sum-ℕ n (λ i → pow-ℕ (succ-ℕ (succ-ℕ zero-ℕ)) (map-Ackermann-ℍ (f i)))

{- In order to construct the inverse of the Ackermann map, we need to show
   first that every natural number can be uniquely represented as a list of
   booleans. -}

ℕ-list-bool : list bool → ℕ
ℕ-list-bool nil = zero-ℕ
ℕ-list-bool (cons false l) = pow-ℕ (succ-ℕ (succ-ℕ zero-ℕ)) (ℕ-list-bool l)
ℕ-list-bool (cons true l) = succ-ℕ (pow-ℕ (succ-ℕ (succ-ℕ zero-ℕ)) (ℕ-list-bool l))

list-bool-ℕ : ℕ → list bool
list-bool-ℕ zero-ℕ = nil
list-bool-ℕ (succ-ℕ n) = {!!}

inv-Ackermann-ℍ : ℕ → ℍ
inv-Ackermann-ℍ n = {!!}
-}

max_stars_repo_name: tmoux/HoTT-Intro

max_issues_repo_name: tmoux/HoTT-Intro

max_forks_repo_name: tmoux/HoTT-Intro


text:
-- The default include path should contain Agda.Primitive

module TestDefaultIncludePath where

import Agda.Primitive

-- That's it.

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
record Pointed (A : Set) : Set where
  field
    point : A

point : {A : Set} ⦃ p : Pointed A ⦄ → A
point ⦃ p = p ⦄ = Pointed.point p

record R : Set₁ where
  field
    A : Set
    instance
      is-pointed : Pointed A

postulate
  r : R

open R r

x : R.A r
x = point


text:
module Generic.Test.Data.Product where

open import Generic.Main as Main hiding (Σ; proj₁; proj₂; _,′_) renaming (_,_ to _,′_)

infixr 4 _,_

Σ : ∀ {α β} -> (A : Set α) -> (A -> Set β) -> Set (α ⊔ β)
Σ = readData Main.Σ

pattern _,_ x y = !#₀ (relv x ,′ relv y ,′ lrefl)

proj₁ : ∀ {α β} {A : Set α} {B : A -> Set β} -> Σ A B -> A
proj₁ (x , y) = x

proj₂ : ∀ {α β} {A : Set α} {B : A -> Set β} -> (p : Σ A B) -> B (proj₁ {B = B} p)
proj₂ (x , y) = y

ηo : ∀ {α β} {A : Set α} {B : A -> Set β} -> (p : Σ A B) -> p ≡ proj₁ {B = B} p , proj₂ {B = B} p
ηo (x , y) = refl

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic