text:
------------------------------------------------------------------------
-- Canonically kinded hereditary substitutions in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Canonical.HereditarySubstitution where

open import Data.Fin using (Fin; zero; suc; raise; lift)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Typed
open import Data.Product as Prod using (∃; _,_; _×_; proj₁; proj₂)
open import Data.Vec as Vec using ([]; _∷_)
import Data.Vec.Properties as VecProps
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.SingleVariableSubstitution
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization
open import FOmegaInt.Kinding.Canonical as CanonicalKinding
open import FOmegaInt.Kinding.Simple    as SimpleKinding

open Syntax
open ElimCtx
open SimpleCtx          using (⌊_⌋Asc; kd; tp)
open ContextConversions using (⌊_⌋Ctx)
open Substitution       hiding (_↑; sub; subst)
open RenamingCommutes
open SimpHSubstLemmas
open SimpleKinding.Kinding using (_⊢_kds; kds-Π)
open CanonicalKinding.Kinding
open KindedHereditarySubstitution
  using (_⊢/⟨_⟩_∈_; ∈-hsub; ∈-H↑; kds-/⟨⟩; kds-[]-/⟨⟩-↑⋆)
open CanonicalKinding.KindedRenaming
  using (typedVarSubst; kd-/Var; ≃-/Var; <∷-/Var; kd-weaken; <∷-weaken)
module TV = TypedVarSubst typedVarSubst
open ContextNarrowing

----------------------------------------------------------------------
-- Ascription order: a wrapper judgment that combines subtyping and
-- subkinding.
--
-- NOTE. Subtyping instances are always trivial, i.e. they only
-- support (syntactic) reflexivity.

infix 4 _⊢_≤_

data _⊢_≤_ {n} (Γ : Ctx n) : ElimAsc n → ElimAsc n → Set where
  ≤-<∷   : ∀ {j k} → Γ ⊢ j <∷ k → Γ ⊢ k kd → Γ ⊢ kd j ≤ kd k
  ≤-refl : ∀ {a} → Γ ⊢ a ≤ a

-- Transitivity of the ascription order.

≤-trans : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢ a ≤ b → Γ ⊢ b ≤ c → Γ ⊢ a ≤ c
≤-trans (≤-<∷ j<∷k _)    (≤-<∷ k<∷l l-kd) = ≤-<∷ (<∷-trans j<∷k k<∷l) l-kd
≤-trans (≤-<∷ j<∷k k-kd) ≤-refl           = ≤-<∷ j<∷k k-kd
≤-trans ≤-refl           a≤c              = a≤c

-- Kinds in related ascriptions have the same shape.

≤-⌊⌋ : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ kd j ≤ kd k → ⌊ j ⌋ ≡ ⌊ k ⌋
≤-⌊⌋ (≤-<∷ j<∷k _) = <∷-⌊⌋ j<∷k
≤-⌊⌋ ≤-refl        = refl

-- Renamings preserve the ascription order.

≤-/Var : ∀ {m n Γ Δ a b} {ρ : Sub Fin m n} →
         Γ ⊢ a ≤ b → Δ TV.⊢/Var ρ ∈ Γ → Δ ⊢ a ElimAsc/Var ρ ≤ b ElimAsc/Var ρ
≤-/Var (≤-<∷ j<∷k k-kd) ρ∈Γ = ≤-<∷ (<∷-/Var j<∷k ρ∈Γ) (kd-/Var k-kd ρ∈Γ)
≤-/Var ≤-refl           ρ∈Γ = ≤-refl

-- Admissible subsumption rules w.r.t. the ascription order.

Nf⇇-⇑-≤ : ∀ {n} {Γ : Ctx n} {a k j} →
          Γ ⊢Nf a ⇇ k → Γ ⊢ kd k ≤ kd j → Γ ⊢Nf a ⇇ j
Nf⇇-⇑-≤ a⇇k (≤-<∷ k<∷j j-kd) = Nf⇇-⇑ a⇇k k<∷j
Nf⇇-⇑-≤ a⇇k ≤-refl           = a⇇k

≃-⇑-≤ : ∀ {n} {Γ : Ctx n} {a b k j} →
        Γ ⊢ a ≃ b ⇇ k → Γ ⊢ kd k ≤ kd j → Γ ⊢ a ≃ b ⇇ j
≃-⇑-≤ a≃b⇇k (≤-<∷ k<∷j j-kd) = ≃-⇑ a≃b⇇k k<∷j j-kd
≃-⇑-≤ a≃b⇇k ≤-refl           = a≃b⇇k

-- An admissible variable rule based on the ascription order.

Var∈-⇑-≤  : ∀ {n} {Γ : Ctx n} {a k} x →
            Γ ctx → lookup Γ x ≡ a → Γ ⊢ a ≤ kd k → Γ ⊢Var x ∈ k
Var∈-⇑-≤ x Γ-ctx Γ[x]≡j (≤-<∷ j<∷k k-kd) = ⇇-⇑ (⇉-var x Γ-ctx Γ[x]≡j) j<∷k k-kd
Var∈-⇑-≤ x Γ-ctx Γ[x]≡k ≤-refl           = ⇉-var x Γ-ctx Γ[x]≡k

----------------------------------------------------------------------
-- Well-kinded hereditary substitutions (i.e. substitution lemmas) in
-- canonical types

infix 4 _⊢/⟨_⟩_⇇_ _⊢/⟨_⟩_≃_⇇_ _⊢?⟨_⟩_⇇_ _⊢?⟨_⟩_≃_⇇_

-- Well-kinded pointwise equality of hereditary substitutions and
-- their lookup results.

data _⊢/⟨_⟩_≃_⇇_ : ∀ {m n} →
                   Ctx n → SKind → SVSub m n → SVSub m n → Ctx m → Set where
  ≃-hsub : ∀ {n} {Γ : Ctx n} {k a b j} →
           Γ ⊢ a ≃ b ⇇ j → ⌊ j ⌋≡ k →
           Γ ⊢/⟨ k ⟩ sub a ≃ sub b ⇇ kd j ∷ Γ
  ≃-H↑   : ∀ {m n Δ k Γ} {σ τ : SVSub m n} {j l} →
           Δ ⊢ j ≅ l Kind/⟨ k ⟩ σ → Δ ⊢ j ≅ l Kind/⟨ k ⟩ τ →
           Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ → kd j ∷ Δ ⊢/⟨ k ⟩ σ ↑ ≃ τ ↑ ⇇ kd l ∷ Γ

data _⊢?⟨_⟩_≃_⇇_ {n} (Γ : Ctx n) (k : SKind)
                 : SVRes n → SVRes n → ElimAsc n → Set where
  ≃-hit  : ∀ {a b j} →
           Γ ⊢ a ≃ b ⇇ j → ⌊ j ⌋≡ k → Γ ⊢?⟨ k ⟩ hit a ≃ hit b ⇇ kd j
  ≃-miss : ∀ y {a b} → Γ ctx → lookup Γ y ≡ a → Γ ⊢ a ≤ b →
           Γ ⊢?⟨ k ⟩ miss y ≃ miss y ⇇ b

-- Well-kinded suspended hereditary substations are just a degenerate
-- case of equal hereditary substitutions where the underlying
-- substitutions coincide (syntactically).

_⊢/⟨_⟩_⇇_ : ∀ {m n} → Ctx n → SKind → SVSub m n → Ctx m → Set
Δ ⊢/⟨ k ⟩ σ ⇇ Γ = Δ ⊢/⟨ k ⟩ σ ≃ σ ⇇ Γ

⇇-hsub : ∀ {n} {Γ : Ctx n} {k a j} →
         Γ ⊢Nf a ⇇ j → Γ ⊢ j kd → ⌊ j ⌋≡ k →
         Γ ⊢/⟨ k ⟩ sub a ⇇ kd j ∷ Γ
⇇-hsub a⇇j j-kd ⌊j⌋≡k = ≃-hsub (≃-reflNf⇇ a⇇j j-kd) ⌊j⌋≡k

⇇-H↑ : ∀ {m n Δ k Γ} {σ : SVSub m n} {j l} →
       Δ ⊢ j ≅ l Kind/⟨ k ⟩ σ → Δ ⊢/⟨ k ⟩ σ ⇇ Γ →
       kd j ∷ Δ ⊢/⟨ k ⟩ σ ↑ ⇇ kd l ∷ Γ
⇇-H↑ j≅l/σ σ⇇Γ = ≃-H↑ j≅l/σ j≅l/σ σ⇇Γ

_⊢?⟨_⟩_⇇_ : ∀ {n} → Ctx n → SKind → SVRes n → ElimAsc n → Set
Δ ⊢?⟨ k ⟩ σ ⇇ Γ = Δ ⊢?⟨ k ⟩ σ ≃ σ ⇇ Γ

⇇-hit  : ∀ {n} {Γ : Ctx n} {k a j} →
         Γ ⊢Nf a ⇇ j → Γ ⊢ j kd → ⌊ j ⌋≡ k → Γ ⊢?⟨ k ⟩ hit a ⇇ kd j
⇇-hit a⇇j j-kd ⌊j⌋≡k = ≃-hit (≃-reflNf⇇ a⇇j j-kd) ⌊j⌋≡k

⇇-miss = λ {n} {Γ} {k} → ≃-miss {n} {Γ} {k}

-- Renamings preserve equality of SV results.

?≃-/Var : ∀ {m n Γ k Δ r₁ r₂ a} {ρ : Sub Fin m n} →
          Γ ⊢?⟨ k ⟩ r₁ ≃ r₂ ⇇ a → Δ TV.⊢/Var ρ ∈ Γ →
          Δ ⊢?⟨ k ⟩ r₁ ?/Var ρ ≃ r₂ ?/Var ρ ⇇ a ElimAsc/Var ρ
?≃-/Var (≃-hit a≃b∈k ⌊j⌋≡k) ρ∈Γ =
  ≃-hit (≃-/Var a≃b∈k ρ∈Γ) (⌊⌋≡-/Var ⌊j⌋≡k)
?≃-/Var {Γ = Γ} {k} {Δ} {ρ = ρ} (≃-miss y {a} {b} _ Γ[x]≡a a≤b) ρ∈Γ =
  helper (cong (_ElimAsc/Var ρ) Γ[x]≡a) (TV.lookup ρ∈Γ y)
  where
    helper : ∀ {x c} → c ≡ a ElimAsc/Var ρ → Δ TV.⊢Var x ∈ c →
             Δ ⊢?⟨ k ⟩ miss x ≃ miss x ⇇ b ElimAsc/Var ρ
    helper Δ[x]≡a/ρ (TV.∈-var x Δ-ctx) =
      ≃-miss x (TV./∈-wf ρ∈Γ) Δ[x]≡a/ρ (≤-/Var a≤b ρ∈Γ)

?≃-weaken : ∀ {n} {Γ : Ctx n} {k r₁ r₂ a b} →
            Γ ⊢ a wf → Γ ⊢?⟨ k ⟩ r₁ ≃ r₂ ⇇ b →
            (a ∷ Γ) ⊢?⟨ k ⟩ weakenSVRes r₁ ≃ weakenSVRes r₂ ⇇ weakenElimAsc b
?≃-weaken a-wf r₁≃r₂⇇a = ?≃-/Var r₁≃r₂⇇a (TV.∈-wk a-wf)

-- Look up a variable in a pair of well-kinded pointwise equal
-- hereditary substitution.

lookup-/⟨⟩≃ : ∀ {m n Δ k Γ} {σ τ : SVSub m n} →
              Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ → (x : Fin m) →
              Δ ⊢?⟨ k ⟩ lookupSV σ x ≃ lookupSV τ x ⇇ lookup Γ x Asc/⟨ k ⟩ σ
lookup-/⟨⟩≃ (≃-hsub {_} {Γ} {k} {a} {b} {j} a≃b⇇k ⌊j⌋≡k) zero =
  subst (Γ ⊢?⟨ k ⟩ hit a ≃ hit b ⇇_)
        (cong kd (sym (Kind/Var-wk-↑⋆-hsub-vanishes 0 j))) (≃-hit a≃b⇇k ⌊j⌋≡k)
lookup-/⟨⟩≃ (≃-hsub {Γ = Γ} {k} {a} {_} {j} a≃b⇇k ⌊j⌋≡k) (suc x) =
  subst (Γ ⊢?⟨ k ⟩ miss x ≃ miss x ⇇_) (begin
      lookup Γ x
    ≡˘⟨ Asc/Var-wk-↑⋆-hsub-vanishes 0 (lookup Γ x) ⟩
      weakenElimAsc (lookup Γ x) Asc/⟨ k ⟩ sub a
    ≡˘⟨ cong (_Asc/⟨ k ⟩ sub a) (VecProps.lookup-map x weakenElimAsc (toVec Γ)) ⟩
       lookup (kd j ∷ Γ) (suc x) Asc/⟨ k ⟩ sub a
    ∎) (≃-miss x (≃-ctx a≃b⇇k) refl ≤-refl)
lookup-/⟨⟩≃ (≃-H↑ {Δ = Δ} {k} {j = j} {l} j≅l/σ j≅l/τ σ≃τ⇇Γ) zero =
  let j-kd , l/σ-kd = ≅-valid j≅l/σ
      j-wf  = wf-kd j-kd
      j≤l/σ = ≤-<∷ (<∷-weaken j-wf (≅⇒<∷ j≅l/σ)) (kd-weaken j-wf l/σ-kd)
  in subst (kd j ∷ Δ ⊢?⟨ k ⟩ miss zero ≃ miss zero ⇇_)
           (sym (wk-Asc/⟨⟩-↑⋆ 0 (kd l)))
           (≃-miss zero (j-wf ∷ (kd-ctx j-kd)) refl j≤l/σ)
lookup-/⟨⟩≃ (≃-H↑ {k = k} {Γ} {σ} {_} {_} {l} j≅l/σ _ σ≃τ⇇Γ) (suc x) =
  subst (_ ⊢?⟨ k ⟩ _ ≃ _ ⇇_) (begin
      weakenElimAsc (lookup Γ x Asc/⟨ k ⟩ σ)
    ≡˘⟨ wk-Asc/⟨⟩-↑⋆ 0 (lookup Γ x) ⟩
      weakenElimAsc (lookup Γ x) Asc/⟨ k ⟩ σ ↑
    ≡˘⟨ cong (_Asc/⟨ k ⟩ σ ↑)
             (VecProps.lookup-map x weakenElimAsc (toVec Γ)) ⟩
      lookup (kd l ∷ Γ) (suc x) Asc/⟨ k ⟩ σ ↑
    ∎) (?≃-weaken (wf-kd (proj₁ (≅-valid j≅l/σ))) (lookup-/⟨⟩≃ σ≃τ⇇Γ x))

-- Equation and context validity lemmas for hereditary substitutions.

/⟨⟩≃-valid₁ : ∀ {k m n Δ Γ} {σ τ : SVSub m n} →
              Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ → Δ ⊢/⟨ k ⟩ σ ⇇ Γ
/⟨⟩≃-valid₁ (≃-hsub a≃b⇇j ⌊j⌋≡k) =
  ⇇-hsub (proj₁ (≃-valid a≃b⇇j)) (≃-valid-kd a≃b⇇j) ⌊j⌋≡k
/⟨⟩≃-valid₁ (≃-H↑ a≅b/σ _ σ≃τ∈Γ) = ⇇-H↑ a≅b/σ (/⟨⟩≃-valid₁ σ≃τ∈Γ)

/⟨⟩≃-valid₂ : ∀ {k m n Δ Γ} {σ τ : SVSub m n} →
              Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ → Δ ⊢/⟨ k ⟩ τ ⇇ Γ
/⟨⟩≃-valid₂ (≃-hsub a≃b⇇j ⌊j⌋≡k) =
  ⇇-hsub (proj₂ (≃-valid a≃b⇇j)) (≃-valid-kd a≃b⇇j) ⌊j⌋≡k
/⟨⟩≃-valid₂ (≃-H↑ _ a≅b/τ σ≃τ∈Γ) = ⇇-H↑ a≅b/τ (/⟨⟩≃-valid₂ σ≃τ∈Γ)

/⟨⟩≃-ctx : ∀ {k m n Γ Δ} {σ τ : SVSub m n} →
           Γ ctx → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ → Δ ctx
/⟨⟩≃-ctx j∷Γ-ctx (≃-hsub a≃b⇇j ⌊j⌋≡k)     = wf-∷₂ j∷Γ-ctx
/⟨⟩≃-ctx l∷Γ-ctx (≃-H↑ j≅l/σ j≅l/τ σ≃τ⇇Γ) =
  let j-kd , _ = ≅-valid j≅l/σ
      Γ-ctx    = wf-∷₂ l∷Γ-ctx
  in (wf-kd j-kd) ∷ /⟨⟩≃-ctx Γ-ctx σ≃τ⇇Γ

-- Symmetry of hereditary substitution equality.

/⟨⟩≃-sym : ∀ {k m n Δ Γ} {σ τ : SVSub m n} →
           Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ → Δ ⊢/⟨ k ⟩ τ ≃ σ ⇇ Γ
/⟨⟩≃-sym (≃-hsub a≃b⇇j ⌊j⌋≡k)     = ≃-hsub (≃-sym a≃b⇇j) ⌊j⌋≡k
/⟨⟩≃-sym (≃-H↑ a≅b/σ a≅b/τ σ≃τ∈Γ) = ≃-H↑ a≅b/τ a≅b/σ (/⟨⟩≃-sym σ≃τ∈Γ)

-- Simplification of kinded substitutions.
--
-- NOTE. The second substitution τ is ignored by the simplification.
-- It is tempting to rephrase the lemma in terms of _⊢/⟨_⟩_⇇_ instead
-- of _⊢/⟨_⟩_≃_⇇_ but that introduces extra constraints for the Agda
-- pattern matcher that require UIP (aka axiom K) to resolve.  Since
-- this assumption is unnecessary, we prove the more general version
-- instead. (See the Agda documentation about the --without-K option
-- for more info).

/⟨⟩⇇-/⟨⟩∈ : ∀ {k m n Δ Γ} {σ τ : SVSub m n} →
            Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ → ⌊ Δ ⌋Ctx ⊢/⟨ k ⟩ σ ∈ ⌊ Γ ⌋Ctx
/⟨⟩⇇-/⟨⟩∈ (≃-hsub a≃b⇇j ⌊j⌋≡k) =
  subst (_ ⊢/⟨_⟩ _ ∈ _) (⌊⌋≡⇒⌊⌋-≡ ⌊j⌋≡k)
        (∈-hsub (Nf⇇-Nf∈ (proj₁ (≃-valid a≃b⇇j))))
/⟨⟩⇇-/⟨⟩∈ (≃-H↑ {Δ = Δ} {k} {Γ} {σ} {_} {j} {l} j≅l/σ _ σ≃σ∈Γ) =
  subst ((_⊢/⟨ k ⟩ σ ↑ ∈ ⌊ kd l ∷ Γ ⌋Ctx) ∘ (_∷ ⌊ Δ ⌋Ctx)) (begin
          ⌊ kd l ⌋Asc              ≡˘⟨ ⌊⌋-Asc/⟨⟩ (kd l) ⟩
          ⌊ kd l Asc/⟨ k ⟩ σ ⌋Asc  ≡˘⟨ cong kd (≅-⌊⌋ j≅l/σ) ⟩
          ⌊ kd j ⌋Asc              ∎)
        (∈-H↑ (/⟨⟩⇇-/⟨⟩∈ σ≃σ∈Γ))

-- TODO: explain why we need to track shapes explicitly.

module TrackSimpleKindsSubst where

  -- TODO: explain how/why preservation of (sub)kinding/subtyping
  -- under reducing applications, hereditary substitution and equal
  -- hereditary substitutions circularly depend on each other.

  mutual

    -- Hereditary substitutions preserve well-formedness of kinds.

    kd-/⟨⟩ : ∀ {k m n Γ Δ} {σ : SVSub m n} {j} →
             Γ ⊢ j kd → Δ ⊢/⟨ k ⟩ σ ⇇ Γ → Δ ⊢ j Kind/⟨ k ⟩ σ kd
    kd-/⟨⟩ (kd-⋯ a⇉a⋯a b⇉b⋯b) σ⇇Γ =
      kd-⋯ (Nf⇉-/⟨⟩ a⇉a⋯a σ⇇Γ) (Nf⇉-/⟨⟩ b⇉b⋯b σ⇇Γ)
    kd-/⟨⟩ (kd-Π j-kd k-kd)   σ⇇Γ =
      let j/σ-kd = kd-/⟨⟩ j-kd σ⇇Γ
      in kd-Π j/σ-kd (kd-/⟨⟩ k-kd (⇇-H↑ (≅-refl j/σ-kd) σ⇇Γ))

    -- Hereditary substitutions preserve synthesized kinds of normal
    -- types.

    Nf⇉-/⟨⟩ : ∀ {k m n Γ Δ} {σ : SVSub m n} {a j} →
              Γ ⊢Nf a ⇉ j → Δ ⊢/⟨ k ⟩ σ ⇇ Γ → Δ ⊢Nf a /⟨ k ⟩ σ ⇉ j Kind/⟨ k ⟩ σ
    Nf⇉-/⟨⟩ (⇉-⊥-f Γ-ctx) σ⇇Γ = ⇉-⊥-f (/⟨⟩≃-ctx Γ-ctx σ⇇Γ)
    Nf⇉-/⟨⟩ (⇉-⊤-f Γ-ctx) σ⇇Γ = ⇉-⊤-f (/⟨⟩≃-ctx Γ-ctx σ⇇Γ)
    Nf⇉-/⟨⟩ (⇉-∀-f k-kd a⇉a⋯a)  σ⇇Γ =
      let k/σ-kd = kd-/⟨⟩ k-kd σ⇇Γ
      in ⇉-∀-f k/σ-kd (Nf⇉-/⟨⟩ a⇉a⋯a (⇇-H↑ (≅-refl k/σ-kd) σ⇇Γ))
    Nf⇉-/⟨⟩ (⇉-→-f a⇉a⋯a b⇉b⋯b) σ⇇Γ =
      ⇉-→-f (Nf⇉-/⟨⟩ a⇉a⋯a σ⇇Γ) (Nf⇉-/⟨⟩ b⇉b⋯b σ⇇Γ)
    Nf⇉-/⟨⟩ (⇉-Π-i k-kd a⇉a⋯a)  σ⇇Γ =
      let k/σ-kd = kd-/⟨⟩ k-kd σ⇇Γ
      in ⇉-Π-i k/σ-kd (Nf⇉-/⟨⟩ a⇉a⋯a (⇇-H↑ (≅-refl k/σ-kd) σ⇇Γ))
    Nf⇉-/⟨⟩ (⇉-s-i a∈b⋯c) σ⇇Γ = Nf⇇-s-i (Ne∈-/⟨⟩ a∈b⋯c σ⇇Γ)

    -- Neutral proper types kind-check against their synthesized kinds
    -- after substitution.

    Ne∈-/⟨⟩ : ∀ {k m n Γ Δ} {σ : SVSub m n} {a b c} →
              Γ ⊢Ne a ∈ b ⋯ c → Δ ⊢/⟨ k ⟩ σ ⇇ Γ →
              Δ ⊢Nf a /⟨ k ⟩ σ ⇇ b /⟨ k ⟩ σ ⋯ c /⟨ k ⟩ σ
    Ne∈-/⟨⟩ (∈-∙ {x} x∈j j⇉as⇉b⋯c) σ⇇Γ =
      let j-kds = kd-kds (Var∈-valid x∈j)
      in Var∈-/⟨⟩-⇑-?∙∙ x∈j σ⇇Γ ≤-refl (Sp⇉-/⟨⟩ j-kds j⇉as⇉b⋯c σ⇇Γ)

    Var∈-/⟨⟩-⇑-?∙∙ : ∀ {k m n Γ Δ} {σ : SVSub m n} {x j l as b c} →
                     Γ ⊢Var x ∈ j → Δ ⊢/⟨ k ⟩ σ ⇇ Γ →
                     Δ ⊢ kd j Asc/⟨ k ⟩ σ ≤ kd l → Δ ⊢ l ⇉∙ as ⇉ b ⋯ c →
                     Δ ⊢Nf lookupSV σ x ?∙∙⟨ k ⟩ as ⇇ b ⋯ c
    Var∈-/⟨⟩-⇑-?∙∙ (⇉-var x _ Γ[x]≡kd-j) σ⇇Γ j/σ≤l l⇉as⇉b⋯c =
      ?⇇-⇑-?∙∙ (subst (_ ⊢?⟨ _ ⟩ _ ⇇_) (cong (_Asc/⟨ _ ⟩ _) Γ[x]≡kd-j)
                      (lookup-/⟨⟩≃ σ⇇Γ x))
               j/σ≤l l⇉as⇉b⋯c
    Var∈-/⟨⟩-⇑-?∙∙ (⇇-⇑ x∈j₁ j₁<∷j₂ j₂-kd) σ⇇Γ j₂/σ≤l l⇉as⇉b⋯c =
      let j₁/σ≤j₂/σ = ≤-<∷ (<∷-/⟨⟩≃ j₁<∷j₂ σ⇇Γ) (kd-/⟨⟩ j₂-kd σ⇇Γ)
      in Var∈-/⟨⟩-⇑-?∙∙ x∈j₁ σ⇇Γ (≤-trans j₁/σ≤j₂/σ j₂/σ≤l) l⇉as⇉b⋯c

    -- Hereditary substitutions preserve synthesized kinds of spines.
    Sp⇉-/⟨⟩ : ∀ {k m n Γ Δ} {σ : SVSub m n} {as j₁ j₂} →
              ⌊ Γ ⌋Ctx ⊢ j₁ kds → Γ ⊢ j₁ ⇉∙ as ⇉ j₂ → Δ ⊢/⟨ k ⟩ σ ⇇ Γ →
              Δ ⊢ j₁ Kind/⟨ k ⟩ σ ⇉∙ as //⟨ k ⟩ σ ⇉ j₂ Kind/⟨ k ⟩ σ
    Sp⇉-/⟨⟩ _ ⇉-[] σ⇇Γ = ⇉-[]
    Sp⇉-/⟨⟩ {k} (kds-Π j₁-kds j₂-kds)
            (⇉-∷ {a} {_} {j₁} {j₂} a⇇j₁ j₁-kd j₂[a]⇉as⇉j₃) σ⇇Γ =
      ⇉-∷ (Nf⇇-/⟨⟩ a⇇j₁ σ⇇Γ) (kd-/⟨⟩ j₁-kd σ⇇Γ)
          (subst (_ ⊢_⇉∙ _ ⇉ _) j₂[a]/σ≡j₂/σ[a/σ]
                 (Sp⇉-/⟨⟩ (kds-/⟨⟩ j₂-kds (∈-hsub a∈⌊j₁⌋)) j₂[a]⇉as⇉j₃ σ⇇Γ))
      where
        a∈⌊j₁⌋ = Nf⇇-Nf∈ a⇇j₁

        j₂[a]/σ≡j₂/σ[a/σ] = begin
            j₂ Kind[ a ∈ ⌊ j₁ ⌋ ] Kind/⟨ k ⟩ _
          ≡⟨ kds-[]-/⟨⟩-↑⋆ [] j₂-kds a∈⌊j₁⌋ (/⟨⟩⇇-/⟨⟩∈ σ⇇Γ) ⟩
            j₂ Kind/⟨ k ⟩ _ ↑ Kind/⟨ ⌊ j₁ ⌋ ⟩ sub (a /⟨ k ⟩ _)
          ≡⟨ cong (_ Kind[ a /⟨ k ⟩ _ ∈_]) (sym (⌊⌋-Kind/⟨⟩ j₁)) ⟩
            (j₂ Kind/⟨ k ⟩ _ ↑) Kind[ a /⟨ k ⟩ _ ∈ ⌊ j₁ Kind/⟨ k ⟩ _ ⌋ ]
          ∎

    -- Hereditary substitutions preserve checked kinds of normal
    -- types.
    Nf⇇-/⟨⟩ : ∀ {k m n Γ Δ} {σ : SVSub m n} {a j} →
              Γ ⊢Nf a ⇇ j → Δ ⊢/⟨ k ⟩ σ ⇇ Γ → Δ ⊢Nf a /⟨ k ⟩ σ ⇇ j Kind/⟨ k ⟩ σ
    Nf⇇-/⟨⟩ (⇇-⇑ a⇉j j<∷k) σ⇇Γ = ⇇-⇑ (Nf⇉-/⟨⟩ a⇉j σ⇇Γ) (<∷-/⟨⟩≃ j<∷k σ⇇Γ)

    -- Equal hereditary substitutions well-formed kinds to subkinds.
    kd-/⟨⟩≃-<∷ : ∀ {m n Γ k Δ} {σ τ : SVSub m n} {j} →
                 Γ ⊢ j kd → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
                 Δ ⊢ j Kind/⟨ k ⟩ σ <∷ j Kind/⟨ k ⟩ τ
    kd-/⟨⟩≃-<∷ (kd-⋯ a⇉a⋯a b⇉b⋯b) σ≃τ⇇Γ =
      <∷-⋯ (Nf⇉-⋯-/⟨⟩≃ a⇉a⋯a (/⟨⟩≃-sym σ≃τ⇇Γ)) (Nf⇉-⋯-/⟨⟩≃ b⇉b⋯b σ≃τ⇇Γ)
    kd-/⟨⟩≃-<∷ (kd-Π j-kd k-kd)   σ≃τ⇇Γ =
      let σ⇇Γ     = /⟨⟩≃-valid₁ σ≃τ⇇Γ
          τ⇇Γ     = /⟨⟩≃-valid₂ σ≃τ⇇Γ
          τ≃σ⇇Γ   = /⟨⟩≃-sym σ≃τ⇇Γ
          j/σ≅j/σ = kd-/⟨⟩≃-≅ j-kd σ⇇Γ
          j/τ≅j/τ = kd-/⟨⟩≃-≅ j-kd τ⇇Γ
          j/τ≅j/σ = kd-/⟨⟩≃-≅ j-kd τ≃σ⇇Γ
      in <∷-Π (kd-/⟨⟩≃-<∷ j-kd τ≃σ⇇Γ)
              (kd-/⟨⟩≃-<∷ k-kd (≃-H↑ j/τ≅j/σ j/τ≅j/τ σ≃τ⇇Γ))
              (kd-Π (kd-/⟨⟩ j-kd σ⇇Γ) (kd-/⟨⟩ k-kd (⇇-H↑ j/σ≅j/σ σ⇇Γ)))

    -- Equal hereditary substitutions map well-formed kinds to kind
    -- identities.
    kd-/⟨⟩≃-≅ : ∀ {m n Γ k Δ} {σ τ : SVSub m n} {j} →
                Γ ⊢ j kd → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
                Δ ⊢ j Kind/⟨ k ⟩ σ ≅ j Kind/⟨ k ⟩ τ
    kd-/⟨⟩≃-≅ k-kd σ≃τ⇇Γ =
      <∷-antisym (kd-/⟨⟩ k-kd (/⟨⟩≃-valid₁ σ≃τ⇇Γ))
                 (kd-/⟨⟩ k-kd (/⟨⟩≃-valid₂ σ≃τ⇇Γ))
                 (kd-/⟨⟩≃-<∷ k-kd σ≃τ⇇Γ) (kd-/⟨⟩≃-<∷ k-kd (/⟨⟩≃-sym σ≃τ⇇Γ))

    -- Equal hereditary substitutions map normal forms to subtypes.

    Nf⇉-⋯-/⟨⟩≃ : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {a b c} →
                 Γ ⊢Nf a ⇉ b ⋯ c → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
                 Δ ⊢ a /⟨ k ⟩ σ <: a /⟨ k ⟩ τ
    Nf⇉-⋯-/⟨⟩≃ (⇉-⊥-f Γ-ctx) σ≃τ⇇Γ =
      <:-⊥ (⇉-⊥-f (/⟨⟩≃-ctx Γ-ctx (/⟨⟩≃-valid₁ σ≃τ⇇Γ)))
    Nf⇉-⋯-/⟨⟩≃ (⇉-⊤-f Γ-ctx) σ≃τ⇇Γ =
      <:-⊤ (⇉-⊤-f (/⟨⟩≃-ctx Γ-ctx (/⟨⟩≃-valid₂ σ≃τ⇇Γ)))
    Nf⇉-⋯-/⟨⟩≃ (⇉-∀-f k-kd a⇉a⋯a) σ≃τ⇇Γ =
      let σ⇇Γ       = /⟨⟩≃-valid₁ σ≃τ⇇Γ
          τ⇇Γ       = /⟨⟩≃-valid₂ σ≃τ⇇Γ
          τ≃σ⇇Γ     = /⟨⟩≃-sym  σ≃τ⇇Γ
          k/τ≅k/τ   = kd-/⟨⟩≃-≅ k-kd τ⇇Γ
          k/σ≅k/σ   = kd-/⟨⟩≃-≅ k-kd σ⇇Γ
          k/τ≅k/σ   = kd-/⟨⟩≃-≅ k-kd τ≃σ⇇Γ
          σ≃τ⇇j/τ∷Γ = ≃-H↑ k/τ≅k/σ k/τ≅k/τ σ≃τ⇇Γ
      in <:-∀ (≅⇒<∷ k/τ≅k/σ) (Nf⇉-⋯-/⟨⟩≃ a⇉a⋯a σ≃τ⇇j/τ∷Γ)
              (⇉-∀-f (kd-/⟨⟩ k-kd σ⇇Γ)
                     (Nf⇉-/⟨⟩ a⇉a⋯a (⇇-H↑ k/σ≅k/σ σ⇇Γ)))
    Nf⇉-⋯-/⟨⟩≃ (⇉-→-f a⇉a⋯a b⇉b⋯b) σ≃τ⇇Γ =
      <:-→ (Nf⇉-⋯-/⟨⟩≃ a⇉a⋯a (/⟨⟩≃-sym σ≃τ⇇Γ)) (Nf⇉-⋯-/⟨⟩≃ b⇉b⋯b σ≃τ⇇Γ)
    Nf⇉-⋯-/⟨⟩≃ (⇉-s-i a∈b⋯c) σ≃τ⇇Γ = Ne∈-/⟨⟩≃ a∈b⋯c σ≃τ⇇Γ

    Nf⇉-/⟨⟩≃ : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {a j} →
               Γ ⊢Nf a ⇉ j → Γ ⊢ j kd → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
               Δ ⊢ a /⟨ k ⟩ σ <: a /⟨ k ⟩ τ ⇇ j Kind/⟨ k ⟩ σ
    Nf⇉-/⟨⟩≃ a⇉b⋯c (kd-⋯ b⇉b⋯b c⇉c⋯c) σ≃τ⇇Γ =
      let σ⇇Γ   = /⟨⟩≃-valid₁ σ≃τ⇇Γ
          τ⇇Γ   = /⟨⟩≃-valid₂ σ≃τ⇇Γ
          τ≃σ⇇Γ = /⟨⟩≃-sym σ≃τ⇇Γ
      in <:-⇇ (Nf⇉⇒Nf⇇ (Nf⇉-/⟨⟩ a⇉b⋯c σ⇇Γ))
              (⇇-⇑ (Nf⇉-/⟨⟩ a⇉b⋯c τ⇇Γ)
                   (<∷-⋯ (Nf⇉-⋯-/⟨⟩≃ b⇉b⋯b σ≃τ⇇Γ) (Nf⇉-⋯-/⟨⟩≃ c⇉c⋯c τ≃σ⇇Γ)))
              (Nf⇉-⋯-/⟨⟩≃ a⇉b⋯c σ≃τ⇇Γ)
    Nf⇉-/⟨⟩≃ (⇉-Π-i _ a⇉l) (kd-Π j-kd l-kd) σ≃τ⇇Γ =
      let τ≃σ⇇Γ = /⟨⟩≃-sym σ≃τ⇇Γ
          σ⇇Γ   = /⟨⟩≃-valid₁ σ≃τ⇇Γ
          τ⇇Γ   = /⟨⟩≃-valid₂ σ≃τ⇇Γ
          j/σ-kd  = kd-/⟨⟩ j-kd σ⇇Γ
          j/τ-kd  = kd-/⟨⟩ j-kd τ⇇Γ
          j/σ≅j/σ = kd-/⟨⟩≃-≅ j-kd σ⇇Γ
          j/τ≅j/τ = kd-/⟨⟩≃-≅ j-kd τ⇇Γ
          j/σ≅j/τ = kd-/⟨⟩≃-≅ j-kd σ≃τ⇇Γ
          a/σ⇉l/σ = Nf⇉-/⟨⟩ a⇉l (⇇-H↑ j/σ≅j/σ σ⇇Γ)
          a/τ⇉l/τ = Nf⇉-/⟨⟩ a⇉l (⇇-H↑ j/τ≅j/τ τ⇇Γ)
          a/σ<:a/τ⇇l/σ = Nf⇉-/⟨⟩≃ a⇉l l-kd (≃-H↑ j/σ≅j/σ j/σ≅j/τ σ≃τ⇇Γ)
          Πjl/τ<∷Πjl/σ = kd-/⟨⟩≃-<∷ (kd-Π j-kd l-kd) τ≃σ⇇Γ
          Λja/σ⇇Πjl/σ = Nf⇉⇒Nf⇇ (⇉-Π-i j/σ-kd a/σ⇉l/σ)
          Λja/τ⇇Πjl/σ = ⇇-⇑ (⇉-Π-i j/τ-kd a/τ⇉l/τ) Πjl/τ<∷Πjl/σ
      in <:-λ a/σ<:a/τ⇇l/σ Λja/σ⇇Πjl/σ Λja/τ⇇Πjl/σ

    -- Equal hereditary substitutions map proper neutrals to subtypes.
    Ne∈-/⟨⟩≃ : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {a b c} →
               Γ ⊢Ne a ∈ b ⋯ c → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
               Δ ⊢ a /⟨ k ⟩ σ <: a /⟨ k ⟩ τ
    Ne∈-/⟨⟩≃ (∈-∙ {x} x∈j j⇉as⇉b⋯c) σ≃τ⇇Γ =
      let j-kds = kd-kds (Var∈-valid x∈j)
      in Var∈-/⟨⟩≃-⇑-?∙∙ x∈j σ≃τ⇇Γ ≤-refl (Sp⇉-/⟨⟩≃ j-kds j⇉as⇉b⋯c σ≃τ⇇Γ)

    Var∈-/⟨⟩≃-⇑-?∙∙ : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {x j l as bs b c} →
                      Γ ⊢Var x ∈ j → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
                      Δ ⊢ kd j Asc/⟨ k ⟩ σ ≤ kd l → Δ ⊢ l ⇉∙ as ≃ bs ⇉ b ⋯ c →
                      Δ ⊢ lookupSV σ x ?∙∙⟨ k ⟩ as <: lookupSV τ x ?∙∙⟨ k ⟩ bs
    Var∈-/⟨⟩≃-⇑-?∙∙ (⇉-var x _ Γ[x]≡kd-j) σ≃τ⇇Γ j/σ≤l l⇉as≃bs⇉b⋯c =
      ?≃-⇑-?∙∙ (subst (_ ⊢?⟨ _ ⟩ _ ≃ _ ⇇_) (cong (_Asc/⟨ _ ⟩ _) Γ[x]≡kd-j)
                      (lookup-/⟨⟩≃ σ≃τ⇇Γ x))
               j/σ≤l l⇉as≃bs⇉b⋯c
    Var∈-/⟨⟩≃-⇑-?∙∙ (⇇-⇑ x∈j₁ j₁<∷j₂ j₂-kd) σ≃τ⇇Γ j₂/σ≤l l⇉as≃bs⇉b⋯c =
      let σ⇇Γ       = /⟨⟩≃-valid₁ σ≃τ⇇Γ
          j₁/σ≤j₂/σ = ≤-<∷ (<∷-/⟨⟩≃ j₁<∷j₂ σ⇇Γ) (kd-/⟨⟩ j₂-kd σ⇇Γ)
      in Var∈-/⟨⟩≃-⇑-?∙∙ x∈j₁ σ≃τ⇇Γ (≤-trans j₁/σ≤j₂/σ j₂/σ≤l) l⇉as≃bs⇉b⋯c

    -- Equal hereditary substitutions map spines to spine identities.
    Sp⇉-/⟨⟩≃ : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {as j₁ j₂} →
               ⌊ Γ ⌋Ctx ⊢ j₁ kds → Γ ⊢ j₁ ⇉∙ as ⇉ j₂ → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
               Δ ⊢ j₁ Kind/⟨ k ⟩ σ ⇉∙ as //⟨ k ⟩ σ ≃
                                      as //⟨ k ⟩ τ ⇉ j₂ Kind/⟨ k ⟩ σ
    Sp⇉-/⟨⟩≃ _ ⇉-[] σ⇇Γ = ≃-[]
    Sp⇉-/⟨⟩≃ {k} (kds-Π j₁-kds j₂-kds)
             (⇉-∷ {a} {_} {j₁} {j₂} a⇇j₁ j₁-kd j₂[a]⇉as⇉j₃) σ⇇Γ =
      ≃-∷ (Nf⇇-/⟨⟩≃-≃ a⇇j₁ j₁-kd σ⇇Γ)
          (subst (_ ⊢_⇉∙ _ ≃ _ ⇉ _) j₂[a]/σ≡j₂/σ[a/σ]
                 (Sp⇉-/⟨⟩≃ (kds-/⟨⟩ j₂-kds (∈-hsub a∈⌊j₁⌋)) j₂[a]⇉as⇉j₃ σ⇇Γ))
      where
        a∈⌊j₁⌋ = Nf⇇-Nf∈ a⇇j₁

        j₂[a]/σ≡j₂/σ[a/σ] = begin
            j₂ Kind[ a ∈ ⌊ j₁ ⌋ ] Kind/⟨ k ⟩ _
          ≡⟨ kds-[]-/⟨⟩-↑⋆ [] j₂-kds a∈⌊j₁⌋ (/⟨⟩⇇-/⟨⟩∈ (/⟨⟩≃-valid₁ σ⇇Γ)) ⟩
            j₂ Kind/⟨ k ⟩ _ ↑ Kind/⟨ ⌊ j₁ ⌋ ⟩ sub (a /⟨ k ⟩ _)
          ≡⟨ cong (_ Kind[ a /⟨ k ⟩ _ ∈_]) (sym (⌊⌋-Kind/⟨⟩ j₁)) ⟩
            (j₂ Kind/⟨ k ⟩ _ ↑) Kind[ a /⟨ k ⟩ _ ∈ ⌊ j₁ Kind/⟨ k ⟩ _ ⌋ ]
          ∎

    -- Equal hereditary substitutions map checked normal forms to
    -- subtypes.
    Nf⇇-/⟨⟩≃-<: : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {a j} →
                  Γ ⊢Nf a ⇇ j → Γ ⊢ j kd → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
                  Δ ⊢ a /⟨ k ⟩ σ <: a /⟨ k ⟩ τ ⇇ j Kind/⟨ k ⟩ σ
    Nf⇇-/⟨⟩≃-<: (⇇-⇑ a⇉b₁⋯c₁ (<∷-⋯ b₂<:b₁ c₁<:c₂)) _ σ≃τ⇇Γ =
      let σ⇇Γ   = /⟨⟩≃-valid₁ σ≃τ⇇Γ
          τ⇇Γ   = /⟨⟩≃-valid₂ σ≃τ⇇Γ
          τ≃σ⇇Γ = /⟨⟩≃-sym σ≃τ⇇Γ
      in <:-⇇ (⇇-⇑ (Nf⇉-/⟨⟩ a⇉b₁⋯c₁ σ⇇Γ) (<∷-/⟨⟩≃ (<∷-⋯ b₂<:b₁ c₁<:c₂) σ⇇Γ))
              (⇇-⇑ (Nf⇉-/⟨⟩ a⇉b₁⋯c₁ τ⇇Γ) (<∷-/⟨⟩≃ (<∷-⋯ b₂<:b₁ c₁<:c₂) τ≃σ⇇Γ))
              (Nf⇉-⋯-/⟨⟩≃ a⇉b₁⋯c₁ σ≃τ⇇Γ)
    Nf⇇-/⟨⟩≃-<: (⇇-⇑ a⇉Πj₁l₁ (<∷-Π j₂<∷j₁ l₁<∷l₂ Πj₁l₁-kd)) Πj₂k₂-kd σ≃τ⇇Γ =
      let σ⇇Γ = /⟨⟩≃-valid₁ σ≃τ⇇Γ
          Πj₁l₁/σ<∷Πj₂l₂/σ = <∷-/⟨⟩≃ (<∷-Π j₂<∷j₁ l₁<∷l₂ Πj₁l₁-kd) σ⇇Γ
          Πj₂l₂/σ-kd       = kd-/⟨⟩ Πj₂k₂-kd σ⇇Γ
      in <:⇇-⇑ (Nf⇉-/⟨⟩≃ a⇉Πj₁l₁ Πj₁l₁-kd σ≃τ⇇Γ) Πj₁l₁/σ<∷Πj₂l₂/σ Πj₂l₂/σ-kd

    -- Equal hereditary substitutions map checked normal forms to type
    -- identities.
    Nf⇇-/⟨⟩≃-≃ : ∀ {m n Γ k Δ} {σ τ : SVSub m n} {a j} →
                 Γ ⊢Nf a ⇇ j → Γ ⊢ j kd → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
                 Δ ⊢ a /⟨ k ⟩ σ ≃ a /⟨ k ⟩ τ ⇇ j Kind/⟨ k ⟩ σ
    Nf⇇-/⟨⟩≃-≃ a⇇k k-kd σ≃τ⇇Γ =
      let τ≃σ⇇Γ  = /⟨⟩≃-sym σ≃τ⇇Γ
          k/σ-kd = kd-/⟨⟩ k-kd (/⟨⟩≃-valid₁ σ≃τ⇇Γ)
      in <:-antisym k/σ-kd (Nf⇇-/⟨⟩≃-<: a⇇k k-kd σ≃τ⇇Γ)
                    (<:⇇-⇑ (Nf⇇-/⟨⟩≃-<: a⇇k k-kd τ≃σ⇇Γ)
                    (kd-/⟨⟩≃-<∷ k-kd τ≃σ⇇Γ) k/σ-kd)

    -- Equal hereditary substitutions preserve subkinding.
    <∷-/⟨⟩≃ : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {j₁ j₂} →
              Γ ⊢ j₁ <∷ j₂ → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
              Δ ⊢ j₁ Kind/⟨ k ⟩ σ <∷ j₂ Kind/⟨ k ⟩ τ
    <∷-/⟨⟩≃ (<∷-⋯ a₂<:a₁ b₁<:b₂) σ≃τ⇇Γ =
      <∷-⋯ (<:-/⟨⟩≃ a₂<:a₁ (/⟨⟩≃-sym σ≃τ⇇Γ)) (<:-/⟨⟩≃ b₁<:b₂ σ≃τ⇇Γ)
    <∷-/⟨⟩≃ (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) σ≃τ⇇Γ =
      let τ≃σ⇇Γ = /⟨⟩≃-sym σ≃τ⇇Γ
          τ≃τ⇇Γ = /⟨⟩≃-valid₂ σ≃τ⇇Γ
      in <∷-Π (<∷-/⟨⟩≃ j₂<∷j₁ (/⟨⟩≃-sym σ≃τ⇇Γ))
              (<∷-/⟨⟩≃ k₁<∷k₂ (≃-H↑ (<∷-/⟨⟩≃-wf k₁<∷k₂ τ≃σ⇇Γ)
                                    (<∷-/⟨⟩≃-wf k₁<∷k₂ τ≃τ⇇Γ) σ≃τ⇇Γ))
              (kd-/⟨⟩ Πj₁k₁-kd (/⟨⟩≃-valid₁ σ≃τ⇇Γ))

    -- Equal hereditary substitutions preserve subtyping.

    <:-/⟨⟩≃ : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {a₁ a₂} →
              Γ ⊢ a₁ <: a₂ → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
              Δ ⊢ a₁ /⟨ k ⟩ σ <: a₂ /⟨ k ⟩ τ
    <:-/⟨⟩≃ (<:-trans a<:b b<:c) σ≃τ⇇Γ =
      <:-trans (<:-/⟨⟩≃ a<:b (/⟨⟩≃-valid₁ σ≃τ⇇Γ)) (<:-/⟨⟩≃ b<:c σ≃τ⇇Γ)
    <:-/⟨⟩≃ (<:-⊥ a⇉a⋯a) σ≃τ⇇Γ = <:-⊥ (Nf⇉-/⟨⟩ a⇉a⋯a (/⟨⟩≃-valid₂ σ≃τ⇇Γ))
    <:-/⟨⟩≃ (<:-⊤ a⇉a⋯a) σ≃τ⇇Γ = <:-⊤ (Nf⇉-/⟨⟩ a⇉a⋯a (/⟨⟩≃-valid₁ σ≃τ⇇Γ))
    <:-/⟨⟩≃ (<:-∀ k₂<∷k₁ a₁<:a₂ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁) σ≃τ⇇Γ =
      let τ≃σ⇇Γ = /⟨⟩≃-sym σ≃τ⇇Γ
          τ≃τ⇇Γ = /⟨⟩≃-valid₂ σ≃τ⇇Γ
      in <:-∀ (<∷-/⟨⟩≃ k₂<∷k₁ τ≃σ⇇Γ)
              (<:-/⟨⟩≃ a₁<:a₂ (≃-H↑ (<:-/⟨⟩≃-wf a₁<:a₂ τ≃σ⇇Γ)
                                    (<:-/⟨⟩≃-wf a₁<:a₂ τ≃τ⇇Γ) σ≃τ⇇Γ))
         (Nf⇉-/⟨⟩ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁ (/⟨⟩≃-valid₁ σ≃τ⇇Γ))
    <:-/⟨⟩≃ (<:-→ a₂<:a₁ b₁<:b₂) σ≃τ⇇Γ =
      <:-→ (<:-/⟨⟩≃ a₂<:a₁ (/⟨⟩≃-sym σ≃τ⇇Γ)) (<:-/⟨⟩≃ b₁<:b₂ σ≃τ⇇Γ)
    <:-/⟨⟩≃ {σ = σ} (<:-∙ {x} x∈j j⇉as≃bs⇉c⋯d) σ≃τ⇇Γ =
      let j-kds = kd-kds (Var∈-valid x∈j)
      in Var∈-/⟨⟩≃-⇑-?∙∙ x∈j σ≃τ⇇Γ ≤-refl (Sp≃-/⟨⟩≃ j-kds j⇉as≃bs⇉c⋯d σ≃τ⇇Γ)
    <:-/⟨⟩≃ (<:-⟨| a∈b⋯c) σ≃τ⇇Γ =
      let a/σ⇉b/σ⋯c/σ = Ne∈-/⟨⟩ a∈b⋯c (/⟨⟩≃-valid₁ σ≃τ⇇Γ)
      in <:-trans (<:-⟨|-Nf⇇ a/σ⇉b/σ⋯c/σ) (Ne∈-/⟨⟩≃ a∈b⋯c σ≃τ⇇Γ)
    <:-/⟨⟩≃ (<:-|⟩ a∈b⋯c) σ≃τ⇇Γ =
      let a/τ⇉b/τ⋯c/τ = Ne∈-/⟨⟩ a∈b⋯c (/⟨⟩≃-valid₂ σ≃τ⇇Γ)
      in <:-trans (Ne∈-/⟨⟩≃ a∈b⋯c σ≃τ⇇Γ) (<:-|⟩-Nf⇇ a/τ⇉b/τ⋯c/τ)

    <:⇇-/⟨⟩≃ : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {a₁ a₂ j} →
               Γ ⊢ a₁ <: a₂ ⇇ j → Γ ⊢ j kd → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
               Δ ⊢ a₁ /⟨ k ⟩ σ <: a₂ /⟨ k ⟩ τ ⇇ j Kind/⟨ k ⟩ σ
    <:⇇-/⟨⟩≃ (<:-⇇ a₁⇇b⋯c a₂⇇b⋯c a₁<:a₂) b⋯c-kd σ≃τ⇇Γ =
      let σ⇇Γ     = /⟨⟩≃-valid₁ σ≃τ⇇Γ
          τ⇇Γ     = /⟨⟩≃-valid₂ σ≃τ⇇Γ
          τ≃σ⇇Γ   = /⟨⟩≃-sym σ≃τ⇇Γ
      in <:-⇇ (Nf⇇-/⟨⟩ a₁⇇b⋯c σ⇇Γ)
              (Nf⇇-⇑ (Nf⇇-/⟨⟩ a₂⇇b⋯c τ⇇Γ) (kd-/⟨⟩≃-<∷ b⋯c-kd τ≃σ⇇Γ))
              (<:-/⟨⟩≃ a₁<:a₂ σ≃τ⇇Γ)
    <:⇇-/⟨⟩≃ (<:-λ a₁<:a₂⇇l Λj₁a₁⇇Πjl Λj₂a₂⇇Πjl) (kd-Π j-kd l-kd) σ≃τ⇇Γ =
      let σ⇇Γ     = /⟨⟩≃-valid₁ σ≃τ⇇Γ
          τ⇇Γ     = /⟨⟩≃-valid₂ σ≃τ⇇Γ
          τ≃σ⇇Γ   = /⟨⟩≃-sym σ≃τ⇇Γ
          j/σ≅j/σ = kd-/⟨⟩≃-≅ j-kd σ⇇Γ
          j/σ≅j/τ = kd-/⟨⟩≃-≅ j-kd σ≃τ⇇Γ
      in <:-λ (<:⇇-/⟨⟩≃ a₁<:a₂⇇l l-kd (≃-H↑ j/σ≅j/σ j/σ≅j/τ σ≃τ⇇Γ))
              (Nf⇇-/⟨⟩ Λj₁a₁⇇Πjl σ⇇Γ)
              (Nf⇇-⇑ (Nf⇇-/⟨⟩ Λj₂a₂⇇Πjl τ⇇Γ) (kd-/⟨⟩≃-<∷ (kd-Π j-kd l-kd) τ≃σ⇇Γ))

    -- Equal hereditary substitutions preserve spine equality.
    Sp≃-/⟨⟩≃ : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {as₁ as₂ j₁ j₂} →
               ⌊ Γ ⌋Ctx ⊢ j₁ kds →
               Γ ⊢ j₁ ⇉∙ as₁ ≃ as₂ ⇉ j₂ → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
               Δ ⊢ j₁ Kind/⟨ k ⟩ σ ⇉∙ as₁ //⟨ k ⟩ σ ≃
                                      as₂ //⟨ k ⟩ τ ⇉ j₂ Kind/⟨ k ⟩ σ
    Sp≃-/⟨⟩≃ _ ≃-[] σ≃τ⇇Γ = ≃-[]
    Sp≃-/⟨⟩≃ {k} (kds-Π j₁-kds j₂-kds)
             (≃-∷ {a} {j = j₁} {j₂} a≃b as≃bs) σ≃τ⇇Γ =
      let a∈⌊j₁⌋            = Nf⇇-Nf∈ (proj₁ (≃-valid a≃b))
          j₂[a]/σ≡j₂/σ[a/σ] = begin
              j₂ Kind[ a ∈ ⌊ j₁ ⌋ ] Kind/⟨ k ⟩ _
            ≡⟨ kds-[]-/⟨⟩-↑⋆ [] j₂-kds a∈⌊j₁⌋ (/⟨⟩⇇-/⟨⟩∈ (/⟨⟩≃-valid₁ σ≃τ⇇Γ)) ⟩
              j₂ Kind/⟨ k ⟩ _ ↑ Kind/⟨ ⌊ j₁ ⌋ ⟩ sub (a /⟨ k ⟩ _)
            ≡⟨ cong (_ Kind[ a /⟨ k ⟩ _ ∈_]) (sym (⌊⌋-Kind/⟨⟩ j₁)) ⟩
              (j₂ Kind/⟨ k ⟩ _ ↑) Kind[ a /⟨ k ⟩ _ ∈ ⌊ j₁ Kind/⟨ k ⟩ _ ⌋ ]
            ∎
      in ≃-∷ (≃-/⟨⟩≃ a≃b σ≃τ⇇Γ)
             (subst (_ ⊢_⇉∙ _ ≃ _ ⇉ _) j₂[a]/σ≡j₂/σ[a/σ]
                    (Sp≃-/⟨⟩≃ (kds-/⟨⟩ j₂-kds (∈-hsub a∈⌊j₁⌋)) as≃bs σ≃τ⇇Γ))

    -- Equal hereditary substitutions preserve type equality.
    ≃-/⟨⟩≃ : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {a₁ a₂ j} →
             Γ ⊢ a₁ ≃ a₂ ⇇ j → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
             Δ ⊢ a₁ /⟨ k ⟩ σ ≃ a₂ /⟨ k ⟩ τ ⇇ j Kind/⟨ k ⟩ σ
    ≃-/⟨⟩≃ (<:-antisym k-kd a<:b⇇k b<:a⇇k) σ≃τ⇇Γ =
      let τ≃σ⇇Γ = /⟨⟩≃-sym σ≃τ⇇Γ
          k/σ-kd = kd-/⟨⟩ k-kd (/⟨⟩≃-valid₁ σ≃τ⇇Γ)
      in <:-antisym k/σ-kd (<:⇇-/⟨⟩≃ a<:b⇇k k-kd σ≃τ⇇Γ)
                    (<:⇇-⇑ (<:⇇-/⟨⟩≃ b<:a⇇k k-kd τ≃σ⇇Γ)
                           (kd-/⟨⟩≃-<∷ k-kd τ≃σ⇇Γ) k/σ-kd)

    -- Applications in canonical kind checking are admissible.
    --
    -- NOTE. In the ?⇇-⇑-?∙∙ lemma, the second result r₂ is ignored.
    -- See the comment above on /⟨⟩⇇-/⟨⟩∈ for an explanation.

    ?⇇-⇑-?∙∙ : ∀ {k n} {Γ : Ctx n} {r₁ r₂ a j as b c} →
               Γ ⊢?⟨ k ⟩ r₁ ≃ r₂ ⇇ a → Γ ⊢ a ≤ kd j →
               Γ ⊢ j ⇉∙ as ⇉ b ⋯ c → Γ ⊢Nf r₁ ?∙∙⟨ k ⟩ as ⇇ b ⋯ c
    ?⇇-⇑-?∙∙ (≃-hit a≃a⇇j ⌊j⌋≡k) j≤l l⇉as⇉b⋯c =
      Nf⇇-∙∙ (Nf⇇-⇑-≤ (proj₁ (≃-valid a≃a⇇j)) j≤l) l⇉as⇉b⋯c
             (⌊⌋≡-trans (sym (≤-⌊⌋ j≤l)) ⌊j⌋≡k)
    ?⇇-⇑-?∙∙ (≃-miss y Γ-ctx Γ[y]≡a₁ a₁≤a₂) a₂≤l l⇉as⇉b⋯c =
      Nf⇇-ne (∈-∙ (Var∈-⇑-≤ y Γ-ctx Γ[y]≡a₁ (≤-trans a₁≤a₂ a₂≤l)) l⇉as⇉b⋯c)

    Nf⇇-∙∙ : ∀ {n} {Γ : Ctx n} {a as j₁ j₂ k} →
             Γ ⊢Nf a ⇇ j₁ → Γ ⊢ j₁ ⇉∙ as ⇉ j₂ → ⌊ j₁ ⌋≡ k →
             Γ ⊢Nf a ∙∙⟨ k ⟩ as ⇇ j₂
    Nf⇇-∙∙ a⇇j₁ ⇉-[] ⌊j₁⌋≡k = a⇇j₁
    Nf⇇-∙∙ a⇇Πj₁j₂ (⇉-∷ b⇇j₁ j₁-kd j₂[b]⇉as⇉j₃) (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) =
      Nf⇇-∙∙ (Nf⇇-Π-e a⇇Πj₁j₂ b⇇j₁ j₁-kd (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂))
             j₂[b]⇉as⇉j₃ (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂)

    Nf⇇-Π-e : ∀ {n} {Γ : Ctx n} {a b j₁ j₂ k} →
              Γ ⊢Nf a ⇇ Π j₁ j₂ → Γ ⊢Nf b ⇇ j₁ → Γ ⊢ j₁ kd →
              ⌊ Π j₁ j₂ ⌋≡ k → Γ ⊢Nf a ⌜·⌝⟨ k ⟩ b ⇇ j₂ Kind[ b ∈ ⌊ j₁ ⌋ ]
    Nf⇇-Π-e {_} {Γ} {_} {b}
            (⇇-⇑ (⇉-Π-i j₁-kd a⇉l₁)
            (<∷-Π {j₁} {j₂} {l₁} {l₂} j₂<∷j₁ l₁<∷l₂ Πj₁l₁-kd))
            b⇇j₂ j₂-kd (is-⇒ {_} {_} {k₁} ⌊j₂⌋≡k₁ ⌊l₂⌋≡k₂) =
      let σ⇇j₂∷Γ = ⇇-hsub b⇇j₂ j₂-kd ⌊j₂⌋≡k₁
      in ⇇-⇑ (Nf⇉-/⟨⟩ (⇓-Nf⇉ j₂-kd j₂<∷j₁ a⇉l₁) σ⇇j₂∷Γ)
             (subst (λ k → Γ ⊢ l₁ Kind[ b ∈ k₁ ] <∷ l₂ Kind[ b ∈ k ])
                    (sym (⌊⌋≡⇒⌊⌋-≡ ⌊j₂⌋≡k₁))
                    (<∷-/⟨⟩≃ l₁<∷l₂ σ⇇j₂∷Γ))

    -- Applications in checked type equality are admissible.

    ?≃-⇑-?∙∙ : ∀ {k n} {Γ : Ctx n} {r₁ r₂ a j as bs c d} →
               Γ ⊢?⟨ k ⟩ r₁ ≃ r₂ ⇇ a → Γ ⊢ a ≤ kd j →
               Γ ⊢ j ⇉∙ as ≃ bs ⇉ c ⋯ d →
               Γ ⊢ r₁ ?∙∙⟨ k ⟩ as <: r₂ ?∙∙⟨ k ⟩ bs
    ?≃-⇑-?∙∙ (≃-hit a≃b⇇j ⌊j⌋≡k) j≤l l⇉as≃bs⇉c⋯d =
      ≃⇒<:-⋯ (≃-∙∙ (≃-⇑-≤ a≃b⇇j j≤l) l⇉as≃bs⇉c⋯d
                   (⌊⌋≡-trans (sym (≤-⌊⌋ j≤l)) ⌊j⌋≡k))
    ?≃-⇑-?∙∙ (≃-miss y Γ-ctx Γ[y]≡a₁ a₁≤a₂) a₂≤l l⇉as≃bs⇉c⋯d =
      <:-∙ (Var∈-⇑-≤ y Γ-ctx Γ[y]≡a₁ (≤-trans a₁≤a₂ a₂≤l)) l⇉as≃bs⇉c⋯d

    ≃-∙∙ : ∀ {n} {Γ : Ctx n} {a b as bs j₁ j₂ k} →
           Γ ⊢ a ≃ b ⇇ j₁ → Γ ⊢ j₁ ⇉∙ as ≃ bs ⇉ j₂ → ⌊ j₁ ⌋≡ k →
           Γ ⊢ a ∙∙⟨ k ⟩ as ≃ b ∙∙⟨ k ⟩ bs ⇇ j₂
    ≃-∙∙ a≃b⇇j₁ ≃-[] ⌊j₁⌋≡k = a≃b⇇j₁
    ≃-∙∙ a≃b⇇Πj₁j₂ (≃-∷ c≃d⇇j₁ j₂[b]⇉cs≃ds⇉j₃) (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) =
      ≃-∙∙ (≃-Π-e a≃b⇇Πj₁j₂ c≃d⇇j₁ (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂))
           j₂[b]⇉cs≃ds⇉j₃ (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂)

    ≃-Π-e : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂ j₁ j₂ k} →
            Γ ⊢ a₁ ≃ a₂ ⇇ Π j₁ j₂ → Γ ⊢ b₁ ≃ b₂ ⇇ j₁ → ⌊ Π j₁ j₂ ⌋≡ k →
            Γ ⊢ a₁ ⌜·⌝⟨ k ⟩ b₁ ≃ a₂ ⌜·⌝⟨ k ⟩ b₂ ⇇ j₂ Kind[ b₁ ∈ ⌊ j₁ ⌋ ]
    ≃-Π-e a₁≃a₂⇇Πj₁j₂ b₁≃b₂⇇j₂ (is-⇒ ⌊j₂⌋≡k₁ ⌊j₂⌋≡k₂) with ≃-Π-can a₁≃a₂⇇Πj₁j₂
    ≃-Π-e {_} {Γ} {_} {_} {b₁} {b₂} Λl₁a₁≃Λl₂a₂⇇Πj₁j₂ b₁≃b₂⇇j₁
          (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂)
      | l₁ , a₁ , l₂ , a₂ , Λl₁a₁⇇Πj₁j₂ , Λl₂a₂⇇Πj₁j₂ , kd-Π j₁-kd j₂-kd ,
        j₁<∷l₁ , l₁≅l₂ , a₁<:a₂⇇j₂ , a₂<:a₁⇇j₂ , refl , refl =
        let ⌊Πj₁j₂⌋≡k     = is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂
            k₁≡⌊j₁⌋       = sym (⌊⌋≡⇒⌊⌋-≡ ⌊j₁⌋≡k₁)
            b₁⇇j₁ , b₂⇇j₁ = ≃-valid b₁≃b₂⇇j₁
            σ≃τ⇇j₁∷Γ      = ≃-hsub b₁≃b₂⇇j₁ ⌊j₁⌋≡k₁
            τ≃σ⇇j₁∷Γ      = /⟨⟩≃-sym σ≃τ⇇j₁∷Γ
            σ⇇j₁∷Γ        = /⟨⟩≃-valid₁ σ≃τ⇇j₁∷Γ
        in <:-antisym (subst (λ k → _ ⊢ _ Kind[ _ ∈ k ] kd)
                             (sym (⌊⌋≡⇒⌊⌋-≡ ⌊j₁⌋≡k₁))
                             (kd-/⟨⟩ j₂-kd (/⟨⟩≃-valid₁ σ≃τ⇇j₁∷Γ)))
                      (subst (λ k → _ ⊢ _ <: _ ⇇ _ Kind[ _ ∈ k ]) k₁≡⌊j₁⌋
                             (<:⇇-/⟨⟩≃ a₁<:a₂⇇j₂ j₂-kd σ≃τ⇇j₁∷Γ))
                      (<:⇇-⇑ (<:⇇-/⟨⟩≃ a₂<:a₁⇇j₂ j₂-kd τ≃σ⇇j₁∷Γ)
                             (subst (λ k → Γ ⊢ _ <∷ _ Kind[ _ ∈ k ]) k₁≡⌊j₁⌋
                                    (kd-/⟨⟩≃-<∷ j₂-kd τ≃σ⇇j₁∷Γ))
                             (subst (λ k → Γ ⊢ _ Kind[ _ ∈ k ] kd) k₁≡⌊j₁⌋
                                    (kd-/⟨⟩ j₂-kd σ⇇j₁∷Γ)))

    -- Helpers (to satisfy the termination checker).
    --
    -- These are simply (manual) expansions of the form
    --
    --   XX-/⟨⟩≃-wf x σ≃τ⇇Γ  =  kd-/⟨⟩≃-≅ (wf-kd-inv (wf-∷₁ (XX-ctx x))) σ≃τ⇇Γ
    --
    -- to ensure the above definitions remain structurally recursive
    -- in the various derivations.

    kd-/⟨⟩≃-wf : ∀ {m n Γ l Δ} {σ τ : SVSub m n} {j k} →
                 kd j ∷ Γ ⊢ k kd → Δ ⊢/⟨ l ⟩ σ ≃ τ ⇇ Γ →
                 Δ ⊢ j Kind/⟨ l ⟩ σ ≅ j Kind/⟨ l ⟩ τ
    kd-/⟨⟩≃-wf (kd-⋯ a⇉a⋯a _) σ≃τ⇇Γ = Nf⇉-/⟨⟩≃-wf a⇉a⋯a σ≃τ⇇Γ
    kd-/⟨⟩≃-wf (kd-Π j-kd _)  σ≃τ⇇Γ = kd-/⟨⟩≃-wf j-kd σ≃τ⇇Γ

    Nf⇉-/⟨⟩≃-wf : ∀ {m n Γ l Δ} {σ τ : SVSub m n} {j a k} →
                  kd j ∷ Γ ⊢Nf a ⇉ k → Δ ⊢/⟨ l ⟩ σ ≃ τ ⇇ Γ →
                  Δ ⊢ j Kind/⟨ l ⟩ σ ≅ j Kind/⟨ l ⟩ τ
    Nf⇉-/⟨⟩≃-wf (⇉-⊥-f (wf-kd j-kd ∷ Γ-ctx)) σ≃τ⇇Γ = kd-/⟨⟩≃-≅ j-kd σ≃τ⇇Γ
    Nf⇉-/⟨⟩≃-wf (⇉-⊤-f (wf-kd j-kd ∷ Γ-ctx)) σ≃τ⇇Γ = kd-/⟨⟩≃-≅ j-kd σ≃τ⇇Γ
    Nf⇉-/⟨⟩≃-wf (⇉-∀-f k-kd _)               σ≃τ⇇Γ = kd-/⟨⟩≃-wf k-kd σ≃τ⇇Γ
    Nf⇉-/⟨⟩≃-wf (⇉-→-f a⇉a⋯a _)              σ≃τ⇇Γ = Nf⇉-/⟨⟩≃-wf a⇉a⋯a σ≃τ⇇Γ
    Nf⇉-/⟨⟩≃-wf (⇉-Π-i j-kd _)               σ≃τ⇇Γ = kd-/⟨⟩≃-wf j-kd σ≃τ⇇Γ
    Nf⇉-/⟨⟩≃-wf (⇉-s-i a∈b⋯c)                σ≃τ⇇Γ = Ne∈-/⟨⟩≃-wf a∈b⋯c σ≃τ⇇Γ

    Ne∈-/⟨⟩≃-wf : ∀ {m n Γ l Δ} {σ τ : SVSub m n} {j a k} →
                  kd j ∷ Γ ⊢Ne a ∈ k → Δ ⊢/⟨ l ⟩ σ ≃ τ ⇇ Γ →
                  Δ ⊢ j Kind/⟨ l ⟩ σ ≅ j Kind/⟨ l ⟩ τ
    Ne∈-/⟨⟩≃-wf (∈-∙ x∈k _) σ≃τ⇇Γ = Var∈-/⟨⟩≃-wf x∈k σ≃τ⇇Γ

    Var∈-/⟨⟩≃-wf : ∀ {m n Γ l Δ} {σ τ : SVSub m n} {j a k} →
                   kd j ∷ Γ ⊢Var a ∈ k → Δ ⊢/⟨ l ⟩ σ ≃ τ ⇇ Γ →
                   Δ ⊢ j Kind/⟨ l ⟩ σ ≅ j Kind/⟨ l ⟩ τ
    Var∈-/⟨⟩≃-wf (⇉-var x (wf-kd j-kd ∷ Γ-ctx) _) σ≃τ⇇Γ = kd-/⟨⟩≃-≅ j-kd σ≃τ⇇Γ
    Var∈-/⟨⟩≃-wf (⇇-⇑ x∈k _ _)                    σ≃τ⇇Γ = Var∈-/⟨⟩≃-wf x∈k σ≃τ⇇Γ

    <∷-/⟨⟩≃-wf : ∀ {m n Γ l Δ} {σ τ : SVSub m n} {j k₁ k₂} →
                 kd j ∷ Γ ⊢ k₁ <∷ k₂ → Δ ⊢/⟨ l ⟩ σ ≃ τ ⇇ Γ →
                 Δ ⊢ j Kind/⟨ l ⟩ σ ≅ j Kind/⟨ l ⟩ τ
    <∷-/⟨⟩≃-wf (<∷-⋯ a₂<:a₁ _)   σ≃τ⇇Γ = <:-/⟨⟩≃-wf a₂<:a₁ σ≃τ⇇Γ
    <∷-/⟨⟩≃-wf (<∷-Π j₁<∷j₂ _ _) σ≃τ⇇Γ = <∷-/⟨⟩≃-wf j₁<∷j₂ σ≃τ⇇Γ

    <:-/⟨⟩≃-wf : ∀ {m n Γ l Δ} {σ τ : SVSub m n} {j a₁ a₂} →
                kd j ∷ Γ ⊢ a₁ <: a₂ → Δ ⊢/⟨ l ⟩ σ ≃ τ ⇇ Γ →
                Δ ⊢ j Kind/⟨ l ⟩ σ ≅ j Kind/⟨ l ⟩ τ
    <:-/⟨⟩≃-wf (<:-trans a<:b _) σ≃τ⇇Γ = <:-/⟨⟩≃-wf a<:b σ≃τ⇇Γ
    <:-/⟨⟩≃-wf (<:-⊥ a⇉a⋯a)      σ≃τ⇇Γ = Nf⇉-/⟨⟩≃-wf a⇉a⋯a σ≃τ⇇Γ
    <:-/⟨⟩≃-wf (<:-⊤ a⇉a⋯a)      σ≃τ⇇Γ = Nf⇉-/⟨⟩≃-wf a⇉a⋯a σ≃τ⇇Γ
    <:-/⟨⟩≃-wf (<:-∀ k₂<∷k₁ _ _) σ≃τ⇇Γ = <∷-/⟨⟩≃-wf k₂<∷k₁ σ≃τ⇇Γ
    <:-/⟨⟩≃-wf (<:-→ a₂<:a₁ _)   σ≃τ⇇Γ = <:-/⟨⟩≃-wf a₂<:a₁ σ≃τ⇇Γ
    <:-/⟨⟩≃-wf (<:-∙ x∈j _)      σ≃τ⇇Γ = Var∈-/⟨⟩≃-wf x∈j σ≃τ⇇Γ
    <:-/⟨⟩≃-wf (<:-⟨| a∈b⋯c)     σ≃τ⇇Γ = Ne∈-/⟨⟩≃-wf a∈b⋯c σ≃τ⇇Γ
    <:-/⟨⟩≃-wf (<:-|⟩ a∈b⋯c)     σ≃τ⇇Γ = Ne∈-/⟨⟩≃-wf a∈b⋯c σ≃τ⇇Γ

  -- Equal hereditary substitutions preserve kind equality.
  ≅-/⟨⟩≃ : ∀ {k m n Γ Δ} {σ τ : SVSub m n} {k₁ k₂} →
           Γ ⊢ k₁ ≅ k₂ → Δ ⊢/⟨ k ⟩ σ ≃ τ ⇇ Γ →
           Δ ⊢ k₁ Kind/⟨ k ⟩ σ ≅ k₂ Kind/⟨ k ⟩ τ
  ≅-/⟨⟩≃ (<∷-antisym j-kd k-kd j<∷k k<∷j) σ≃τ⇇Γ =
    <∷-antisym (kd-/⟨⟩ j-kd (/⟨⟩≃-valid₁ σ≃τ⇇Γ))
               (kd-/⟨⟩ k-kd (/⟨⟩≃-valid₂ σ≃τ⇇Γ))
               (<∷-/⟨⟩≃ j<∷k σ≃τ⇇Γ) (<∷-/⟨⟩≃ k<∷j (/⟨⟩≃-sym σ≃τ⇇Γ))

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


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence
open import HoTT.Identity.Product

module HoTT.Equivalence.Product where

private
  variable
    i : Level
    A A' B B' : 𝒰 i

×-swap : A × B → B × A
×-swap x = pr₂ x , pr₁ x

×-comm : A × B ≃ B × A
×-comm = ×-swap , qinv→isequiv (×-swap , ×-uniq , ×-uniq)

×-equiv₁ : A ≃ A' → A × B ≃ A' × B
×-equiv₁ {A = A} {A' = A'} {B = B} (f₁ , e₁) = f , qinv→isequiv (g , η , ε)
  where
  open qinv (isequiv→qinv e₁) renaming (g to g₁ ; η to η₁ ; ε to ε₁)
  f : A × B → A' × B
  f (a , b) = f₁ a , b
  g : A' × B → A × B
  g (a' , b) = g₁ a' , b
  η : g ∘ f ~ id
  η (a , b) = ×-pair⁼ (η₁ a , refl)
  ε : f ∘ g ~ id
  ε (a' , b) = ×-pair⁼ (ε₁ a' , refl)

×-equiv₂ : B ≃ B' → A × B ≃ A × B'
×-equiv₂ {B = B} {B' = B'} {A = A} (f₂ , e₂) = f , qinv→isequiv (g , η , ε)
  where
  open qinv (isequiv→qinv e₂) renaming (g to g₂ ; η to η₂ ; ε to ε₂)
  f : A × B → A × B'
  f (a , b) = a , f₂ b
  g : A × B' → A × B
  g (a , b') = a , g₂ b'
  η : g ∘ f ~ id
  η (a , b) = ×-pair⁼ (refl , η₂ b)
  ε : f ∘ g ~ id
  ε (a , b') = ×-pair⁼ (refl , ε₂ b')

ext: agda

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
{-# OPTIONS --cubical --safe #-}
module Algebra where

open import Prelude

module _ {a} {A : Type a} (_∙_ : A → A → A) where
  Associative : Type a
  Associative = ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)

  Commutative : Type _
  Commutative = ∀ x y → x ∙ y ≡ y ∙ x

  Idempotent : Type _
  Idempotent = ∀ x → x ∙ x ≡ x

module _ {a b} {A : Type a} {B : Type b} where
  Identityˡ : (A → B → B) → A → Type _
  Identityˡ _∙_ x = ∀ y → x ∙ y ≡ y

  Zeroˡ : (A → B → A) → A → Type _
  Zeroˡ _∙_ x = ∀ y → x ∙ y ≡ x

  Zeroʳ : (A → B → B) → B → Type _
  Zeroʳ _∙_ x = ∀ y → y ∙ x ≡ x

  Identityʳ : (A → B → A) → B → Type _
  Identityʳ _∙_ x = ∀ y → y ∙ x ≡ y

  _Distributesʳ_ : (A → B → B) → (B → B → B) → Type _
  _⊗_ Distributesʳ _⊕_ = ∀ x y z → x ⊗ (y ⊕ z) ≡ (x ⊗ y) ⊕ (x ⊗ z)

  _Distributesˡ_ : (B → A → B) → (B → B → B) → Type _
  _⊗_ Distributesˡ _⊕_ = ∀ x y z → (x ⊕ y) ⊗ z ≡ (x ⊗ z) ⊕ (y ⊗ z)

record  Semigroup ℓ : Type (ℓsuc ℓ) where
  infixl 6 _∙_
  field
    𝑆      : Type ℓ
    _∙_    : 𝑆 → 𝑆 → 𝑆
    assoc  : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)

record  Monoid ℓ : Type (ℓsuc ℓ) where
  infixl 6 _∙_
  field
    𝑆      : Type ℓ
    _∙_    : 𝑆 → 𝑆 → 𝑆
    ε      : 𝑆
    assoc  : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
    ε∙     : ∀ x → ε ∙ x ≡ x
    ∙ε     : ∀ x → x ∙ ε ≡ x

  semigroup : Semigroup ℓ
  semigroup = record
    { 𝑆 = 𝑆; _∙_ = _∙_; assoc = assoc }

record MonoidHomomorphism_⟶_
         {ℓ₁ ℓ₂}
         (from : Monoid ℓ₁)
         (to : Monoid ℓ₂)
       : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  open Monoid from
  open Monoid to
    renaming ( 𝑆 to 𝑅
             ; _∙_ to _⊙_
             ; ε to ⓔ
             )
  field
    f : 𝑆 → 𝑅
    ∙-homo : ∀ x y → f (x ∙ y) ≡ f x ⊙ f y
    ε-homo : f ε ≡ ⓔ

record Group ℓ : Type (ℓsuc ℓ) where
  field
    monoid : Monoid ℓ
  open Monoid monoid public
  field
    inv : 𝑆 → 𝑆
    ∙⁻ : ∀ x → x ∙ inv x ≡ ε
    ⁻∙ : ∀ x → inv x ∙ x ≡ ε

record CommutativeMonoid ℓ : Type (ℓsuc ℓ) where
  field
    monoid : Monoid ℓ
  open Monoid monoid public
  field
    comm : Commutative _∙_

record Semilattice ℓ : Type (ℓsuc ℓ) where
  field
    commutativeMonoid : CommutativeMonoid ℓ
  open CommutativeMonoid commutativeMonoid public
  field
    idem : Idempotent _∙_

record NearSemiring ℓ : Type (ℓsuc ℓ) where
  infixl 6 _+_
  infixl 7 _*_
  field
    𝑅 : Type ℓ
    _+_ : 𝑅 → 𝑅 → 𝑅
    _*_ : 𝑅 → 𝑅 → 𝑅
    1# : 𝑅
    0# : 𝑅
    +-assoc : Associative _+_
    *-assoc : Associative _*_
    0+ : Identityˡ _+_ 0#
    +0 : Identityʳ _+_ 0#
    1* : Identityˡ _*_ 1#
    *1 : Identityʳ _*_ 1#
    0* : Zeroˡ _*_ 0#
    ⟨+⟩* : _*_ Distributesˡ _+_

record Semiring ℓ : Type (ℓsuc ℓ) where
  field
    nearSemiring : NearSemiring ℓ
  open NearSemiring nearSemiring public
  field
    +-comm : Commutative _+_
    *0 : Zeroʳ _*_ 0#
    *⟨+⟩ : _*_ Distributesʳ _+_

record IdempotentSemiring ℓ : Type (ℓsuc ℓ) where
  field
    semiring : Semiring ℓ
  open Semiring semiring public
  field
    +-idem : Idempotent _+_

record CommutativeSemiring ℓ : Type (ℓsuc ℓ) where
  field
    semiring : Semiring ℓ
  open Semiring semiring public
  field
    *-comm : Commutative _*_

record LeftSemimodule ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    semiring : Semiring ℓ₁
  open Semiring semiring public
  field
    semimodule : CommutativeMonoid ℓ₂
  open CommutativeMonoid semimodule renaming (_∙_ to _∪_) public
    renaming (𝑆 to 𝑉
             ; assoc to ∪-assoc
             ; ε∙ to ∅∪
             ; ∙ε to ∪∅
             ; ε to ∅
             )
  infixr 7 _⋊_
  field
    _⋊_ : 𝑅 → 𝑉 → 𝑉
    ⟨*⟩⋊ : ∀ x y z → (x * y) ⋊ z ≡ x ⋊ (y ⋊ z)
    ⟨+⟩⋊ : ∀ x y z → (x + y) ⋊ z ≡ (x ⋊ z) ∪ (y ⋊ z)
    ⋊⟨∪⟩ : _⋊_ Distributesʳ _∪_
    1⋊ : Identityˡ _⋊_ 1#
    0⋊ : ∀ x → 0# ⋊ x ≡ ∅

record StarSemiring ℓ : Type (ℓsuc ℓ) where
  field
    semiring : Semiring ℓ
  open Semiring semiring public
  field
    _⋆ : 𝑅 → 𝑅
    star-iterʳ : ∀ x → x ⋆ ≡ 1# + x * x ⋆
    star-iterˡ : ∀ x → x ⋆ ≡ 1# + x ⋆ * x
  _⁺ : 𝑅 → 𝑅
  x ⁺ = x * x ⋆

record Functor ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    𝐹   : Type ℓ₁ → Type ℓ₂
    map : (A → B) → 𝐹 A → 𝐹 B
    map-id : map (id {ℓ₁} {A}) ≡ id
    map-comp : (f : B → C) → (g : A → B) → map (f ∘ g) ≡ map f ∘ map g

record Applicative ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    functor : Functor ℓ₁ ℓ₂
  open Functor functor public
  infixl 5 _<*>_
  field
    pure : A → 𝐹 A
    _<*>_ : 𝐹 (A → B) → 𝐹 A → 𝐹 B
    map-ap : (f : A → B) → map f ≡ pure f <*>_
    pure-homo : (f : A → B) → (x : A) → map f (pure x) ≡ pure (f x)
    <*>-interchange : (u : 𝐹 (A → B)) → (y : A) → u <*> pure y ≡ map (_$ y) u
    <*>-comp : (u : 𝐹 (B → C)) → (v : 𝐹 (A → B)) → (w : 𝐹 A) → pure _∘′_ <*> u <*> v <*> w ≡ u <*> (v <*> w)

record Monad ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    applicative : Applicative ℓ₁ ℓ₂
  open Applicative applicative public
  infixl 1 _>>=_
  field
    _>>=_ : 𝐹 A → (A → 𝐹 B) → 𝐹 B
    >>=-idˡ : (f : A → 𝐹 B) → (x : A) → (pure x >>= f) ≡ f x
    >>=-idʳ : (x : 𝐹 A) → (x >>= pure) ≡ x
    >>=-assoc : (xs : 𝐹 A) (f : A → 𝐹 B) (g : B → 𝐹 C) → ((xs >>= f) >>= g) ≡ (xs >>= (λ x → f x >>= g))
  return : A → 𝐹 A
  return = pure

record Alternative ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    applicative : Applicative ℓ₁ ℓ₂
  open Applicative applicative public
  field
    0# : 𝐹 A
    _<|>_ : 𝐹 A → 𝐹 A → 𝐹 A
    <|>-idˡ : (x : 𝐹 A) → 0# <|> x ≡ x
    <|>-idʳ : (x : 𝐹 A) → x <|> 0# ≡ x
    0-annˡ : (x : 𝐹 A) → 0# <*> x ≡ 0# {B}
    <|>-distrib : (x y : 𝐹 (A → B)) → (z : 𝐹 A) → (x <|> y) <*> z ≡ (x <*> z) <|> (y <*> z)

record MonadPlus ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    monad : Monad ℓ₁ ℓ₂
  open Monad monad public
  field
    0# : 𝐹 A
    _<|>_ : 𝐹 A → 𝐹 A → 𝐹 A
    <|>-idˡ : (x : 𝐹 A) → 0# <|> x ≡ x
    <|>-idʳ : (x : 𝐹 A) → x <|> 0# ≡ x
    0-annˡ : (x : A → 𝐹 B) → (0# >>= x) ≡ 0#
    <|>-distrib : (x y : 𝐹 A) → (z : A → 𝐹 B) → ((x <|> y) >>= z) ≡ (x >>= z) <|> (y >>= z)

Endo : Type a → Type a
Endo A = A → A

endoMonoid : ∀ {a} → Type a → Monoid a
endoMonoid A .Monoid.𝑆 = Endo A
endoMonoid A .Monoid.ε x = x
endoMonoid A .Monoid._∙_ f g x = f (g x)
endoMonoid A .Monoid.assoc _ _ _ = refl
endoMonoid A .Monoid.ε∙ _ = refl
endoMonoid A .Monoid.∙ε _ = refl

record Foldable ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    𝐹 : Type ℓ₁ → Type ℓ₂
  open Monoid ⦃ ... ⦄
  field
    foldMap : {A : Type ℓ₁} ⦃ _ : Monoid ℓ₁ ⦄ → (A → 𝑆) → 𝐹 A → 𝑆
  foldr : {A B : Type ℓ₁} → (A → B → B) → B → 𝐹 A → B
  foldr f b xs = foldMap ⦃ endoMonoid _ ⦄ f xs b

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module syntax-util where

open import lib
open import cedille-types
open import general-util
open import constants

posinfo-gen : posinfo
posinfo-gen = "generated"

first-position : posinfo
first-position = "1"

dummy-var : var
dummy-var = "_dummy"

id-term : term
id-term = Lam posinfo-gen NotErased posinfo-gen "x" NoClass (Var posinfo-gen "x")

compileFailType : type
compileFailType = Abs posinfo-gen Erased posinfo-gen "X" (Tkk (Star posinfo-gen))  (TpVar posinfo-gen "X")

qualif-info : Set
qualif-info = var × args

qualif : Set
qualif = trie qualif-info

tag : Set
tag = string × rope

tagged-val : Set
tagged-val = string × rope × 𝕃 tag

tags-to-rope : 𝕃 tag → rope
tags-to-rope [] = [[]]
tags-to-rope ((t , v) :: []) = [[ "\"" ^ t ^ "\":" ]] ⊹⊹ v
tags-to-rope ((t , v) :: ts) = [[ "\"" ^ t ^ "\":" ]] ⊹⊹ v ⊹⊹ [[ "," ]] ⊹⊹ tags-to-rope ts

-- We number these when so we can sort them back in emacs
tagged-val-to-rope : ℕ → tagged-val → rope
tagged-val-to-rope n (t , v , []) = [[ "\"" ^ t ^ "\":[\"" ^ ℕ-to-string n ^ "\",\"" ]] ⊹⊹ v ⊹⊹ [[ "\"]" ]]
tagged-val-to-rope n (t , v , tags) = [[ "\"" ^ t ^ "\":[\"" ^ ℕ-to-string n ^ "\",\"" ]] ⊹⊹ v ⊹⊹ [[ "\",{" ]] ⊹⊹ tags-to-rope tags ⊹⊹ [[ "}]" ]]

tagged-vals-to-rope : ℕ → 𝕃 tagged-val → rope
tagged-vals-to-rope n [] = [[]]
tagged-vals-to-rope n (s :: []) = tagged-val-to-rope n s
tagged-vals-to-rope n (s :: (s' :: ss)) = tagged-val-to-rope n s ⊹⊹ [[ "," ]] ⊹⊹ tagged-vals-to-rope (suc n) (s' :: ss)

make-tag : (name : string) → (values : 𝕃 tag) → (start : ℕ) → (end : ℕ) → tag
make-tag name vs start end = name , [[ "{\"start\":\"" ^ ℕ-to-string start ^ "\",\"end\":\"" ^ ℕ-to-string end ^ "\"" ]] ⊹⊹ vs-to-rope vs ⊹⊹ [[ "}" ]]
  where
    vs-to-rope : 𝕃 tag → rope
    vs-to-rope [] = [[]]
    vs-to-rope ((t , v) :: ts) = [[ ",\"" ^ t ^ "\":\"" ]] ⊹⊹ v ⊹⊹ [[ "\"" ]] ⊹⊹ vs-to-rope ts

posinfo-to-ℕ : posinfo → ℕ
posinfo-to-ℕ pi with string-to-ℕ pi
posinfo-to-ℕ pi | just n = n
posinfo-to-ℕ pi | nothing = 0 -- should not happen

posinfo-plus : posinfo → ℕ → posinfo
posinfo-plus pi n = ℕ-to-string (posinfo-to-ℕ pi + n)

posinfo-plus-str : posinfo → string → posinfo
posinfo-plus-str pi s = posinfo-plus pi (string-length s)

star : kind
star = Star posinfo-gen

-- qualify variable by module name
_#_ : string → string → string
fn # v = fn ^ qual-global-str ^  v

_%_ : posinfo → var → string
pi % v = pi ^ qual-local-str ^ v

compileFail : var
compileFail = "compileFail"
compileFail-qual = "" % compileFail

mk-inst : params → args → trie arg × params
mk-inst (ParamsCons (Decl _ _ _ x _ _) ps) (ArgsCons a as) with mk-inst ps as
...| σ , ps' = trie-insert σ x a , ps'
mk-inst ps as = empty-trie , ps

apps-term : term → args → term
apps-term f (ArgsNil) = f
apps-term f (ArgsCons (TermArg me t) as) = apps-term (App f me t) as
apps-term f (ArgsCons (TypeArg t) as) = apps-term (AppTp f t) as

apps-type : type → args → type
apps-type f (ArgsNil) = f
apps-type f (ArgsCons (TermArg _ t) as) = apps-type (TpAppt f t) as
apps-type f (ArgsCons (TypeArg t) as) = apps-type (TpApp f t) as

append-params : params → params → params
append-params (ParamsCons p ps) qs = ParamsCons p (append-params ps qs)
append-params ParamsNil qs = qs

append-args : args → args → args
append-args (ArgsCons p ps) qs = ArgsCons p (append-args ps qs)
append-args (ArgsNil) qs = qs

append-cmds : cmds → cmds → cmds
append-cmds CmdsStart = id
append-cmds (CmdsNext c cs) = CmdsNext c ∘ append-cmds cs

qualif-lookup-term : qualif → string → term
qualif-lookup-term σ x with trie-lookup σ x
... | just (x' , as) = apps-term (Var posinfo-gen x') as
... | _ = Var posinfo-gen x

qualif-lookup-type : qualif → string → type
qualif-lookup-type σ x with trie-lookup σ x
... | just (x' , as) = apps-type (TpVar posinfo-gen x') as
... | _ = TpVar posinfo-gen x

qualif-lookup-kind : args → qualif → string → kind
qualif-lookup-kind xs σ x with trie-lookup σ x
... | just (x' , as) = KndVar posinfo-gen x' (append-args as xs)
... | _ = KndVar posinfo-gen x xs

inst-lookup-term : trie arg → string → term
inst-lookup-term σ x with trie-lookup σ x
... | just (TermArg me t) = t
... | _ = Var posinfo-gen x

inst-lookup-type : trie arg → string → type
inst-lookup-type σ x with trie-lookup σ x
... | just (TypeArg t) = t
... | _ = TpVar posinfo-gen x

params-to-args : params → args
params-to-args ParamsNil = ArgsNil
params-to-args (ParamsCons (Decl _ p me v (Tkt t) _) ps) = ArgsCons (TermArg me (Var posinfo-gen v)) (params-to-args ps)
params-to-args (ParamsCons (Decl _ p _ v (Tkk k) _) ps) = ArgsCons (TypeArg (TpVar posinfo-gen v)) (params-to-args ps)

qualif-insert-params : qualif → var → var → params → qualif
qualif-insert-params σ qv v ps = trie-insert σ v (qv , params-to-args ps)

qualif-insert-import : qualif → var → optAs → 𝕃 string → args → qualif
qualif-insert-import σ mn oa [] as = σ
qualif-insert-import σ mn oa (v :: vs) as = qualif-insert-import (trie-insert σ (import-as v oa) (mn # v , as)) mn oa vs as
  where
  import-as : var → optAs → var
  import-as v NoOptAs = v
  import-as v (SomeOptAs _ pfx) = pfx # v

tk-is-type : tk → 𝔹
tk-is-type (Tkt _) = tt
tk-is-type (Tkk _) = ff

me-unerased : maybeErased → 𝔹
me-unerased Erased = ff
me-unerased NotErased = tt

me-erased : maybeErased → 𝔹
me-erased x = ~ (me-unerased x)

term-start-pos : term → posinfo
type-start-pos : type → posinfo
kind-start-pos : kind → posinfo
liftingType-start-pos : liftingType → posinfo

term-start-pos (App t x t₁) = term-start-pos t
term-start-pos (AppTp t tp) = term-start-pos t
term-start-pos (Hole pi) = pi
term-start-pos (Lam pi x _ x₁ x₂ t) = pi
term-start-pos (Let pi _ _) = pi
term-start-pos (Open pi _ _) = pi
term-start-pos (Parens pi t pi') = pi
term-start-pos (Var pi x₁) = pi
term-start-pos (Beta pi _ _) = pi
term-start-pos (IotaPair pi _ _ _ _) = pi
term-start-pos (IotaProj t _ _) = term-start-pos t
term-start-pos (Epsilon pi _ _ _) = pi
term-start-pos (Phi pi _ _ _ _) = pi
term-start-pos (Rho pi _ _ _ _ _) = pi
term-start-pos (Chi pi _ _) = pi
term-start-pos (Delta pi _ _) = pi
term-start-pos (Sigma pi _) = pi
term-start-pos (Theta pi _ _ _) = pi
term-start-pos (Mu pi _ _ _ _ _ _) = pi
term-start-pos (Mu' pi _ _ _ _ _) = pi

type-start-pos (Abs pi _ _ _ _ _) = pi
type-start-pos (TpLambda pi _ _ _ _) = pi
type-start-pos (Iota pi _ _ _ _) = pi
type-start-pos (Lft pi _ _ _ _) = pi
type-start-pos (TpApp t t₁) = type-start-pos t
type-start-pos (TpAppt t x) = type-start-pos t
type-start-pos (TpArrow t _ t₁) = type-start-pos t
type-start-pos (TpEq pi _ _ pi') = pi
type-start-pos (TpParens pi _ pi') = pi
type-start-pos (TpVar pi x₁) = pi
type-start-pos (NoSpans t _) = type-start-pos t -- we are not expecting this on input
type-start-pos (TpHole pi) = pi --ACG
type-start-pos (TpLet pi _ _) = pi

kind-start-pos (KndArrow k k₁) = kind-start-pos k
kind-start-pos (KndParens pi k pi') = pi
kind-start-pos (KndPi pi _ x x₁ k) = pi
kind-start-pos (KndTpArrow x k) = type-start-pos x
kind-start-pos (KndVar pi x₁ _) = pi
kind-start-pos (Star pi) = pi

liftingType-start-pos (LiftArrow l l') = liftingType-start-pos l
liftingType-start-pos (LiftParens pi l pi') = pi
liftingType-start-pos (LiftPi pi x₁ x₂ l) = pi
liftingType-start-pos (LiftStar pi) = pi
liftingType-start-pos (LiftTpArrow t l) = type-start-pos t

term-end-pos : term → posinfo
type-end-pos : type → posinfo
kind-end-pos : kind → posinfo
liftingType-end-pos : liftingType → posinfo
tk-end-pos : tk → posinfo
lterms-end-pos : lterms → posinfo
args-end-pos : (if-nil : posinfo) → args → posinfo
arg-end-pos : arg → posinfo
kvar-end-pos : posinfo → var → args → posinfo

term-end-pos (App t x t') = term-end-pos t'
term-end-pos (AppTp t tp) = type-end-pos tp
term-end-pos (Hole pi) = posinfo-plus pi 1
term-end-pos (Lam pi x _ x₁ x₂ t) = term-end-pos t
term-end-pos (Let _ _ t) = term-end-pos t
term-end-pos (Open pi _ t) = term-end-pos t
term-end-pos (Parens pi t pi') = pi'
term-end-pos (Var pi x) = posinfo-plus-str pi x
term-end-pos (Beta pi _ (SomeTerm t pi')) = pi'
term-end-pos (Beta pi (SomeTerm t pi') _) = pi'
term-end-pos (Beta pi NoTerm NoTerm) = posinfo-plus pi 1
term-end-pos (IotaPair _ _ _ _ pi) = pi
term-end-pos (IotaProj _ _ pi) = pi
term-end-pos (Epsilon pi _ _ t) = term-end-pos t
term-end-pos (Phi _ _ _ _ pi) = pi
term-end-pos (Rho pi _ _ _ t t') = term-end-pos t'
term-end-pos (Chi pi T t') = term-end-pos t'
term-end-pos (Delta pi oT t) = term-end-pos t
term-end-pos (Sigma pi t) = term-end-pos t
term-end-pos (Theta _ _ _ ls) = lterms-end-pos ls
term-end-pos (Mu _ _ _ _ _ _ pi) = pi
term-end-pos (Mu' _ _ _ _ _ pi) = pi

type-end-pos (Abs pi _ _ _ _ t) = type-end-pos t
type-end-pos (TpLambda _ _ _ _ t) = type-end-pos t
type-end-pos (Iota _ _ _ _ tp) = type-end-pos tp
type-end-pos (Lft pi _ _ _ t) = liftingType-end-pos t
type-end-pos (TpApp t t') = type-end-pos t'
type-end-pos (TpAppt t x) = term-end-pos x
type-end-pos (TpArrow t _ t') = type-end-pos t'
type-end-pos (TpEq pi _ _ pi') = pi'
type-end-pos (TpParens pi _ pi') = pi'
type-end-pos (TpVar pi x) = posinfo-plus-str pi x
type-end-pos (TpHole pi) = posinfo-plus pi 1
type-end-pos (NoSpans t pi) = pi
type-end-pos (TpLet _ _ t) = type-end-pos t

kind-end-pos (KndArrow k k') = kind-end-pos k'
kind-end-pos (KndParens pi k pi') = pi'
kind-end-pos (KndPi pi _ x x₁ k) = kind-end-pos k
kind-end-pos (KndTpArrow x k) = kind-end-pos k
kind-end-pos (KndVar pi x ys) = args-end-pos (posinfo-plus-str pi x) ys
kind-end-pos (Star pi) = posinfo-plus pi 1

tk-end-pos (Tkt T) = type-end-pos T
tk-end-pos (Tkk k) = kind-end-pos k

args-end-pos pi (ArgsCons x ys) = args-end-pos (arg-end-pos x) ys
args-end-pos pi ArgsNil = pi

arg-end-pos (TermArg me t) = term-end-pos t
arg-end-pos (TypeArg T) = type-end-pos T

kvar-end-pos pi v = args-end-pos (posinfo-plus-str pi v)

liftingType-end-pos (LiftArrow l l') = liftingType-end-pos l'
liftingType-end-pos (LiftParens pi l pi') = pi'
liftingType-end-pos (LiftPi x x₁ x₂ l) = liftingType-end-pos l
liftingType-end-pos (LiftStar pi) = posinfo-plus pi 1
liftingType-end-pos (LiftTpArrow x l) = liftingType-end-pos l

lterms-end-pos (LtermsNil pi) = posinfo-plus pi 1 -- must add one for the implicit Beta that we will add at the end
lterms-end-pos (LtermsCons _ _ ls) = lterms-end-pos ls

{- return the end position of the given term if it is there, otherwise
   the given posinfo -}
optTerm-end-pos : posinfo → optTerm → posinfo
optTerm-end-pos pi NoTerm = pi
optTerm-end-pos pi (SomeTerm x x₁) = x₁

optTerm-end-pos-beta : posinfo → optTerm → optTerm → posinfo
optTerm-end-pos-beta pi _ (SomeTerm x pi') = pi'
optTerm-end-pos-beta pi (SomeTerm x pi') NoTerm = pi'
optTerm-end-pos-beta pi NoTerm NoTerm = posinfo-plus pi 1

optAs-or : optAs → posinfo → var → posinfo × var
optAs-or NoOptAs pi x = pi , x
optAs-or (SomeOptAs pi x) _ _ = pi , x

tk-arrow-kind : tk → kind → kind
tk-arrow-kind (Tkk k) k' = KndArrow k k'
tk-arrow-kind (Tkt t) k = KndTpArrow t k

TpApp-tk : type → var → tk → type
TpApp-tk tp x (Tkk _) = TpApp tp (TpVar posinfo-gen x)
TpApp-tk tp x (Tkt _) = TpAppt tp (Var posinfo-gen x)

-- expression descriptor
data exprd : Set where
  TERM : exprd
  TYPE : exprd
  KIND : exprd
  LIFTINGTYPE : exprd
  TK : exprd
  ARG : exprd
  QUALIF : exprd

⟦_⟧ : exprd → Set
⟦ TERM ⟧ = term
⟦ TYPE ⟧ = type
⟦ KIND ⟧ = kind
⟦ LIFTINGTYPE ⟧ = liftingType
⟦ TK ⟧ = tk
⟦ ARG ⟧ = arg
⟦ QUALIF ⟧ = qualif-info

exprd-name : exprd → string
exprd-name TERM = "term"
exprd-name TYPE = "type"
exprd-name KIND = "kind"
exprd-name LIFTINGTYPE = "lifting type"
exprd-name TK = "type-kind"
exprd-name ARG = "argument"
exprd-name QUALIF = "qualification"

-- checking-sythesizing enum
data checking-mode : Set where
  checking : checking-mode
  synthesizing : checking-mode
  untyped : checking-mode

maybe-to-checking : {A : Set} → maybe A → checking-mode
maybe-to-checking (just _) = checking
maybe-to-checking nothing = synthesizing

is-app : {ed : exprd} → ⟦ ed ⟧ → 𝔹
is-app{TERM} (App _ _ _) = tt
is-app{TERM} (AppTp _ _) = tt
is-app{TYPE} (TpApp _ _) = tt
is-app{TYPE} (TpAppt _ _) = tt
is-app _ = ff

is-term-level-app : {ed : exprd} → ⟦ ed ⟧ → 𝔹
is-term-level-app{TERM} (App _ _ _) = tt
is-term-level-app{TERM} (AppTp _ _) = tt
is-term-level-app _ = ff

is-type-level-app : {ed : exprd} → ⟦ ed ⟧ → 𝔹
is-type-level-app{TYPE} (TpApp _ _) = tt
is-type-level-app{TYPE} (TpAppt _ _) = tt
is-type-level-app _ = ff

is-parens : {ed : exprd} → ⟦ ed ⟧ → 𝔹
is-parens{TERM} (Parens _ _ _) = tt
is-parens{TYPE} (TpParens _ _ _) = tt
is-parens{KIND} (KndParens _ _ _) = tt
is-parens{LIFTINGTYPE} (LiftParens _ _ _) = tt
is-parens _ = ff

is-arrow : {ed : exprd} → ⟦ ed ⟧ → 𝔹
is-arrow{TYPE} (TpArrow _ _ _) = tt
is-arrow{KIND} (KndTpArrow _ _) = tt
is-arrow{KIND} (KndArrow _ _) = tt
is-arrow{LIFTINGTYPE} (LiftArrow _ _) = tt
is-arrow{LIFTINGTYPE} (LiftTpArrow _ _) = tt
is-arrow _ = ff

is-abs : {ed : exprd} → ⟦ ed ⟧ → 𝔹
is-abs{TERM} (Let _ _ _) = tt
is-abs{TERM} (Lam _ _ _ _ _ _) = tt
is-abs{TYPE} (Abs _ _ _ _ _ _) = tt
is-abs{TYPE} (TpLambda _ _ _ _ _) = tt
is-abs{TYPE} (Iota _ _ _ _ _) = tt
is-abs{KIND} (KndPi _ _ _ _ _) = tt
is-abs{LIFTINGTYPE} (LiftPi _ _ _ _) = tt
is-abs _ = ff

is-eq-op : {ed : exprd} → ⟦ ed ⟧ → 𝔹
is-eq-op{TERM} (Sigma _ _) = tt
is-eq-op{TERM} (Epsilon _ _ _ _) = tt
is-eq-op{TERM} (Rho _ _ _ _ _ _) = tt
is-eq-op{TERM} (Chi _ _ _) = tt
is-eq-op{TERM} (Phi _ _ _ _ _) = tt
is-eq-op{TERM} (Delta _ _ _) = tt
is-eq-op _ = ff

is-beta : {ed : exprd} → ⟦ ed ⟧ → 𝔹
is-beta{TERM} (Beta _ _ _) = tt
is-beta _ = ff

is-hole : {ed : exprd} → ⟦ ed ⟧ → 𝔹
is-hole{TERM} (Hole _) = tt
is-hole{TERM} _        = ff
is-hole{TYPE} (TpHole _) = tt
is-hole{TYPE} _          = ff
is-hole{KIND} e = ff
is-hole{LIFTINGTYPE} e = ff
is-hole{TK} (Tkk x) = is-hole x
is-hole{TK} (Tkt x) = is-hole x
is-hole{ARG} (TermArg e? t) = is-hole t
is-hole{ARG} (TypeArg tp) = is-hole tp
is-hole{QUALIF} _ = ff

eq-maybeErased : maybeErased → maybeErased → 𝔹
eq-maybeErased Erased Erased = tt
eq-maybeErased Erased NotErased = ff
eq-maybeErased NotErased Erased = ff
eq-maybeErased NotErased NotErased = tt

eq-checking-mode : (m₁ m₂ : checking-mode) → 𝔹
eq-checking-mode checking checking = tt
eq-checking-mode checking synthesizing = ff
eq-checking-mode checking untyped = ff
eq-checking-mode synthesizing checking = ff
eq-checking-mode synthesizing synthesizing = tt
eq-checking-mode synthesizing untyped = ff
eq-checking-mode untyped checking = ff
eq-checking-mode untyped synthesizing = ff
eq-checking-mode untyped untyped = tt

optPublic-is-public : optPublic → 𝔹
optPublic-is-public IsPublic = tt
optPublic-is-public NotPublic = ff

------------------------------------------------------
-- functions intended for building terms for testing
------------------------------------------------------
mlam : var → term → term
mlam x t = Lam posinfo-gen NotErased posinfo-gen x NoClass t

Mlam : var → term → term
Mlam x t = Lam posinfo-gen Erased posinfo-gen x NoClass t

mappe : term → term → term
mappe t1 t2 = App t1 Erased t2

mapp : term → term → term
mapp t1 t2 = App t1 NotErased t2

mvar : var → term
mvar x = Var posinfo-gen x

mtpvar : var → type
mtpvar x = TpVar posinfo-gen x

mall : var → tk → type → type
mall x tk tp = Abs posinfo-gen All posinfo-gen x tk tp

mtplam : var → tk → type → type
mtplam x tk tp = TpLambda posinfo-gen posinfo-gen x tk tp

{- strip off lambda-abstractions from the term, return the lambda-bound vars and the innermost body.
   The intention is to call this with at least the erasure of a term, if not the hnf -- so we do
   not check for parens, etc. -}
decompose-lams : term → (𝕃 var) × term
decompose-lams (Lam _ _ _ x _ t) with decompose-lams t
decompose-lams (Lam _ _ _ x _ t) | vs , body = (x :: vs) , body
decompose-lams t = [] , t

{- decompose a term into spine form consisting of a non-applications head and arguments.
   The outer arguments will come earlier in the list than the inner ones.
   As for decompose-lams, we assume the term is at least erased. -}
decompose-apps : term → term × (𝕃 term)
decompose-apps (App t _ t') with decompose-apps t
decompose-apps (App t _ t') | h , args = h , (t' :: args)
decompose-apps t = t , []

decompose-var-headed : (var → 𝔹) → term → maybe (var × (𝕃 term))
decompose-var-headed is-bound t with decompose-apps t
decompose-var-headed is-bound t | Var _ x , args = if is-bound x then nothing else (just (x , args))
decompose-var-headed is-bound t | _ = nothing

data tty : Set where
  tterm : term → tty
  ttype : type → tty

decompose-tpapps : type → type × 𝕃 tty
decompose-tpapps (TpApp t t') with decompose-tpapps t
decompose-tpapps (TpApp t t') | h , args = h , (ttype t') :: args
decompose-tpapps (TpAppt t t') with decompose-tpapps t
decompose-tpapps (TpAppt t t') | h , args = h , (tterm t') :: args
decompose-tpapps (TpParens _ t _) = decompose-tpapps t
decompose-tpapps t = t , []

recompose-tpapps : type × 𝕃 tty → type
recompose-tpapps (h , []) = h
recompose-tpapps (h , ((tterm t') :: args)) = TpAppt (recompose-tpapps (h , args)) t'
recompose-tpapps (h , ((ttype t') :: args)) = TpApp (recompose-tpapps (h , args)) t'

recompose-apps : maybeErased → 𝕃 tty → term → term
recompose-apps me [] h = h
recompose-apps me ((tterm t') :: args) h = App (recompose-apps me args h) me t'
recompose-apps me ((ttype t') :: args) h = AppTp (recompose-apps me args h) t'

vars-to-𝕃 : vars → 𝕃 var
vars-to-𝕃 (VarsStart v) = [ v ]
vars-to-𝕃 (VarsNext v vs) = v :: vars-to-𝕃 vs

{- lambda-abstract the input variables in reverse order around the
   given term (so closest to the top of the list is bound deepest in
   the resulting term). -}
Lam* : 𝕃 var → term → term
Lam* [] t = t
Lam* (x :: xs) t = Lam* xs (Lam posinfo-gen NotErased posinfo-gen x NoClass t)

App* : term → 𝕃 (maybeErased × term) → term
App* t [] = t
App* t ((m , arg) :: args) = App (App* t args) m arg

App*' : term → 𝕃 term → term
App*' t [] = t
App*' t (arg :: args) = App*' (App t NotErased arg) args

TpApp* : type → 𝕃 type → type
TpApp* t [] = t
TpApp* t (arg :: args) = (TpApp (TpApp* t args) arg)

LiftArrow* : 𝕃 liftingType → liftingType → liftingType
LiftArrow* [] l = l
LiftArrow* (l' :: ls) l = LiftArrow* ls (LiftArrow l' l)

is-intro-form : term → 𝔹
is-intro-form (Lam _ _ _ _ _ _) = tt
--is-intro-form (IotaPair _ _ _ _ _) = tt
is-intro-form _ = ff

erase : { ed : exprd } → ⟦ ed ⟧ → ⟦ ed ⟧
erase-term : term → term
erase-type : type → type
erase-kind : kind → kind
erase-lterms : term → lterms → term
erase-tk : tk → tk
-- erase-optType : optType → optType
erase-liftingType : liftingType → liftingType
erase-cases : cases → cases
erase-varargs : varargs → varargs

erase-if : 𝔹 → { ed : exprd } → ⟦ ed ⟧ → ⟦ ed ⟧
erase-if tt = erase
erase-if ff = id

erase-term (Parens _ t _) = erase-term t
erase-term (App t1 Erased t2) = erase-term t1
erase-term (App t1 NotErased t2) = App (erase-term t1) NotErased (erase-term t2)
erase-term (AppTp t tp) = erase-term t
erase-term (Lam _ Erased _ _ _ t) = erase-term t
erase-term (Lam _ NotErased _ x oc t) = Lam posinfo-gen NotErased posinfo-gen x NoClass (erase-term t)
erase-term (Let _ (DefTerm _ x _ t) t') = Let posinfo-gen (DefTerm posinfo-gen x NoType (erase-term t)) (erase-term t')
erase-term (Let _ (DefType _ _ _ _) t) = erase-term t
erase-term (Open _ _ t) = erase-term t
erase-term (Var _ x) = Var posinfo-gen x
erase-term (Beta _ _ NoTerm) = id-term
erase-term (Beta _ _ (SomeTerm t _)) = erase-term t
erase-term (IotaPair _ t1 t2 _ _) = erase-term t1
erase-term (IotaProj t n _) = erase-term t
erase-term (Epsilon _ lr _ t) = erase-term t
erase-term (Sigma _ t) = erase-term t
erase-term (Hole _) = Hole posinfo-gen
erase-term (Phi _ t t₁ t₂ _) = erase-term t₂
erase-term (Rho _ _ _ t _ t') = erase-term t'
erase-term (Chi _ T t') = erase-term t'
erase-term (Delta _ T t) = id-term
erase-term (Theta _ u t ls) = erase-lterms (erase-term t) ls
erase-term (Mu _ x t ot _ c _) = Mu posinfo-gen x (erase-term t) NoType posinfo-gen (erase-cases c) posinfo-gen
erase-term (Mu' _ t ot _ c _)  = Mu' posinfo-gen (erase-term t) NoType posinfo-gen (erase-cases c) posinfo-gen

erase-cases NoCase = NoCase
erase-cases (SomeCase _ x varargs t cs) = SomeCase posinfo-gen x (erase-varargs varargs) (erase-term t) (erase-cases cs)

erase-varargs NoVarargs = NoVarargs
erase-varargs (NormalVararg x varargs) = NormalVararg x (erase-varargs varargs)
erase-varargs (ErasedVararg x varargs) = erase-varargs varargs
erase-varargs (TypeVararg x varargs  ) = erase-varargs varargs

-- Only erases TERMS in types, leaving the structure of types the same
erase-type (Abs _ b _ v atk tp) = Abs posinfo-gen b posinfo-gen v (erase-tk atk) (erase-type tp)
erase-type (Iota _ _ v otp tp) = Iota posinfo-gen posinfo-gen v (erase-type otp) (erase-type tp)
erase-type (Lft _ _ v t lt) = Lft posinfo-gen posinfo-gen v (erase-term t) (erase-liftingType lt)
erase-type (NoSpans tp _) = NoSpans (erase-type tp) posinfo-gen
erase-type (TpApp tp tp') = TpApp (erase-type tp) (erase-type tp')
erase-type (TpAppt tp t) = TpAppt (erase-type tp) (erase-term t)
erase-type (TpArrow tp at tp') = TpArrow (erase-type tp) at (erase-type tp')
erase-type (TpEq _ t t' _) = TpEq posinfo-gen (erase-term t) (erase-term t') posinfo-gen
erase-type (TpLambda _ _ v atk tp) = TpLambda posinfo-gen posinfo-gen v (erase-tk atk) (erase-type tp)
erase-type (TpParens _ tp _) = erase-type tp
erase-type (TpHole _) = TpHole posinfo-gen
erase-type (TpVar _ x) = TpVar posinfo-gen x
erase-type (TpLet _ (DefTerm _ x _ t) T) = TpLet posinfo-gen (DefTerm posinfo-gen x NoType (erase-term t)) (erase-type T)
erase-type (TpLet _ (DefType _ x k T) T') = TpLet posinfo-gen (DefType posinfo-gen x (erase-kind k) (erase-type T)) (erase-type T')

-- Only erases TERMS in types in kinds, leaving the structure of kinds and types in those kinds the same
erase-kind (KndArrow k k') = KndArrow (erase-kind k) (erase-kind k')
erase-kind (KndParens _ k _) = erase-kind k
erase-kind (KndPi _ _ v atk k) = KndPi posinfo-gen posinfo-gen v (erase-tk atk) (erase-kind k)
erase-kind (KndTpArrow tp k) = KndTpArrow (erase-type tp) (erase-kind k)
erase-kind (KndVar _ x ps) = KndVar posinfo-gen x ps
erase-kind (Star _) = Star posinfo-gen

erase{TERM} t = erase-term t
erase{TYPE} tp = erase-type tp
erase{KIND} k = erase-kind k
erase{LIFTINGTYPE} lt = erase-liftingType lt
erase{TK} atk = erase-tk atk
erase{ARG} a = a
erase{QUALIF} q = q

erase-tk (Tkt tp) = Tkt (erase-type tp)
erase-tk (Tkk k) = Tkk (erase-kind k)

erase-liftingType (LiftArrow lt lt') = LiftArrow (erase-liftingType lt) (erase-liftingType lt')
erase-liftingType (LiftParens _ lt _) = erase-liftingType lt
erase-liftingType (LiftPi _ v tp lt) = LiftPi posinfo-gen v (erase-type tp) (erase-liftingType lt)
erase-liftingType (LiftTpArrow tp lt) = LiftTpArrow (erase-type tp) (erase-liftingType lt)
erase-liftingType lt = lt

erase-lterms t (LtermsNil _) = t
erase-lterms t (LtermsCons Erased t' ls) = erase-lterms t ls
erase-lterms t (LtermsCons NotErased t' ls) = erase-lterms (App t NotErased (erase-term t')) ls

lterms-to-term : theta → term → lterms → term
lterms-to-term AbstractEq t (LtermsNil _) = App t Erased (Beta posinfo-gen NoTerm NoTerm)
lterms-to-term _ t (LtermsNil _) = t
lterms-to-term u t (LtermsCons e t' ls) = lterms-to-term u (App t e t') ls

imps-to-cmds : imports → cmds
imps-to-cmds ImportsStart = CmdsStart
imps-to-cmds (ImportsNext i is) = CmdsNext (ImportCmd i) (imps-to-cmds is)

-- TODO handle qualif & module args
get-imports : start → 𝕃 string
get-imports (File _ is _ _ mn _ cs _) = imports-to-include is ++ get-imports-cmds cs
  where import-to-include : imprt → string
        import-to-include (Import _ _ _ x oa _ _) = x
        imports-to-include : imports → 𝕃 string
        imports-to-include ImportsStart = []
        imports-to-include (ImportsNext x is) = import-to-include x :: imports-to-include is
        singleton-if-include : cmd → 𝕃 string
        singleton-if-include (ImportCmd imp) = [ import-to-include imp ]
        singleton-if-include _ = []
        get-imports-cmds : cmds → 𝕃 string
        get-imports-cmds (CmdsNext c cs) = singleton-if-include c ++ get-imports-cmds cs
        get-imports-cmds CmdsStart = []

data language-level : Set where
  ll-term : language-level
  ll-type : language-level
  ll-kind : language-level

ll-to-string : language-level → string
ll-to-string ll-term = "term"
ll-to-string ll-type = "type"
ll-to-string ll-kind = "kind"

is-rho-plus : optPlus → 𝔹
is-rho-plus RhoPlus = tt
is-rho-plus _ = ff

split-var-h : 𝕃 char → 𝕃 char × 𝕃 char
split-var-h [] = [] , []
split-var-h (qual-global-chr :: xs) = [] , xs
split-var-h (x :: xs) with split-var-h xs
... | xs' , ys = (x :: xs') , ys

split-var : var → var × var
split-var v with split-var-h (reverse (string-to-𝕃char v))
... | xs , ys = 𝕃char-to-string (reverse ys) , 𝕃char-to-string (reverse xs)

var-suffix : var → maybe var
var-suffix v with split-var v
... | "" , _ = nothing
... | _ , sfx = just sfx

-- unique qualif domain prefixes
qual-pfxs : qualif → 𝕃 var
qual-pfxs q = uniq (prefixes (trie-strings q))
  where
  uniq : 𝕃 var → 𝕃 var
  uniq vs = stringset-strings (stringset-insert* empty-stringset vs)
  prefixes : 𝕃 var → 𝕃 var
  prefixes [] = []
  prefixes (v :: vs) with split-var v
  ... | "" , sfx = vs
  ... | pfx , sfx = pfx :: prefixes vs

unqual-prefix : qualif → 𝕃 var → var → var → var
unqual-prefix q [] sfx v = v
unqual-prefix q (pfx :: pfxs) sfx v
  with trie-lookup q (pfx # sfx)
... | just (v' , _) = if v =string v' then pfx # sfx else v
... | nothing = v

unqual-bare : qualif → var → var → var
unqual-bare q sfx v with trie-lookup q sfx
... | just (v' , _) = if v =string v' then sfx else v
... | nothing = v

unqual-local : var → var
unqual-local v = f' (string-to-𝕃char v) where
  f : 𝕃 char → maybe (𝕃 char)
  f [] = nothing
  f ('@' :: t) = f t maybe-or just t
  f (h :: t) = f t
  f' : 𝕃 char → string
  f' (meta-var-pfx :: t) = maybe-else' (f t) v (𝕃char-to-string ∘ _::_ meta-var-pfx)
  f' t = maybe-else' (f t) v 𝕃char-to-string

unqual-all : qualif → var → string
unqual-all q v with var-suffix v
... | nothing = v
... | just sfx = unqual-bare q sfx (unqual-prefix q (qual-pfxs q) sfx v)

erased-params : params → 𝕃  string
erased-params (ParamsCons (Decl _ _ Erased x (Tkt _) _) ps) with var-suffix x
... | nothing = x :: erased-params ps
... | just x' = x' :: erased-params ps
erased-params (ParamsCons p ps) = erased-params ps
erased-params ParamsNil = []

lam-expand-term : params → term → term
lam-expand-term (ParamsCons (Decl _ _ me x tk _) ps) t =
  Lam posinfo-gen (if tk-is-type tk then me else Erased) posinfo-gen x (SomeClass tk) (lam-expand-term ps t)
lam-expand-term ParamsNil t = t

lam-expand-type : params → type → type
lam-expand-type (ParamsCons (Decl _ _ me x tk _) ps) t =
  TpLambda posinfo-gen posinfo-gen x tk (lam-expand-type ps t)
lam-expand-type ParamsNil t = t

abs-expand-type : params → type → type
abs-expand-type (ParamsCons (Decl _ _ me x tk _) ps) t =
  Abs posinfo-gen (if tk-is-type tk then me else All) posinfo-gen x tk (abs-expand-type ps t)
abs-expand-type ParamsNil t = t

abs-expand-type' : params → type → type
abs-expand-type' (ParamsCons (Decl _ _ me x tk _) ps) t =
  Abs posinfo-gen (if tk-is-type tk then me else All) posinfo-gen x tk (abs-expand-type' ps t)
abs-expand-type' ParamsNil t = t

abs-expand-kind : params → kind → kind
abs-expand-kind (ParamsCons (Decl _ _ me x tk _) ps) k =
  KndPi posinfo-gen posinfo-gen x tk (abs-expand-kind ps k)
abs-expand-kind ParamsNil k = k

args-length : args → ℕ
args-length (ArgsCons p ps) = suc (args-length ps)
args-length ArgsNil = 0

erased-args-length : args → ℕ
erased-args-length (ArgsCons (TermArg NotErased _) ps) = suc (erased-args-length ps)
erased-args-length (ArgsCons (TermArg Erased _) ps) = erased-args-length ps
erased-args-length (ArgsCons (TypeArg _) ps) = erased-args-length ps
erased-args-length ArgsNil = 0

me-args-length : maybeErased → args → ℕ
me-args-length Erased = erased-args-length
me-args-length NotErased = args-length

spineApp : Set
spineApp = qvar × 𝕃 arg

term-to-spapp : term → maybe spineApp
term-to-spapp (App t me t') = term-to-spapp t ≫=maybe
  (λ { (v , as) → just (v , TermArg me t' :: as) })
term-to-spapp (AppTp t T) = term-to-spapp t ≫=maybe
  (λ { (v , as) → just (v , TypeArg T :: as) })
term-to-spapp (Var _ v) = just (v , [])
term-to-spapp _ = nothing

type-to-spapp : type → maybe spineApp
type-to-spapp (TpApp T T') = type-to-spapp T ≫=maybe
  (λ { (v , as) → just (v , TypeArg T' :: as) })
type-to-spapp (TpAppt T t) = type-to-spapp T ≫=maybe
  (λ { (v , as) → just (v , TermArg NotErased t :: as) })
type-to-spapp (TpVar _ v) = just (v , [])
type-to-spapp _ = nothing

spapp-term : spineApp → term
spapp-term (v , []) = Var posinfo-gen v
spapp-term (v , TermArg me t :: as) = App (spapp-term (v , as)) me t
spapp-term (v , TypeArg T :: as) = AppTp (spapp-term (v , as)) T

spapp-type : spineApp → type
spapp-type (v , []) = TpVar posinfo-gen v
spapp-type (v , TermArg me t :: as) = TpAppt (spapp-type (v , as)) t
spapp-type (v , TypeArg T :: as) = TpApp (spapp-type (v , as)) T

num-gt : num → ℕ → 𝕃 string
num-gt n n' = maybe-else [] (λ n'' → if n'' > n' then [ n ] else []) (string-to-ℕ n)
nums-gt : nums → ℕ → 𝕃 string
nums-gt (NumsStart n) n' = num-gt n n'
nums-gt (NumsNext n ns) n' =
  maybe-else [] (λ n'' → if n'' > n' || iszero n'' then [ n ] else []) (string-to-ℕ n)
  ++ nums-gt ns n'

nums-to-stringset : nums → stringset × 𝕃 string {- Repeated numbers -}
nums-to-stringset (NumsStart n) = stringset-insert empty-stringset n , []
nums-to-stringset (NumsNext n ns) with nums-to-stringset ns
...| ss , rs = if stringset-contains ss n
  then ss , n :: rs
  else stringset-insert ss n , rs

optNums-to-stringset : optNums → maybe stringset × (ℕ → maybe string)
optNums-to-stringset NoNums = nothing , λ _ → nothing
optNums-to-stringset (SomeNums ns) with nums-to-stringset ns
...| ss , [] = just ss , λ n → case nums-gt ns n of λ where
  [] → nothing
  ns-g → just ("Occurrences not found: " ^ 𝕃-to-string id ", " ns-g ^ " (total occurrences: " ^ ℕ-to-string n ^ ")")
...| ss , rs = just ss , λ n →
  just ("The list of occurrences contains the following repeats: " ^ 𝕃-to-string id ", " rs)

------------------------------------------------------
-- any delta contradiction → boolean contradiction
------------------------------------------------------
nlam : ℕ → term → term
nlam 0 t = t
nlam (suc n) t = mlam ignored-var (nlam n t)

delta-contra-app : ℕ → (ℕ → term) → term
delta-contra-app 0 nt = mvar "x"
delta-contra-app (suc n) nt = mapp (delta-contra-app n nt) (nt n)

delta-contrahh : ℕ → trie ℕ → trie ℕ → var → var → 𝕃 term → 𝕃 term → maybe term
delta-contrahh n ls rs x1 x2 as1 as2 with trie-lookup ls x1 | trie-lookup rs x2
...| just n1 | just n2 =
  let t1 = nlam (length as1) (mlam "x" (mlam "y" (mvar "x")))
      t2 = nlam (length as2) (mlam "x" (mlam "y" (mvar "y"))) in
  if n1 =ℕ n2
    then nothing
    else just (mlam "x" (delta-contra-app n
      (λ n → if n =ℕ n1 then t1 else if n =ℕ n2 then t2 else id-term)))
...| _ | _ = nothing

{-# TERMINATING #-}
delta-contrah : ℕ → trie ℕ → trie ℕ → term → term → maybe term
delta-contrah n ls rs (Lam _ _ _ x1 _ t1) (Lam _ _ _ x2 _ t2) =
  delta-contrah (suc n) (trie-insert ls x1 n) (trie-insert rs x2 n) t1 t2
delta-contrah n ls rs (Lam _ _ _ x1 _ t1) t2 =
  delta-contrah (suc n) (trie-insert ls x1 n) (trie-insert rs x1 n) t1 (mapp t2 (mvar x1))
delta-contrah n ls rs t1 (Lam _ _ _ x2 _ t2) =
  delta-contrah (suc n) (trie-insert ls x2 n) (trie-insert rs x2 n) (mapp t1 (mvar x2)) t2
delta-contrah n ls rs t1 t2 with decompose-apps t1 | decompose-apps t2
...| Var _ x1 , as1 | Var _ x2 , as2 = delta-contrahh n ls rs x1 x2 as1 as2
...| _ | _ = nothing

-- For terms t1 and t2, given that check-beta-inequiv t1 t2 ≡ tt,
-- delta-contra produces a function f such that f t1 ≡ tt and f t2 ≡ ff
-- If it returns nothing, no contradiction could be found
delta-contra : term → term → maybe term
delta-contra = delta-contrah 0 empty-trie empty-trie
-- postulate: check-beta-inequiv t1 t2 ≡ isJust (delta-contra t1 t2)

check-beta-inequiv : term → term → 𝔹
check-beta-inequiv t1 t2 = isJust (delta-contra t1 t2)

tk-map : tk → (type → type) → (kind → kind) → tk
tk-map (Tkt T) fₜ fₖ = Tkt $ fₜ T
tk-map (Tkk k) fₜ fₖ = Tkk $ fₖ k

tk-map2 : tk → (∀ {ed} → ⟦ ed ⟧ → ⟦ ed ⟧) → tk
tk-map2 atk f = tk-map atk f f

optTerm-map : optTerm → (term → term) → optTerm
optTerm-map NoTerm f = NoTerm
optTerm-map (SomeTerm t pi) f = SomeTerm (f t) pi

optType-map : optType → (type → type) → optType
optType-map NoType f = NoType
optType-map (SomeType T) f = SomeType $ f T

optGuide-map : optGuide → (var → type → type) → optGuide
optGuide-map NoGuide f = NoGuide
optGuide-map (Guide pi x T) f = Guide pi x $ f x T

optClass-map : optClass → (tk → tk) → optClass
optClass-map NoClass f = NoClass
optClass-map (SomeClass atk) f = SomeClass $ f atk

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
module SizedPolyIO.Object where

open import Data.Product

open import Level using (_⊔_) renaming (suc to lsuc)

record Interface μ ρ : Set (lsuc (μ ⊔ ρ)) where
  field
    Method  : Set μ
    Result  : (m : Method) → Set ρ
open Interface public

-- A simple object just returns for a method the response
-- and the object itself
record Object {μ ρ} (i : Interface μ ρ) : Set (μ ⊔ ρ) where
  coinductive
  field
    objectMethod : (m : Method i) → Result i m × Object i

open Object public

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
open import Prelude

module Implicits.Resolution.Stack.Algorithm where

open import Induction.WellFounded
open import Induction.Nat
open import Data.Fin.Substitution
open import Data.Nat.Base using (_<′_)
open import Data.List.Any
open Membership-≡
open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Resolution.Stack.Resolution
open import Implicits.Resolution.Termination
open import Implicits.Syntax.Type.Unification
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.Equality hiding (cong; flip; const)
open import Data.List.Any.Properties using (Any↔)
open import Data.Nat hiding (_<_)
open import Data.Nat.Properties
open import Relation.Binary using (module DecTotalOrder)
open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl)

module M = MetaTypeMetaSubst

module Lemmas where
  postulate lem₄ : ∀ {m ν} (a : MetaType m (suc ν)) u us → from-meta ((M.open-meta a) M./ (us M.↑) M./ (M.sub u)) ≡ (from-meta (a M./ (us M.↑tp))) tp[/tp from-meta u ]

open Lemmas

_s<'_ : ∀ {ν} → (∃ λ (Δ : ICtx ν) → Stack Δ) →  (∃ λ (Δ' : ICtx ν) → Stack Δ') → Set
s s<' t = {!!}

module Arg<-well-founded  where
  open Lexicographic (_s<_) (const _sρ<_)

  arg<-well-founded : Well-founded _<_
  arg<-well-founded = well-founded s<-well-founded sρ<-well-founded

  _arg<_ = _<_

open Lexicographic using (left; right)
open Arg<-well-founded

{-# NO_TERMINATION_CHECK #-}
mutual

  match' : ∀ {m ν ρ} (Δ : ICtx ν) s (r∈Δ : ρ List.∈ Δ) τ → (r : MetaType m ν) →
           Acc _arg<_ (s , (, simpl τ)) →
           Acc _m<_ (, , r) →
          Maybe (∃ λ u → Δ & s , r∈Δ ⊢ from-meta (r M./ u) ↓ τ)
  match' Δ s r∈Δ τ (simpl x) (acc f) _ with mgu (simpl x) τ
  match' Δ s r∈Δ τ (simpl x) (acc f) _ | just (u , p) =
    just (
      (asub u) ,
      subst (λ a → Δ & s , r∈Δ  ⊢ a ↓ τ) (sym $ mgu-unifies (simpl x) τ (u , p)) (i-simp τ)
    )
  match' Δ s r∈Δ τ (simpl x) (acc f) _ | nothing = nothing

  match' Δ s r∈Δ τ (a ⇒ b) (acc f) (acc g) with match' Δ s r∈Δ τ b (acc f) (g _ (b-m<-a⇒b a b))
  match' Δ s r∈Δ τ (a ⇒ b) (acc f) (acc g) | nothing = nothing
  match' Δ s r∈Δ τ (a ⇒ b) (acc f) (acc g) | just (u , b/u↓τ) with
    (from-meta (a M./ u)) for r∈Δ ?⊬dom s
  match' Δ s r∈Δ τ (a ⇒ b) (acc f) (acc g) | just (u , b/u↓τ) | yes p
    with
      let a' = from-meta (a M./ u) in
        let s' = (s push a' for r∈Δ) in
          resolve' Δ s' a' (f (s' , _ , a') (left {!!}))
  match' Δ s r∈Δ τ (a ⇒ b) (acc f) (acc g) | just (u , b/u↓τ) | yes p | just ⊢ᵣa = just (u , i-iabs p ⊢ᵣa b/u↓τ)
  match' Δ s r∈Δ τ (a ⇒ b) (acc f) (acc g) | just (u , b/u↓τ) | yes p | nothing = nothing
  match' Δ s r∈Δ τ (a ⇒ b) (acc f) (acc g) | just (u , b/u↓τ) | no ¬p = nothing

  -- The following with clause fails to satisfy termination checking.
  -- Somehow we have to prove to Agda that (open-meta a) is structurally smaller than (∀' a)
  match' Δ s r∈Δ τ (∀' a) (acc f) (acc g) with
    match' Δ s r∈Δ τ (open-meta a) (acc f) (g _ (open-meta-a-m<-∀'a a))
  match' Δ s r∈Δ τ (∀' a) (acc f) (acc g) | just p = just $ lem p
    where
      lem : (∃ λ u → Δ & s , r∈Δ ⊢ (from-meta ((open-meta a) M./ u)) ↓ τ) →
          ∃ λ u' → Δ & s , r∈Δ ⊢ (from-meta (∀' a M./ u')) ↓ τ
      lem (u ∷ us , p) = us , (i-tabs (from-meta u) (subst (λ v → Δ & s , r∈Δ ⊢ v ↓ τ) (begin
            from-meta (M._/_ (open-meta a) (u ∷ us))
              ≡⟨ cong (λ v → from-meta (M._/_ (open-meta a) v)) (sym $ us↑-⊙-sub-u≡u∷us u us) ⟩
            from-meta ((open-meta a) M./ (us M.↑ M.⊙ (M.sub u)))
              ≡⟨ cong from-meta (/-⊙ (open-meta a)) ⟩
            from-meta ((open-meta a) M./ us M.↑ M./ (M.sub u))
              ≡⟨ lem₄ a u us ⟩
            from-meta (a M./ (us M.↑tp)) tp[/tp from-meta u ] ∎) p))
          where open MetaTypeMetaLemmas hiding (subst)
  match' Δ s r∈Δ τ (∀' r) (acc f) (acc g) | nothing = nothing

  -- match defers to match', which concerns itself with MetaTypes.
  -- If match' finds a match, we can use the fact that we have zero unification variables open here
  -- to show that we found the right thing.
  match : ∀ {ν ρ} (Δ : ICtx ν) s (r∈Δ : ρ List.∈ Δ) r τ → Acc _arg<_ (s , _ , simpl τ) →
          Maybe (Δ & s , r∈Δ ⊢ r ↓ τ)
  match Δ s r∈Δ a τ ac with match' Δ s r∈Δ τ (to-meta {zero} a) ac (m<-well-founded _)
  match Δ s r∈Δ a τ ac | just x = just (lem x)
    where
      eq : ∀ {ν} {a : Type ν} {s} → from-meta (to-meta {zero} a M./ s) ≡ a
      eq {a = a} {s = []} = begin
          from-meta (M._/_ (to-meta {zero} a) [])
          ≡⟨ cong (λ q → from-meta q) (MetaTypeMetaLemmas.id-vanishes (to-meta {zero} a)) ⟩
          from-meta (to-meta {zero} a)
          ≡⟨ to-meta-zero-vanishes ⟩
          a ∎
      lem : ∃ (λ u → Δ & s , r∈Δ ⊢ from-meta (to-meta {zero} a M./ u) ↓ τ) →
                Δ & s , r∈Δ ⊢ a ↓ τ
      lem ([] , proj₂) = subst (λ u → Δ & s , r∈Δ ⊢ u ↓ τ) eq proj₂
  match Δ s r∈Δ a τ ac | nothing = nothing

  match1st : ∀ {ν} (Δ : ICtx ν) (s : Stack Δ) τ → Acc _arg<_ (s , _ , simpl τ) →
             Maybe (∃₂ λ r (r∈Δ : r List.∈ Δ) → Δ & s , r∈Δ ⊢ r ↓ τ)
  match1st Δ s τ ac = match1st' Δ Δ Prelude.id s τ ac -- any (λ r → match Δ r τ)
    where
      match1st' : ∀ {ν} (Δ ρs : ICtx ν) → ρs ⊆ Δ → (s : Stack Δ) → (τ : SimpleType ν) →
                  Acc _arg<_ (s , _ , simpl τ) →
                  Maybe (∃₂ λ r (r∈Δ : r List.∈ Δ) → Δ & s , r∈Δ ⊢ r ↓ τ)
      match1st' Δ List.[] sub s τ ac = nothing
      match1st' Δ (x List.∷ xs) sub s τ ac with match Δ s (sub (here refl)) x τ ac
      match1st' Δ (x List.∷ xs) sub s τ ac | just px = just (x , ((sub (here refl)) , px))
      match1st' Δ (x List.∷ xs) sub s τ ac | nothing with
        match1st' Δ xs {!!} s τ ac
      match1st' Δ (x List.∷ xs) sub s τ ac | nothing | just p = just p
      match1st' Δ (x List.∷ xs) sub s τ ac | nothing | nothing = nothing

  resolve' : ∀ {ν} (Δ : ICtx ν) s r → Acc _arg<_ (s , _ , r) → (Maybe (Δ & s ⊢ᵣ r))
  resolve' Δ s (simpl x) ac with match1st Δ s x ac
  resolve' Δ s (simpl x) ac | just (_ , r∈Δ , r↓x) = just (r-simp r∈Δ r↓x)
  resolve' Δ s (simpl x) ac | nothing = nothing
    -- no (λ{ (r-simp x₁ x₂) → ¬p (_⟨$⟩_ (Inverse.to Any↔) (_ , (x₁ , x₂))) })
  resolve' Δ s (a ⇒ b) (acc f) with resolve' (a List.∷ Δ) (s prepend a) b {!f!}
  resolve' Δ s (a ⇒ b) (acc f) | just p = just (r-iabs p)
  resolve' Δ s (a ⇒ b) (acc f) | nothing = nothing -- no (λ{ (r-iabs x) → ¬p x })
  resolve' Δ s (∀' r) (acc f) with resolve' (ictx-weaken Δ) (stack-weaken s) r {!f ? ?!}
  resolve' Δ s (∀' r) (acc f) | just p = just (r-tabs p)
  resolve' Δ s (∀' r) (acc f) | nothing = nothing --no (λ{ (r-tabs x) → ¬p x })

  resolve : ∀ {ν} (Δ : ICtx ν) r → (Maybe (Δ ⊢ᵣ r))
  resolve Δ r = resolve' Δ (All.tabulate (const r)) r (arg<-well-founded _)


text:
{-# OPTIONS --cubical-compatible #-}
module Common.Bool where

open import Agda.Builtin.Bool public

not : Bool -> Bool
not true  = false
not false = true

notnot : Bool -> Bool
notnot true  = not (not true)
notnot false = not (not false)

if_then_else_ : ∀ {a} {A : Set a} → Bool → A → A → A
if true  then t else f = t
if false then t else f = f


text:
{- This file shows a natural attempt to do formatted printing, and where
   that attempt goes wrong.  See string-format.agda for a (working) solution
   to this problem.  -}
module string-format-issue where

open import char
open import eq
open import list
open import nat

open import nat-to-string
open import string

format-th : 𝕃 char → Set
format-th ('%' :: 'n' :: f) = ℕ → format-th f
format-th ('%' :: 's' :: f) = string → format-th f
format-th (c :: f) = format-th f
format-th [] = string

format-t : string → Set
format-t s = format-th (string-to-𝕃char s)

test-format-t : format-t "The %n% %s are %s." ≡ (ℕ → string → string → string)
test-format-t = refl

format-h : 𝕃 char → (f : 𝕃 char) → format-th f
format-h s ('%' :: 'n' :: f) = λ n → format-h (s ++ (string-to-𝕃char (ℕ-to-string n))) f
format-h s ('%' :: 's' :: f) = λ s' → format-h (s ++ (string-to-𝕃char s')) f
format-h s (c :: f) = {!!}
format-h s [] = 𝕃char-to-string s

format : (f : string) → format-t f
format f = format-h [] (string-to-𝕃char f)

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --safe #-}
{-
  This uses ideas from Floris van Doorn's phd thesis and the code in
  https://github.com/cmu-phil/Spectral/blob/master/spectrum/basic.hlean
-}
module Cubical.Homotopy.Prespectrum where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Pointed
open import Cubical.Data.Unit.Pointed

open import Cubical.Structures.Successor

open import Cubical.Data.Nat
open import Cubical.Data.Int

open import Cubical.HITs.Susp

open import Cubical.Homotopy.Loopspace

private
  variable
    ℓ ℓ' : Level

record GenericPrespectrum (S : SuccStr ℓ) (ℓ' : Level) : Type (ℓ-max (ℓ-suc ℓ') ℓ) where
  open SuccStr S
  field
    space : Index → Pointed ℓ'
    map : (i : Index) → (space i →∙ Ω (space (succ i)))

Prespectrum = GenericPrespectrum ℤ+

Unit∙→ΩUnit∙ : {ℓ : Level} → (Unit∙ {ℓ = ℓ}) →∙ Ω (Unit∙ {ℓ = ℓ})
Unit∙→ΩUnit∙ = (λ {tt* → refl}) , refl

makeℤPrespectrum : (space : ℕ → Pointed ℓ)
                  (map : (i : ℕ) → (space i) →∙ Ω (space (suc i)))
                → Prespectrum ℓ
GenericPrespectrum.space (makeℤPrespectrum space map) (pos n) = space n
GenericPrespectrum.space (makeℤPrespectrum space map) (negsuc n) = Unit∙
GenericPrespectrum.map (makeℤPrespectrum space map) (pos n) = map n
GenericPrespectrum.map (makeℤPrespectrum space map) (negsuc zero) = (λ {tt* → refl}) , refl
GenericPrespectrum.map (makeℤPrespectrum space map) (negsuc (suc n)) = Unit∙→ΩUnit∙

SuspensionPrespectrum : Pointed ℓ → Prespectrum ℓ
SuspensionPrespectrum A = makeℤPrespectrum space map
          where
            space : ℕ → Pointed _
            space zero = A
            space (suc n) = Susp∙ (typ (space n))

            map : (n : ℕ) → _
            map n = toSuspPointed (space n)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Alternative definition of divisibility without using modulus.
------------------------------------------------------------------------

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

module Data.Integer.Divisibility.Signed where

open import Function
open import Data.Integer
open import Data.Integer.Properties
open import Data.Integer.Divisibility as Unsigned
  using (divides)
  renaming (_∣_ to _∣ᵤ_)
import Data.Nat as ℕ
import Data.Nat.Divisibility as ℕ
import Data.Nat.Coprimality as ℕ
import Data.Nat.Properties as ℕ
import Data.Sign as S
import Data.Sign.Properties as SProp
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
import Relation.Binary.Reasoning.Preorder as PreorderReasoning
open import Relation.Nullary using (yes; no)
import Relation.Nullary.Decidable as DEC

------------------------------------------------------------------------
-- Type

infix 4 _∣_

record _∣_ (k z : ℤ) : Set where
  constructor divides
  field quotient : ℤ
        equality : z ≡ quotient * k
open _∣_ using (quotient) public

------------------------------------------------------------------------
-- Conversion between signed and unsigned divisibility

∣ᵤ⇒∣ : ∀ {k i} → k ∣ᵤ i → k ∣ i
∣ᵤ⇒∣ {k} {i} (divides 0 eq) = divides (+ 0) (∣n∣≡0⇒n≡0 eq)
∣ᵤ⇒∣ {k} {i} (divides q@(ℕ.suc q') eq) with k ≟ + 0
... | yes refl = divides (+ 0) (∣n∣≡0⇒n≡0 (trans eq (ℕ.*-zeroʳ q)))
... | no ¬k≠0  = divides ((S._*_ on sign) i k ◃ q) (◃-≡ sign-eq abs-eq) where

  k'   = ℕ.suc (ℕ.pred ∣ k ∣)
  ikq' = sign i S.* sign k ◃ ℕ.suc q'

  sign-eq : sign i ≡ sign (((S._*_ on sign) i k ◃ q) * k)
  sign-eq = sym $ begin
    sign (((S._*_ on sign) i k ◃ ℕ.suc q') * k)
      ≡⟨ cong (λ m → sign (sign ikq' S.* sign k ◃ ∣ ikq' ∣ ℕ.* m))
              (sym (ℕ.m≢0⇒suc[pred[m]]≡m (¬k≠0 ∘ ∣n∣≡0⇒n≡0))) ⟩
    sign (sign ikq' S.* sign k ◃ ∣ ikq' ∣ ℕ.* k')
      ≡⟨ cong (λ m → sign (sign ikq' S.* sign k ◃ m ℕ.* k'))
              (abs-◃ (sign i S.* sign k) (ℕ.suc q')) ⟩
    sign (sign ikq' S.* sign k ◃ _)
      ≡⟨ sign-◃ (sign ikq' S.* sign k) (ℕ.pred ∣ k ∣ ℕ.+ q' ℕ.* k') ⟩
    sign ikq' S.* sign k
      ≡⟨ cong (S._* sign k) (sign-◃ (sign i S.* sign k) q') ⟩
    sign i S.* sign k S.* sign k
        ≡⟨ SProp.*-assoc (sign i) (sign k) (sign k) ⟩
    sign i S.* (sign k S.* sign k)
      ≡⟨ cong (sign i S.*_) (SProp.s*s≡+ (sign k)) ⟩
    sign i S.* S.+
      ≡⟨ SProp.*-identityʳ (sign i) ⟩
    sign i
      ∎ where open ≡-Reasoning

  abs-eq : ∣ i ∣ ≡ ∣ ((S._*_ on sign) i k ◃ q) * k ∣
  abs-eq = sym $ begin
    ∣ ((S._*_ on sign) i k ◃ ℕ.suc q') * k ∣
      ≡⟨ abs-◃ (sign ikq' S.* sign k) (∣ ikq' ∣ ℕ.* ∣ k ∣) ⟩
    ∣ ikq' ∣ ℕ.* ∣ k ∣
      ≡⟨ cong (ℕ._* ∣ k ∣) (abs-◃ (sign i S.* sign k) (ℕ.suc q')) ⟩
    ℕ.suc q' ℕ.* ∣ k ∣
      ≡⟨ sym eq ⟩
    ∣ i ∣
      ∎ where open ≡-Reasoning

∣⇒∣ᵤ : ∀ {k i} → k ∣ i → k ∣ᵤ i
∣⇒∣ᵤ {k} {i} (divides q eq) = divides ∣ q ∣ $′ begin
  ∣ i ∣           ≡⟨ cong ∣_∣ eq ⟩
  ∣ q * k ∣       ≡⟨ abs-*-commute q k ⟩
  ∣ q ∣ ℕ.* ∣ k ∣ ∎ where open ≡-Reasoning

------------------------------------------------------------------------
-- _∣_ is a preorder

∣-refl : Reflexive _∣_
∣-refl = ∣ᵤ⇒∣ ℕ.∣-refl

∣-reflexive : _≡_ ⇒ _∣_
∣-reflexive refl = ∣-refl

∣-trans : Transitive _∣_
∣-trans i∣j j∣k = ∣ᵤ⇒∣ (ℕ.∣-trans (∣⇒∣ᵤ i∣j) (∣⇒∣ᵤ j∣k))

∣-isPreorder : IsPreorder _≡_ _∣_
∣-isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = ∣-reflexive
  ; trans         = ∣-trans
  }

∣-preorder : Preorder _ _ _
∣-preorder = record { isPreorder = ∣-isPreorder }

module ∣-Reasoning = PreorderReasoning ∣-preorder
  hiding   (_≈⟨_⟩_)
  renaming (_∼⟨_⟩_ to _∣⟨_⟩_)

------------------------------------------------------------------------
-- Other properties of _∣_

_∣?_ : Decidable _∣_
k ∣? m = DEC.map′ ∣ᵤ⇒∣ ∣⇒∣ᵤ (∣ k ∣ ℕ.∣? ∣ m ∣)

0∣⇒≡0 : ∀ {m} → + 0 ∣ m → m ≡ + 0
0∣⇒≡0 0|m = ∣n∣≡0⇒n≡0 (ℕ.0∣⇒≡0 (∣⇒∣ᵤ 0|m))

m∣∣m∣ : ∀ {m} → m ∣ (+ ∣ m ∣)
m∣∣m∣ = ∣ᵤ⇒∣ ℕ.∣-refl

∣m∣∣m : ∀ {m} → (+ ∣ m ∣) ∣ m
∣m∣∣m = ∣ᵤ⇒∣ ℕ.∣-refl

∣m∣n⇒∣m+n : ∀ {i m n} → i ∣ m → i ∣ n → i ∣ m + n
∣m∣n⇒∣m+n (divides q refl) (divides p refl) =
  divides (q + p) (sym (*-distribʳ-+ _ q p))

∣m⇒∣-m : ∀ {i m} → i ∣ m → i ∣ - m
∣m⇒∣-m {i} {m} i∣m = ∣ᵤ⇒∣ $′ begin
  ∣ i ∣   ∣⟨ ∣⇒∣ᵤ i∣m ⟩
  ∣ m ∣   ≡⟨ sym (∣-n∣≡∣n∣ m) ⟩
  ∣ - m ∣ ∎
  where open ℕ.∣-Reasoning

∣m∣n⇒∣m-n : ∀ {i m n} → i ∣ m → i ∣ n → i ∣ m - n
∣m∣n⇒∣m-n i∣m i∣n = ∣m∣n⇒∣m+n i∣m (∣m⇒∣-m i∣n)

∣m+n∣m⇒∣n : ∀ {i m n} → i ∣ m + n → i ∣ m → i ∣ n
∣m+n∣m⇒∣n {i} {m} {n} i∣m+n i∣m = begin
  i             ∣⟨ ∣m∣n⇒∣m-n i∣m+n i∣m ⟩
  m + n - m     ≡⟨ +-comm (m + n) (- m) ⟩
  - m + (m + n) ≡⟨ sym (+-assoc (- m) m n) ⟩
  - m + m + n   ≡⟨ cong (_+ n) (+-inverseˡ m) ⟩
  + 0 + n       ≡⟨ +-identityˡ n ⟩
  n             ∎
  where open ∣-Reasoning

∣m+n∣n⇒∣m : ∀ {i m n} → i ∣ m + n → i ∣ n → i ∣ m
∣m+n∣n⇒∣m {i} {m} {n} i|m+n i|n
  rewrite +-comm m n
        = ∣m+n∣m⇒∣n i|m+n i|n

∣n⇒∣m*n : ∀ {i} m {n} → i ∣ n → i ∣ m * n
∣n⇒∣m*n {i} m {n} (divides q eq) = divides (m * q) $′ begin
  m * n       ≡⟨ cong (m *_) eq ⟩
  m * (q * i) ≡⟨ sym (*-assoc m q i) ⟩
  m * q * i   ∎
  where open ≡-Reasoning

∣m⇒∣m*n : ∀ {i m} n → i ∣ m → i ∣ m * n
∣m⇒∣m*n {i} {m} n i|m
  rewrite *-comm m n
        = ∣n⇒∣m*n {i} n {m} i|m

*-monoʳ-∣ : ∀ k → (k *_) Preserves _∣_ ⟶ _∣_
*-monoʳ-∣ k i∣j = ∣ᵤ⇒∣ (Unsigned.*-monoʳ-∣ k (∣⇒∣ᵤ i∣j))

*-monoˡ-∣ : ∀ k → (_* k) Preserves _∣_ ⟶ _∣_
*-monoˡ-∣ k {i} {j} i∣j = ∣ᵤ⇒∣ (Unsigned.*-monoˡ-∣ k {i} {j} (∣⇒∣ᵤ i∣j))

*-cancelˡ-∣ : ∀ k {i j} → k ≢ + 0 → k * i ∣ k * j → i ∣ j
*-cancelˡ-∣ k k≢0 = ∣ᵤ⇒∣ ∘ Unsigned.*-cancelˡ-∣ k k≢0 ∘ ∣⇒∣ᵤ

*-cancelʳ-∣ : ∀ k {i j} → k ≢ + 0 → i * k ∣ j * k → i ∣ j
*-cancelʳ-∣ k {i} {j} k≢0 = ∣ᵤ⇒∣ ∘′ Unsigned.*-cancelʳ-∣ k {i} {j} k≢0 ∘′ ∣⇒∣ᵤ


text:
module Numeral.Natural.Relation.Order.Classical where

import Lvl
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Decidable
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Relator.Properties
open import Relator.Ordering.Proofs
open import Type.Properties.Decidable.Proofs
open import Type

instance
  [≰][>]-sub : (_≰_) ⊆₂ (_>_)
  [≰][>]-sub = From-[≤][<].ByReflTriSub.[≰][>]-sub (_≤_)(_<_) ⦃ [<][≤]-sub = intro(sub₂(_<_)(_≤_)) ⦄ ⦃ [<]-classical = decider-classical _ ⦄

instance
  [≯][≤]-sub : (_≯_) ⊆₂ (_≤_)
  [≯][≤]-sub = From-[≤][<].ByReflTriSub.[≯][≤]-sub (_≤_)(_<_) ⦃ [<][≤]-sub = intro(sub₂(_<_)(_≤_)) ⦄ ⦃ [≤]-classical = decider-classical _ ⦄

instance
  [≱][<]-sub : (_≱_) ⊆₂ (_<_)
  [≱][<]-sub = From-[≤][<].ByReflTriSub.[≱][<]-sub (_≤_)(_<_) ⦃ [<][≤]-sub = intro(sub₂(_<_)(_≤_)) ⦄ ⦃ [<]-classical = decider-classical _ ⦄

instance
  [≮][≥]-sub : (_≮_) ⊆₂ (_≥_)
  [≮][≥]-sub = From-[≤][<].ByReflTriSub.[≮][≥]-sub (_≤_)(_<_) ⦃ [<][≤]-sub = intro(sub₂(_<_)(_≤_)) ⦄ ⦃ [≤]-classical = decider-classical _ ⦄

[≤]-or-[>] : ∀{a b : ℕ} → (a ≤ b) ∨ (a > b)
[≤]-or-[>] = From-[≤][<].ByReflTriSub.[≤]-or-[>] (_≤_)(_<_) ⦃ [<][≤]-sub = intro(sub₂(_<_)(_≤_)) ⦄ ⦃ [≤]-classical = decider-classical _ ⦄ ⦃ [<]-classical = decider-classical _ ⦄

[≥]-or-[<] : ∀{a b : ℕ} → (a ≥ b) ∨ (a < b)
[≥]-or-[<] = From-[≤][<].ByReflTriSub.[≥]-or-[<] (_≤_)(_<_) ⦃ [<][≤]-sub = intro(sub₂(_<_)(_≤_)) ⦄ ⦃ [≤]-classical = decider-classical _ ⦄ ⦃ [<]-classical = decider-classical _ ⦄

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Cubical.Core.Everything

------------------------------------------------------------------------
-- Unary and binary operations

Op₁ : ∀ {ℓ} → Type ℓ → Type ℓ
Op₁ A = A → A

Op₂ : ∀ {ℓ} → Type ℓ → Type ℓ
Op₂ A = A → A → A

------------------------------------------------------------------------
-- Left and right actions

Opₗ : ∀ {a b} → Type a → Type b → Type _
Opₗ A B = A → B → B

Opᵣ : ∀ {a b} → Type a → Type b → Type _
Opᵣ A B = B → A → B


text:
------------------------------------------------------------------------
-- Safe modules that use --erased-cubical and --prop
------------------------------------------------------------------------

{-# OPTIONS --safe --erased-cubical --prop #-}

module README.Safe.Cubical.Erased.Prop where

-- Squashing.

import Squash

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; subst; setoid)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂; zip; map; <_,_>; swap)
import Function.Equality
open import Relation.Binary using (Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidR

import Categories.Category
import Categories.Functor
import Categories.Category.Instance.Setoids
import Categories.Monad.Relative
import Categories.Category.Equivalence
import Categories.Category.Cocartesian
import Categories.Category.Construction.Functors
import Categories.Category.Product
import Categories.NaturalTransformation
import Categories.NaturalTransformation.NaturalIsomorphism

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.VRenaming
import SecondOrder.MRenaming
import SecondOrder.Term
import SecondOrder.Substitution
import SecondOrder.RelativeMonadMorphism
import SecondOrder.Instantiation
import SecondOrder.IndexedCategory
import SecondOrder.RelativeKleisli
import SecondOrder.Mslot
import SecondOrder.MRelativeMonad
import SecondOrder.VRelativeMonad

module SecondOrder.VRelMonMorphism
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.RelativeMonadMorphism
  open SecondOrder.Metavariable Σ
  open SecondOrder.VRelativeMonad Σ
  open SecondOrder.Instantiation Σ
  open SecondOrder.MRenaming Σ
  open SecondOrder.VRenaming Σ
  open SecondOrder.Term Σ
  open SecondOrder.Substitution Σ

  -- In this file, the goal is to show that given two variable relative monads
  -- on different metacontexts, metarenaming from one of the metacontexts to the other
  -- we can define a relative monad morphism between the two variable relative monads

  Fⱽ : ∀ (Θ Θ′ : MContext) (μ : Θ ⇒ᵐ Θ′) →  RMonadMorph (VMonad {Θ}) (VMonad {Θ′})
  Fⱽ Θ Θ′ μ = record
            { morph = λ A →
                        record
                          { _⟨$⟩_ = [ μ ]ᵐ_
                          ; cong = λ s≈t → []ᵐ-resp-≈ s≈t
                          }
            ; law-unit = λ A x≡y → ≈-≡ (σ-resp-≡ {σ = tm-var} x≡y)
            ; law-extend = λ {Γ} {Δ} {k} A {s} {t} s≈t →
                                           ≈-trans
                                             (≈-sym ([ᵐ∘ˢ] s))
                                             (≈-trans
                                               ([]ˢ-resp-≈ˢ ([ μ ]ᵐ s)   λ x → ≈-refl  )
                                               ([]ˢ-resp-≈ (λ {B} x → [ μ ]ᵐ (k B Function.Equality.⟨$⟩ x)) ([]ᵐ-resp-≈ s≈t)))
            }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: cilinder/formaltt

max_forks_repo_name: cilinder/formaltt


text:
module Example1 where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

data _==_ {l} {a : Set l} : a -> a -> Set l where
  refl : ∀{x} -> x == x

{-# BUILTIN EQUALITY _==_ #-}

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

sym : ∀{l} {A : Set l} {x y : A} -> x == y -> y == x
sym refl = refl

_+_ : Nat -> Nat -> Nat
x + zero = x
x + suc y = suc (x + y)

_+₂_ : Nat -> Nat -> Nat
zero +₂ y = y
suc x +₂ y = {!!}

plus-right-identity : ∀{n} -> (n + 0) == n
plus-right-identity {n} = refl

plus-left-identity : (n : Nat) -> (0 + n) == n
plus-left-identity zero = refl
plus-left-identity (suc n) = cong suc (plus-left-identity n)

plus-comm : (m n : Nat) -> (m + n) == (n + m)
plus-comm m zero = sym (plus-left-identity m)
plus-comm m (suc n) = {!!}

plus-succ : ∀{m n} -> (m + suc n) == suc (m + n)
plus-succ = refl

data Vec (A : Set) : Nat -> Set where
  []  : Vec A 0
  _∷_ : ∀{n} -> A -> Vec A n -> Vec A (suc n)

replicate : ∀{A} -> (n : Nat) -> A -> Vec A n
replicate zero x = []
replicate (suc n) x = x ∷ replicate n x

data Pair (A B : Set) : Set where
  _,_ : A -> B -> Pair A B

zip : ∀{n A B} -> Vec A n -> Vec B n -> Vec (Pair A B) n
zip [] ys = []
zip {suc n} (x ∷ xs) (y ∷ ys) = replicate (suc n) (x , y)

map : ∀{n A B} -> (A -> B) -> Vec A n -> Vec B n
map f [] = []
map {suc n} f (x ∷ xs) = (f x) ∷ (map f xs) -- f x ∷ map f xs -- replicate (suc n) (f x)

id : {A : Set} -> A -> A
id x = x

map-id : ∀{n A} (xs : Vec A n) -> map id xs == xs
map-id [] = refl
map-id (x ∷ xs) = cong (_∷_ x) (map-id xs)

data Bool : Set where
  false true : Bool

not : Bool -> Bool
not false = true
not true = false

not-self-inverse : {x : Bool} -> not (not x) == x
not-self-inverse {false} = refl
not-self-inverse {true} = refl

data Empty : Set where

not-not-id : {x : Bool} -> not x == id x -> Empty
not-not-id {false} ()
not-not-id {true} ()

max_stars_repo_name: carlostome/martin

max_issues_repo_name: carlostome/martin

max_forks_repo_name: carlostome/martin


text:
module Issue482 where

open import Common.Level using (_⊔_)

postulate
  P      : ∀ a b → Set a → Set b → Set (a ⊔ b)
  F      : ∀ ℓ → Set ℓ
  p      : ∀ a (A : Set a) → P a a A (F a)
  Q      : ∀ a → Set a → ∀ b → Set (a ⊔ b)
  P-to-Q : ∀ a b (A : Set a) (B : Set b) → P a b A B → Q a A b

q : ∀ a (A : Set a) → Q a A _
q a A = P-to-Q _ _ _ _ (p _ _)

{-

  There was a bug in the level constraint solver that looks
  at pairs of constraints.

-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Demos.Cantor where

open import Prelude
open import Data.Bool.Properties using (false≢true; true≢false)

Stream : Type a → Type a
Stream A = ℕ → A

_∈_ : ∀ {A : Type a} (x : A) → Stream A → Type a
x ∈ xs = ∃ i × (xs i ≡ x)

Countable : Type a → Type a
Countable A = Σ[ xs ⦂ Stream A ] × (∀ x → x ∈ xs)

x≢¬x : ∀ x → x ≢ not x
x≢¬x false = false≢true
x≢¬x true  = true≢false

cantor : ¬ (Countable (Stream Bool))
cantor (support , cover) =
  let p , ps = cover (λ i → not (support i i))
      q = cong (_$ p) ps
  in x≢¬x _ q

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground