text:
------------------------------------------------------------------------
-- Canonical kinding of Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Canonical where

open import Data.Context.WellFormed
open import Data.Fin using (Fin; zero; suc)
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.List using ([]; _∷_; _∷ʳ_)
open import Data.Product using (∃; _,_; _×_)
open import Data.Vec as Vec using ([])
open import Level using () renaming (zero to lzero)
open import Relation.Binary.PropositionalEquality

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization
import FOmegaInt.Kinding.Simple as SimpleKinding

------------------------------------------------------------------------
-- Canonical kinding derivations.
--
-- TODO: explain the point of this and how "canonical" kinding differs
-- from "algorithmic" kinding.
--
-- NOTE. In the rules below, we use (singleton) kind synthesis
-- judgments of the form `Γ ⊢Nf a ⇉ a ⋯ a' to ensure that `a' is a
-- well-kinded proper type rather than kind checking judgments of the
-- form `Γ ⊢Nf a ⇇ *'.  While the latter may seem more natural, it
-- involves the use of subsumption/subtyping to ensure that `Γ ⊢ a ⋯ a
-- <∷ *'.  As we will show, this is always true (if `a' is indeed a
-- proper type) but the extra use of subsumption complicates the
-- proofs of properties that require (partial) inversion of kinding
-- derivations.  See e.g. the Nf⇉-⋯-* and Nf⇇-⋯-* lemmas.

module Kinding where
  open ElimCtx
  open Syntax

  infix 4 _⊢_wf _ctx _⊢_kd
  infix 4 _⊢Nf_⇉_ _⊢Ne_∈_ _⊢Var_∈_ _⊢_⇉∙_⇉_ _⊢Nf_⇇_
  infix 4 _⊢_<∷_ _⊢_<:_ _⊢_<:_⇇_
  infix 4 _⊢_≅_ _⊢_≃_⇇_ _⊢_⇉∙_≃_⇉_

  mutual

    -- Well-formed type/kind ascriptions in typing contexts.
    --
    -- A raw kind ascriptions is considered well-formed if it
    -- corresponds to a well-formed normal kind.  Raw type ascriptions
    -- are are considered well-formed if they correspond to proper
    -- normal types.
    data _⊢_wf {n} (Γ : Ctx n) : ElimAsc n → Set where
      wf-kd : ∀ {a} → Γ ⊢ a kd        → Γ ⊢ kd a wf
      wf-tp : ∀ {a} → Γ ⊢Nf a ⇉ a ⋯ a → Γ ⊢ tp a wf

    -- Well-formed typing contexts.
    --
    -- Contexts and context extensions are well-formed if all the
    -- ascriptions they contain are well-formed.
    _ctx : ∀ {n} → Ctx n → Set
    Γ ctx = ContextFormation._wf _⊢_wf Γ

    -- Well-formedness checking for η-long β-normal kinds.
    data _⊢_kd {n} (Γ : Ctx n) : Kind Elim n → Set where
      kd-⋯ : ∀ {a b} → Γ ⊢Nf a ⇉ a ⋯ a → Γ ⊢Nf b ⇉ b ⋯ b → Γ ⊢ a ⋯ b kd
      kd-Π : ∀ {j k} → Γ ⊢ j kd → kd j ∷ Γ ⊢ k kd        → Γ ⊢ Π j k kd

    -- Kind synthesis for η-long β-normal types.
    data _⊢Nf_⇉_ {n} (Γ : Ctx n) : Elim n → Kind Elim n → Set where
      ⇉-⊥-f : Γ ctx → Γ ⊢Nf ⊥∙ ⇉ ⊥∙ ⋯ ⊥∙
      ⇉-⊤-f : Γ ctx → Γ ⊢Nf ⊤∙ ⇉ ⊤∙ ⋯ ⊤∙
      ⇉-∀-f : ∀ {k a} → Γ ⊢ k kd → kd k ∷ Γ ⊢Nf a ⇉ a ⋯ a →
              Γ ⊢Nf ∀∙ k a ⇉ ∀∙ k a ⋯ ∀∙ k a
      ⇉-→-f : ∀ {a b} → Γ ⊢Nf a ⇉ a ⋯ a → Γ ⊢Nf b ⇉ b ⋯ b →
              Γ ⊢Nf a ⇒∙ b ⇉ a ⇒∙ b ⋯ a ⇒∙ b
      ⇉-Π-i : ∀ {j a k} → Γ ⊢ j kd → kd j ∷ Γ ⊢Nf a ⇉ k → Γ ⊢Nf Λ∙ j a ⇉ Π j k
      ⇉-s-i : ∀ {a b c} → Γ ⊢Ne a ∈ b ⋯ c → Γ ⊢Nf a ⇉ a ⋯ a

    -- Canonical kinding of neutral types.
    --
    -- NOTE.  This is *not* a kind synthesis judgment!  See the
    -- comment on canonical variable kinding for an explanation.

    data _⊢Ne_∈_ {n} (Γ : Ctx n) : Elim n → Kind Elim n → Set where
      ∈-∙ : ∀ {x j k} {as : Spine n} → Γ ⊢Var x ∈ j →
            Γ ⊢ j ⇉∙ as ⇉ k → Γ ⊢Ne var x ∙ as ∈ k

    -- Canonical kinding of variables.
    --
    -- NOTE.  This would be a kind synthesis judgment if it weren't
    -- for the subsumption rule (⇇-⇑).  Thanks to this rule, the proof
    -- of the "context narrowing" property is easy to establish for
    -- canonical typing (see the ContextNarrowing module below).
    -- Without a proof of this property, the various lemmas about
    -- kinded hereditary substitutions become difficult to establish
    -- (see Kinding.HereditarySubstitution).  Unfortunately, proving
    -- that context narrowing is admissible *without* (⇇-⇑) would
    -- require precisely these substitution lemmas, leading to a
    -- cyclic dependency.  Introducing the subsumption rule for
    -- variables thus allows us to break that cycle.  On the other
    -- hand, the subsumption rule breaks functionality of the
    -- canonical kinding relations for variables and neutral types,
    -- i.e. their canonical kinds are no longer unique.  This is
    -- partly remedied by the singleton-introduction rule (⇉-s-i) in
    -- the kind synthesis judgment for normal types: neutrals have
    -- unique (singleton) kinds when viewed as normal forms.  However,
    -- neutral kinding is also used in subtyping, in particular by the
    -- bound projection rules (<:-⟨|) and (<:-|⟩).  Because the kinds
    -- of neutrals are not unique, neither are the bounds projected by
    -- these subtyping rules, and eliminating adjacent instances of
    -- (<:-⟨|) and (<:-|⟩) becomes difficult.  This, in turn,
    -- complicates transitivity elimination (i.e. a proof that
    -- transitivity of subtyping is admissible) in arbitrary contexts.
    -- However, it does not affect elimination of *top-level*
    -- occurrences of the transitivity rule (<:-trans), i.e. those in
    -- the empty contexts, because there are no closed neutral terms,
    -- and therefore no instances of the bound projection rules in
    -- top-level subtyping statements.

    data _⊢Var_∈_ {n} (Γ : Ctx n) : Fin n → Kind Elim n → Set where
      ⇉-var : ∀ {k} x → Γ ctx → lookup Γ x ≡ kd k → Γ ⊢Var x ∈ k
      ⇇-⇑   : ∀ {x j k} → Γ ⊢Var x ∈ j → Γ ⊢ j <∷ k → Γ ⊢ k kd →
              Γ ⊢Var x ∈ k

    -- Kind synthesis for spines: given the kind of the head and a
    -- spine, synthesize the overall kind of the elimination.
    data _⊢_⇉∙_⇉_ {n} (Γ : Ctx n)
      : Kind Elim n → Spine n → Kind Elim n → Set where
      ⇉-[] : ∀ {k} → Γ ⊢ k ⇉∙ [] ⇉ k
      ⇉-∷  : ∀ {a as j k l} → Γ ⊢Nf a ⇇ j → Γ ⊢ j kd →
             Γ ⊢ k Kind[ a ∈ ⌊ j ⌋ ] ⇉∙ as ⇉ l →
             Γ ⊢ Π j k ⇉∙ a ∷ as ⇉ l

    -- Kind checking for η-long β-normal types.
    data _⊢Nf_⇇_ {n} (Γ : Ctx n) : Elim n → Kind Elim n → Set where
      ⇇-⇑  : ∀ {a j k} → Γ ⊢Nf a ⇉ j → Γ ⊢ j <∷ k → Γ ⊢Nf a ⇇ k

    -- Canonical subkinding derivations.
    data _⊢_<∷_ {n} (Γ : Ctx n) : Kind Elim n → Kind Elim n → Set where
      <∷-⋯ : ∀ {a₁ a₂ b₁ b₂} →
             Γ ⊢ a₂ <: a₁ → Γ ⊢ b₁ <: b₂ → Γ ⊢ a₁ ⋯ b₁ <∷ a₂ ⋯ b₂
      <∷-Π : ∀ {j₁ j₂ k₁ k₂} →
             Γ ⊢ j₂ <∷ j₁ → kd j₂ ∷ Γ ⊢ k₁ <∷ k₂ → Γ ⊢ Π j₁ k₁ kd →
             Γ ⊢ Π j₁ k₁ <∷ Π j₂ k₂

    -- Canonical subtyping of proper types.
    data _⊢_<:_ {n} (Γ : Ctx n) : Elim n → Elim n → Set where
      <:-trans : ∀ {a b c} → Γ ⊢ a <: b → Γ ⊢ b <: c → Γ ⊢ a <: c
      <:-⊥     : ∀ {a} → Γ ⊢Nf a ⇉ a ⋯ a → Γ ⊢ ⊥∙ <: a
      <:-⊤     : ∀ {a} → Γ ⊢Nf a ⇉ a ⋯ a → Γ ⊢ a <: ⊤∙
      <:-∀     : ∀ {k₁ k₂ a₁ a₂} →
                 Γ ⊢ k₂ <∷ k₁ → kd k₂ ∷ Γ ⊢ a₁ <: a₂ →
                 Γ ⊢Nf ∀∙ k₁ a₁ ⇉  ∀∙ k₁ a₁ ⋯ ∀∙ k₁ a₁ →
                 Γ ⊢ ∀∙ k₁ a₁ <: ∀∙ k₂ a₂
      <:-→     : ∀ {a₁ a₂ b₁ b₂} →
                 Γ ⊢ a₂ <: a₁ → Γ ⊢ b₁ <: b₂ → Γ ⊢ a₁ ⇒∙ b₁ <: a₂ ⇒∙ b₂
      <:-∙     : ∀ {x as₁ as₂ k b c} →
                 Γ ⊢Var x ∈ k → Γ ⊢ k ⇉∙ as₁ ≃ as₂ ⇉ b ⋯ c →
                 Γ ⊢ var x ∙ as₁ <: var x ∙ as₂
      <:-⟨|    : ∀ {a b c} → Γ ⊢Ne a ∈ b ⋯ c → Γ ⊢ b <: a
      <:-|⟩    : ∀ {a b c} → Γ ⊢Ne a ∈ b ⋯ c → Γ ⊢ a <: c

    -- Checked/kind-driven subtyping.
    data _⊢_<:_⇇_ {n} (Γ : Ctx n) : Elim n → Elim n → Kind Elim n → Set where
      <:-⇇ : ∀ {a b c d} → Γ ⊢Nf a ⇇ c ⋯ d → Γ ⊢Nf b ⇇ c ⋯ d →
             Γ ⊢ a <: b → Γ ⊢ a <: b ⇇ c ⋯ d
      <:-λ : ∀ {j₁ j₂ a₁ a₂ j k} → kd j ∷ Γ ⊢ a₁ <: a₂ ⇇ k →
             Γ ⊢Nf Λ∙ j₁ a₁ ⇇ Π j k → Γ ⊢Nf Λ∙ j₂ a₂ ⇇ Π j k →
             Γ ⊢ Λ∙ j₁ a₁ <: Λ∙ j₂ a₂ ⇇ Π j k

    -- Canonical kind equality.
    data _⊢_≅_ {n} (Γ : Ctx n) : Kind Elim n → Kind Elim n → Set where
      <∷-antisym : ∀ {j k} → Γ ⊢ j kd → Γ ⊢ k kd →
                   Γ ⊢ j <∷ k → Γ ⊢ k <∷ j → Γ ⊢ j ≅ k

    -- Canonical type equality derivations with checked kinds.
    data _⊢_≃_⇇_ {n} (Γ : Ctx n) : Elim n → Elim n → Kind Elim n → Set where
      <:-antisym : ∀ {a b k} →
                   Γ ⊢ k kd → Γ ⊢ a <: b ⇇ k → Γ ⊢ b <: a ⇇ k → Γ ⊢ a ≃ b ⇇ k

    -- Canonical equality of spines.
    data _⊢_⇉∙_≃_⇉_ {n} (Γ : Ctx n)
      : Kind Elim n → Spine n → Spine n → Kind Elim n → Set where
      ≃-[] : ∀ {k} → Γ ⊢ k ⇉∙ [] ≃ [] ⇉ k
      ≃-∷  : ∀ {a as b bs j k l} →
             Γ ⊢ a ≃ b ⇇ j → Γ ⊢ k Kind[ a ∈ ⌊ j ⌋ ] ⇉∙ as ≃ bs ⇉ l →
             Γ ⊢ Π j k ⇉∙ a ∷ as ≃ b ∷ bs ⇉ l

  -- Well-formed context extensions.
  open ContextFormation _⊢_wf public
    hiding (_wf) renaming (_⊢_wfExt to _⊢_ext)

  -- A wrapper for the _⊢Var_∈_ judgment that also provides term
  -- variable bindings.

  infix 4 _⊢Var′_∈_

  data _⊢Var′_∈_ {n} (Γ : Ctx n) : Fin n → ElimAsc n → Set where
    ∈-tp : ∀ {x k} → Γ ⊢Var x ∈ k → Γ ⊢Var′ x ∈ kd k
    ∈-tm : ∀ x {a} → Γ ctx → lookup Γ x ≡ tp a → Γ ⊢Var′ x ∈ tp a

  -- A derived variable rule.

  ∈-var′ : ∀ {n} {Γ : Ctx n} x → Γ ctx → Γ ⊢Var′ x ∈ lookup Γ x
  ∈-var′ {Γ = Γ} x Γ-ctx with lookup Γ x | inspect (lookup Γ) x
  ∈-var′ x Γ-ctx | kd k | [ Γ[x]≡kd-k ] = ∈-tp (⇉-var x Γ-ctx Γ[x]≡kd-k)
  ∈-var′ x Γ-ctx | tp a | [ Γ[x]≡tp-a ] = ∈-tm x Γ-ctx Γ[x]≡tp-a

------------------------------------------------------------------------
-- Simple properties of canonical kindings

open Syntax
open ElimCtx
open SimpleCtx using (kd; tp; ⌊_⌋Asc)
open Kinding
open ContextConversions using (⌊_⌋Ctx; module ⌊⌋Ctx-Lemmas)

-- An inversion lemma for _⊢_wf.

wf-kd-inv : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ kd k wf → Γ ⊢ k kd
wf-kd-inv (wf-kd k-kd) = k-kd

-- Subkinds have the same shape.

<∷-⌊⌋ : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j <∷ k → ⌊ j ⌋ ≡ ⌊ k ⌋
<∷-⌊⌋ (<∷-⋯ _ _)             = refl
<∷-⌊⌋ (<∷-Π j₂<∷j₁ k₁<∷k₂ _) = cong₂ _⇒_ (sym (<∷-⌊⌋ j₂<∷j₁)) (<∷-⌊⌋ k₁<∷k₂)

-- Equal kinds have the same shape.

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

-- Kind and type equality imply subkinding and subtyping, respectively.

≅⇒<∷ : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j ≅ k → Γ ⊢ j <∷ k
≅⇒<∷ (<∷-antisym j-kd k-kd j<∷k k<∷j) = j<∷k

≃⇒<: : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a ≃ b ⇇ k → Γ ⊢ a <: b ⇇ k
≃⇒<: (<:-antisym k-kd a<:b⇇k b<:a⇇k) = a<:b⇇k

≃⇒<:-⋯ : ∀ {n} {Γ : Ctx n} {a b c d} → Γ ⊢ a ≃ b ⇇ c ⋯ d → Γ ⊢ a <: b
≃⇒<:-⋯ (<:-antisym c⋯d-kd (<:-⇇ a⇇c⋯d b⇇c⋯d a<:b) b<:a⇇c⋯d) = a<:b

-- Symmetry of kind and type equality.

≅-sym : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j ≅ k → Γ ⊢ k ≅ j
≅-sym (<∷-antisym j-kd k-kd j<:k k<∷j) = <∷-antisym k-kd j-kd k<∷j j<:k

≃-sym : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a ≃ b ⇇ k → Γ ⊢ b ≃ a ⇇ k
≃-sym (<:-antisym k-kd a<:b b<:a) = <:-antisym k-kd b<:a a<:b

-- Transitivity of checked subtyping and type equality are admissible.

<:⇇-trans : ∀ {n} {Γ : Ctx n} {a b c k} →
            Γ ⊢ a <: b ⇇ k → Γ ⊢ b <: c ⇇ k → Γ ⊢ a <: c ⇇ k
<:⇇-trans (<:-⇇ a₁⇇b⋯c _ a₁<:a₂) (<:-⇇ _ a₃⇇b⋯c a₂<:a₃) =
  <:-⇇ a₁⇇b⋯c a₃⇇b⋯c (<:-trans a₁<:a₂ a₂<:a₃)
<:⇇-trans (<:-λ a₁<:a₂ Λj₁a₁⇇Πjk _) (<:-λ a₂<:a₃ _ Λj₃a₃⇇Πjk) =
  <:-λ (<:⇇-trans a₁<:a₂ a₂<:a₃) Λj₁a₁⇇Πjk Λj₃a₃⇇Πjk

≃-trans : ∀ {n} {Γ : Ctx n} {a b c k} →
          Γ ⊢ a ≃ b ⇇ k → Γ ⊢ b ≃ c ⇇ k → Γ ⊢ a ≃ c ⇇ k
≃-trans (<:-antisym k-kd a<:b⇇k b<:a⇇k) (<:-antisym _ b<:c⇇k c<:b⇇k) =
  <:-antisym k-kd (<:⇇-trans a<:b⇇k b<:c⇇k) (<:⇇-trans c<:b⇇k b<:a⇇k)

-- The synthesized kind of a normal proper type is exactly the singleton
-- containing that type.
Nf⇉-≡ : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇉ b ⋯ c → a ≡ b × a ≡ c
Nf⇉-≡ (⇉-⊥-f Γ-ctx)       = refl , refl
Nf⇉-≡ (⇉-⊤-f Γ-ctx)       = refl , refl
Nf⇉-≡ (⇉-∀-f k-kd  b⇉b⋯b) = refl , refl
Nf⇉-≡ (⇉-→-f a⇉a⋯a b⇉b⋯b) = refl , refl
Nf⇉-≡ (⇉-s-i a∈b⋯c)       = refl , refl

-- Derived singleton introduction rules where the premises are
-- well-kinded normal forms rather than neutrals.

Nf⇉-s-i : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇉ b ⋯ c → Γ ⊢Nf a ⇉ a ⋯ a
Nf⇉-s-i a⇉b⋯c with Nf⇉-≡ a⇉b⋯c
Nf⇉-s-i a⇉a⋯a | refl , refl = a⇉a⋯a

Nf⇇-s-i : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇇ b ⋯ c → Γ ⊢Nf a ⇉ a ⋯ a
Nf⇇-s-i (⇇-⇑ a⇉b₁⋯c₁ (<∷-⋯ b₂<:b₁ c₁<:c₂)) = Nf⇉-s-i a⇉b₁⋯c₁

-- Inhabitants of interval kinds are proper types.

Nf⇉-⋯-* : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇉ b ⋯ c → Γ ⊢Nf a ⇇ ⌜*⌝
Nf⇉-⋯-* a⇉b⋯c with Nf⇉-≡ a⇉b⋯c
Nf⇉-⋯-* a⇉a⋯a | refl , refl = ⇇-⇑ a⇉a⋯a (<∷-⋯ (<:-⊥ a⇉a⋯a) (<:-⊤ a⇉a⋯a))

Nf⇇-⋯-* : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇇ b ⋯ c → Γ ⊢Nf a ⇇ ⌜*⌝
Nf⇇-⋯-* (⇇-⇑ a⇉b₁⋯c₁ (<∷-⋯ b₂<:b₁ c₁<:c₂)) = Nf⇉-⋯-* a⇉b₁⋯c₁

-- Validity of synthesized kinds: synthesized kinds are well-formed.
Nf⇉-valid : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Nf a ⇉ k → Γ ⊢ k kd
Nf⇉-valid (⇉-⊥-f Γ-ctx)       = kd-⋯ (⇉-⊥-f Γ-ctx) (⇉-⊥-f Γ-ctx)
Nf⇉-valid (⇉-⊤-f Γ-ctx)       = kd-⋯ (⇉-⊤-f Γ-ctx) (⇉-⊤-f Γ-ctx)
Nf⇉-valid (⇉-∀-f k-kd a⇉a⋯a)  = kd-⋯ (⇉-∀-f k-kd a⇉a⋯a) (⇉-∀-f k-kd a⇉a⋯a)
Nf⇉-valid (⇉-→-f a⇉a⋯a b⇉b⋯b) = kd-⋯ (⇉-→-f a⇉a⋯a b⇉b⋯b) (⇉-→-f a⇉a⋯a b⇉b⋯b)
Nf⇉-valid (⇉-Π-i j-kd a⇉k)    = kd-Π j-kd (Nf⇉-valid a⇉k)
Nf⇉-valid (⇉-s-i a∈b⋯c)       = kd-⋯ (⇉-s-i a∈b⋯c) (⇉-s-i a∈b⋯c)

-- Validity of checked subtyping: the checked subtyping judgment
-- relates well-kinded types.

<:⇇-valid : ∀ {n} {Γ : Ctx n} {a b k} →
            Γ ⊢ a <: b ⇇ k → Γ ⊢Nf a ⇇ k × Γ ⊢Nf b ⇇ k
<:⇇-valid (<:-⇇ a⇇k b⇇k a<:b)               = a⇇k , b⇇k
<:⇇-valid (<:-λ a₁<:a₂ Λj₁a₁⇇Πjk Λj₂a₂⇇Πjk) = Λj₁a₁⇇Πjk , Λj₂a₂⇇Πjk

-- Validity of kind and type equality: the equality judgments relate
-- well-formed kinds, resp. well-kinded types.

≅-valid : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j ≅ k → Γ ⊢ j kd × Γ ⊢ k kd
≅-valid (<∷-antisym j-kd k-kd j<∷k k<∷j) = j-kd , k-kd

≃-valid : ∀ {n} {Γ : Ctx n} {a b k} →
          Γ ⊢ a ≃ b ⇇ k → Γ ⊢Nf a ⇇ k × Γ ⊢Nf b ⇇ k
≃-valid (<:-antisym k-kd a<:b⇇k b<:a⇇k) = <:⇇-valid a<:b⇇k

≃-valid-kd : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a ≃ b ⇇ k → Γ ⊢ k kd
≃-valid-kd (<:-antisym k-kd a<:b b<:a) = k-kd

-- NOTE.  In order to prove validity for the remainder of the kinding,
-- subkinding and subtyping judgments, we first need to prove that
-- hereditary substitutions preserve well-formedness of kinds (see
-- Kinding.Canonical.HereditarySubstitution).  See the definition of
-- `Var∈-valid' below and the module Kinding.Canonical.Validity for
-- the remaining (strong) validity lemmas.

-- The synthesized kinds of neutrals kind-check.
Nf⇇-ne : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Ne a ∈ b ⋯ c → Γ ⊢Nf a ⇇ b ⋯ c
Nf⇇-ne (∈-∙ x∈k k⇉as⇉b⋯c) =
  ⇇-⇑ (⇉-s-i (∈-∙ x∈k k⇉as⇉b⋯c))
      (<∷-⋯ (<:-⟨| (∈-∙ x∈k k⇉as⇉b⋯c)) (<:-|⟩ (∈-∙ x∈k k⇉as⇉b⋯c)))

-- The contexts of (most of) the above judgments are well-formed.
--
-- NOTE. The exceptions are kinding and equality of spines, as the
-- ⇉-[] and ≃-[] rules offer no guarantee that the enclosing context
-- is well-formed.  This is not a problem in practice, since
-- well-kinded spines are used in the kinding of neutral types, the
-- head of which is guaranteed to be kinded in a well-formed context.
mutual

  kd-ctx : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ctx
  kd-ctx (kd-⋯ a⇉a⋯a b⇉b⋯b) = Nf⇉-ctx a⇉a⋯a
  kd-ctx (kd-Π j-kd  k-kd)  = kd-ctx j-kd

  Nf⇉-ctx : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Nf a ⇉ k → Γ ctx
  Nf⇉-ctx (⇉-⊥-f Γ-ctx)       = Γ-ctx
  Nf⇉-ctx (⇉-⊤-f Γ-ctx)       = Γ-ctx
  Nf⇉-ctx (⇉-∀-f k-kd  a⇉a⋯a) = kd-ctx k-kd
  Nf⇉-ctx (⇉-→-f a⇉a⋯a b⇉b⋯b) = Nf⇉-ctx a⇉a⋯a
  Nf⇉-ctx (⇉-Π-i j-kd  a⇉k)   = kd-ctx j-kd
  Nf⇉-ctx (⇉-s-i a∈b⋯c)       = Ne∈-ctx a∈b⋯c

  Ne∈-ctx : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Ne a ∈ k → Γ ctx
  Ne∈-ctx (∈-∙ x∈j j⇉as⇉k) = Var∈-ctx x∈j

  Var∈-ctx : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Var a ∈ k → Γ ctx
  Var∈-ctx (⇉-var x Γ-ctx _)   = Γ-ctx
  Var∈-ctx (⇇-⇑ x∈j j<∷k k-kd) = Var∈-ctx x∈j

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

mutual

  <∷-ctx : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j <∷ k → Γ ctx
  <∷-ctx (<∷-⋯ b₁<:a₁ a₂<:b₂)          = <:-ctx b₁<:a₁
  <∷-ctx (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) = <∷-ctx j₂<∷j₁

  <:-ctx : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a <: b → Γ ctx
  <:-ctx (<:-trans a<:b b<:c)   = <:-ctx a<:b
  <:-ctx (<:-⊥ a⇉a⋯a)           = Nf⇉-ctx a⇉a⋯a
  <:-ctx (<:-⊤ a⇉a⋯a)           = Nf⇉-ctx a⇉a⋯a
  <:-ctx (<:-∀ k₂<∷k₁ a₁<:a₂ _) = <∷-ctx k₂<∷k₁
  <:-ctx (<:-→ a₂<:a₁ b₁<:b₂)   = <:-ctx a₂<:a₁
  <:-ctx (<:-∙ x∈j as<:bs)      = Var∈-ctx x∈j
  <:-ctx (<:-⟨| a∈b⋯c)          = Ne∈-ctx a∈b⋯c
  <:-ctx (<:-|⟩ a∈b⋯c)          = Ne∈-ctx a∈b⋯c

  ≅-ctx : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j ≅ k → Γ ctx
  ≅-ctx (<∷-antisym j-kd k-kd j<∷k k<∷j) = <∷-ctx j<∷k

wf-ctx : ∀ {n} {Γ : Ctx n} {a} → Γ ⊢ a wf → Γ ctx
wf-ctx (wf-kd k-kd)  = kd-ctx k-kd
wf-ctx (wf-tp a⇉a⋯a) = Nf⇉-ctx a⇉a⋯a

<:⇇-ctx : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a <: b ⇇ k → Γ ctx
<:⇇-ctx (<:-⇇ a⇇k b⇇k a<:b)               = Nf⇇-ctx a⇇k
<:⇇-ctx (<:-λ a₁<:a₂ Λj₁a₁⇇Πjk Λj₂a₂⇇Πjk) = Nf⇇-ctx Λj₁a₁⇇Πjk

≃-ctx : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a ≃ b ⇇ k → Γ ctx
≃-ctx (<:-antisym k-kd a<:b b<:a) = <:⇇-ctx a<:b

Var′∈-ctx : ∀ {n} {Γ : Ctx n} {x a} → Γ ⊢Var′ x ∈ a → Γ ctx
Var′∈-ctx (∈-tp x∈k)       = Var∈-ctx x∈k
Var′∈-ctx (∈-tm _ Γ-ctx _) = Γ-ctx

-- An admissible formation rule for the kind of proper types.

kd-⌜*⌝ : ∀ {n} {Γ : Ctx n} → Γ ctx → Γ ⊢ ⌜*⌝ kd
kd-⌜*⌝ Γ-ctx = kd-⋯ (⇉-⊥-f Γ-ctx) (⇉-⊤-f Γ-ctx)

-- Admissible formation rules for canonically kinded proper types.

Nf⇇-∀-f : ∀ {n} {Γ : Ctx n} {k a} →
          Γ ⊢ k kd → kd k ∷ Γ ⊢Nf a ⇇ ⌜*⌝ → Γ ⊢Nf ∀∙ k a ⇇ ⌜*⌝
Nf⇇-∀-f k-kd a⇇* =
  let a⇉a⋯a = Nf⇇-s-i a⇇*
  in Nf⇉-⋯-* (⇉-∀-f k-kd a⇉a⋯a)

Nf⇇-→-f : ∀ {n} {Γ : Ctx n} {a b} →
          Γ ⊢Nf a ⇇ ⌜*⌝ → Γ ⊢Nf b ⇇ ⌜*⌝ → Γ ⊢Nf a ⇒∙ b ⇇ ⌜*⌝
Nf⇇-→-f a⇇* b⇇* =
  let a⇉a⋯a = Nf⇇-s-i a⇇*
      b⇉b⋯b = Nf⇇-s-i b⇇*
  in Nf⇉-⋯-* (⇉-→-f a⇉a⋯a b⇉b⋯b)

-- Admissible kinding and equality rules for appending a normal form
-- to a spine.

⇉-∷ʳ : ∀ {n} {Γ : Ctx n} {as : Spine n} {a j k l} →
       Γ ⊢ j ⇉∙ as ⇉ Π k l → Γ ⊢Nf a ⇇ k → Γ ⊢ k kd →
       Γ ⊢ j ⇉∙ as ∷ʳ a ⇉ l Kind[ a ∈ ⌊ k ⌋ ]
⇉-∷ʳ ⇉-[]                       a⇇k k-kd = ⇉-∷ a⇇k k-kd ⇉-[]
⇉-∷ʳ (⇉-∷ a⇇j j-kd k[a]⇉as⇉Πlm) b⇇l l-kd =
  ⇉-∷ a⇇j j-kd (⇉-∷ʳ k[a]⇉as⇉Πlm b⇇l l-kd)

≃-∷ʳ : ∀ {n} {Γ : Ctx n} {as bs : Spine n} {a b j k l} →
       Γ ⊢ j ⇉∙ as ≃ bs ⇉ Π k l → Γ ⊢ a ≃ b ⇇ k →
       Γ ⊢ j ⇉∙ as ∷ʳ a ≃ bs ∷ʳ b ⇉ l Kind[ a ∈ ⌊ k ⌋ ]
≃-∷ʳ ≃-[]            a≃b = ≃-∷ a≃b ≃-[]
≃-∷ʳ (≃-∷ a≃b as≃bs) c≃d = ≃-∷ a≃b (≃-∷ʳ as≃bs c≃d)

----------------------------------------------------------------------
-- Well-kinded variable substitutions in canonically kinded types
--
-- We define two different kinds of well-kinded variable
-- substitutions:
--
--  1. well-kinded renamings, which don't change kinds of variables,
--
--  2. variable substitutions that also allow conversion/subsumption.
--
-- The first kind are used to prove e.g. that weakening preserve
-- (canonical) well-kindedness, while the second kind are used to
-- prove context conversion/narrowing preserves well-kindedness.  The
-- two definitions share a common generic core, which is instantiated
-- to obtain the concrete definitions.  The two separate definitions
-- are necessary because the latter requires the weakening lemma,
-- which in turn depends on the former.

-- Liftings between variable typings

record LiftTo-Var′∈ (_⊢V_∈_ : Typing ElimAsc Fin ElimAsc lzero) : Set₁ where
  open Substitution using (weakenElimAsc; _ElimAsc/Var_)

  typedSub : TypedSub ElimAsc Fin lzero
  typedSub = record
    { _⊢_wf               = _⊢_wf
    ; _⊢_∈_               = _⊢V_∈_
    ; typeExtension       = record { weaken = weakenElimAsc }
    ; typeTermApplication = record { _/_ = _ElimAsc/Var_ }
    ; termSimple          = VarSubst.simple
    }
  open TypedSub typedSub public
    renaming (_⊢/_∈_ to _⊢/Var_∈_) hiding (_⊢_wf; _⊢_∈_; typeExtension)

  -- Simple typed variable substitutions.

  field typedSimple : TypedSimple typedSub
  open TypedSimple typedSimple public renaming (lookup to /∈-lookup)

  -- Lifts well-typed Term₁-terms to well-typed Term₂-terms.

  field ∈-lift : ∀ {n} {Γ : Ctx n} {x a} → Γ ⊢V x ∈ a → Γ ⊢Var′ x ∈ a

module TypedVarSubstApp (_⊢V_∈_ : Typing ElimAsc Fin ElimAsc lzero)
                        (liftTyped : LiftTo-Var′∈ _⊢V_∈_)
                        where

  open LiftTo-Var′∈ liftTyped
  open Substitution hiding (subst; _/Var_) renaming (_Elim/Var_ to _/Var_)
  open RenamingCommutes using (Kind[∈⌊⌋]-/Var)

  -- A helper.

  ∈-↑′ : ∀ {m n} {Δ : Ctx n} {Γ : Ctx m} {k ρ} →
         Δ ⊢ k Kind′/Var ρ kd → Δ ⊢/Var ρ ∈ Γ →
         kd (k Kind′/Var ρ) ∷ Δ ⊢/Var ρ VarSubst.↑ ∈ kd k ∷ Γ
  ∈-↑′ k/ρ-kd ρ∈Γ = ∈-↑ (wf-kd k/ρ-kd) ρ∈Γ

  -- Convert between well-kindedness judgments for variables.

  V∈-Var∈ : ∀ {n} {Γ : Ctx n} {x a k} → a ≡ kd k →
            Γ ⊢V x ∈ a → Γ ⊢Var x ∈ k
  V∈-Var∈ refl xT∈kd-k with ∈-lift xT∈kd-k
  V∈-Var∈ refl xT∈kd-k | ∈-tp x∈k = x∈k

  mutual

    -- Renamings preserve well-formedness of ascriptions.

    wf-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a ρ} →
              Γ ⊢ a wf → Δ ⊢/Var ρ ∈ Γ → Δ ⊢ a ElimAsc/Var ρ wf
    wf-/Var (wf-kd k-kd)  ρ∈Γ = wf-kd (kd-/Var k-kd ρ∈Γ)
    wf-/Var (wf-tp a⇉a⋯a) ρ∈Γ = wf-tp (Nf⇉-/Var a⇉a⋯a ρ∈Γ)

    -- Renamings preserve well-formedness of kinds.

    kd-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {k ρ} →
              Γ ⊢ k kd → Δ ⊢/Var ρ ∈ Γ → Δ ⊢ k Kind′/Var ρ kd
    kd-/Var (kd-⋯ a⇉a⋯a b⇉b⋯b) ρ∈Γ =
      kd-⋯ (Nf⇉-/Var a⇉a⋯a ρ∈Γ) (Nf⇉-/Var b⇉b⋯b ρ∈Γ)
    kd-/Var (kd-Π j-kd  k-kd) ρ∈Γ =
      let j/ρ-kd = kd-/Var j-kd ρ∈Γ
      in kd-Π j/ρ-kd (kd-/Var k-kd (∈-↑′ j/ρ-kd ρ∈Γ))

    -- Renamings preserve synthesized kinds of normal types.

    Nf⇉-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a k ρ} →
               Γ ⊢Nf a ⇉ k → Δ ⊢/Var ρ ∈ Γ → Δ ⊢Nf a /Var ρ ⇉ k Kind′/Var ρ
    Nf⇉-/Var (⇉-⊥-f Γ-ctx)       ρ∈Γ = ⇉-⊥-f (/∈-wf ρ∈Γ)
    Nf⇉-/Var (⇉-⊤-f Γ-ctx)       ρ∈Γ = ⇉-⊤-f (/∈-wf ρ∈Γ)
    Nf⇉-/Var (⇉-∀-f k-kd a⇉a⋯a)  ρ∈Γ =
      let k/ρ-kd = kd-/Var k-kd ρ∈Γ
      in ⇉-∀-f k/ρ-kd (Nf⇉-/Var a⇉a⋯a (∈-↑′ k/ρ-kd ρ∈Γ))
    Nf⇉-/Var (⇉-→-f a⇉a⋯a b⇉b⋯b) ρ∈Γ =
      ⇉-→-f (Nf⇉-/Var a⇉a⋯a ρ∈Γ) (Nf⇉-/Var b⇉b⋯b ρ∈Γ)
    Nf⇉-/Var (⇉-Π-i j-kd a⇉k)    ρ∈Γ =
      let j/ρ-kd = kd-/Var j-kd ρ∈Γ
      in ⇉-Π-i j/ρ-kd (Nf⇉-/Var a⇉k (∈-↑′ j/ρ-kd ρ∈Γ))
    Nf⇉-/Var (⇉-s-i a∈b⋯c)       ρ∈Γ = ⇉-s-i (Ne∈-/Var a∈b⋯c ρ∈Γ)

    -- Renamings preserve the kinds of variables.

    Var∈-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {x k ρ} →
                Γ ⊢Var x ∈ k → Δ ⊢/Var ρ ∈ Γ →
                Δ ⊢Var (Vec.lookup ρ x) ∈ k Kind′/Var ρ
    Var∈-/Var {ρ = ρ} (⇉-var x Γ-ctx Γ[x]≡kd-k) ρ∈Γ =
      V∈-Var∈ (cong (_ElimAsc/Var ρ) Γ[x]≡kd-k) (/∈-lookup ρ∈Γ x)
    Var∈-/Var (⇇-⇑ x∈j j<∷k k-kd) ρ∈Γ =
      ⇇-⇑ (Var∈-/Var x∈j ρ∈Γ) (<∷-/Var j<∷k ρ∈Γ) (kd-/Var k-kd ρ∈Γ)

    -- Renamings preserve synthesized kinds of neutral types.

    Ne∈-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a k ρ} →
               Γ ⊢Ne a ∈ k → Δ ⊢/Var ρ ∈ Γ → Δ ⊢Ne a /Var ρ ∈ k Kind′/Var ρ
    Ne∈-/Var (∈-∙ x∈j k⇉as⇉l) ρ∈Γ =
      ∈-∙ (Var∈-/Var x∈j ρ∈Γ) (Sp⇉-/Var k⇉as⇉l ρ∈Γ)

    -- Renamings preserve spine kindings.

    Sp⇉-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {as j k ρ} →
               Γ ⊢ j ⇉∙ as ⇉ k → Δ ⊢/Var ρ ∈ Γ →
               Δ ⊢ j Kind′/Var ρ ⇉∙ as //Var ρ ⇉ k Kind′/Var ρ
    Sp⇉-/Var ⇉-[]                                ρ∈Γ = ⇉-[]
    Sp⇉-/Var (⇉-∷ {a} {_} {j} {k} a⇇j j-kd k[a]⇉as⇉l) ρ∈Γ =
      ⇉-∷ (Nf⇇-/Var a⇇j ρ∈Γ) (kd-/Var j-kd ρ∈Γ)
          (subst (_ ⊢_⇉∙ _ ⇉ _) (Kind[∈⌊⌋]-/Var k a j)
                 (Sp⇉-/Var k[a]⇉as⇉l ρ∈Γ))

    -- Renamings preserve checked kinds of neutral types.

    Nf⇇-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a k ρ} →
               Γ ⊢Nf a ⇇ k → Δ ⊢/Var ρ ∈ Γ → Δ ⊢Nf a /Var ρ ⇇ k Kind′/Var ρ
    Nf⇇-/Var (⇇-⇑ a⇉j j<∷k) ρ∈Γ = ⇇-⇑ (Nf⇉-/Var a⇉j ρ∈Γ) (<∷-/Var j<∷k ρ∈Γ)

    -- Renamings preserve subkinding.

    <∷-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k ρ} →
              Γ ⊢ j <∷ k → Δ ⊢/Var ρ ∈ Γ → Δ ⊢ j Kind′/Var ρ <∷ k Kind′/Var ρ
    <∷-/Var (<∷-⋯ a₂<:a₁ b₁<:b₂) ρ∈Γ =
      <∷-⋯ (<:-/Var a₂<:a₁ ρ∈Γ) (<:-/Var b₁<:b₂ ρ∈Γ)
    <∷-/Var (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) ρ∈Γ =
      <∷-Π (<∷-/Var j₂<∷j₁ ρ∈Γ)
           (<∷-/Var k₁<∷k₂ (∈-↑ (<∷-/Var-wf k₁<∷k₂ ρ∈Γ) ρ∈Γ))
           (kd-/Var Πj₁k₁-kd ρ∈Γ)

    -- Renamings preserve subtyping.

    <:-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b ρ} →
              Γ ⊢ a <: b → Δ ⊢/Var ρ ∈ Γ → Δ ⊢ a /Var ρ <: b /Var ρ
    <:-/Var (<:-trans a<:b b<:c) ρ∈Γ =
      <:-trans (<:-/Var a<:b ρ∈Γ) (<:-/Var b<:c ρ∈Γ)
    <:-/Var (<:-⊥ a⇉a⋯a) ρ∈Γ = <:-⊥ (Nf⇉-/Var a⇉a⋯a ρ∈Γ)
    <:-/Var (<:-⊤ a⇉a⋯a) ρ∈Γ = <:-⊤ (Nf⇉-/Var a⇉a⋯a ρ∈Γ)
    <:-/Var (<:-∀ k₂<∷k₁ a₁<:a₂ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁) ρ∈Γ =
      <:-∀ (<∷-/Var k₂<∷k₁ ρ∈Γ)
           (<:-/Var a₁<:a₂ (∈-↑ (<:-/Var-wf a₁<:a₂ ρ∈Γ) ρ∈Γ))
           (Nf⇉-/Var Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁ ρ∈Γ)
    <:-/Var (<:-→ a₂<:a₁ b₁<:b₂) ρ∈Γ =
      <:-→ (<:-/Var a₂<:a₁ ρ∈Γ) (<:-/Var b₁<:b₂ ρ∈Γ)
    <:-/Var (<:-∙ x∈j j⇉as₁<:as₂⇉k) ρ∈Γ =
      <:-∙ (Var∈-/Var x∈j ρ∈Γ) (Sp≃-/Var j⇉as₁<:as₂⇉k ρ∈Γ)
    <:-/Var (<:-⟨| a∈b⋯c) ρ∈Γ = <:-⟨| (Ne∈-/Var a∈b⋯c ρ∈Γ)
    <:-/Var (<:-|⟩ a∈b⋯c) ρ∈Γ = <:-|⟩ (Ne∈-/Var a∈b⋯c ρ∈Γ)

    <:⇇-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b k ρ} →
               Γ ⊢ a <: b ⇇ k → Δ ⊢/Var ρ ∈ Γ →
               Δ ⊢ a /Var ρ <: b /Var ρ ⇇ k Kind′/Var ρ
    <:⇇-/Var (<:-⇇ a⇇k b⇇k a<:b) ρ∈Γ =
      <:-⇇ (Nf⇇-/Var a⇇k ρ∈Γ) (Nf⇇-/Var b⇇k ρ∈Γ) (<:-/Var a<:b ρ∈Γ)
    <:⇇-/Var (<:-λ a₁<:a₂ Λj₁a₁⇇Πjk Λj₂a₂⇇Πjk) ρ∈Γ =
      <:-λ (<:⇇-/Var a₁<:a₂ (∈-↑ (<:⇇-/Var-wf a₁<:a₂ ρ∈Γ) ρ∈Γ))
           (Nf⇇-/Var Λj₁a₁⇇Πjk ρ∈Γ) (Nf⇇-/Var Λj₂a₂⇇Πjk ρ∈Γ)

    -- Renamings preserve type equality.

    ≃-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b k ρ} →
              Γ ⊢ a ≃ b ⇇ k → Δ ⊢/Var ρ ∈ Γ →
              Δ ⊢ a /Var ρ ≃ b /Var ρ ⇇ k Kind′/Var ρ
    ≃-/Var (<:-antisym k-kd a<:b b<:a) ρ∈Γ =
      <:-antisym (kd-/Var k-kd ρ∈Γ) (<:⇇-/Var a<:b ρ∈Γ) (<:⇇-/Var b<:a ρ∈Γ)

    Sp≃-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {as bs j k ρ} →
                Γ ⊢ j ⇉∙ as ≃ bs ⇉ k → Δ ⊢/Var ρ ∈ Γ →
                Δ ⊢ j Kind′/Var ρ ⇉∙ as //Var ρ ≃ bs //Var ρ ⇉ k Kind′/Var ρ
    Sp≃-/Var ≃-[] ρ∈Γ = ≃-[]
    Sp≃-/Var (≃-∷ {a} {_} {_} {_} {j} {k} a≃b as≃bs) ρ∈Γ =
      ≃-∷ (≃-/Var a≃b ρ∈Γ)
          (subst (_ ⊢_⇉∙ _ ≃ _ ⇉ _) (Kind[∈⌊⌋]-/Var k a j)
                 (Sp≃-/Var as≃bs ρ∈Γ))

    -- Helpers (to satisfy the termination checker).
    --
    -- These are simply (manual) expansions of the form
    --
    --   XX-/Var-wf x ρ∈Γ  =  wf-/Var (wf-∷₁ (XX-ctx x)) ρ∈Γ
    --
    -- to ensure the above definitions remain structurally recursive
    -- in the various derivations.

    kd-/Var-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k ρ} →
                 kd j ∷ Γ ⊢ k kd → Δ ⊢/Var ρ ∈ Γ → Δ ⊢ kd (j Kind′/Var ρ) wf
    kd-/Var-wf (kd-⋯ a∈a⋯a _) ρ∈Γ = Nf⇉-/Var-wf a∈a⋯a ρ∈Γ
    kd-/Var-wf (kd-Π j-kd _)  ρ∈Γ = kd-/Var-wf j-kd ρ∈Γ

    Nf⇉-/Var-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a j k ρ} →
                  kd j ∷ Γ ⊢Nf a ⇉ k → Δ ⊢/Var ρ ∈ Γ →
                  Δ ⊢ kd (j Kind′/Var ρ) wf
    Nf⇉-/Var-wf (⇉-⊥-f (j-wf ∷ _)) ρ∈Γ = wf-/Var j-wf ρ∈Γ
    Nf⇉-/Var-wf (⇉-⊤-f (j-wf ∷ _)) ρ∈Γ = wf-/Var j-wf ρ∈Γ
    Nf⇉-/Var-wf (⇉-∀-f k-kd _)     ρ∈Γ = kd-/Var-wf k-kd ρ∈Γ
    Nf⇉-/Var-wf (⇉-→-f a⇉a⋯a _)    ρ∈Γ = Nf⇉-/Var-wf a⇉a⋯a ρ∈Γ
    Nf⇉-/Var-wf (⇉-Π-i j-kd _)     ρ∈Γ = kd-/Var-wf j-kd ρ∈Γ
    Nf⇉-/Var-wf (⇉-s-i a∈b⋯c)      ρ∈Γ = Ne∈-/Var-wf a∈b⋯c ρ∈Γ

    Ne∈-/Var-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a j k ρ} →
                  kd j ∷ Γ ⊢Ne a ∈ k → Δ ⊢/Var ρ ∈ Γ →
                  Δ ⊢ kd (j Kind′/Var ρ) wf
    Ne∈-/Var-wf (∈-∙ x∈k _) ρ∈Γ = Var∈-/Var-wf x∈k ρ∈Γ

    Var∈-/Var-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a j k ρ} →
                   kd j ∷ Γ ⊢Var a ∈ k → Δ ⊢/Var ρ ∈ Γ →
                   Δ ⊢ kd (j Kind′/Var ρ) wf
    Var∈-/Var-wf (⇉-var x (j-wf ∷ _) _) ρ∈Γ = wf-/Var j-wf ρ∈Γ
    Var∈-/Var-wf (⇇-⇑ x∈j _ _)          ρ∈Γ = Var∈-/Var-wf x∈j ρ∈Γ

    Nf⇇-/Var-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a j k ρ} →
                  kd j ∷ Γ ⊢Nf a ⇇ k → Δ ⊢/Var ρ ∈ Γ →
                  Δ ⊢ kd (j Kind′/Var ρ) wf
    Nf⇇-/Var-wf (⇇-⇑ a⇉j _) ρ∈Γ = Nf⇉-/Var-wf a⇉j ρ∈Γ

    <∷-/Var-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k l ρ} →
                 kd j ∷ Γ ⊢ k <∷ l → Δ ⊢/Var ρ ∈ Γ → Δ ⊢ kd (j Kind′/Var ρ) wf
    <∷-/Var-wf (<∷-⋯ a₂<:a₁ _)   ρ∈Γ = <:-/Var-wf a₂<:a₁ ρ∈Γ
    <∷-/Var-wf (<∷-Π j₂<∷j₁ _ _) ρ∈Γ = <∷-/Var-wf j₂<∷j₁ ρ∈Γ

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

    <:⇇-/Var-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b j k ρ} →
                  kd j ∷ Γ ⊢ a <: b ⇇ k → Δ ⊢/Var ρ ∈ Γ →
                  Δ ⊢ kd (j Kind′/Var ρ) wf
    <:⇇-/Var-wf (<:-⇇ a⇇k _ _)       ρ∈Γ = Nf⇇-/Var-wf a⇇k ρ∈Γ
    <:⇇-/Var-wf (<:-λ _ Λj₁a₁⇇Πjk _) ρ∈Γ = Nf⇇-/Var-wf Λj₁a₁⇇Πjk ρ∈Γ

    ≅-/Var-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k l ρ} →
                kd j ∷ Γ ⊢ k ≅ l → Δ ⊢/Var ρ ∈ Γ → Δ ⊢ kd (j Kind′/Var ρ) wf
    ≅-/Var-wf (<∷-antisym _ _ j<∷k _) ρ∈Γ = <∷-/Var-wf j<∷k ρ∈Γ

  -- Renamings preserve kind equality.

  ≅-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k ρ} →
           Γ ⊢ j ≅ k → Δ ⊢/Var ρ ∈ Γ → Δ ⊢ j Kind′/Var ρ ≅ k Kind′/Var ρ
  ≅-/Var (<∷-antisym j-kd k-kd j<∷k k<∷j) ρ∈Γ =
    <∷-antisym (kd-/Var j-kd ρ∈Γ) (kd-/Var k-kd ρ∈Γ)
               (<∷-/Var j<∷k ρ∈Γ) (<∷-/Var k<∷j ρ∈Γ)

  -- Renamings preserve wrapped variable typing

  Var′∈-/Var : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {x k ρ} →
               Γ ⊢Var′ x ∈ k → Δ ⊢/Var ρ ∈ Γ →
               Δ ⊢Var′ (Vec.lookup ρ x) ∈ k ElimAsc/Var ρ
  Var′∈-/Var         (∈-tp x∈k)               ρ∈Γ = ∈-tp (Var∈-/Var x∈k ρ∈Γ)
  Var′∈-/Var {ρ = ρ} (∈-tm x Γ-ctx Γ[x]≡tp-t) ρ∈Γ =
    subst (_ ⊢Var′ _ ∈_) (cong (_ElimAsc/Var ρ) Γ[x]≡tp-t)
          (∈-lift (/∈-lookup ρ∈Γ x))

-- Well-kinded renamings in canonically kinded types, i.e. lemmas
-- showing that renaming preserves kinding.
--
-- Note that these are pure renamings that cannot change the kinds of
-- variables (i.e. they cannot be used to implement context conversion
-- or narrowing).

module KindedRenaming where
  open Substitution using (termLikeLemmasElimAsc)

  typedVarSubst : TypedVarSubst ElimAsc lzero
  typedVarSubst = record
    { _⊢_wf              = _⊢_wf
    ; typeExtension      = ElimCtx.weakenOps
    ; typeVarApplication = AppLemmas.application appLemmas
    ; wf-wf              = wf-ctx
    ; /-wk               = refl
    ; id-vanishes        = id-vanishes
    ; /-⊙                 = /-⊙
    }
    where
      open TermLikeLemmas termLikeLemmasElimAsc using (varLiftAppLemmas)
      open LiftAppLemmas  varLiftAppLemmas

  open TypedVarSubst typedVarSubst
    hiding (_⊢_wf) renaming (_⊢Var_∈_ to _⊢GenVar_∈_)

  -- Liftings from generic variable typings to variable kindings.

  liftTyped : LiftTo-Var′∈ _⊢GenVar_∈_
  liftTyped = record
    { typedSimple  = typedSimple
    ; ∈-lift       = ∈-lift
    }
    where
      ∈-lift : ∀ {n} {Γ : Ctx n} {x a} → Γ ⊢GenVar x ∈ a → Γ ⊢Var′ x ∈ a
      ∈-lift (∈-var x Γ-ctx) = ∈-var′ x Γ-ctx

  open TypedVarSubstApp _⊢GenVar_∈_ liftTyped public
  open Substitution hiding (subst)

  -- Weakening preserves well-formedness of kinds.

  kd-weaken : ∀ {n} {Γ : Ctx n} {a k} →
              Γ ⊢ a wf → Γ ⊢ k kd → a ∷ Γ ⊢ weakenKind′ k kd
  kd-weaken a-wf k-kd = kd-/Var k-kd (∈-wk a-wf)

  -- Weakening preserves variable kinding.

  Var∈-weaken : ∀ {n} {Γ : Ctx n} {a x k} → Γ ⊢ a wf →
                Γ ⊢Var x ∈ k →
                a ∷ Γ ⊢Var Vec.lookup VarSubst.wk x ∈ weakenKind′ k
  Var∈-weaken a-wf x∈k = Var∈-/Var x∈k (∈-wk a-wf)

  Var′∈-weaken : ∀ {n} {Γ : Ctx n} {a x b} → Γ ⊢ a wf →
                 Γ ⊢Var′ x ∈ b → a ∷ Γ ⊢Var′ suc x ∈ weakenElimAsc b
  Var′∈-weaken a-wf x∈b =
    subst (_ ⊢Var′_∈ _) VarLemmas./-wk (Var′∈-/Var x∈b (∈-wk a-wf))

  -- Weakening preserves spine kinding.

  Sp⇉-weaken : ∀ {n} {Γ : Ctx n} {a bs j k} → Γ ⊢ a wf → Γ ⊢ j ⇉∙ bs ⇉ k →
               a ∷ Γ ⊢ weakenKind′ j ⇉∙ weakenSpine bs ⇉ weakenKind′ k
  Sp⇉-weaken a-wf j⇉bs⇉k = Sp⇉-/Var j⇉bs⇉k (∈-wk a-wf)

  -- Weakening preserves checked kinding.

  Nf⇇-weaken : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a wf →
               Γ ⊢Nf b ⇇ k → (a ∷ Γ) ⊢Nf weakenElim b ⇇ weakenKind′ k
  Nf⇇-weaken a-wf b⇇k = Nf⇇-/Var b⇇k (∈-wk a-wf)

  -- Weakening preserves subkinding.

  <∷-weaken : ∀ {n} {Γ : Ctx n} {a j k} → Γ ⊢ a wf →
              Γ ⊢ j <∷ k → (a ∷ Γ) ⊢ weakenKind′ j <∷ weakenKind′ k
  <∷-weaken a-wf j<∷k = <∷-/Var j<∷k (∈-wk a-wf)

  -- Weakening preserves subtyping.

  <:-weaken : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢ a wf → Γ ⊢ b <: c →
              a ∷ Γ ⊢ weakenElim b <: weakenElim c
  <:-weaken a-wf b<:c = <:-/Var b<:c (∈-wk a-wf)

  <:⇇-weaken : ∀ {n} {Γ : Ctx n} {a b c k} → Γ ⊢ a wf → Γ ⊢ b <: c ⇇ k →
               a ∷ Γ ⊢ weakenElim b <: weakenElim c ⇇ weakenKind′ k
  <:⇇-weaken a-wf b<:c = <:⇇-/Var b<:c (∈-wk a-wf)

  -- Weakening preserves well-formedness of ascriptions.

  wf-weaken : ∀ {n} {Γ : Ctx n} {a b} →
              Γ ⊢ a wf → Γ ⊢ b wf → a ∷ Γ ⊢ weakenElimAsc b wf
  wf-weaken a-wf b-wf = wf-/Var b-wf (∈-wk a-wf)

  -- Weakening preserves kind and type equality.

  ≃-weaken : ∀ {n} {Γ : Ctx n} {a b c k} → Γ ⊢ a wf → Γ ⊢ b ≃ c ⇇ k →
              a ∷ Γ ⊢ weakenElim b ≃ weakenElim c ⇇ weakenKind′ k
  ≃-weaken a-wf b≃c = ≃-/Var b≃c (∈-wk a-wf)

  ≅-weaken : ∀ {n} {Γ : Ctx n} {a j k} → Γ ⊢ a wf → Γ ⊢ j ≅ k →
             a ∷ Γ ⊢ weakenKind′ j ≅ weakenKind′ k
  ≅-weaken a-wf j≅k = ≅-/Var j≅k (∈-wk a-wf)

  Sp≃-weaken : ∀ {n} {Γ : Ctx n} {a bs cs j k} → Γ ⊢ a wf →
               Γ ⊢ j ⇉∙ bs ≃ cs ⇉ k →
               a ∷ Γ ⊢ weakenKind′ j ⇉∙ weakenSpine bs ≃ weakenSpine cs ⇉
                 weakenKind′ k
  Sp≃-weaken a-wf bs≃cs = Sp≃-/Var bs≃cs (∈-wk a-wf)

-- Operations on well-formed contexts that require weakening of
-- well-formedness judgments.

module WfCtxOps where
  open KindedRenaming using (wf-weaken)

  wfWeakenOps : WellFormedWeakenOps weakenOps
  wfWeakenOps = record { wf-weaken = wf-weaken }

  open WellFormedWeakenOps wfWeakenOps public
    hiding (wf-weaken) renaming (lookup to lookup-wf)

  -- Lookup the kind of a type variable in a well-formed context.

  lookup-kd : ∀ {m} {Γ : Ctx m} {k} x →
              Γ ctx → ElimCtx.lookup Γ x ≡ kd k → Γ ⊢ k kd
  lookup-kd x Γ-ctx Γ[x]≡kd-k =
    wf-kd-inv (subst (_ ⊢_wf) Γ[x]≡kd-k (lookup-wf Γ-ctx x))

open WfCtxOps

-- A corollary (validity of variable kinding): the kinds of variables
-- are well-formed.

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

----------------------------------------------------------------------
-- Context narrowing
--
-- The various judgments are preserved by narrowing of kind
-- ascriptions in their contexts.

module ContextNarrowing where
  open Substitution
    using (termLikeLemmasElim; termLikeLemmasKind′; termLikeLemmasElimAsc)
  open TermLikeLemmas termLikeLemmasElimAsc using (varLiftAppLemmas)
  open LiftAppLemmas varLiftAppLemmas
  open KindedRenaming using (kd-weaken; <∷-weaken; Var′∈-weaken)
  private
    module EL = LiftAppLemmas
                (TermLikeLemmas.varLiftAppLemmas termLikeLemmasElim)
    module KL = LiftAppLemmas
                (TermLikeLemmas.varLiftAppLemmas termLikeLemmasKind′)

  -- NOTE. Rather than proving context narrowing directly by induction
  -- on typing derivations, we instead define a more flexible variant
  -- of well-typed variable substitutions based on the canonical
  -- variable kinding judgment (_⊢Var_∈_).  This judgment features a
  -- subsumption rule (∈-⇑), which is not available in the generic
  -- variable judgment from Data.Fin.Substitutions.Typed that we used
  -- to define basic typed renamings.  With support for subsumption in
  -- typed renamings, we get context narrowing "for free", as it is
  -- just another variable substitution (one that happens to change
  -- the kind rather than the name of a variable).  This way of
  -- proving context narrowing is more convenient since we can reuse
  -- the generic lemmas proven for typed variable substitution and
  -- avoid some explicit fiddling with context.
  --
  -- Note also that we could not have defined typed renamings
  -- directly using the _⊢Var_∈_ judgment since that would have
  -- required a weakening lemma for subkiding, which in turn is
  -- implemented via typed renamings.

  -- The trivial lifting from _⊢Var′_∈_ to itself, and simple typed
  -- variable substitutions.

  liftTyped : LiftTo-Var′∈ _⊢Var′_∈_
  liftTyped = record
    { typedSimple      = record
      { typedWeakenOps = record
        { ∈-weaken     = Var′∈-weaken
        ; ∈-wf         = Var′∈-ctx
        ; /-wk         = refl
        ; /-weaken     = /-weaken
        ; weaken-/-∷   = weaken-/-∷
        }
      ; ∈-var          = ∈-var′
      ; wf-wf          = wf-ctx
      ; id-vanishes    = id-vanishes
      }
    ; ∈-lift           = λ x∈a → x∈a
    }
    where
      weakenLemmas : WeakenLemmas ElimAsc Fin
      weakenLemmas = record { appLemmas = appLemmas ; /-wk = refl }
      open WeakenLemmas weakenLemmas

  open LiftTo-Var′∈ liftTyped
  open TypedVarSubstApp _⊢Var′_∈_ liftTyped

  -- A typed renaming that narrows the kind of the first type
  -- variable.

  ∈-<∷-sub : ∀ {n} {Γ : Ctx n} {j k} →
             Γ ⊢ j kd → Γ ⊢ j <∷ k → (kd k ∷ Γ) ctx →
             kd j ∷ Γ ⊢/Var id ∈ kd k ∷ Γ
  ∈-<∷-sub j-kd j<∷k k∷Γ-ctx =
    ∈-tsub (∈-tp (⇇-⇑ x∈k (<∷-weaken j-wf j<∷k) k-kd))
    where
      j-wf  = wf-kd j-kd
      Γ-ctx = kd-ctx j-kd
      x∈k   = ⇉-var zero (j-wf ∷ Γ-ctx) refl
      k-kd  = kd-weaken j-wf (wf-kd-inv (wf-∷₁ k∷Γ-ctx))

  -- Narrowing the kind of the first type variable preserves
  -- well-formedness of kinds.

  ⇓-kd : ∀ {n} {Γ : Ctx n} {j₁ j₂ k} →
         Γ ⊢ j₁ kd → Γ ⊢ j₁ <∷ j₂ → kd j₂ ∷ Γ ⊢ k kd → kd j₁ ∷ Γ ⊢ k kd
  ⇓-kd j₁-kd j₁<∷j₂ k-kd =
    subst (_ ⊢_kd) (KL.id-vanishes _)
          (kd-/Var k-kd (∈-<∷-sub j₁-kd j₁<∷j₂ (kd-ctx k-kd)))

  -- Narrowing the kind of the first type variable preserves
  -- well-kindedness.

  ⇓-Nf⇉ : ∀ {n} {Γ : Ctx n} {j₁ j₂ a k} →
          Γ ⊢ j₁ kd → Γ ⊢ j₁ <∷ j₂ → kd j₂ ∷ Γ ⊢Nf a ⇉ k → kd j₁ ∷ Γ ⊢Nf a ⇉ k
  ⇓-Nf⇉ j₁-kd j₁<∷j₂ a⇉k =
    subst₂ (_ ⊢Nf_⇉_) (EL.id-vanishes _) (KL.id-vanishes _)
           (Nf⇉-/Var a⇉k (∈-<∷-sub j₁-kd j₁<∷j₂ (Nf⇉-ctx a⇉k)))

  -- Narrowing the kind of the first type variable preserves
  -- subkinding and subtyping.

  ⇓-<∷ : ∀ {n} {Γ : Ctx n} {j₁ j₂ k₁ k₂} →
         Γ ⊢ j₁ kd → Γ ⊢ j₁ <∷ j₂ → kd j₂ ∷ Γ ⊢ k₁ <∷ k₂ → kd j₁ ∷ Γ ⊢ k₁ <∷ k₂
  ⇓-<∷ j₁-kd j₁<∷j₂ k₁<∷k₂ =
    subst₂ (_ ⊢_<∷_) (KL.id-vanishes _) (KL.id-vanishes _)
           (<∷-/Var k₁<∷k₂ (∈-<∷-sub j₁-kd j₁<∷j₂ (<∷-ctx k₁<∷k₂)))

  ⇓-<: : ∀ {n} {Γ : Ctx n} {j₁ j₂ a₁ a₂} →
         Γ ⊢ j₁ kd → Γ ⊢ j₁ <∷ j₂ → kd j₂ ∷ Γ ⊢ a₁ <: a₂ → kd j₁ ∷ Γ ⊢ a₁ <: a₂
  ⇓-<: j₁-kd j₁<∷j₂ a₁<:a₂ =
    subst₂ (_ ⊢_<:_) (EL.id-vanishes _) (EL.id-vanishes _)
           (<:-/Var a₁<:a₂ (∈-<∷-sub j₁-kd j₁<∷j₂ (<:-ctx a₁<:a₂)))

  ⇓-<:⇇ : ∀ {n} {Γ : Ctx n} {j₁ j₂ a₁ a₂ k} →
          Γ ⊢ j₁ kd → Γ ⊢ j₁ <∷ j₂ → kd j₂ ∷ Γ ⊢ a₁ <: a₂ ⇇ k →
          kd j₁ ∷ Γ ⊢ a₁ <: a₂ ⇇ k
  ⇓-<:⇇ j₁-kd j₁<∷j₂ a₁<:a₂∈k =
    subst (_ ⊢ _ <: _ ⇇_) (KL.id-vanishes _)
          (subst₂ (_ ⊢_<:_⇇ _) (EL.id-vanishes _) (EL.id-vanishes _)
                  (<:⇇-/Var a₁<:a₂∈k
                            (∈-<∷-sub j₁-kd j₁<∷j₂ (<:⇇-ctx a₁<:a₂∈k))))

open KindedRenaming
open ContextNarrowing
open Substitution hiding (subst)
private module TV = TypedVarSubst typedVarSubst

-- Some corollaries of context narrowing: transitivity of subkinding
-- and kind equality are admissible.

<∷-trans : ∀ {n} {Γ : Ctx n} {j k l} → Γ ⊢ j <∷ k → Γ ⊢ k <∷ l → Γ ⊢ j <∷ l
<∷-trans (<∷-⋯ a₂<:a₁ b₁<:b₂) (<∷-⋯ a₃<:a₂ b₂<:b₃) =
  <∷-⋯ (<:-trans a₃<:a₂ a₂<:a₁) (<:-trans b₁<:b₂ b₂<:b₃)
<∷-trans (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) (<∷-Π j₃<∷j₂ k₂<∷k₃ _) =
  let j₃-kd = wf-kd-inv (wf-∷₁ (<∷-ctx k₂<∷k₃))
  in <∷-Π (<∷-trans j₃<∷j₂ j₂<∷j₁)
          (<∷-trans (⇓-<∷ j₃-kd j₃<∷j₂ k₁<∷k₂) k₂<∷k₃) Πj₁k₁-kd

≅-trans : ∀ {n} {Γ : Ctx n} {j k l} → Γ ⊢ j ≅ k → Γ ⊢ k ≅ l → Γ ⊢ j ≅ l
≅-trans (<∷-antisym j-kd _ j<∷k k<∷j) (<∷-antisym _ l-kd k<∷l l<∷k) =
  <∷-antisym j-kd l-kd (<∷-trans j<∷k k<∷l) (<∷-trans l<∷k k<∷j)

-- Some more corollaries: subsumption is admissible in canonical kind
-- checking, checked subtyping and kind equality.
--
-- NOTE. The proof of (<:⇇-⇑) is by induction on subkinding
-- derivations (the second hypothesis) rather than kinding derivations
-- (the first hypothesis).

Nf⇇-⇑ : ∀ {n} {Γ : Ctx n} {a j k} → Γ ⊢Nf a ⇇ j → Γ ⊢ j <∷ k → Γ ⊢Nf a ⇇ k
Nf⇇-⇑ (⇇-⇑ a⇇j₁ j₁<∷j₂) j₂<∷j₃ = ⇇-⇑ a⇇j₁ (<∷-trans j₁<∷j₂ j₂<∷j₃)

<:⇇-⇑ : ∀ {n} {Γ : Ctx n} {a b j k} →
        Γ ⊢ a <: b ⇇ j → Γ ⊢ j <∷ k → Γ ⊢ k kd → Γ ⊢ a <: b ⇇ k
<:⇇-⇑ (<:-⇇ a⇇c₁⋯d₁ b⇇c₁⋯d₁ a<:b) (<∷-⋯ c₂<:c₁ d₁<:d₂) _ =
  <:-⇇ (Nf⇇-⇑ a⇇c₁⋯d₁ (<∷-⋯ c₂<:c₁ d₁<:d₂))
       (Nf⇇-⇑ b⇇c₁⋯d₁ (<∷-⋯ c₂<:c₁ d₁<:d₂)) a<:b
<:⇇-⇑ (<:-λ a₁<:a₂ Λj₁a₁⇇Πk₁l₁ Λj₂a₂⇇Πk₁l₁) (<∷-Π k₂<∷k₁ l₁<∷l₂ Πk₁l₁-kd)
      (kd-Π k₂-kd l₂-kd) =
  <:-λ (<:⇇-⇑ (⇓-<:⇇ k₂-kd k₂<∷k₁ a₁<:a₂) l₁<∷l₂ l₂-kd)
       (Nf⇇-⇑ Λj₁a₁⇇Πk₁l₁ (<∷-Π k₂<∷k₁ l₁<∷l₂ Πk₁l₁-kd))
       (Nf⇇-⇑ Λj₂a₂⇇Πk₁l₁ (<∷-Π k₂<∷k₁ l₁<∷l₂ Πk₁l₁-kd))

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

------------------------------------------------------------------------
-- Reflexivity of the various relations.
--
-- NOTE. The proof is by mutual induction in the structure of the
-- types and kinds being related to themselves, and then by
-- case-analysis on formation/kinding derivations (rather than
-- induction on the typing/kinding derivations directly).  For
-- example, the proof of (<:⇇-reflNf⇉-⇑) is not decreasing in the
-- kinding derivation of `a' in the type abstraction (Π-intro) case.
-- To avoid clutter, we do not make the corresponding type/kind
-- parameters explicit in the implementations below: thanks to the
-- structure of canonical formation/kinding, every kind/type
-- constructor corresponds to exactly one kinding/typing rule
-- (i.e. the rules are syntax directed).

mutual

  -- Reflexivity of canonical subkinding.
  <∷-refl : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ⊢ k <∷ k
  <∷-refl (kd-⋯ a⇉a⋯a b⇉b⋯b) = <∷-⋯ (<:-reflNf⇉ a⇉a⋯a) (<:-reflNf⇉ b⇉b⋯b)
  <∷-refl (kd-Π j-kd k-kd)   =
    <∷-Π (<∷-refl j-kd) (<∷-refl k-kd) (kd-Π j-kd k-kd)

  -- Reflexivity of canonical subtyping.

  <:-reflNf⇉ : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇉ b ⋯ c → Γ ⊢ a <: a
  <:-reflNf⇉ (⇉-⊥-f Γ-ctx)       = <:-⊥ (⇉-⊥-f Γ-ctx)
  <:-reflNf⇉ (⇉-⊤-f Γ-ctx)       = <:-⊤ (⇉-⊤-f Γ-ctx)
  <:-reflNf⇉ (⇉-∀-f k-kd a⇉a⋯a)  =
    <:-∀ (<∷-refl k-kd) (<:-reflNf⇉ a⇉a⋯a) (⇉-∀-f k-kd a⇉a⋯a)
  <:-reflNf⇉ (⇉-→-f a⇉a⋯a b⇉b⋯b) =
    <:-→ (<:-reflNf⇉ a⇉a⋯a) (<:-reflNf⇉ b⇉b⋯b)
  <:-reflNf⇉ (⇉-s-i (∈-∙ x∈j j⇉as⇉k)) = <:-∙ x∈j (≃-reflSp⇉ j⇉as⇉k)

  <:⇇-reflNf⇉-⇑ : ∀ {n} {Γ : Ctx n} {a j k} →
                  Γ ⊢Nf a ⇉ j → Γ ⊢ j <∷ k → Γ ⊢ k kd → Γ ⊢ a <: a ⇇ k
  <:⇇-reflNf⇉-⇑ a⇉b₁⋯c₁ (<∷-⋯ b₂<:b₁ c₁<:c₂) _ =
    let a⇇b₂⋯c₂ = ⇇-⇑ a⇉b₁⋯c₁ (<∷-⋯ b₂<:b₁ c₁<:c₂)
    in <:-⇇ a⇇b₂⋯c₂ a⇇b₂⋯c₂ (<:-reflNf⇉ a⇉b₁⋯c₁)
  <:⇇-reflNf⇉-⇑ (⇉-Π-i j₁-kd a⇉k₁) (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd)
                (kd-Π j₂-kd k₂-kd) =
    let a<:a⇇k₂ = <:⇇-reflNf⇉-⇑ (⇓-Nf⇉ j₂-kd j₂<∷j₁ a⇉k₁) k₁<∷k₂ k₂-kd
        Λj₁a⇇Πj₂k₂ = ⇇-⇑ (⇉-Π-i j₁-kd a⇉k₁) (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd)
    in <:-λ a<:a⇇k₂ Λj₁a⇇Πj₂k₂ Λj₁a⇇Πj₂k₂

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

  -- Reflexivity of canonical spine equality.
  ≃-reflSp⇉ : ∀ {n} {Γ : Ctx n} {as j k} →
              Γ ⊢ j ⇉∙ as ⇉ k → Γ ⊢ j ⇉∙ as ≃ as ⇉ k
  ≃-reflSp⇉ ⇉-[]                     = ≃-[]
  ≃-reflSp⇉ (⇉-∷ a⇇j j-kd k[a]⇉as⇉l) =
    ≃-∷ (≃-reflNf⇇ a⇇j j-kd) (≃-reflSp⇉ k[a]⇉as⇉l)

  -- A checked variant of reflexivity.
  ≃-reflNf⇇ : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Nf a ⇇ k → Γ ⊢ k kd → Γ ⊢ a ≃ a ⇇ k
  ≃-reflNf⇇ a⇇k k-kd =
    <:-antisym k-kd (<:⇇-reflNf⇇ a⇇k k-kd) (<:⇇-reflNf⇇ a⇇k k-kd)

-- Reflexivity of canonical kind equality.
≅-refl : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ⊢ k ≅ k
≅-refl k-kd = <∷-antisym k-kd k-kd (<∷-refl k-kd) (<∷-refl k-kd)

-- A shorthand.
<:⇇-reflNf⇉ : ∀ {n} {Γ : Ctx n} {a k} →
              Γ ⊢Nf a ⇉ k → Γ ⊢ k kd → Γ ⊢ a <: a ⇇ k
<:⇇-reflNf⇉ a⇉k k-kd = <:⇇-reflNf⇉-⇑ a⇉k (<∷-refl k-kd) k-kd

-- Some corollaryies of reflexivity.

-- The synthesized kinds of normal forms kind-check.
Nf⇉⇒Nf⇇ : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Nf a ⇉ k → Γ ⊢Nf a ⇇ k
Nf⇉⇒Nf⇇ a⇉k = ⇇-⇑ a⇉k (<∷-refl (Nf⇉-valid a⇉k))

-- An admissible operator introduction rule accepting a checked body.
Nf⇇-Π-i : ∀ {n} {Γ : Ctx n} {j a k} →
          Γ ⊢ j kd → kd j ∷ Γ ⊢Nf a ⇇ k → Γ ⊢Nf Λ∙ j a ⇇ Π j k
Nf⇇-Π-i j-kd (⇇-⇑ a⇉l l<∷k) =
  ⇇-⇑ (⇉-Π-i j-kd a⇉l) (<∷-Π (<∷-refl j-kd) l<∷k (kd-Π j-kd (Nf⇉-valid a⇉l)))

-- Admissible projection rules for canonically kinded proper types.

<:-⟨|-Nf⇉ : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇉ b ⋯ c → Γ ⊢ b <: a
<:-⟨|-Nf⇉ a⇉b⋯c with Nf⇉-≡ a⇉b⋯c
<:-⟨|-Nf⇉ a⇉a⋯a | refl , refl = <:-reflNf⇉ a⇉a⋯a

<:-⟨|-Nf⇇ : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇇ b ⋯ c → Γ ⊢ b <: a
<:-⟨|-Nf⇇ (⇇-⇑ a⇉b₁⋯c₁ (<∷-⋯ b₂<:b₁ c₁<:c₂)) =
  <:-trans b₂<:b₁ (<:-⟨|-Nf⇉ a⇉b₁⋯c₁)

<:-|⟩-Nf⇉ : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇉ b ⋯ c → Γ ⊢ a <: c
<:-|⟩-Nf⇉ a⇉b⋯c with Nf⇉-≡ a⇉b⋯c
<:-|⟩-Nf⇉ a⇉a⋯a | refl , refl = <:-reflNf⇉ a⇉a⋯a

<:-|⟩-Nf⇇ : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇇ b ⋯ c → Γ ⊢ a <: c
<:-|⟩-Nf⇇ (⇇-⇑ a⇉b₁⋯c₁ (<∷-⋯ b₂<:b₁ c₁<:c₂)) =
  <:-trans (<:-|⟩-Nf⇉ a⇉b₁⋯c₁) c₁<:c₂

-- An admissible interval rule for checked subtyping.
<:⇇-⋯-i : ∀ {n} {Γ : Ctx n} {a b c d} →
          Γ ⊢ a <: b ⇇ c ⋯ d → Γ ⊢ a <: b ⇇ a ⋯ b
<:⇇-⋯-i (<:-⇇ a⇇c⋯d b⇇c⋯d a<:b) =
  let a⇉a⋯a = Nf⇇-s-i a⇇c⋯d
      b⇉b⋯b = Nf⇇-s-i b⇇c⋯d
  in <:-⇇ (⇇-⇑ a⇉a⋯a (<∷-⋯ (<:-reflNf⇉ a⇉a⋯a) a<:b))
          (⇇-⇑ b⇉b⋯b (<∷-⋯ a<:b (<:-reflNf⇉ b⇉b⋯b))) a<:b

-- An inversion lemma about variable kinding.
Var∈-inv : ∀ {n} {Γ : Ctx n} {x k} → Γ ⊢Var x ∈ k →
           ∃ λ j → lookup Γ x ≡ kd j × Γ ⊢ j <∷ k × Γ ⊢ j kd × Γ ⊢ k kd
Var∈-inv (⇉-var x Γ-ctx Γ[x]≡kd-j) =
  let j-kd = lookup-kd x Γ-ctx Γ[x]≡kd-j
  in _ , Γ[x]≡kd-j , <∷-refl j-kd , j-kd , j-kd
Var∈-inv (⇇-⇑ x∈j j<∷k k-kd) =
  let l , Γ[x]≡kd-l , l<∷j , l-kd , _ = Var∈-inv x∈j
  in l , Γ[x]≡kd-l , <∷-trans l<∷j j<∷k , l-kd , k-kd

-- A "canonical forms" lemma for operator equality.
≃-Π-can : ∀ {n} {Γ : Ctx n} {a₁ a₂ j k} → Γ ⊢ a₁ ≃ a₂ ⇇ Π j k →
          ∃ λ j₁ → ∃ λ b₁ → ∃ λ j₂ → ∃ λ b₂ →
            Γ ⊢Nf Λ∙ j₁ b₁ ⇇ Π j k × Γ ⊢Nf Λ∙ j₂ b₂ ⇇ Π j k × Γ ⊢ Π j k kd ×
              Γ ⊢ j <∷ j₁ × Γ ⊢ j <∷ j₂ ×
              kd j ∷ Γ ⊢ b₁ <: b₂ ⇇ k × kd j ∷ Γ ⊢ b₂ <: b₁ ⇇ k ×
              a₁ ≡ Λ∙ j₁ b₁ × a₂ ≡ Λ∙ j₂ b₂
≃-Π-can (<:-antisym Πjk-kd
          (<:-λ a₁<:a₂
            (⇇-⇑ (⇉-Π-i j₁-kd a₁⇉k₁) (<∷-Π j<∷j₁ k₁<∷k Πj₁k₁-kd))
            (⇇-⇑ (⇉-Π-i j₂-kd a₂⇉k₂) (<∷-Π j<∷j₂ k₂<∷k Πj₂k₂-kd)))
          (<:-λ a₂<:a₁ _ _)) =
  _ , _ , _ , _ ,
  (⇇-⇑ (⇉-Π-i j₁-kd a₁⇉k₁) (<∷-Π j<∷j₁ k₁<∷k Πj₁k₁-kd)) ,
  (⇇-⇑ (⇉-Π-i j₂-kd a₂⇉k₂) (<∷-Π j<∷j₂ k₂<∷k Πj₂k₂-kd)) ,
  Πjk-kd , j<∷j₁ , j<∷j₂ , a₁<:a₂ , a₂<:a₁ , refl , refl

------------------------------------------------------------------------
-- Simplification of well-formed kinding.

module _ where
  open SimpleKinding
  open SimpleKinding.Kinding
    renaming (_⊢Var_∈_ to _⊢sVar_∈_; _⊢Ne_∈_ to _⊢sNe_∈_)
  open KindedHereditarySubstitution
  open ≡-Reasoning

  -- Simplification of well-formedness and kinding: well-formed kinds
  -- resp. well-kinded normal forms, neutrals and spines are also
  -- simply well-formed resp. well-kinded.

  Var∈-sVar∈ : ∀ {n} {Γ : Ctx n} {a k} →
               Γ ⊢Var a ∈ k → ⌊ Γ ⌋Ctx ⊢sVar a ∈ ⌊ k ⌋
  Var∈-sVar∈ {_} {Γ} {_} {k} (⇉-var x Γ-ctx Γ[x]≡kd-k) = ∈-var x (begin
    SimpleCtx.lookup ⌊ Γ ⌋Ctx x   ≡⟨ ⌊⌋Asc-lookup Γ x ⟩
    ⌊ ElimCtx.lookup Γ x ⌋Asc     ≡⟨ cong ⌊_⌋Asc Γ[x]≡kd-k ⟩
    kd ⌊ k ⌋                      ∎)
    where open ContextConversions
  Var∈-sVar∈ (⇇-⇑ x∈j j<∷k k-kd) =
    subst (_ ⊢sVar _ ∈_) (<∷-⌊⌋ j<∷k) (Var∈-sVar∈ x∈j)

  mutual

    kd-kds : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → ⌊ Γ ⌋Ctx ⊢ k kds
    kd-kds (kd-⋯ a∈a⋯a b∈b⋯b) = kds-⋯ (Nf⇉-Nf∈ a∈a⋯a) (Nf⇉-Nf∈ b∈b⋯b)
    kd-kds (kd-Π j-kd k-kd)   = kds-Π (kd-kds j-kd) (kd-kds k-kd)

    Nf⇉-Nf∈ : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Nf a ⇉ k → ⌊ Γ ⌋Ctx ⊢Nf a ∈ ⌊ k ⌋
    Nf⇉-Nf∈ (⇉-⊥-f Γ-ctx)       = ∈-⊥-f
    Nf⇉-Nf∈ (⇉-⊤-f Γ-ctx)       = ∈-⊤-f
    Nf⇉-Nf∈ (⇉-∀-f k-kd a⇉a⋯a)  = ∈-∀-f (kd-kds k-kd) (Nf⇉-Nf∈ a⇉a⋯a)
    Nf⇉-Nf∈ (⇉-→-f a∈a⋯a b∈b⋯b) = ∈-→-f (Nf⇉-Nf∈ a∈a⋯a) (Nf⇉-Nf∈ b∈b⋯b)
    Nf⇉-Nf∈ (⇉-Π-i j-kd a⇉k)    = ∈-Π-i (kd-kds j-kd) (Nf⇉-Nf∈ a⇉k)
    Nf⇉-Nf∈ (⇉-s-i a∈b⋯c)       = ∈-ne (Ne∈-sNe∈ a∈b⋯c)

    Ne∈-sNe∈ : ∀ {n} {Γ : Ctx n} {a k} →
               Γ ⊢Ne a ∈ k → ⌊ Γ ⌋Ctx ⊢sNe a ∈ ⌊ k ⌋
    Ne∈-sNe∈ (∈-∙ x∈j j⇉as⇉k) = ∈-∙ (Var∈-sVar∈ x∈j) (Sp⇉-Sp∈ j⇉as⇉k)

    Sp⇉-Sp∈ : ∀ {n} {Γ : Ctx n} {as j k} → Γ ⊢ j ⇉∙ as ⇉ k →
              ⌊ Γ ⌋Ctx ⊢ ⌊ j ⌋ ∋∙ as ∈ ⌊ k ⌋
    Sp⇉-Sp∈ ⇉-[] = ∈-[]
    Sp⇉-Sp∈ (⇉-∷ a⇇j j-kd k[a]⇉as⇉l) =
      ∈-∷ (Nf⇇-Nf∈ a⇇j)
          (subst (_ ⊢_∋∙ _ ∈ _) (⌊⌋-Kind/⟨⟩ _) (Sp⇉-Sp∈ k[a]⇉as⇉l))

    Nf⇇-Nf∈ : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Nf a ⇇ k → ⌊ Γ ⌋Ctx ⊢Nf a ∈ ⌊ k ⌋
    Nf⇇-Nf∈ (⇇-⇑ a⇉j j<∷k) = subst (_ ⊢Nf _ ∈_) (<∷-⌊⌋ j<∷k) (Nf⇉-Nf∈ a⇉j)

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:
------------------------------------------------------------------------------
-- The the power function
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.Pow where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.UnaryNumbers

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

infixr 11 _^_

postulate
  _^_ : D → D → D
  ^-0 : ∀ n → n ^ zero      ≡ 1'
  ^-S : ∀ m n → m ^ succ₁ n ≡ m * m ^ n
{-# ATP axioms ^-0 ^-S #-}

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module List.Permutation.Base.Concatenation (A : Set) where

open import List.Permutation.Base A
open import List.Permutation.Base.Equivalence A
open import List.Permutation.Base.Preorder A
open import Data.List
open import Data.Product
open import Relation.Binary.PreorderReasoning ∼-preorder
open import Algebra
open import Algebra.Structures

lemma++/r : {x : A}{xs ys xs' : List A} → (xs / x ⟶ xs') → (xs ++ ys) / x ⟶ (xs' ++ ys)
lemma++/r /head = /head
lemma++/r (/tail xs/x⟶xs') = /tail (lemma++/r xs/x⟶xs')

lemma++/l : {y : A}{xs ys ys' : List A} → (ys / y ⟶ ys') → (xs ++ ys) / y ⟶ (xs ++ ys')
lemma++/l {xs = []} ys/y⟶ys' = ys/y⟶ys'
lemma++/l {xs = x ∷ xs} ys/y⟶ys' = /tail (lemma++/l {xs = xs} ys/y⟶ys')

lemma++/ : {y : A}{xs ys : List A} → (xs ++ y ∷ ys) / y ⟶ (xs ++ ys)
lemma++/ {xs = xs} = lemma++/l {xs = xs} /head

lemma++∼r : {xs xs' ys : List A} →  xs ∼ xs' → (xs ++ ys) ∼ (xs' ++ ys)
lemma++∼r {xs} {xs'} {[]} xs∼xs'
                   rewrite ((proj₂ (IsMonoid.identity (Monoid.isMonoid (monoid A)))) xs)
                            | ((proj₂ (IsMonoid.identity (Monoid.isMonoid (monoid A)))) xs') = xs∼xs'
lemma++∼r {xs} {xs'} {y ∷ ys} xs∼xs' =  ∼x (lemma++/ {y} {xs} {ys}) (lemma++/ {y} {xs'} {ys}) (lemma++∼r xs∼xs')

lemma++∼l : {xs ys ys' : List A} →  ys ∼  ys' → (xs ++ ys) ∼ (xs ++ ys')
lemma++∼l {xs = []} ys∼ys' = ys∼ys'
lemma++∼l {xs = x ∷ xs} ys∼ys' = ∼x /head /head (lemma++∼l {xs = xs} ys∼ys')

lemma++∼ : {xs ys xs' ys' : List A} →  xs ∼  xs' →  ys ∼ ys' → (xs ++ ys) ∼ (xs' ++ ys')
lemma++∼ {xs} {ys} {xs'} {ys'} xs∼xs' ys∼ys'
  = begin
     xs ++ ys
     ∼⟨ lemma++∼r xs∼xs'  ⟩
     xs' ++ ys
     ∼⟨ lemma++∼l {xs = xs'} ys∼ys'  ⟩
     xs' ++ ys'
    ∎

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

module 08-contractible-types where

import 07-equivalences
open 07-equivalences public

-- Section 6.1 Contractible types

is-contr :
  {i : Level} → UU i → UU i
is-contr A = Σ A (λ a → (x : A) → Id a x)

abstract
  center :
    {i : Level} {A : UU i} → is-contr A → A
  center (pair c is-contr-A) = c

  -- We make sure that the contraction is coherent in a straightforward way
  contraction :
    {i : Level} {A : UU i} (is-contr-A : is-contr A) →
    (const A A (center is-contr-A) ~ id)
  contraction (pair c C) x = (inv (C c)) ∙ (C x)

  coh-contraction :
    {i : Level} {A : UU i} (is-contr-A : is-contr A) →
    Id (contraction is-contr-A (center is-contr-A)) refl
  coh-contraction (pair c C) = left-inv (C c)

-- We show that contractible types satisfy an induction principle akin to the induction principle of the unit type: singleton induction. This can be helpful to give short proofs of many facts.

ev-pt :
  {i j : Level} (A : UU i) (a : A) (B : A → UU j) → ((x : A) → B x) → B a
ev-pt A a B f = f a

abstract
  sing-ind-is-contr :
    {i j : Level} (A : UU i) (is-contr-A : is-contr A) (B : A → UU j) →
    (a : A) → B a → (x : A) → B x
  sing-ind-is-contr A is-contr-A B a b x =
    tr B ((inv (contraction is-contr-A a)) ∙ (contraction is-contr-A x)) b

  sing-comp-is-contr :
    {i j : Level} (A : UU i) (is-contr-A : is-contr A) (B : A → UU j) (a : A) →
    ((ev-pt A a B) ∘ (sing-ind-is-contr A is-contr-A B a)) ~ id
  sing-comp-is-contr A is-contr-A B a b =
    ap (λ ω → tr B ω b) (left-inv (contraction is-contr-A a))

  sec-ev-pt-is-contr :
    {i j : Level} (A : UU i) (is-contr-A : is-contr A) (B : A → UU j) (a : A) →
    sec (ev-pt A a B)
  sec-ev-pt-is-contr A is-contr-A B a =
    pair
      ( sing-ind-is-contr A is-contr-A B a)
      ( sing-comp-is-contr A is-contr-A B a)

abstract
  is-sing-is-contr :
    {i j : Level} (A : UU i) (is-contr-A : is-contr A) (B : A → UU j) →
    ( a : A) → sec (ev-pt A a B)
  is-sing-is-contr A is-contr-A B a =
    pair
      ( sing-ind-is-contr A is-contr-A B a)
      ( sing-comp-is-contr A is-contr-A B a)

is-sing :
  {i : Level} (A : UU i) → A → UU (lsuc i)
is-sing {i} A a = (B : A → UU i) → sec (ev-pt A a B)

abstract
  is-contr-sing-ind :
    {i : Level} (A : UU i) (a : A) →
    ((P : A → UU i) → P a → (x : A) → P x) → is-contr A
  is-contr-sing-ind A a S = pair a (S (λ x → Id a x) refl)

abstract
  is-contr-is-sing :
    {i : Level} (A : UU i) (a : A) → is-sing A a → is-contr A
  is-contr-is-sing A a S = is-contr-sing-ind A a (λ P → pr1 (S P))

abstract
  is-sing-unit : is-sing unit star
  is-sing-unit B = pair ind-unit (λ b → refl)

is-contr-unit : is-contr unit
is-contr-unit = is-contr-is-sing unit star (is-sing-unit)

abstract
  is-sing-total-path :
    {i : Level} (A : UU i) (a : A) →
    is-sing (Σ A (λ x → Id a x)) (pair a refl)
  is-sing-total-path A a B = pair (ind-Σ ∘ (ind-Id a _)) (λ b → refl)

abstract
  is-contr-total-path :
    {i : Level} {A : UU i} (a : A) → is-contr (Σ A (λ x → Id a x))
  is-contr-total-path {A = A} a = is-contr-is-sing _ _ (is-sing-total-path A a)

-- Section 6.2 Contractible maps

-- We first introduce the notion of a fiber of a map.
fib :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) (b : B) → UU (i ⊔ j)
fib f b = Σ _ (λ x → Id (f x) b)

fib' :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) (b : B) → UU (i ⊔ j)
fib' f b = Σ _ (λ x → Id b (f x))

-- A map is said to be contractible if its fibers are contractible in the usual sense.
is-contr-map :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
is-contr-map f = (y : _) → is-contr (fib f y)

-- Our goal is to show that contractible maps are equivalences.
-- First we construct the inverse of a contractible map.
inv-is-contr-map :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  is-contr-map f → B → A
inv-is-contr-map is-contr-f y = pr1 (center (is-contr-f y))

-- Then we show that the inverse is a section.
issec-is-contr-map :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B}
  (is-contr-f : is-contr-map f) → (f ∘ (inv-is-contr-map is-contr-f)) ~ id
issec-is-contr-map is-contr-f y = pr2 (center (is-contr-f y))

-- Then we show that the inverse is also a retraction.
isretr-is-contr-map :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B}
  (is-contr-f : is-contr-map f) → ((inv-is-contr-map is-contr-f) ∘ f) ~ id
isretr-is-contr-map {_} {_} {A} {B} {f} is-contr-f x =
  ap ( pr1 {B = λ z → Id (f z) (f x)})
     ( ( inv
         ( contraction
           ( is-contr-f (f x))
           ( pair
             ( inv-is-contr-map is-contr-f (f x))
             ( issec-is-contr-map is-contr-f (f x))))) ∙
       ( contraction (is-contr-f (f x)) (pair x refl)))

-- Finally we put it all together to show that contractible maps are equivalences.

abstract
  is-equiv-is-contr-map :
    {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
    is-contr-map f → is-equiv f
  is-equiv-is-contr-map is-contr-f =
    is-equiv-has-inverse
      ( inv-is-contr-map is-contr-f)
      ( issec-is-contr-map is-contr-f)
      ( isretr-is-contr-map is-contr-f)

-- Section 6.3 Equivalences are contractible maps

-- The goal in this section is to show that all equivalences are contractible maps. This theorem is much harder than anything we've seen so far, but many future results will depend on it.

-- We characterize the identity types of fibers

Eq-fib :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) (y : B) →
  fib f y → fib f y → UU (i ⊔ j)
Eq-fib f y s t =
  Σ (Id (pr1 s) (pr1 t)) (λ α → Id ((ap f α) ∙ (pr2 t)) (pr2 s))

reflexive-Eq-fib :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) (y : B) →
  (s : fib f y) → Eq-fib f y s s
reflexive-Eq-fib f y s = pair refl refl

Eq-fib-eq :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) (y : B) →
  {s t : fib f y} → (Id s t) → Eq-fib f y s t
Eq-fib-eq f y {s} refl = reflexive-Eq-fib f y s

eq-Eq-fib :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) (y : B) →
  {s t : fib f y} → Eq-fib f y s t → Id s t
eq-Eq-fib f y {pair x p} {pair .x .p} (pair refl refl) = refl

issec-eq-Eq-fib :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) (y : B) →
  {s t : fib f y} → ((Eq-fib-eq f y {s} {t}) ∘ (eq-Eq-fib f y {s} {t})) ~ id
issec-eq-Eq-fib f y {pair x p} {pair .x .p} (pair refl refl) = refl

isretr-eq-Eq-fib :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) (y : B) →
  {s t : fib f y} → ((eq-Eq-fib f y {s} {t}) ∘ (Eq-fib-eq f y {s} {t})) ~ id
isretr-eq-Eq-fib f y {pair x p} {.(pair x p)} refl = refl

abstract
  is-equiv-Eq-fib-eq :
    {i j : Level} {A : UU i} {B : UU j} (f : A → B) (y : B) →
    {s t : fib f y} → is-equiv (Eq-fib-eq f y {s} {t})
  is-equiv-Eq-fib-eq f y {s} {t} =
    is-equiv-has-inverse
      ( eq-Eq-fib f y)
      ( issec-eq-Eq-fib f y)
      ( isretr-eq-Eq-fib f y)

abstract
  is-equiv-eq-Eq-fib :
    {i j : Level} {A : UU i} {B : UU j} (f : A → B) (y : B) →
    {s t : fib f y} → is-equiv (eq-Eq-fib f y {s} {t})
  is-equiv-eq-Eq-fib f y {s} {t} =
    is-equiv-has-inverse
      ( Eq-fib-eq f y)
      ( isretr-eq-Eq-fib f y)
      ( issec-eq-Eq-fib f y)

-- Next, we improve the homotopy G : f ∘ g ~ id if f comes equipped with the
-- structure has-inverse f.

inv-has-inverse :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  has-inverse f → B → A
inv-has-inverse inv-f = pr1 inv-f

issec-inv-has-inverse :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  (inv-f : has-inverse f) → (f ∘ (inv-has-inverse inv-f)) ~ id
issec-inv-has-inverse {f = f} (pair g (pair G H)) y =
  (inv (G (f (g y)))) ∙ (ap f (H (g y)) ∙ (G y))

isretr-inv-has-inverse :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  (inv-f : has-inverse f) → ((inv-has-inverse inv-f) ∘ f) ~ id
isretr-inv-has-inverse inv-f = pr2 (pr2 inv-f)

-- Before we start we will develop some of the ingredients of the construction.

-- We will need the naturality of homotopies.
htpy-nat :
  {i j : Level} {A : UU i} {B : UU j} {f g : A → B} (H : f ~ g)
  {x y : A} (p : Id x y) →
  Id ((H x) ∙ (ap g p)) ((ap f p) ∙ (H y))
htpy-nat H refl = right-unit

-- We will also need to undo concatenation on the left and right. One might notice that, in the terminology of Lecture 9, we almost show here that concat p and concat' q are embeddings.
left-unwhisk :
  {i : Level} {A : UU i} {x y z : A} (p : Id x y) {q r : Id y z} →
  Id (p ∙ q) (p ∙ r) → Id q r
left-unwhisk refl s = (inv left-unit) ∙ (s ∙ left-unit)

right-unwhisk :
  {i : Level} {A : UU i} {x y z : A} {p q : Id x y}
  (r : Id y z) → Id (p ∙ r) (q ∙ r) → Id p q
right-unwhisk refl s = (inv right-unit) ∙ (s ∙ right-unit)

-- We will also need to compute with homotopies to the identity function.
htpy-red :
  {i : Level} {A : UU i} {f : A → A} (H : f ~ id) →
  (x : A) → Id (H (f x)) (ap f (H x))
htpy-red {_} {A} {f} H x =
  right-unwhisk (H x)
    ( ( ap (concat (H (f x)) x) (inv (ap-id (H x)))) ∙
      ( htpy-nat H (H x)))

square :
  {i : Level} {A : UU i} {x y1 y2 z : A}
  (p1 : Id x y1) (q1 : Id y1 z) (p2 : Id x y2) (q2 : Id y2 z) → UU i
square p q p' q' = Id (p ∙ q) (p' ∙ q')

sq-left-whisk :
  {i : Level} {A : UU i} {x y1 y2 z : A} {p1 p1' : Id x y1}
  (s : Id p1 p1') {q1 : Id y1 z} {p2 : Id x y2} {q2 : Id y2 z} →
  square p1 q1 p2 q2 → square p1' q1 p2 q2
sq-left-whisk refl sq = sq

sq-top-whisk :
  {i : Level} {A : UU i} {x y1 y2 z : A}
  (p1 : Id x y1) (q1 : Id y1 z)
  (p2 : Id x y2) {p2' : Id x y2} (s : Id p2 p2') (q2 : Id y2 z) →
  square p1 q1 p2 q2 → square p1 q1 p2' q2
sq-top-whisk p1 q1 p2 refl q2 sq = sq

coherence-inv-has-inverse :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  (inv-f : has-inverse f) →
  (f ·l (isretr-inv-has-inverse inv-f)) ~ ((issec-inv-has-inverse inv-f) ·r f)
coherence-inv-has-inverse {f = f} (pair g (pair G H)) x =
  inv-con
    ( G (f (g (f x))))
    ( ap f (H x))
    ( (ap f (H (g (f x)))) ∙ (G (f x)))
    ( sq-top-whisk
      ( G (f (g (f x))))
      ( ap f (H x))
      ( (ap (f ∘ (g ∘ f)) (H x)))
      ( (ap-comp f (g ∘ f) (H x)) ∙ (inv (ap (ap f) (htpy-red H x))))
      ( G (f x))
      ( htpy-nat (htpy-right-whisk G f) (H x)))

-- Now the proof that equivalences are contractible maps really begins. Note that we have already shown that any equivalence has an inverse. Our strategy is therefore to first show that maps with inverses are contractible, and then deduce the claim about equivalences.

abstract
  center-has-inverse :
    {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
    has-inverse f → (y : B) → fib f y
  center-has-inverse {i} {j} {A} {B} {f} inv-f y =
    pair
      ( inv-has-inverse inv-f y)
      ( issec-inv-has-inverse inv-f y)

  contraction-has-inverse :
    {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
    (I : has-inverse f) → (y : B) → (t : fib f y) →
    Id (center-has-inverse I y) t
  contraction-has-inverse {i} {j} {A} {B} {f}
    ( pair g (pair G H)) y (pair x refl) =
    eq-Eq-fib f y (pair
      ( H x)
      ( ( right-unit) ∙
        ( coherence-inv-has-inverse (pair g (pair G H)) x)))

  is-contr-map-has-inverse : {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
    has-inverse f → is-contr-map f
  is-contr-map-has-inverse inv-f y =
    pair
      ( center-has-inverse inv-f y)
      ( contraction-has-inverse inv-f y)

  is-contr-map-is-equiv : {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
    is-equiv f → is-contr-map f
  is-contr-map-is-equiv = is-contr-map-has-inverse ∘ has-inverse-is-equiv

abstract
  is-contr-total-path' :
    {i : Level} {A : UU i} (a : A) → is-contr (Σ A (λ x → Id x a))
  is-contr-total-path' a = is-contr-map-is-equiv (is-equiv-id _) a

-- Exercises

-- Exercise 6.1

-- In this exercise we are asked to show that the identity types of a contractible type are again contractible. In the terminology of Lecture 8: we are showing that contractible types are propositions.

abstract
  is-prop-is-contr : {i : Level} {A : UU i} → is-contr A →
    (x y : A) → is-contr (Id x y)
  is-prop-is-contr {i} {A} is-contr-A =
    sing-ind-is-contr A is-contr-A
      ( λ x → ((y : A) → is-contr (Id x y)))
      ( center is-contr-A)
      ( λ y → pair
        ( contraction is-contr-A y)
        ( ind-Id
          ( center is-contr-A)
          ( λ z (p : Id (center is-contr-A) z) →
            Id (contraction is-contr-A z) p)
          ( coh-contraction is-contr-A)
          ( y)))

abstract
  is-prop-is-contr' : {i : Level} {A : UU i} → is-contr A →
    (x y : A) → Id x y
  is-prop-is-contr' is-contr-A x y =
    center (is-prop-is-contr is-contr-A x y)

-- Exercise 6.2

-- In this exercise we are showing that contractible types are closed under retracts.

abstract
  is-contr-retract-of : {i j : Level} {A : UU i} (B : UU j) →
    A retract-of B → is-contr B → is-contr A
  is-contr-retract-of B (pair i (pair r isretr)) is-contr-B =
    pair
      ( r (center is-contr-B))
      ( λ x → (ap r (contraction is-contr-B (i x))) ∙ (isretr x))

-- Exercise 6.3

-- In this exercise we are showing that a type is contractible if and only if the constant map to the unit type is an equivalence. This can be used to derive a '3-for-2 property' for contractible types, which may come in handy sometimes.

abstract
  is-equiv-const-is-contr :
    {i : Level} {A : UU i} → is-contr A → is-equiv (const A unit star)
  is-equiv-const-is-contr {i} {A} is-contr-A =
    pair
      ( pair (ind-unit (center is-contr-A)) (ind-unit refl))
      ( pair (const unit A (center is-contr-A)) (contraction is-contr-A))

abstract
  is-contr-is-equiv-const :
    {i : Level} {A : UU i} → is-equiv (const A unit star) → is-contr A
  is-contr-is-equiv-const (pair (pair g issec) (pair h isretr)) =
    pair (h star) isretr

abstract
  is-contr-is-equiv :
    {i j : Level} {A : UU i} (B : UU j) (f : A → B) →
    is-equiv f → is-contr B → is-contr A
  is-contr-is-equiv B f is-equiv-f is-contr-B =
    is-contr-is-equiv-const
      ( is-equiv-comp'
        ( const B unit star)
        ( f)
        ( is-equiv-f)
        ( is-equiv-const-is-contr is-contr-B))

abstract
  is-contr-equiv :
    {i j : Level} {A : UU i} (B : UU j) (e : A ≃ B) → is-contr B → is-contr A
  is-contr-equiv B (pair e is-equiv-e) is-contr-B =
    is-contr-is-equiv B e is-equiv-e is-contr-B

abstract
  is-contr-is-equiv' :
    {i j : Level} (A : UU i) {B : UU j} (f : A → B) →
    is-equiv f → is-contr A → is-contr B
  is-contr-is-equiv' A f is-equiv-f is-contr-A =
    is-contr-is-equiv A
      ( inv-is-equiv is-equiv-f)
      ( is-equiv-inv-is-equiv is-equiv-f)
      ( is-contr-A)

abstract
  is-contr-equiv' :
    {i j : Level} (A : UU i) {B : UU j} (e : A ≃ B) → is-contr A → is-contr B
  is-contr-equiv' A (pair e is-equiv-e) is-contr-A =
    is-contr-is-equiv' A e is-equiv-e is-contr-A

abstract
  is-equiv-is-contr :
    {i j : Level} {A : UU i} {B : UU j} (f : A → B) →
    is-contr A → is-contr B → is-equiv f
  is-equiv-is-contr {i} {j} {A} {B} f is-contr-A is-contr-B =
    is-equiv-has-inverse
      ( const B A (center is-contr-A))
      ( sing-ind-is-contr B is-contr-B _ _
        ( inv (contraction is-contr-B (f (center is-contr-A)))))
      ( contraction is-contr-A)

equiv-is-contr :
  {i j : Level} {A : UU i} {B : UU j} →
  is-contr A → is-contr B → A ≃ B
equiv-is-contr is-contr-A is-contr-B =
  pair
    ( λ a → center is-contr-B)
    ( is-equiv-is-contr _ is-contr-A is-contr-B)

-- Exercise 6.4

-- In this exercise we will show that if the base type in a Σ-type is contractible, then the Σ-type is equivalent to the fiber at the center of contraction. This can be seen as a left unit law for Σ-types. We will derive a right unit law for Σ-types in Lecture 7 (not because it is unduable here, but it is useful to have some knowledge of fiberwise equivalences).

left-unit-law-Σ-map :
  {i j : Level} {C : UU i} (B : C → UU j)
  (is-contr-C : is-contr C) → B (center is-contr-C) → Σ C B
left-unit-law-Σ-map B is-contr-C y = pair (center is-contr-C) y

left-unit-law-Σ-map-conv :
  {i j : Level} {C : UU i} (B : C → UU j)
  (is-contr-C : is-contr C) → Σ C B → B (center is-contr-C)
left-unit-law-Σ-map-conv B is-contr-C =
  ind-Σ
    ( sing-ind-is-contr _ is-contr-C
      ( λ x → B x → B (center is-contr-C))
      ( center is-contr-C)
      ( id))

left-inverse-left-unit-law-Σ-map-conv :
  {i j : Level} {C : UU i} (B : C → UU j) (is-contr-C : is-contr C) →
  ( ( left-unit-law-Σ-map-conv B is-contr-C) ∘
    ( left-unit-law-Σ-map B is-contr-C)) ~ id
left-inverse-left-unit-law-Σ-map-conv B is-contr-C y =
  ap
    ( λ (f : B (center is-contr-C) → B (center is-contr-C)) → f y)
    ( sing-comp-is-contr _ is-contr-C
      ( λ x → B x → B (center is-contr-C))
      ( center is-contr-C)
      ( id))

right-inverse-left-unit-law-Σ-map-conv :
  {i j : Level} {C : UU i} (B : C → UU j) (is-contr-C : is-contr C) →
  ( ( left-unit-law-Σ-map B is-contr-C) ∘
    ( left-unit-law-Σ-map-conv B is-contr-C)) ~ id
right-inverse-left-unit-law-Σ-map-conv B is-contr-C =
  ind-Σ
    ( sing-ind-is-contr _ is-contr-C
      ( λ x → (y : B x) →
        Id ( ( ( left-unit-law-Σ-map B is-contr-C) ∘
               ( left-unit-law-Σ-map-conv B is-contr-C))
             ( pair x y))
           ( id (pair x y))) (center is-contr-C)
      ( λ y → ap
        ( left-unit-law-Σ-map B is-contr-C)
        ( ap
          ( λ f → f y)
          ( sing-comp-is-contr _ is-contr-C
            ( λ x → B x → B (center is-contr-C)) (center is-contr-C) id))))

abstract
  is-equiv-left-unit-law-Σ-map :
    {i j : Level} {C : UU i} (B : C → UU j) (is-contr-C : is-contr C) →
    is-equiv (left-unit-law-Σ-map B is-contr-C)
  is-equiv-left-unit-law-Σ-map B is-contr-C =
    is-equiv-has-inverse
      ( left-unit-law-Σ-map-conv B is-contr-C)
      ( right-inverse-left-unit-law-Σ-map-conv B is-contr-C)
      ( left-inverse-left-unit-law-Σ-map-conv B is-contr-C)

abstract
  is-equiv-left-unit-law-Σ-map-conv :
    {i j : Level} {C : UU i} (B : C → UU j) (is-contr-C : is-contr C) →
    is-equiv (left-unit-law-Σ-map-conv B is-contr-C)
  is-equiv-left-unit-law-Σ-map-conv B is-contr-C =
    is-equiv-has-inverse
      ( left-unit-law-Σ-map B is-contr-C)
      ( left-inverse-left-unit-law-Σ-map-conv B is-contr-C)
      ( right-inverse-left-unit-law-Σ-map-conv B is-contr-C)

left-unit-law-Σ : {i j : Level} {C : UU i} (B : C → UU j)
  (is-contr-C : is-contr C) → B (center is-contr-C) ≃ Σ C B
left-unit-law-Σ B is-contr-C =
  pair
    ( left-unit-law-Σ-map B is-contr-C)
    ( is-equiv-left-unit-law-Σ-map B is-contr-C)

left-unit-law-Σ-map-gen :
  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) →
  is-contr A → (x : A) → B x → Σ A B
left-unit-law-Σ-map-gen B is-contr-A x y = pair x y

abstract
  is-equiv-left-unit-law-Σ-map-gen :
    {l1 l2 : Level} {A : UU l1} (B : A → UU l2) →
    (is-contr-A : is-contr A) →
    (x : A) → is-equiv (left-unit-law-Σ-map-gen B is-contr-A x)
  is-equiv-left-unit-law-Σ-map-gen B is-contr-A x =
    is-equiv-comp
      ( left-unit-law-Σ-map-gen B is-contr-A x)
      ( left-unit-law-Σ-map B is-contr-A)
      ( tr B (inv (contraction is-contr-A x)))
      ( λ y → eq-pair (inv (contraction is-contr-A x)) refl)
      ( is-equiv-tr B (inv (contraction is-contr-A x)))
      ( is-equiv-left-unit-law-Σ-map B is-contr-A)

left-unit-law-Σ-gen :
  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) →
  (is-contr-A : is-contr A) →
  (x : A) → B x ≃ Σ A B
left-unit-law-Σ-gen B is-contr-A x =
  pair
    ( left-unit-law-Σ-map-gen B is-contr-A x)
    ( is-equiv-left-unit-law-Σ-map-gen B is-contr-A x)

-- Exercise 6.6

-- In this exercise we show that the domain of a map is equivalent to the total space of its fibers.

Σ-fib-to-domain :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B ) → (Σ B (fib f)) → A
Σ-fib-to-domain f t = pr1 (pr2 t)

triangle-Σ-fib-to-domain :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B ) →
  pr1 ~ (f ∘ (Σ-fib-to-domain f))
triangle-Σ-fib-to-domain f t = inv (pr2 (pr2 t))

domain-to-Σ-fib :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) → A → Σ B (fib f)
domain-to-Σ-fib f x = pair (f x) (pair x refl)

left-inverse-domain-to-Σ-fib :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B ) →
  ((domain-to-Σ-fib f) ∘ (Σ-fib-to-domain f)) ~ id
left-inverse-domain-to-Σ-fib f (pair .(f x) (pair x refl)) = refl

right-inverse-domain-to-Σ-fib :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B ) →
  ((Σ-fib-to-domain f) ∘ (domain-to-Σ-fib f)) ~ id
right-inverse-domain-to-Σ-fib f x = refl

abstract
  is-equiv-Σ-fib-to-domain :
    {i j : Level} {A : UU i} {B : UU j} (f : A → B ) →
    is-equiv (Σ-fib-to-domain f)
  is-equiv-Σ-fib-to-domain f =
    is-equiv-has-inverse
      ( domain-to-Σ-fib f)
      ( right-inverse-domain-to-Σ-fib f)
      ( left-inverse-domain-to-Σ-fib f)

equiv-Σ-fib-to-domain :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B ) → Σ B (fib f) ≃ A
equiv-Σ-fib-to-domain f =
  pair (Σ-fib-to-domain f) (is-equiv-Σ-fib-to-domain f)

-- Exercise 6.7

-- In this exercise we show that if a cartesian product is contractible, then so are its factors. We make use of the fact that contractible types are closed under retracts, just because that is a useful property to practice with. Other proofs are possible too.

abstract
  is-contr-left-factor-prod :
    {i j : Level} (A : UU i) (B : UU j) → is-contr (A × B) → is-contr A
  is-contr-left-factor-prod A B is-contr-AB =
    is-contr-retract-of
      ( A × B)
      ( pair
        ( λ x → pair x (pr2 (center is-contr-AB)))
        ( pair pr1 (λ x → refl)))
      ( is-contr-AB)

abstract
  is-contr-right-factor-prod :
    {i j : Level} (A : UU i) (B : UU j) → is-contr (A × B) → is-contr B
  is-contr-right-factor-prod A B is-contr-AB =
    is-contr-left-factor-prod B A
      ( is-contr-equiv
        ( A × B)
        ( equiv-swap-prod B A)
        ( is-contr-AB))

abstract
  is-contr-prod :
    {i j : Level} {A : UU i} {B : UU j} →
    is-contr A → is-contr B → is-contr (A × B)
  is-contr-prod {A = A} {B = B} is-contr-A is-contr-B =
    is-contr-equiv' B
      ( left-unit-law-Σ (λ x → B) is-contr-A)
      ( is-contr-B)

-- Exercise 6.8

-- Given any family B over A, there is a map from the fiber of the projection map (pr1 : Σ A B → A) to the type (B a), i.e. the fiber of B at a. In this exercise we define this map, and show that it is an equivalence, for every a : A.

fib-fam-fib-pr1 :
  {i j : Level} {A : UU i} (B : A → UU j)
  (a : A) → fib (pr1 {B = B}) a → B a
fib-fam-fib-pr1 B a (pair (pair x y) p) = tr B p y

fib-pr1-fib-fam :
  {i j : Level} {A : UU i} (B : A → UU j)
  (a : A) → B a → fib (pr1 {B = B}) a
fib-pr1-fib-fam B a b = pair (pair a b) refl

left-inverse-fib-pr1-fib-fam :
  {i j : Level} {A : UU i} (B : A → UU j) (a : A) →
  ((fib-pr1-fib-fam B a) ∘ (fib-fam-fib-pr1 B a)) ~ id
left-inverse-fib-pr1-fib-fam B a (pair (pair .a y) refl) = refl

right-inverse-fib-pr1-fib-fam :
  {i j : Level} {A : UU i} (B : A → UU j) (a : A) →
  ((fib-fam-fib-pr1 B a) ∘ (fib-pr1-fib-fam B a)) ~ id
right-inverse-fib-pr1-fib-fam B a b = refl

abstract
  is-equiv-fib-fam-fib-pr1 :
    {i j : Level} {A : UU i} (B : A → UU j) (a : A) →
    is-equiv (fib-fam-fib-pr1 B a)
  is-equiv-fib-fam-fib-pr1 B a =
    is-equiv-has-inverse
      ( fib-pr1-fib-fam B a)
      ( right-inverse-fib-pr1-fib-fam B a)
      ( left-inverse-fib-pr1-fib-fam B a)

equiv-fib-fam-fib-pr1 :
  {i j : Level} {A : UU i} (B : A → UU j) (a : A) →
  fib (pr1 {B = B}) a ≃ B a
equiv-fib-fam-fib-pr1 B a =
  pair (fib-fam-fib-pr1 B a) (is-equiv-fib-fam-fib-pr1 B a)

abstract
  is-equiv-fib-pr1-fib-fam :
    {i j : Level} {A : UU i} (B : A → UU j) (a : A) →
    is-equiv (fib-pr1-fib-fam B a)
  is-equiv-fib-pr1-fib-fam B a =
    is-equiv-has-inverse
      ( fib-fam-fib-pr1 B a)
      ( left-inverse-fib-pr1-fib-fam B a)
      ( right-inverse-fib-pr1-fib-fam B a)

equiv-fib-pr1-fib-fam :
  {i j : Level} {A : UU i} (B : A → UU j) (a : A) →
  B a ≃ fib (pr1 {B = B}) a
equiv-fib-pr1-fib-fam B a =
  pair (fib-pr1-fib-fam B a) (is-equiv-fib-pr1-fib-fam B a)

abstract
  is-equiv-pr1-is-contr :
    {i j : Level} {A : UU i} (B : A → UU j) →
    ((a : A) → is-contr (B a)) → is-equiv (pr1 {B = B})
  is-equiv-pr1-is-contr B is-contr-B =
    is-equiv-is-contr-map
      ( λ x → is-contr-equiv
        ( B x)
        ( equiv-fib-fam-fib-pr1 B x)
        ( is-contr-B x))

equiv-pr1 :
  {i j : Level} {A : UU i} {B : A → UU j} →
  ((a : A) → is-contr (B a)) → (Σ A B) ≃ A
equiv-pr1 is-contr-B = pair pr1 (is-equiv-pr1-is-contr _ is-contr-B)

abstract
  is-contr-is-equiv-pr1 :
    {i j : Level} {A : UU i} (B : A → UU j) →
    (is-equiv (pr1 {B = B})) → ((a : A) → is-contr (B a))
  is-contr-is-equiv-pr1 B is-equiv-pr1-B a =
    is-contr-equiv'
      ( fib pr1 a)
      ( equiv-fib-fam-fib-pr1 B a)
      ( is-contr-map-is-equiv is-equiv-pr1-B a)

right-unit-law-Σ :
  {i j : Level} {A : UU i} (B : A → UU j) →
  ((a : A) → is-contr (B a)) → (Σ A B) ≃ A
right-unit-law-Σ B is-contr-B =
  pair pr1 (is-equiv-pr1-is-contr B is-contr-B)

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A bunch of properties about natural number operations
------------------------------------------------------------------------

-- See README.Nat for some examples showing how this module can be
-- used.

module Data.Nat.Properties where

open import Data.Nat as Nat
open ≤-Reasoning
  renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≡⟨_⟩'_)
open import Relation.Binary
open DecTotalOrder Nat.decTotalOrder using () renaming (refl to ≤-refl)
open import Function
open import Algebra
open import Algebra.Structures
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym; cong; cong₂)
open PropEq.≡-Reasoning
import Algebra.FunctionProperties as P; open P (_≡_ {A = ℕ})
open import Data.Product
open import Data.Sum

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

-- basic lemmas about (ℕ, +, *, 0, 1):
open import Data.Nat.Properties.Simple

-- (ℕ, +, *, 0, 1) is a commutative semiring
isCommutativeSemiring : IsCommutativeSemiring _≡_ _+_ _*_ 0 1
isCommutativeSemiring = record
  { +-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = PropEq.isEquivalence
      ; assoc         = +-assoc
      ; ∙-cong        = cong₂ _+_
      }
    ; identityˡ = λ _ → refl
    ; comm      = +-comm
    }
  ; *-isCommutativeMonoid = record
    { isSemigroup = record
      { isEquivalence = PropEq.isEquivalence
      ; assoc         = *-assoc
      ; ∙-cong        = cong₂ _*_
      }
    ; identityˡ = +-right-identity
    ; comm      = *-comm
    }
  ; distribʳ = distribʳ-*-+
  ; zeroˡ    = λ _ → refl
  }

commutativeSemiring : CommutativeSemiring _ _
commutativeSemiring = record
  { _+_                   = _+_
  ; _*_                   = _*_
  ; 0#                    = 0
  ; 1#                    = 1
  ; isCommutativeSemiring = isCommutativeSemiring
  }

import Algebra.RingSolver.Simple as Solver
import Algebra.RingSolver.AlmostCommutativeRing as ACR
module SemiringSolver =
  Solver (ACR.fromCommutativeSemiring commutativeSemiring) _≟_

------------------------------------------------------------------------
-- (ℕ, ⊔, ⊓, 0) is a commutative semiring without one

private

  ⊔-assoc : Associative _⊔_
  ⊔-assoc zero    _       _       = refl
  ⊔-assoc (suc m) zero    o       = refl
  ⊔-assoc (suc m) (suc n) zero    = refl
  ⊔-assoc (suc m) (suc n) (suc o) = cong suc $ ⊔-assoc m n o

  ⊔-identity : Identity 0 _⊔_
  ⊔-identity = (λ _ → refl) , n⊔0≡n
    where
    n⊔0≡n : RightIdentity 0 _⊔_
    n⊔0≡n zero    = refl
    n⊔0≡n (suc n) = refl

  ⊔-comm : Commutative _⊔_
  ⊔-comm zero    n       = sym $ proj₂ ⊔-identity n
  ⊔-comm (suc m) zero    = refl
  ⊔-comm (suc m) (suc n) =
    begin
      suc m ⊔ suc n
    ≡⟨ refl ⟩
      suc (m ⊔ n)
    ≡⟨ cong suc (⊔-comm m n) ⟩
      suc (n ⊔ m)
    ≡⟨ refl ⟩
      suc n ⊔ suc m
    ∎

  ⊓-assoc : Associative _⊓_
  ⊓-assoc zero    _       _       = refl
  ⊓-assoc (suc m) zero    o       = refl
  ⊓-assoc (suc m) (suc n) zero    = refl
  ⊓-assoc (suc m) (suc n) (suc o) = cong suc $ ⊓-assoc m n o

  ⊓-zero : Zero 0 _⊓_
  ⊓-zero = (λ _ → refl) , n⊓0≡0
    where
    n⊓0≡0 : RightZero 0 _⊓_
    n⊓0≡0 zero    = refl
    n⊓0≡0 (suc n) = refl

  ⊓-comm : Commutative _⊓_
  ⊓-comm zero    n       = sym $ proj₂ ⊓-zero n
  ⊓-comm (suc m) zero    = refl
  ⊓-comm (suc m) (suc n) =
    begin
      suc m ⊓ suc n
    ≡⟨ refl ⟩
      suc (m ⊓ n)
    ≡⟨ cong suc (⊓-comm m n) ⟩
      suc (n ⊓ m)
    ≡⟨ refl ⟩
      suc n ⊓ suc m
    ∎

  distrib-⊓-⊔ : _⊓_ DistributesOver _⊔_
  distrib-⊓-⊔ = (distribˡ-⊓-⊔ , distribʳ-⊓-⊔)
    where
    distribʳ-⊓-⊔ : _⊓_ DistributesOverʳ _⊔_
    distribʳ-⊓-⊔ (suc m) (suc n) (suc o) = cong suc $ distribʳ-⊓-⊔ m n o
    distribʳ-⊓-⊔ (suc m) (suc n) zero    = cong suc $ refl
    distribʳ-⊓-⊔ (suc m) zero    o       = refl
    distribʳ-⊓-⊔ zero    n       o       = begin
      (n ⊔ o) ⊓ 0    ≡⟨ ⊓-comm (n ⊔ o) 0 ⟩
      0 ⊓ (n ⊔ o)    ≡⟨ refl ⟩
      0 ⊓ n ⊔ 0 ⊓ o  ≡⟨ ⊓-comm 0 n ⟨ cong₂ _⊔_ ⟩ ⊓-comm 0 o ⟩
      n ⊓ 0 ⊔ o ⊓ 0  ∎

    distribˡ-⊓-⊔ : _⊓_ DistributesOverˡ _⊔_
    distribˡ-⊓-⊔ m n o = begin
      m ⊓ (n ⊔ o)    ≡⟨ ⊓-comm m _ ⟩
      (n ⊔ o) ⊓ m    ≡⟨ distribʳ-⊓-⊔ m n o ⟩
      n ⊓ m ⊔ o ⊓ m  ≡⟨ ⊓-comm n m ⟨ cong₂ _⊔_ ⟩ ⊓-comm o m ⟩
      m ⊓ n ⊔ m ⊓ o  ∎

⊔-⊓-0-isCommutativeSemiringWithoutOne
  : IsCommutativeSemiringWithoutOne _≡_ _⊔_ _⊓_ 0
⊔-⊓-0-isCommutativeSemiringWithoutOne = record
  { isSemiringWithoutOne = record
    { +-isCommutativeMonoid = record
      { isSemigroup = record
        { isEquivalence = PropEq.isEquivalence
        ; assoc         = ⊔-assoc
        ; ∙-cong        = cong₂ _⊔_
        }
      ; identityˡ = proj₁ ⊔-identity
      ; comm      = ⊔-comm
      }
    ; *-isSemigroup = record
      { isEquivalence = PropEq.isEquivalence
      ; assoc         = ⊓-assoc
      ; ∙-cong        = cong₂ _⊓_
      }
    ; distrib = distrib-⊓-⊔
    ; zero    = ⊓-zero
    }
  ; *-comm = ⊓-comm
  }

⊔-⊓-0-commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _ _
⊔-⊓-0-commutativeSemiringWithoutOne = record
  { _+_                             = _⊔_
  ; _*_                             = _⊓_
  ; 0#                              = 0
  ; isCommutativeSemiringWithoutOne =
      ⊔-⊓-0-isCommutativeSemiringWithoutOne
  }

------------------------------------------------------------------------
-- (ℕ, ⊓, ⊔) is a lattice

private

  absorptive-⊓-⊔ : Absorptive _⊓_ _⊔_
  absorptive-⊓-⊔ = abs-⊓-⊔ , abs-⊔-⊓
    where
    abs-⊔-⊓ : _⊔_ Absorbs _⊓_
    abs-⊔-⊓ zero    n       = refl
    abs-⊔-⊓ (suc m) zero    = refl
    abs-⊔-⊓ (suc m) (suc n) = cong suc $ abs-⊔-⊓ m n

    abs-⊓-⊔ : _⊓_ Absorbs _⊔_
    abs-⊓-⊔ zero    n       = refl
    abs-⊓-⊔ (suc m) (suc n) = cong suc $ abs-⊓-⊔ m n
    abs-⊓-⊔ (suc m) zero    = cong suc $
                   begin
      m ⊓ m
                   ≡⟨ cong (_⊓_ m) $ sym $ proj₂ ⊔-identity m ⟩
      m ⊓ (m ⊔ 0)
                   ≡⟨ abs-⊓-⊔ m zero ⟩
      m
                   ∎

isDistributiveLattice : IsDistributiveLattice _≡_ _⊓_ _⊔_
isDistributiveLattice = record
  { isLattice = record
      { isEquivalence = PropEq.isEquivalence
      ; ∨-comm        = ⊓-comm
      ; ∨-assoc       = ⊓-assoc
      ; ∨-cong        = cong₂ _⊓_
      ; ∧-comm        = ⊔-comm
      ; ∧-assoc       = ⊔-assoc
      ; ∧-cong        = cong₂ _⊔_
      ; absorptive    = absorptive-⊓-⊔
      }
  ; ∨-∧-distribʳ = proj₂ distrib-⊓-⊔
  }

distributiveLattice : DistributiveLattice _ _
distributiveLattice = record
  { _∨_                   = _⊓_
  ; _∧_                   = _⊔_
  ; isDistributiveLattice = isDistributiveLattice
  }

------------------------------------------------------------------------
-- Converting between ≤ and ≤′

≤-step : ∀ {m n} → m ≤ n → m ≤ 1 + n
≤-step z≤n       = z≤n
≤-step (s≤s m≤n) = s≤s (≤-step m≤n)

≤′⇒≤ : _≤′_ ⇒ _≤_
≤′⇒≤ ≤′-refl        = ≤-refl
≤′⇒≤ (≤′-step m≤′n) = ≤-step (≤′⇒≤ m≤′n)

z≤′n : ∀ {n} → zero ≤′ n
z≤′n {zero}  = ≤′-refl
z≤′n {suc n} = ≤′-step z≤′n

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

≤⇒≤′ : _≤_ ⇒ _≤′_
≤⇒≤′ z≤n       = z≤′n
≤⇒≤′ (s≤s m≤n) = s≤′s (≤⇒≤′ m≤n)

------------------------------------------------------------------------
-- Various order-related properties

≤-steps : ∀ {m n} k → m ≤ n → m ≤ k + n
≤-steps zero    m≤n = m≤n
≤-steps (suc k) m≤n = ≤-step (≤-steps k m≤n)

m≤m+n : ∀ m n → m ≤ m + n
m≤m+n zero    n = z≤n
m≤m+n (suc m) n = s≤s (m≤m+n m n)

m≤′m+n : ∀ m n → m ≤′ m + n
m≤′m+n m n = ≤⇒≤′ (m≤m+n m n)

n≤′m+n : ∀ m n → n ≤′ m + n
n≤′m+n zero    n = ≤′-refl
n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n)

n≤m+n : ∀ m n → n ≤ m + n
n≤m+n m n = ≤′⇒≤ (n≤′m+n m n)

n≤1+n : ∀ n → n ≤ 1 + n
n≤1+n _ = ≤-step ≤-refl

1+n≰n : ∀ {n} → ¬ 1 + n ≤ n
1+n≰n (s≤s le) = 1+n≰n le

≤pred⇒≤ : ∀ m n → m ≤ pred n → m ≤ n
≤pred⇒≤ m zero    le = le
≤pred⇒≤ m (suc n) le = ≤-step le

≤⇒pred≤ : ∀ m n → m ≤ n → pred m ≤ n
≤⇒pred≤ zero    n le = le
≤⇒pred≤ (suc m) n le = start
  m     ≤⟨ n≤1+n m ⟩
  suc m ≤⟨ le ⟩
  n     □

¬i+1+j≤i : ∀ i {j} → ¬ i + suc j ≤ i
¬i+1+j≤i zero    ()
¬i+1+j≤i (suc i) le = ¬i+1+j≤i i (≤-pred le)

n∸m≤n : ∀ m n → n ∸ m ≤ n
n∸m≤n zero    n       = ≤-refl
n∸m≤n (suc m) zero    = ≤-refl
n∸m≤n (suc m) (suc n) = start
  n ∸ m  ≤⟨ n∸m≤n m n ⟩
  n      ≤⟨ n≤1+n n ⟩
  suc n  □

n≤m+n∸m : ∀ m n → n ≤ m + (n ∸ m)
n≤m+n∸m m       zero    = z≤n
n≤m+n∸m zero    (suc n) = ≤-refl
n≤m+n∸m (suc m) (suc n) = s≤s (n≤m+n∸m m n)

m⊓n≤m : ∀ m n → m ⊓ n ≤ m
m⊓n≤m zero    _       = z≤n
m⊓n≤m (suc m) zero    = z≤n
m⊓n≤m (suc m) (suc n) = s≤s $ m⊓n≤m m n

m≤m⊔n : ∀ m n → m ≤ m ⊔ n
m≤m⊔n zero    _       = z≤n
m≤m⊔n (suc m) zero    = ≤-refl
m≤m⊔n (suc m) (suc n) = s≤s $ m≤m⊔n m n

⌈n/2⌉≤′n : ∀ n → ⌈ n /2⌉ ≤′ n
⌈n/2⌉≤′n zero          = ≤′-refl
⌈n/2⌉≤′n (suc zero)    = ≤′-refl
⌈n/2⌉≤′n (suc (suc n)) = s≤′s (≤′-step (⌈n/2⌉≤′n n))

⌊n/2⌋≤′n : ∀ n → ⌊ n /2⌋ ≤′ n
⌊n/2⌋≤′n zero    = ≤′-refl
⌊n/2⌋≤′n (suc n) = ≤′-step (⌈n/2⌉≤′n n)

<-trans : Transitive _<_
<-trans {i} {j} {k} i<j j<k = start
  1 + i  ≤⟨ i<j ⟩
  j      ≤⟨ n≤1+n j ⟩
  1 + j  ≤⟨ j<k ⟩
  k      □

≰⇒> : _≰_ ⇒ _>_
≰⇒> {zero}          z≰n with z≰n z≤n
... | ()
≰⇒> {suc m} {zero}  _   = s≤s z≤n
≰⇒> {suc m} {suc n} m≰n = s≤s (≰⇒> (m≰n ∘ s≤s))

------------------------------------------------------------------------
-- (ℕ, _≡_, _<_) is a strict total order

m≢1+m+n : ∀ m {n} → m ≢ suc (m + n)
m≢1+m+n zero    ()
m≢1+m+n (suc m) eq = m≢1+m+n m (cong pred eq)

strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = record
  { Carrier            = ℕ
  ; _≈_                = _≡_
  ; _<_                = _<_
  ; isStrictTotalOrder = record
    { isEquivalence = PropEq.isEquivalence
    ; trans         = <-trans
    ; compare       = cmp
    ; <-resp-≈      = PropEq.resp₂ _<_
    }
  }
  where
  2+m+n≰m : ∀ {m n} → ¬ 2 + (m + n) ≤ m
  2+m+n≰m (s≤s le) = 2+m+n≰m le

  cmp : Trichotomous _≡_ _<_
  cmp m n with compare m n
  cmp .m .(suc (m + k)) | less    m k = tri< (m≤m+n (suc m) k) (m≢1+m+n _) 2+m+n≰m
  cmp .n             .n | equal   n   = tri≈ 1+n≰n refl 1+n≰n
  cmp .(suc (n + k)) .n | greater n k = tri> 2+m+n≰m (m≢1+m+n _ ∘ sym) (m≤m+n (suc n) k)

------------------------------------------------------------------------
-- Miscellaneous other properties

0∸n≡0 : LeftZero zero _∸_
0∸n≡0 zero    = refl
0∸n≡0 (suc _) = refl

n∸n≡0 : ∀ n → n ∸ n ≡ 0
n∸n≡0 zero    = refl
n∸n≡0 (suc n) = n∸n≡0 n

∸-+-assoc : ∀ m n o → (m ∸ n) ∸ o ≡ m ∸ (n + o)
∸-+-assoc m       n       zero    = cong (_∸_ m) (sym $ +-right-identity n)
∸-+-assoc zero    zero    (suc o) = refl
∸-+-assoc zero    (suc n) (suc o) = refl
∸-+-assoc (suc m) zero    (suc o) = refl
∸-+-assoc (suc m) (suc n) (suc o) = ∸-+-assoc m n (suc o)

+-∸-assoc : ∀ m {n o} → o ≤ n → (m + n) ∸ o ≡ m + (n ∸ o)
+-∸-assoc m (z≤n {n = n})             = begin m + n ∎
+-∸-assoc m (s≤s {m = o} {n = n} o≤n) = begin
  (m + suc n) ∸ suc o  ≡⟨ cong (λ n → n ∸ suc o) (+-suc m n) ⟩
  suc (m + n) ∸ suc o  ≡⟨ refl ⟩
  (m + n) ∸ o          ≡⟨ +-∸-assoc m o≤n ⟩
  m + (n ∸ o)          ∎

m+n∸n≡m : ∀ m n → (m + n) ∸ n ≡ m
m+n∸n≡m m n = begin
  (m + n) ∸ n  ≡⟨ +-∸-assoc m (≤-refl {x = n}) ⟩
  m + (n ∸ n)  ≡⟨ cong (_+_ m) (n∸n≡0 n) ⟩
  m + 0        ≡⟨ +-right-identity m ⟩
  m            ∎

m+n∸m≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
m+n∸m≡n {m} {n} m≤n = begin
  m + (n ∸ m)  ≡⟨ sym $ +-∸-assoc m m≤n ⟩
  (m + n) ∸ m  ≡⟨ cong (λ n → n ∸ m) (+-comm m n) ⟩
  (n + m) ∸ m  ≡⟨ m+n∸n≡m n m ⟩
  n            ∎

m⊓n+n∸m≡n : ∀ m n → (m ⊓ n) + (n ∸ m) ≡ n
m⊓n+n∸m≡n zero    n       = refl
m⊓n+n∸m≡n (suc m) zero    = refl
m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n

[m∸n]⊓[n∸m]≡0 : ∀ m n → (m ∸ n) ⊓ (n ∸ m) ≡ 0
[m∸n]⊓[n∸m]≡0 zero zero       = refl
[m∸n]⊓[n∸m]≡0 zero (suc n)    = refl
[m∸n]⊓[n∸m]≡0 (suc m) zero    = refl
[m∸n]⊓[n∸m]≡0 (suc m) (suc n) = [m∸n]⊓[n∸m]≡0 m n

[i+j]∸[i+k]≡j∸k : ∀ i j k → (i + j) ∸ (i + k) ≡ j ∸ k
[i+j]∸[i+k]≡j∸k zero    j k = refl
[i+j]∸[i+k]≡j∸k (suc i) j k = [i+j]∸[i+k]≡j∸k i j k

-- TODO: Can this proof be simplified? An automatic solver which can
-- handle ∸ would be nice...

i∸k∸j+j∸k≡i+j∸k : ∀ i j k → i ∸ (k ∸ j) + (j ∸ k) ≡ i + j ∸ k
i∸k∸j+j∸k≡i+j∸k zero j k = begin
  0 ∸ (k ∸ j) + (j ∸ k)
                         ≡⟨ cong (λ x → x + (j ∸ k)) (0∸n≡0 (k ∸ j)) ⟩
  0 + (j ∸ k)
                         ≡⟨ refl ⟩
  j ∸ k
                         ∎
i∸k∸j+j∸k≡i+j∸k (suc i) j zero = begin
  suc i ∸ (0 ∸ j) + j
                       ≡⟨ cong (λ x → suc i ∸ x + j) (0∸n≡0 j) ⟩
  suc i ∸ 0 + j
                       ≡⟨ refl ⟩
  suc (i + j)
                       ∎
i∸k∸j+j∸k≡i+j∸k (suc i) zero (suc k) = begin
  i ∸ k + 0
             ≡⟨ +-right-identity _ ⟩
  i ∸ k
             ≡⟨ cong (λ x → x ∸ k) (sym (+-right-identity _)) ⟩
  i + 0 ∸ k
             ∎
i∸k∸j+j∸k≡i+j∸k (suc i) (suc j) (suc k) = begin
  suc i ∸ (k ∸ j) + (j ∸ k)
                             ≡⟨ i∸k∸j+j∸k≡i+j∸k (suc i) j k ⟩
  suc i + j ∸ k
                             ≡⟨ cong (λ x → x ∸ k)
                                     (sym (+-suc i j)) ⟩
  i + suc j ∸ k
                             ∎

i+j≡0⇒i≡0 : ∀ i {j} → i + j ≡ 0 → i ≡ 0
i+j≡0⇒i≡0 zero    eq = refl
i+j≡0⇒i≡0 (suc i) ()

i+j≡0⇒j≡0 : ∀ i {j} → i + j ≡ 0 → j ≡ 0
i+j≡0⇒j≡0 i {j} i+j≡0 = i+j≡0⇒i≡0 j $ begin
  j + i
    ≡⟨ +-comm j i ⟩
  i + j
    ≡⟨ i+j≡0 ⟩
  0
    ∎

i*j≡0⇒i≡0∨j≡0 : ∀ i {j} → i * j ≡ 0 → i ≡ 0 ⊎ j ≡ 0
i*j≡0⇒i≡0∨j≡0 zero    {j}     eq = inj₁ refl
i*j≡0⇒i≡0∨j≡0 (suc i) {zero}  eq = inj₂ refl
i*j≡0⇒i≡0∨j≡0 (suc i) {suc j} ()

i*j≡1⇒i≡1 : ∀ i j → i * j ≡ 1 → i ≡ 1
i*j≡1⇒i≡1 (suc zero)    j             _  = refl
i*j≡1⇒i≡1 zero          j             ()
i*j≡1⇒i≡1 (suc (suc i)) (suc (suc j)) ()
i*j≡1⇒i≡1 (suc (suc i)) (suc zero)    ()
i*j≡1⇒i≡1 (suc (suc i)) zero          eq with begin
  0      ≡⟨ *-comm 0 i ⟩
  i * 0  ≡⟨ eq ⟩
  1      ∎
... | ()

i*j≡1⇒j≡1 : ∀ i j → i * j ≡ 1 → j ≡ 1
i*j≡1⇒j≡1 i j eq = i*j≡1⇒i≡1 j i (begin
  j * i  ≡⟨ *-comm j i ⟩
  i * j  ≡⟨ eq ⟩
  1      ∎)

cancel-+-left : ∀ i {j k} → i + j ≡ i + k → j ≡ k
cancel-+-left zero    eq = eq
cancel-+-left (suc i) eq = cancel-+-left i (cong pred eq)

cancel-+-left-≤ : ∀ i {j k} → i + j ≤ i + k → j ≤ k
cancel-+-left-≤ zero    le       = le
cancel-+-left-≤ (suc i) (s≤s le) = cancel-+-left-≤ i le

cancel-*-right : ∀ i j {k} → i * suc k ≡ j * suc k → i ≡ j
cancel-*-right zero    zero        eq = refl
cancel-*-right zero    (suc j)     ()
cancel-*-right (suc i) zero        ()
cancel-*-right (suc i) (suc j) {k} eq =
  cong suc (cancel-*-right i j (cancel-+-left (suc k) eq))

cancel-*-right-≤ : ∀ i j k → i * suc k ≤ j * suc k → i ≤ j
cancel-*-right-≤ zero    _       _ _  = z≤n
cancel-*-right-≤ (suc i) zero    _ ()
cancel-*-right-≤ (suc i) (suc j) k le =
  s≤s (cancel-*-right-≤ i j k (cancel-+-left-≤ (suc k) le))

*-distrib-∸ʳ : _*_ DistributesOverʳ _∸_
*-distrib-∸ʳ i zero k = begin
  (0 ∸ k) * i  ≡⟨ cong₂ _*_ (0∸n≡0 k) refl ⟩
  0            ≡⟨ sym $ 0∸n≡0 (k * i) ⟩
  0 ∸ k * i    ∎
*-distrib-∸ʳ i (suc j) zero    = begin i + j * i ∎
*-distrib-∸ʳ i (suc j) (suc k) = begin
  (j ∸ k) * i             ≡⟨ *-distrib-∸ʳ i j k ⟩
  j * i ∸ k * i           ≡⟨ sym $ [i+j]∸[i+k]≡j∸k i _ _ ⟩
  i + j * i ∸ (i + k * i) ∎

im≡jm+n⇒[i∸j]m≡n
  : ∀ i j m n →
    i * m ≡ j * m + n → (i ∸ j) * m ≡ n
im≡jm+n⇒[i∸j]m≡n i j m n eq = begin
  (i ∸ j) * m            ≡⟨ *-distrib-∸ʳ m i j ⟩
  (i * m) ∸ (j * m)      ≡⟨ cong₂ _∸_ eq (refl {x = j * m}) ⟩
  (j * m + n) ∸ (j * m)  ≡⟨ cong₂ _∸_ (+-comm (j * m) n) (refl {x = j * m}) ⟩
  (n + j * m) ∸ (j * m)  ≡⟨ m+n∸n≡m n (j * m) ⟩
  n                      ∎

i+1+j≢i : ∀ i {j} → i + suc j ≢ i
i+1+j≢i i eq = ¬i+1+j≤i i (reflexive eq)
  where open DecTotalOrder decTotalOrder

⌊n/2⌋-mono : ⌊_/2⌋ Preserves _≤_ ⟶ _≤_
⌊n/2⌋-mono z≤n             = z≤n
⌊n/2⌋-mono (s≤s z≤n)       = z≤n
⌊n/2⌋-mono (s≤s (s≤s m≤n)) = s≤s (⌊n/2⌋-mono m≤n)

⌈n/2⌉-mono : ⌈_/2⌉ Preserves _≤_ ⟶ _≤_
⌈n/2⌉-mono m≤n = ⌊n/2⌋-mono (s≤s m≤n)

pred-mono : pred Preserves _≤_ ⟶ _≤_
pred-mono z≤n      = z≤n
pred-mono (s≤s le) = le

_+-mono_ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
_+-mono_ {zero} {m₂} {n₁} {n₂} z≤n n₁≤n₂ = start
  n₁      ≤⟨ n₁≤n₂ ⟩
  n₂      ≤⟨ n≤m+n m₂ n₂ ⟩
  m₂ + n₂ □
s≤s m₁≤m₂ +-mono n₁≤n₂ = s≤s (m₁≤m₂ +-mono n₁≤n₂)

_*-mono_ : _*_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
z≤n       *-mono n₁≤n₂ = z≤n
s≤s m₁≤m₂ *-mono n₁≤n₂ = n₁≤n₂ +-mono (m₁≤m₂ *-mono n₁≤n₂)

∸-mono : _∸_ Preserves₂ _≤_ ⟶ _≥_ ⟶ _≤_
∸-mono           z≤n         (s≤s n₁≥n₂)    = z≤n
∸-mono           (s≤s m₁≤m₂) (s≤s n₁≥n₂)    = ∸-mono m₁≤m₂ n₁≥n₂
∸-mono {m₁} {m₂} m₁≤m₂       (z≤n {n = n₁}) = start
  m₁ ∸ n₁  ≤⟨ n∸m≤n n₁ m₁ ⟩
  m₁       ≤⟨ m₁≤m₂ ⟩
  m₂       □