text:
module Relator.Ordering.Proofs where

open import Data
import      Lvl
open import Functional
open import Lang.Instance
open import Logic
open import Logic.Classical
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Type
import      Relator.Ordering
open import Structure.Relator.Ordering
import      Structure.Relator.Names as Names
open import Structure.Relator.Proofs
open import Structure.Relator.Properties
open import Structure.Relator.Properties.Proofs
open import Structure.Relator
open import Structure.Setoid
open import Syntax.Implication
open import Syntax.Transitivity

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓₗ ℓₑ ℓₗₑ ℓₗₜ : Lvl.Level
private variable T : Type{ℓ}

module From-[≤] (_≤_ : T → T → Stmt{ℓₗ}) where
  open        Relator.Ordering.From-[≤] (_≤_)

  [≤][>]-not : ∀{a b} → (a ≤ b) → (a > b) → ⊥
  [≤][>]-not = apply

  [≥][<]-not : ∀{a b} → (a ≥ b) → (a < b) → ⊥
  [≥][<]-not = apply

  module _ ⦃ _ : Equiv{ℓₑ}(T) ⦄ ⦃ _ : Weak.TotalOrder(_≤_)(_≡_) ⦄ where
    [<]-to-[≤] : Names.Subrelation(_<_)(_≤_)
    [<]-to-[≤] {a} {b} nba with converseTotal(_≤_){a}{b}
    [<]-to-[≤] {a} {b} nba | [∨]-introₗ ab = ab
    [<]-to-[≤] {a} {b} nba | [∨]-introᵣ ba = [⊥]-elim(nba ba)
    instance
      [<][≤]-sub : (_<_) ⊆₂ (_≤_)
      _⊆₂_.proof [<][≤]-sub = [<]-to-[≤]

    [>]-to-[≥] : Names.Subrelation(_>_)(_≥_)
    [>]-to-[≥] = [<]-to-[≤]

    [>][≥]-sub : (_>_) ⊆₂ (_≥_)
    _⊆₂_.proof [>][≥]-sub = [>]-to-[≥]

    instance
      [<]-irreflexivity : Irreflexivity(_<_)
      Irreflexivity.proof [<]-irreflexivity = [¬¬]-intro(reflexivity(_≤_))

    instance
      [<]-transitivity : Transitivity(_<_)
      Transitivity.proof [<]-transitivity {a} {b} {c} nba ncb ca = [≤][>]-not (transitivity(_≤_) ca ([<]-to-[≤] nba)) ncb

    instance
      [<]-asymmetry : Asymmetry(_<_) -- TODO: Proof of this property is independent of the model. Actually, many of them here are
      [<]-asymmetry = [irreflexivity,transitivity]-to-asymmetry

    [<]-strictOrder : Strict.PartialOrder(_<_)
    [<]-strictOrder = Strict.intro

    {- TODO: Maybe one must assume decidability of (_≡_)?
    instance
      [<]-total : ConverseTotal(_<_)
      ConverseTotal.proof [<]-total {x} {y} with converseTotal(_≤_)
      ... | [∨]-introₗ x₁ = {!!}
      ... | [∨]-introᵣ x₁ = {!!}
    -}

    instance
      [<][≤]-subtransitivityₗ : Subtransitivityₗ(_<_)(_≤_)
      Subtransitivityₗ.proof [<][≤]-subtransitivityₗ xy yz zx = yz(transitivity(_≤_) zx xy)

    instance
      [<][≤]-subtransitivityᵣ : Subtransitivityᵣ(_<_)(_≤_)
      Subtransitivityᵣ.proof [<][≤]-subtransitivityᵣ xy yz zx = xy(transitivity(_≤_) yz zx)

    [≤][≢]-to-[<] : ∀{a b} → (a ≤ b) → (a ≢ b) → (a < b)
    [≤][≢]-to-[<] le ne ba = ne(antisymmetry(_≤_)(_≡_) le ba)

    [≥][≢]-to-[>] : ∀{a b} → (a ≥ b) → (a ≢ b) → (a > b)
    [≥][≢]-to-[>] ge ne = [≤][≢]-to-[<] ge (ne ∘ symmetry(_≡_))

    module _ ⦃ _ : (_≡_) ⊆₂ (_≤_) ⦄ where -- TODO: Consider including this in weak orders. Or just assume that (_≤_) is a relation and this will follow
      instance
        [≤][≡]-subtransitivityₗ : Subtransitivityₗ(_≤_)(_≡_)
        [≤][≡]-subtransitivityₗ = subrelation-transitivity-to-subtransitivityₗ

      instance
        [≤][≡]-subtransitivityᵣ : Subtransitivityᵣ(_≤_)(_≡_)
        [≤][≡]-subtransitivityᵣ = subrelation-transitivity-to-subtransitivityᵣ

      [≡]-to-[≥] : Names.Subrelation(_≡_)(_≥_)
      [≡]-to-[≥] = sub₂(_≡_)(_≤_) ∘ symmetry(_≡_)
      instance
        [≡][≥]-sub : (_≡_) ⊆₂ (_≥_)
        _⊆₂_.proof [≡][≥]-sub = [≡]-to-[≥]

      [≡][>]-not : ∀{a b} → (a ≡ b) → (a > b) → ⊥
      [≡][>]-not eq gt = [≤][>]-not (sub₂(_≡_)(_≤_) eq) gt

      instance
        [≡][≯]-sub : (_≡_) ⊆₂ (_≯_)
        _⊆₂_.proof [≡][≯]-sub = [≡][>]-not

      instance
        [>][≢]-sub : (_>_) ⊆₂ (_≢_)
        _⊆₂_.proof [>][≢]-sub = swap [≡][>]-not

      [≡][<]-not : ∀{a b} → (a ≡ b) → (a < b) → ⊥
      [≡][<]-not eq lt = [≤][>]-not ([≡]-to-[≥] eq) lt

      instance
        [≡][≮]-sub : (_≡_) ⊆₂ (_≮_)
        _⊆₂_.proof [≡][≮]-sub = [≡][<]-not

      instance
        [<][≢]-sub : (_<_) ⊆₂ (_≢_)
        _⊆₂_.proof [<][≢]-sub = swap [≡][<]-not

      instance
        [<][≡]-subtransitivityₗ : Subtransitivityₗ(_<_)(_≡_)
        Subtransitivityₗ.proof [<][≡]-subtransitivityₗ xy yz zx = [≡][>]-not xy (subtransitivityᵣ(_<_)(_≤_) yz zx)

      instance
        [<][≡]-subtransitivityᵣ : Subtransitivityᵣ(_<_)(_≡_)
        Subtransitivityᵣ.proof [<][≡]-subtransitivityᵣ xy yz zx = [≡][>]-not yz (subtransitivityₗ(_<_)(_≤_) zx xy)

      module _ ⦃ [≡]-classical : Classical₂(_≡_) ⦄ where
        [≤]-or-[>] : ∀{a b} → (a ≤ b) ∨ (a > b)
        [≤]-or-[>] {a} {b} with converseTotal(_≤_){a}{b}
        [≤]-or-[>] {a} {b} | [∨]-introₗ ab = [∨]-introₗ ab
        [≤]-or-[>] {a} {b} | [∨]-introᵣ ba with excluded-middle _ ⦃ [≡]-classical {a}{b} ⦄
        [≤]-or-[>] {a} {b} | [∨]-introᵣ ba | [∨]-introₗ eqab  = [∨]-introₗ (sub₂(_≡_)(_≤_) eqab)
        [≤]-or-[>] {a} {b} | [∨]-introᵣ ba | [∨]-introᵣ neqab = [∨]-introᵣ (ab ↦ neqab(antisymmetry(_≤_)(_≡_) ab ba))

        instance
          [≤]-classical : Classical₂(_≤_)
          Classical.excluded-middle [≤]-classical = [≤]-or-[>]

        [≥]-or-[<] : ∀{a b} → (a ≥ b) ∨ (a < b)
        [≥]-or-[<] = [≤]-or-[>]

        [≥]-classical : Classical₂(_≥_)
        Classical.excluded-middle [≥]-classical = [≥]-or-[<]

        instance
          [<]-classical : Classical₂(_<_)
          Classical.excluded-middle ([<]-classical {a}{b}) with [≤]-or-[>] {b}{a}
          Classical.excluded-middle ([<]-classical {a}{b}) | [∨]-introₗ x = [∨]-introᵣ ([¬¬]-intro x)
          Classical.excluded-middle ([<]-classical {a}{b}) | [∨]-introᵣ x = [∨]-introₗ x

        [>]-classical : Classical₂(_>_)
        [>]-classical = [<]-classical

        [≤]-to-[<][≡] : ∀{a b} → (a ≤ b) → ((a < b) ∨ (a ≡ b))
        [≤]-to-[<][≡] {a} {b} ab with excluded-middle _ ⦃ [≡]-classical {a}{b} ⦄
        [≤]-to-[<][≡] {a} {b} ab | [∨]-introₗ eq = [∨]-introᵣ eq
        [≤]-to-[<][≡] {a} {b} ab | [∨]-introᵣ ne = [∨]-introₗ (ba ↦ ne(antisymmetry(_≤_)(_≡_) ab ba))

        [≥]-to-[>][≡] : ∀{a b} → (a ≥ b) → ((a > b) ∨ (a ≡ b))
        [≥]-to-[>][≡] ab = [∨]-elim2 id (symmetry(_≡_)) ([≤]-to-[<][≡] ab)

module From-[≤][≢] {ℓ₁ ℓ₂ ℓ₃} {T : Type{ℓ₁}} (_≤_ : T → T → Stmt{ℓ₂}) (_≢_ : T → T → Stmt{ℓ₃}) where
  open Relator.Ordering.From-[≤][≢] (_≤_)(_≢_)

  -- postulate instance [<]-totalOrder : Strict.TotalOrder(_<_)

  instance
    [<][≤]-sub : (_<_) ⊆₂ (_≤_)
    _⊆₂_.proof [<][≤]-sub = [∧]-elimₗ

  instance
    [>][≥]-sub : (_>_) ⊆₂ (_≥_)
    _⊆₂_.proof [>][≥]-sub = sub₂(_<_)(_≤_)

  instance
    [<][≢]-sub : (_<_) ⊆₂ (_≢_)
    _⊆₂_.proof [<][≢]-sub = [∧]-elimᵣ

  [>][≢]-sub : ⦃ sym : Symmetry(_≢_) ⦄ → ((_>_) ⊆₂ (_≢_))
  _⊆₂_.proof [>][≢]-sub = symmetry(_≢_) ∘ sub₂(_<_)(_≢_)

  -- [<]-transitivity : ⦃ [≤]-trans : Transitivity(_≤_) ⦄ → Transitivity(_<_)
  -- Transitivity.proof [<]-transitivity ([∧]-intro xy neq-xy) ([∧]-intro yz neq-yz) = [∧]-intro (transitivity(_≤_) xy yz) {!!} xy

  {-
  instance
    [<][≤]-subtransitivityₗ : Subtransitivityₗ(_<_)(_≤_)
    left (Subtransitivityₗ.proof [<][≤]-subtransitivityₗ xy ([∧]-intro yz nyz)) = transitivity(_≤_) xy yz
    Tuple.right (Subtransitivityₗ.proof [<][≤]-subtransitivityₗ xy yz) xz = {!!}
  postulate instance [<][≤]-subtransitivityᵣ : Subtransitivityᵣ(_<_)(_≤_)
  postulate instance [≤][≡]-subtransitivityₗ : Subtransitivityₗ(_≤_)(_≡_)
  postulate instance [≤][≡]-subtransitivityᵣ : Subtransitivityᵣ(_≤_)(_≡_)
  -}

module From-[≤][<]
  ⦃ equiv : Equiv{ℓₑ}(T) ⦄
  (_≤_ : T → T → Stmt{ℓₗₑ}) ⦃ [≤]-relator : BinaryRelator(_≤_) ⦄
  (_<_ : T → T → Stmt{ℓₗₜ}) ⦃ [<]-relator : BinaryRelator(_<_) ⦄
  where

  open Relator.Ordering.From-[≤][<] (_≤_)(_<_)

  private variable a b : T

  [≤]-def-[<][≡]ₗ-[<]-def-[≤][≢]ᵣ : ((∀{a b} → (a ≤ b) ← ((a < b) ∨ (a ≡ b))) ∧ Irreflexivity(_<_)) ↔ ((∀{a b} → (a < b) → ((a ≤ b) ∧ (a ≢ b))) ∧ Reflexivity(_≤_))
  [≤]-def-[<][≡]ₗ-[<]-def-[≤][≢]ᵣ = [↔]-intro (\([∧]-intro p q) → l p ⦃ q ⦄) (\([∧]-intro p q) → r p ⦃ q ⦄) where
    l : (∀{a b} → (a < b) → ((a ≤ b) ∧ (a ≢ b))) → ⦃ refl : Reflexivity(_≤_) ⦄ → ((∀{a b} → (a ≤ b) ← ((a < b) ∨ (a ≡ b))) ∧ Irreflexivity(_<_))
    l [<]-def-[≤][≢]ᵣ = [∧]-intro
      ([∨]-elim (lt ↦ [∧]-elimₗ ([<]-def-[≤][≢]ᵣ lt)) (sub₂(_≡_)(_≤_) ⦃ reflexive-binaryRelator-sub ⦄))
      (intro(xx ↦ [∧]-elimᵣ ([<]-def-[≤][≢]ᵣ xx) (reflexivity(_≡_))))

    r : (∀{a b} → (a ≤ b) ← ((a < b) ∨ (a ≡ b))) → ⦃ irrefl : Irreflexivity(_<_) ⦄ → ((∀{a b} → (a < b) → ((a ≤ b) ∧ (a ≢ b))) ∧ Reflexivity(_≤_))
    r [≤]-def-[<][≡]ᵣ = [∧]-intro
      (lt ↦ [∧]-intro ([≤]-def-[<][≡]ᵣ ([∨]-introₗ lt)) (eq ↦ empty(irreflexivity(_<_) (substitute₂ₗ(_<_) eq lt))))
      (intro ([≤]-def-[<][≡]ᵣ ([∨]-introᵣ (reflexivity(_≡_)))))

  module By-[≤] ([<]-def-[≤][≢] : ∀{a b} → (a < b) ↔ ((a ≤ b) ∧ (a ≢ b))) where
    instance
      [<][≤]-sub : (_<_) ⊆₂ (_≤_)
      _⊆₂_.proof [<][≤]-sub = [∧]-elimₗ ∘ [↔]-to-[→] [<]-def-[≤][≢]

    instance
      [<][≢]-sub : (_<_) ⊆₂ (_≢_)
      _⊆₂_.proof [<][≢]-sub = [∧]-elimᵣ ∘ [↔]-to-[→] [<]-def-[≤][≢]

    module _ ⦃ [≡]-classical : ∀{a b : T} → Classical(a ≡ b) ⦄ where
      [≤]-def-[<][≡]ᵣ-by-classical : (a ≤ b) → ((a < b) ∨ (a ≡ b))
      [≤]-def-[<][≡]ᵣ-by-classical {a}{b} le with excluded-middle(a ≡ b)
      ... | [∨]-introₗ eq = [∨]-introᵣ eq
      ... | [∨]-introᵣ ne = [∨]-introₗ ([↔]-to-[←] [<]-def-[≤][≢] ([∧]-intro le ne))

    module _ ⦃ [<]-tri : ConverseTrichotomy(_<_)(_≡_) ⦄ ⦃ [≤]-antisym : Antisymmetry(_≤_)(_≡_) ⦄ where
      [≤]-def-[<][≡]ᵣ-by-tri-antisym : (a ≤ b) → ((a < b) ∨ (a ≡ b))
      [≤]-def-[<][≡]ᵣ-by-tri-antisym {a}{b} le with trichotomy(_<_)(_≡_) {a}{b}
      ... | [∨]-introₗ ([∨]-introₗ lt) = [∨]-introₗ lt
      ... | [∨]-introₗ ([∨]-introᵣ eq) = [∨]-introᵣ eq
      ... | [∨]-introᵣ             gt  = [∨]-introᵣ (antisymmetry(_≤_)(_≡_) le ([∧]-elimₗ ([↔]-to-[→] [<]-def-[≤][≢] gt)))

    [<]-asymmetry-by-antisym : ⦃ antisym : Antisymmetry(_≤_)(_≡_) ⦄ → Asymmetry(_<_)
    Asymmetry.proof [<]-asymmetry-by-antisym xy yx =
      let [∧]-intro xy-le nxy = [↔]-to-[→] [<]-def-[≤][≢] xy
          [∧]-intro yx-le nyx = [↔]-to-[→] [<]-def-[≤][≢] yx
      in  nxy(antisymmetry(_≤_)(_≡_) xy-le yx-le)

    instance
      [<]-irreflexivity : Irreflexivity(_<_)
      Irreflexivity.proof [<]-irreflexivity xx = [∧]-elimᵣ ([↔]-to-[→] [<]-def-[≤][≢] xx) (reflexivity(_≡_))

    [<]-transitivity-by-asym-trans : ⦃ antisym : Asymmetry(_<_) ⦄ → ⦃ trans : Transitivity(_≤_) ⦄ → Transitivity(_<_)
    Transitivity.proof [<]-transitivity-by-asym-trans xy yz =
      let [∧]-intro xy-le nxy = [↔]-to-[→] [<]-def-[≤][≢] xy
          [∧]-intro yz-le nyz = [↔]-to-[→] [<]-def-[≤][≢] yz
      in  [↔]-to-[←] [<]-def-[≤][≢] ([∧]-intro (transitivity(_≤_) xy-le yz-le) (xz ↦ asymmetry(_<_) (substitute₂ₗ(_<_) xz xy) yz))

  module By-[<] ([≤]-def-[<][≡] : ∀{a b} → (a ≤ b) ↔ ((a < b) ∨ (a ≡ b))) where
    instance
      [<][≤]-sub : (_<_) ⊆₂ (_≤_)
      _⊆₂_.proof [<][≤]-sub = [↔]-to-[←] [≤]-def-[<][≡] ∘ [∨]-introₗ

    instance
      [≡][≤]-sub : (_≡_) ⊆₂ (_≤_)
      _⊆₂_.proof [≡][≤]-sub = [↔]-to-[←] [≤]-def-[<][≡] ∘ [∨]-introᵣ

    instance
      [≰][≮]-sub : (_≰_) ⊆₂ (_≮_)
      _⊆₂_.proof [≰][≮]-sub = contrapositiveᵣ(sub₂(_<_)(_≤_))

    instance
      [≰][≢]-sub : (_≰_) ⊆₂ (_≢_)
      _⊆₂_.proof [≰][≢]-sub = contrapositiveᵣ(sub₂(_≡_)(_≤_))

    instance
      [>][≥]-sub : (_>_) ⊆₂ (_≥_)
      _⊆₂_.proof [>][≥]-sub = sub₂(_<_)(_≤_)

    instance
      [≡][≥]-sub : (_≡_) ⊆₂ (_≥_)
      _⊆₂_.proof [≡][≥]-sub = sub₂(_≡_)(_≤_) ∘ symmetry(_≡_)

    instance
      [≱][≯]-sub : (_≱_) ⊆₂ (_≯_)
      _⊆₂_.proof [≱][≯]-sub = sub₂(_≰_)(_≮_)

    instance
      [≱][≢]-sub : (_≱_) ⊆₂ (_≢_)
      _⊆₂_.proof [≱][≢]-sub = (_∘ symmetry(_≡_)) ∘ sub₂(_≰_)(_≢_)

    [<]-def-[≤][≢]ₗ : (a < b) ← ((a ≤ b) ∧ (a ≢ b))
    [<]-def-[≤][≢]ₗ([∧]-intro le ne) = [∨]-elim id ([⊥]-elim ∘ ne) ([↔]-to-[→] [≤]-def-[<][≡] le)

    instance
      [≤]-reflexivity : Reflexivity(_≤_)
      Reflexivity.proof [≤]-reflexivity = [↔]-to-[←] [≤]-def-[<][≡] ([∨]-introᵣ (reflexivity(_≡_)))

    [≤]-transitivity-by-trans : ⦃ [<]-trans : Transitivity(_<_) ⦄ → Transitivity(_≤_)
    Transitivity.proof [≤]-transitivity-by-trans xy yz with [↔]-to-[→] [≤]-def-[<][≡] xy | [↔]-to-[→] [≤]-def-[<][≡] yz
    ... | [∨]-introₗ xy-lt | [∨]-introₗ yz-lt = [↔]-to-[←] [≤]-def-[<][≡] ([∨]-introₗ (transitivity(_<_) xy-lt yz-lt))
    ... | [∨]-introₗ xy-lt | [∨]-introᵣ yz-eq = [↔]-to-[←] [≤]-def-[<][≡] ([∨]-introₗ (substitute₂ᵣ(_<_) yz-eq xy-lt))
    ... | [∨]-introᵣ xy-eq | [∨]-introₗ yz-lt = [↔]-to-[←] [≤]-def-[<][≡] ([∨]-introₗ (substitute₂ₗ(_<_) (symmetry(_≡_) xy-eq) yz-lt))
    ... | [∨]-introᵣ xy-eq | [∨]-introᵣ yz-eq = [↔]-to-[←] [≤]-def-[<][≡] ([∨]-introᵣ (transitivity(_≡_) xy-eq yz-eq))

    module _ ⦃ asym : Asymmetry(_<_) ⦄ where
      [≤]-antisymmetry-by-asym : Antisymmetry(_≤_)(_≡_)
      Antisymmetry.proof [≤]-antisymmetry-by-asym le ge with [↔]-to-[→] [≤]-def-[<][≡] le | [↔]-to-[→] [≤]-def-[<][≡] ge
      ... | [∨]-introₗ lt  | [∨]-introₗ gt  with () ← asymmetry(_<_) lt gt
      ... | [∨]-introₗ lt  | [∨]-introᵣ eq  = symmetry(_≡_) eq
      ... | [∨]-introᵣ eq  | [∨]-introₗ gt  = eq
      ... | [∨]-introᵣ eq₁ | [∨]-introᵣ eq₂ = eq₁

      [<]-transitivity-by-asym-trans : ⦃ trans : Transitivity(_≤_) ⦄ → Transitivity(_<_)
      Transitivity.proof [<]-transitivity-by-asym-trans {x}{y}{z} xy yz =
        • (
          • (xy ⇒
            (x < y) ⇒-[ [↔]-to-[←] [≤]-def-[<][≡] ∘ [∨]-introₗ ]
            (x ≤ y) ⇒-end
          )
          • (yz ⇒
            (y < z) ⇒-[ [↔]-to-[←] [≤]-def-[<][≡] ∘ [∨]-introₗ ]
            (y ≤ z) ⇒-end
          )
          ⇒₂-[ transitivity(_≤_) ]
          (x ≤ z)           ⇒-[ [↔]-to-[→] [≤]-def-[<][≡] ]
          (x < z) ∨ (x ≡ z) ⇒-end
        )
        • (
          (\xz →
            • (xz ⇒
              (x ≡ z) ⇒-[ apply xy ∘ substitute₂ₗ(_<_) ]
              (z < y) ⇒-end
            )
            • (yz ⇒
              (y < z) ⇒-end
            )
            ⇒₂-[ asymmetry(_<_) ]
            ⊥       ⇒-end
          ) ⇒
          (x ≢ z) ⇒-end
        )
        ⇒₂-[ [∨]-not-right ]
        (x < z) ⇒-end

      [<][≱]-sub-by-asym : ((_<_) ⊆₂ (_≱_))
      _⊆₂_.proof [<][≱]-sub-by-asym lt-xy ge-xy = [∨]-elim
        (lt-yx ↦ asymmetry(_<_) lt-xy lt-yx)
        (eq-yx ↦ irreflexivity(_<_) ⦃ [asymmetry]-to-irreflexivity ⦄ (substitute₂ᵣ(_<_) eq-yx lt-xy))
        ([↔]-to-[→] [≤]-def-[<][≡] ge-xy)

      [>][≰]-sub-by-asym : ((_>_) ⊆₂ (_≰_))
      _⊆₂_.proof [>][≰]-sub-by-asym gt le = [∨]-elim
        (asymmetry(_<_) gt)
        (eq ↦ irreflexivity(_<_) ⦃ [asymmetry]-to-irreflexivity ⦄ (substitute₂ᵣ(_<_) eq gt))
        ([↔]-to-[→] [≤]-def-[<][≡] le)

    module _
      ⦃ [<]-classical : Classical₂(_<_) ⦄
      ⦃ [≡]-classical : Classical₂(_≡_) ⦄
      where

      [≤]-classical-by-classical : Classical₂(_≤_)
      Classical.excluded-middle ([≤]-classical-by-classical {x}{y}) with excluded-middle(x < y) | excluded-middle(x ≡ y)
      ... | [∨]-introₗ lt  | _             = [∨]-introₗ (sub₂(_<_)(_≤_) lt)
      ... | [∨]-introᵣ nlt | [∨]-introₗ eq = [∨]-introₗ (sub₂(_≡_)(_≤_) eq)
      ... | [∨]-introᵣ nlt | [∨]-introᵣ ne = [∨]-introᵣ (le ↦ nlt ([<]-def-[≤][≢]ₗ ([∧]-intro le ne)))

    module _
      ⦃ [<]-asym : Asymmetry(_<_) ⦄
      ⦃ [<]-total : ConverseTrichotomy(_<_)(_≡_) ⦄
      where

      [≤]-classical-by-asym-tri : Classical₂(_≤_)
      Classical.excluded-middle ([≤]-classical-by-asym-tri {x} {y}) with trichotomy(_<_)(_≡_) {x}{y}
      ... | [∨]-introₗ([∨]-introₗ lt) = [∨]-introₗ (sub₂(_<_)(_≤_) lt)
      ... | [∨]-introₗ([∨]-introᵣ eq) = [∨]-introₗ (sub₂(_≡_)(_≤_) eq)
      ... | [∨]-introᵣ            gt  =
        let [<]-def-[≤][≢]ᵣ = [∧]-elimₗ ([↔]-to-[→] [≤]-def-[<][≡]ₗ-[<]-def-[≤][≢]ᵣ ([∧]-intro ([↔]-to-[←] [≤]-def-[<][≡]) [asymmetry]-to-irreflexivity))
            [∧]-intro ge ne = [<]-def-[≤][≢]ᵣ gt
        in  [∨]-introᵣ (ne ∘ antisymmetry(_≤_)(_≡_) ⦃ [≤]-antisymmetry-by-asym ⦄ ge)

  -- TODO: Move to Structure.Relator.Properties.Proofs
  module _
    ⦃ [<]-asym : Asymmetry(_<_) ⦄
    ⦃ [<]-total : ConverseTrichotomy(_<_)(_≡_) ⦄
    where

    [<]-classical-by-asym-tri : Classical₂(_<_)
    Classical.excluded-middle ([<]-classical-by-asym-tri {x} {y}) with trichotomy(_<_)(_≡_) {x}{y}
    ... | [∨]-introₗ([∨]-introₗ lt) = [∨]-introₗ lt
    ... | [∨]-introₗ([∨]-introᵣ eq) = [∨]-introᵣ (lt ↦ irreflexivity(_<_) ⦃ [asymmetry]-to-irreflexivity ⦄ (substitute₂ₗ(_<_) eq lt))
    ... | [∨]-introᵣ            gt  = [∨]-introᵣ (lt ↦ asymmetry(_<_) lt gt)

  module ByReflTriSub
    ⦃ [≤]-refl : Reflexivity(_≤_) ⦄
    ⦃ [<]-total : ConverseTrichotomy(_<_)(_≡_) ⦄
    ⦃ [<][≤]-sub : (_<_) ⊆₂ (_≤_) ⦄
    where

    [≰][≯]-not : (a ≰ b) → (a ≯ b) → ⊥
    [≰][≯]-not {a}{b} nle ngt with trichotomy(_<_)(_≡_) {a}{b}
    ... | [∨]-introₗ([∨]-introₗ lt) = nle (sub₂(_<_)(_≤_) lt)
    ... | [∨]-introₗ([∨]-introᵣ eq) = substitute₂ₗ(_≰_) ⦃ [¬]-binaryRelator ⦄ eq nle (reflexivity(_≤_))
    ... | [∨]-introᵣ            gt  = ngt gt

    [≮][≱]-not : (a ≮ b) → (a ≱ b) → ⊥
    [≮][≱]-not = swap [≰][≯]-not

    module _ ⦃ [<]-classical : Classical₂(_<_) ⦄ where
      [≰][>]-sub : (_≰_) ⊆₂ (_>_)
      _⊆₂_.proof [≰][>]-sub = [¬¬]-elim ∘ [≰][≯]-not

      [≱][<]-sub : (_≱_) ⊆₂ (_<_)
      _⊆₂_.proof [≱][<]-sub = _⊆₂_.proof [≰][>]-sub

    module _ ⦃ [≤]-classical : Classical₂(_≤_) ⦄ where
      [≯][≤]-sub : (_≯_) ⊆₂ (_≤_)
      _⊆₂_.proof [≯][≤]-sub = [¬¬]-elim ∘ swap [≰][≯]-not

      [≮][≥]-sub : (_≮_) ⊆₂ (_≥_)
      _⊆₂_.proof [≮][≥]-sub = _⊆₂_.proof [≯][≤]-sub

    module _
      ⦃ [≤]-classical : Classical₂(_≤_) ⦄
      ⦃ [<]-classical : Classical₂(_<_) ⦄
      where

      [≤]-or-[>] : (a ≤ b) ∨ (a > b)
      [≤]-or-[>] {a}{b} with excluded-middle(a ≤ b)
      ... | [∨]-introₗ a≤b = [∨]-introₗ a≤b
      ... | [∨]-introᵣ a≰b = [∨]-introᵣ (sub₂(_≰_)(_>_) ⦃ [≰][>]-sub ⦄ a≰b)

      [≥]-or-[<] : (a ≥ b) ∨ (a < b)
      [≥]-or-[<] {a}{b} with excluded-middle(a ≥ b)
      ... | [∨]-introₗ a≥b = [∨]-introₗ a≥b
      ... | [∨]-introᵣ a≱b = [∨]-introᵣ (sub₂(_≱_)(_<_) ⦃ [≱][<]-sub ⦄ a≱b)

  module ByStrictPartialOrder ([≤]-def-[<][≡] : ∀{a b} → (a ≤ b) ↔ ((a < b) ∨ (a ≡ b))) ⦃ ord : Strict.PartialOrder(_<_) ⦄ where
    open By-[<] [≤]-def-[<][≡]

    open By-[<] [≤]-def-[<][≡] public
      using
      ( [<][≤]-sub
      ; [≡][≤]-sub
      ; [≰][≮]-sub
      ; [≰][≢]-sub
      ; [>][≥]-sub
      ; [≡][≥]-sub
      ; [≱][≯]-sub
      ; [≱][≢]-sub
      ; [<]-def-[≤][≢]ₗ
      ; [≤]-reflexivity
      )

    instance
      [≤]-transitivity : Transitivity(_≤_)
      [≤]-transitivity = [≤]-transitivity-by-trans

    instance
      [≤]-antisymmetry : Antisymmetry(_≤_)(_≡_)
      [≤]-antisymmetry = [≤]-antisymmetry-by-asym

    instance
      [≤]-weakPartialorder : Weak.PartialOrder(_≤_)(_≡_)
      [≤]-weakPartialorder = record{}

    instance
      [<][≱]-sub : ((_<_) ⊆₂ (_≱_))
      [<][≱]-sub = [<][≱]-sub-by-asym

    instance
      [>][≰]-sub : ((_>_) ⊆₂ (_≰_))
      [>][≰]-sub = [>][≰]-sub-by-asym

  module ByStrictTotalOrder ([≤]-def-[<][≡] : ∀{a b} → (a ≤ b) ↔ ((a < b) ∨ (a ≡ b))) ⦃ ord : Strict.TotalOrder(_<_)(_≡_) ⦄ where
    open By-[<] [≤]-def-[<][≡]

    open ByStrictPartialOrder [≤]-def-[<][≡] public

    instance
      [<]-classical : Classical₂(_<_)
      [<]-classical = [<]-classical-by-asym-tri

    instance
      [≤]-classical : Classical₂(_≤_)
      [≤]-classical = [≤]-classical-by-asym-tri

    [≰][≯]-not : (a ≰ b) → (a ≯ b) → ⊥
    [≰][≯]-not = ByReflTriSub.[≰][≯]-not

    [≮][≱]-not : (a ≮ b) → (a ≱ b) → ⊥
    [≮][≱]-not = ByReflTriSub.[≮][≱]-not

    instance
      [≰][>]-sub : (_≰_) ⊆₂ (_>_)
      [≰][>]-sub = ByReflTriSub.[≰][>]-sub

    instance
      [≱][<]-sub : (_≱_) ⊆₂ (_<_)
      [≱][<]-sub = ByReflTriSub.[≱][<]-sub

    instance
      [≯][≤]-sub : (_≯_) ⊆₂ (_≤_)
      [≯][≤]-sub = ByReflTriSub.[≯][≤]-sub

    instance
      [≮][≥]-sub : (_≮_) ⊆₂ (_≥_)
      [≮][≥]-sub = ByReflTriSub.[≮][≥]-sub

    [≤]-or-[>] : (a ≤ b) ∨ (a > b)
    [≤]-or-[>] = ByReflTriSub.[≤]-or-[>]

    [≥]-or-[<] : (a ≥ b) ∨ (a < b)
    [≥]-or-[<] = ByReflTriSub.[≥]-or-[<]


text:
module HasSatisfaction where

open import OscarPrelude
open import Interpretation

record HasSatisfaction (A : Set) : Set₁
 where
  field
    _⊨_ : Interpretation → A → Set

  _⊭_ : Interpretation → A → Set
  _⊭_ I = ¬_ ∘ I ⊨_

open HasSatisfaction ⦃ … ⦄ public

{-# DISPLAY HasSatisfaction._⊨_ _ = _⊨_ #-}
{-# DISPLAY HasSatisfaction._⊭_ _ = _⊭_ #-}

instance HasSatisfactionList : {A : Set} ⦃ _ : HasSatisfaction A ⦄ → HasSatisfaction $ List A
HasSatisfaction._⊨_ HasSatisfactionList I [] = ⊤
HasSatisfaction._⊨_ HasSatisfactionList I (x ∷ xs) = I ⊨ x × I ⊨ xs

module _ {A} ⦃ _ : HasSatisfaction A ⦄
 where

   ⊨_ : A → Set
   ⊨ x = (I : Interpretation) → I ⊨ x

   ⊭_ : A → Set
   ⊭_ = ¬_ ∘ ⊨_

record HasDecidableValidation (A : Set) ⦃ _ : HasSatisfaction A ⦄ : Set₁
 where
  field
    ⊨?_ : (x : A) → Dec $ ⊨ x

open HasDecidableValidation ⦃ … ⦄ public

{-# DISPLAY HasDecidableValidation.⊨?_ _ = ⊨?_ #-}

record HasDecidableSatisfaction (A : Set) ⦃ _ : HasSatisfaction A ⦄ : Set₁
 where
  field
    _⊨?_ : (I : Interpretation) → (x : A) → Dec (I ⊨ x)

open HasDecidableSatisfaction ⦃ … ⦄ public

{-# DISPLAY HasDecidableSatisfaction._⊨?_ _ = _⊨?_ #-}

ext: agda


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

open import Algebra
open import Relation.Unary
open import Relation.Binary hiding (Decidable)

module Data.FingerTree.Split.Intermediate
  {r m}
  (ℳ : Monoid r m)
  {s}
  {ℙ : Pred (Monoid.Carrier ℳ) s}
  (ℙ-resp : ℙ Respects (Monoid._≈_ ℳ))
  (ℙ? : Decidable ℙ)
  where

open import Relation.Nullary using (¬_; yes; no; Dec)
open import Level using (_⊔_)
open import Data.Product
open import Function
open import Data.List as List using (List; _∷_; [])

open import Data.FingerTree.Measures ℳ
open import Data.FingerTree.Structures ℳ
open import Data.FingerTree.Reasoning ℳ
open import Data.FingerTree.View ℳ using (deepₗ; deepᵣ)
open import Data.FingerTree.Cons ℳ using (listToTree)

open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (True; toWitness; False; toWitnessFalse)

open σ ⦃ ... ⦄

open Monoid ℳ renaming (Carrier to 𝓡)

open import Data.FingerTree.Relation.Binary.Reasoning.FasterInference.Setoid setoid

open import Data.FingerTree.Split.Point ℳ ℙ-resp ℙ?
open import Data.FingerTree.Split.StoredPredicate ℳ ℙ-resp ℙ?

open import Data.Empty.Irrelevant using (⊥-elim)

record Split′ (i : 𝓡) {a b} (Σ : Set a) (A : Set b) ⦃ _ : σ Σ ⦄ ⦃ _ : σ A ⦄ : Set (a ⊔ b ⊔ s) where
  constructor _∷⟨_⟩∷_[_]
  field
    left′  : Σ
    focus′ : A
    right′ : Σ
    .proof′ : i ∙ μ left′ ∣ μ focus′
open Split′ public
instance
  σ-Split′ : ∀  {a b} {Σ : Set a} {A : Set b} ⦃ _ : σ Σ ⦄ ⦃ _ : σ A ⦄ {i : 𝓡} → σ (Split′ i Σ A)
  μ ⦃ σ-Split′ {i = i} ⦄ (l ∷⟨ x ⟩∷ r [ _ ]) = i ∙ (μ l ∙ (μ x ∙ μ r))

infixl 2 _i≈[_]
_i≈[_] : ∀ {a b} {Σ : Set a} {A : Set b} ⦃ _ : σ Σ ⦄ ⦃ _ : σ A ⦄
          → ∀ {i xs}
          → μ⟨ Split′ i Σ A ⟩≈ (i ∙ xs)
          → ∀ {j}
          → i ≈ j → μ⟨ Split′ j Σ A ⟩≈ (j ∙ xs)
xs ∷⟨ x ⟩∷ ys [ p₁ ] ⇑[ p₂ ] i≈[ i≈ ] = xs ∷⟨ x ⟩∷ ys [ p₁ ≈◄⟅ ≪∙ i≈ ⟆ ] ⇑[ ≪∙ sym i≈ ⍮ p₂ ⍮ ≪∙ i≈ ]
{-# INLINE _i≈[_] #-}

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.AbGroup.Instances.Unit where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Unit renaming (Unit* to UnitType)

open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Group.Instances.Unit using (UnitGroup)
open import Cubical.Algebra.Group.Base using (GroupStr)

private
  variable
    ℓ : Level

open AbGroupStr
open IsAbGroup

UnitAbGroup : AbGroup ℓ
fst UnitAbGroup = UnitType
0g (snd UnitAbGroup) = tt*
_+_ (snd UnitAbGroup) = λ _ _ → tt*
- snd UnitAbGroup = λ _ → tt*
isGroup (isAbGroup (snd UnitAbGroup)) = GroupStr.isGroup (snd UnitGroup)
+Comm (isAbGroup (snd UnitAbGroup)) = λ _ _ → refl

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2019-05-30, issue #3824:
-- Named where module should be in scope even if defined under a rewrite.

open import Agda.Builtin.Equality

postulate
  A   : Set
  a b : A
  a≡b : a ≡ b
  P   : A → Set

cast : P a → P b
cast p rewrite a≡b = q
  module M where
    q = p

test : P b → P b
test = M.q

-- ERROR WAS: M.q not in scope.

module Test = M

-- ERROR WAS: M not in scope.

-- Should succeed.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module TelescopingLet4 where

module Star where
  ★ : Set₁
  ★ = Set

  ★₁ : Set₂
  ★₁ = Set₁

data D5 (open Star using (★₁)) : ★₁ where


text:
open import Data.Bool.Base using (Bool)
------------------------------------------------------------------------
-- The Agda standard library
--
-- IO
------------------------------------------------------------------------

open import Coinduction
open import Data.Unit
open import Data.String
open import Data.Colist
open import Function
import IO.Primitive as Prim
open import Level

------------------------------------------------------------------------
-- The IO monad

-- One cannot write "infinitely large" computations with the
-- postulated IO monad in IO.Primitive without turning off the
-- termination checker (or going via the FFI, or perhaps abusing
-- something else). The following coinductive deep embedding is
-- introduced to avoid this problem. Possible non-termination is
-- isolated to the run function below.

infixl 1 _>>=_ _>>_

data IO {a} (A : Set a) : Set (suc a) where
  lift   : (m : Prim.IO A) → IO A
  return : (x : A) → IO A
  _>>=_  : {B : Set a} (m : ∞ (IO B)) (f : (x : B) → ∞ (IO A)) → IO A
  _>>_   : {B : Set a} (m₁ : ∞ (IO B)) (m₂ : ∞ (IO A)) → IO A

{-# NON_TERMINATING #-}

run : ∀ {a} {A : Set a} → IO A → Prim.IO A
run (lift m)   = m
run (return x) = Prim.return x
run (m  >>= f) = Prim._>>=_ (run (♭ m )) λ x → run (♭ (f x))
run (m₁ >> m₂) = Prim._>>=_ (run (♭ m₁)) λ _ → run (♭ m₂)

putStr∞ : Costring → IO ⊤
putStr∞ s =
  ♯ lift (Prim.putStr s) >>
  ♯ return _

putStr : String → IO ⊤
putStr s = putStr∞ (toCostring s)

putStrLn∞ : Costring → IO ⊤
putStrLn∞ s =
  ♯ lift (Prim.putStrLn s) >>
  ♯ return _

putStrLn : String → IO ⊤
putStrLn s = putStrLn∞ (toCostring s)

_∨_ : Bool → Bool → Bool
Bool.true ∨ _  = Bool.true
Bool.false ∨ b = b

_∧_ : Bool → Bool → Bool
Bool.false ∧ _ = Bool.false
Bool.true ∧ b  = b

if_then_else_ : {A : Set} → Bool → A → A → A
if Bool.true  then a else _ = a
if Bool.false then _ else b = b

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

_>>>_ : String → String → String
_>>>_ = primStringAppend

infixl 1 _>>>_

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

data Principle : Set where
  # : String → Principle

_=p=_ : Principle → Principle → Bool
(# a) =p= (# b) = a == b

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

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A
infixr 5 _∷_

[[_]] : {A : Set} → A → List A
[[ x ]] = x ∷ []

any : {A : Set} → (A → Bool) → List A → Bool
any _ []       = Bool.false
any f (x ∷ xs) = (f x) ∨ (any f xs)

_∈∈_ : Principle → List Principle → Bool
x ∈∈ []       = Bool.false
x ∈∈ (y ∷ ys) with x =p= y
...             | Bool.true  = Bool.true
...             | Bool.false = x ∈∈ ys

_∋∋_ : List Principle → Principle → Bool
xs ∋∋ y = y ∈∈ xs

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

data Arrow : Set where
  ⇒_  : Principle → Arrow
  _⇒_ : Principle → Arrow → Arrow

_≡≡_ : Arrow → Arrow → Bool
(⇒ q) ≡≡ (⇒ s)     = q =p= s
(p ⇒ q) ≡≡ (r ⇒ s) = (p =p= r) ∧ (q ≡≡ s)
_ ≡≡ _             = Bool.false

_∈∈∈∈_ : Arrow → List Arrow → Bool
x ∈∈∈∈ []       = Bool.false
x ∈∈∈∈ (y ∷ ys) with x ≡≡ y
...              | Bool.true  = Bool.true
...              | Bool.false = x ∈∈∈∈ ys

closure : List Arrow → List Principle → List Principle
closure [] found               = found
closure ((⇒ n) ∷ rest) found   = n ∷ (closure rest (n ∷ found))
closure ((n ⇒ q) ∷ rest) found with (n ∈∈ found) ∨ (n ∈∈ (closure rest found))
...                               | Bool.true  = closure (q ∷ rest) found
...                               | Bool.false = closure rest found

_,_⊢_ : List Arrow → List Principle → Principle → Bool
cs , ps ⊢ q = q ∈∈ (closure cs ps)

_⊢_ : List Arrow → Arrow → Bool
cs ⊢ (⇒ q)   = q ∈∈ (closure cs [])
cs ⊢ (p ⇒ q) = ((⇒ p) ∷ cs) ⊢ q

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

data Separation : Set where
  model : List Principle → List Principle → Separation

modelsupports : Separation → List Arrow → Principle → Bool
modelsupports (model holds _) cs n = cs , holds ⊢ n

modeldenies : Separation → List Arrow → Principle → Bool
modeldenies (model _ fails) cs n = any (_∋∋_ (closure cs ([[ n ]]))) fails

_⟪!_⟫_ : List Arrow → Separation → Arrow → Bool
cs ⟪! m ⟫ (⇒ q) = modeldenies m cs q
cs ⟪! m ⟫ (p ⇒ q) = (modelsupports m cs p) ∧ (cs ⟪! m ⟫ q)

_⟪_⟫_ : List Arrow → List Separation → Arrow → Bool
cs ⟪ [] ⟫ arr     = Bool.false
cs ⟪ m ∷ ms ⟫ arr = (cs ⟪! m ⟫ arr) ∨ (cs ⟪ ms ⟫ arr)

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

data Relation : Set where
  Proved    : Relation
  Derivable : Relation
  Separated : Relation
  Unknown   : Relation

consider : List Arrow → List Separation → Arrow → Relation
consider cs ms arr with (arr ∈∈∈∈ cs)
...                   | Bool.true  = Proved
...                   | Bool.false with (cs ⊢ arr)
...                              | Bool.true  = Derivable
...                              | Bool.false with (cs ⟪ ms ⟫ arr)
...                                         | Bool.true  = Separated
...                                         | Bool.false = Unknown

proofs : List Arrow
proofs =
   ((# "3") ⇒ (⇒ (# "4"))) ∷
--   ((# "5") ⇒ (⇒ (# "4"))) ∷
   ((# "6") ⇒ (⇒ (# "4"))) ∷
   ((# "3") ⇒ (⇒ (# "3"))) ∷
   ((# "3") ⇒ (⇒ (# "3"))) ∷
   ((# "9") ⇒ (⇒ (# "3"))) ∷
   ((# "9") ⇒ (⇒ (# "3"))) ∷
   ((# "5") ⇒ (⇒ (# "7"))) ∷
   ((# "9") ⇒ (⇒ (# "7"))) ∷
   ((# "6") ⇒ (⇒ (# "8"))) ∷
   ((# "10") ⇒ (⇒ (# "8"))) ∷
   ((# "10") ⇒ (⇒ (# "7"))) ∷
   ((# "5") ⇒ (⇒ (# "10"))) ∷
   ((# "10") ⇒ (⇒ (# "4"))) ∷
   ((# "5") ⇒ (⇒ (# "11"))) ∷
   ((# "6") ⇒ (⇒ (# "11"))) ∷
   ((# "11") ⇒ (⇒ (# "4"))) ∷
   ((# "10") ⇒ (⇒ (# "7"))) ∷
   ((# "8") ⇒ (⇒ (# "4"))) ∷
   ((# "9") ⇒ (⇒ (# "7"))) ∷
   ((# "9") ⇒ (⇒ (# "8"))) ∷
   ((# "3") ⇒ (⇒ (# "8"))) ∷
   ((# "5") ⇒ ((# "3") ⇒ (⇒ (# "9")))) ∷
   ((# "6") ⇒ ((# "7") ⇒ (⇒ (# "10")))) ∷
   ((# "6") ⇒ ((# "3") ⇒ (⇒ (# "3")))) ∷
   ((# "7") ⇒ (⇒ (# "7"))) ∷
   ((# "7") ⇒ (⇒ (# "7"))) ∷
   ((# "7") ⇒ ((# "8") ⇒ (⇒ (# "10")))) ∷
   ((# "3") ⇒ ((# "10") ⇒ (⇒ (# "9")))) ∷
   ((# "5") ⇒ (⇒ (# "1"))) ∷
   ((# "3") ⇒ ((# "1") ⇒ (⇒ (# "9")))) ∷
   ((# "1") ⇒ (⇒ (# "2"))) ∷
   ((# "10") ⇒ (⇒ (# "2"))) ∷ []

cms : List Separation
cms =
  (model ((# "12") ∷ (# "6") ∷ (# "11") ∷ (# "4") ∷ (# "1") ∷ []) ((# "5") ∷ (# "3") ∷ (# "7") ∷ (# "7") ∷ [])) ∷
  (model ((# "6") ∷ (# "3") ∷ (# "11") ∷ (# "4") ∷ (# "7") ∷ (# "8") ∷ (# "3") ∷ (# "9") ∷ (# "10") ∷ (# "1") ∷ []) ((# "5") ∷ [])) ∷
  (model ((# "12") ∷ (# "5") ∷ (# "11") ∷ (# "4") ∷ (# "1") ∷ []) ((# "6") ∷ (# "3") ∷ [])) ∷
  (model ((# "5") ∷ (# "3") ∷ (# "11") ∷ (# "4") ∷ (# "7") ∷ (# "8") ∷ (# "3") ∷ (# "9") ∷ (# "10") ∷ (# "1") ∷ []) ((# "6") ∷ [])) ∷
  (model ((# "12") ∷ (# "4") ∷ (# "11") ∷ []) ((# "5") ∷ (# "6") ∷ (# "3") ∷ (# "8") ∷ (# "9") ∷ (# "1") ∷ [])) ∷
  (model ((# "12") ∷ (# "5") ∷ (# "6") ∷ (# "4") ∷ (# "11") ∷ (# "1") ∷ []) ((# "3") ∷ [])) ∷
  (model ((# "12") ∷ (# "4") ∷ (# "11") ∷ (# "7") ∷ []) ((# "9") ∷ (# "5") ∷ (# "6") ∷ (# "10") ∷ (# "8") ∷ (# "1") ∷ [])) ∷
  (model ((# "10") ∷ (# "9") ∷ []) ((# "1") ∷ [])) ∷
  (model ((# "3") ∷ (# "4") ∷ (# "11") ∷ []) ((# "9") ∷ (# "5") ∷ (# "6") ∷ (# "10") ∷ (# "7") ∷ (# "1") ∷ [])) ∷
  (model ((# "12") ∷ (# "7") ∷ (# "1") ∷ []) ((# "4") ∷ (# "11") ∷ (# "8") ∷ [])) ∷
  (model ((# "9") ∷ (# "3") ∷ (# "10") ∷ (# "8") ∷ (# "1") ∷ []) ((# "11") ∷ [])) ∷
  (model ((# "12") ∷ (# "4") ∷ (# "10") ∷ (# "1") ∷ []) ((# "11") ∷ (# "3") ∷ [])) ∷
  (model ((# "3") ∷ (# "6") ∷ (# "5") ∷ []) ([])) ∷
  (model ((# "1") ∷ (# "2") ∷ (# "3") ∷ (# "4") ∷ (# "5") ∷ (# "6") ∷ (# "7") ∷ (# "8") ∷ (# "9") ∷ (# "10") ∷ (# "11") ∷ []) ((# "12") ∷ [])) ∷ []

testp : Relation
testp = consider proofs cms ((# "5") ⇒ (⇒ (# "10")))

testd : Relation
testd = consider proofs cms ((# "5") ⇒ (⇒ (# "4")))

tests : Relation
tests = consider proofs cms ((# "5") ⇒ (⇒ (# "3")))

testu : Relation
testu = consider proofs cms ((# "6") ⇒ (⇒ (# "1")))

testcl : List Principle
testcl = closure proofs ((# "5") ∷ [])

stringifylp : List Principle → String
stringifylp [] = "[]"
stringifylp ((# s) ∷ xs) = s >>> " ∷ " >>> (stringifylp xs)

main = run (putStrLn (stringifylp testcl))

max_stars_repo_name: louisswarren/hieretikz

max_issues_repo_name: louisswarren/hieretikz

max_forks_repo_name: louisswarren/hieretikz


text:
open import Relation.Binary.PropositionalEquality as P
open import Function
open import Streams

tl' : ∀{A} → Stream A → Stream A
tl' s = tl s

coind : ∀{A X : Set} → (f g : X → Stream A) →
        hd ∘ f ≡ hd ∘ g →
        (u : ?) →
        ((v : ∀ x → f x ~ g x) → v ∘ u
        ∀ x → f x ~ g x
hd~ (coind f g p x) = cong-app p x
tl~ (coind f g p x) = coind (tl' ∘ f) (tl' ∘ g) {!!} {!!}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Coinductive vectors
------------------------------------------------------------------------

module Data.Covec where

open import Coinduction
open import Data.Nat using (ℕ; zero; suc)
open import Data.Conat as Coℕ using (Coℕ; zero; suc; _+_)
open import Data.Cofin using (Cofin; zero; suc)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Colist as Colist using (Colist; []; _∷_)
open import Data.Product using (_,_)
open import Relation.Binary

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

infixr 5 _∷_

data Covec (A : Set) : Coℕ → Set where
  []  : Covec A zero
  _∷_ : ∀ {n} (x : A) (xs : ∞ (Covec A (♭ n))) → Covec A (suc n)

------------------------------------------------------------------------
-- Some operations

map : ∀ {A B n} → (A → B) → Covec A n → Covec B n
map f []       = []
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

fromVec : ∀ {A n} → Vec A n → Covec A (Coℕ.fromℕ n)
fromVec []       = []
fromVec (x ∷ xs) = x ∷ ♯ fromVec xs

fromColist : ∀ {A} (xs : Colist A) → Covec A (Colist.length xs)
fromColist []       = []
fromColist (x ∷ xs) = x ∷ ♯ fromColist (♭ xs)

take : ∀ {A} m {n} → Covec A (m + n) → Covec A m
take zero    xs       = []
take (suc n) (x ∷ xs) = x ∷ ♯ take (♭ n) (♭ xs)

drop : ∀ {A} m {n} → Covec A (Coℕ.fromℕ m + n) → Covec A n
drop zero    xs       = xs
drop (suc n) (x ∷ xs) = drop n (♭ xs)

replicate : ∀ {A} n → A → Covec A n
replicate zero    x = []
replicate (suc n) x = x ∷ ♯ replicate (♭ n) x

lookup : ∀ {A n} → Cofin n → Covec A n → A
lookup zero    (x ∷ xs) = x
lookup (suc n) (x ∷ xs) = lookup n (♭ xs)

infixr 5 _++_

_++_ : ∀ {A m n} → Covec A m → Covec A n → Covec A (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)

[_] : ∀ {A} → A → Covec A (suc (♯ zero))
[ x ] = x ∷ ♯ []

------------------------------------------------------------------------
-- Equality and other relations

-- xs ≈ ys means that xs and ys are equal.

infix 4 _≈_

data _≈_ {A} : ∀ {n} (xs ys : Covec A n) → Set where
  []  : [] ≈ []
  _∷_ : ∀ {n} x {xs ys}
        (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → _≈_ {n = suc n} (x ∷ xs) (x ∷ ys)

-- x ∈ xs means that x is a member of xs.

infix 4 _∈_

data _∈_ {A} : ∀ {n} → A → Covec A n → Set where
  here  : ∀ {n x  } {xs}                   → _∈_ {n = suc n} x (x ∷ xs)
  there : ∀ {n x y} {xs} (x∈xs : x ∈ ♭ xs) → _∈_ {n = suc n} x (y ∷ xs)

-- xs ⊑ ys means that xs is a prefix of ys.

infix 4 _⊑_

data _⊑_ {A} : ∀ {m n} → Covec A m → Covec A n → Set where
  []  : ∀ {n} {ys : Covec A n} → [] ⊑ ys
  _∷_ : ∀ {m n} x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) →
        _⊑_ {m = suc m} {suc n} (x ∷ xs) (x ∷ ys)

------------------------------------------------------------------------
-- Some proofs

setoid : Set → Coℕ → Setoid _ _
setoid A n = record
  { Carrier       = Covec A n
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : ∀ {A n} → Reflexive (_≈_ {A} {n})
  refl {x = []}     = []
  refl {x = x ∷ xs} = x ∷ ♯ refl

  sym : ∀ {A n} → Symmetric (_≈_ {A} {n})
  sym []        = []
  sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈)

  trans : ∀ {A n} → Transitive (_≈_ {A} {n})
  trans []        []         = []
  trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)

poset : Set → Coℕ → Poset _ _ _
poset A n = record
  { Carrier        = Covec A n
  ; _≈_            = _≈_
  ; _≤_            = _⊑_
  ; isPartialOrder = record
    { isPreorder = record
      { isEquivalence = Setoid.isEquivalence (setoid A n)
      ; reflexive     = reflexive
      ; trans         = trans
      }
    ; antisym  = antisym
    }
  }
  where
  reflexive : ∀ {A n} → _≈_ {A} {n} ⇒ _⊑_
  reflexive []        = []
  reflexive (x ∷ xs≈) = x ∷ ♯ reflexive (♭ xs≈)

  trans : ∀ {A n} → Transitive (_⊑_ {A} {n})
  trans []        _          = []
  trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)

  antisym : ∀ {A n} → Antisymmetric (_≈_ {A} {n}) _⊑_
  antisym []       []        = []
  antisym (x ∷ p₁) (.x ∷ p₂) = x ∷ ♯ antisym (♭ p₁) (♭ p₂)

map-cong : ∀ {A B n} (f : A → B) → _≈_ {n = n} =[ map f ]⇒ _≈_
map-cong f []        = []
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)

take-⊑ : ∀ {A} m {n} (xs : Covec A (m + n)) → take m xs ⊑ xs
take-⊑ zero    xs       = []
take-⊑ (suc n) (x ∷ xs) = x ∷ ♯ take-⊑ (♭ n) (♭ xs)


text:
-- Andreas, 2022-03-28, issue #5856, reported by Szumi Xie.
-- Patterns in path-lambdas were simply ignored, but should be illegal.

{-# OPTIONS --cubical #-}

-- {-# OPTIONS -v tc.term.lambda:30 #-}

open import Agda.Builtin.Cubical.Path

postulate
  A E : Set
  a : A

data C : Set where
  c : E → C

p : a ≡ a
p = λ (c e) → a

-- WAS: accepted.

-- Expected error:
-- Patterns are not allowed in Path-lambdas
-- when checking that the expression λ .patternInTele0 @ (c e) → a has type a ≡ a


text:
{- Reported by Nils Anders Danielsson, 2011-07-06

From the release notes for Agda 2.2.10:

  "Projections now preserve sizes, both in patterns and expressions."

However, the following code is rejected:
-}

module Issue425 where

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

open _×_

id : {A : Set} → A → A
id x = x

data I : Set where
  c : I → I → I

data D : I → Set where
  d : (j : I × I)  → D (proj₁ j) → D (proj₂ j) → D (c (proj₁ j) (proj₂ j))

f : ∀ i → D i → Set
f .(c (proj₁ j) (proj₂ j)) (d j l r) = f (proj₁ j) (id l)

{- Is this intentional? I guess the issue here is the subterm relation
rather than the sizes. Should we modify the subterm relation?
-}
-- Andreas, 2011-07-07 this should termination check.


text:
module Structure.Category.Functor.Functors where

import      Functional as Fn
open import Function.Proofs
open import Logic.Predicate
import      Lvl
open import Structure.Category
open import Structure.Category.Functor
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₒ ℓₘ ℓₑ ℓₗₑ ℓᵣₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ : Lvl.Level
private variable Obj Obj₁ Obj₂ Obj₃ : Type{ℓ}
private variable Morphism Morphism₁ Morphism₂ Morphism₃ : Obj → Obj → Type{ℓ}

module Raw where
  constᶠᵘⁿᶜᵗᵒʳ : Obj₂ → (Obj₁ → Obj₂)
  constᶠᵘⁿᶜᵗᵒʳ = Fn.const

  idᶠᵘⁿᶜᵗᵒʳ : Obj → Obj
  idᶠᵘⁿᶜᵗᵒʳ = Fn.id

  _∘ᶠᵘⁿᶜᵗᵒʳ_ : (Obj₂ → Obj₃) → (Obj₁ → Obj₂) → (Obj₁ → Obj₃)
  _∘ᶠᵘⁿᶜᵗᵒʳ_ = Fn._∘_

  infixl 10000 _∘ᶠᵘⁿᶜᵗᵒʳ_

module _
  ⦃ morphism-equivₗ : ∀{x y : Obj₁} → Equiv{ℓₗₑ}(Morphism₁ x y) ⦄
  ⦃ morphism-equivᵣ : ∀{x y : Obj₂} → Equiv{ℓᵣₑ}(Morphism₂ x y) ⦄
  {Category₁ : Category(Morphism₁)}
  {Category₂ : Category(Morphism₂)}
  where

  module _ where
    private open module Equivₗ {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equivₗ{x}{y} ⦄) using ()
    private open module Equivᵣ {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equivᵣ{x}{y} ⦄) using ()
    open Category ⦃ … ⦄
    open Functor
    open Raw

    private instance _ = Category₁
    private instance _ = Category₂

    -- A constant functor maps every object and morphism in a category to a single specified object and the identity morphism.
    constant : (objᵣ : Obj₂) → Functor(Category₁)(Category₂)(constᶠᵘⁿᶜᵗᵒʳ(objᵣ))
    map           (constant(objᵣ)) = Fn.const(id)
    op-preserving (constant(objᵣ)) = symmetry(_≡_) (Morphism.identityₗ(_∘_)(id))
    id-preserving (constant(objᵣ)) = reflexivity(_≡_)

module _
  ⦃ morphism-equiv : ∀{x y : Obj} → Equiv{ℓₑ}(Morphism x y) ⦄
  {Category : Category(Morphism)}
  where

  private open module [≡]-Equivalence {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equiv{x}{y} ⦄) using ()
  open Functor
  open Raw

  private instance _ = Category

  identity : Endofunctor(Category)(idᶠᵘⁿᶜᵗᵒʳ)
  map           (identity) = Fn.id
  op-preserving (identity) = reflexivity(_≡_)
  id-preserving (identity) = reflexivity(_≡_)

module _
  ⦃ morphism-equiv₁ : ∀{x y : Obj₁} → Equiv{ℓₑ₁}(Morphism₁ x y) ⦄
  ⦃ morphism-equiv₂ : ∀{x y : Obj₂} → Equiv{ℓₑ₂}(Morphism₂ x y) ⦄
  ⦃ morphism-equiv₃ : ∀{x y : Obj₃} → Equiv{ℓₑ₃}(Morphism₃ x y) ⦄
  {Category₁ : Category(Morphism₁)}
  {Category₂ : Category(Morphism₂)}
  {Category₃ : Category(Morphism₃)}
  where

  private open module Equiv₃ {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equiv₃{x}{y} ⦄) using ()
  open Category ⦃ … ⦄
  open Functor
  open Raw

  private instance _ = Category₁
  private instance _ = Category₂
  private instance _ = Category₃

  composition :
    ∀{F₂₃}{F₁₂}
    → (functor₂₃ : Functor(Category₂)(Category₃)(F₂₃))
    → (functor₁₂ : Functor(Category₁)(Category₂)(F₁₂))
    → Functor(Category₁)(Category₃)(F₂₃ ∘ᶠᵘⁿᶜᵗᵒʳ F₁₂)

  map              (composition{F₂₃}{F₁₂}(functor₂₃)(functor₁₂)){x}{y} = (map(functor₂₃){F₁₂(x)}{F₁₂(y)}) Fn.∘ (map(functor₁₂){x}{y})
  map-function     (composition{F₂₃}{F₁₂}(functor₂₃)(functor₁₂)) = [∘]-function ⦃ func-f = map-function(functor₂₃) ⦄ ⦃ func-g = map-function(functor₁₂) ⦄
  op-preserving    (composition{F₂₃}{F₁₂}(functor₂₃)(functor₁₂)){x}{y}{z} {f}{g} =
    map(functor₂₃) (map(functor₁₂) (f ∘ g))                               🝖-[ congruence₁(map(functor₂₃)) (op-preserving(functor₁₂)) ]
    map(functor₂₃) (map(functor₁₂) f ∘ map functor₁₂ g)                   🝖-[ op-preserving(functor₂₃)]
    map(functor₂₃) (map(functor₁₂) f) ∘ map(functor₂₃) (map(functor₁₂) g) 🝖-end
  id-preserving    (composition{F₂₃}{F₁₂}(functor₂₃)(functor₁₂)) {x} =
    map(functor₂₃) (map(functor₁₂) id) 🝖-[ congruence₁(_) (id-preserving(functor₁₂)) ]
    map(functor₂₃) id                  🝖-[ id-preserving(functor₂₃) ]
    id                                 🝖-end

module Wrapped where
  open CategoryObject

  private variable A B C : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}

  constᶠᵘⁿᶜᵗᵒʳ : let _ = A in Object(B) → (A →ᶠᵘⁿᶜᵗᵒʳ B)
  ∃.witness (constᶠᵘⁿᶜᵗᵒʳ c) = Raw.constᶠᵘⁿᶜᵗᵒʳ c
  ∃.proof   (constᶠᵘⁿᶜᵗᵒʳ c) = constant c

  idᶠᵘⁿᶜᵗᵒʳ : A →ᶠᵘⁿᶜᵗᵒʳ A
  ∃.witness idᶠᵘⁿᶜᵗᵒʳ = Raw.idᶠᵘⁿᶜᵗᵒʳ
  ∃.proof   idᶠᵘⁿᶜᵗᵒʳ = identity

  _∘ᶠᵘⁿᶜᵗᵒʳ_ : let _ = A ; _ = B ; _ = C in (B →ᶠᵘⁿᶜᵗᵒʳ C) → (A →ᶠᵘⁿᶜᵗᵒʳ B) → (A →ᶠᵘⁿᶜᵗᵒʳ C)
  ∃.witness (_∘ᶠᵘⁿᶜᵗᵒʳ_ ([∃]-intro F)               ([∃]-intro G))               = Raw._∘ᶠᵘⁿᶜᵗᵒʳ_ F G
  ∃.proof   (_∘ᶠᵘⁿᶜᵗᵒʳ_ ([∃]-intro _ ⦃ F-functor ⦄) ([∃]-intro _ ⦃ G-functor ⦄)) = composition F-functor G-functor

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:
open import Everything

module Test.UnifiesSubstitunction {𝔭} (𝔓 : Ø 𝔭) where

  open Substitunction 𝔓
  open Term 𝔓
  open Substitist 𝔓

  ≡-Unifies₀-Term : ∀ {m} → Term m → Term m → Ṗroperty ∅̂ (Arrow Fin Term m)
  ≡-Unifies₀-Term = ≡-surjcollation

  ≡-Unifies₀-Term' : ∀ {m} → Term m → Term m → Ṗroperty ∅̂ (Arrow Fin Term m)
  ≡-Unifies₀-Term' = ≡-surjcollation[ Term ]⟦ Substitunction ⟧

  ≡-Unifies₀-Terms : ∀ {N m} → Terms N m → Terms N m → Ṗroperty ∅̂ (Arrow Fin Term m)
  ≡-Unifies₀-Terms = λ x → ≡-surjcollation x

  ≡-ExtensionalUnifies-Term : ∀ {m} → Term m → Term m → ArrowExtensionṖroperty ∅̂ Fin Term _≡_ m
  ≡-ExtensionalUnifies-Term = Surjextenscollation.method Substitunction _≡̇_

  ≡-ExtensionalUnifies-Terms : ∀ {N m} → Terms N m → Terms N m → LeftExtensionṖroperty ∅̂ (Arrow Fin Term) (Pointwise Proposequality) m
  ≡-ExtensionalUnifies-Terms = surjextenscollation⟦ Pointwise _≡_ ⟧


text:
-- Modified: Andreas, 2011-04-11 freezing Metas
module HereditarilySingletonRecord where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

-- * trivial unit type

record Singleton : Set where

foo : Singleton
foo = _

-- * product of unit types

record HereditarilySingleton : Set where
  field
    singleton      : Singleton
    also-singleton : Singleton

bar : HereditarilySingleton
bar = _

-- * hiding the unit types behind a type case

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

Unit : ℕ → Set
Unit zero    = Singleton
Unit (suc n) = Unit n

mutual -- needed to avoid freezing

  one : ℕ
  one = _

  record HereditarilySingleton₂ : Set where
    field
      singleton : Unit one

  baz : HereditarilySingleton₂
  baz = _

  force : one ≡ suc zero
  force = refl


text:
-- Andreas, 2018-11-15, issue #3394 and testcase by Guillaume Brunerie
--
-- Internal error in termination checking the type of Ploop
-- due to uninitialized terSizeDepth.

postulate
  A : Set
  B : Set
  P : B → Set

mutual
  loop  : A → B → B
  loop a b = loop a b

  Ploop : (b : B) → P (loop _ b)  -- Unsolved meta caused internal error
  Ploop b = whatever
    where postulate whatever : _

-- Should fail termination checking in a controlled fashion.


text:
{- defining Nat as a kind of List -}
-- the need for ‼ is unfortunate
module Oscar.Data2 where

record ⊤ : Set where
  constructor tt

-- List
data ⟦_⟧ {a} (A : Set a) : Set a where
  ∅ : ⟦ A ⟧
  _∷_ : A → ⟦ A ⟧ → ⟦ A ⟧

-- Nat
⟦⟧ = ⟦ ⊤ ⟧
pattern ‼ ⟦A⟧ = tt ∷ ⟦A⟧

-- Fin
data ⟦⟧[_] : ⟦⟧ → Set where
  ∅ : ∀ {n} → ⟦⟧[ ‼ n ]
  ! : ∀ {n} → ⟦⟧[ n ] → ⟦⟧[ ‼ n ]

test : ⟦⟧[ ‼ (‼ ∅) ]
test = ! ∅


text:
------------------------------------------------------------------------
-- Lemmas related to strong similarity for CCS
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude

module Similarity.CCS {ℓ} {Name : Type ℓ} where

open import Equality.Propositional
open import Prelude.Size

open import Function-universe equality-with-J hiding (id; _∘_)

import Bisimilarity.CCS as BL
import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning
open import Labelled-transition-system.CCS Name
import Similarity.Equational-reasoning-instances

open import Bisimilarity CCS as B using (_∼_; _∼′_)
open import Similarity CCS

------------------------------------------------------------------------
-- Congruence lemmas

private
  module CL {i} = BL.Cong-lemmas [ i ]_≤′_ challenge

mutual

  -- _∣_ preserves similarity.

  infix 6 _∣-cong_ _∣-cong′_

  _∣-cong_ : ∀ {i P P′ Q Q′} →
             [ i ] P ≤ P′ → [ i ] Q ≤ Q′ → [ i ] P ∣ Q ≤ P′ ∣ Q′
  P≤P′ ∣-cong Q≤Q′ = ⟨ CL.∣-cong _∣-cong′_ P≤P′ Q≤Q′ ⟩

  _∣-cong′_ : ∀ {i P P′ Q Q′} →
              [ i ] P ≤′ P′ → [ i ] Q ≤′ Q′ → [ i ] P ∣ Q ≤′ P′ ∣ Q′
  force (P≤P′ ∣-cong′ Q≤Q′) = force P≤P′ ∣-cong force Q≤Q′

-- _⊕_ preserves similarity.

infix 8 _⊕-cong_ _⊕-cong′_

_⊕-cong_ : ∀ {i P P′ Q Q′} →
           [ i ] P ≤ P′ → [ i ] Q ≤ Q′ → [ i ] P ⊕ Q ≤ P′ ⊕ Q′
P≤P′ ⊕-cong Q≤Q′ = ⟨ CL.⊕-cong P≤P′ Q≤Q′ ⟩

_⊕-cong′_ : ∀ {i P P′ Q Q′} →
            [ i ] P ≤′ P′ → [ i ] Q ≤′ Q′ → [ i ] P ⊕ Q ≤′ P′ ⊕ Q′
force (P≤P′ ⊕-cong′ Q≤Q′) = force P≤P′ ⊕-cong force Q≤Q′

-- _·_ preserves similarity.

infix 12 _·-cong_ _·-cong′_

_·-cong_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] force P ≤′ force P′ → [ i ] μ · P ≤ μ′ · P′
_·-cong_ {i} refl P≤P′ = ⟨ CL.·-cong {i = i} P≤P′ ⟩

_·-cong′_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] force P ≤′ force P′ → [ i ] μ · P ≤′ μ′ · P′
force (μ≡μ′ ·-cong′ P≤P′) = μ≡μ′ ·-cong P≤P′

-- _∙_ preserves similarity.

infix 12 _∙-cong_ _∙-cong′_

_∙-cong_ : ∀ {i μ μ′ P P′} →
           μ ≡ μ′ → [ i ] P ≤ P′ → [ i ] μ ∙ P ≤ μ′ ∙ P′
refl ∙-cong P≤P′ = refl ·-cong convert {a = ℓ} P≤P′

_∙-cong′_ : ∀ {i μ μ′ P P′} →
            μ ≡ μ′ → [ i ] P ≤′ P′ → [ i ] μ ∙ P ≤′ μ′ ∙ P′
force (μ≡μ′ ∙-cong′ P≤P′) = μ≡μ′ ∙-cong force P≤P′

-- _∙ turns equal actions into similar processes.

infix 12 _∙-cong _∙-cong′

_∙-cong : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ≤ μ′ ∙
refl ∙-cong = reflexive

_∙-cong′ : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ≤′ μ′ ∙
refl ∙-cong′ = reflexive

mutual

  -- ⟨ν_⟩ preserves similarity.

  ⟨ν_⟩-cong : ∀ {i a a′ P P′} →
              a ≡ a′ → [ i ] P ≤ P′ → [ i ] ⟨ν a ⟩ P ≤ ⟨ν a′ ⟩ P′
  ⟨ν refl ⟩-cong P≤P′ = ⟨ CL.⟨ν⟩-cong ⟨ν refl ⟩-cong′ P≤P′ ⟩

  ⟨ν_⟩-cong′ : ∀ {i a a′ P P′} →
               a ≡ a′ → [ i ] P ≤′ P′ → [ i ] ⟨ν a ⟩ P ≤′ ⟨ν a′ ⟩ P′
  force (⟨ν a≡a′ ⟩-cong′ P≤P′) = ⟨ν a≡a′ ⟩-cong (force P≤P′)

mutual

  -- !_ preserves similarity.

  infix 10 !-cong_ !-cong′_

  !-cong_ : ∀ {i P P′} →
            [ i ] P ≤ P′ → [ i ] ! P ≤ ! P′
  !-cong P≤P′ = ⟨ CL.!-cong BL.6-1-3-2 _∣-cong′_ !-cong′_ P≤P′ ⟩

  !-cong′_ : ∀ {i P P′} → [ i ] P ≤′ P′ → [ i ] ! P ≤′ ! P′
  force (!-cong′ P≤P′) = !-cong force P≤P′

-- _[_] preserves similarity.

mutual

  infix 5 _[_]-cong _[_]-cong′

  _[_]-cong :
    ∀ {i n Ps Qs}
    (C : Context ∞ n) → (∀ x → [ i ] Ps x ≤ Qs x) →
    [ i ] C [ Ps ] ≤ C [ Qs ]
  hole x   [ Ps≤Qs ]-cong = Ps≤Qs x
  ∅        [ Ps≤Qs ]-cong = reflexive
  C₁ ∣ C₂  [ Ps≤Qs ]-cong = (C₁ [ Ps≤Qs ]-cong) ∣-cong (C₂ [ Ps≤Qs ]-cong)
  C₁ ⊕ C₂  [ Ps≤Qs ]-cong = (C₁ [ Ps≤Qs ]-cong) ⊕-cong (C₂ [ Ps≤Qs ]-cong)
  μ · C    [ Ps≤Qs ]-cong = refl ·-cong λ { .force → force C [ Ps≤Qs ]-cong }
  ⟨ν a ⟩ C [ Ps≤Qs ]-cong = ⟨ν refl ⟩-cong (C [ Ps≤Qs ]-cong)
  ! C      [ Ps≤Qs ]-cong = !-cong (C [ Ps≤Qs ]-cong)

  _[_]-cong′ :
    ∀ {i n Ps Qs}
    (C : Context ∞ n) → (∀ x → [ i ] Ps x ≤′ Qs x) →
    [ i ] C [ Ps ] ≤′ C [ Qs ]
  force (C [ Ps≤Qs ]-cong′) = C [ (λ x → force (Ps≤Qs x)) ]-cong

------------------------------------------------------------------------
-- Other results

-- P is similar to P ⊕ Q.

≤-⊕-left : ∀ {i P Q} → [ i ] P ≤ P ⊕ Q
≤-⊕-left = ⟨ (λ P⟶P′ → _ , sum-left P⟶P′ , reflexive) ⟩

-- Q is similar to P ⊕ Q.

≤-⊕-right : ∀ {i P Q} → [ i ] Q ≤ P ⊕ Q
≤-⊕-right = ⟨ (λ Q⟶Q′ → _ , sum-right Q⟶Q′ , reflexive) ⟩

-- If Name is inhabited, then there are two processes that are similar
-- in both directions, but not bisimilar.
--
-- I took this example from Wikipedia; I suspect that it is due to
-- Milner.

≤≥≁ : Name → ∃ λ P → ∃ λ Q → P ≤ Q × Q ≤ P × ¬ P ∼ Q
≤≥≁ x = machine₁ , machine₂
      , machine₁≤machine₂ , machine₂≤machine₁ , machine₁≁machine₂
  where

  -- Some names (with kinds), constructed using x.

  pay coffee tea : Name-with-kind

  pay    = x , true
  coffee = pay
  tea    = x , false

  -- Two vending machines.

  machine₁ machine₂ machine₁′ machine₂′ : Proc ∞

  machine₁′ = name pay ∙ (coffee ∙ ⊕ tea ∙)
  machine₁  = ! machine₁′

  machine₂′ = (name pay ∙ (coffee ∙) ⊕ name pay ∙ (tea ∙))
                ⊕
              machine₁′
  machine₂  = ! machine₂′

  -- A lemma.

  machine₁⟶ :
    ∀ {P μ} → machine₁ [ μ ]⟶ P →
    μ ≡ name pay × P ∼ machine₁ ∣ (coffee ∙ ⊕ tea ∙)
  machine₁⟶ tr = case BL.6-1-3-2 tr of λ where
    (inj₁ (_ , action , P∼))                 → refl , P∼
    (inj₂ (_ , _ , _ , _ , action , tr , _)) →
      ⊥-elim (names-are-not-inverted tr)

  -- The first machine is similar to the second one.

  machine₁≤machine₂ : ∀ {i} → [ i ] machine₁ ≤ machine₂
  machine₁≤machine₂ {i} =
    StepC.⟨ (λ {P} tr →
               case machine₁⟶ tr of λ where
                 (refl , P∼) →
                     _
                   , (machine₂                      [ name pay ]⟶⟨ replication (par-right (sum-right action)) ⟩
                      machine₂ ∣ coffee ∙ ⊕ tea ∙)
                   , (P                            ∼⟨ ≤: convert {a = ℓ} P∼ ⟩
                      machine₁ ∣ coffee ∙ ⊕ tea ∙  ∼⟨ machine₁≤′machine₂ ∣-cong′ (_ ■) ⟩■
                      machine₂ ∣ coffee ∙ ⊕ tea ∙))
          ⟩
    where
    machine₁≤′machine₂ : [ i ] machine₁ ≤′ machine₂
    force machine₁≤′machine₂ = machine₁≤machine₂

  -- The second machine is similar to the first one.

  machine₂≤machine₁ : ∀ {i} → [ i ] machine₂ ≤ machine₁
  machine₂≤machine₁ {i} = StepC.⟨ helper ∘ BL.6-1-3-2 ⟩
    where
    machine₂≤′machine₁ : [ i ] machine₂ ≤′ machine₁
    force machine₂≤′machine₁ = machine₂≤machine₁

    lemma =
      machine₁                     [ name pay ]⟶⟨ replication (par-right action) ⟩
      machine₁ ∣ coffee ∙ ⊕ tea ∙

    helper :
      ∀ {P μ} →
      (∃ λ P′ → machine₂′ [ μ ]⟶ P′ × P ∼ machine₂ ∣ P′)
        ⊎
      (μ ≡ τ × ∃ λ P′ → ∃ λ P″ → ∃ λ a →
       machine₂′ [ name a ]⟶ P′ × machine₂′ [ name (co a) ]⟶ P″ ×
       P ∼ (machine₂ ∣ P′) ∣ P″) →
      ∃ λ Q → machine₁ [ μ ]⟶ Q × [ i ] P ≤′ Q
    helper {P} (inj₁ (_ , sum-left (sum-left action) , P∼)) =
        _
      , lemma
      , (P                            ∼⟨ ≤: convert {a = ℓ} P∼ ⟩
         machine₂ ∣ coffee ∙          ∼⟨ machine₂≤′machine₁ ∣-cong′ convert {a = ℓ} ≤-⊕-left ⟩■
         machine₁ ∣ coffee ∙ ⊕ tea ∙)

    helper {P} (inj₁ (_ , sum-left (sum-right action) , P∼)) =
        _
      , lemma
      , (P                            ∼⟨ ≤: convert {a = ℓ} P∼ ⟩
         machine₂ ∣ tea ∙             ∼⟨ machine₂≤′machine₁ ∣-cong′ convert {a = ℓ} ≤-⊕-right ⟩■
         machine₁ ∣ coffee ∙ ⊕ tea ∙)

    helper {P} (inj₁ (_ , sum-right action , P∼)) =
        _
      , lemma
      , (P                            ∼⟨ ≤: convert {a = ℓ} P∼ ⟩
         machine₂ ∣ coffee ∙ ⊕ tea ∙  ∼⟨ machine₂≤′machine₁ ∣-cong′ (_ ■) ⟩■
         machine₁ ∣ coffee ∙ ⊕ tea ∙)

    helper (inj₂ (_ , _ , _ , _ , sum-left (sum-left action)  , sum-left (sum-left tr)  , _)) = ⊥-elim (names-are-not-inverted tr)
    helper (inj₂ (_ , _ , _ , _ , sum-left (sum-left action)  , sum-left (sum-right tr) , _)) = ⊥-elim (names-are-not-inverted tr)
    helper (inj₂ (_ , _ , _ , _ , sum-left (sum-left action)  , sum-right tr            , _)) = ⊥-elim (names-are-not-inverted tr)
    helper (inj₂ (_ , _ , _ , _ , sum-left (sum-right action) , sum-left (sum-left tr)  , _)) = ⊥-elim (names-are-not-inverted tr)
    helper (inj₂ (_ , _ , _ , _ , sum-left (sum-right action) , sum-left (sum-right tr) , _)) = ⊥-elim (names-are-not-inverted tr)
    helper (inj₂ (_ , _ , _ , _ , sum-left (sum-right action) , sum-right tr            , _)) = ⊥-elim (names-are-not-inverted tr)
    helper (inj₂ (_ , _ , _ , _ , sum-right action            , sum-left (sum-left tr)  , _)) = ⊥-elim (names-are-not-inverted tr)
    helper (inj₂ (_ , _ , _ , _ , sum-right action            , sum-left (sum-right tr) , _)) = ⊥-elim (names-are-not-inverted tr)
    helper (inj₂ (_ , _ , _ , _ , sum-right action            , sum-right tr            , _)) = ⊥-elim (names-are-not-inverted tr)

  -- The two machines are not bisimilar.

  machine₁≁machine₂ : ¬ machine₁ ∼ machine₂
  machine₁≁machine₂ =
    machine₁ ∼ machine₂                                            ↝⟨ (λ hyp → B.right-to-left hyp
                                                                                (replication (par-right (sum-left (sum-left action))))) ⟩

    (∃ λ P → machine₁ [ name pay ]⟶ P × P ∼′ machine₂ ∣ coffee ∙)  ↝⟨ Σ-map id (Σ-map (proj₂ ∘ machine₁⟶) id) ⟩

    (∃ λ P → P ∼ machine₁ ∣ (coffee ∙ ⊕ tea ∙) ×
             P ∼′ machine₂ ∣ coffee ∙)                             ↝⟨ (λ { (_ , P∼ , P∼′) → transitive {a = ℓ} (symmetric P∼) (convert {a = ℓ} P∼′) }) ⟩

    machine₁ ∣ (coffee ∙ ⊕ tea ∙) ∼ machine₂ ∣ coffee ∙            ↝⟨ (λ hyp → Σ-map id proj₁ $
                                                                                B.left-to-right hyp (par-right (sum-right action))) ⟩

    (∃ λ P → machine₂ ∣ coffee ∙ [ name tea ]⟶ P)                  ↝⟨ helper ∘ proj₂ ⟩

    pay ≡ tea ⊎ coffee ≡ tea                                       ↝⟨ [ (λ ()) , (λ ()) ] ⟩□

    ⊥                                                              □
    where
    helper : ∀ {P} →
             machine₂ ∣ coffee ∙ [ name tea ]⟶ P →
             pay ≡ tea ⊎ coffee ≡ tea
    helper (par-right tr) = inj₂ $ cancel-name $ ·-only tr
    helper (par-left  tr) =
      inj₁ $ cancel-name $
        !-only (⊕-only (⊕-only ·-only ·-only) ·-only) tr

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
 {-# OPTIONS --type-in-type #-}

module RevisedHutton where

--********************************************
-- Prelude
--********************************************

-- Some preliminary stuffs, to avoid relying on the stdlib

--****************
-- Sigma and friends
--****************

data Sigma (A : Set) (B : A -> Set) : Set where
  _,_ : (x : A) (y : B x) -> Sigma A B

_*_ : (A : Set)(B : Set) -> Set
A * B = Sigma A \_ -> B

fst : {A : Set}{B : A -> Set} -> Sigma A B -> A
fst (a , _) = a

snd : {A : Set}{B : A -> Set} (p : Sigma A B) -> B (fst p)
snd (a , b) = b

data Zero : Set where
data Unit  : Set where
  Void : Unit

--****************
-- Sum and friends
--****************

data _+_ (A : Set)(B : Set) : Set where
  l : A -> A + B
  r : B -> A + B

--****************
-- Equality
--****************

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

subst : forall {x y} -> x == y -> x -> y
subst refl x = x

cong : {A B : Set}(f : A -> B){x y : A} -> x == y -> f x == f y
cong f refl = refl

cong2 : {A B C : Set}(f : A -> B -> C){x y : A}{z t : B} ->
        x == y -> z == t -> f x z == f y t
cong2 f refl refl = refl

postulate
  reflFun : {A B : Set}(f : A -> B)(g : A -> B)-> ((a : A) -> f a == g a) -> f == g

--****************
-- Meta-language
--****************

-- Note that we could define Nat, Bool, and the related operations in
-- IDesc. But it is awful to code with them, in Agda.

data Nat : Set where
  ze : Nat
  su : Nat -> Nat

data Bool : Set where
  true : Bool
  false : Bool

plus : Nat -> Nat -> Nat
plus ze n' = n'
plus (su n) n' = su (plus n n')

le : Nat -> Nat -> Bool
le ze _ = true
le (su _) ze = false
le (su n) (su n') = le n n'

data Vec (A : Set) : Nat -> Set where
   vnil : Vec A ze
   vcons : {n : Nat} -> A -> Vec A n -> Vec A (su n)

data Fin : Nat -> Set where
  fze : {n : Nat} -> Fin (su n)
  fsu : {n : Nat} -> Fin n -> Fin (su n)

--********************************************
-- Desc code
--********************************************

data IDesc (I : Set) : Set where
  var : I -> IDesc I
  const : Set -> IDesc I
  prod : IDesc I -> IDesc I -> IDesc I
  sigma : (S : Set) -> (S -> IDesc I) -> IDesc I
  pi : (S : Set) -> (S -> IDesc I) -> IDesc I

--********************************************
-- Desc interpretation
--********************************************

[|_|] : {I : Set} -> IDesc I -> (I -> Set) -> Set
[| var i |] P = P i
[| const X |] P = X
[| prod D D' |] P = [| D |] P * [| D' |] P
[| sigma S T |] P = Sigma S (\s -> [| T s |] P)
[| pi S T |] P = (s : S) -> [| T s |] P

--********************************************
-- Fixpoint construction
--********************************************

data IMu {I : Set}(R : I -> IDesc I)(i : I) : Set where
  con : [| R i |] (\j -> IMu R j) -> IMu R i

--********************************************
-- Predicate: All
--********************************************

All : {I : Set}(D : IDesc I)(P : I -> Set) -> [| D |] P -> IDesc (Sigma I P)
All (var i)     P x        = var (i , x)
All (const X)   P x        = const Unit
All (prod D D') P (d , d') = prod (All D P d) (All D' P d')
All (sigma S T) P (a , b)  = All (T a) P b
All (pi S T)    P f        = pi S (\s -> All (T s) P (f s))

--********************************************
-- Elimination principle: induction
--********************************************

module Elim {I : Set}
            (R : I -> IDesc I)
            (P : Sigma I (IMu R) -> Set)
            (m : (i : I)
                 (xs : [| R i |] (IMu R))
                 (hs : [| All (R i) (IMu R) xs |] P) ->
                 P ( i , con xs ))
       where

  mutual
    indI : (i : I)(x : IMu R i) -> P (i , x)
    indI i (con xs) = m i xs (hyps (R i) xs)

    hyps : (D : IDesc I) ->
           (xs : [| D |] (IMu R)) ->
           [| All D (IMu R) xs |] P
    hyps (var i) x = indI i x
    hyps (const X) x = Void
    hyps (prod D D') (d , d') =  hyps D d , hyps D' d'
    hyps (pi S R) f = \ s -> hyps (R s) (f s)
    hyps (sigma S R) ( a , b ) = hyps (R a) b

indI : {I : Set}
       (R : I -> IDesc I)
       (P : Sigma I (IMu R) -> Set)
       (m : (i : I)
            (xs : [| R i |] (IMu R))
            (hs : [| All (R i) (IMu R) xs |] P) ->
            P ( i , con xs)) ->
       (i : I)(x : IMu R i) -> P ( i , x )
indI = Elim.indI

--********************************************
-- Enumerations (hard-coded)
--********************************************

-- Unlike in Desc.agda, we don't carry the levitation of finite sets
-- here. We hard-code them and manipulate with standard Agda
-- machinery. Both presentation are isomorph but, in Agda, the coded
-- one quickly gets unusable.

data EnumU : Set where
  nilE : EnumU
  consE : EnumU -> EnumU

data EnumT : (e : EnumU) -> Set where
  EZe : {e : EnumU} -> EnumT (consE e)
  ESu : {e : EnumU} -> EnumT e -> EnumT (consE e)

spi : (e : EnumU)(P : EnumT e -> Set) -> Set
spi nilE P = Unit
spi (consE e) P = P EZe * spi e (\e -> P (ESu e))

switch : (e : EnumU)(P : EnumT e -> Set)(b : spi e P)(x : EnumT e) -> P x
switch nilE P b ()
switch (consE e) P b EZe = fst b
switch (consE e) P b (ESu n) = switch e (\e -> P (ESu e)) (snd b) n

_++_ : EnumU -> EnumU -> EnumU
nilE ++ e' = e'
(consE e) ++ e' = consE (e ++ e')

-- A special switch, for tagged descriptions. Switching on a
-- concatenation of finite sets:
sswitch : (e : EnumU)(e' : EnumU)(P : Set)
       (b : spi e (\_ -> P))(b' : spi e' (\_ -> P))(x : EnumT (e ++ e')) -> P
sswitch nilE nilE P b b' ()
sswitch nilE (consE e') P b b' EZe = fst b'
sswitch nilE (consE e') P b b' (ESu n) = sswitch nilE e' P b (snd b') n
sswitch (consE e) e' P b b' EZe = fst b
sswitch (consE e) e' P b b' (ESu n) = sswitch e e' P (snd b) b' n

--********************************************
-- Tagged indexed description
--********************************************

FixMenu : Set -> Set
FixMenu I = Sigma EnumU (\e -> (i : I) -> spi e (\_ -> IDesc I))

SensitiveMenu : Set -> Set
SensitiveMenu I = Sigma (I -> EnumU) (\F -> (i : I) -> spi (F i) (\_ -> IDesc I))

TagIDesc : Set -> Set
TagIDesc I = FixMenu I * SensitiveMenu I

toIDesc : (I : Set) -> TagIDesc I -> (I -> IDesc I)
toIDesc I ((E , ED) , (F , FD)) i = sigma (EnumT (E ++ F i))
                                          (\x -> sswitch E (F i) (IDesc I) (ED i) (FD i) x)

--********************************************
-- Catamorphism
--********************************************

cata : (I : Set)
       (R : I -> IDesc I)
       (T : I -> Set) ->
       ((i : I) -> [| R i |] T -> T i) ->
       (i : I) -> IMu R i -> T i
cata I R T phi i x = indI R (\it -> T (fst it)) (\i xs ms -> phi i (replace (R i) T xs ms)) i x
  where replace : (D : IDesc I)(T : I -> Set)
                  (xs : [| D |] (IMu R))
                  (ms : [| All D (IMu R) xs |] (\it -> T (fst it))) ->
                  [| D |] T
        replace (var i) T x y = y
        replace (const Z) T z z' = z
        replace (prod D D') T (x , x') (y , y') = replace D T x y , replace D' T x' y'
        replace (sigma A B) T (a , b) t = a , replace (B a) T b t
        replace (pi A B) T f t = \s -> replace (B s) T (f s) (t s)

--********************************************
-- Hutton's razor
--********************************************

--********************************
-- Types code
--********************************

data Type : Set where
  nat : Type
  bool : Type
  pair : Type -> Type -> Type

--********************************************
-- Free monad construction
--********************************************

_**_ : {I : Set} (R : TagIDesc I)(X : I -> Set) -> TagIDesc I
((E , ED) , FFD) ** X = ((( consE E ,  \ i -> ( const (X i) , ED i ))) , FFD)

--********************************************
-- Substitution
--********************************************

apply : {I : Set}
        (R : TagIDesc I)(X Y : I -> Set) ->
        ((i : I) -> X i -> IMu (toIDesc I (R ** Y)) i) ->
        (i : I) ->
        [| toIDesc I (R ** X) i |] (IMu (toIDesc I (R ** Y))) ->
        IMu (toIDesc I (R ** Y)) i
apply (( E , ED) , (F , FD)) X Y sig i (EZe , x) = sig i x
apply (( E , ED) , (F , FD)) X Y sig i (ESu n , t) = con (ESu n , t)

substI : {I : Set} (X Y : I -> Set)(R : TagIDesc I)
         (sigma : (i : I) -> X i -> IMu (toIDesc I (R ** Y)) i)
         (i : I)(D : IMu (toIDesc I (R ** X)) i) ->
         IMu (toIDesc I (R ** Y)) i
substI {I} X Y R sig i term = cata I (toIDesc I (R ** X)) (IMu (toIDesc I (R ** Y))) (apply R X Y sig) i term

--********************************************
-- Hutton's razor is free monad
--********************************************

-- Fix menu:
exprFreeFixMenu : FixMenu Type
exprFreeFixMenu = ( consE nilE ,
                    \ty -> (prod (var bool) (prod (var ty) (var ty)), -- if b then t1 else t2
                           Void))

-- Index-dependent menu:
choiceFreeMenu : Type -> EnumU
choiceFreeMenu nat = consE nilE
choiceFreeMenu bool = consE nilE
choiceFreeMenu (pair x y) = nilE

choiceFreeDessert : (ty : Type) -> spi (choiceFreeMenu ty) (\ _ -> IDesc Type)
choiceFreeDessert nat = (prod (var nat) (var nat) , Void)     -- plus x y
choiceFreeDessert bool = (prod (var nat) (var nat) , Void )   -- le x y
choiceFreeDessert (pair x y) = Void

exprFreeSensitiveMenu : SensitiveMenu Type
exprFreeSensitiveMenu = ( choiceFreeMenu ,  choiceFreeDessert )

-- Tagged description of expressions
exprFree : TagIDesc Type
exprFree = exprFreeFixMenu , exprFreeSensitiveMenu

-- Free monadic expressions
exprFreeC : (Type -> Set) -> TagIDesc Type
exprFreeC X = exprFree ** X

--********************************
-- Closed terms
--********************************

Val : Type -> Set
Val nat = Nat
Val bool = Bool
Val (pair x y) = (Val x) * (Val y)

closeTerm : Type -> IDesc Type
closeTerm = toIDesc Type (exprFree ** Val)

--********************************
-- Closed term evaluation
--********************************

eval : {ty : Type} -> IMu closeTerm ty -> Val ty
eval {ty} term = cata Type closeTerm Val evalOneStep ty term
        where evalOneStep : (ty : Type) -> [| closeTerm ty |] Val -> Val ty
              evalOneStep _ (EZe , t) = t
              evalOneStep _ ((ESu EZe) , (true , ( x , _))) = x
              evalOneStep _ ((ESu EZe) , (false , ( _ , y ))) = y
              evalOneStep nat ((ESu (ESu EZe)) , (x , y)) = plus x y
              evalOneStep nat ((ESu (ESu (ESu ()))) , t)
              evalOneStep bool ((ESu (ESu EZe)) , (x , y) ) =   le x y
              evalOneStep bool ((ESu (ESu (ESu ()))) , _)
              evalOneStep (pair x y) (ESu (ESu ()) , _)

--********************************
-- [Open terms]
--********************************

-- A context is a snoc-list of types
-- put otherwise, a context is a type telescope
data Context : Set where
  [] : Context
  _,_ : Context -> Type -> Context

-- The environment realizes the context, having a value for each type
Env : Context -> Set
Env []      = Unit
Env (G , S)  = Env G * Val S

-- A typed-variable indexes into the context, obtaining a proof that
-- what we get is what you want (WWGIWYW)
Var : Context -> Type -> Set
Var []      T = Zero
Var (G , S) T = Var G T + (S == T)

-- The lookup gets into the context to extract the value
lookup : (G : Context) -> Env G -> (T : Type) -> Var G T -> Val T
lookup []        _       T ()
lookup (G , .T)  (g , t) T (r refl) = t
lookup (G , S)   (g , t) T (l x)    = lookup G g T x

-- Open term: holes are either values or variables in a context
openTerm : Context -> Type -> IDesc Type
openTerm c = toIDesc Type (exprFree ** (\ty -> Val ty + Var c ty))

--********************************
-- Evaluation of open terms
--********************************

-- |discharge| is the local substitution expected by |substI|. It is
-- just sugar around context lookup
discharge : (context : Context) ->
            Env context ->
            (ty : Type) ->
            (Val ty + Var context ty) ->
            IMu closeTerm ty
discharge ctxt env ty (l value) = con (EZe , value)
discharge ctxt env ty (r variable) = con (EZe , lookup ctxt env ty variable )

-- |substExpr| is the specialized |substI| to expressions. We get it
-- generically from the free monad construction.
substExpr : {ty : Type}
            (context : Context)
            (sigma : (ty : Type) ->
                     (Val ty + Var context ty) ->
                     IMu closeTerm ty) ->
            IMu (openTerm context) ty ->
            IMu closeTerm ty
substExpr {ty} c sig term =
    substI (\ty -> Val ty + Var c ty) Val exprFree sig ty term

-- By first doing substitution to close the term, we can use
-- evaluation of closed terms, obtaining evaluation of open terms
-- under a valid context.
evalOpen : {ty : Type}(context : Context) ->
           Env context ->
           IMu (openTerm context) ty ->
           Val ty
evalOpen ctxt env tm = eval (substExpr ctxt (discharge ctxt env) tm)

--********************************
-- Tests
--********************************

-- Test context:
-- V 0 :-> true, V 1 :-> 2, V 2 :-> ( false , 1 )
testContext : Context
testContext = (([] , bool) , nat) , pair bool nat
testEnv : Env testContext
testEnv = ((Void , true ) , su (su ze)) , (false , su ze)

-- V 1
test1 : IMu (openTerm testContext) nat
test1 = con (EZe , r ( l (r refl) ) )

testSubst1 : IMu closeTerm nat
testSubst1 = substExpr testContext
                       (discharge testContext testEnv)
                       test1
-- = 2
testEval1 : Val nat
testEval1 = evalOpen testContext testEnv test1

-- add 1 (V 1)
test2 : IMu (openTerm testContext) nat
test2 = con (ESu (ESu EZe) , (con (EZe , l (su ze)) , con ( EZe , r (l (r refl)) )) )

testSubst2 : IMu closeTerm nat
testSubst2 = substExpr testContext
                       (discharge testContext testEnv)
                        test2

-- = 3
testEval2 : Val nat
testEval2 = evalOpen testContext testEnv test2

-- if (V 0) then (V 1) else 0
test3 : IMu (openTerm testContext) nat
test3 = con (ESu EZe , (con (EZe , r (l (l (r refl)))) ,
                       (con (EZe , r (l (r refl))) ,
                        con (EZe , l ze))))

testSubst3 : IMu closeTerm nat
testSubst3 = substExpr testContext
                       (discharge testContext testEnv)
                       test3

-- = 2
testEval3 : Val nat
testEval3 = evalOpen testContext testEnv test3

-- V 2
test4 : IMu (openTerm testContext) (pair bool nat)
test4 = con (EZe , r ( r refl ) )

testSubst4 : IMu closeTerm (pair bool nat)
testSubst4 = substExpr testContext
                       (discharge testContext testEnv)
                       test4
-- = (false , 1)
testEval4 : Val (pair bool nat)
testEval4 = evalOpen testContext testEnv test4

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


text:
------------------------------------------------------------------------
-- Untyped kind/type/term equality in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Syntax.WeakEquality where

open import Data.Fin using (Fin; zero; suc; raise)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Relation
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.List using ([]; _∷_; _++_)
open import Data.Vec as Vec using ([])
open import Relation.Binary using (IsEquivalence; Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Relation.Binary.PropositionalEquality as P

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.SingleVariableSubstitution
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization

------------------------------------------------------------------------
-- Weak untyped kind/type/term equality.
--
-- A "weak" equality that identifies syntactically equal terms and
-- types in elimination form up to type/kind ascriptions in
-- abstractions (lambdas).
--
-- Certain commutation lemmas about hereditary substitution,
-- η-expansion and normalization of raw types do not hold on the nose
-- (i.e. up to α-equivalence) because type-directed η-expansion can
-- change domain annotations in type operator abstractions.  Since
-- untyped normalization involves some degree of η-expansion, the
-- order in which these operations are performed can affect the domain
-- annotations in the resulting raw type expressions.  This is not a
-- problem semantically because the two type expressions are
-- considered equal as types (by the type equality judgment).  But
-- proving the relevant commutation lemmas directly w.r.t. to type
-- equality is difficult because of the complexity of that judgment.
-- Instead, we introduce a separate equivalence relation, called "weak
-- equality", that is essentially α-equivalence modulo shape-equal
-- domain annotations.  The problematic commutation lemmas then all
-- hold weakly (i.e. up to weak equality, see the nf-/⟨⟩ lemma in the
-- FOmegaInt.Kinding.Simple.Normalization for example).  Weak equality
-- is much easier to work with and can be embedded into (canonical)
-- type equivalence (see the FOmegaInt.Kinding.Canonical.WeakEquality
-- module).

open Syntax

infix 4 _≋_ _≈_ _≈Hd_ _≈Sp_ _≈Asc_ _≈Ctx_ _⟨≈⟩_ _≈?_

mutual

  data _≋_ {n} : Kind Elim n → Kind Elim n → Set where
    ≋-Π : ∀ {j₁ j₂ k₁ k₂} → j₁ ≋ j₂ → k₁ ≋ k₂ → Π j₁ k₁ ≋ Π j₂ k₂
    ≋-⋯ : ∀ {a₁ a₂ b₁ b₂} → a₁ ≈ a₂ → b₁ ≈ b₂ → a₁ ⋯ b₁ ≋ a₂ ⋯ b₂

  data _≈_ {n} : Elim n → Elim n → Set where
    ≈-∙ : ∀ {a₁ a₂ bs₁ bs₂} → a₁ ≈Hd a₂ → bs₁ ≈Sp bs₂ → a₁ ∙ bs₁ ≈ a₂ ∙ bs₂

  data _≈Hd_ {n} : Head n → Head n → Set where
    ≈-var : ∀ x →                                           var x ≈Hd var x
    ≈-⊥   :                                                     ⊥ ≈Hd ⊥
    ≈-⊤   :                                                     ⊤ ≈Hd ⊤
    ≈-∀   : ∀ {k₁ k₂ a₁ a₂} → k₁ ≋ k₂         → a₁ ≈ a₂ → Π k₁ a₁ ≈Hd Π k₂ a₂
    ≈-→   : ∀ {a₁ a₂ b₁ b₂} → a₁ ≈ a₂         → b₁ ≈ b₂ → a₁ ⇒ b₁ ≈Hd a₂ ⇒ b₂
    ≈-Λ   : ∀ {k₁ k₂ a₁ a₂} → ⌊ k₁ ⌋ ≡ ⌊ k₂ ⌋ → a₁ ≈ a₂ → Λ k₁ a₁ ≈Hd Λ k₂ a₂
    ≈-λ   : ∀ {a₁ a₂ b₁ b₂}                   → b₁ ≈ b₂ → ƛ a₁ b₁ ≈Hd ƛ a₂ b₂
    ≈-⊡   : ∀ {a₁ a₂ b₁ b₂} → a₁ ≈ a₂         → b₁ ≈ b₂ → a₁ ⊡ b₁ ≈Hd a₂ ⊡ b₂

  data _≈Sp_ {n} : Spine n → Spine n → Set where
    ≈-[] :                                                   [] ≈Sp []
    ≈-∷  : ∀ {a₁ a₂ bs₁ bs₂} → a₁ ≈ a₂ → bs₁ ≈Sp bs₂ → a₁ ∷ bs₁ ≈Sp a₂ ∷ bs₂

data _≈Asc_ {n} : ElimAsc n → ElimAsc n → Set where
  ≈-kd : ∀ {k₁ k₂} → k₁ ≋ k₂ → kd k₁ ≈Asc kd k₂
  ≈-tp : ∀ {a₁ a₂} → a₁ ≈ a₂ → tp a₁ ≈Asc tp a₂

open ElimCtx hiding (_++_)

data _≈Ctx_ : ∀ {n} → Ctx n → Ctx n → Set where
  ≈-[] : [] ≈Ctx []
  ≈-∷  : ∀ {n a₁ a₂} {Γ₁ Γ₂ : Ctx n} →
         a₁ ≈Asc a₂ → Γ₁ ≈Ctx Γ₂ → a₁ ∷ Γ₁ ≈Ctx a₂ ∷ Γ₂

-- Weak equality of single-variable substations and results.

data _⟨≈⟩_ : ∀ {m n} → SVSub m n → SVSub m n → Set where
  ≈-sub : ∀ {n}   {a b : Elim n}    →  a ≈ b  → sub a ⟨≈⟩ sub b
  ≈-↑   : ∀ {m n} {σ τ : SVSub m n} → σ ⟨≈⟩ τ →   σ ↑ ⟨≈⟩ τ ↑

data _≈?_ {n} : SVRes n → SVRes n → Set where
  ≈-hit  : ∀ {a b : Elim n} → a ≈ b →  hit a ≈? hit b
  ≈-miss : ∀ (x : Fin n)            → miss x ≈? miss x

-- Shorthands.

≈-var∙ : ∀ {n} (x : Fin n) → var∙ x ≈ var∙ x
≈-var∙ x = ≈-∙ (≈-var x) ≈-[]

≈-⊥∙ : ∀ {n} → _≈_ {n = n} ⊥∙ ⊥∙
≈-⊥∙ = ≈-∙ (≈-⊥) ≈-[]

≈-⊤∙ : ∀ {n} → _≈_ {n = n} ⊤∙ ⊤∙
≈-⊤∙ = ≈-∙ (≈-⊤) ≈-[]

≈-∀∙ : ∀ {n} {k₁ k₂ : Kind Elim n} {a₁ a₂} →
       k₁ ≋ k₂ → a₁ ≈ a₂ → ∀∙ k₁ a₁ ≈ ∀∙ k₂ a₂
≈-∀∙ k₁≋k₂ a₁≈a₂ = ≈-∙ (≈-∀ k₁≋k₂ a₁≈a₂) ≈-[]

≈-⇒∙ : ∀ {n} {a₁ a₂ : Elim n} {b₁ b₂} →
       a₁ ≈ a₂ → b₁ ≈ b₂ → a₁ ⇒∙ b₁ ≈ a₂ ⇒∙ b₂
≈-⇒∙ a₁≈a₂ b₁≈b₂ = ≈-∙ (≈-→ a₁≈a₂ b₁≈b₂) ≈-[]

≈-Λ∙ : ∀ {n} {k₁ k₂ : Kind Elim n} {a₁ a₂} → ⌊ k₁ ⌋ ≡ ⌊ k₂ ⌋ → a₁ ≈ a₂ →
       Λ∙ k₁ a₁ ≈ Λ∙ k₂ a₂
≈-Λ∙ ⌊k₁⌋≡⌊k₂⌋ a₁≈a₂ = ≈-∙ (≈-Λ ⌊k₁⌋≡⌊k₂⌋ a₁≈a₂) ≈-[]

≈-λ∙ : ∀ {n} {a₁ a₂ : Elim n} {b₁ b₂} → b₁ ≈ b₂ → ƛ∙ a₁ b₁ ≈ ƛ∙ a₂ b₂
≈-λ∙ a₁≈a₂ = ≈-∙ (≈-λ a₁≈a₂) ≈-[]

≈-⊡∙ : ∀ {n} {a₁ a₂ : Elim n} {b₁ b₂} →
       a₁ ≈ a₂ → b₁ ≈ b₂ → a₁ ⊡∙ b₁ ≈ a₂ ⊡∙ b₂
≈-⊡∙ a₁≈a₂ b₁≈b₂ = ≈-∙ (≈-⊡ a₁≈a₂ b₁≈b₂) ≈-[]

------------------------------------------------------------------------
-- Simple properties of weake equality.

-- Some simple congruence rules w.r.t. operations on spines and
-- eliminations.

≈-++ : ∀ {n} {as₁ as₂ : Spine n} {bs₁ bs₂} →
       as₁ ≈Sp as₂ → bs₁ ≈Sp bs₂ → as₁ ++ bs₁ ≈Sp as₂ ++ bs₂
≈-++ ≈-[]                bs₁≈bs₂ = bs₁≈bs₂
≈-++ (≈-∷ a₁≈a₂ as₁≈as₂) bs₁≈bs₂ = ≈-∷ a₁≈a₂ (≈-++ as₁≈as₂ bs₁≈bs₂)

≈-∙∙ : ∀ {n} {a₁ a₂ : Elim n} {bs₁ bs₂} →
       a₁ ≈ a₂ → bs₁ ≈Sp bs₂ → a₁ ∙∙ bs₁ ≈ a₂ ∙∙ bs₂
≈-∙∙ (≈-∙ a₁≈a₂ as₁≈as₂) bs₁≈bs₂ = ≈-∙ a₁≈a₂ (≈-++ as₁≈as₂ bs₁≈bs₂)

≈-⌜·⌝ : ∀ {n} {a₁ a₂ : Elim n} {b₁ b₂} →
        a₁ ≈ a₂ → b₁ ≈ b₂ → a₁ ⌜·⌝ b₁ ≈ a₂ ⌜·⌝ b₂
≈-⌜·⌝ a₁≈a₂ b₁≈b₂ = ≈-∙∙ a₁≈a₂ (≈-∷ b₁≈b₂ ≈-[])

-- Weakly equal kinds have equal shapes.

≋-⌊⌋ : ∀ {n} {k₁ k₂ : Kind Elim n} → k₁ ≋ k₂ → ⌊ k₁ ⌋ ≡ ⌊ k₂ ⌋
≋-⌊⌋ (≋-Π j₁≋j₂ k₁≋k₂) = cong₂ _⇒_ (≋-⌊⌋ j₁≋j₂) (≋-⌊⌋ k₁≋k₂)
≋-⌊⌋ (≋-⋯ a₁≈a₂ b₁≈b₂) = refl

module _ where
  open SimpleCtx          using (kd; ⌊_⌋Asc)
  open ContextConversions using (⌊_⌋Ctx)

  -- Weakly equal ascriptions and contexts have equal shapes.

  ≈Asc-⌊⌋ : ∀ {n} {a₁ a₂ : ElimAsc n} → a₁ ≈Asc a₂ → ⌊ a₁ ⌋Asc ≡ ⌊ a₂ ⌋Asc
  ≈Asc-⌊⌋ (≈-kd k₁≋k₂) = cong kd (≋-⌊⌋ k₁≋k₂)
  ≈Asc-⌊⌋ (≈-tp a₁≈a₂) = refl

  ≈Ctx-⌊⌋ : ∀ {n} {Γ₁ Γ₂ : Ctx n} → Γ₁ ≈Ctx Γ₂ → ⌊ Γ₁ ⌋Ctx ≡ ⌊ Γ₂ ⌋Ctx
  ≈Ctx-⌊⌋ ≈-[]              = refl
  ≈Ctx-⌊⌋ (≈-∷ a₁≈a₂ Γ₁≈Γ₂) = cong₂ _∷_ (≈Asc-⌊⌋ a₁≈a₂) (≈Ctx-⌊⌋ Γ₁≈Γ₂)

-- Reflexivity of weak equality.

mutual

  ≋-refl : ∀ {n} (k : Kind Elim n) → k ≋ k
  ≋-refl (a ⋯ b) = ≋-⋯ (≈-refl a) (≈-refl b)
  ≋-refl (Π j k) = ≋-Π (≋-refl j) (≋-refl k)

  ≈-refl : ∀ {n} (a : Elim n) → a ≈ a
  ≈-refl (a ∙ as) = ≈-∙ (≈Hd-refl a) (≈Sp-refl as)

  ≈Hd-refl : ∀ {n} (a : Head n) → a ≈Hd a
  ≈Hd-refl (var x) = ≈-var x
  ≈Hd-refl ⊥       = ≈-⊥
  ≈Hd-refl ⊤       = ≈-⊤
  ≈Hd-refl (Π k a) = ≈-∀ (≋-refl k) (≈-refl a)
  ≈Hd-refl (a ⇒ b) = ≈-→ (≈-refl a) (≈-refl b)
  ≈Hd-refl (Λ k a) = ≈-Λ refl (≈-refl a)
  ≈Hd-refl (ƛ a b) = ≈-λ (≈-refl b)
  ≈Hd-refl (a ⊡ b) = ≈-⊡ (≈-refl a) (≈-refl b)

  ≈Sp-refl : ∀ {n} (as : Spine n) → as ≈Sp as
  ≈Sp-refl []       = ≈-[]
  ≈Sp-refl (a ∷ as) = ≈-∷ (≈-refl a) (≈Sp-refl as)

≈Asc-refl : ∀ {n} (a : ElimAsc n) → a ≈Asc a
≈Asc-refl (kd k) = ≈-kd (≋-refl k)
≈Asc-refl (tp a) = ≈-tp (≈-refl a)

≈Ctx-refl : ∀ {n} (Γ : Ctx n) → Γ ≈Ctx Γ
≈Ctx-refl []      = ≈-[]
≈Ctx-refl (a ∷ Γ) = ≈-∷ (≈Asc-refl a) (≈Ctx-refl Γ)

-- Transitivity of weak equality.

mutual

  ≋-trans : ∀ {n} {j k l : Kind Elim n} → j ≋ k → k ≋ l → j ≋ l
  ≋-trans (≋-Π j₁≋j₂ k₁≋k₂) (≋-Π j₂≋j₃ k₂≋k₃) =
    ≋-Π (≋-trans j₁≋j₂ j₂≋j₃) (≋-trans k₁≋k₂ k₂≋k₃)
  ≋-trans (≋-⋯ a₁≈a₂ b₁≈b₂) (≋-⋯ a₂≈a₃ b₂≈b₃) =
    ≋-⋯ (≈-trans a₁≈a₂ a₂≈a₃) (≈-trans b₁≈b₂ b₂≈b₃)

  ≈-trans : ∀ {n} {a b c : Elim n} → a ≈ b → b ≈ c → a ≈ c
  ≈-trans (≈-∙ a₁≈a₂ bs₁≈bs₂) (≈-∙ a₂≈a₃ bs₂≈bs₃) =
    ≈-∙ (≈Hd-trans a₁≈a₂ a₂≈a₃) (≈Sp-trans bs₁≈bs₂ bs₂≈bs₃)

  ≈Hd-trans : ∀ {n} {a b c : Head n} → a ≈Hd b → b ≈Hd c → a ≈Hd c
  ≈Hd-trans (≈-var x)         (≈-var .x)        = ≈-var x
  ≈Hd-trans ≈-⊥               ≈-⊥               = ≈-⊥
  ≈Hd-trans ≈-⊤               ≈-⊤               = ≈-⊤
  ≈Hd-trans (≈-∀ k₁≋k₂ a₁≈a₂) (≈-∀ k₂≋k₃ a₂≈a₃) =
    ≈-∀ (≋-trans k₁≋k₂ k₂≋k₃) (≈-trans a₁≈a₂ a₂≈a₃)
  ≈Hd-trans (≈-→ a₁≈a₂ b₁≈b₂) (≈-→ a₂≈a₃ b₂≈b₃) =
    ≈-→ (≈-trans a₁≈a₂ a₂≈a₃) (≈-trans b₁≈b₂ b₂≈b₃)
  ≈Hd-trans (≈-Λ ⌊k₁⌋≡⌊k₂⌋ a₁≈a₂) (≈-Λ ⌊k₂⌋≡⌊k₃⌋ a₂≈a₃) =
    ≈-Λ (trans ⌊k₁⌋≡⌊k₂⌋ ⌊k₂⌋≡⌊k₃⌋) (≈-trans a₁≈a₂ a₂≈a₃)
  ≈Hd-trans (≈-λ a₁≈a₂)       (≈-λ a₂≈a₃)       = ≈-λ (≈-trans a₁≈a₂ a₂≈a₃)
  ≈Hd-trans (≈-⊡ a₁≈a₂ b₁≈b₂) (≈-⊡ a₂≈a₃ b₂≈b₃) =
    ≈-⊡ (≈-trans a₁≈a₂ a₂≈a₃) (≈-trans b₁≈b₂ b₂≈b₃)

  ≈Sp-trans : ∀ {n} {as bs cs : Spine n} → as ≈Sp bs → bs ≈Sp cs → as ≈Sp cs
  ≈Sp-trans ≈-[]                ≈-[]                = ≈-[]
  ≈Sp-trans (≈-∷ a₁≈a₂ bs₁≈bs₂) (≈-∷ a₂≈a₃ bs₂≈bs₃) =
    ≈-∷ (≈-trans a₁≈a₂ a₂≈a₃) (≈Sp-trans bs₁≈bs₂ bs₂≈bs₃)

≈Asc-trans : ∀ {n} {a b c : ElimAsc n} → a ≈Asc b → b ≈Asc c → a ≈Asc c
≈Asc-trans (≈-kd k₁≋k₂) (≈-kd k₂≋k₃) = ≈-kd (≋-trans k₁≋k₂ k₂≋k₃)
≈Asc-trans (≈-tp a₁≈a₂) (≈-tp a₂≈a₃) = ≈-tp (≈-trans a₁≈a₂ a₂≈a₃)

≈Ctx-trans : ∀ {n} {Γ Δ E : Ctx n} → Γ ≈Ctx Δ → Δ ≈Ctx E → Γ ≈Ctx E
≈Ctx-trans ≈-[]              ≈-[]                = ≈-[]
≈Ctx-trans (≈-∷ a₁≈a₂ Γ₁≈Γ₂) (≈-∷ a₂≈a₃ Γ₂≈Γ₃) =
  ≈-∷ (≈Asc-trans a₁≈a₂ a₂≈a₃) (≈Ctx-trans Γ₁≈Γ₂ Γ₂≈Γ₃)

-- Symmetry of weak equality.

mutual

  ≋-sym : ∀ {n} {j k : Kind Elim n} → j ≋ k → k ≋ j
  ≋-sym (≋-⋯ a₁≈a₂ b₁≈b₂) = ≋-⋯ (≈-sym a₁≈a₂) (≈-sym b₁≈b₂)
  ≋-sym (≋-Π j₁≋j₂ k₁≋k₂) = ≋-Π (≋-sym j₁≋j₂) (≋-sym k₁≋k₂)

  ≈-sym : ∀ {n} {a b : Elim n} → a ≈ b → b ≈ a
  ≈-sym (≈-∙ a≈b as≈bs) = ≈-∙ (≈Hd-sym a≈b) (≈Sp-sym as≈bs)

  ≈Hd-sym : ∀ {n} {a b : Head n} → a ≈Hd b → b ≈Hd a
  ≈Hd-sym (≈-var x)             = ≈-var x
  ≈Hd-sym ≈-⊥                   = ≈-⊥
  ≈Hd-sym ≈-⊤                   = ≈-⊤
  ≈Hd-sym (≈-∀ k₁≋k₂ a₁≈a₂)     = ≈-∀ (≋-sym k₁≋k₂) (≈-sym a₁≈a₂)
  ≈Hd-sym (≈-→ a₁≈a₂ b₁≈b₂)     = ≈-→ (≈-sym a₁≈a₂) (≈-sym b₁≈b₂)
  ≈Hd-sym (≈-Λ ⌊k₁⌋≡⌊k₂⌋ a₁≈a₂) = ≈-Λ (sym ⌊k₁⌋≡⌊k₂⌋) (≈-sym a₁≈a₂)
  ≈Hd-sym (≈-λ a₁≈a₂)           = ≈-λ (≈-sym a₁≈a₂)
  ≈Hd-sym (≈-⊡ a₁≈a₂ b₁≈b₂)     = ≈-⊡ (≈-sym a₁≈a₂) (≈-sym b₁≈b₂)

  ≈Sp-sym : ∀ {n} {as bs : Spine n} → as ≈Sp bs → bs ≈Sp as
  ≈Sp-sym ≈-[]                = ≈-[]
  ≈Sp-sym (≈-∷ a₁≈a₂ as₁≈as₂) = ≈-∷ (≈-sym a₁≈a₂) (≈Sp-sym as₁≈as₂)

≈Asc-sym : ∀ {n} {a b : ElimAsc n} → a ≈Asc b → b ≈Asc a
≈Asc-sym (≈-kd j≋k) = ≈-kd (≋-sym j≋k)
≈Asc-sym (≈-tp a≈b) = ≈-tp (≈-sym a≈b)

≈Ctx-sym : ∀ {n} {Γ Δ : Ctx n} → Γ ≈Ctx Δ → Δ ≈Ctx Γ
≈Ctx-sym ≈-[]              = ≈-[]
≈Ctx-sym (≈-∷ a₁≈a₂ Γ₁≈Γ₂) = ≈-∷ (≈Asc-sym a₁≈a₂) (≈Ctx-sym Γ₁≈Γ₂)

-- Weak equality is an equivalence relation.

≋-isEquivalence : (n : ℕ) → IsEquivalence (_≋_ {n})
≋-isEquivalence n = record
  { refl  = λ {k} → ≋-refl k
  ; sym   = ≋-sym
  ; trans = ≋-trans
  }

≈-isEquivalence : (n : ℕ) → IsEquivalence (_≈_ {n})
≈-isEquivalence n = record
  { refl  = λ {k} → ≈-refl k
  ; sym   = ≈-sym
  ; trans = ≈-trans
  }

≈Hd-isEquivalence : (n : ℕ) → IsEquivalence (_≈Hd_ {n})
≈Hd-isEquivalence n = record
  { refl  = λ {k} → ≈Hd-refl k
  ; sym   = ≈Hd-sym
  ; trans = ≈Hd-trans
  }

≈Sp-isEquivalence : (n : ℕ) → IsEquivalence (_≈Sp_ {n})
≈Sp-isEquivalence n = record
  { refl  = λ {k} → ≈Sp-refl k
  ; sym   = ≈Sp-sym
  ; trans = ≈Sp-trans
  }

≈Asc-isEquivalence : (n : ℕ) → IsEquivalence (_≈Asc_ {n})
≈Asc-isEquivalence n = record
  { refl  = λ {k} → ≈Asc-refl k
  ; sym   = ≈Asc-sym
  ; trans = ≈Asc-trans
  }

≈Ctx-isEquivalence : (n : ℕ) → IsEquivalence (_≈Ctx_ {n})
≈Ctx-isEquivalence n = record
  { refl  = λ {k} → ≈Ctx-refl k
  ; sym   = ≈Ctx-sym
  ; trans = ≈Ctx-trans
  }

-- Kinds together with weak equality form a setoid.
≋-setoid : ℕ → Setoid _ _
≋-setoid n = record
  { Carrier       = Kind Elim n
  ; _≈_           = _≋_
  ; isEquivalence = ≋-isEquivalence n
  }

-- Types and terms together with weak equality form a setoid.

≈-setoid : ℕ → Setoid _ _
≈-setoid n = record
  { Carrier       = Elim n
  ; _≈_           = _≈_
  ; isEquivalence = ≈-isEquivalence n
  }

≈Hd-setoid : ℕ → Setoid _ _
≈Hd-setoid n = record
  { Carrier       = Head n
  ; _≈_           = _≈Hd_
  ; isEquivalence = ≈Hd-isEquivalence n
  }

≈Sp-setoid : ℕ → Setoid _ _
≈Sp-setoid n = record
  { Carrier       = Spine n
  ; _≈_           = _≈Sp_
  ; isEquivalence = ≈Sp-isEquivalence n
  }

≈Asc-setoid : ℕ → Setoid _ _
≈Asc-setoid n = record
  { Carrier       = ElimAsc n
  ; _≈_           = _≈Asc_
  ; isEquivalence = ≈Asc-isEquivalence n
  }

≈Ctx-setoid : ℕ → Setoid _ _
≈Ctx-setoid n = record
  { Carrier       = Ctx n
  ; _≈_           = _≈Ctx_
  ; isEquivalence = ≈Ctx-isEquivalence n
  }

-- Equational reasoning for weak equality.
module ≈-Reasoning {n : ℕ} where
  open SetoidReasoning (≈-setoid n) public
  module Kd = SetoidReasoning (≋-setoid n)
  module Hd = SetoidReasoning (≈Hd-setoid n)
  module Sp = SetoidReasoning (≈Sp-setoid n)
  module Asc = SetoidReasoning (≈Asc-setoid n)
  module Ctx = SetoidReasoning (≈Ctx-setoid n)

------------------------------------------------------------------------
-- Substitution lemmas for weak equality.

-- Renamings in weakly equal terms.
--
-- The substitution lemmas below establishe that renamings of
-- variables in kinds, heads, eliminations and spines preserve weak
-- equality:
--
--                                ≈
--                           a ------→ b
--                           |         |
--                       -/ρ |         | -/ρ
--                           ↓    ≈    ↓
--                          a/ρ ····→ b/ρ
--
-- where ρ is a renaming.
module Renaming where
  open Substitution
  module V = VarSubst

  mutual

    -- Renamings preserve weak equality.

    ≋-/Var : ∀ {m n k₁ k₂} →
             k₁ ≋ k₂ → (ρ : Sub Fin m n) → k₁ Kind′/Var ρ ≋ k₂ Kind′/Var ρ
    ≋-/Var (≋-Π j₁≋j₂ k₁≋k₂) ρ =
      ≋-Π (≋-/Var j₁≋j₂ ρ) (≋-/Var k₁≋k₂ (ρ V.↑))
    ≋-/Var (≋-⋯ a₁≈a₂ b₁≈b₂) ρ =
      ≋-⋯ (≈-/Var a₁≈a₂ ρ) (≈-/Var b₁≈b₂ ρ)

    ≈-/Var : ∀ {m n a₁ a₂} →
             a₁ ≈ a₂ → (ρ : Sub Fin m n) → a₁ Elim/Var ρ ≈ a₂ Elim/Var ρ
    ≈-/Var (≈-∙ a₁≈a₂ bs₁≈bs₂) ρ =
      ≈-∙∙ (≈Hd-/Var a₁≈a₂ ρ) (≈Sp-/Var bs₁≈bs₂ ρ)

    ≈Hd-/Var : ∀ {m n a₁ a₂} →
               a₁ ≈Hd a₂ → (ρ : Sub Fin m n) → a₁ Head/Var′ ρ ≈ a₂ Head/Var′ ρ
    ≈Hd-/Var (≈-var x)             ρ = ≈-var∙ (Vec.lookup ρ x)
    ≈Hd-/Var ≈-⊥                   ρ = ≈-⊥∙
    ≈Hd-/Var ≈-⊤                   ρ = ≈-⊤∙
    ≈Hd-/Var (≈-∀ k₁≋k₂ a₁≈a₂)     ρ =
      ≈-∀∙ (≋-/Var k₁≋k₂ ρ) (≈-/Var a₁≈a₂ (ρ V.↑))
    ≈Hd-/Var (≈-→ a₁≈a₂ b₁≈b₂)     ρ =
      ≈-⇒∙ (≈-/Var a₁≈a₂ ρ) (≈-/Var b₁≈b₂ ρ)
    ≈Hd-/Var (≈-Λ {k₁} {k₂} ⌊k₁⌋≡⌊k₂⌋ a₁≈a₂) ρ =
      ≈-Λ∙ (begin
             ⌊ k₁ Kind′/Var _ ⌋   ≡⟨ ⌊⌋-Kind′/Var k₁ ⟩
             ⌊ k₁ ⌋               ≡⟨ ⌊k₁⌋≡⌊k₂⌋ ⟩
             ⌊ k₂ ⌋               ≡⟨ sym (⌊⌋-Kind′/Var k₂) ⟩
             ⌊ k₂ Kind′/Var _ ⌋   ∎)
           (≈-/Var a₁≈a₂ (ρ V.↑))
      where open ≡-Reasoning
    ≈Hd-/Var (≈-λ a₁≈a₂)           ρ = ≈-λ∙ (≈-/Var a₁≈a₂ (ρ V.↑))
    ≈Hd-/Var (≈-⊡ a₁≈a₂ b₁≈b₂)     ρ =
      ≈-⊡∙ (≈-/Var a₁≈a₂ ρ) (≈-/Var b₁≈b₂ ρ)

    ≈Sp-/Var : ∀ {m n as₁ as₂} →
               as₁ ≈Sp as₂ → (ρ : Sub Fin m n) → as₁ //Var ρ ≈Sp as₂ //Var ρ
    ≈Sp-/Var ≈-[]                ρ = ≈-[]
    ≈Sp-/Var (≈-∷ a₁≈a₂ as₁≈as₂) ρ =
      ≈-∷ (≈-/Var a₁≈a₂ ρ) (≈Sp-/Var as₁≈as₂ ρ)

  ≈?-/Var : ∀ {m n r₁ r₂} →
            r₁ ≈? r₂ → (ρ : Sub Fin m n) → r₁ ?/Var ρ ≈? r₂ ?/Var ρ
  ≈?-/Var (≈-hit a₁≈a₂) ρ = ≈-hit (≈-/Var a₁≈a₂ ρ)
  ≈?-/Var (≈-miss x)    ρ = ≈-miss (Vec.lookup ρ x)

  ≈-weakenElim : ∀ {n} {a₁ a₂ : Elim n} →
                 a₁ ≈ a₂ → weakenElim a₁ ≈ weakenElim a₂
  ≈-weakenElim a₁≈a₂ = ≈-/Var a₁≈a₂ V.wk

  ≈-weakenSVRes : ∀ {n} {r₁ r₂ : SVRes n} →
                  r₁ ≈? r₂ → weakenSVRes r₁ ≈? weakenSVRes r₂
  ≈-weakenSVRes r₁≈r₂ = ≈?-/Var r₁≈r₂ V.wk

open Renaming

-- Look up a weak equation in a pair of pointwise weakly equal
-- single-variable substitutions.

⟨≈⟩-lookup : ∀ {m n σ₁} {σ₂ : SVSub m n} →
             σ₁ ⟨≈⟩ σ₂ → (x : Fin m) → lookupSV σ₁ x ≈? lookupSV σ₂ x
⟨≈⟩-lookup (≈-sub a₁≈a₂) zero    = ≈-hit a₁≈a₂
⟨≈⟩-lookup (≈-sub a₁≈a₂) (suc x) = ≈-miss x
⟨≈⟩-lookup (≈-↑ σ₁≈σ₂)   zero    = ≈-miss zero
⟨≈⟩-lookup (≈-↑ σ₁≈σ₂)   (suc x) = ≈-weakenSVRes (⟨≈⟩-lookup σ₁≈σ₂ x)

-- Weak equality lifted to hereditary substitutions.
--
-- The substitution lemmas below establishe that simoultaneous
-- hereditary substitutions of weakly equal types or terms in kinds,
-- heads, eliminations and spines preserve weak equality:
--
--                                ≈
--                           a ------- b
--                           |         |
--                      -/σ₁ |         | -/σ₂
--                           ↓    ≈    ↓
--                          a/σ₁ ···· b/σ₂
--
-- where σ₁ and σ₁ are weakly equal hereditary substitutions.

module WeakHereditarySubstitutionEquality where
  open Substitution hiding (_↑; sub)

  mutual

    -- Point-wise weakly equal hereditary substitutions preserve weak
    -- equality.

    ≋-/⟨⟩ : ∀ {k m n j₁ j₂} {σ₁ σ₂ : SVSub m n} →
            j₁ ≋ j₂ → σ₁ ⟨≈⟩ σ₂ → j₁ Kind/⟨ k ⟩ σ₁ ≋ j₂ Kind/⟨ k ⟩ σ₂
    ≋-/⟨⟩ (≋-Π j₁≋j₂ k₁≋k₂) σ₁≈σ₂ =
      ≋-Π (≋-/⟨⟩ j₁≋j₂ σ₁≈σ₂) (≋-/⟨⟩ k₁≋k₂ (≈-↑ σ₁≈σ₂))
    ≋-/⟨⟩ (≋-⋯ a₁≈a₂ b₁≈b₂) σ₁≈σ₂ =
      ≋-⋯ (≈-/⟨⟩ a₁≈a₂ σ₁≈σ₂) (≈-/⟨⟩ b₁≈b₂ σ₁≈σ₂)

    ≈-/⟨⟩ : ∀ {k m n a₁ a₂} {σ₁ σ₂ : SVSub m n} →
            a₁ ≈ a₂ → σ₁ ⟨≈⟩ σ₂ → a₁ /⟨ k ⟩ σ₁ ≈ a₂ /⟨ k ⟩ σ₂
    ≈-/⟨⟩ (≈-∙ (≈-var x) bs₁≈bs₂) σ₁≈σ₂ =
      ≈-?∙∙⟨⟩ _ (⟨≈⟩-lookup σ₁≈σ₂ x) (≈Sp-/⟨⟩ bs₁≈bs₂ σ₁≈σ₂)
    ≈-/⟨⟩ (≈-∙ ≈-⊥ bs₁≈bs₂) σ₁≈σ₂ = ≈-∙ ≈-⊥ (≈Sp-/⟨⟩ bs₁≈bs₂ σ₁≈σ₂)
    ≈-/⟨⟩ (≈-∙ ≈-⊤ bs₁≈bs₂) σ₁≈σ₂ = ≈-∙ ≈-⊤ (≈Sp-/⟨⟩ bs₁≈bs₂ σ₁≈σ₂)
    ≈-/⟨⟩ (≈-∙ (≈-∀ k₁≋k₂ a₁≈a₂) bs₁≈bs₂) σ₁≈σ₂ =
      ≈-∙ (≈-∀ (≋-/⟨⟩ k₁≋k₂ σ₁≈σ₂) (≈-/⟨⟩ a₁≈a₂ (≈-↑ σ₁≈σ₂)))
          (≈Sp-/⟨⟩ bs₁≈bs₂ σ₁≈σ₂)
    ≈-/⟨⟩ (≈-∙ (≈-→ a₁≈a₂ b₁≈b₂) cs₁≈cs₂) σ₁≈σ₂ =
      ≈-∙ (≈-→ (≈-/⟨⟩ a₁≈a₂ σ₁≈σ₂) (≈-/⟨⟩ b₁≈b₂ σ₁≈σ₂))
          (≈Sp-/⟨⟩ cs₁≈cs₂ σ₁≈σ₂)
    ≈-/⟨⟩ (≈-∙ (≈-Λ {k₁} {k₂} ⌊k₁⌋≡⌊k₂⌋ a₁≈a₂) bs₁≈bs₂) σ₁≈σ₂ =
      ≈-∙ (≈-Λ (begin
                 ⌊ k₁ Kind/⟨ _ ⟩ _ ⌋   ≡⟨ ⌊⌋-Kind/⟨⟩ k₁ ⟩
                 ⌊ k₁ ⌋                ≡⟨ ⌊k₁⌋≡⌊k₂⌋ ⟩
                 ⌊ k₂ ⌋                ≡⟨ sym (⌊⌋-Kind/⟨⟩ k₂) ⟩
                 ⌊ k₂ Kind/⟨ _ ⟩ _ ⌋   ∎)
               (≈-/⟨⟩ a₁≈a₂ (≈-↑ σ₁≈σ₂)))
          (≈Sp-/⟨⟩ bs₁≈bs₂ σ₁≈σ₂)
      where open ≡-Reasoning
    ≈-/⟨⟩ (≈-∙ (≈-λ a₁≈a₂) bs₁≈bs₂) σ₁≈σ₂ =
      ≈-∙ (≈-λ (≈-/⟨⟩ a₁≈a₂ (≈-↑ σ₁≈σ₂))) (≈Sp-/⟨⟩ bs₁≈bs₂ σ₁≈σ₂)
    ≈-/⟨⟩ (≈-∙ (≈-⊡ a₁≈a₂ b₁≈b₂) cs₁≈cs₂) σ₁≈σ₂ =
      ≈-∙ (≈-⊡ (≈-/⟨⟩ a₁≈a₂ σ₁≈σ₂) (≈-/⟨⟩ b₁≈b₂ σ₁≈σ₂))
          (≈Sp-/⟨⟩ cs₁≈cs₂ σ₁≈σ₂)

    ≈Sp-/⟨⟩ : ∀ {k m n as₁ as₂} {σ₁ σ₂ : SVSub m n} →
              as₁ ≈Sp as₂ → σ₁ ⟨≈⟩ σ₂ → as₁ //⟨ k ⟩ σ₁ ≈Sp as₂ //⟨ k ⟩ σ₂
    ≈Sp-/⟨⟩ ≈-[]                σ₁≈σ₂ = ≈-[]
    ≈Sp-/⟨⟩ (≈-∷ a₁≈a₂ as₁≈as₂) σ₁≈σ₂ =
      ≈-∷ (≈-/⟨⟩ a₁≈a₂ σ₁≈σ₂) (≈Sp-/⟨⟩ as₁≈as₂ σ₁≈σ₂)

    -- Weak equality is a congruence w.r.t reducing applications.

    ≈-?∙∙⟨⟩ : ∀ k {n} {r₁ r₂ : SVRes n} {as₁ as₂} →
              r₁ ≈? r₂ → as₁ ≈Sp as₂ → r₁ ?∙∙⟨ k ⟩ as₁ ≈ r₂ ?∙∙⟨ k ⟩ as₂
    ≈-?∙∙⟨⟩ k (≈-hit a₁≈a₂) as₁≈as₂ = ≈-∙∙⟨⟩ k a₁≈a₂ as₁≈as₂
    ≈-?∙∙⟨⟩ k (≈-miss x)    as₁≈as₂ = ≈-∙ (≈-var x) as₁≈as₂

    ≈-∙∙⟨⟩ : ∀ k {n} {a₁ a₂ : Elim n} {bs₁ bs₂} →
             a₁ ≈ a₂ → bs₁ ≈Sp bs₂ → a₁ ∙∙⟨ k ⟩ bs₁ ≈ a₂ ∙∙⟨ k ⟩ bs₂
    ≈-∙∙⟨⟩ k         a₁≈a₂ ≈-[]                = a₁≈a₂
    ≈-∙∙⟨⟩ ★         a₁≈a₂ (≈-∷ b₁≈b₂ bs₁≈bs₂) = ≈-∙∙ a₁≈a₂ (≈-∷ b₁≈b₂ bs₁≈bs₂)
    ≈-∙∙⟨⟩ (k₁ ⇒ k₂) a₁≈a₂ (≈-∷ b₁≈b₂ bs₁≈bs₂) =
      ≈-∙∙⟨⟩ k₂ (≈-⌜·⌝⟨⟩ (k₁ ⇒ k₂) a₁≈a₂ b₁≈b₂) bs₁≈bs₂

    ≈-⌜·⌝⟨⟩ : ∀ k {n} {a₁ a₂ : Elim n} {b₁ b₂} →
              a₁ ≈ a₂ → b₁ ≈ b₂ → a₁ ⌜·⌝⟨ k ⟩ b₁ ≈ a₂ ⌜·⌝⟨ k ⟩ b₂
    ≈-⌜·⌝⟨⟩ ★         a₁≈a₂                            b₁≈b₂ = ≈-⌜·⌝ a₁≈a₂ b₁≈b₂
    ≈-⌜·⌝⟨⟩ (k₁ ⇒ k₂) (≈-∙ a₁≈a₂ (≈-∷ b₁≈b₂ bs₁≈bs₂))  c₁≈c₂ =
      ≈-⌜·⌝ (≈-∙ a₁≈a₂ (≈-∷ b₁≈b₂ bs₁≈bs₂)) c₁≈c₂
    ≈-⌜·⌝⟨⟩ (k₁ ⇒ k₂) (≈-∙ (≈-Λ ⌊k₁⌋≡⌊k₂⌋ a₁≈a₂) ≈-[]) c₁≈c₂ =
      ≈-/⟨⟩ a₁≈a₂ (≈-sub c₁≈c₂)
    -- Degenerate cases.
    ≈-⌜·⌝⟨⟩ (k₁ ⇒ k₂) (≈-∙ ≈-⊥ ≈-[]) c₁≈c₂ = ≈-∙ ≈-⊥ (≈-∷ c₁≈c₂ ≈-[])
    ≈-⌜·⌝⟨⟩ (k₁ ⇒ k₂) (≈-∙ ≈-⊤ ≈-[]) c₁≈c₂ = ≈-∙ ≈-⊤ (≈-∷ c₁≈c₂ ≈-[])
    ≈-⌜·⌝⟨⟩ (k₁ ⇒ k₂) (≈-∙ (≈-var x) ≈-[])         c₁≈c₂ =
      ≈-∙ (≈-var x) (≈-∷ c₁≈c₂ ≈-[])
    ≈-⌜·⌝⟨⟩ (k₁ ⇒ k₂) (≈-∙ (≈-∀ j₁≋j₂ a₁≈a₂) ≈-[]) c₁≈c₂ =
      ≈-∙ (≈-∀ j₁≋j₂ a₁≈a₂) (≈-∷ c₁≈c₂ ≈-[])
    ≈-⌜·⌝⟨⟩ (k₁ ⇒ k₂) (≈-∙ (≈-→ a₁≈a₂ b₁≈b₂) ≈-[]) c₁≈c₂ =
      ≈-∙ (≈-→ a₁≈a₂ b₁≈b₂) (≈-∷ c₁≈c₂ ≈-[])
    ≈-⌜·⌝⟨⟩ (k₁ ⇒ k₂) (≈-∙ (≈-λ a₁≈a₂) ≈-[])       c₁≈c₂ =
      ≈-∙ (≈-λ a₁≈a₂) (≈-∷ c₁≈c₂ ≈-[])
    ≈-⌜·⌝⟨⟩ (k₁ ⇒ k₂) (≈-∙ (≈-⊡ a₁≈a₂ b₁≈b₂) ≈-[]) c₁≈c₂ =
      ≈-∙ (≈-⊡ a₁≈a₂ b₁≈b₂) (≈-∷ c₁≈c₂ ≈-[])

  -- A corollary.
  ≈-[∈] : ∀ {k n a₁ a₂} {b₁ b₂ : Elim n} →
          a₁ ≈ a₂ → b₁ ≈ b₂ → a₁ [ b₁ ∈ k ] ≈ a₂ [ b₂ ∈ k ]
  ≈-[∈] a₁≈a₂ b₁≈b₂ = ≈-/⟨⟩ a₁≈a₂ (≈-sub b₁≈b₂)

  -- Weak equality is a congruence w.r.t potentially reducing
  -- applications.
  ≈-↓⌜·⌝ : ∀ {n} {a₁ a₂ : Elim n} {b₁ b₂} → a₁ ≈ a₂ → b₁ ≈ b₂ →
                  a₁ ↓⌜·⌝ b₁ ≈ a₂ ↓⌜·⌝ b₂
  ≈-↓⌜·⌝ (≈-∙ a₁≈a₂ (≈-∷ b₁≈b₂ bs₁≈bs₂))  c₁≈c₂ =
    ≈-⌜·⌝ (≈-∙ a₁≈a₂ (≈-∷ b₁≈b₂ bs₁≈bs₂)) c₁≈c₂
  ≈-↓⌜·⌝ {_} {_} {_} {b₁} {b₂}
         (≈-∙ (≈-Λ {k₁} {k₂} {a₁} {a₂} ⌊k₁⌋≡⌊k₂⌋ a₁≈a₂) ≈-[]) c₁≈c₂ =
    begin
      a₁ [ b₁ ∈ ⌊ k₁ ⌋ ]   ≈⟨ ≈-/⟨⟩ a₁≈a₂ (≈-sub c₁≈c₂) ⟩
      a₂ [ b₂ ∈ ⌊ k₁ ⌋ ]   ≡⟨ cong (a₂ [ b₂ ∈_]) ⌊k₁⌋≡⌊k₂⌋ ⟩
      a₂ [ b₂ ∈ ⌊ k₂ ⌋ ]   ∎
    where open ≈-Reasoning
  -- Degenerate cases.
  ≈-↓⌜·⌝ (≈-∙ ≈-⊥ ≈-[]) c₁≈c₂ = ≈-∙ ≈-⊥ (≈-∷ c₁≈c₂ ≈-[])
  ≈-↓⌜·⌝ (≈-∙ ≈-⊤ ≈-[]) c₁≈c₂ = ≈-∙ ≈-⊤ (≈-∷ c₁≈c₂ ≈-[])
  ≈-↓⌜·⌝ (≈-∙ (≈-var x) ≈-[])         c₁≈c₂ =
    ≈-∙ (≈-var x) (≈-∷ c₁≈c₂ ≈-[])
  ≈-↓⌜·⌝ (≈-∙ (≈-∀ j₁≋j₂ a₁≈a₂) ≈-[]) c₁≈c₂ =
    ≈-∙ (≈-∀ j₁≋j₂ a₁≈a₂) (≈-∷ c₁≈c₂ ≈-[])
  ≈-↓⌜·⌝ (≈-∙ (≈-→ a₁≈a₂ b₁≈b₂) ≈-[]) c₁≈c₂ =
    ≈-∙ (≈-→ a₁≈a₂ b₁≈b₂) (≈-∷ c₁≈c₂ ≈-[])
  ≈-↓⌜·⌝ (≈-∙ (≈-λ a₁≈a₂) ≈-[])       c₁≈c₂ =
    ≈-∙ (≈-λ a₁≈a₂) (≈-∷ c₁≈c₂ ≈-[])
  ≈-↓⌜·⌝ (≈-∙ (≈-⊡ a₁≈a₂ b₁≈b₂) ≈-[]) c₁≈c₂ =
    ≈-∙ (≈-⊡ a₁≈a₂ b₁≈b₂) (≈-∷ c₁≈c₂ ≈-[])

open WeakHereditarySubstitutionEquality

module WeakEqEtaExpansion where
  private module TK = TrackSimpleKindsEtaExp
  open Substitution
  open SimpHSubstLemmas
  open ≈-Reasoning

  -- NOTE. The definition of the function ≈-η-exp′ in this module is
  -- structurally recursive in the *shape* parameter k, but *not* in
  -- the kinds (j₁ j₂ : Kind Elim n) because we need to weaken the
  -- domains j₁₁ and j₂₁ of the dependent kinds (j₁ = Π j₁₁ j₁₂) and
  -- (j₂ = Π j₂₁ j₂₂) in the arrow case.  The additional premises ⌊ j₁
  -- ⌋≡ k and ⌊ j₂ ⌋≡ k ensure that k is indeed the shape of the kinds
  -- j₁ and j₂.

  -- Weak equality is a congruence w.r.t. untyped η-expansion.
  --
  -- NOTE. We do *not* require the kinds j₁ and j₂ to be (weakly)
  -- equal, we only require them to have the same shape.

  ≈-η-exp′ : ∀ {n k j₁ j₂} {a₁ a₂ : Elim n}
             (hyp₁ : ⌊ j₁ ⌋≡ k) (hyp₂ : ⌊ j₂ ⌋≡ k) → a₁ ≈ a₂ →
             TK.η-exp j₁ hyp₁ a₁ ≈ TK.η-exp j₂ hyp₂ a₂
  ≈-η-exp′ (is-★) (is-★) a₁≈a₂ = a₁≈a₂
  ≈-η-exp′ (is-⇒ ⌊j₁⌋≡l₁ ⌊k₁⌋≡l₂) (is-⇒ ⌊j₂⌋≡l₁ ⌊k₂⌋≡l₂) a₁≈a₂ =
    ≈-Λ∙ ⌊j₁⌋≡⌊j₂⌋ (≈-η-exp′ ⌊k₁⌋≡l₂ ⌊k₂⌋≡l₂ a₁·ηz≈a₂·ηz)
    where
      ⌊j₁⌋≡⌊j₂⌋   = trans (⌊⌋≡⇒⌊⌋-≡ ⌊j₁⌋≡l₁) (sym (⌊⌋≡⇒⌊⌋-≡ ⌊j₂⌋≡l₁))
      a₁·ηz≈a₂·ηz =
        ≈-⌜·⌝ (≈-weakenElim a₁≈a₂)
              (≈-η-exp′ (⌊⌋≡-weaken ⌊j₁⌋≡l₁) (⌊⌋≡-weaken ⌊j₂⌋≡l₁) (≈-var∙ zero))

  ≈-η-exp : ∀ {n} {j₁ j₂ : Kind Elim n} {a₁ a₂} →
            ⌊ j₁ ⌋ ≡ ⌊ j₂ ⌋ → a₁ ≈ a₂ → η-exp j₁ a₁ ≈ η-exp j₂ a₂
  ≈-η-exp {_} {j₁} {j₂} {a₁} {a₂} ⌊j₁⌋≡⌊j₂⌋ a₁≈a₂ = begin
      η-exp j₁ a₁
    ≡⟨ TK.η-exp-⌊⌋≡ (⌊⌋-⌊⌋≡ j₁) (⌊⌋≡-trans ⌊j₁⌋≡⌊j₂⌋ (⌊⌋-⌊⌋≡ j₂))
                    refl ⌊j₁⌋≡⌊j₂⌋ ⟩
      TK.η-exp j₁ _ a₁
    ≈⟨ ≈-η-exp′ (⌊⌋≡-trans ⌊j₁⌋≡⌊j₂⌋ (⌊⌋-⌊⌋≡ j₂)) (⌊⌋-⌊⌋≡ j₂) a₁≈a₂ ⟩
      η-exp j₂ a₂
    ∎

  open SimpleCtx using (kd; ⌊_⌋Asc; kd-inj′)
  open ContextConversions using (⌊_⌋Ctx)

  -- A variant of `nf-var-kd' that is a corollary of the above.

  nf-var-kd-⌊⌋ : ∀ {n} (Γ : Ctx n) {k} x →
                 ⌊ lookup Γ x ⌋Asc ≡ kd ⌊ k ⌋ → nf Γ (var x) ≈ η-exp k (var∙ x)
  nf-var-kd-⌊⌋ Γ x hyp with lookup Γ x
  nf-var-kd-⌊⌋ Γ x hyp | kd j = ≈-η-exp (kd-inj′ hyp) (≈-var∙ x)
  nf-var-kd-⌊⌋ Γ x ()  | tp _

open WeakEqEtaExpansion

module WeakEqNormalization where
  open SimpleCtx using (kd; ⌊_⌋Asc; ⌊⌋-ElimAsc/Var; kd-inj′)
  open ContextConversions

  -- A helper lemma.

  ⌊⌋≡⌊⌋-lookup : ∀ {n} (Γ₁ Γ₂ : Ctx n) x → ⌊ Γ₁ ⌋Ctx ≡ ⌊ Γ₂ ⌋Ctx →
                 ⌊ lookup Γ₁ x ⌋Asc ≡ ⌊ lookup Γ₂ x ⌋Asc
  ⌊⌋≡⌊⌋-lookup Γ₁ Γ₂ x ⌊Γ₁⌋≡⌊Γ₂⌋ = begin
      ⌊ lookup Γ₁ x ⌋Asc
    ≡˘⟨ ⌊⌋Asc-lookup Γ₁ x ⟩
      SimpleCtx.lookup ⌊ Γ₁ ⌋Ctx x
    ≡⟨ cong (λ Δ → SimpleCtx.lookup Δ x) ⌊Γ₁⌋≡⌊Γ₂⌋ ⟩
      SimpleCtx.lookup ⌊ Γ₂ ⌋Ctx x
    ≡⟨ ⌊⌋Asc-lookup Γ₂ x ⟩
      ⌊ lookup Γ₂ x ⌋Asc
    ∎
    where open ≡-Reasoning

  -- If two contexts have the same shape, then kinds, types and terms
  -- normalize weakly equally in these contexts.

  mutual

    ≈-nf : ∀ {n} {Γ₁ Γ₂ : Ctx n} →
           ⌊ Γ₁ ⌋Ctx ≡ ⌊ Γ₂ ⌋Ctx → ∀ a → nf Γ₁ a ≈ nf Γ₂ a
    ≈-nf {_} {Γ₁} {Γ₂} ⌊Γ₁⌋≡⌊Γ₂⌋ (var x)
      with lookup Γ₁ x | lookup Γ₂ x | ⌊⌋≡⌊⌋-lookup Γ₁ Γ₂ x ⌊Γ₁⌋≡⌊Γ₂⌋
    ≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ (var x) | kd k₁ | kd k₂ | ⌊kd-k₁⌋≡⌊kd-k₂⌋ =
      ≈-η-exp (kd-inj′ ⌊kd-k₁⌋≡⌊kd-k₂⌋) (≈-var∙ x)
    ≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ (var x) | kd _  | tp _  | ()
    ≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ (var x) | tp _  | kd _  | ()
    ≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ (var x) | tp a₁ | tp a₂ | refl = ≈-var∙ x
    ≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ ⊥       = ≈-⊥∙
    ≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ ⊤       = ≈-⊤∙
    ≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ (Π k a) =
      let k≋k′ = ≋-nfKind ⌊Γ₁⌋≡⌊Γ₂⌋ k
      in ≈-∀∙ k≋k′ (≈-nf (cong₂ _∷_ (cong kd (≋-⌊⌋ k≋k′)) ⌊Γ₁⌋≡⌊Γ₂⌋) a)
    ≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ (a ⇒ b) = ≈-⇒∙ (≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ a) (≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ b)
    ≈-nf {_} {Γ₁} ⌊Γ₁⌋≡⌊Γ₂⌋ (Λ k a) =
      let k≋k′ = ≋-nfKind ⌊Γ₁⌋≡⌊Γ₂⌋ k
      in ≈-Λ∙ (≋-⌊⌋ k≋k′) (≈-nf (cong₂ _∷_ (cong kd (≋-⌊⌋ k≋k′)) ⌊Γ₁⌋≡⌊Γ₂⌋) a)
    ≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ (ƛ a b) = ≈-λ∙ (≈-refl ⌜ b ⌝)
    ≈-nf {_} {Γ₁} {Γ₂} ⌊Γ₁⌋≡⌊Γ₂⌋ (a · b) =
      ≈-↓⌜·⌝ (≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ a) (≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ b)
    ≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ (a ⊡ b) = ≈-⊡∙ (≈-refl ⌜ a ⌝) (≈-refl ⌜ b ⌝)

    ≋-nfKind : ∀ {n} {Γ₁ Γ₂ : Ctx n} →
               ⌊ Γ₁ ⌋Ctx ≡ ⌊ Γ₂ ⌋Ctx → ∀ k → nfKind Γ₁ k ≋ nfKind Γ₂ k
    ≋-nfKind ⌊Γ₁⌋≡⌊Γ₂⌋ (a ⋯ b) = ≋-⋯ (≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ a) (≈-nf ⌊Γ₁⌋≡⌊Γ₂⌋ b)
    ≋-nfKind ⌊Γ₁⌋≡⌊Γ₂⌋ (Π j k) =
      let j≋j′ = ≋-nfKind ⌊Γ₁⌋≡⌊Γ₂⌋ j
      in ≋-Π j≋j′ (≋-nfKind (cong₂ _∷_ (cong kd (≋-⌊⌋ j≋j′)) ⌊Γ₁⌋≡⌊Γ₂⌋) k)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda