text:
module Function.Iteration.Proofs where

import Lvl
open import Functional
open import Function.Names as Names using (_⊜_)
open import Function.Iteration
open import Function.Proofs
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Oper using (_+_ ; _⋅_ ; _𝄩_)
open import Numeral.Natural.Oper.Proofs
import      Structure.Function.Names as Names
import      Structure.Function
open import Structure.Operator.Properties
open import Structure.Operator.Proofs.Util
import      Structure.Operator.Names as Names
import      Structure.Operator
open import Structure.Relator.Properties
open import Structure.Function.Domain
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ : Lvl.Level
private variable T A B C X Y Z : Type{ℓ}

module _ where
  open import Structure.Setoid
  open        Structure.Function
  open        Structure.Operator

  module _ ⦃ equiv-X : Equiv{ℓₑ}(X) ⦄ where
    -- Propositions that state something about arbitrary composed functions also apply to arbitrary function iterations of the first function.
    [^]-from-[∘]-proof : ∀{ℓ₂}{P : (X → X) → Type{ℓ₂}} → (∀{f g : X → X} → P(f ∘ g)) → (∀{f : X → X}{n} → P(f ^ n))
    [^]-from-[∘]-proof {P = P} p {f} {𝟎}   = p{id}{id}
    [^]-from-[∘]-proof {P = P} p {f} {𝐒 n} = p{f}{f ^ n}

    [^]-function-raw : ∀{f : X → X} → Names.Congruence₁(f) → ∀{n} → Names.Congruence₁(f ^ n)
    [^]-function-raw func-f {𝟎}    xy = xy
    [^]-function-raw func-f {𝐒(n)} xy = func-f([^]-function-raw func-f {n} xy)

    -- Iterated function is a function when the function is.
    [^]-function : ∀{f : X → X} → ⦃ func : Function(f) ⦄ → ∀{n} → Function(f ^ n)
    Function.congruence ([^]-function ⦃ intro func-f ⦄ {n}) = [^]-function-raw func-f {n}

    [^]-injective-raw : ∀{f : X → X} → Names.Injective(f) → ∀{n} → Names.Injective(f ^ n)
    [^]-injective-raw inj-f {𝟎}    fnxfny = fnxfny
    [^]-injective-raw inj-f {𝐒(n)} fnxfny = [^]-injective-raw inj-f {n} (inj-f fnxfny)

    -- Iterated function is injective when the function is.
    [^]-injective : ∀{f : X → X} → ⦃ inj : Injective(f) ⦄ → ∀{n} → Injective(f ^ n)
    Injective.proof ([^]-injective ⦃ intro inj-f ⦄ {n}) = [^]-injective-raw inj-f {n}

    [^]-surjective-raw : ∀{f : X → X} → ⦃ func : Function(f) ⦄ → Names.Surjective(f) → ∀{n} → Names.Surjective(f ^ n)
    [^]-surjective-raw     surj-f {𝟎}    {y} = [∃]-intro y ⦃ reflexivity(_≡_) ⦄
    [^]-surjective-raw {f} surj-f {𝐒(n)} {y} = [∃]-map-proof (p ↦ (congruence₁(f) p) 🝖 [∃]-proof(surj-f {y})) ([^]-surjective-raw surj-f {n} {[∃]-witness(surj-f {y})})

    -- Iterated function is surjective when the function is.
    [^]-surjective : ∀{f : X → X} → ⦃ func : Function(f) ⦄ → ⦃ surj : Surjective(f) ⦄ → ∀{n} → Surjective(f ^ n)
    Surjective.proof ([^]-surjective ⦃ _ ⦄ ⦃ intro surj-f ⦄ {n}) = [^]-surjective-raw surj-f {n}

    -- Argument applied to the iterated function is one extra iteration.
    -- Note: This implies: (f ^ n)(f x) ≡ f((f ^ n)(x))
    [^]-inner-value : ∀{f : X → X} → ⦃ func : Function(f) ⦄ → ∀{x}{n} → ((f ^ n)(f x) ≡ (f ^ (𝐒(n)))(x))
    [^]-inner-value {f} {x} {𝟎}   = reflexivity(_≡_)
    [^]-inner-value {f} {x} {𝐒 n} = congruence₁(f) ([^]-inner-value {f} {x} {n})

    -- A fixpoint of the function is also a fixpoint of the iterated function.
    [^]-of-fixpoint : ∀{f : X → X} → ⦃ func : Function(f) ⦄ → ∀{x : X} → ⦃ fix : Fixpoint f(x) ⦄ → ∀{n} → ((f ^ n)(x) ≡ x)
    [^]-of-fixpoint {f} {x} {𝟎}    = reflexivity(_≡_)
    [^]-of-fixpoint {f} {x} {𝐒(n)} =
      (f ^ 𝐒(n))(x)    🝖-[ reflexivity(_≡_) ]
      (f ∘ (f ^ n))(x) 🝖-[ reflexivity(_≡_) ]
      f((f ^ n)(x))    🝖-[ congruence₁(f) ([^]-of-fixpoint {f} {x} {n}) ]
      f(x)             🝖-[ fixpoint f(x) ]
      x                🝖-end

  module _ ⦃ equiv-XX : Equiv{ℓₑ}(X → X) ⦄ where
    [^]-by-1 : ∀{f : X → X} → (f ^ 1 ≡ f)
    [^]-by-1 {f} = reflexivity(_≡_)

    [^]-of-id : ∀{n} → (id ^ n ≡ id)
    [^]-of-id {𝟎}   = reflexivity(_≡_)
    [^]-of-id {𝐒 n} = [^]-of-id {n}

    [^]-inner : ∀{f : X → X} → ⦃ _ : Function(f ∘_) ⦄ → ∀{n} → ((f ^ n) ∘ f ≡ f ^ (𝐒(n)))
    [^]-inner {f} {𝟎}   = reflexivity(_≡_)
    [^]-inner {f} {𝐒 n} = congruence₁(f ∘_) ([^]-inner {f} {n})

    [^]-add : ⦃ [∘]-op : BinaryOperator(_∘_) ⦄ → ∀{f : X → X} → ∀{a b} → ((f ^ a) ∘ (f ^ b) ≡ f ^ (a + b))
    [^]-add {f} {𝟎} {𝟎}     = reflexivity(_≡_)
    [^]-add {f} {𝟎} {𝐒 b}   = reflexivity(_≡_)
    [^]-add {f} {𝐒 a} {𝟎}   = reflexivity(_≡_)
    [^]-add ⦃ [∘]-op ⦄ {f} {𝐒 a} {𝐒 b} =
      (f ^ 𝐒(a)) ∘ (f ^ 𝐒(b))    🝖-[ reflexivity(_≡_) ]
      (f ^ 𝐒(a)) ∘ (f ∘ (f ^ b)) 🝖-[ reflexivity(_≡_) ]
      ((f ^ 𝐒(a)) ∘ f) ∘ (f ^ b) 🝖-[ congruence₂ₗ(_∘_)(f ^ b) ([^]-inner {f} ⦃ [≡]-congruence2-right(_∘_)(f) ⦄ {𝐒(a)}) ]
      f ∘ ((f ^ 𝐒(a)) ∘ (f ^ b)) 🝖-[ reflexivity(_≡_) ]
      (f ∘ (f ^ 𝐒(a))) ∘ (f ^ b) 🝖-[ congruence₂ᵣ(_∘_)(f) ([^]-add{f} {𝐒 a} {b}) ]
      f ∘ (f ^ (𝐒(a) + b))       🝖-[ reflexivity(_≡_) ]
      f ^ (𝐒(a) + 𝐒(b))          🝖-end

    [^]-multiply : ⦃ [∘]-op : BinaryOperator(_∘_) ⦄ → ∀{f : X → X} → ∀{a b} → ((f ^ a) ^ b ≡ f ^ (a ⋅ b))
    [^]-multiply ⦃ [∘]-op ⦄ {f} {𝟎}   {𝟎}   = reflexivity(_≡_)
    [^]-multiply ⦃ [∘]-op ⦄ {f} {𝟎}   {𝐒 b} = [^]-of-id {𝐒 b}
    [^]-multiply ⦃ [∘]-op ⦄ {f} {𝐒 a} {𝟎}   = reflexivity(_≡_)
    [^]-multiply ⦃ [∘]-op ⦄ {f} {𝐒 a} {𝐒 b} =
      (f ^ 𝐒(a)) ^ 𝐒(b)             🝖-[ reflexivity(_≡_) ]
      (f ^ 𝐒(a)) ∘ ((f ^ 𝐒(a)) ^ b) 🝖-[ congruence₂ᵣ(_∘_)(f ^ 𝐒(a)) ([^]-multiply{f} {𝐒 a} {b}) ]
      (f ^ 𝐒(a)) ∘ (f ^ (𝐒(a) ⋅ b)) 🝖-[ [^]-add {f} {𝐒(a)} {𝐒(a) ⋅ b} ]
      f ^ (𝐒(a) + (𝐒(a) ⋅ b))       🝖-[ reflexivity(_≡_) ]
      f ^ (𝐒(a) ⋅ 𝐒(b))             🝖-end

    [^]-distanceₗ : ⦃ [∘]-op : BinaryOperator(_∘_) ⦄ → ∀{f : X → X}{a b} → (f ^ a ≡ f ^ b) ← (f ^ (a 𝄩 b) ≡ id)
    [^]-distanceₗ {f} {𝟎}   {𝟎}   = id
    [^]-distanceₗ {f} {𝟎}   {𝐒 b} = symmetry(_≡_)
    [^]-distanceₗ {f} {𝐒 a} {𝟎}   = id
    [^]-distanceₗ {f} {𝐒 a} {𝐒 b} = congruence₂ᵣ(_∘_)(f) ∘ ([^]-distanceₗ {f} {a} {b})

    [^]-distanceᵣ : ⦃ [∘]-op : BinaryOperator(_∘_) ⦄ → ⦃ [∘]-cancₗ : Cancellationₗ(_∘_) ⦄ → ∀{f : X → X}{a b} → (f ^ a ≡ f ^ b) → (f ^ (a 𝄩 b) ≡ id)
    [^]-distanceᵣ {f} {𝟎}   {𝟎}   = id
    [^]-distanceᵣ {f} {𝟎}   {𝐒 b} = symmetry(_≡_)
    [^]-distanceᵣ {f} {𝐒 a} {𝟎}   = id
    [^]-distanceᵣ {f} {𝐒 a} {𝐒 b} p = [^]-distanceᵣ {f} {a} {b} (cancellationₗ(_∘_) {f} p)

    module _ ⦃ op : BinaryOperator(_∘_) ⦄ ⦃ assoc : Associativity(_∘_) ⦄ where
      [^]-commuting : ∀{f g : X → X} → Names.Commuting(_∘_)(f)(g) → ∀{a b} → Names.Commuting(_∘_)(f ^ a)(g ^ b)
      [^]-commuting {f} {g} com {𝟎}   {𝟎}   = reflexivity(_≡_)
      [^]-commuting {f} {g} com {𝟎}   {𝐒 b} = reflexivity(_≡_)
      [^]-commuting {f} {g} com {𝐒 a} {𝟎}   = reflexivity(_≡_)
      [^]-commuting {f} {g} com {𝐒 a} {𝐒 b} =
        (f ^ 𝐒(a)) ∘ (g ^ 𝐒(b))       🝖-[ reflexivity(_≡_) ]
        (f ∘ (f ^ a)) ∘ (g ∘ (g ^ b)) 🝖-[ One.associate-commute4 {a = f} {f ^ a} {g} {g ^ b} ([^]-commuting {f} {g} com {a} {1}) ]
        (f ∘ g) ∘ ((f ^ a) ∘ (g ^ b)) 🝖-[ congruence₂(_∘_) com ([^]-commuting {f} {g} com {a} {b}) ]
        (g ∘ f) ∘ ((g ^ b) ∘ (f ^ a)) 🝖-[ One.associate-commute4 {a = g} {f} {g ^ b} {f ^ a} ([^]-commuting {f} {g} com {1} {b}) ]
        (g ∘ (g ^ b)) ∘ (f ∘ (f ^ a)) 🝖-[ reflexivity(_≡_) ]
        (g ^ 𝐒(b)) ∘ (f ^ 𝐒(a))       🝖-end

      [^]-of-[∘] :  ∀{f : X → X}{g : X → X} → Names.Commuting(_∘_)(f)(g) → ∀{n} → ((f ∘ g) ^ n ≡ (f ^ n) ∘ (g ^ n))
      [^]-of-[∘] {f}{g} com {𝟎}   = reflexivity(_≡_)
      [^]-of-[∘] {f}{g} com {𝐒 n} =
        (f ∘ g) ^ 𝐒(n)                🝖-[ reflexivity(_≡_) ]
        (f ∘ g) ∘ ((f ∘ g) ^ n)       🝖-[ congruence₂ᵣ(_∘_)(f ∘ g) ([^]-of-[∘] {f}{g} com {n}) ]
        (f ∘ g) ∘ ((f ^ n) ∘ (g ^ n)) 🝖-[ One.associate-commute4 {a = f} {g} {f ^ n}{g ^ n} (symmetry(_≡_) ([^]-commuting {f} {g} com {n} {1})) ]
        (f ∘ (f ^ n)) ∘ (g ∘ (g ^ n)) 🝖-[ reflexivity(_≡_) ]
        (f ^ 𝐒(n)) ∘ (g ^ 𝐒(n))       🝖-end

  module _ {ℓ₁}{ℓ₂} {X : Type{ℓ₁}} ⦃ equiv-x : Equiv{ℓₑ₁}(X) ⦄ {Y : Type{ℓ₂}} ⦃ equiv-y : Equiv{ℓₑ₂}(Y) ⦄ where
    private variable n : ℕ
    private variable x : X
    private variable init : Y

    repeatᵣₗ-flip-equality : ∀{_▫_ : Y → X → Y} → ⦃ op : BinaryOperator(_▫_) ⦄ → (repeatᵣ n (swap(_▫_)) x init ≡ repeatₗ n (_▫_) init x)
    repeatᵣₗ-flip-equality {n = 𝟎}                      = reflexivity(_≡_)
    repeatᵣₗ-flip-equality {n = 𝐒(n)}{x = x}{_▫_ = _▫_} = congruence₂ₗ(_▫_)(x) (repeatᵣₗ-flip-equality {n = n}{_▫_ = _▫_})

    repeatₗᵣ-flip-equality : ∀{_▫_ : X → Y → Y} → ⦃ op : BinaryOperator(_▫_) ⦄ → (repeatₗ n (swap _▫_) init x ≡ repeatᵣ n (_▫_) x init)
    repeatₗᵣ-flip-equality {n = n}{init = init}{x = x}{_▫_ = _▫_} = symmetry(_≡_) (repeatᵣₗ-flip-equality {n = n}{x = x}{init = init}{_▫_ = swap(_▫_)} ⦃ op = swap-binaryOperator ⦄)

  module _ ⦃ equiv-X : Equiv{ℓₑ}(X) ⦄ where
    private variable f : X → X
    private variable _▫_ : X → X → X
    private variable x elem init : X
    private variable n : ℕ

    [^]-from-repeatᵣ-alt : ⦃ func : Function(f) ⦄ → ((f ^ n) ⊜ repeatᵣ(n) (f ∘_) id)
    [^]-from-repeatᵣ-alt    {n = 𝟎}   = reflexivity(_≡_)
    [^]-from-repeatᵣ-alt {f}{n = 𝐒 n} = congruence₁(f) ([^]-from-repeatᵣ-alt {n = n})

    [^]-from-repeatᵣ : ⦃ func : Function(f) ⦄ → ((f ^ n) ⊜ repeatᵣ(n) (_∘_) f id)
    [^]-from-repeatᵣ    {n = 𝟎}   = reflexivity(_≡_)
    [^]-from-repeatᵣ {f}{n = 𝐒 n} = congruence₁(f) ([^]-from-repeatᵣ {f}{n = n})

    -- TODO: Should also be provable using associativity? Prove (CommutingOn(_▫_)(x)(x) → AssociativityOn(_▫_)(x)). Is this helping?
    repeat-swap-side : ⦃ op : BinaryOperator(_▫_) ⦄ ⦃ comm : Commutativity(_▫_) ⦄ → (repeatₗ n (_▫_) x x ≡ repeatᵣ n (_▫_) x x)
    repeat-swap-side            {n = 𝟎}      = reflexivity(_≡_)
    repeat-swap-side {_▫_ = _▫_}{n = 𝐒 n}{x} = congruence₂ₗ(_▫_)(x) (repeat-swap-side {n = n}) 🝖 commutativity(_▫_)

    repeat-swap-side-by-associativity : ⦃ op : BinaryOperator(_▫_) ⦄ ⦃ _ : Associativity(_▫_) ⦄ → (repeatₗ n (_▫_) x x ≡ repeatᵣ n (_▫_) x x)
    repeat-swap-side-by-associativity             {n = 𝟎}         = reflexivity(_≡_)
    repeat-swap-side-by-associativity             {n = 𝐒 𝟎}   {x} = reflexivity(_≡_)
    repeat-swap-side-by-associativity {_▫_ = _▫_} {n = 𝐒(𝐒 n)}{x} =
      repeatₗ (𝐒(𝐒(n))) (_▫_) x x        🝖[ _≡_ ]-[]
      repeatₗ (𝐒(n)) (_▫_) x x ▫ x       🝖[ _≡_ ]-[ congruence₂ₗ(_▫_)(x) (repeat-swap-side-by-associativity {n = 𝐒 n}) ]
      repeatᵣ (𝐒(n)) (_▫_) x x ▫ x       🝖[ _≡_ ]-[]
      (x ▫ repeatᵣ n (_▫_) x x) ▫ x      🝖[ _≡_ ]-[ associativity(_▫_) ]
      x ▫ (repeatᵣ n (_▫_) x x ▫ x)      🝖[ _≡_ ]-[ congruence₂ᵣ(_▫_)(x) (congruence₂ₗ(_▫_)(x) (repeat-swap-side-by-associativity {n = n})) ]-sym
      x ▫ (repeatₗ n (_▫_) x x ▫ x)      🝖[ _≡_ ]-[]
      x ▫ repeatₗ (𝐒(n)) (_▫_) x x       🝖[ _≡_ ]-[ congruence₂ᵣ(_▫_)(x) (repeat-swap-side-by-associativity {n = 𝐒(n)}) ]
      x ▫ repeatᵣ (𝐒(n)) (_▫_) x x       🝖[ _≡_ ]-[]
      repeatᵣ (𝐒(𝐒(n))) (_▫_) x x        🝖[ _≡_ ]-end

    repeat-with-id-swap-side : ⦃ op : BinaryOperator(_▫_) ⦄ ⦃ comm : Commutativity(_▫_) ⦄ ⦃ ident : Identity(_▫_)(init) ⦄ → (repeatₗ n (_▫_) init x ≡ repeatᵣ n (_▫_) x init)
    repeat-with-id-swap-side {n = 𝟎} = reflexivity(_≡_)
    repeat-with-id-swap-side {_▫_ = _▫_}{n = 𝐒 n}{x = x} = congruence₂ₗ(_▫_)(x) (repeat-with-id-swap-side {n = n}) 🝖 commutativity(_▫_)

    repeat-raise-equality : ⦃ op : BinaryOperator(_▫_) ⦄ → (repeatᵣ n (_▫_) elem (x) ≡ ((elem ▫_) ^ n)(x))
    repeat-raise-equality           {n = 𝟎}             = reflexivity(_≡_)
    repeat-raise-equality{_▫_ = _▫_}{n = 𝐒(n)}{elem}{x} = congruence₂ᵣ(_▫_)(elem) (repeat-raise-equality{_▫_ = _▫_}{n = n}{elem}{x})

module _ {X : Type{ℓ}} where
  open import Relator.Equals
  open import Relator.Equals.Proofs

  raise-repeat-equality : ∀{n : ℕ}{f : X → X} → (f ^ n ≡ repeatᵣ n (_∘_) f id)
  raise-repeat-equality{𝟎}       = reflexivity(_≡_)
  raise-repeat-equality{𝐒(n)}{f} = [≡]-with(f ∘_) (raise-repeat-equality{n}{f})

module _ where
  open import Structure.Setoid
  open        Structure.Function
  open        Structure.Operator

  module _ ⦃ equiv-X : Equiv{ℓₑ}(X) ⦄ where
    repeatₗ-by-0 : ∀{_▫_ : X → X → X}{x id} → ⦃ _ : Identityᵣ(_▫_)(id) ⦄ → (repeatᵣ 0 (_▫_) x id ≡ id)
    repeatₗ-by-0 {_▫_} {x}{id} ⦃ identᵣ ⦄ = reflexivity(_≡_)

    repeatₗ-by-1 : ∀{_▫_ : X → X → X}{x id} → ⦃ _ : Identityᵣ(_▫_)(id) ⦄ → (repeatᵣ 1 (_▫_) x id ≡ x)
    repeatₗ-by-1 {_▫_} {x}{id} ⦃ identᵣ ⦄ = identityᵣ(_▫_)(id)

    repeatₗ-by-sum : ∀{_▫_ : X → X → X}{x id} → ⦃ _ : BinaryOperator(_▫_) ⦄ → ⦃ _ : Identityᵣ(_▫_)(id) ⦄ → ⦃ _ : Associativity(_▫_) ⦄ → ∀{a b} → ((repeatₗ a (_▫_) id x) ▫ (repeatₗ b (_▫_) id x) ≡ repeatₗ (a + b) (_▫_) id x)
    repeatₗ-by-sum {_▫_} {x} {id} ⦃ identᵣ ⦄ {a} {𝟎}   =
      (repeatₗ a (_▫_) id x) ▫ (repeatₗ 𝟎 (_▫_) id x) 🝖-[ reflexivity(_≡_) ]
      (repeatₗ a (_▫_) id x) ▫ id                     🝖-[ identityᵣ(_▫_)(id) ]
      repeatₗ a (_▫_) id x                            🝖-[ reflexivity(_≡_) ]
      repeatₗ (a + 𝟎) (_▫_) id x                      🝖-end
    repeatₗ-by-sum {_▫_} {x} {id} ⦃ identᵣ ⦄ {a} {𝐒 b} =
      (repeatₗ a (_▫_) id x) ▫ (repeatₗ (𝐒(b)) (_▫_) id x)  🝖-[ reflexivity(_≡_) ]
      (repeatₗ a (_▫_) id x) ▫ ((repeatₗ b (_▫_) id x) ▫ x) 🝖-[ symmetry(_≡_) (associativity(_▫_)) ]
      ((repeatₗ a (_▫_) id x) ▫ (repeatₗ b (_▫_) id x)) ▫ x 🝖-[ congruence₂ₗ(_▫_)(_) (repeatₗ-by-sum{a = a}{b = b}) ]
      (repeatₗ (a + b) (_▫_) id x) ▫ x                      🝖-[ reflexivity(_≡_) ]
      repeatₗ (a + 𝐒(b)) (_▫_) id x                         🝖-end

    repeatₗ-by-product : ∀{_▫_ : X → X → X}{x id} → ⦃ _ : BinaryOperator(_▫_) ⦄ → ⦃ _ : Identityᵣ(_▫_)(id) ⦄ → ⦃ _ : Associativity(_▫_) ⦄ → ∀{a b} → (repeatₗ b (_▫_) id ((repeatₗ a (_▫_) id x)) ≡ repeatₗ (a ⋅ b) (_▫_) id x)
    repeatₗ-by-product {_▫_} {x} {id} ⦃ identᵣ ⦄ {a} {𝟎}   =
      repeatₗ 𝟎 (_▫_) id ((repeatₗ a (_▫_) id x)) 🝖-[ reflexivity(_≡_) ]
      repeatₗ (a ⋅ 𝟎) (_▫_) id x                  🝖-end
    repeatₗ-by-product {_▫_} {x} {id} ⦃ identᵣ ⦄ {a} {𝐒 b} =
      repeatₗ (𝐒(b)) (_▫_) id ((repeatₗ a (_▫_) id x))                       🝖-[ reflexivity(_≡_) ]
      (repeatₗ b (_▫_) id ((repeatₗ a (_▫_) id x))) ▫ (repeatₗ a (_▫_) id x) 🝖-[ congruence₂ₗ(_▫_)(_) (repeatₗ-by-product{a = a}{b = b}) ]
      (repeatₗ (a ⋅ b) (_▫_) id x) ▫ (repeatₗ a (_▫_) id x)                  🝖-[ repeatₗ-by-sum {a = a ⋅ b}{a} ]
      repeatₗ ((a ⋅ b) + a) (_▫_) id x                                       🝖-[ [≡]-to-equivalence (congruence₁(expr ↦ repeatₗ expr (_▫_) id x) {a ⋅ b + a}{a + a ⋅ b} (commutativity(_+_) {a ⋅ b})) ]
      repeatₗ (a ⋅ 𝐒(b)) (_▫_) id x                                          🝖-end
      where
        open import Relator.Equals.Proofs.Equiv using ([≡]-to-equivalence)

    repeatₗ-by-distanceₗ : ∀{_▫_ : X → X → X}{x id} → ⦃ _ : BinaryOperator(_▫_) ⦄ → ⦃ _ : Identityᵣ(_▫_)(id) ⦄ → ⦃ _ : Associativity(_▫_) ⦄ → ∀{a b} → (repeatₗ a (_▫_) id x ≡ repeatₗ b (_▫_) id x) ← (repeatₗ (a 𝄩 b) (_▫_) id x ≡ id)
    repeatₗ-by-distanceₗ {_▫_} {x} {id} {𝟎}   {𝟎}   p = p
    repeatₗ-by-distanceₗ {_▫_} {x} {id} {𝟎}   {𝐒 b} p = symmetry(_≡_) p
    repeatₗ-by-distanceₗ {_▫_} {x} {id} {𝐒 a} {𝟎}   p = p
    repeatₗ-by-distanceₗ {_▫_} {x} {id} {𝐒 a} {𝐒 b} p = congruence₂ₗ(_▫_)(_) (repeatₗ-by-distanceₗ {_▫_} {x} {id} {a} {b} p)

    repeatₗ-by-distanceᵣ : ∀{_▫_ : X → X → X}{x id} → ⦃ _ : BinaryOperator(_▫_) ⦄ → ⦃ _ : Identityᵣ(_▫_)(id) ⦄ → ⦃ _ : Associativity(_▫_) ⦄ → ⦃ cancᵣ : Cancellationᵣ(_▫_) ⦄ → ∀{a b} → (repeatₗ a (_▫_) id x ≡ repeatₗ b (_▫_) id x) → (repeatₗ (a 𝄩 b) (_▫_) id x ≡ id)
    repeatₗ-by-distanceᵣ {_▫_} {x} {id} {𝟎}   {𝟎}   p = p
    repeatₗ-by-distanceᵣ {_▫_} {x} {id} {𝟎}   {𝐒 b} p = symmetry(_≡_) p
    repeatₗ-by-distanceᵣ {_▫_} {x} {id} {𝐒 a} {𝟎}   p = p
    repeatₗ-by-distanceᵣ {_▫_} {x} {id} {𝐒 a} {𝐒 b} p = repeatₗ-by-distanceᵣ {_▫_} {x} {id} {a} {b} (cancellationᵣ(_▫_) {x} p)

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:
module Vec where

open import Star
open import Nat

data Step (A : Set) : Nat -> Nat -> Set where
  step : (x : A){n : Nat} -> Step A (suc n) n

Vec : (A : Set) -> Nat -> Set
Vec A n = Star (Step A) n zero

[] : {A : Set} -> Vec A zero
[] = ε

_::_ : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (suc n)
x :: xs = step x • xs

_+++_ : {A : Set}{n m : Nat} -> Vec A n -> Vec A m -> Vec A (n + m)
_+++_ {A}{m = m} xs ys = map +m step+m xs ++ ys
  where
    +m = \z -> z + m
    step+m : Step A =[ +m ]=> Step A
    step+m (step x) = step x

vec : {A : Set}{n : Nat} -> A -> Vec A n
vec {n = ε}     x = []
vec {n = _ • n} x = x :: vec x

_⊗_ : {A B : Set}{n : Nat} -> Vec (A -> B) n -> Vec A n -> Vec B n
ε             ⊗ ε             = []
(step f • fs) ⊗ (step x • xs) = f x :: (fs ⊗ xs)
ε             ⊗ (() • _)

{- Some proof about _-_ needed...

vreverse : {A : Set}{n : Nat} -> Vec A n -> Vec A n
vreverse {A}{n} xs = {! !} -- map i f (reverse xs)
  where
    i : Nat -> Nat
    i m = n - m

    f : Step A op =[ i ]=> Step A
    f (step x) = {! !} -- step x
-}

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module sv20.exam2 where

-------------------------- FIRST TASK PREPARATION CODE --------------------------
open import Data.Unit using (⊤; tt)
open import Data.Product using (_×_ ; ∃) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary using (¬_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_∘_)
import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _≡˘⟨_⟩_; _∎)
open Eq using (_≡_; refl; cong; sym; trans)

Subset : (A : Set) -> Set _
Subset A = A → Set

_∈_ : ∀ {A} → A → Subset A → Set
a ∈ P = P a

Relation : ∀ A B → Set₁
Relation A B = Subset (A × B)

Range : ∀ {A B} → Relation A B → Subset B
Range R b = ∃ (R ∘ ⟨_, b ⟩)  -- equivalent to ∃ \a → R ⟨ a , b ⟩

Dom : ∀ {A B} → Relation A B → Subset A
Dom R a = ∃ (R ∘ ⟨ a ,_⟩)  -- equivalent to ∃ \b → R ⟨ a , b ⟩

_⊆_ : ∀ {A} → Subset A → Subset A → Set
A ⊆ B = ∀ x → x ∈ A → x ∈ B

_∩_ : ∀ {A} → Subset A → Subset A → Subset A
A ∩ B = λ x → x ∈ A × x ∈ B

_∪_ : ∀ {A} → Subset A → Subset A → Subset A
A ∪ B = λ x → x ∈ A ⊎ x ∈ B

_/_ : ∀ {A} → Subset A → Subset A → Subset A
A / B = λ x → x ∈ A × ¬ (x ∈ B)

postulate
  ⊆→≡ : ∀ {a} {A B : Subset a} → A ⊆ B → B ⊆ A → A ≡ B

-------------------------- Solution to TASK 1 --------------------------

diff-theorem-3 : ∀ {a} {A B : Subset a}
               → (A / (A ∩ B)) ≡ (A / B)
-- The proof is divided in two parts, forwards (right contained in left) and
-- backwards (left contained in right)
diff-theorem-3 = ⊆→≡ diff-theorem-3→ diff-theorem-3←
  where
    diff-theorem-3→ : ∀ {a} {A B : Subset a}
                    → (A / (A ∩ B)) ⊆ (A / B)
    diff-theorem-3→ x x∈A/A∩B =           -- Given an x such that `x ∈ (A / (A ∩ B))`
      let
        ⟨ x∈A , ¬x∈A∩B ⟩ = x∈A/A∩B        -- (1) By def. of diff, we have that `x ∈ A` and `¬ x ∈ A ∩ B`
        ¬x∈B  =                           -- (2) Proof by contradiction that ¬ x ∈ B
               λ{ x∈B →                    -- (a) Suppose `x ∈ B`
               let x∈A∩B = ⟨ x∈A , x∈B ⟩   -- (b) then by def. of ∩ and (1) (a), we have that `x ∈ A ∩ B`
               in ¬x∈A∩B x∈A∩B }           -- Contradiction `x ∈ A ∩ B` (b) and `¬ x ∈ A ∩ B` (1).
        x∈A/B = ⟨ x∈A , ¬x∈B ⟩            -- From (1), (2) and by def. of /, we have that `x ∈ A / B`
      in x∈A/B                            -- QED
    --Proof without comments
    --diff-theorem-3→ x ⟨ x∈A , ¬x∈A∩B ⟩ = ⟨ x∈A , (λ{x∈B → ¬x∈A∩B ⟨ x∈A , x∈B ⟩}) ⟩

    diff-theorem-3← : ∀ {a} {A B : Subset a}
                    → (A / B) ⊆ (A / (A ∩ B))
    diff-theorem-3← x x∈A/B =             -- Given an x such that `x ∈ A / B`
      let
        ⟨ x∈A , ¬x∈B ⟩ = x∈A/B            -- (1) By def. of diff, we have that `x ∈ A` and `¬ x ∈ B`
        ¬x∈A∩B =                          -- (2) Proof by contradiction that `¬ x ∈ A ∩ B`
                λ{ x∈A∩B →                 -- (a) Suppose `x ∈ A ∩ B`
                let ⟨ x∈A , x∈B ⟩ = x∈A∩B  -- (b) then by def. of ∩, we have that `x ∈ A` and `x ∈ B`
                in ¬x∈B x∈B }              -- Contraduction `x ∈ B` (b) and `¬ x ∈ B` (1)
        x∈A/A∩B = ⟨ x∈A , ¬x∈A∩B ⟩        -- From (1), (2) and by the def. of /, `x ∈ (A / (A ∩ B))`
      in x∈A/A∩B                          -- QED
    --Proof without comments
    --diff-theorem-3← x ⟨ x∈A , ¬x∈B ⟩ = ⟨ x∈A , (λ{⟨ x∈A , x∈B ⟩ → ¬x∈B x∈B}) ⟩

-- This might be another way to prove it, it still seems to require some postulate to work
--diff-theorem-3` : ∀ {a} {A B : Subset a}
--                (y : a)
--                → y ∈ (A / (A ∩ B)) ≡ y ∈ (A / B)
---- The proof is divided in two parts, forwards (right contained in left) and
---- backwards (left contained in right)
--diff-theorem-3` {_} {A} {B} y =
--  begin
--    y ∈ (A / (A ∩ B))
--  ≡⟨⟩
--    (A / (A ∩ B)) y
--  ≡⟨⟩
--    (A y × ¬ (A y × B y))
--  ≡⟨ cong (A y ×_) ? ⟩
--    (A y × ¬ (B y))
--  ≡⟨⟩
--    (A / B) y
--  ≡⟨⟩
--    y ∈ (A / B)
--  ∎

-------------------------- END FIRST TASK --------------------------

-------------------------- SECOND TASK PREPARATION CODE --------------------------

open import Data.List using (List; []; _∷_; _++_; length; reverse; map; foldr; downFrom; foldl)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties using (*-identityʳ; +-identityʳ; *-assoc)

pattern [_] z = z ∷ []

product : List ℕ → ℕ
product [] = 1
product (n ∷ ns) = n * product ns

-------------------------- Solution to TASK 2 --------------------------

of-singleton : ∀ (n : ℕ) → product [ n ] ≡ n
of-singleton n =
  begin
    product [ n ]     ≡⟨⟩
    product (n ∷ [])  ≡⟨⟩
    n * product []    ≡⟨⟩
    n * 1             ≡⟨ *-identityʳ n ⟩
    n
  ∎

of-join : ∀ (ms ns : List ℕ)
        → product (ms ++ ns) ≡ (product ms) * (product ns)
of-join [] ns =
  begin
    product ([] ++ ns)       ≡⟨⟩
    product ns               ≡˘⟨ +-identityʳ (product ns) ⟩  -- product ns ≡ 1 * product ns
    1 * product ns           ≡⟨⟩
    product [] * product ns
  ∎
of-join (m ∷ ms) ns =
  begin
    product ((m ∷ ms) ++ ns)        ≡⟨⟩
    product (m ∷ (ms ++ ns))        ≡⟨⟩
    m * product (ms ++ ns)          ≡⟨ cong (m *_) (of-join ms ns) ⟩ -- product (ms ++ ns) ≡ product ms * product ns
    m * (product ms * product ns)   ≡˘⟨ *-assoc m (product ms) (product ns) ⟩ -- * associativity
    (m * product ms) * product ns   ≡⟨⟩
    product (m ∷ ms) * product ns
  ∎

-------------------------- END SECOND TASK --------------------------


text:
------------------------------------------------------------------------
-- A parser for PBM images; illustrates "essential" use of bind
------------------------------------------------------------------------

-- Note that I am using the simple "Plain PBM" format, and I try to
-- adhere to the following statement from the pbm man page:
--
--   "Programs that read this format should be as lenient as possible,
--   accepting anything that looks remotely like a bitmap."

-- I got the idea to write this particular parser from "The Power of
-- Pi" by Oury and Swierstra.

module TotalParserCombinators.Examples.PBM where

open import Data.Bool
open import Data.Char as Char using (Char; _==_)
open import Data.List as List using (List)
open import Data.Maybe hiding (_>>=_)
open import Data.Nat hiding (_^_)
import Data.Nat.Show as ℕ
open import Data.String as String
  using (String) renaming (_++_ to _<+>_)
open import Data.Unit
open import Data.Vec as Vec using (Vec; _++_; [_])
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open import TotalParserCombinators.BreadthFirst
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser

open Token Char Char._≟_

------------------------------------------------------------------------
-- PBM images

module PBM where

  -- Colours.

  data Colour : Set where
    white : Colour
    black : Colour

  -- Matrices.

  Matrix : Set → ℕ → ℕ → Set
  Matrix A rows cols = Vec (Vec A cols) rows

  -- PBM images.

  record PBM : Set where
    constructor toPBM
    field
      {rows cols} : ℕ
      matrix      : Matrix Colour rows cols

  open PBM public

  -- Showing PBM images.

  showColour : Colour → Char
  showColour white = '0'
  showColour black = '1'

  show : PBM → String
  show i = "P1\n" <+>
           ℕ.show (cols i) <+> " " <+> ℕ.show (rows i) <+> "\n" <+>
           showMatrix (matrix i)
    where
    showMatrix = String.fromList ∘
                 Vec.toList ∘
                 Vec.concat ∘
                 Vec.map ((λ xs → xs ++ [ '\n' ]) ∘ Vec.map showColour)

open PBM

------------------------------------------------------------------------
-- Parsing PBM images

comment : Parser Char ⊤ _
comment =
  tok '#'                  >>= λ _ →
  sat′ (not ∘ _==_ '\n') ⋆ >>= λ _ →
  tok '\n'                 >>= λ _ →
  return tt

colour : Parser Char Colour _
colour = const white <$> tok '0'
       ∣ const black <$> tok '1'

pbm : Parser Char PBM _
pbm =
  w∣c ⋆                                  >>= λ _ →
  tok 'P' >>= λ _ → tok '1'              >>= λ _ →
  w∣c ⋆                                  >>= λ _ →
  number                                 >>= λ cols →
  w∣c +                                  >>= λ _ →
  number                                 >>= λ rows →
  w∣c                                    >>= λ _ →
  (w∣c ⋆ >>= λ _ → colour) ^ cols ^ rows >>= λ m →
  token ⋆                                >>= λ _ →
  return (toPBM m)
  where
  w∣c = whitespace ∣ comment

-- The example is commented out, because it takes ages to run this
-- parser.

-- module Example where

--   open Vec.Vec

--   image = toPBM ((white ∷ black ∷ []) ∷
--                  (black ∷ white ∷ []) ∷
--                  (black ∷ black ∷ []) ∷ [])

--   ex : parse pbm (String.toList $ show image) ≡ List.[_] image
--   ex = P.refl

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module L where

open import Data.Nat using (ℕ; suc) -- ; _*_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans)
open import Data.Product
open import Data.Empty

-- Recursion principle

recℕ : (C : Set) → C → (ℕ → C → C) → ℕ → C
recℕ C c f 0 = c
recℕ C c f (suc n) = f n (recℕ C c f n)

double : ℕ → ℕ
double = recℕ ℕ 0 (λ n r → suc (suc r))

add : ℕ → ℕ → ℕ
add = recℕ (ℕ → ℕ) (λ n → n) (λ m r → λ n → suc (r n))

-- fact : ℕ → ℕ
-- fact = recℕ ℕ 1 (λ n r → suc n * r)

-- Induction principle

indℕ : (C : ℕ → Set) → C 0 → ((n : ℕ) → C n → C (suc n)) → (n : ℕ) → C n
indℕ C c f 0 = c
indℕ C c f (suc n) = f n (indℕ C c f n)

add-assoc : (i j k : ℕ) → add i (add j k) ≡ add (add i j) k
add-assoc = indℕ
              (λ i → (j k : ℕ) → add i (add j k) ≡ add (add i j) k)
              (λ j k → refl)
              (λ i i+[j+k]≡[i+j]+k j k → cong suc (i+[j+k]≡[i+j]+k j k))

add-right-unit : (i : ℕ) → add i 0 ≡ i
add-right-unit = indℕ (λ i → add i 0 ≡ i) refl (λ i i+0≡i → cong suc i+0≡i)

add-suc : (i j : ℕ) → suc (add i j) ≡ add i (suc j)
add-suc = indℕ (λ i → (j : ℕ) → suc (add i j) ≡ add i (suc j))
               (λ j → refl)
               (λ i s[i+j]≡i+s[j] j → cong suc (s[i+j]≡i+s[j] j))

add-comm : (i j : ℕ) → add i j ≡ add j i
add-comm = indℕ
             (λ i → (j : ℕ) → add i j ≡ add j i)
             (λ j → sym (add-right-unit j))
             (λ i i+j≡j+i j → trans (cong suc (i+j≡j+i j)) (add-suc j i))

-- Some type definitions

_≤_ : (i j : ℕ) → Set
i ≤ j = Σ[ k ∈ ℕ ] (add i k ≡ j)

i≤i+j : (i j : ℕ) → i ≤ add i j
i≤i+j = indℕ
          (λ i → (j : ℕ) → i ≤ add i j)
          (λ j → (j , refl))
          (λ i i≤i+j j → (j , refl))

¬ : Set → Set
¬ A = A → ⊥

_<_ : (i j : ℕ) → Set
i < j = (i ≤ j) × ¬ (i ≡ j)

0≠si : (i : ℕ) → ¬ (0 ≡ suc i)
0≠si i = λ ()

0< : (i : ℕ) → (0 < suc i)
0< = indℕ  (λ i → 0 < suc i)
           {!!}
           {!!}

max_stars_repo_name: andmkent/misc-HoTT

max_issues_repo_name: andmkent/misc-HoTT

max_forks_repo_name: andmkent/misc-HoTT


text:
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

module MLib.Matrix.Tensor {c ℓ} (struct : Struct bimonoidCode c ℓ) where

open import MLib.Prelude
open import MLib.Matrix.Core
open import MLib.Matrix.Equality struct
open import MLib.Matrix.Mul struct
open import MLib.Algebra.Operations struct

open Table using (head; tail; rearrange; fromList; toList; _≗_; replicate)
open Nat using () renaming (_+_ to _+ℕ_; _*_ to _*ℕ_)

open FunctionProperties

open import MLib.Fin.Parts.Simple

-- Tensor product

_⊠_ : ∀ {m n p q} → Matrix S m n → Matrix S p q → Matrix S (m *ℕ p) (n *ℕ q)
(A ⊠ B) i j =
  let i₁ , i₂ = toParts i
      j₁ , j₂ = toParts j
  in A i₁ j₁ *′ B i₂ j₂

private
  ≡⇒≡×≡×≡ :
    ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
    {i i′ : A} {j j′ : B} {k k′ : C} →
    (i , j , k) ≡ (i′ , j′ , k′) →
    i ≡ i′ × j ≡ j′ × k ≡ k′
  ≡⇒≡×≡×≡ = Σ.map id Σ.≡⇒≡×≡ ∘ Σ.≡⇒≡×≡

open _≃_

module _ ⦃ props : Has (associative on * ∷ []) ⦄ {m n p q r s} where

  ⊠-associative :
    (A : Matrix S m n) (B : Matrix S p q) (C : Matrix S r s) →
    (A ⊠ B) ⊠ C ≃ A ⊠ (B ⊠ C)
  ⊠-associative A B C .m≡p = Nat.*-assoc m p r
  ⊠-associative A B C .n≡q = Nat.*-assoc n q s
  ⊠-associative A B C .equal {i} {i′} {j} {j′} i≅i′ j≅j′ =
    let i₁ , i₂ , i₃ = toParts³ m p r i
        j₁ , j₂ , j₃ = toParts³ n q s j

        i′₁ , i′₂ , i′₃ = toParts³′ m p r i′
        j′₁ , j′₂ , j′₃ = toParts³′ n q s j′

        i₁-eq , i₂-eq , i₃-eq = ≡⇒≡×≡×≡ (toParts-assoc m p r i≅i′)
        j₁-eq , j₂-eq , j₃-eq = ≡⇒≡×≡×≡ (toParts-assoc n q s j≅j′)

        open EqReasoning S.setoid
    in begin
      ((A ⊠ B) ⊠ C) i j                        ≡⟨⟩
      A i₁ j₁ *′ B i₂ j₂ *′ C i₃ j₃            ≈⟨ from props (associative on *) _ _ _ ⟩
      A i₁ j₁ *′ (B i₂ j₂ *′ C i₃ j₃)          ≡⟨ ≡.cong₂ _*′_ (≡.cong₂ A i₁-eq j₁-eq) (≡.cong₂ _*′_ (≡.cong₂ B i₂-eq j₂-eq) (≡.cong₂ C i₃-eq j₃-eq)) ⟩
      A i′₁ j′₁ *′ (B i′₂ j′₂ *′ C i′₃ j′₃)    ≡⟨⟩
      (A ⊠ (B ⊠ C)) i′ j′                      ∎

⊠-cong : ∀ {m n m′ n′} {p q p′ q′} {A : Matrix S m n} {A′ : Matrix S m′ n′} {B : Matrix S p q} {B′ : Matrix S p′ q′} → A ≃ A′ → B ≃ B′ → (A ⊠ B) ≃ (A′ ⊠ B′)
⊠-cong A≃A′ B≃B′ with A≃A′ .m≡p | B≃B′ .m≡p | A≃A′ .n≡q | B≃B′ .n≡q
⊠-cong {A = A} {A′} {B} {B′} A≃A′ B≃B′ | ≡.refl | ≡.refl | ≡.refl | ≡.refl = lem
  where
  lem : (A ⊠ B) ≃ (A′ ⊠ B′)
  lem .m≡p = ≡.refl
  lem .n≡q = ≡.refl
  lem .equal ≅.refl ≅.refl = cong * (A≃A′ .equal ≅.refl ≅.refl) (B≃B′ .equal ≅.refl ≅.refl)

⊠-identityˡ :
  ⦃ props : Has (1# is leftIdentity for * ∷ []) ⦄ →
  ∀ {m n} (A : Matrix S m n) → 1● {1} ⊠ A ≃ A
⊠-identityˡ A .m≡p = Nat.*-identityˡ _
⊠-identityˡ A .n≡q = Nat.*-identityˡ _
⊠-identityˡ ⦃ props ⦄ A .equal {i} {i′} {j} {j′} i≅i′ j≅j′ =
  let i₁ , i₂ = toParts {1} i
      j₁ , j₂ = toParts {1} j
      -- x  : i₁ ≡ zero
      -- x′ : i₂ ≡ i′
      -- y  : j₁ ≡ zero
      -- y′ : j₂ ≡ j′
      x , x′ = Σ.≡⇒≡×≡ (toParts-1ˡ i i′ i≅i′)
      y , y′ = Σ.≡⇒≡×≡ (toParts-1ˡ j j′ j≅j′)

      open EqReasoning S.setoid
  in begin
    (1● {1} ⊠ A) i j           ≡⟨⟩
    1● {1} i₁ j₁     *′ A i₂ j₂ ≡⟨ ≡.cong₂ _*′_ (≡.cong₂ (1● {1}) x y) (≡.cong₂ A x′ y′) ⟩
    1● {1} zero zero *′ A i′ j′ ≡⟨⟩
    1′               *′ A i′ j′ ≈⟨ from props (1# is leftIdentity for *) _ ⟩
    A i′ j′ ∎

⊠-identityʳ :
  ⦃ props : Has (1# is rightIdentity for * ∷ []) ⦄ →
  ∀ {m n} (A : Matrix S m n) → A ⊠ 1● {1} ≃ A
⊠-identityʳ A .m≡p = Nat.*-identityʳ _
⊠-identityʳ A .n≡q = Nat.*-identityʳ _
⊠-identityʳ A .equal {i} {i′} {j} {j′} i≅i′ j≅j′ with Σ.≡⇒≡×≡ (toParts-1ʳ i i′ i≅i′) | Σ.≡⇒≡×≡ (toParts-1ʳ j j′ j≅j′)
⊠-identityʳ ⦃ props ⦄ A .equal {i} {i′} {j} {j′} i≅i′ j≅j′ | x , x′ | y , y′
  rewrite x | x′ | y | y′ = from props (1# is rightIdentity for *) _


text:
open import Prelude
open import Nat
open import core
open import contexts
open import lemmas-disjointness

module lemmas-freshness where
  -- if x is fresh in an eexp, it's fresh in its expansion
  mutual
    fresh-elab-synth1 : ∀{x e τ d Γ Δ} →
                         x # Γ →
                         freshe x e →
                         Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                         fresh x d
    fresh-elab-synth1 _ FRHConst ESConst = FConst
    fresh-elab-synth1 apt (FRHAsc frsh) (ESAsc x₁) = FCast (fresh-elab-ana1 apt frsh x₁)
    fresh-elab-synth1 _ (FRHVar x₂) (ESVar x₃) = FVar x₂
    fresh-elab-synth1 {Γ = Γ} apt (FRHLam2 x₂ frsh) (ESLam x₃ exp) = FLam x₂ (fresh-elab-synth1 (apart-extend1 Γ x₂ apt) frsh exp)
    fresh-elab-synth1 apt FRHEHole ESEHole = FHole (EFId apt)
    fresh-elab-synth1 apt (FRHNEHole frsh) (ESNEHole x₁ exp) = FNEHole (EFId apt) (fresh-elab-synth1 apt frsh exp)
    fresh-elab-synth1 apt (FRHAp frsh frsh₁) (ESAp x₁ x₂ x₃ x₄ x₅ x₆) =
                               FAp (FCast (fresh-elab-ana1 apt frsh x₅))
                                   (FCast (fresh-elab-ana1 apt frsh₁ x₆))
    fresh-elab-synth1 apt (FRHLam1 x₁ frsh) ()
    fresh-elab-synth1 apt (FRHFst frsh) (ESFst s m esana) = FFst (FCast (fresh-elab-ana1 apt frsh esana))
    fresh-elab-synth1 apt (FRHSnd frsh) (ESSnd s m esana) = FSnd (FCast (fresh-elab-ana1 apt frsh esana))
    fresh-elab-synth1 apt (FRHPair frsh frsh₁) (ESPair x₁ x₂ exp exp₁) = FPair (fresh-elab-synth1 apt frsh exp)
                                                                           (fresh-elab-synth1 apt frsh₁ exp₁)

    fresh-elab-ana1 : ∀{ x e τ d τ' Γ Δ} →
                      x # Γ →
                      freshe x e →
                      Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                      fresh x d
    fresh-elab-ana1 {Γ = Γ}  apt (FRHLam1 x₁ frsh) (EALam x₂ x₃ exp) = FLam x₁ (fresh-elab-ana1 (apart-extend1 Γ x₁ apt) frsh exp )
    fresh-elab-ana1 apt frsh (EASubsume x₁ x₂ x₃ x₄) = fresh-elab-synth1 apt frsh x₃
    fresh-elab-ana1 apt FRHEHole EAEHole = FHole (EFId apt)
    fresh-elab-ana1 apt (FRHNEHole frsh) (EANEHole x₁ x₂) = FNEHole (EFId apt) (fresh-elab-synth1 apt frsh x₂)

  -- if x is fresh in the expansion of an eexp, it's fresh in that eexp
  mutual
    fresh-elab-synth2 : ∀{x e τ d Γ Δ} →
                         fresh x d →
                         Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                         freshe x e
    fresh-elab-synth2 FConst ESConst = FRHConst
    fresh-elab-synth2 (FVar x₂) (ESVar x₃) = FRHVar x₂
    fresh-elab-synth2 (FLam x₂ frsh) (ESLam x₃ exp) = FRHLam2 x₂ (fresh-elab-synth2 frsh exp)
    fresh-elab-synth2 (FHole x₁) ESEHole = FRHEHole
    fresh-elab-synth2 (FNEHole x₁ frsh) (ESNEHole x₂ exp) = FRHNEHole (fresh-elab-synth2 frsh exp)
    fresh-elab-synth2 (FAp (FCast frsh) (FCast frsh₁)) (ESAp x₁ x₂ x₃ x₄ x₅ x₆) =
                        FRHAp (fresh-elab-ana2 frsh x₅)
                              (fresh-elab-ana2 frsh₁ x₆)
    fresh-elab-synth2 (FCast frsh) (ESAsc x₁) = FRHAsc (fresh-elab-ana2 frsh x₁)
    fresh-elab-synth2 (FFailedCast frsh) ()
    fresh-elab-synth2 (FFst (FCast frsh)) (ESFst s m esana) = FRHFst (fresh-elab-ana2 frsh esana)
    fresh-elab-synth2 (FSnd (FCast frsh)) (ESSnd s m esana) = FRHSnd (fresh-elab-ana2 frsh esana)
    fresh-elab-synth2 (FPair frsh frsh₁) (ESPair x₁ x₂ exp exp₁) = FRHPair (fresh-elab-synth2 frsh exp) (fresh-elab-synth2 frsh₁ exp₁)

    fresh-elab-ana2 : ∀{ x e τ d τ' Γ Δ} →
                      fresh x d →
                      Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                      freshe x e
    fresh-elab-ana2 (FLam x₁ frsh) (EALam x₂ x₃ exp) = FRHLam1 x₁ (fresh-elab-ana2 frsh exp)
    fresh-elab-ana2 frsh (EASubsume x₁ x₂ x₃ x₄) = fresh-elab-synth2 frsh x₃
    fresh-elab-ana2 (FHole x₁) EAEHole = FRHEHole
    fresh-elab-ana2 (FNEHole x₁ frsh) (EANEHole x₂ x₃) = FRHNEHole (fresh-elab-synth2 frsh x₃)

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
module Issue499 where

data A : Set where
  a : A

data B : Set where
  b : .A → B

data C : B → Set where
  c : C (b a)

f : ∀ {i} → C i → A
f x = {!!} -- Hitting C-c C-c x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import HoTT

module cw.cohomology.GridMap {i j k}
  {A : Type i} {B : Type j} {C : Type k}
  (f : A → B) (g : B → C) where

  B/A = Cofiber f
  C/A = Cofiber (g ∘ f)
  C/B = Cofiber g

  B/A-to-C/A-span-map : SpanMap (cofiber-span f) (cofiber-span (g ∘ f))
  B/A-to-C/A-span-map = span-map (idf _) g (idf _)
    (comm-sqr λ _ → idp) (comm-sqr λ _ → idp)
  module B/AToC/A = PushoutFmap B/A-to-C/A-span-map
  B/A-to-C/A : B/A → C/A
  B/A-to-C/A = B/AToC/A.f

  C/A-to-C/B-span-map : SpanMap (cofiber-span (g ∘ f)) (cofiber-span g)
  C/A-to-C/B-span-map = span-map (idf _) (idf _) f
    (comm-sqr λ _ → idp) (comm-sqr λ _ → idp)
  module C/AToC/B = PushoutFmap C/A-to-C/B-span-map
  C/A-to-C/B : C/A → C/B
  C/A-to-C/B = C/AToC/B.f

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
------------------------------------------------------------------------------
-- The gcd is divisible by any common divisor
------------------------------------------------------------------------------

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

module FOTC.Program.GCD.Total.DivisibleATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Divisibility.By0
open import FOTC.Data.Nat.Divisibility.By0.PropertiesATP
open import FOTC.Data.Nat.Induction.NonAcc.LexicographicATP
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesATP
open import FOTC.Data.Nat.Inequalities.PropertiesATP
open import FOTC.Data.Nat.PropertiesATP
open import FOTC.Program.GCD.Total.Definitions
open import FOTC.Program.GCD.Total.GCD

------------------------------------------------------------------------------
-- The gcd 0 0 is Divisible.
postulate gcd-00-Divisible : Divisible zero zero (gcd zero zero)
{-# ATP prove gcd-00-Divisible #-}

-- The gcd 0 (succ n) is Divisible.
postulate
  gcd-0S-Divisible : ∀ {n} → N n → Divisible zero (succ₁ n) (gcd zero (succ₁ n))
{-# ATP prove gcd-0S-Divisible #-}

postulate
  gcd-S0-Divisible : ∀ {n} → N n → Divisible (succ₁ n) zero (gcd (succ₁ n) zero)
{-# ATP prove gcd-S0-Divisible #-}

------------------------------------------------------------------------------
-- The gcd (succ₁ m) (succ₁ n) when succ₁ m > succ₁ n is Divisible.
-- For the proof using the ATP we added the helper hypothesis
-- c | succ₁ m → c | succ₁ c → c | succ₁ m ∸ succ₁ n.
postulate
  gcd-S>S-Divisible-ah :
    ∀ {m n} → N m → N n →
    (Divisible (succ₁ m ∸ succ₁ n) (succ₁ n) (gcd (succ₁ m ∸ succ₁ n) (succ₁ n))) →
    succ₁ m > succ₁ n →
    ∀ c → N c → CD (succ₁ m) (succ₁ n) c →
    (c ∣ succ₁ m ∸ succ₁ n) →
    c ∣ gcd (succ₁ m) (succ₁ n)
{-# ATP prove gcd-S>S-Divisible-ah #-}

gcd-S>S-Divisible :
  ∀ {m n} → N m → N n →
  (Divisible (succ₁ m ∸ succ₁ n) (succ₁ n) (gcd (succ₁ m ∸ succ₁ n) (succ₁ n))) →
  succ₁ m > succ₁ n →
  Divisible (succ₁ m) (succ₁ n) (gcd (succ₁ m) (succ₁ n))
gcd-S>S-Divisible {m} {n} Nm Nn acc Sm>Sn c Nc (c∣Sm , c∣Sn) =
    gcd-S>S-Divisible-ah Nm Nn acc Sm>Sn c Nc (c∣Sm , c∣Sn)
                         (x∣y→x∣z→x∣y∸z Nc (nsucc Nm) (nsucc Nn) c∣Sm c∣Sn)

------------------------------------------------------------------------------
-- The gcd (succ₁ m) (succ₁ n) when succ₁ m ≯ succ₁ n is Divisible.
-- For the proof using the ATP we added the helper hypothesis
-- c | succ₁ n → c | succ₁ m → c | succ₁ n ∸ succ₁ m.
postulate
  gcd-S≯S-Divisible-ah :
    ∀ {m n} → N m → N n →
    (Divisible (succ₁ m) (succ₁ n ∸ succ₁ m) (gcd (succ₁ m) (succ₁ n ∸ succ₁ m))) →
    succ₁ m ≯ succ₁ n →
    ∀ c → N c → CD (succ₁ m) (succ₁ n) c →
    (c ∣ succ₁ n ∸ succ₁ m) →
    c ∣ gcd (succ₁ m) (succ₁ n)
{-# ATP prove gcd-S≯S-Divisible-ah #-}

gcd-S≯S-Divisible :
  ∀ {m n} → N m → N n →
  (Divisible (succ₁ m) (succ₁ n ∸ succ₁ m) (gcd (succ₁ m) (succ₁ n ∸ succ₁ m))) →
  succ₁ m ≯ succ₁ n →
  Divisible (succ₁ m) (succ₁ n) (gcd (succ₁ m) (succ₁ n))
gcd-S≯S-Divisible {m} {n} Nm Nn acc Sm≯Sn c Nc (c∣Sm , c∣Sn) =
    gcd-S≯S-Divisible-ah Nm Nn acc Sm≯Sn c Nc (c∣Sm , c∣Sn)
                         (x∣y→x∣z→x∣y∸z Nc (nsucc Nn) (nsucc Nm) c∣Sn c∣Sm)

------------------------------------------------------------------------------
-- The gcd m n when m > n is Divisible.
gcd-x>y-Divisible :
  ∀ {m n} → N m → N n →
  (∀ {o p} → N o → N p → Lexi o p m n → Divisible o p (gcd o p)) →
  m > n →
  Divisible m n (gcd m n)
gcd-x>y-Divisible nzero Nn _ 0>n _ _ = ⊥-elim (0>x→⊥ Nn 0>n)
gcd-x>y-Divisible (nsucc Nm) nzero _ _ c Nc = gcd-S0-Divisible Nm c Nc
gcd-x>y-Divisible (nsucc {m} Nm) (nsucc {n} Nn) ah Sm>Sn c Nc =
  gcd-S>S-Divisible Nm Nn ih Sm>Sn c Nc
  where
  -- Inductive hypothesis.
  ih : Divisible (succ₁ m ∸ succ₁ n) (succ₁ n) (gcd (succ₁ m ∸ succ₁ n) (succ₁ n))
  ih = ah {succ₁ m ∸ succ₁ n}
          {succ₁ n}
          (∸-N (nsucc Nm) (nsucc Nn))
          (nsucc Nn)
          ([Sx∸Sy,Sy]<[Sx,Sy] Nm Nn)

------------------------------------------------------------------------------
-- The gcd m n when m ≯ n is Divisible.
gcd-x≯y-Divisible :
  ∀ {m n} → N m → N n →
  (∀ {o p} → N o → N p → Lexi o p m n → Divisible o p (gcd o p)) →
  m ≯ n →
  Divisible m n (gcd m n)
gcd-x≯y-Divisible nzero nzero _ _ c Nc = gcd-00-Divisible c Nc
gcd-x≯y-Divisible nzero (nsucc Nn) _ _ c Nc = gcd-0S-Divisible Nn c Nc
gcd-x≯y-Divisible (nsucc _) nzero _ Sm≯0 _ _ = ⊥-elim (S≯0→⊥ Sm≯0)
gcd-x≯y-Divisible (nsucc {m} Nm) (nsucc {n} Nn) ah Sm≯Sn c Nc =
  gcd-S≯S-Divisible Nm Nn ih Sm≯Sn c Nc
  where
  -- Inductive hypothesis.
  ih : Divisible (succ₁ m) (succ₁ n ∸ succ₁ m) (gcd (succ₁ m) (succ₁ n ∸ succ₁ m))
  ih = ah {succ₁ m}
          {succ₁ n ∸ succ₁ m}
          (nsucc Nm)
          (∸-N (nsucc Nn) (nsucc Nm))
          ([Sx,Sy∸Sx]<[Sx,Sy] Nm Nn)

------------------------------------------------------------------------------
-- The gcd is Divisible.
gcdDivisible : ∀ {m n} → N m → N n → Divisible m n (gcd m n)
gcdDivisible = Lexi-wfind A h
  where
  A : D → D → Set
  A i j = Divisible i j (gcd i j)

  h : ∀ {i j} → N i → N j → (∀ {k l} → N k → N l → Lexi k l i j → A k l) →
      A i j
  h Ni Nj ah = case (gcd-x>y-Divisible Ni Nj ah)
                    (gcd-x≯y-Divisible Ni Nj ah)
                    (x>y∨x≯y Ni Nj)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Vecs where

open import Nats

infixr 5 _∷_ _++_ _∷ʳ_
infix 4 _∈_ _⊛_

data Vec {a} (A : Set a) : ℕ → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

data _∈_ {a} {A : Set a} : A → {n : ℕ} → Vec A n → Set a where
  here  : ∀ {n} {x}   {xs : Vec A n} → x ∈ x ∷ xs
  there : ∀ {n} {x y} {xs : Vec A n} (x∈xs : x ∈ xs) → x ∈ y ∷ xs

head : ∀ {a n} {A : Set a} → Vec A (suc n) → A
head (x ∷ xs) = x

tail : ∀ {a n} {A : Set a} → Vec A (suc n) → Vec A n
tail (x ∷ xs) = xs

[_] : ∀ {a} {A : Set a} → A → Vec A 1
[ x ] = x ∷ []

_++_ : ∀ {a m n} {A : Set a} → Vec A m → Vec A n → Vec A (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

_⊛_ : ∀ {a b n} {A : Set a} {B : Set b} →
      Vec (A → B) n → Vec A n → Vec B n
[]       ⊛ _        = []
(f ∷ fs) ⊛ (x ∷ xs) = f x ∷ (fs ⊛ xs)

replicate : ∀ {a n} {A : Set a} → A → Vec A n
replicate {n = zero}  x = []
replicate {n = suc n} x = x ∷ replicate x

_∷ʳ_ : ∀ {a n} {A : Set a} → Vec A n → A → Vec A (suc n)
[]       ∷ʳ y = [ y ]
(x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y)

reverse : ∀ {n m} {A : Set n} → Vec A m → Vec A m
reverse [] = []
reverse (x ∷ xs) = reverse xs ∷ʳ x


text:
{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Cubical.Path where

  open import Agda.Primitive.Cubical using (PathP) public

  infix 4 _≡_

  -- We have a variable name in `(λ i → A)` as a hint for case
  -- splitting.
  _≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
  _≡_ {A = A} = PathP (λ i → A)

  {-# BUILTIN PATH         _≡_     #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --no-universe-polymorphism #-}

open import Data.List
open import Data.Product
open import Data.Unit hiding (_≤_)
open import Data.Nat
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.Core hiding (Total)
import Level as L using (zero)

open import Lists
open import BagEquality
open import Equivalence
open import DivideEtImpera

module Mergesort where

merge : {A : Set} → {_<_ : Rel A L.zero} → Total _<_ → List A → List A → List A
merge _ [] ys = ys
merge _ (x ∷ xs) [] = (x ∷ xs)
merge total (x ∷ xs) (y ∷ ys) with (total x y)
merge total (x ∷ xs) (y ∷ ys) | (inj₁ x≤y) = x ∷ merge total xs (y ∷ ys)
merge total (x ∷ xs) (y ∷ ys) | (inj₂ y≤x) = y ∷ merge total (x ∷ xs) ys

merge-cong : {A : Set} → {_<_ : Rel A L.zero} → (total : Total _<_) → (xs ys : List A) → merge total xs ys ≈ (xs ++ ys)
merge-cong _ [] ys = λ z → z ∈ ys □↔
merge-cong _ (x ∷ xs) [] = λ z → z ∈ (x ∷ xs) ↔⟨ ++-comm [] (x ∷ xs) z ⟩
                                       z ∈ ((x ∷ xs) ++ [])  □↔
merge-cong total (x ∷ xs) (y ∷ ys) with (total x y)
merge-cong total (x ∷ xs) (y ∷ ys) | (inj₁ x≤y) = λ z →
               (z ≡ x) ⊕ z ∈ merge total xs (y ∷ ys)  ↔⟨ ⊕-cong ((z ≡ x) □↔) (merge-cong total xs (y ∷ ys) z) ⟩
               (z ≡ x) ⊕ z ∈ (xs ++ (y ∷ ys)) □↔

merge-cong total (x ∷ xs) (y ∷ ys) | (inj₂ y≤x) = λ z →
               (z ≡ y) ⊕ z ∈ merge total (x ∷ xs) ys  ↔⟨ ⊕-cong ((z ≡ y) □↔) (merge-cong total (x ∷ xs) ys z) ⟩
               (z ≡ y) ⊕ z ∈ ((x ∷ xs) ++ ys)         ↔⟨ ⊕-cong ((z ≡ y) □↔) (++-comm (x ∷ xs) ys z) ⟩
               (z ≡ y) ⊕ z ∈ (ys ++ (x ∷ xs))         ↔⟨ ++-comm (y ∷ ys) (x ∷ xs) z ⟩
               z ∈ ((x ∷ xs) ++ (y ∷ ys)) □↔

SmallerThanHead : {A : Set} → Rel A L.zero → A → List A → Set
SmallerThanHead _ x [] = ⊤
SmallerThanHead _<_ x (y ∷ ys) = _<_ x y

ord : {A : Set} → {_<_ : Rel A L.zero} → {x : A} → {xs : List A} → SmallerThanHead _<_ x xs →  Ordered _<_ xs → Ordered _<_ (x ∷ xs)
ord {xs = []} _ _ = SingleIsOrd
ord {xs = (y ∷ ys)} x≤y ordXs = HeadTailOrd x≤y ordXs

merge-order : {A : Set} → {_<_ : Rel A L.zero} → (total : Total _<_) → (xs ys : List A)
                               → Ordered _<_ xs → Ordered _<_ ys → Ordered _<_ (merge total xs ys)
merge-order _ []        ys _ ysOrd = ysOrd
merge-order _ (x ∷ xs) [] xsOrd _ = xsOrd
merge-order total (x ∷ xs) (y ∷ ys) _ _  with (total x y)
merge-order total (x ∷ xs) (y ∷ ys) _ _     | (inj₁ x≤y) with xs
merge-order total (x ∷ xs) (y ∷ ys) _ ysOrd | (inj₁ x≤y) | [] = HeadTailOrd x≤y ysOrd
merge-order {_<_ = _<_} total (x ∷ xs) (y ∷ ys) (HeadTailOrd x≤x₂ xsOrd)  ysOrd | (inj₁ x≤y) | (x₂ ∷ xs₂)
                      = ord x≤z (merge-order total (x₂ ∷ xs₂) (y ∷ ys) xsOrd ysOrd) where
                             x≤z : SmallerThanHead _<_ x (merge total (x₂ ∷ xs₂) (y ∷ ys))
                             x≤z with (total x₂ y)
                             x≤z | (inj₁ _) = x≤x₂
                             x≤z | (inj₂ _) = x≤y
merge-order total (x ∷ xs) (y ∷ ys) _ _     | (inj₂ y≤x) with ys
merge-order total (x ∷ xs) (y ∷ ys) xsOrd _ | (inj₂ y≤x) | [] = HeadTailOrd y≤x xsOrd
merge-order {_<_ = _<_} total (x ∷ xs) (y ∷ ys) xsOrd (HeadTailOrd y≤y₂ ysOrd) | (inj₂ y≤x) | (y₂ ∷ ys₂)
                      = ord y≤z (merge-order total (x ∷ xs) (y₂ ∷ ys₂) xsOrd ysOrd) where
                               y≤z : SmallerThanHead _<_ y (merge total (x ∷ xs) (y₂ ∷ ys₂))
                               y≤z with (total x y₂)
                               y≤z | (inj₁ _) = y≤x
                               y≤z | (inj₂ _) = y≤y₂

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

minus-suc : {n m : ℕ} → m ≤ n → minus (suc n) m ≡ suc (minus n m)
minus-suc z≤n      = refl
minus-suc (s≤s pf) = minus-suc pf

bisect : {A : Set} → List A → (List A × List A)
bisect xs = splitAt ⌊ length xs /2⌋ xs

splitAtLen1 : {A : Set} →  (n : ℕ) → (xs : List A) → n ≤ (length xs) → length (proj₁ (splitAt n xs)) ≡ n
splitAtLen1 zero xs _ = refl
splitAtLen1 (suc n) [] ()
splitAtLen1 (suc n) (x ∷ xs) (s≤s pf) = suc (length (proj₁ (splitAt n xs))) =⟨ splitAtLen1 n xs pf under suc ⟩
                                        suc n □=

splitAtLen2 : {A : Set} →  (n : ℕ) → (xs : List A) → length (proj₂ (splitAt n xs)) ≡ minus (length xs) n
splitAtLen2 zero xs = refl
splitAtLen2 (suc n) [] = refl
splitAtLen2 (suc n) (x ∷ xs) = length (proj₂ (splitAt n xs)) =⟨ splitAtLen2 n xs ⟩
                                minus (length xs) n □=

s≤′s : {n m : ℕ} → n ≤′ m → suc n ≤′ suc m
s≤′s ≤′-refl      = ≤′-refl
s≤′s (≤′-step pf) = ≤′-step (s≤′s pf)

lte-cong : {n m : ℕ} → (n ≤ m) ⇔ (n ≤′ m)
lte-cong = record { to   = to' ;
                    from = from' } where
                            to' : {n m : ℕ} → n ≤ m → n ≤′ m
                            to' {m = zero}  z≤n = ≤′-refl
                            to' {m = suc m} z≤n = ≤′-step (to' z≤n)
                            to' (s≤s pf) = s≤′s (to' pf)
                            from' : {n m : ℕ} → n ≤′ m → n ≤ m
                            from' {zero} ≤′-refl = z≤n
                            from' {suc n} ≤′-refl = s≤s (from' ≤′-refl)
                            from' (≤′-step pf) = ≤-step (from' pf) where
                                   ≤-step : {n m : ℕ} → n ≤ m → n ≤ (suc m)
                                   ≤-step z≤n = z≤n
                                   ≤-step (s≤s pf) = s≤s (≤-step pf)

eq-rel-cong : {A : Set} → {rel : Rel A L.zero} →  {x y z : A} → x ≡ y → rel y z → rel x z
eq-rel-cong refl pf = pf

halfLte1 : (n : ℕ) → ⌊ n /2⌋ ≤′ n
halfLte1 zero          = ≤′-refl
halfLte1 (suc zero)    = ≤′-step ≤′-refl
halfLte1 (suc (suc n)) = ≤′-step (s≤′s (halfLte1 n))

halfLt1 : (n : ℕ) → ⌊ (suc (suc n)) /2⌋ <′ (suc (suc n))
halfLt1 n = s≤′s (s≤′s (halfLte1 n))

halfLte2 : (n : ℕ) → (minus n ⌊ n /2⌋) ≤′ n
halfLte2 zero          = ≤′-refl
halfLte2 (suc zero)    = ≤′-refl
halfLte2 (suc (suc n)) = ≤′-step (eq-rel-cong {rel = _≤′_} {x = minus (suc n) ⌊ n /2⌋} {y = suc (minus n ⌊ n /2⌋)}
                          (minus-suc (_⇔_.from lte-cong (halfLte1 n))) (s≤′s (halfLte2 n)))

halfLt2 : (n : ℕ) → (minus (suc (suc n)) ⌊ (suc (suc n)) /2⌋) <′ (suc (suc n))
halfLt2 n = s≤′s (eq-rel-cong {rel = _≤′_} {x = minus (suc n) ⌊ n /2⌋} {y = suc (minus n ⌊ n /2⌋)}
                          (minus-suc (_⇔_.from lte-cong (halfLte1 n))) (s≤′s (halfLte2 n)))

bisectPf1 : {A : Set} → (x y : A) → (zs : List A) → proj₁ (bisect (x ∷ y ∷ zs)) <l (x ∷ y ∷ zs)
bisectPf1 x y zs = eq-rel-cong {rel = _<′_}
        (splitAtLen1 ⌊ (suc (suc (length zs))) /2⌋ (x ∷ y ∷ zs) (_⇔_.from lte-cong (halfLte1 (suc (suc (length zs))))))
                   (halfLt1 (length zs))

bisectPf2 : {A : Set} → (x y : A) → (zs : List A) → proj₂ (bisect (x ∷ y ∷ zs)) <l (x ∷ y ∷ zs)
bisectPf2 x y zs = eq-rel-cong {rel = _<′_}
        (splitAtLen2 ⌊ (suc (suc (length zs))) /2⌋ (x ∷ y ∷ zs))
                   (halfLt2 (length zs))

splitAt-cong : {A : Set} → (n : ℕ) → (xs : List A) → proj₁ (splitAt n xs) ++ proj₂ (splitAt n xs) ≈ xs
splitAt-cong zero xs           z = z ∈ xs □↔
splitAt-cong (suc n) []        z = ⊥ □↔
splitAt-cong (suc n) (x ∷ xs) z = (z ≡ x) ⊕ z ∈ (proj₁ (splitAt n xs) ++ proj₂ (splitAt n xs))
                                             ↔⟨ ⊕-cong ((z ≡ x) □↔) (splitAt-cong n xs z) ⟩
                                   (z ≡ x) ⊕ z ∈ xs □↔

ms-inputCond : {A : Set} → List A → Set
ms-inputCond _ = ⊤

ms-decompCond : {A : Set} → List A → (⊤ × List A × List A) → Set
ms-decompCond xs (_ , ys , zs ) = ys ++ zs ≈ xs

ms-compCond : {A : Set} → Rel A L.zero → (⊤ × List A × List A) → List A → Set
ms-compCond rel (_ , xs , ys ) zs = zs ≈ xs ++ ys × (Ordered rel xs → Ordered rel ys → Ordered rel zs)

ms-outputCond : {A : Set} → Rel A L.zero → List A → List A → Set
ms-outputCond rel xs zs = (zs ≈ xs) × Ordered rel zs

ms-G : ⊤ → ⊤ → Σ ⊤ (λ x → ⊤)
ms-G _ _ = (⊤.tt , ⊤.tt)

ms-decomp : {A : Set} → (xs : List A) → ⊤ → ¬ ListPrimitive2 xs → Σ (⊤ × List A × List A)
              (λ z → ⊤ × ⊤ × ⊤ × (proj₁ (proj₂ z) <l xs) × (proj₂ (proj₂ z) <l xs) × ms-decompCond xs z)
ms-decomp [] _ notPrim = ⊥-elim (notPrim NilIsPrim2)
ms-decomp (x ∷ []) _ notPrim = ⊥-elim (notPrim SingleIsPrim2)
ms-decomp (x ∷ y ∷ zs)  _ _ = (⊤.tt , bisect (x ∷ y ∷ zs)) , (⊤.tt , ⊤.tt , ⊤.tt ,
                                                        bisectPf1 x y zs ,
                                                        bisectPf2 x y zs ,
                                                        splitAt-cong ⌊ (suc (suc (length zs))) /2⌋ (x ∷ y ∷ zs))

ms-comp : {A : Set} → {rel : Rel A L.zero} → Total rel → (z : (⊤ × List A × List A)) → Σ (List A) (ms-compCond rel z)
ms-comp total ( _ , xs , ys) = (merge total xs ys) , (merge-cong total xs ys , merge-order total xs ys)

ms-dirSolve : {A : Set} → (rel : Rel A L.zero) → (xs : List A) → ⊤ → ListPrimitive2 xs → Σ (List A) (ms-outputCond rel xs)
ms-dirSolve _ []             _ _    = [] , ((λ z → ⊥ □↔) , NilIsOrd)
ms-dirSolve _ (x ∷ [])      _ _    = (x ∷ []) , ((λ z → z ∈ (x ∷ []) □↔) , SingleIsOrd)
ms-dirSolve _ (x ∷ y ∷ zs) _ prim = ⊥-elim (consConsIsNotPrim2 prim)

ms-lemma : {A : Set} → (rel : Rel A L.zero) → ∀{xs ys₁ ys₂ zs₁ zs₂ ws} → ms-decompCond xs (⊤.tt , ys₁ , ys₂)
                           → ⊤ → ms-outputCond rel ys₁ zs₁ → ms-outputCond rel ys₂ zs₂
                              → ms-compCond rel (⊤.tt , zs₁ , zs₂) ws → ms-outputCond rel xs ws
ms-lemma rel {xs} {ys₁} {ys₂} {zs₁} {zs₂} {ws} ys₁++ys₂≈xs _ ( ys₁≈zs₁ , zs₁Ord ) ( ys₂≈zs₂ , zs₂Ord ) ( ws≈zs₁++zs₂ , compOrd)
                 = (λ z → z ∈ ws              ↔⟨ ws≈zs₁++zs₂ z ⟩
                           z ∈ (zs₁ ++ zs₂)    ↔⟨ Any-++ (z ≡_) zs₁ zs₂ ⟩
                           z ∈ zs₁ ⊕ z ∈ zs₂ ↔⟨ ⊕-cong (ys₁≈zs₁ z) (ys₂≈zs₂ z) ⟩
                           z ∈ ys₁ ⊕ z ∈ ys₂ ↔⟨ ↔sym (Any-++ (z ≡_) ys₁ ys₂) ⟩
                           z ∈ (ys₁ ++ ys₂)    ↔⟨ ys₁++ys₂≈xs z ⟩
                           z ∈ xs □↔) ,
                   compOrd zs₁Ord zs₂Ord

mergesort : {A : Set} → {rel : Rel A L.zero} → Total rel → (xs : List A) → Σ (List A) (λ zs → (zs ≈ xs) × Ordered rel zs)
mergesort {rel = rel} total xs = makeD&C2 <l-wellFounded
                                          prim2Dec
                                          ms-decomp
                                          (ms-comp total)
                                          ms-G
                                          (ms-dirSolve rel)
                                          (ms-lemma rel)
                                          xs ⊤.tt

max_stars_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda

max_issues_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda

max_forks_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda


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

module Categories.Adjoint.Instance.StrictCore where

-- The adjunction between the forgetful functor from (strict) Cats to
-- (strict) Groupoids and the (strict) Core functor.

open import Data.Product
open import Level using (_⊔_)
import Function
open import Relation.Binary using (IsEquivalence)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Categories.Adjoint
open import Categories.Category using (Category)
open import Categories.Category.Groupoid using (Groupoid)
import Categories.Category.Construction.Core as C
open import Categories.Category.Instance.StrictCats
open import Categories.Category.Instance.StrictGroupoids
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Equivalence
open import Categories.Functor.Instance.StrictCore
import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning as MR
open import Categories.Morphism.IsoEquiv using (⌞_⌟; _≃_)

-- The forgetful functor from StrictGroupoids to StrictCats

Forgetful : ∀ {o ℓ e} → Functor (Groupoids o ℓ e) (Cats o ℓ e)
Forgetful {o} {ℓ} {e} = record
  { F₀ = Groupoid.category
  ; F₁ = Function.id
  ; identity     = λ {G} → Groupoids.Equiv.refl {G} {G} {idF}
  ; homomorphism = λ {G H K F H} → Groupoids.Equiv.refl {G} {K} {H ∘F F}
  ; F-resp-≈     = Function.id
  }
  where
    module Groupoids = Category (Groupoids o ℓ e)

-- Core is right-adjoint to the forgetful functor from Groupoids to
-- Cats

CoreAdj : ∀ {o ℓ e} → Forgetful {o} {ℓ ⊔ e} {e} ⊣ Core
CoreAdj = record
  { unit   = record { η = unit   ; commute = λ {G H} F → unit-commute {G} {H} F ; sym-commute = λ {G H} F → unit-sym-commute {G} {H} F }
  ; counit = record { η = counit ; commute = counit-commute                     ; sym-commute = counit-sym-commute }
  ; zig    = λ {G} → zig {G}
  ; zag    = zag
  }
  where
    open Groupoid using (category)
    module Core = Functor Core

    unit : ∀ G → Functor (category G) (C.Core (category G))
    unit G = record
      { F₀ = Function.id
      ; F₁ = λ f → record { from = f ; to = f ⁻¹ ; iso = iso }
      ; identity     = ⌞ Equiv.refl ⌟
      ; homomorphism = ⌞ Equiv.refl ⌟
      ; F-resp-≈     = ⌞_⌟
      }
      where open Groupoid G

    unit-commute : ∀ {G H} (F : Functor (category G) (category H)) →
                   unit H ∘F F ≡F Core.F₁ F ∘F unit G
    unit-commute {_} {H} F = record
      { eq₀ = λ _ → refl
      ; eq₁ = λ _ → ⌞ MR.id-comm-sym (category H) ⌟
      }

    unit-sym-commute : ∀ {G H} (F : Functor (category G) (category H)) →
                       Core.F₁ F ∘F unit G ≡F unit H ∘F F
    unit-sym-commute {_} {H} F = record
      { eq₀ = λ _ → refl
      ; eq₁ = λ _ → ⌞ MR.id-comm-sym (category H) ⌟
      }

    counit : ∀ C → Functor (C.Core C) C
    counit C = record
      { F₀ = Function.id
      ; F₁ = _≅_.from
      ; identity     = Equiv.refl
      ; homomorphism = Equiv.refl
      ; F-resp-≈     = _≃_.from-≈
      }
      where
        open Category C
        open Morphism C

    counit-commute : ∀ {C D} (F : Functor C D) →
                     counit D ∘F Core.F₁ F ≡F F ∘F counit C
    counit-commute {C} {D} F = record
      { eq₀ = λ _ → refl
      ; eq₁ = λ _ → MR.id-comm-sym D
      }

    counit-sym-commute : ∀ {C D} (F : Functor C D) →
                         F ∘F counit C ≡F counit D ∘F Core.F₁ F
    counit-sym-commute {C} {D} F = record
      { eq₀ = λ _ → refl
      ; eq₁ = λ _ → MR.id-comm-sym D
      }

    zig : ∀ {G} → counit (category G) ∘F unit G ≡F idF
    zig {G} = record
      { eq₀ = λ _ → refl
      ; eq₁ = λ _ → MR.id-comm-sym (category G)
      }

    zag : ∀ {B} → Core.F₁ (counit B) ∘F unit (Core.F₀ B) ≡F idF
    zag {B} = record { eq₀ = λ _ → refl ; eq₁ = λ _ → ⌞ MR.id-comm-sym B ⌟ }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
open import Data.Product using ( ∃ ; _×_ ; _,_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
open import Relation.Nullary using ( ¬_ )
open import Relation.Unary using ( _∈_ ; ∅ )
open import Web.Semantic.DL.Signature using ( Signature ; CN ; RN )
open import Web.Semantic.Util using ( Setoid ; Subset ; _∘_ ; False )

module Web.Semantic.DL.TBox.Interp where

{- TBox interpretation of a Signature Σ
   consists essentially of:
     1. A Domain Δ of intepretation
     2. An equivalence relation on Δ
     3. An interpretation of Σ, i.e. a function from CN and RN to Δ
     4. Proofs that the interpretations respect the Equivalence Relation
   One would use records in Agda 2.6.x
 -}
data Interp (Σ : Signature) : Set₁ where
  interp :
    (Δ : Set) → -- The Domain of Interpretation (e.g. representing real objects in the world)
    (_≈_ : Δ → Δ → Set) →     -- an equivalence relation between those objects (one may have hesperus ≈ phosphorus)
    (ref : ∀ {x} → (x ≈ x)) →             -- proof of reflexivity of equivalence relation
    (sym : ∀ {x y} → (x ≈ y) → (y ≈ x)) → -- proof of symmetry of ≈
    (trans : ∀ {x y z} → (x ≈ y) → (y ≈ z) → (x ≈ z)) → -- proof of transitivity
    (con : CN Σ → Subset Δ) →             -- concept names of signature map
    (rol : RN Σ → Subset (Δ × Δ)) →       -- role name of signature map
    (con-≈ : ∀ {x y} c → (x ∈ con c) → (x ≈ y) → (y ∈ con c)) →
    (rol-≈ : ∀ {w x y z} r → (w ≈ x) → ((x , y) ∈ rol r) → (y ≈ z) → ((w , z) ∈ rol r)) →
    Interp Σ

{-
 the functions below return some elements of Interp,
 which would with Agda 2.6.* be given by the record structure
 -}

-- The Domain of Interpretation (e.g. representing real objects in the world)
Δ : ∀ {Σ} → Interp Σ → Set
Δ (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = Δ

-- this semantic entailment relation is unusual as it relates an interpretation to
-- elements in the domain whereas usually we have
-- M ⊨ P where M is a model and P a sentence of the language (as done in Institution Theory)
-- so we might have I ⊨ { a owl:sameAs b }
-- which would be true if a refers to the same object as b in Δ via I
-- this may indicate a confusion of syntax with semantics here.
_⊨_≈_ : ∀ {Σ} → (I : Interp Σ) → (Δ I) → (Δ I) → Set
_⊨_≈_ (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = _≈_

≈-refl : ∀ {Σ} → (I : Interp Σ) → ∀ {x} → (I ⊨ x ≈ x)
≈-refl (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = ref

≈-sym : ∀ {Σ} → (I : Interp Σ) → ∀ {x y} → (I ⊨ x ≈ y) → (I ⊨ y ≈ x)
≈-sym (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = sym

≈-trans : ∀ {Σ} → (I : Interp Σ) → ∀ {x y z} → (I ⊨ x ≈ y) → (I ⊨ y ≈ z) → (I ⊨ x ≈ z)
≈-trans (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = trans

-- concept names of signature map
con : ∀ {Σ} → (I : Interp Σ) → CN Σ → Subset (Δ I)
con (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = con

-- role name of signature map
rol : ∀ {Σ} → (I : Interp Σ) → RN Σ → Subset (Δ I × Δ I)
rol (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = rol

con-≈ : ∀ {Σ} → (I : Interp Σ) → ∀ {x y} c → (x ∈ con I c) → (I ⊨ x ≈ y) → (y ∈ con I c)
con-≈ (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = con-≈

rol-≈ : ∀ {Σ} → (I : Interp Σ) → ∀ {w x y z} r → (I ⊨ w ≈ x) → ((x , y) ∈ rol I r) → (I ⊨ y ≈ z) → ((w , z) ∈ rol I r)
rol-≈ (interp Δ _≈_ ref sym trans con rol con-≈ rol-≈) = rol-≈

{-
 Additional functions
-}

-- Interpretation implies two elements are not equal
_⊨_≉_ : ∀ {Σ} → (I : Interp Σ) → (Δ I) → (Δ I) → Set
I ⊨ x ≉ y = ¬(I ⊨ x ≈ y)

-- the Empty Interpretation
emp : ∀ {Σ} → Interp Σ
emp = interp False (λ ()) (λ {}) (λ {}) (λ {}) (λ c → ∅) (λ r → ∅) (λ {}) (λ {})

-- relf implies ≈
≈-refl′ : ∀ {Σ} (I : Interp Σ) → ∀ {x y} → (x ≡ y) → (I ⊨ x ≈ y)
≈-refl′ I refl = ≈-refl I

max_stars_repo_name: bblfish/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
{-
  This is the readme of the Agda mechanization accompanying our
  POPL 2018 paper:

    "Intrinsically-Typed Interpreters for Imperative Languages"

  The repository is hosted here:
  - https://github.com/metaborg/mj.agda

  A rendered and linked version of this readme can be found here:
  - https://metaborg.github.io/mj.agda/

  This development has been tested against Agda 2.6.1.1 (see CHANGELOG for previous versions).
  If you have this installed, you should simply be able to run
  `make` in the project root. This will checkout the two dependencies in
  `./lib/` first and then build this `./Readme.agda` which serves as the main
  entrypoint to the development.

  Alternatively you can run `make docs` to build the html version of
  the development which is useful if you want to navigate the code
  (starting e.g. in `docs/index.html`) without having an editor setup
  for it. The html docs are syntax-highlighted and you can click
  references to navigate to their definitions.

  There are some minor differences between the Agda code used in the
  paper and this mechanization.  One general (but minor) discrepancy
  is that the definitions in the paper are typed in a manner that is
  not universe polymorphic.  However, the development makes extensive
  use of universe polymorphism, by explicitly quantifying over
  universe levels (e.g., `i` in `{i} → Set i`).

  Other discrepancies are summarized below in this readme.
-}

module Readme where

{-
  * Section 2 *

  We develop a monadic, well-typed interpreter for STLC and interpret
  a few example programs.

  Unlike the interpreter summarized in the paper, the STLC semantics
  in the development makes use of integers and integer operations.
-}
open import STLC.Semantics
open import STLC.Examples

{-
  * Section 3.1 - 3.3 *

  We demonstrate how naively extending the approach to cover
  imperative state is possible, but requires explicit weakening of
  bound values in the interpreter.
-}

open import STLCRef.SemanticsLB

{-
  * Section 3.4 : dependent passing style *

  We can improve the semantics with a form of monadic strength to get
  rid of explicit weakening.
-}
open import STLCRef.Semantics
open import STLCRef.Examples

{-
  * Section 4 until 4.3 *

  We implement the scopes and frames approach in the following small
  Agda library.
-}

open import ScopesFrames.ScopesFrames

{-
  * Section 4.4 *

  We demonstrate the basic usage of this library on an interpreter for
  STLC using scopes and frames.
-}
open import STLCSF.Semantics

{-
  * Section 5 *

  We show how our techniques scale by defining an intrinsically-typed
  interpreter for Middleweight Java (MJ), a language with:

  - Imperative objects
  - Sub-typing
  - Mutable, block-scoped environments
  - Early returns

  The only discrepancy between the code in this development and the
  code shown in the paper is the following:

  - Pattern matching lambdas are not useful for pattern matching
    against.  Instead of using `All` types with pattern matching
    lambdas (Section 5.3 and 5.4), we use tagging predicates in
    `MJSF.Syntax`.

  Then there are some notable differences between the original
  presentation of MJ and our development:

  - Original MJ distinguishes promotable expressions (method
    invocation and object creation) and all other expressions. We
    admit arbitrary expressions to be promoted. This does not change
    the semantics in any significant way. The expressions that we
    allow to be promoted are side-effect free.

  - returns are implemented by modeling non-void methods as having an
    expression as its last statement (technically, this is enforced by
    the type rules of Original MJ; in our development it is
    syntactically enforced).

  - MJ only has equality comparison expressions that can be used as
    conditional expressions.  We allow arbitrary expressions, and use
    if-zero (`ifz`) for conditionals.  This does not correspond to MJ
    or Java, but it would be straightforward to add Booleans and use a
    more conventional `if` statement instead.

  - If-zero statements have ordinary statements as their
    sub-statements.  These can either be block statements or any other
    statement which does not allocate a new frame.  In Original MJ, if
    statements must be blocks.

  - We include integers and integer operations, which are not in
    Original MJ.

  - Our MJ syntax admits fields typed by `void`, which Original MJ
    does not.

  - Our MJ syntax incorporates a dedicated `this` expression for
    referencing the "self" of an object.

-}

open import MJSF.Syntax
open import MJSF.Values
open import MJSF.Monad
open import MJSF.Semantics

{-
  We demonstrate that our interpreter is executable:
-}
open import MJSF.Examples.Integer
open import MJSF.Examples.DynamicDispatch

{-
  * Appendix A *

  The following code artifacts *are not* described in the paper, but
  are used as a comparison point to evaluate the impact on the
  interpreter of using the scopes and frames model of binding.

  This is an intrinsically-typed interpreter for MJ without the use of
  scope-and-frames. Instead it describes a language-*dependent*
  classtable construction to deal with object dot-access binding and
  typing contexts and environments to deal with lexical binding
  respectively.
-}
open import MJ.Syntax.Typed

-- lexical contexts
open import MJ.LexicalScope

-- class table
open import MJ.Classtable.Core
open import MJ.Classtable.Membership
open import MJ.Classtable.Code

-- semantics
open import MJ.Semantics.Values
open import MJ.Semantics.Environments
open import MJ.Semantics.Objects
open import MJ.Semantics.Objects.Flat
open import MJ.Semantics.Monadic

-- examples
open import MJ.Examples.Integer
open import MJ.Examples.Exceptions
open import MJ.Examples.While
open import MJ.Examples.DynDispatch

{-
  * Appendix B *

  Additionally we demonstrate briefly how Agda's typeclass mechanism
  is not sufficiently strong to infer store extension facts for
  weakening. (Notably Idris rejects an equivalent program as well
  because the two instances are overlapping)
-}
open import Experiments.Infer

{-
  * Appendix C *

  Our interpreters make use of the operator `_^_` operator, defined
  as:

  (1) `_^_ : ∀ {Σ Γ}{p q : List Type → Set} ⦃ w : Weakenable q ⦄ →
             M Γ p Σ → q Σ → M Γ (p ⊗ q) Σ`

  This operator is strikingly similar to the strength operator that is
  characteristic of strong monads:

  (2)  `_^_ : ∀ {p q} → M p → q → M (p ⊗ q)`

  Here, `p` and `q` are objects in a category ℂ, and M is a monad for
  ℂ.

  In the following development we show how to define a monad that is
  morally equivalent to ours.  The monad in the development below is
  defined over the category of monotone predicates.  In this category,
  the store-passing monad is a strong monad, with the usual notion of
  monadic strength, i.e., (2) above.

  We also show how, in this category, we can write an interpreter
  without explicit weakening, by writing the interpreter in a
  point-free style.
-}

open import Experiments.Category
open import Experiments.StrongMonad
open import Experiments.STLCRefPointfree

{-
  We briefly outline how these experiments relate to our paper.

  The interpreters in our paper are defined in terms of ordinary Agda
  functions and indexed types.  Agda functions and indexed types are
  not guaranteed to be weakenable, and Agda does not have built-in
  support for automatically weakening types across monadic binds.  In
  our paper, we address the weakening problem by making explicit use
  in our interpreters of the `_^_` operator, which is morally
  equivalent to the monadic strength operator for monotone predicates
  over store types, defined in the categorical development above.  Our
  `_^_` operator explicitly requires `q` to be weakenable, which is a
  fairly minimal requirement for convincing Agda's type checker that
  carrying types over monadic binds is safe.

  The categorical model enjoys a cleaner treatment of weakening, but
  it is more cumbersome to write interpreters in Agda using this
  model, because of the additional level of encoding imposed by
  constructing and working with objects and morphisms in a category,
  as encoded in Agda.  However, we imagine that the categorical
  development is a good target model for a future specification
  language for dynamic semantics.
-}


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

{- Here, we derive our main theorem: there is a type in the n-th universe
   that is not an n-type, implying the n-th universe is not n-truncated.
   The n-th universe restricted to n-types is hence a 'strict' n-type.
   For this, we first derive local-global looping in a modular way.

   A technical point worth noting is that Agda does not implement
   cumulative universes. Since that means the crucial steps in our
   transformations (where we pass between universes uning univalence)
   can not be expressed using equality without resorting to explicit lifting,
   we decide to explicitely uses equivalences (and pointed equivalences,
   respectively) instead where possible.
   As a drawback, we have to use lemmata showing preservation of
   (pointed) equivalences of various (pointed) type constructions,
   a parametricity property derived for free
   from univalence-induced equalities. -}
module Universe.Hierarchy where

open import lib.Basics
open import lib.Equivalences2
open import lib.NType2
open import lib.types.Bool
open import lib.types.Nat hiding (_+_)
open import lib.types.Paths
open import lib.types.Sigma
open import lib.types.TLevel

open import Universe.Utility.General
open import Universe.Utility.Pointed
open import Universe.Utility.TruncUniverse

-- *** Lemma 5.2 ***
{- Our Local-global looping principle.
   We would like to state this principle in the form of
     Ωⁿ⁺¹ (Type i , A) == ∀• a → Ωⁿ (A , a)
   for n ≥ 1. Unfortunately, the two sides have different universe
   levels since (Type i , A) lives in Type• (suc i) instead of Type• i.
   Morally, this is outbalanced by the extra Ω on the left-hand side,
   which might help explain on an intuitive level why
   the n-th universe ends up being not an n-type.

   The reason why the univalence principle (A ≡ B) ≃ (A ≃ B)
   cannot be written as (A ≡ B) ≡ (A ≃ B) is precisely the same. -}
module _ {i} {A : Type i} where
  -- The degenerate pre-base case carries around a propositional component.
  Ω-Type : Ω (Type i , A) ≃• Σ• (Π• (A , λ a → (A , a))
                               , (is-equiv , idf-is-equiv _))
  Ω-Type =
      Ω (Type i , A)
    ≃•⟨ ide• _ ⟩
      (A == A , idp)
    ≃•⟨ ua-equiv• ⁻¹• ⟩
      (A ≃ A , ide _)
    ≃•⟨ ide• _ ⟩
      ((Σ (A → A) is-equiv) , (idf _ , idf-is-equiv _))
    ≃•⟨ ide• _ ⟩
      Σ• (Π• (A , λ a → (A , a)) , (is-equiv , idf-is-equiv _))
    ≃•∎

  -- The base case.
  Ω²-Type : (Ω ^ 2) (Type i , A) ≃• Π• (A , λ a → Ω (A , a))
  Ω²-Type =
      (Ω ^ 2) (Type i , A)
    ≃•⟨ equiv-Ω Ω-Type ⟩
      Ω (Σ• (Π• (A , λ a → (A , a)) , (is-equiv , idf-is-equiv _)))
    ≃•⟨ forget-Ω^-Σ•₂ {i} _ 1 (is-equiv-is-prop ∘ _) ⟩
      Ω (Π• (A , λ a → (A , a)))
    ≃•⟨ Ω-Π•-comm _ ⟩
      Π• (A , λ a → Ω (A , a))
    ≃•∎

  -- The general case follows by permuting Ω and Π• repeatedly.
  Ω^-Type : (n : ℕ) → (Ω ^ (n + 2)) (Type i , A)
                   ≃• Π• (A , λ a → (Ω ^ (n + 1)) (A , a))
  Ω^-Type n = Ω^-Π•-comm _ _ n ∘e• equiv-Ω^ n Ω²-Type

{- The pointed family P from the article.
   It takes an n-type A and returns the space of (n+1)-loops
   with basepoint A in U_n^n (the n-th universe restricted to n-types).
   This crucial restriction to n-types implies it is just a set. -}
module _ (n : ℕ) (A : ⟨ n ⟩ -Type ｢ n ｣) where
  -- *** Definition of P and Corollary 5.6 ***
  P : ⟨0⟩ -Type• ｢ n + 1 ｣
  P = Ω^-≤' (n + 1) q where
    q : ⟨ n + 1 ⟩ -Type• ｢ n + 1 ｣
    q = –> Σ-comm-snd ((⟨ n ⟩ -Type-≤ ｢ n ｣ , A))

  -- Forgetting about the truncation level, we may present P as follows:
  Q : Type• ｢ n + 1 ｣
  Q = (Ω ^ (n + 1)) (Type ｢ n ｣ , fst A)

  P-is-Q : fst P ≃• Q
  P-is-Q = equiv-Ω^ n (forget-Ω^-Σ•₂ _ 1 (λ _ → has-level-is-prop))

-- *** Definition of Loop and Lemma 5.7 ***
{- The type Loop of (images of) n-loops in U_(n-1)^(n-1) is
   just the dependent sum over P except for the special case n ≡ 0,
   where we take U_(-1)^(-1) (and hence Loop) to be the booleans.

   The boilerplate with raise-≤T is just to verify Loop n is n-truncated.
   The bulk of the rest of this module consists of showing
   the n-th universe is not n-truncated at basepoint Loop n,
   i.e. that Q n (Loop n) is not contractible.

   Warning: The indexing of Loop starts at -1 in the article,
            but we use natural numbers here (starting at 0),
            thus everything is shifted by one. -}
Loop : (n : ℕ) → ⟨ n ⟩ -Type ｢ n ｣
Loop 0     = (Bool , Bool-is-set)
Loop (S n) = Σ-≤ (⟨ n ⟩ -Type-≤ ｢ n ｣) (λ A →
               raise-≤T {n = ⟨ n + 1 ⟩} (≤T-+2+-l ⟨0⟩ (-2≤T _))
                                        (fst (<– Σ-comm-snd (P n A))))

-- *** Section 2: the base case ***
-- The base case is as usual (there is a non-trivial automorphism on booleans).
base-case : ¬ (is-contr• (Q 0 (Loop 0)))
base-case c = Bool-false≠true false-is-true where
  -- Negation.
  ~ : Bool → Bool
  ~ = λ {true → false; false → true}

  -- Negation is an equivalence.
  e : Bool ≃ Bool
  e = equiv ~ ~ inv inv where
    inv = λ {true → idp; false → idp}

  -- Negation being equal to the identity yields a contradiction.
  false-is-true =
    false             =⟨ ! (coe-β e true) ⟩
    coe (ua e) true   =⟨ ap (λ p → coe p true) (! (c (ua e))) ⟩
    coe idp true      =⟨ idp ⟩
    true              ∎

-- Let us now turn towards the successor case.
module _ (m : ℕ) where

  -- We expand the type we are later going to assume contractible.
  Q-L-is-… =
      Q (m + 1) (Loop (m + 1))
    ≃•⟨ ide• _ ⟩
      (Ω ^ (m + 2)) (_ , ⟦ Loop (m + 1) ⟧)
    ≃•⟨ (Ω^-Type m) ⟩
      Π• (_ , λ {(A , q) → Ω ^ (m + 1) $ (⟦ Loop (m + 1) ⟧ , (A , q))})
    ≃•⟨ ide• _ ⟩
      Π• (_ , λ {(A , q) → Ω ^ (m + 1) $ Σ• ((_ , A) , (base ∘ fst ∘ P m , q))})
    ≃•∎

  -- What we really want is to arrive at contractibility of E (m ≥ 1)...
  E = Π• (⟦ Loop (m + 1) ⟧ , λ {(A , q) → Ω ^ (m + 1) $ (⟨ m ⟩ -Type ｢ m ｣ , A)})

  -- ...or at least show that the following element f of E is trivial (m ≡ 0).
  f : base E
  f (_ , q) = q

{- We want to use our assumption of contractibility of Q (n + 1) (Loop (n + 1))
   to show that f is trivial, i.e. constant with value the basepoint. -}
f-is-trivial : (m : ℕ) → is-contr• (Q (m + 1) (Loop (m + 1))) → f m == pt (E m)

-- m ≡ 0
f-is-trivial 0 c = ap (λ f' → fst ∘ f')
                      (! (–> (equiv-is-contr• …-is-E') c f')) where
  {- This is almost E, except for the additional component
      specifying that the first component p should commute with q. -}
  E' = Π• (_ , λ {(A , q) → (Σ (A == A) (λ p → q == q [ (λ x → x == x) ↓ p ])
                                       , (idp , idp))})

  -- This "almost" E comes from Q 1 (Loop 1), hence can be shown contractible.
  …-is-E' : Q 1 (Loop 1) ≃• E'
  …-is-E' = equiv-Π• (ide _ , Ω-Σ•-comm ∘ _) ∘e• Q-L-is-… 0

  {- Fortunately, f can be 'extended' to an element f' of E',
     and triviality of f' implies triviality of f. -}
  f' = λ {(_ , q) → (q , ↓-idf=idf-in (∙=∙' q q))}

{- m ≥ 1: We can show Q (k + 2) (Loop (k + 2)) ≃ E (k + 1),
          thus E is contractible, hence f trivial. -}
f-is-trivial (S k) c = ! (–> (equiv-is-contr• (…-is-E ∘e• Q-L-is-… (k + 1)))
                             c
                             (f (k + 1))) where
  …-is-E : _ ≃• E (k + 1)
  …-is-E = equiv-Π• (ide _ , equiv-Ω^ k ∘ (λ {(A , q) → forget-Ω^-Σ•₂
             {｢ k + 2 ｣} (base ∘ fst ∘ P (k + 1) , q) 2
             (snd ∘ P (k + 1))}))

-- *** Lemma 5.8, part one ***
-- Our main lemma: like in the article, but in negative form.
main : (n : ℕ) → ¬ (is-contr• (Q n (Loop n)))
main 0       = base-case
main (S m) c = main m step where
  {- We know Q (m + 1) (Loop (m + 1)) is contractible,
     use that to show that the above f is trivial,
     deduce f (Loop m , p) ≡ p is trivial for all p in P m (Loop m),
     which implies P m (Loop m) is contractible.
     But this is just another form of Q m (Loop m),
     so the conclusion follows by induction hypothesis. -}
  step : is-contr• (Q m (Loop m))
  step = –> (equiv-is-contr• (P-is-Q m (Loop m)))
            (λ q → app= (! (f-is-trivial m c)) (Loop m , q))

-- *** Lemma 5.8, part two ***
-- Alternate form of the main lemma
main' : (n : ℕ) → ¬ (is-contr• ((Ω ^ (n + 1)) (⟨ n ⟩ -Type ｢ n ｣ , Loop n )))
main' n = main n ∘ –> (equiv-is-contr• (P-is-Q n (Loop n)))

-- Small helper thingy
helpy : ∀ {i} {n : ℕ} {X : Type• i}
        → has-level• (n -1) X → is-contr• ((Ω ^ n) X)
helpy {n = n} {X} = <– contr•-equiv-prop
                  ∘ trunc-many n
                  ∘ transport (λ k → has-level• (k -2) X)
                              (+-comm 1 n)

-- Main theorems now fall out as corollaries.
module _ (n : ℕ) where
  {- Recall that L n is n-truncated.
     We also know it is not (n-1)-truncated, it is thus a 'strict' n-type. -}
  Loop-is-not-trunc : ¬ (has-level (n -1) ⟦ Loop n ⟧)
  Loop-is-not-trunc = main n ∘ helpy ∘ (λ t → universe-=-level t t)

  -- *** Theorem 5.9 ***
  -- The n-th universe is not n-truncated.
  Type-is-not-trunc : ¬ (has-level ⟨ n ⟩ (Type ｢ n ｣))
  Type-is-not-trunc = main n ∘ helpy

  -- *** Theorem 5.11 ***
  {- MAIN RESULT:
     The n-th universe restricted to n-types is a 'strict' (n+1)-type. -}
  Type-≤-is-not-trunc : ¬ (has-level ⟨ n ⟩ (⟨ n ⟩ -Type ｢ n ｣))
  Type-≤-is-not-trunc = main' n ∘ helpy

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
-- Andreas, 2015-07-20, record patterns

open import Common.Product
open import Common.Prelude
open import Common.Equality

swap : {A B : Set} (p : A × B) → B × A
swap record{ proj₁ = a; proj₂ = b } = record{ proj₁ = b; proj₂ = a }

fst : {A : Set}{B : A → Set} (p : Σ A B) → A
fst record{ proj₁ = a } = a

snd : {A : Set}{B : A → Set} (p : Σ A B) → B (fst p)
snd record{ proj₂ = b } = b

module _ (A : Set) (B : A → Set) (C : (a : A) → B a → Set) where

  Tr = Σ A (λ a → Σ (B a) (C a))

  fst3 : Tr → A
  fst3 record{ proj₁ = a } = a

  snd3 : (t : Tr) → B (fst3 t)
  snd3 record{ proj₂ = record { proj₁ = b }} = b

  thd3 : (t : Tr) → C (fst3 t) (snd3 t)
  thd3 record{ proj₂ = record { proj₂ = c }} = c

  thd32 : (t u : Tr) → C (fst3 t) (snd3 t)
  thd32 record{ proj₂ = record { proj₂ = c }}
        record{ proj₂ = record { proj₂ = _ }} = c

postulate A : Set

record R : Set where
  field f : A

T : Bool → Set
T true  = R
T false = A

-- Postponed record pattern
test : ∀{b} → T b → b ≡ true → A
test record{f = a} refl = a


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

open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; subst; cong; trans)
open import Relation.Nullary.Decidable using (toWitness; fromWitness)
open import Relation.Nullary using (yes; no)
open import Function.Reasoning
open import Function using (_∘_)

import Data.Empty as Empty
import Data.Product as Product
import Data.Product.Properties as Productₚ
import Data.Unit as Unit
import Data.Nat.Base as Nat
import Data.Vec.Base as Vec
import Data.Vec.Properties as Vecₚ
import Data.Fin.Base as Fin
import Data.Fin.Properties as Finₚ
import Data.Vec.Relation.Unary.All as All

open Empty using (⊥-elim)
open Unit using (tt)
open Nat using (ℕ; zero; suc)
open Vec using (Vec; []; _∷_)
open All using (All; []; _∷_)
open Fin using (Fin ; zero ; suc)
open Product using (Σ-syntax; ∃-syntax; _×_; _,_; proj₁; proj₂)

import PiCalculus.Syntax
open PiCalculus.Syntax.Scoped
open import PiCalculus.Semantics
open import PiCalculus.Semantics.Properties
open import PiCalculus.LinearTypeSystem.Algebras

module PiCalculus.LinearTypeSystem.Substitution (Ω : Algebras) where
open Algebras Ω
open import PiCalculus.LinearTypeSystem Ω
open import PiCalculus.LinearTypeSystem.ContextLemmas Ω
open import PiCalculus.LinearTypeSystem.Framing Ω

private
  variable
    n : ℕ
    i j : Fin n
    t t' : Type
    γ : PreCtx n
    idx idx' : Idx
    idxs : Idxs n
    x y z m m' l δ : Usage idx ²
    Γ Γₗ Γᵣ Ξₗ Ξᵣ Δ Δ' Ξ' Θ Ψ Ξ Ψ' Θ' Δₗ Δᵣ Β : Ctx idxs
    P : Scoped n

midpoint : {Γᵢ Γ Δ Ψ ΔP Ξᵢ ΔQ Ψᵢ : Ctx idxs} {m n : Usage idx ²}
         → Γᵢ ∋[ i ] m ▹ Γ
         → Γ ≔ Δ ⊗ Ψ
         → All.lookup i Δ ≡ ℓ∅
         → Γᵢ ≔ ΔP ⊗ Ξᵢ
         → Ξᵢ ≔ ΔQ ⊗ Ψᵢ
         → Ψᵢ ∋[ i ] n ▹ Ψ
         → Σ[ δ ∈ Usage idx ² ]
           Σ[ Θ ∈ Ctx idxs ]
           Σ[ Δ₁ ∈ Ctx idxs ]
           Σ[ Δ₂ ∈ Ctx idxs ] (
           Ξᵢ ∋[ i ] δ ▹ Θ
         × Γ ≔ Δ₁ ⊗ Θ
         × Θ ≔ Δ₂ ⊗ Ψ)

midpoint {i = zero} (zero γᵢ≔m∙γ) (Γ≔Δ∙Ψ , γ≔δ∙ψ) refl (Γᵢ≔ΔP∙Ξᵢ , γᵢ≔δp∙ξᵢ) (Ξᵢ≔ΔQ∙Ψᵢ , ξᵢ≔δq∙ψᵢ) (zero ψᵢ≔n∙ψ)
  rewrite ∙²-unique γ≔δ∙ψ ∙²-idˡ =
  let _ , ξᵢ≔δ∙θ , _ = ∙²-assoc⁻¹ ξᵢ≔δq∙ψᵢ ψᵢ≔n∙ψ in
  _ , _ , (_ -, _) , _ , zero ξᵢ≔δ∙θ , (Γᵢ≔ΔP∙Ξᵢ , ∙²-idˡ) , (Ξᵢ≔ΔQ∙Ψᵢ , ∙²-idˡ)
midpoint {i = suc i} (suc Γᵢ≔m∙Γ) (Γ≔Δ∙Ψ , _) Δ[i]≡ℓ∅ (Γᵢ≔ΔP∙Ξᵢ , γᵢ≔δp∙ξᵢ) (Ξᵢ≔ΔQ∙Ψᵢ , ξᵢ≔δq∙ψᵢ) (suc ψᵢ≔n∙ψ) =
  let _ , _ , _ , _ , Ξᵢ≔δ∙Θ , Γ≔Δ₁∙Θ , Θ≔Δ₂∙Ψ = midpoint Γᵢ≔m∙Γ Γ≔Δ∙Ψ Δ[i]≡ℓ∅ Γᵢ≔ΔP∙Ξᵢ Ξᵢ≔ΔQ∙Ψᵢ ψᵢ≔n∙ψ in
  _ , _ , (_ -, _) , _ , suc Ξᵢ≔δ∙Θ , (Γ≔Δ₁∙Θ , γᵢ≔δp∙ξᵢ) , (Θ≔Δ₂∙Ψ , ξᵢ≔δq∙ψᵢ)

cutpoint : {Γ Δ Θ Γⱼ : Ctx idxs} {m n l : Usage idx ²}
       → Γ ≔ Δ ⊗ Θ
       → Γⱼ ∋[ j ] m ▹ Γ
       → m ≔ n ∙² l
       → Σ[ Θⱼ ∈ Ctx idxs ] (Θⱼ ∋[ j ] l ▹ Θ)
cutpoint (_ , γ≔) (zero x) m≔ =
  let
    _ , _ , a = ∙²-assoc x m≔
    _ , _ , c = ∙²-assoc (∙²-comm a) γ≔
  in _ , zero (∙²-comm c)
cutpoint (Γ≔ , _) (suc ∋j) m≔ with cutpoint Γ≔ ∋j m≔
cutpoint (Γ≔ , _) (suc ∋j) m≔ | _ , r = _ , suc r

∋-subst : {Γ Γᵢ Γⱼ Δ Ψ Ψᵢ Ψⱼ Ξᵢ CONT : Ctx idxs} {i j x : Fin n} {mx : Usage idx' ²} {m n : Usage idx ²}
        → Vec.lookup γ i ≡ Vec.lookup γ j
        → Γᵢ ∋[ i ] m ▹ Γ
        → Γⱼ ∋[ j ] m ▹ Γ
        → Ψᵢ ∋[ i ] n ▹ Ψ
        → Ψⱼ ∋[ j ] n ▹ Ψ
        → Γ ≔ Δ ⊗ Ψ
        → All.lookup i Δ ≡ ℓ∅
        → γ ； Γᵢ ∋[ x ] t ； mx ▹ Ξᵢ
        → Ξᵢ ≔ CONT ⊗ Ψᵢ
        → Σ[ Ξⱼ ∈ Ctx idxs ]
          Σ[ Θ ∈ Ctx idxs ]
          Σ[ Δ' ∈ Ctx idxs ]
          Σ[ m' ∈ Usage idx ² ]
         (γ ； Γⱼ ∋[ x [ i ↦ j ]' ] t ； mx ▹ Ξⱼ
        × Ξᵢ ∋[ i ] m' ▹ Θ
        × Ξⱼ ∋[ j ] m' ▹ Θ
        × Θ ≔ Δ' ⊗ Ψ
        × All.lookup i Δ' ≡ ℓ∅)
∋-subst {i = i} {x = x} eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ (∋t , ∋x) Ξᵢ≔CONT∙Ψᵢ with i Finₚ.≟ x
∋-subst {i = i} {x = x} eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ (∋t , ∋x) Ξᵢ≔CONT∙Ψᵢ | yes refl with ∋-≡Idx ∋i | ∋-≡Idx ∋x
∋-subst {i = i} {x = x} eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ (∋t , ∋x) Ξᵢ≔CONT∙Ψᵢ | yes refl | refl | refl =
  let
    _ , Ξᵢ≔CONTn∙Ψ , _ = ⊗-assoc⁻¹ Ξᵢ≔CONT∙Ψᵢ (proj₁ (proj₂ (∋-⊗ ∈i)))
    δ , m≔ℓ∙δ = boil ∋i ∋x Ξᵢ≔CONTn∙Ψ Γ≔Δ∙Ψ Δ∋iℓ∅
    _ , Γᵢ≔ℓ∙⁇ᵢ , ⁇ᵢ≔δ∙Γ = split m≔ℓ∙δ ∋i
    _ , Γⱼ≔ℓ∙⁇ⱼ , ⁇ⱼ≔δ∙Γ = split m≔ℓ∙δ ∋j
    ⁇ᵢ≡Ξᵢ = ∋-uniqueʳ Γᵢ≔ℓ∙⁇ᵢ ∋x
    Ξᵢ≔δ∙Γ = subst (λ ● → ● ∋[ _ ] δ ▹ _) ⁇ᵢ≡Ξᵢ ⁇ᵢ≔δ∙Γ
  in _ , _ , _ , _ , (≡Type-∋ (trans (sym eq) (∋-≡Type ∋t)) , Γⱼ≔ℓ∙⁇ⱼ) , Ξᵢ≔δ∙Γ , ⁇ⱼ≔δ∙Γ , Γ≔Δ∙Ψ , Δ∋iℓ∅

∋-subst {i = i} {x = x} eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ (∋t , ∋x) Ξᵢ≔CONT∙Ψᵢ | no i≢x =
  let
    _ , Ξᵢ≔m∙Θ , Γ≔ℓ∙Θ = diamond i≢x ∋x ∋i
    _ , Γⱼ≔m'∙Γ , m'≔m∙ε = ∋-⊗ ∋j
    _ , Γ≔ℓ'∙Θ ,  ℓ'≔ℓ∙ε = ∋-⊗ Γ≔ℓ∙Θ
    _ , Γⱼ≔ℓ'∙Ξⱼ , Ξⱼ≔m'∙Θ = reverse Γⱼ≔m'∙Γ Γ≔ℓ'∙Θ
    _ , Γᵢ≔ℓCONT∙Ψᵢ , _ = ⊗-assoc⁻¹ (proj₁ (proj₂ (∋-⊗ ∋x))) Ξᵢ≔CONT∙Ψᵢ
    _ , Ξᵢ≔CONTn∙Ψ , _ = ⊗-assoc⁻¹ Ξᵢ≔CONT∙Ψᵢ (proj₁ (proj₂ (∋-⊗ ∈i)))
    _ , Θ≔Δ'∙Ψ = outer-diamond i≢x ∋i ∋x Γ≔ℓ∙Θ Ξᵢ≔m∙Θ Γ≔Δ∙Ψ Ξᵢ≔CONTn∙Ψ
    _ , Δ'∋iℓ∅ = split-ℓ∅ Γ≔Δ∙Ψ (proj₁ (proj₂ (∋-⊗ Γ≔ℓ∙Θ))) Θ≔Δ'∙Ψ Δ∋iℓ∅
  in _ , _ , _ , _ , (∋t , ⊗-∋ Γⱼ≔ℓ'∙Ξⱼ ℓ'≔ℓ∙ε) , Ξᵢ≔m∙Θ , ⊗-∋ Ξⱼ≔m'∙Θ m'≔m∙ε , Θ≔Δ'∙Ψ , Δ'∋iℓ∅

⊢-subst-ih : ∀ {γ : PreCtx n} {idxs : Idxs n} {Γ Γᵢ Γⱼ Δ Ψ Ψᵢ Ψⱼ : Ctx idxs} {i j : Fin n} {m n : Usage idx ²}
           → Vec.lookup γ i ≡ Vec.lookup γ j
           → Γᵢ ∋[ i ] m ▹ Γ
           → Γⱼ ∋[ j ] m ▹ Γ
           → Ψᵢ ∋[ i ] n ▹ Ψ
           → Ψⱼ ∋[ j ] n ▹ Ψ
           → Γ ≔ Δ ⊗ Ψ
           → All.lookup i Δ ≡ ℓ∅
           → γ ； Γᵢ ⊢ P ▹ Ψᵢ
           → γ ； Γⱼ ⊢ P [ i ↦ j ] ▹ Ψⱼ

⊢-subst-ih {i = i} eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ 𝟘 with ⊗-get i Γ≔Δ∙Ψ | ∋-≡Idx ∈i | ∋-≡Idx ∋i
⊢-subst-ih {i = i} eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ 𝟘 | Γi≔Δi∙Ψi | refl | refl with ∋-lookup-≡ ∈i | ∋-lookup-≡ ∋i
⊢-subst-ih {i = i} eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ 𝟘 | Γi≔Δi∙Ψi | refl | refl | qeq | qe
  rewrite Δ∋iℓ∅ | ∙²-unique Γi≔Δi∙Ψi ∙²-idˡ | ∙²-uniqueˡ qe qeq | ∋-uniqueʳ ∋i ∈i | ∋-uniqueˡ ∋j ∈j = 𝟘
⊢-subst-ih eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ (ν t m μ ⊢P) =
  ν t m μ (⊢-subst-ih eq (suc ∋i) (suc ∋j) (suc ∈i) (suc ∈j) (Γ≔Δ∙Ψ , ∙²-idʳ) Δ∋iℓ∅ ⊢P)
⊢-subst-ih eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ (∋x ⦅⦆ ⊢P) with ⊢-⊗ ⊢P
⊢-subst-ih eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ (∋x ⦅⦆ ⊢P) | (_ -, _) , (Ξᵢ≔δ⊢P∙Ψᵢ , _) =
  let _ , _ , _ , _ , ∋x' , ∋i' , ∋j' , Θ≔Δ'∙Ψ , Δ'∋iℓ∅ = ∋-subst eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ ∋x Ξᵢ≔δ⊢P∙Ψᵢ in
  ∋x' ⦅⦆ ⊢-subst-ih eq (suc ∋i') (suc ∋j') (suc ∈i) (suc ∈j) (Θ≔Δ'∙Ψ , ∙²-idʳ) Δ'∋iℓ∅ ⊢P
⊢-subst-ih eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ ((∋tx , ∋x) ⟨ ∋ty , ∋y ⟩ ⊢P) =
  let
    _ , δ⊢P = ⊢-⊗ ⊢P
    _ , δy , _ = ∋-⊗ ∋y
    _ , δy⊢P , _ = ⊗-assoc⁻¹ δy δ⊢P
    _ , _ , _ , _ , ∋x' , ∋i' , ∋j' , Θ≔Δ'∙Ψ , Δ'∋iℓ∅ = ∋-subst eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ (∋tx , ∋x) δy⊢P
    _ , _ , _ , _ , ∋y' , ∋i'' , ∋j'' , Θ≔Δ''∙Ψ , Δ''∋iℓ∅ = ∋-subst eq ∋i' ∋j' ∈i ∈j Θ≔Δ'∙Ψ Δ'∋iℓ∅ (∋ty , ∋y) δ⊢P
  in ∋x' ⟨ ∋y' ⟩ ⊢-subst-ih eq ∋i'' ∋j'' ∈i ∈j Θ≔Δ''∙Ψ Δ''∋iℓ∅ ⊢P
⊢-subst-ih eq ∋i ∋j ∈i ∈j Γ≔Δ∙Ψ Δ∋iℓ∅ (_∥_ {Δ = Ξᵢ} ⊢P ⊢Q) =
  let
    _ , Γᵢ≔δ⊢P∙Ξᵢ = ⊢-⊗ ⊢P
    _ , Ξᵢ≔δ⊢Q∙Ψᵢ = ⊢-⊗ ⊢Q
    _ , _ , _ , _ , Ξᵢ≔δ∙Θ , Γ≔Δ₁∙Θ , Θ≔Δ₂∙Ψ = midpoint ∋i Γ≔Δ∙Ψ Δ∋iℓ∅ Γᵢ≔δ⊢P∙Ξᵢ Ξᵢ≔δ⊢Q∙Ψᵢ ∈i
    _ , Ξᵢ≔δ'∙Θ , δ'≔δ∙ε = ∋-⊗ Ξᵢ≔δ∙Θ
    _ , Γᵢ≔δ'∙⁇ᵢ , ⁇ᵢ≔δ⊢P∙Θ = reverse Γᵢ≔δ⊢P∙Ξᵢ Ξᵢ≔δ'∙Θ
    Δ₁∋iℓ∅ , Δ₂∋iℓ∅ = split-ℓ∅ Γ≔Δ∙Ψ Γ≔Δ₁∙Θ Θ≔Δ₂∙Ψ Δ∋iℓ∅
    _ , m≔δ∙δ⊢P = boil ∋i (⊗-∋ Γᵢ≔δ'∙⁇ᵢ δ'≔δ∙ε) ⁇ᵢ≔δ⊢P∙Θ Γ≔Δ₁∙Θ Δ₁∋iℓ∅
    _ , Ξⱼ≔δ∙Θ = cutpoint Γ≔Δ₁∙Θ ∋j (∙²-comm m≔δ∙δ⊢P)
  in ⊢-subst-ih eq ∋i ∋j Ξᵢ≔δ∙Θ Ξⱼ≔δ∙Θ Γ≔Δ₁∙Θ Δ₁∋iℓ∅ ⊢P ∥ ⊢-subst-ih eq Ξᵢ≔δ∙Θ Ξⱼ≔δ∙Θ ∈i ∈j Θ≔Δ₂∙Ψ Δ₂∋iℓ∅ ⊢Q

switch : ∀ {γ : PreCtx n} {idxs : Idxs n} {Γ Ξ Ψ : Ctx idxs} {t  idx}  {m : Usage idx ²}
       → γ -, t ； Γ -, m ⊢ P ▹ Ψ -, ℓ∅
       → Ψ ∋[ j ] m ▹ Ξ
       → ∃[ Θ ] (Γ      ∋[ j ] m ▹ Θ
      × γ -, t ； Θ -, m ⊢ P      ▹ Ξ -, ℓ∅)
switch ⊢P ∋j with ⊢-⊗ ⊢P | ∋-⊗ ∋j
switch ⊢P ∋j | (Δ⊢P -, _) , (Γ≔ , _) | _ , Ψ≔ , _ =
  let W , Γ≔Δj∙W , W≔Δ⊢P∙Ξ = ⊗-assoc (⊗-comm Γ≔) Ψ≔ in
  _ , ∋-frame Ψ≔ Γ≔Δj∙W  ∋j , ⊢-frame (Γ≔ , ∙²-idʳ) (⊗-comm W≔Δ⊢P∙Ξ , ∙²-idʳ) ⊢P

⊢-subst : ∀ {γ : PreCtx n} {idxs : Idxs n} {Γ Ξ Ψ : Ctx idxs} {t  idx}  {m : Usage idx ²}
        → γ ； Ψ ∋[ j ] t ； m ▹ Ξ
        → γ -, t ； Γ -, m ⊢ P ▹ Ψ -, ℓ∅
        → γ -, t ； Γ -, m ⊢ P [ zero ↦ suc j ] ▹ Ξ -, m
⊢-subst {Γ = Γ} {Ξ} (t , y) ⊢P with switch ⊢P y
⊢-subst {Γ = Γ} {Ξ} (t , y) ⊢P | Θ , y' , ⊢P' with ⊢-⊗ ⊢P'
⊢-subst {Γ = Γ} {Ξ} (t , y) ⊢P | Θ , y' , ⊢P' | (_ -, _) , (⊢P'≔ , _) =
  ⊢-frame (proj₂ Γ≔ , ∙²-idˡ) (proj₂ Γ≔ , ∙²-idˡ) ⊢P''
  where
  ⊢P'' = ⊢-subst-ih (sym (∋-≡Type t)) (zero ∙²-idʳ) (suc y') (zero ∙²-idʳ) (suc (∋-ℓ∅ (∋-≡Idx y))) (⊢P'≔ , ∙²-idʳ) refl ⊢P'
  Γ≔ : ∃[ Δ ] (Γ ≔ Δ ⊗ Ξ)
  Γ≔ with ⊢-⊗ ⊢P''
  Γ≔ | (_ -, _) , (x , _) = _ , x

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi