text:
------------------------------------------------------------------------
-- A variant of declarative kinding in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Declarative where

open import Data.Context.WellFormed
open import Data.Fin using (Fin; zero)
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.Fin.Substitution.TypedRelation
open import Data.Nat using (ℕ)
open import Data.Product using (_,_; _×_; proj₁)
import Data.Vec as Vec
open import Function using (_∘_)
import Level
open import Relation.Binary.PropositionalEquality as PropEq hiding ([_])

open import FOmegaInt.Syntax

------------------------------------------------------------------------
-- Declarative (sub)kinding, subtyping and kind/type equality.
--
-- This module contains variants of the declarative kinding and
-- subtyping judgments which differ slightly from those given in the
-- Typing module.  Some of the rules in this module have additional
-- premises which we call "validity conditions".  These validity
-- conditions are redundant in the sense that they follow (more or
-- less) directly from so-called "validity" properties of the
-- corresponding judgments.  For example, the kinding rule (∈-Π-e)
-- below concludes that `Γ ⊢ a · b ∈ k Kind[ b ]' and has, among
-- others, the validity condition `Γ ⊢ k Kind[ b ] kd' as one of its
-- premises.  But this is a direct consequence of "kinding validity"
-- which states that the kinds of well-kinded types are themselves
-- well-formed, i.e. that `Γ ⊢ k kd' whenever `Γ ⊢Tp a ∈ k' (see the
-- Kinding.Declarative.Validity module for the full set of validity
-- lemmas).  Since all the validity conditions follow from
-- corresponding validity lemmas, they are, in principle, redundant.
-- Indeed, this is why they do not appear in the kinding and subtyping
-- rules of the Typing module.  The reason for including the validity
-- conditions as premises in the rules below is that the proofs of
-- some lemmas (notably the validity lemmas themselves) are done by
-- induction on kinding and subtyping derivations and require the
-- proofs of these conditions to be proper sub-derivations of the
-- derivations on which the induction is performed.
--
-- To proof the validity lemmas for both variants of the kinding and
-- subtyping judgments, we use the following strategy:
--
--  1. prove the validity lemmas for the judgments containing the
--     additional validity conditions as premises,
--
--  2. prove that the two variants of the judgments are
--     equivalent, i.e.
--
--     a) the extended judgments are sound w.r.t to the original
--        judgments: we can drop the validity conditions without
--        affecting the conclusion of the derivations, and
--
--     b) the extended judgments are complete w.r.t. to the original
--        judgments: crucially, the additional validity conditions
--        follow from the *remaining premises* of the extended rules
--        via the validity lemmas proved in step 1,
--
--  3. prove that validity holds for the original judgments via the
--     equivalence: convert to the extended judgment (via
--     completeness), apply the lemma in question, convert the
--     conclusion back (via soundness).
--
--  See the Kinding.Declarative.Equivalence module for the full proof
--  of equivalence (point 2) and the `Tp∈-valid' lemma in the
--  Typing.Inversion module for an example of point 3.

module Kinding where
  open TermCtx
  open Syntax
  open Substitution using (_[_]; _Kind[_]; weaken)

  infix 4 _ctx _⊢_kd _⊢_wf
  infix 4 _⊢Tp_∈_ _⊢_∈_
  infix 4 _⊢_<:_∈_ _⊢_<∷_
  infix 4 _⊢_≃_∈_ _⊢_≅_ _⊢_≃⊎≡_∈_

  mutual

    -- Well-formed typing contexts.

    _ctx : ∀ {n} → Ctx n → Set
    _ctx = ContextFormation._wf _⊢_wf

    -- Well-formed type/kind ascriptions in typing contexts.
    data _⊢_wf {n} (Γ : Ctx n) : TermAsc n → Set where
      wf-kd : ∀ {a} → Γ ⊢ a kd    → Γ ⊢ (kd a) wf
      wf-tp : ∀ {a} → Γ ⊢Tp a ∈ * → Γ ⊢ (tp a) wf

    -- Well-formed kinds.
    data _⊢_kd {n} (Γ : Ctx n) : Kind Term n → Set where
      kd-⋯ : ∀ {a b} → Γ ⊢Tp a ∈ * → Γ ⊢Tp b ∈ * → Γ ⊢ a ⋯ b kd
      kd-Π : ∀ {j k} → Γ ⊢ j kd → kd j ∷ Γ ⊢ k kd → Γ ⊢ Π j k kd

    -- Kinding derivations.
    data _⊢Tp_∈_ {n} (Γ : Ctx n) : Term n → Kind Term n → Set where
      ∈-var : ∀ {k} x → Γ ctx → lookup Γ x ≡ kd k → Γ ⊢Tp var x ∈ k
      ∈-⊥-f : Γ ctx → Γ ⊢Tp ⊥ ∈ *
      ∈-⊤-f : Γ ctx → Γ ⊢Tp ⊤ ∈ *
      ∈-∀-f : ∀ {k a} → Γ ⊢ k kd → kd k ∷ Γ ⊢Tp a ∈ * → Γ ⊢Tp Π k a ∈ *
      ∈-→-f : ∀ {a b} → Γ ⊢Tp a ∈ * → Γ ⊢Tp b ∈ * → Γ ⊢Tp a ⇒ b ∈ *
      ∈-Π-i : ∀ {j a k} → Γ ⊢ j kd → kd j ∷ Γ ⊢Tp a ∈ k →
              -- Validity condition:
              kd j ∷ Γ ⊢ k kd →
              Γ ⊢Tp Λ j a ∈ Π j k
      ∈-Π-e : ∀ {a b j k} → Γ ⊢Tp a ∈ Π j k → Γ ⊢Tp b ∈ j →
              -- Validity conditions:
              kd j ∷ Γ ⊢ k kd → Γ ⊢ k Kind[ b ] kd →
              Γ ⊢Tp a · b ∈ k Kind[ b ]
      ∈-s-i : ∀ {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢Tp a ∈ a ⋯ a
      ∈-⇑   : ∀ {a j k} → Γ ⊢Tp a ∈ j → Γ ⊢ j <∷ k → Γ ⊢Tp a ∈ k

    -- Subkinding derivations.
    data _⊢_<∷_ {n} (Γ : Ctx n) : Kind Term n → Kind Term 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₂

    -- Subtyping derivations.
    data _⊢_<:_∈_ {n} (Γ : Ctx n) : Term n → Term n → Kind Term n → Set where
      <:-refl  : ∀ {a k}     → Γ ⊢Tp a ∈ k → Γ ⊢ a <: a ∈ k
      <:-trans : ∀ {a b c k} → Γ ⊢ a <: b ∈ k → Γ ⊢ b <: c ∈ k → Γ ⊢ a <: c ∈ k
      <:-β₁    : ∀ {j a k b} → kd j ∷ Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ j →
                 -- Validity conditions:
                 Γ ⊢Tp a [ b ] ∈ k Kind[ b ] →
                 kd j ∷ Γ ⊢ k kd → Γ ⊢ k Kind[ b ] kd →
                 Γ ⊢ (Λ j a) · b <: a [ b ] ∈ k Kind[ b ]
      <:-β₂    : ∀ {j a k b} → kd j ∷ Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ j →
                 -- Validity conditions:
                 Γ ⊢Tp a [ b ] ∈ k Kind[ b ] →
                 kd j ∷ Γ ⊢ k kd → Γ ⊢ k Kind[ b ] kd →
                 Γ ⊢ a [ b ] <: (Λ j a) · b ∈ k Kind[ b ]
      <:-η₁    : ∀ {a j k} → Γ ⊢Tp a ∈ Π j k →
                 Γ ⊢ Λ j (weaken a · var zero) <: a ∈ Π j k
      <:-η₂    : ∀ {a j k} → Γ ⊢Tp a ∈ Π j k →
                 Γ ⊢ a <: Λ j (weaken a · var zero) ∈ Π j k
      <:-⊥     : ∀ {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢ ⊥ <: a ∈ *
      <:-⊤     : ∀ {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢ a <: ⊤ ∈ *
      <:-∀     : ∀ {k₁ k₂ a₁ a₂} →
                 Γ ⊢ k₂ <∷ k₁ → kd k₂ ∷ Γ ⊢ a₁ <: a₂ ∈ * → Γ ⊢Tp Π k₁ a₁ ∈ * →
                 Γ ⊢ Π k₁ a₁ <: Π k₂ a₂ ∈ *
      <:-→     : ∀ {a₁ a₂ b₁ b₂} → Γ ⊢ a₂ <: a₁ ∈ * → Γ ⊢ b₁ <: b₂ ∈ * →
                 Γ ⊢ a₁ ⇒ b₁ <: a₂ ⇒ b₂ ∈ *
      <:-λ     : ∀ {j₁ j₂ a₁ a₂ j k} → kd j ∷ Γ ⊢ a₁ <: a₂ ∈ k →
                 Γ ⊢Tp Λ j₁ a₁ ∈ Π j k → Γ ⊢Tp Λ j₂ a₂ ∈ Π j k →
                 Γ ⊢ Λ j₁ a₁ <: Λ j₂ a₂ ∈ Π j k
      <:-·     : ∀ {a₁ a₂ b₁ b₂ j k} → Γ ⊢ a₁ <: a₂ ∈ Π j k → Γ ⊢ b₁ ≃ b₂ ∈ j →
                 -- Validity conditions:
                 Γ ⊢Tp b₁ ∈ j → kd j ∷ Γ ⊢ k kd → Γ ⊢ k Kind[ b₁ ] kd →
                 Γ ⊢ a₁ · b₁ <: a₂ · b₂ ∈ k Kind[ b₁ ]
      <:-⟨|    : ∀ {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢ b <: a ∈ *
      <:-|⟩    : ∀ {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢ a <: c ∈ *
      <:-⋯-i   : ∀ {a b c d} → Γ ⊢ a <: b ∈ c ⋯ d → Γ ⊢ a <: b ∈ a ⋯ b
      <:-⇑     : ∀ {a b j k} → Γ ⊢ a <: b ∈ j → Γ ⊢ j <∷ k → Γ ⊢ a <: b ∈ k

    -- Type equality.
    data _⊢_≃_∈_ {n} (Γ : Ctx n) : Term n → Term n → Kind Term n → Set where
      <:-antisym : ∀ {a b k} → Γ ⊢ a <: b ∈ k → Γ ⊢ b <: a ∈ k → Γ ⊢ a ≃ b ∈ k

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

  -- Combined kinding of types and term variable typing.
  data _⊢_∈_ {n} (Γ : Ctx n) : Term n → TermAsc n → Set where
    ∈-tp  : ∀ {a k} → Γ ⊢Tp a ∈ k → Γ ⊢ a ∈ kd k
    ∈-var : ∀ x {a} → Γ ctx → lookup Γ x ≡ tp a → Γ ⊢ var x ∈ tp a

  -- Combined type equality and syntactic term variable equality (used
  -- for well-formed equality lifted to substitutions).
  data _⊢_≃⊎≡_∈_ {n} (Γ : Ctx n) : Term n → Term n → TermAsc n → Set where
    ≃-tp  : ∀ {a b k} → Γ ⊢ a ≃ b ∈ k           → Γ ⊢ a     ≃⊎≡ b     ∈ kd k
    ≃-var : ∀ x {a} → Γ ctx → lookup Γ x ≡ tp a → Γ ⊢ var x ≃⊎≡ var x ∈ tp a

  open PropEq using ([_])

  -- Derived variable rules.

  ∈-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 ] = ∈-var x Γ-ctx Γ[x]≡tp-a

  ≃⊎≡-var : ∀ {n} {Γ : Ctx n} x → Γ ctx → Γ ⊢ var x ≃⊎≡ var x ∈ lookup Γ x
  ≃⊎≡-var {Γ = Γ} x Γ-ctx with lookup Γ x | inspect (lookup Γ) x
  ≃⊎≡-var x Γ-ctx | kd k | [ Γ[x]≡kd-k ] =
    let x∈a = ∈-var x Γ-ctx Γ[x]≡kd-k
    in ≃-tp (<:-antisym (<:-refl x∈a) (<:-refl x∈a))
  ≃⊎≡-var x Γ-ctx | tp a | [ Γ[x]≡tp-a ] = ≃-var x Γ-ctx Γ[x]≡tp-a

  open ContextFormation _⊢_wf public
    hiding (_wf) renaming (_⊢_wfExt to _⊢_ext)

------------------------------------------------------------------------
-- Properties of typings

open Syntax
open TermCtx
open Kinding

-- 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<∷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<∷k k<∷j) = j<∷k

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

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

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

-- Symmetry of kind equality.
≅-sym : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j ≅ k → Γ ⊢ k ≅ j
≅-sym (<∷-antisym j<∷k k<∷j) = <∷-antisym k<∷j j<∷k

-- An admissible kind equality rule for interval kinds.
≅-⋯ : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂} →
      Γ ⊢ a₁ ≃ a₂ ∈ * → Γ ⊢ b₁ ≃ b₂ ∈ * → Γ ⊢ a₁ ⋯ b₁ ≅ a₂ ⋯ b₂
≅-⋯ (<:-antisym a₁<:a₂ a₂<:a₁) (<:-antisym b₁<:b₂ b₂<:b₁) =
  <∷-antisym (<∷-⋯ a₂<:a₁ b₁<:b₂) (<∷-⋯ a₁<:a₂ b₂<:b₁)

-- Type equality is reflexive.
≃-refl : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Tp a ∈ k → Γ ⊢ a ≃ a ∈ k
≃-refl a∈k = <:-antisym (<:-refl a∈k) (<:-refl a∈k)

-- Type equality is transitive.
≃-trans : ∀ {n} {Γ : Ctx n} {a b c k} →
          Γ ⊢ a ≃ b ∈ k → Γ ⊢ b ≃ c ∈ k → Γ ⊢ a ≃ c ∈ k
≃-trans (<:-antisym a<:b b<:a) (<:-antisym b<:c c<:b) =
  <:-antisym (<:-trans a<:b b<:c) (<:-trans c<:b b<:a)

-- Type equality is symmetric.
≃-sym : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a ≃ b ∈ k → Γ ⊢ b ≃ a ∈ k
≃-sym (<:-antisym a<:b b<:a) = <:-antisym b<:a a<:b

-- Reflexivity of the combined type and term variable equality.
≃⊎≡-refl : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a ∈ b → Γ ⊢ a ≃⊎≡ a ∈ b
≃⊎≡-refl (∈-tp a∈k)                = ≃-tp (≃-refl a∈k)
≃⊎≡-refl (∈-var x Γ-ctx Γ[x]≡tp-a) = ≃-var x Γ-ctx Γ[x]≡tp-a

-- Types inhabiting interval kinds are proper Types.
Tp∈-⋯-* : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Tp a ∈ b ⋯ c → Γ ⊢Tp a ∈ *
Tp∈-⋯-* a∈b⋯c = ∈-⇑ (∈-s-i a∈b⋯c) (<∷-⋯ (<:-⊥ a∈b⋯c) (<:-⊤ a∈b⋯c))

-- Well-formedness of the * kind.
*-kd : ∀ {n} {Γ : Ctx n} → Γ ctx → Γ ⊢ * kd
*-kd Γ-ctx = kd-⋯ (∈-⊥-f Γ-ctx) (∈-⊤-f Γ-ctx)

module _ where
  open Substitution

  -- An admissible β-rule for type equality.
  ≃-β : ∀ {n} {Γ : Ctx n} {j a k b} → kd j ∷ Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ j →
        -- Validity conditions:
        Γ ⊢Tp a [ b ] ∈ k Kind[ b ] → kd j ∷ Γ ⊢ k kd → Γ ⊢ k Kind[ b ] kd →
        Γ ⊢ (Λ j a) · b ≃ a [ b ] ∈ k Kind[ b ]
  ≃-β a∈k b∈j a[b]∈k[b] k-kd k[b]-kd =
    <:-antisym (<:-β₁ a∈k b∈j a[b]∈k[b] k-kd k[b]-kd)
               (<:-β₂ a∈k b∈j a[b]∈k[b] k-kd k[b]-kd)

  -- An admissible η-rule for type equality.
  ≃-η : ∀ {n} {Γ : Ctx n} {a j k} →
        Γ ⊢Tp a ∈ Π j k → Γ ⊢ Λ j (weaken a · var zero) ≃ a ∈ Π j k
  ≃-η a∈Πjk = <:-antisym (<:-η₁ a∈Πjk) (<:-η₂ a∈Πjk)

-- An admissible congruence rule for type equality w.r.t. formation of
-- arrow types.
≃-→ : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂} →
      Γ ⊢ a₁ ≃ a₂ ∈ * → Γ ⊢ b₁ ≃ b₂ ∈ * → Γ ⊢ a₁ ⇒ b₁ ≃ a₂ ⇒ b₂ ∈ *
≃-→ (<:-antisym a₁<:a₂∈* a₂<:a₁∈*) (<:-antisym b₁<:b₂∈* b₂<:b₁∈*) =
  <:-antisym (<:-→ a₂<:a₁∈* b₁<:b₂∈*) (<:-→ a₁<:a₂∈* b₂<:b₁∈*)

-- An admissible congruence rule for type equality w.r.t. operator
-- abstraction.
≃-λ : ∀ {n} {Γ : Ctx n} {j₁ j₂ a₁ a₂ j k} →
      kd j ∷ Γ ⊢ a₁ ≃ a₂ ∈ k → Γ ⊢Tp Λ j₁ a₁ ∈ Π j k → Γ ⊢Tp Λ j₂ a₂ ∈ Π j k →
      Γ ⊢ Λ j₁ a₁ ≃ Λ j₂ a₂ ∈ Π j k
≃-λ (<:-antisym a₁<:a₂∈k a₂<:a₁∈k) Λj₁a₁∈Πjk Λj₂a₂∈Πjk =
  <:-antisym (<:-λ a₁<:a₂∈k Λj₁a₁∈Πjk Λj₂a₂∈Πjk)
             (<:-λ a₂<:a₁∈k Λj₂a₂∈Πjk Λj₁a₁∈Πjk)

-- An admissible subsumption rule for type equality.
≃-⇑ : ∀ {n} {Γ : Ctx n} {a b j k} → Γ ⊢ a ≃ b ∈ j → Γ ⊢ j <∷ k → Γ ⊢ a ≃ b ∈ k
≃-⇑ (<:-antisym a<:b b<:a) j<∷k = <:-antisym (<:-⇑ a<:b j<∷k) (<:-⇑ b<:a j<∷k)

-- The contexts of all the above judgments are well-formed.

mutual

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

  Tp∈-ctx : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Tp a ∈ k → Γ ctx
  Tp∈-ctx (∈-var x Γ-ctx Γ[x]≡kd-k) = Γ-ctx
  Tp∈-ctx (∈-⊥-f Γ-ctx)             = Γ-ctx
  Tp∈-ctx (∈-⊤-f Γ-ctx)             = Γ-ctx
  Tp∈-ctx (∈-∀-f k-kd a∈*)          = kd-ctx k-kd
  Tp∈-ctx (∈-→-f a∈* b∈*)           = Tp∈-ctx a∈*
  Tp∈-ctx (∈-Π-i j-kd a∈k k-kd)     = kd-ctx j-kd
  Tp∈-ctx (∈-Π-e a∈Πjk b∈j k-kd k[b]-kd) = Tp∈-ctx a∈Πjk
  Tp∈-ctx (∈-s-i a∈b⋯c)             = Tp∈-ctx a∈b⋯c
  Tp∈-ctx (∈-⇑ a∈j j<∷k)            = Tp∈-ctx a∈j

wf-ctx : ∀ {n} {Γ : Ctx n} {a} → Γ ⊢ a wf → Γ ctx
wf-ctx (wf-kd k-kd) = kd-ctx k-kd
wf-ctx (wf-tp a∈*)  = Tp∈-ctx a∈*

<:-ctx : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a <: b ∈ k → Γ ctx
<:-ctx (<:-refl a∈k)            = Tp∈-ctx a∈k
<:-ctx (<:-trans a<:b∈k b<:c∈k) = <:-ctx a<:b∈k
<:-ctx (<:-β₁ a∈j b∈k a[b]∈k[b] k-kd k[b]-kd) = Tp∈-ctx b∈k
<:-ctx (<:-β₂ a∈j b∈k a[b]∈k[b] k-kd k[b]-kd) = Tp∈-ctx b∈k
<:-ctx (<:-η₁ a∈Πjk) = Tp∈-ctx a∈Πjk
<:-ctx (<:-η₂ a∈Πjk) = Tp∈-ctx a∈Πjk
<:-ctx (<:-⊥ a∈b⋯c)  = Tp∈-ctx a∈b⋯c
<:-ctx (<:-⊤ a∈b⋯c)  = Tp∈-ctx a∈b⋯c
<:-ctx (<:-∀ k₂<∷k₁ a₁<:a₂ ∀k₁a₁∈*) = Tp∈-ctx ∀k₁a₁∈*
<:-ctx (<:-→ a₂<:a₁ b₁<:b₂)         = <:-ctx a₂<:a₁
<:-ctx (<:-λ a₂<:a₁∈Πjk Λa₁k₁∈Πjk Λa₂k₂∈Πjk)        = Tp∈-ctx Λa₁k₁∈Πjk
<:-ctx (<:-· a₂<:a₁∈Πjk b₂≃b₁∈j b₁∈j k-kd k[b₁]-kd) = <:-ctx a₂<:a₁∈Πjk
<:-ctx (<:-⟨| a∈b⋯c)      = Tp∈-ctx a∈b⋯c
<:-ctx (<:-|⟩ a∈b⋯c)      = Tp∈-ctx a∈b⋯c
<:-ctx (<:-⋯-i a<:b∈c⋯d)  = <:-ctx a<:b∈c⋯d
<:-ctx (<:-⇑ a<:b∈j j<∷k) = <:-ctx a<:b∈j

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

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

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

∈-ctx : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a ∈ b → Γ ctx
∈-ctx (∈-tp a∈k)                = Tp∈-ctx a∈k
∈-ctx (∈-var x Γ-ctx Γ[x]≡tp-a) = Γ-ctx

≃⊎≡-ctx : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢ a ≃⊎≡ b ∈ c → Γ ctx
≃⊎≡-ctx (≃-tp a≃b∈k)              = ≃-ctx a≃b∈k
≃⊎≡-ctx (≃-var x Γ-ctx Γ[x]≡tp-a) = Γ-ctx

----------------------------------------------------------------------
-- Well-kinded/typed substitutions (i.e. substitution lemmas)

-- A shorthand for kindings and typings of Ts by kind or type
-- ascriptions.
TermAscTyping : (ℕ → Set) → Set₁
TermAscTyping T = Typing TermAsc T TermAsc Level.zero

-- Liftings from well-typed Ts to well-typed/kinded terms/types.
LiftTo-∈ : ∀ {T} → TermAscTyping T → Set₁
LiftTo-∈ _⊢T_∈_ = LiftTyped Substitution.termAscTermSubst _⊢_wf _⊢T_∈_ _⊢_∈_

-- Helper lemmas about untyped T-substitutions in raw terms and kinds.

record TypedSubstAppHelpers {T} (rawLift : Lift T Term) : Set where
  open Substitution using (weaken; _[_]; _Kind[_])
  module A = SubstApp rawLift
  module L = Lift     rawLift

  field
    -- Substitutions in kinds and types commute.

    Kind/-sub-↑ : ∀ {m n} k a (σ : Sub T m n) →
                  k Kind[ a ] A.Kind/ σ ≡ (k A.Kind/ σ L.↑) Kind[ a A./ σ ]

    /-sub-↑ : ∀ {m n} b a (σ : Sub T m n) →
              b [ a ] A./ σ ≡ (b A./ σ L.↑) [ a A./ σ ]

    -- Weakening of terms commutes with substitution in terms.

    weaken-/ : ∀ {m n} {σ : Sub T m n} a →
               weaken (a A./ σ) ≡ weaken a A./ σ L.↑

-- Application of generic well-typed T-substitutions to all the judgments.

module TypedSubstApp {T : ℕ → Set} (_⊢T_∈_ : TermAscTyping T)
                     (liftTyped : LiftTo-∈ _⊢T_∈_)
                     (helpers : TypedSubstAppHelpers
                                  (LiftTyped.rawLift liftTyped))
                     where

  open LiftTyped liftTyped renaming (lookup to /∈-lookup)
  open TypedSubstAppHelpers helpers

  -- Lift well-kinded Ts to well-kinded types.
  liftTp : ∀ {n} {Γ : Ctx n} {a k kd-k} →
           kd-k ≡ kd k → Γ ⊢T a ∈ kd-k → Γ ⊢Tp L.lift a ∈ k
  liftTp refl a∈kd-k with ∈-lift a∈kd-k
  liftTp refl a∈kd-k | ∈-tp a∈k = a∈k

  mutual

    -- Substitutions preserve well-formedness of kinds and
    -- well-kindedness of types.

    kd-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {k σ} →
           Γ ⊢ k kd → Δ ⊢/ σ ∈ Γ → Δ ⊢ k A.Kind/ σ kd
    kd-/ (kd-⋯ a∈* b∈*)   σ∈Γ = kd-⋯ (Tp∈-/ a∈* σ∈Γ) (Tp∈-/ b∈* σ∈Γ)
    kd-/ (kd-Π j-kd k-kd) σ∈Γ =
      kd-Π j/σ-kd (kd-/ k-kd (∈-↑ (wf-kd j/σ-kd) σ∈Γ))
      where j/σ-kd = kd-/ j-kd σ∈Γ

    Tp∈-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a k σ} →
            Γ ⊢Tp a ∈ k → Δ ⊢/ σ ∈ Γ → Δ ⊢Tp a A./ σ ∈ k A.Kind/ σ
    Tp∈-/ (∈-var x Γ-ctx Γ[x]≡kd-k) σ∈Γ =
      liftTp (cong (_/ _) Γ[x]≡kd-k) (/∈-lookup σ∈Γ x)
    Tp∈-/ (∈-⊥-f Γ-ctx)    σ∈Γ = ∈-⊥-f (/∈-wf σ∈Γ)
    Tp∈-/ (∈-⊤-f Γ-ctx)    σ∈Γ = ∈-⊤-f (/∈-wf σ∈Γ)
    Tp∈-/ (∈-∀-f k-kd a∈*) σ∈Γ =
      ∈-∀-f k/σ-kd (Tp∈-/ a∈* (∈-↑ (wf-kd k/σ-kd) σ∈Γ))
      where k/σ-kd = kd-/ k-kd σ∈Γ
    Tp∈-/ (∈-→-f a∈* b∈*)  σ∈Γ = ∈-→-f (Tp∈-/ a∈* σ∈Γ) (Tp∈-/ b∈* σ∈Γ)
    Tp∈-/ (∈-Π-i j-kd a∈k k-kd) σ∈Γ =
      ∈-Π-i j/σ-kd (Tp∈-/ a∈k σ↑∈j∷Γ) (kd-/ k-kd σ↑∈j∷Γ)
      where
        j/σ-kd = kd-/ j-kd σ∈Γ
        σ↑∈j∷Γ = ∈-↑ (wf-kd j/σ-kd) σ∈Γ
    Tp∈-/ (∈-Π-e {_} {b} {_} {k} a∈Πjk b∈j k-kd k[b]-kd) σ∈Γ =
      subst (_ ⊢Tp _ ∈_) (sym k[b]/σ≡k/σ[b/σ])
            (∈-Π-e (Tp∈-/ a∈Πjk σ∈Γ) (Tp∈-/ b∈j σ∈Γ)
                   (kd-/ k-kd (∈-↑ (kd-/-wf k-kd σ∈Γ) σ∈Γ))
                   (subst (_ ⊢_kd) k[b]/σ≡k/σ[b/σ] (kd-/ k[b]-kd σ∈Γ)))
      where k[b]/σ≡k/σ[b/σ] = Kind/-sub-↑ k b _
    Tp∈-/ (∈-s-i a∈b⋯c)  σ∈Γ = ∈-s-i (Tp∈-/ a∈b⋯c σ∈Γ)
    Tp∈-/ (∈-⇑ a∈j j<∷k) σ∈Γ = ∈-⇑ (Tp∈-/ a∈j σ∈Γ) (<∷-/ j<∷k σ∈Γ)

    -- Substitutions commute with subkinding, subtyping and type
    -- equality.

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

    <:-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b k σ} →
           Γ ⊢ a <: b ∈ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A./ σ <: b A./ σ ∈ k A.Kind/ σ
    <:-/ (<:-refl a∈k)            σ∈Γ = <:-refl (Tp∈-/ a∈k σ∈Γ)
    <:-/ (<:-trans a<:b∈k b<:c∈k) σ∈Γ =
      <:-trans (<:-/ a<:b∈k σ∈Γ) (<:-/ b<:c∈k σ∈Γ)
    <:-/ (<:-β₁ {j} {a} {k} {b} a∈k b∈j a[b]∈k[b] k-kd k[b]-kd) σ∈Γ =
      subst₂ (_ ⊢ (Λ j a) · b A./ _ <:_∈_)
             (sym a[b]/σ≡a/σ[b/σ]) (sym k[b]/σ≡k/σ[b/σ])
             (<:-β₁ (Tp∈-/ a∈k σ↑∈j∷Γ) (Tp∈-/ b∈j σ∈Γ)
                    (subst₂ (_ ⊢Tp_∈_) a[b]/σ≡a/σ[b/σ] k[b]/σ≡k/σ[b/σ]
                            (Tp∈-/ a[b]∈k[b] σ∈Γ))
                    (kd-/ k-kd σ↑∈j∷Γ)
                    (subst (_ ⊢_kd) k[b]/σ≡k/σ[b/σ] (kd-/ k[b]-kd σ∈Γ)))
      where
        σ↑∈j∷Γ          = ∈-↑ (Tp∈-/-wf a∈k σ∈Γ) σ∈Γ
        k[b]/σ≡k/σ[b/σ] = Kind/-sub-↑ k b _
        a[b]/σ≡a/σ[b/σ] = /-sub-↑ a b _
    <:-/ (<:-β₂ {j} {a} {k} {b} a∈k b∈j a[b]∈k[b] k-kd k[b]-kd) σ∈Γ =
      subst₂ (_ ⊢_<: (Λ j a) · b A./ _ ∈_)
             (sym a[b]/σ≡a/σ[b/σ]) (sym k[b]/σ≡k/σ[b/σ])
             (<:-β₂ (Tp∈-/ a∈k σ↑∈j∷Γ) (Tp∈-/ b∈j σ∈Γ)
                    (subst₂ (_ ⊢Tp_∈_) a[b]/σ≡a/σ[b/σ] k[b]/σ≡k/σ[b/σ]
                            (Tp∈-/ a[b]∈k[b] σ∈Γ))
                    (kd-/ k-kd σ↑∈j∷Γ)
                    (subst (_ ⊢_kd) k[b]/σ≡k/σ[b/σ] (kd-/ k[b]-kd σ∈Γ)))
      where
        σ↑∈j∷Γ          = ∈-↑ (Tp∈-/-wf a∈k σ∈Γ) σ∈Γ
        k[b]/σ≡k/σ[b/σ] = Kind/-sub-↑ k b _
        a[b]/σ≡a/σ[b/σ] = /-sub-↑ a b _
    <:-/ {Δ = Δ} {σ = σ} (<:-η₁ {a} {j} {k} a∈Πjk) σ∈Γ =
      subst (Δ ⊢_<: a A./ σ ∈ Π j k A.Kind/ σ)
            (cong (Λ _) (cong₂ _·_ (weaken-/ a) (sym (lift-var zero))))
            (<:-η₁ (Tp∈-/ a∈Πjk σ∈Γ))
    <:-/ {Δ = Δ} {σ = σ} (<:-η₂  {a} {j} {k} a∈Πjk) σ∈Γ =
      subst (Δ ⊢ a A./ σ <:_∈ Π j k A.Kind/ σ)
            (cong (Λ _) (cong₂ _·_ (weaken-/ a) (sym (lift-var zero))))
            (<:-η₂ (Tp∈-/ a∈Πjk σ∈Γ))
    <:-/ (<:-⊥ a∈b⋯c) σ∈Γ = <:-⊥ (Tp∈-/ a∈b⋯c σ∈Γ)
    <:-/ (<:-⊤ a∈b⋯c) σ∈Γ = <:-⊤ (Tp∈-/ a∈b⋯c σ∈Γ)
    <:-/ (<:-∀ k₂<∷k₁ a₁<:a₂∈* ∀j₁k₁∈*) σ∈Γ =
      <:-∀ (<∷-/ k₂<∷k₁ σ∈Γ) (<:-/ a₁<:a₂∈* (∈-↑ (<:-/-wf a₁<:a₂∈* σ∈Γ) σ∈Γ))
           (Tp∈-/ ∀j₁k₁∈* σ∈Γ)
    <:-/ (<:-→ a₂<:a₁∈* b₁<:b₂∈*) σ∈Γ =
      <:-→ (<:-/ a₂<:a₁∈* σ∈Γ) (<:-/ b₁<:b₂∈* σ∈Γ)
    <:-/ (<:-λ a₁<:a₂∈k Λj₁a₁∈Πjk Λj₂a₂∈Πjk) σ∈Γ =
      <:-λ (<:-/ a₁<:a₂∈k (∈-↑ (<:-/-wf a₁<:a₂∈k σ∈Γ) σ∈Γ))
           (Tp∈-/ Λj₁a₁∈Πjk σ∈Γ) (Tp∈-/ Λj₂a₂∈Πjk σ∈Γ)
    <:-/ (<:-· {k = k} a₁<:a₂∈Πjk b₁≃b₂∈j b₁∈j k-kd k[b₁]-kd) σ∈Γ =
      subst (_ ⊢ _ <: _ ∈_) (sym k[b₁]/σ≡k/σ[b₁/σ])
            (<:-· (<:-/ a₁<:a₂∈Πjk σ∈Γ) (≃-/ b₁≃b₂∈j σ∈Γ)
                  (Tp∈-/ b₁∈j σ∈Γ) (kd-/ k-kd (∈-↑ (kd-/-wf k-kd σ∈Γ) σ∈Γ))
                  (subst (_ ⊢_kd) k[b₁]/σ≡k/σ[b₁/σ] (kd-/ k[b₁]-kd σ∈Γ)))
      where k[b₁]/σ≡k/σ[b₁/σ] = Kind/-sub-↑ k _ _
    <:-/ (<:-⟨| a∈b⋯c)      σ∈Γ = <:-⟨| (Tp∈-/ a∈b⋯c σ∈Γ)
    <:-/ (<:-|⟩ a∈b⋯c)      σ∈Γ = <:-|⟩ (Tp∈-/ a∈b⋯c σ∈Γ)
    <:-/ (<:-⋯-i a<:b∈c⋯d)  σ∈Γ = <:-⋯-i (<:-/ a<:b∈c⋯d σ∈Γ)
    <:-/ (<:-⇑ a<:b∈j j<∷k) σ∈Γ = <:-⇑ (<:-/ a<:b∈j σ∈Γ) (<∷-/ j<∷k σ∈Γ)

    ≃-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b k σ} →
          Γ ⊢ a ≃ b ∈ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A./ σ ≃ b A./ σ ∈ k A.Kind/ σ
    ≃-/ (<:-antisym a<:b∈k b<:a∈k) σ∈Γ =
      <:-antisym (<:-/ a<:b∈k σ∈Γ) (<:-/ b<:a∈k σ∈Γ)

    -- Helpers (to satisfy the termination checker).

    kd-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k σ} →
              kd j ∷ Γ ⊢ k kd → Δ ⊢/ σ ∈ Γ → Δ ⊢ kd (j A.Kind/ σ) wf
    kd-/-wf (kd-⋯ a∈* _)  σ∈Γ = Tp∈-/-wf a∈* σ∈Γ
    kd-/-wf (kd-Π j-kd _) σ∈Γ = kd-/-wf j-kd σ∈Γ

    Tp∈-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a j k σ} →
               kd j ∷ Γ ⊢Tp a ∈ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ kd (j A.Kind/ σ) wf
    Tp∈-/-wf (∈-var x (wf-kd k-kd ∷ Γ-ctx) _) σ∈Γ = wf-kd (kd-/ k-kd σ∈Γ)
    Tp∈-/-wf (∈-⊥-f (wf-kd j-kd ∷ Γ-ctx)) σ∈Γ = wf-kd (kd-/ j-kd σ∈Γ)
    Tp∈-/-wf (∈-⊤-f (wf-kd j-kd ∷ Γ-ctx)) σ∈Γ = wf-kd (kd-/ j-kd σ∈Γ)
    Tp∈-/-wf (∈-∀-f k-kd _)      σ∈Γ = kd-/-wf k-kd σ∈Γ
    Tp∈-/-wf (∈-→-f a∈* _)       σ∈Γ = Tp∈-/-wf a∈* σ∈Γ
    Tp∈-/-wf (∈-Π-i j-kd _ _)    σ∈Γ = kd-/-wf j-kd σ∈Γ
    Tp∈-/-wf (∈-Π-e a∈Πjk _ _ _) σ∈Γ = Tp∈-/-wf a∈Πjk σ∈Γ
    Tp∈-/-wf (∈-s-i a∈b⋯c)       σ∈Γ = Tp∈-/-wf a∈b⋯c σ∈Γ
    Tp∈-/-wf (∈-⇑ a∈b _)         σ∈Γ = Tp∈-/-wf a∈b σ∈Γ

    <:-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b j k σ} →
              kd j ∷ Γ ⊢ a <: b ∈ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ kd (j A.Kind/ σ) wf
    <:-/-wf (<:-refl a∈k)        σ∈Γ = Tp∈-/-wf a∈k σ∈Γ
    <:-/-wf (<:-trans a<:b _)    σ∈Γ = <:-/-wf a<:b σ∈Γ
    <:-/-wf (<:-β₁ _ b∈j _ _ _)  σ∈Γ = Tp∈-/-wf b∈j σ∈Γ
    <:-/-wf (<:-β₂ _ b∈j _ _ _)  σ∈Γ = Tp∈-/-wf b∈j σ∈Γ
    <:-/-wf (<:-η₁ a∈Πjk)        σ∈Γ = Tp∈-/-wf a∈Πjk σ∈Γ
    <:-/-wf (<:-η₂ a∈Πjk)        σ∈Γ = Tp∈-/-wf a∈Πjk σ∈Γ
    <:-/-wf (<:-⊥ a∈b⋯c)         σ∈Γ = Tp∈-/-wf a∈b⋯c σ∈Γ
    <:-/-wf (<:-⊤ a∈b⋯c)         σ∈Γ = Tp∈-/-wf a∈b⋯c σ∈Γ
    <:-/-wf (<:-∀ j₂<∷j₁ _ _)    σ∈Γ = <∷-/-wf j₂<∷j₁ σ∈Γ
    <:-/-wf (<:-→ a₂<:a₁∈* _)    σ∈Γ = <:-/-wf a₂<:a₁∈* σ∈Γ
    <:-/-wf (<:-λ _ Λj₁a₂∈Πjk _) σ∈Γ = Tp∈-/-wf Λj₁a₂∈Πjk σ∈Γ
    <:-/-wf (<:-· a₁<:a₂∈Πjk _ _ _ _) σ∈Γ = <:-/-wf a₁<:a₂∈Πjk σ∈Γ
    <:-/-wf (<:-⟨| a∈b⋯c)        σ∈Γ = Tp∈-/-wf a∈b⋯c σ∈Γ
    <:-/-wf (<:-|⟩ a∈b⋯c)        σ∈Γ = Tp∈-/-wf a∈b⋯c σ∈Γ
    <:-/-wf (<:-⋯-i a<:b∈c⋯d)    σ∈Γ = <:-/-wf a<:b∈c⋯d σ∈Γ
    <:-/-wf (<:-⇑ a<:b∈k _)      σ∈Γ = <:-/-wf a<:b∈k σ∈Γ

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

  -- Substitutions preserve well-formedness of ascriptions.
  wf-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a σ} →
         Γ ⊢ a wf → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A.TermAsc/ σ wf
  wf-/ (wf-kd k-kd) σ∈Γ = wf-kd (kd-/ k-kd σ∈Γ)
  wf-/ (wf-tp a∈b)  σ∈Γ = wf-tp (Tp∈-/ a∈b σ∈Γ)

  -- Substitutions commute with kind equality.
  ≅-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k σ} →
        Γ ⊢ j ≅ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ j A.Kind/ σ ≅ k A.Kind/ σ
  ≅-/ (<∷-antisym j<∷k k<∷j) σ∈Γ = <∷-antisym (<∷-/ j<∷k σ∈Γ) (<∷-/ k<∷j σ∈Γ)

  -- Substitutions preserve well-kindedness and well-typedness.
  ∈-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b σ} →
        Γ ⊢ a ∈ b → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A./ σ ∈ b A.TermAsc/ σ
  ∈-/ (∈-tp a∈b)                σ∈Γ = ∈-tp (Tp∈-/ a∈b σ∈Γ)
  ∈-/ (∈-var x Γ-ctx Γ[x]≡tp-a) σ∈Γ =
    subst (_ ⊢ _ ∈_) (cong (A._TermAsc/ _) Γ[x]≡tp-a)
          (∈-lift (/∈-lookup σ∈Γ x))

  -- Substitutions preserve type and syntactic term equality.
  ≃⊎≡-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b c σ} →
          Γ ⊢ a ≃⊎≡ b ∈ c → Δ ⊢/ σ ∈ Γ →
          Δ ⊢ a A./ σ ≃⊎≡ b A./ σ ∈ c A.TermAsc/ σ
  ≃⊎≡-/ (≃-tp a≃b∈k) σ∈Γ              = ≃-tp (≃-/ a≃b∈k σ∈Γ)
  ≃⊎≡-/ (≃-var x Γ-ctx Γ[x]≡tp-a) σ∈Γ =
    let x/σ∈tp-a/σ = subst (_ ⊢ _ ∈_) (cong (A._TermAsc/ _) Γ[x]≡tp-a)
                           (∈-lift (/∈-lookup σ∈Γ x))
    in ≃⊎≡-refl x/σ∈tp-a/σ

-- Well-kinded type substitutions.
module KindedSubstitution where
  open Substitution           using (simple; termSubst)
  open SimpleExt    simple    using (extension)
  open TermSubst    termSubst using (varLift; termLift)

  private
    module S  = Substitution
    module KL = TermLikeLemmas S.termLikeLemmasKind

  -- Helper lemmas about untyped renamings and substitutions in terms
  -- and kinds.

  varHelpers : TypedSubstAppHelpers varLift
  varHelpers = record
    { Kind/-sub-↑ = KL./-sub-↑
    ; /-sub-↑     = LiftSubLemmas./-sub-↑ S.varLiftSubLemmas
    ; weaken-/    = LiftAppLemmas.wk-commutes S.varLiftAppLemmas
    }

  termHelpers : TypedSubstAppHelpers termLift
  termHelpers = record
    { Kind/-sub-↑ = λ k _ _ → KL.sub-commutes k
    ; /-sub-↑     = λ a _ _ → S.sub-commutes a
    ; weaken-/    = S.weaken-/
    }

  -- Kinded type substitutions.

  typedTermSubst : TypedTermSubst TermAsc Term Level.zero TypedSubstAppHelpers
  typedTermSubst = record
    { _⊢_wf = _⊢_wf
    ; _⊢_∈_ = _⊢_∈_
    ; termLikeLemmas = S.termLikeLemmasTermAsc
    ; varHelpers     = varHelpers
    ; termHelpers    = termHelpers
    ; wf-wf    = wf-ctx
    ; ∈-wf     = ∈-ctx
    ; ∈-var    = ∈-var′
    ; typedApp = TypedSubstApp.∈-/
    }
  open TypedTermSubst typedTermSubst public
    hiding (_⊢_wf; _⊢_∈_; varHelpers; termHelpers; ∈-var; ∈-/Var; ∈-/)
    renaming (lookup to /∈-lookup)
  open TypedSubstApp _⊢Var_∈_ varLiftTyped varHelpers public using () renaming
    ( wf-/  to wf-/Var
    ; kd-/  to kd-/Var
    ; Tp∈-/ to Tp∈-/Var
    ; <∷-/  to <∷-/Var
    ; <:-/  to <:-/Var
    ; ∈-/   to ∈-/Var
    ; ≃⊎≡-/ to ≃⊎≡-/Var
    )
  open Substitution using (weaken; weakenKind; weakenTermAsc)

  -- Weakening preserves the various judgments.

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

  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 (Var∈-wk a-wf)

  Tp∈-weaken : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a wf → Γ ⊢Tp b ∈ k →
               (a ∷ Γ) ⊢Tp weaken b ∈ weakenKind k
  Tp∈-weaken a-wf b∈k = Tp∈-/Var b∈k (Var∈-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 (Var∈-wk a-wf)

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

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

  -- Weakening preserves type and syntactic term equality.
  ≃⊎≡-weaken : ∀ {n} {Γ : Ctx n} {a b c d} → Γ ⊢ a wf → Γ ⊢ b ≃⊎≡ c ∈ d →
               (a ∷ Γ) ⊢ weaken b ≃⊎≡ weaken c ∈ weakenTermAsc d
  ≃⊎≡-weaken a-wf b≃⊎≡c∈d = ≃⊎≡-/Var b≃⊎≡c∈d (Var∈-wk a-wf)

  open TypedSubstApp _⊢_∈_ termLiftTyped termHelpers public
  open Substitution using (_/_; _Kind/_; id; sub; _↑⋆_; _[_]; _Kind[_])

  -- Substitution of a single well-typed term or well-kinded type
  -- preserves the various judgments.

  kd-[] : ∀ {n} {Γ : Ctx n} {a b k} →
          b ∷ Γ ⊢ k kd → Γ ⊢ a ∈ b → Γ ⊢ k Kind[ a ] kd
  kd-[] k-kd a∈b = kd-/ k-kd (∈-sub a∈b)

  ≅-[] : ∀ {n} {Γ : Ctx n} {j k a b} →
         b ∷ Γ ⊢ j ≅ k → Γ ⊢ a ∈ b → Γ ⊢ j Kind[ a ] ≅ k Kind[ a ]
  ≅-[] j≅k a∈b = ≅-/ j≅k (∈-sub a∈b)

  Tp∈-[] : ∀ {n} {Γ : Ctx n} {a b k c} →
           c ∷ Γ ⊢Tp a ∈ k → Γ ⊢ b ∈ c → Γ ⊢Tp a [ b ] ∈ k Kind[ b ]
  Tp∈-[] a∈k b∈c = Tp∈-/ a∈k (∈-sub b∈c)

  -- Context narrowing.

  -- A typed substitution that narrows the kind of the first type
  -- variable.
  ∈-<∷-sub : ∀ {n} {Γ : Ctx n} {j k} →
             Γ ⊢ j kd → Γ ⊢ j <∷ k → kd j ∷ Γ ⊢/ id ∈ kd k ∷ Γ
  ∈-<∷-sub j-kd j<∷k =
    ∈-tsub (∈-tp (∈-⇑ (∈-var zero (j-wf ∷ Γ-ctx) refl) (<∷-weaken j-wf j<∷k)))
    where
      j-wf  = wf-kd j-kd
      Γ-ctx = kd-ctx j-kd

  -- 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-/ k-kd (∈-<∷-sub j₁-kd j₁<∷j₂))

  -- Narrowing the kind of the first type variable preserves
  -- well-kindedness.
  ⇓-Tp∈ : ∀ {n} {Γ : Ctx n} {j₁ j₂ a k} →
          Γ ⊢ j₁ kd → Γ ⊢ j₁ <∷ j₂ → kd j₂ ∷ Γ ⊢Tp a ∈ k → kd j₁ ∷ Γ ⊢Tp a ∈ k
  ⇓-Tp∈ j₁-kd j₁<∷j₂ a∈k =
    subst₂ (_ ⊢Tp_∈_) (S.id-vanishes _) (KL.id-vanishes _)
           (Tp∈-/ a∈k (∈-<∷-sub j₁-kd j₁<∷j₂))

  -- 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 _)
           (<∷-/ k₁<∷k₂ (∈-<∷-sub j₁-kd j₁<∷j₂))

  ⇓-<: : ∀ {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₂ (_ ⊢_<:_∈ _) (S.id-vanishes _) (S.id-vanishes _)
                  (<:-/ a₁<:a₂∈k (∈-<∷-sub j₁-kd j₁<∷j₂)))

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

module WfCtxOps where
  wfWeakenOps : WellFormedWeakenOps weakenOps
  wfWeakenOps = record { wf-weaken = KindedSubstitution.wf-weaken }

  open WellFormedWeakenOps wfWeakenOps public 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 → TermCtx.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 KindedSubstitution
open WfCtxOps

-- Transitivity of subkinding.
<∷-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₃ Πj₂k₂-kd) =
  <∷-Π (<∷-trans j₃<∷j₂ j₂<∷j₁)
       (<∷-trans (⇓-<∷ (wf-kd-inv (wf-∷₁ (<∷-ctx k₂<∷k₃))) j₃<∷j₂ k₁<∷k₂)
                 k₂<∷k₃)
       Πj₁k₁-kd

-- Transitivity of kind equality.
≅-trans : ∀ {n} {Γ : Ctx n} {j k l} → Γ ⊢ j ≅ k → Γ ⊢ k ≅ l → Γ ⊢ j ≅ l
≅-trans (<∷-antisym k₁<∷k₂ k₂<∷k₁) (<∷-antisym k₂<∷k₃ k₃<∷k₂) =
  <∷-antisym (<∷-trans k₁<∷k₂ k₂<∷k₃) (<∷-trans k₃<∷k₂ k₂<∷k₁)

----------------------------------------------------------------------
-- Well-formed equality lifted to substitutions

module WfSubstitutionEquality where
  open Substitution        hiding (subst)
  open TermSubst termSubst using  (termLift)
  open ZipUnzipSimple simple simple
  open TypedSubstAppHelpers KindedSubstitution.termHelpers
  private
    module KL = TermLikeLemmas termLikeLemmasKind
    module AL = TermLikeLemmas termLikeLemmasTermAsc
    module S  = SimpleExt simple
    module Z  = SimpleExt zippedSimple

  -- Well-formed equal substitutions: pairs of substitutions that are
  -- point-wise equal.

  wfEqSub : TypedSubRel TermAsc Term Level.zero
  wfEqSub = record
    { typedRelation       = record { _⊢_wf = _⊢_wf ; _⊢_∼_∈_ = _⊢_≃⊎≡_∈_ }
    ; typeExtension       = TermCtx.weakenOps
    ; typeTermApplication = record { _/_ = λ a ρσ → a TermAsc/ (π₁ ρσ) }
    ; termSimple          = simple
    }
  open TypedSubRel wfEqSub public using ()
    renaming (_⊢/_∼_∈_ to _⊢/_≃_∈_)

  -- Simple substitutions of well-formed equal terms and types.

  wfEqWeakenOps : TypedRelWeakenOps wfEqSub
  wfEqWeakenOps = record
    { ∼∈-weaken  = ≃⊎≡-weaken
    ; ∼∈-wf      = ≃⊎≡-ctx
    ; /-wk       = /-wk-π₁
    ; /-weaken   = λ {m} {n} {στ} a → /-weaken-π₁ {m} {n} {στ} a
    ; weaken-/-∷ = AL.weaken-/-∷
    }
    where
      open ≡-Reasoning

      /-wk-π₁ : ∀ {n} {a : TermAsc n} → a TermAsc/ π₁ Z.wk ≡ weakenTermAsc a
      /-wk-π₁ {_} {a} = begin
        a TermAsc/ π₁ Z.wk   ≡⟨ cong ((a TermAsc/_) ∘ proj₁) (sym wk-unzip) ⟩
        a TermAsc/ wk        ≡⟨ AL./-wk ⟩
        weakenTermAsc a      ∎

      /-weaken-π₁ : ∀ {m n} {στ : Sub (Term ⊗ Term) m n} a →
                    a TermAsc/ π₁ (Vec.map Z.weaken στ) ≡
                      a TermAsc/ π₁ στ TermAsc/ π₁ Z.wk
      /-weaken-π₁ {_} {_} {στ} a = begin
          a TermAsc/ π₁ (Vec.map Z.weaken στ)
        ≡˘⟨ cong ((a TermAsc/_) ∘ proj₁) (map-weaken-unzip στ) ⟩
          a TermAsc/ Vec.map S.weaken (π₁ στ)
        ≡⟨ AL./-weaken a ⟩
          a TermAsc/ π₁ στ TermAsc/ S.wk
        ≡⟨ cong ((a TermAsc/ π₁ στ TermAsc/_) ∘ proj₁) wk-unzip ⟩
          a TermAsc/ π₁ στ TermAsc/ π₁ Z.wk
        ∎

  wfEqSimple : TypedRelSimple wfEqSub
  wfEqSimple = record
    { typedRelWeakenOps = wfEqWeakenOps
    ; ∼∈-var            = ≃⊎≡-var
    ; wf-wf             = wf-ctx
    ; id-vanishes       = id-vanishes-π₁
    }
    where
      open TypedRelWeakenOps wfEqWeakenOps
      open ≡-Reasoning

      id-vanishes-π₁ : ∀ {n} (a : TermAsc n) → a TermAsc/ π₁ Z.id ≡ a
      id-vanishes-π₁ a = begin
        a TermAsc/ π₁ Z.id   ≡⟨ cong ((a TermAsc/_) ∘ proj₁) (sym id-unzip) ⟩
        a TermAsc/ id        ≡⟨ AL.id-vanishes a ⟩
        a                    ∎

  open TypedRelSimple wfEqSimple public
    hiding (typedRelWeakenOps; ∼∈-var; ∼∈-weaken; ∼∈-wf; wf-wf)
    renaming (lookup to ≃-lookup)

  infixl 4  _⊢/_≃′_∈_

  -- An inversion lemma for the generic term/type equality.
  ≃⊎≡-kd-inv : ∀ {n} {Γ : Ctx n} {a b k kd-k} →
               kd-k ≡ kd k → Γ ⊢ a ≃⊎≡ b ∈ kd-k → Γ ⊢ a ≃ b ∈ k
  ≃⊎≡-kd-inv refl (≃-tp a≃b∈k) = a≃b∈k

  -- A shorthand.
  --
  -- TODO: explain why we use this particular representation of equal
  -- substitutions here.
  _⊢/_≃′_∈_ : ∀ {m n} → Ctx n → Sub Term m n → Sub Term m n → Ctx m → Set
  Δ ⊢/ σ ≃′ ρ ∈ Γ = Δ ⊢/ σ ∈ Γ × Δ ⊢/ ρ ∈ Γ × Δ ⊢/ σ ≃ ρ ∈ Γ × Δ ⊢/ ρ ≃ σ ∈ Γ

  -- Symmetry of substitution equality.
  ≃′-sym : ∀ {m n Δ Γ} {ρ σ : Sub Term m n} → Δ ⊢/ ρ ≃′ σ ∈ Γ → Δ ⊢/ σ ≃′ ρ ∈ Γ
  ≃′-sym (ρ∈Γ , σ∈Γ , ρ≃σ∈Γ , σ≃ρ∈Γ) = σ∈Γ , ρ∈Γ , σ≃ρ∈Γ , ρ≃σ∈Γ

  -- Lift a pair of equal substitutions over an additional type
  -- variable.
  ≃′-↑ : ∀ {m n Γ Δ} {ρ σ : Sub Term m n} {j k} →
         Δ ⊢ j kd → Δ ⊢ j ≅ k Kind/ ρ → Δ ⊢ j ≅ k Kind/ σ → Δ ⊢/ ρ ≃′ σ ∈ Γ →
         kd j ∷ Δ ⊢/ ρ ↑ ≃′ σ ↑ ∈ kd k ∷ Γ
  ≃′-↑ j-kd j≅k/ρ j≅k/σ (ρ∈Γ , σ∈Γ , ρ≃σ∈ , σ≃ρ∈) =
    ∈-/∷ (∈-tp z∈k/ρ) ρ∈Γ , ∈-/∷ (∈-tp z∈k/σ) σ∈Γ ,
    ∼∈-/∷ (≃-tp (≃-refl z∈k/ρ′)) ρ≃σ∈ , ∼∈-/∷ (≃-tp (≃-refl z∈k/σ′)) σ≃ρ∈
    where
      j-wf    = wf-kd j-kd
      j∷Δ-ctx = j-wf ∷ kd-ctx j-kd
      z∈k/ρ   = ∈-⇑ (∈-var zero j∷Δ-ctx refl) (<∷-weaken j-wf (≅⇒<∷ j≅k/ρ))
      z∈k/σ   = ∈-⇑ (∈-var zero j∷Δ-ctx refl) (<∷-weaken j-wf (≅⇒<∷ j≅k/σ))
      z∈k/ρ′  = subst (_ ⊢Tp _ ∈_)
                      (cong (weakenKind ∘ (_ Kind/_)) (sym (π₁-zip _ _))) z∈k/ρ
      z∈k/σ′  = subst (_ ⊢Tp _ ∈_)
                      (cong (weakenKind ∘ (_ Kind/_)) (sym (π₁-zip _ _))) z∈k/σ

  -- Lemmas about equal substitutions (weak versions).

  mutual

    -- Equal substitutions map well-formed kinds to kind equations.
    kd-/≃ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {k ρ σ} →
            Γ ⊢ k kd → Δ ⊢/ ρ ≃′ σ ∈ Γ → Δ ⊢ k Kind/ ρ ≅ k Kind/ σ
    kd-/≃ (kd-⋯ a∈* b∈*)   ρ≃σ∈Γ = ≅-⋯ (Tp∈-/≃ a∈* ρ≃σ∈Γ) (Tp∈-/≃ b∈* ρ≃σ∈Γ)
    kd-/≃ (kd-Π j-kd k-kd) ρ≃σ∈Γ =
      let ρ∈Γ , σ∈Γ , _ = ρ≃σ∈Γ
          j/ρ-kd  = kd-/ j-kd ρ∈Γ
          j/σ-kd  = kd-/ j-kd σ∈Γ
          j/ρ≅j/σ = kd-/≃ j-kd ρ≃σ∈Γ
          k/ρ≅k/σ = kd-/≃ k-kd
                          (≃′-↑ j/σ-kd (≅-sym j/ρ≅j/σ) (≅-refl j/σ-kd) ρ≃σ∈Γ)
          k/σ≅k/ρ = kd-/≃ k-kd
                          (≃′-↑ j/ρ-kd j/ρ≅j/σ (≅-refl j/ρ-kd) (≃′-sym ρ≃σ∈Γ))
          Πjk/ρ-kd = kd-/ (kd-Π j-kd k-kd) ρ∈Γ
          Πjk/σ-kd = kd-/ (kd-Π j-kd k-kd) σ∈Γ
      in <∷-antisym (<∷-Π (≅⇒<∷ (≅-sym j/ρ≅j/σ)) (≅⇒<∷ k/ρ≅k/σ) Πjk/ρ-kd)
                    (<∷-Π (≅⇒<∷ j/ρ≅j/σ) (≅⇒<∷ k/σ≅k/ρ) Πjk/σ-kd)

    -- Equal substitutions map well-kinded types to type equations.
    Tp∈-/≃ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a k ρ σ} →
             Γ ⊢Tp a ∈ k → Δ ⊢/ ρ ≃′ σ ∈ Γ → Δ ⊢ a / ρ ≃ a / σ ∈ k Kind/ ρ
    Tp∈-/≃ {ρ = ρ} {σ} (∈-var x Γ-ctx Γ[x]≡kd-k) (_ , _ , ρ≃σ∈Γ , _) =
      (≃⊎≡-kd-inv (cong (_TermAsc/ ρ) Γ[x]≡kd-k)
                  (subst (_ ⊢ _ ≃⊎≡ _ ∈_)
                         (cong (_ TermAsc/_) (π₁-zip ρ σ))
                         (≃-lookup ρ≃σ∈Γ x)))
    Tp∈-/≃ (∈-⊥-f Γ-ctx) (ρ∈Γ , _) = ≃-refl (∈-⊥-f (/∈-wf ρ∈Γ))
    Tp∈-/≃ (∈-⊤-f Γ-ctx) (ρ∈Γ , _) = ≃-refl (∈-⊤-f (/∈-wf ρ∈Γ))
    Tp∈-/≃ (∈-∀-f k-kd a∈*) ρ≃σ∈Γ =
      let ρ∈Γ , σ∈Γ , _ = ρ≃σ∈Γ
          k/ρ-kd    = kd-/ k-kd ρ∈Γ
          k/σ-kd    = kd-/ k-kd σ∈Γ
          k/ρ≅k/σ   = kd-/≃ k-kd ρ≃σ∈Γ
          a/ρ≃a/σ∈* = Tp∈-/≃ a∈* (≃′-↑ k/σ-kd (≅-sym k/ρ≅k/σ)
                                       (≅-refl k/σ-kd) ρ≃σ∈Γ)
          a/σ≃a/ρ∈* = Tp∈-/≃ a∈* (≃′-↑ k/ρ-kd k/ρ≅k/σ
                                       (≅-refl k/ρ-kd) (≃′-sym ρ≃σ∈Γ))
          ∀ka/ρ∈*   = Tp∈-/ (∈-∀-f k-kd a∈*) ρ∈Γ
          ∀ka/σ∈*   = Tp∈-/ (∈-∀-f k-kd a∈*) σ∈Γ
      in <:-antisym (<:-∀ (≅⇒<∷ (≅-sym k/ρ≅k/σ)) (≃⇒<: a/ρ≃a/σ∈*) ∀ka/ρ∈*)
                    (<:-∀ (≅⇒<∷ k/ρ≅k/σ) (≃⇒<: a/σ≃a/ρ∈*) ∀ka/σ∈*)
    Tp∈-/≃ (∈-→-f a∈* b∈*) ρ≃σ∈Γ = ≃-→ (Tp∈-/≃ a∈* ρ≃σ∈Γ) (Tp∈-/≃ b∈* ρ≃σ∈Γ)
    Tp∈-/≃ (∈-Π-i j-kd a∈k k-kd) ρ≃σ∈Γ =
      let ρ∈Γ , σ∈Γ , _ = ρ≃σ∈Γ
          j/ρ-kd        = kd-/ j-kd ρ∈Γ
          j/σ-kd        = kd-/ j-kd σ∈Γ
          j/ρ≅j/σ       = kd-/≃ j-kd ρ≃σ∈Γ
          ρ↑∈j∷Γ        = ∈-↑ (wf-kd j/ρ-kd) ρ∈Γ
          σ↑∈j∷Γ        = ∈-↑ (wf-kd j/σ-kd) σ∈Γ
          ρ↑≃σ↑∈j∷Γ     = ≃′-↑ j/ρ-kd (≅-refl j/ρ-kd) j/ρ≅j/σ ρ≃σ∈Γ
          a/ρ∈k/ρ       = Tp∈-/ a∈k ρ↑∈j∷Γ
          a/σ∈k/σ       = Tp∈-/ a∈k σ↑∈j∷Γ
          a/ρ≃a/σ∈k/ρ   = Tp∈-/≃ a∈k ρ↑≃σ↑∈j∷Γ
          k/ρ-kd        = kd-/ k-kd ρ↑∈j∷Γ
          k/σ-kd        = kd-/ k-kd σ↑∈j∷Γ
          k/ρ≅k/σ       = kd-/≃ k-kd ρ↑≃σ↑∈j∷Γ
          Λja/ρ∈Πjk/ρ   = ∈-Π-i j/ρ-kd a/ρ∈k/ρ k/ρ-kd
          Πjk/σ<∷Πjk/ρ  = <∷-Π (≅⇒<∷ j/ρ≅j/σ) (≅⇒<∷ (≅-sym k/ρ≅k/σ))
                               (kd-Π j/σ-kd k/σ-kd)
          Λja/σ∈Πjk/ρ   = ∈-⇑ (∈-Π-i j/σ-kd a/σ∈k/σ k/σ-kd) Πjk/σ<∷Πjk/ρ
      in ≃-λ a/ρ≃a/σ∈k/ρ Λja/ρ∈Πjk/ρ Λja/σ∈Πjk/ρ
    Tp∈-/≃ (∈-Π-e {k = k} a∈Πjk b∈j k-kd k[b]-kd) ρ≃σ∈Γ =
      let k[b]/ρ≡k/ρ[b/ρ] = Kind/-sub-↑ k _ _
          k[b]/σ≡k/σ[b/σ] = Kind/-sub-↑ k _ _
          ρ∈Γ , σ∈Γ , _ = ρ≃σ∈Γ
          j-wf          = wf-∷₁ (kd-ctx k-kd)
          j-kd          = wf-kd-inv j-wf
          j/σ≅j/ρ       = kd-/≃-≅ k-kd (≃′-sym ρ≃σ∈Γ)
          j/σ-kd        = kd-/ j-kd σ∈Γ
          ρ↑≃σ↑∈j∷Γ     = ≃′-↑ j/σ-kd j/σ≅j/ρ (≅-refl j/σ-kd) ρ≃σ∈Γ
          ρ↑∈j∷Γ        = (∈-↑ (wf-/ j-wf ρ∈Γ) ρ∈Γ)
          a/ρ≃a/σ∈Πjk/ρ = Tp∈-/≃ a∈Πjk ρ≃σ∈Γ
          b/ρ≃b/σ∈j/ρ   = Tp∈-/≃ b∈j   ρ≃σ∈Γ
          k[b]/ρ≅k[b]/σ = kd-/≃ k[b]-kd ρ≃σ∈Γ
          k/ρ≅k/σ       = kd-/≃ k-kd ρ↑≃σ↑∈j∷Γ
          b/ρ∈j/ρ   = Tp∈-/ b∈j ρ∈Γ
          b/σ∈j/σ   = Tp∈-/ b∈j σ∈Γ
          b/σ∈j/ρ   = ∈-⇑ b/σ∈j/σ (≅⇒<∷ j/σ≅j/ρ)
          k/ρ-kd    = kd-/ k-kd ρ↑∈j∷Γ
          k/ρ[b/ρ]-kd = subst (_ ⊢_kd) k[b]/ρ≡k/ρ[b/ρ] (kd-/ k[b]-kd ρ∈Γ)
          k/ρ[b/σ]-kd = kd-[] k/ρ-kd (∈-tp b/σ∈j/ρ)
          k/ρ[b/σ]≅k[b]/σ = subst (_ ⊢ (k Kind/ _) Kind[ _ ] ≅_)
                                  (sym k[b]/σ≡k/σ[b/σ])
                                  (≅-[] k/ρ≅k/σ (∈-tp b/σ∈j/σ))
          k[b]/σ≅k/ρ[b/ρ] = subst (_ ⊢ _ ≅_) k[b]/ρ≡k/ρ[b/ρ]
                                  (≅-sym k[b]/ρ≅k[b]/σ)
          k/ρ[b/σ]≅k/ρ[b/ρ] = ≅-trans k/ρ[b/σ]≅k[b]/σ k[b]/σ≅k/ρ[b/ρ]
      in (subst (_ ⊢ _ ≃ _ ∈_) (sym k[b]/ρ≡k/ρ[b/ρ])
                (<:-antisym (<:-· (≃⇒<: a/ρ≃a/σ∈Πjk/ρ) b/ρ≃b/σ∈j/ρ b/ρ∈j/ρ
                                  k/ρ-kd k/ρ[b/ρ]-kd)
                            (<:-⇑ (<:-· (≃⇒<: (≃-sym a/ρ≃a/σ∈Πjk/ρ))
                                        (≃-sym b/ρ≃b/σ∈j/ρ) b/σ∈j/ρ k/ρ-kd
                                        k/ρ[b/σ]-kd)
                                  (≅⇒<∷ k/ρ[b/σ]≅k/ρ[b/ρ]))))
    Tp∈-/≃ (∈-s-i a∈b⋯d) ρ≃σ∈Γ =
      let ρ∈Γ , σ∈Γ , _    = ρ≃σ∈Γ
          a/ρ∈*            = Tp∈-⋯-* (Tp∈-/ a∈b⋯d ρ∈Γ)
          a/σ∈*            = Tp∈-⋯-* (Tp∈-/ a∈b⋯d σ∈Γ)
          a/ρ≃a/σ∈b/ρ⋯d/ρ  = Tp∈-/≃ a∈b⋯d ρ≃σ∈Γ
          a/ρ<:a/σ∈a/ρ⋯a/σ = <:-⋯-i (≃⇒<: a/ρ≃a/σ∈b/ρ⋯d/ρ)
          a/σ<:a/ρ∈a/σ⋯a/ρ = <:-⋯-i (≃⇒<: (≃-sym a/ρ≃a/σ∈b/ρ⋯d/ρ))
          a/ρ<:a/σ∈*       = <:-⇑ a/ρ<:a/σ∈a/ρ⋯a/σ
                                  (<∷-⋯ (<:-⊥ a/ρ∈*) (<:-⊤ a/σ∈*))
          a/σ<:a/ρ∈*       = <:-⇑ a/σ<:a/ρ∈a/σ⋯a/ρ
                                  (<∷-⋯ (<:-⊥ a/σ∈*) (<:-⊤ a/ρ∈*))
          a/ρ<:a/σ∈a/ρ⋯a/ρ = <:-⇑ a/ρ<:a/σ∈a/ρ⋯a/σ
                                  (<∷-⋯ (<:-refl a/ρ∈*) a/σ<:a/ρ∈*)
          a/σ<:a/ρ∈a/ρ⋯a/ρ = <:-⇑ a/σ<:a/ρ∈a/σ⋯a/ρ
                                  (<∷-⋯ a/ρ<:a/σ∈* (<:-refl a/ρ∈*))
      in <:-antisym a/ρ<:a/σ∈a/ρ⋯a/ρ a/σ<:a/ρ∈a/ρ⋯a/ρ
    Tp∈-/≃ (∈-⇑ a∈j j<∷k) ρ≃σ∈Γ =
      ≃-⇑ (Tp∈-/≃ a∈j ρ≃σ∈Γ) (<∷-/ j<∷k (proj₁ ρ≃σ∈Γ))

    -- Helpers (to satisfy the termination checker).

    kd-/≃-≅ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k ρ σ} →
              kd j ∷ Γ ⊢ k kd → Δ ⊢/ ρ ≃′ σ ∈ Γ → Δ ⊢ j Kind/ ρ ≅ j Kind/ σ
    kd-/≃-≅ (kd-⋯ a∈* _)  ρ≃σ∈Γ = Tp∈-/≃-≅ a∈* ρ≃σ∈Γ
    kd-/≃-≅ (kd-Π j-kd _) ρ≃σ∈Γ = kd-/≃-≅ j-kd ρ≃σ∈Γ

    Tp∈-/≃-≅ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a j k ρ σ} →
               kd j ∷ Γ ⊢Tp a ∈ k → Δ ⊢/ ρ ≃′ σ ∈ Γ → Δ ⊢ j Kind/ ρ ≅ j Kind/ σ
    Tp∈-/≃-≅ (∈-var x (wf-kd k-kd ∷ Γ-ctx) _) ρ≃σ∈Γ = kd-/≃ k-kd ρ≃σ∈Γ
    Tp∈-/≃-≅ (∈-⊥-f (wf-kd k-kd ∷ Γ-ctx))     ρ≃σ∈Γ = kd-/≃ k-kd ρ≃σ∈Γ
    Tp∈-/≃-≅ (∈-⊤-f (wf-kd k-kd ∷ Γ-ctx))     ρ≃σ∈Γ = kd-/≃ k-kd ρ≃σ∈Γ
    Tp∈-/≃-≅ (∈-∀-f k-kd _)                   ρ≃σ∈Γ = kd-/≃-≅ k-kd ρ≃σ∈Γ
    Tp∈-/≃-≅ (∈-→-f a∈* _)                    ρ≃σ∈Γ = Tp∈-/≃-≅ a∈* ρ≃σ∈Γ
    Tp∈-/≃-≅ (∈-Π-i j-kd _ _)                 ρ≃σ∈Γ = kd-/≃-≅ j-kd ρ≃σ∈Γ
    Tp∈-/≃-≅ (∈-Π-e a∈Πjk _ _ _)              ρ≃σ∈Γ = Tp∈-/≃-≅ a∈Πjk ρ≃σ∈Γ
    Tp∈-/≃-≅ (∈-s-i a∈b⋯c)                    ρ≃σ∈Γ = Tp∈-/≃-≅ a∈b⋯c ρ≃σ∈Γ
    Tp∈-/≃-≅ (∈-⇑ a∈k _)                      ρ≃σ∈Γ = Tp∈-/≃-≅ a∈k ρ≃σ∈Γ

  -- Functionality of kind formation and kinding.

  -- Equal single-variable substitutions map well-formed kinds to kind
  -- equations (weak version).
  kd-[≃′] : ∀ {n} {Γ : Ctx n} {a b j k} →
            kd j ∷ Γ ⊢ k kd → Γ ⊢Tp a ∈ j → Γ ⊢Tp b ∈ j → Γ ⊢ a ≃ b ∈ j →
            Γ ⊢ k Kind[ a ] ≅ k Kind[ b ]
  kd-[≃′] k-kd a∈j b∈j a≃b∈j =
    kd-/≃ k-kd (∈-sub (∈-tp a∈j) , ∈-sub (∈-tp b∈j) ,
                ∼∈-sub (≃-tp a≃b∈j) , ∼∈-sub (≃-tp (≃-sym (a≃b∈j))))

  -- Equal single-variable substitutions map well-kinded types to type
  -- equations (weak version).
  Tp∈-[≃′] : ∀ {n} {Γ : Ctx n} {a b c j k} →
             kd j ∷ Γ ⊢Tp a ∈ k → Γ ⊢Tp b ∈ j → Γ ⊢Tp c ∈ j → Γ ⊢ b ≃ c ∈ j →
             Γ ⊢ a [ b ] ≃ a [ c ] ∈ k Kind[ b ]
  Tp∈-[≃′] a∈k b∈j c∈j b≃c∈j =
    Tp∈-/≃ a∈k (∈-sub (∈-tp b∈j) , ∈-sub (∈-tp c∈j) ,
                ∼∈-sub (≃-tp b≃c∈j) , ∼∈-sub (≃-tp (≃-sym (b≃c∈j))))


text:
open import Prelude
open import Container.List

open import Ataca.Utils
open import Ataca.Core
open import Ataca.Tactics

module Ataca.Demo where

test₁ : Nat
test₁ = {! exact 42 !}

test₂ : Nat → Bool → Nat
test₂ x y = {! assumption !}

test₃ : Nat → Bool → Bool
test₃ x y = {! assumption !}

test₄ : Nat → Bool → Nat
test₄ = {! intros !}

test₅ : Bool
test₅ = {! introConstructor !}

test₆ : Nat
test₆ = {! introConstructor !}

test₇ : _≡_ {A = Bool} true true
test₇ = {! introConstructor !}

test₈ : Vec Nat 0
test₈ = {! introConstructor!}

test₉ : Vec Bool 3
test₉ = {! introConstructors !}

test₁₀ : {A : Set} → A → Vec A 5
test₁₀ = {! mini-auto !}

data DecrVec (n : Nat) : Nat → Set where
  []   : DecrVec n zero
  cons : ∀ {k} → (m : Nat) → m < n → DecrVec m k → DecrVec n (suc k)

test₁₁ : DecrVec 4 3
test₁₁ = {! mini-auto !}

test₁₂ : Any {A = Nat} (_≡ 1) (zero ∷ (suc zero) ∷ [])
test₁₂ = {! mini-auto !}

postulate
  X Y : Set
  fun : X → Y

test₁₃ : X → Y
test₁₃ = {! mini-auto-with hints !}
  where
    hints : Hints
    hints = def (quote fun) [] ∷ []

test₁₄ : {A : Set} → ⊥ → A
test₁₄ = {! mini-auto !}

test₁₅ : (x : Nat) → Either (x ≡ 0) (Σ Nat λ y → x ≡ suc y)
test₁₅ x = {! destruct x !}

postulate
  P=NP : Set

proof : P=NP
proof = run do
  try mini-auto'
  admit'

ext: agda

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module NaturalTransFacts where

open import Level
open import Categories.Support.Equivalence
open import Categories.Category
open import Categories.Functor
open import Categories.NaturalTransformation
  renaming (id to natId; _≡_ to _≡N_; setoid to natSetoid)
  hiding (_∘ˡ_; _∘ʳ_)
open import Categories.Support.EqReasoning

_⇒_ = NaturalTransformation

_∘ˡ_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
     → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
     → {F G : Functor C D}
     → (H : Functor D E) → (η : NaturalTransformation F G)
     → (H ∘ F) ⇒ (H ∘ G)
H ∘ˡ η = (natId {F = H}) ∘₀ η

_∘ʳ_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
     → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
     → {F G : Functor C D}
     → (η : NaturalTransformation F G) → (K : Functor E C)
     → (F ∘ K) ⇒ (G ∘ K)
η ∘ʳ K = η ∘₀ (natId {F = K})

.∘₁-resp-≡ˡ : ∀ {o ℓ e} {o′ ℓ′ e′}
               {D : Category o ℓ e} {E : Category o′ ℓ′ e′}
               {A B C : Functor D E}
               {f h : B ⇒ C} {g : A ⇒ B}
            → f ≡N h → f ∘₁ g ≡N h ∘₁ g
∘₁-resp-≡ˡ {f = f} {h} {g} f≡h
  = ∘₁-resp-≡ {f = f} {h} {g} {g} f≡h (Setoid.refl natSetoid {g})

.∘₁-resp-≡ʳ : ∀ {o ℓ e} {o′ ℓ′ e′}
               {D : Category o ℓ e} {E : Category o′ ℓ′ e′}
               {A B C : Functor D E}
               {f : B ⇒ C} {g i : A ⇒ B}
            → g ≡N i → f ∘₁ g ≡N f ∘₁ i
∘₁-resp-≡ʳ {f = f} {g} {i} g≡i
  = ∘₁-resp-≡ {f = f} {f} {g} {i}  (Setoid.refl natSetoid {f}) g≡i

.∘ʳ-distr-∘₁ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
             → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
             → {F G H : Functor C D}
             → (β : G ⇒ H) → (α : F ⇒ G) → (K : Functor E C)
             → (β ∘₁ α) ∘ʳ K ≡N (β ∘ʳ K) ∘₁ (α ∘ʳ K)
∘ʳ-distr-∘₁ {F = F} {G} {H} β α K =
  begin
    (β ∘₁ α) ∘ʳ K
  ↓⟨ Setoid.refl natSetoid {(β ∘₁ α) ∘ʳ K} ⟩
    (β ∘₁ α) ∘₀ idK
  ↑⟨ ∘₀-resp-≡
     {f = (β ∘₁ α)} {(β ∘₁ α)} {idK ∘₁ idK} {idK}
     (Setoid.refl natSetoid {β ∘₁ α})
     (identity₁ʳ {X = idK})
   ⟩
    (β ∘₁ α) ∘₀ (idK ∘₁ idK)
  ↑⟨ interchange {α = β} {idK} {α} {idK} ⟩
    (β ∘₀ idK) ∘₁ (α ∘₀ idK)
  ↓⟨ ∘₁-resp-≡
     {f = β ∘₀ idK} {β ∘ʳ K} {α ∘₀ idK} {α ∘ʳ K}
     (Setoid.refl natSetoid {β ∘₀ idK})
     (Setoid.refl natSetoid {α ∘₀ idK})
   ⟩
    (β ∘ʳ K) ∘₁ (α ∘ʳ K)
  ∎
  where
    open SetoidReasoning (natSetoid {F = F ∘ K} {H ∘ K})
    idK = natId {F = K}

.∘ˡ-distr-∘₁ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
             → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
             → {F G H : Functor C D}
             → (K : Functor D E)
             → (β : G ⇒ H) → (α : F ⇒ G)
             → K ∘ˡ (β ∘₁ α) ≡N (K ∘ˡ β) ∘₁ (K ∘ˡ α)
∘ˡ-distr-∘₁ {F = F} {G} {H} K β α =
  begin
    K ∘ˡ (β ∘₁ α)
  ↓⟨ Setoid.refl natSetoid {K ∘ˡ (β ∘₁ α)} ⟩
    idK ∘₀ (β ∘₁ α)
  ↑⟨ ∘₀-resp-≡
     {f = idK ∘₁ idK} {idK} {(β ∘₁ α)} {(β ∘₁ α)}
     (identity₁ʳ {X = idK})
     (Setoid.refl natSetoid {β ∘₁ α})
   ⟩
    (idK ∘₁ idK) ∘₀ (β ∘₁ α)
  ↑⟨ interchange {α = idK} {β} {idK} {α} ⟩
    (idK ∘₀ β) ∘₁ (idK ∘₀ α)
  ↓⟨ ∘₁-resp-≡
     {f = idK ∘₀ β} {K ∘ˡ β} {idK ∘₀ α} {K ∘ˡ α}
     (Setoid.refl natSetoid {idK ∘₀ β})
     (Setoid.refl natSetoid {idK ∘₀ α})
   ⟩
    (K ∘ˡ β) ∘₁ (K ∘ˡ α)
  ∎
  where
    open SetoidReasoning (natSetoid {F = K ∘ F} {K ∘ H})
    idK = natId {F = K}

.identityNatˡ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
              → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
              → {F : Functor C D}
              → (H : Functor D E)
              → H ∘ˡ natId {F = F} ≡N natId
identityNatˡ H = identity₀ʳ {X = natId {F = H}}

.identityNatʳ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
             → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
             → {F : Functor C D}
             → (K : Functor E C)
             → natId {F = F} ∘ʳ K ≡N natId
identityNatʳ {F = F} K = identity₀ʳ {X = natId {F = F}}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module Data.List.SizeOrdering where

open import Data.List

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import lib.Basics hiding (_⊔_)
open import lib.types.Sigma
open import lib.NType2

open import Preliminaries
open import Truncation_Level_Criteria
open import Anonymous_Existence_CollSplit

open wtrunc
open with-weak-trunc

module Weakly_Constant_Functions where

-- Definition 5.1.1
factorizes-through : ∀ {i j} {X : Type i} {Y : Type j} → Type i → (X → Y) → Type (i ⊔ j)
factorizes-through {X = X} {Y = Y} Z f = Σ (X → Z) λ f₁ → Σ (Z → Y) λ f₂ → (x : X) → f₂ (f₁ x) == f x

-- Definition 5.1.1 addendum: 'factorizes through the truncation'
-- In the theory of the thesis, universes are cumulative.
-- Here, we ask all the types to be in the same universe.
factorizes : ∀ {i} {X : Type i} {Y : Type i} → (X → Y) → Type i
factorizes {X = X} = factorizes-through (∣∣ X ∣∣)

-- Principle 5.2.1
factorize-helper : ∀ {i} {X : Type i} {Y : Type i} → (f : X → Y) → (P : Type i) → (X → is-prop P) → (factorizes-through P f) → factorizes f
factorize-helper {X = X} {Y = Y} f P xpp (f₁ , f₂ , q) = f₁' , f₂' , q' where
  f₁' : X → ∣∣ X ∣∣
  f₁' = ∣_∣

  f₂' : ∣∣ X ∣∣ → Y
  f₂' z = f₂ (tr-rec {X = X} (tr-rec is-prop-is-prop xpp z) f₁ z)

  q' : (x : X) → f₂' (f₁' x) == f x
  q' x =
    f₂' (f₁' x)         =⟨ idp ⟩
    f₂' ∣ x ∣            =⟨ idp ⟩
    f₂ (tr-rec _ f₁ ∣ x ∣ ) =⟨ ap f₂ (trunc-β _ f₁ x) ⟩
    f₂ (f₁ x)           =⟨ q x ⟩
    f x                 ∎

-- Proposition 5.2.2
module st522 {i : ULevel} {X : Type i} {Y : Type i} (f : X → Y) (c : const f) where
  One = ¬ X
  Two = X
  Three = ∣∣ X ∣∣ → X
  Four = coll X
  Five = Y → X

  One→Three : One → Three
  One→Three nx z = Empty-elim {P = λ _ → X} (tr-rec Empty-elim nx z)

  Two→Three : Two → Three
  Two→Three x = λ _ → x

  Five→Four : Five → Four
  Five→Four g = g ∘ f , (λ x₁ x₂ → ap g (c x₁ x₂))

  Three↔Four : Three ↔ Four
  Three↔Four = snd coll↔splitSup , fst coll↔splitSup

  Three→factorizes : Three → factorizes f
  Three→factorizes s = ∣_∣ , f ∘ s , (λ x → c _ _)

-- Proposition 5.2.3 preparation
-- as a small preparation, let us define a function that applies the truncation tr-recursor twice.
-- Because of how we have defined the operator ∣∣_∣∣, we need everything to happen in the same universe
double-tr-rec : ∀ {i} {X₁ X₂ P : Type i} → (is-prop P) → (X₁ → X₂ → P) → ∣∣ X₁ ∣∣ → ∣∣ X₂ ∣∣ → P
double-tr-rec {i} {X₁} {X₂} {P} pp f z₁ z₂ = next-step z₁ z₂ where
  step : X₁ → ∣∣ X₂ ∣∣ → P
  step x₁ = tr-rec {X = X₂} {P = P} pp (f x₁)
  step-switch : ∣∣ X₂ ∣∣ → X₁ → P
  step-switch z₂ x₁ = step x₁ z₂
  next-step : ∣∣ X₁ ∣∣ → ∣∣ X₂ ∣∣ → P
  next-step z₁ z₂ = tr-rec pp (step-switch z₂) z₁ -- tr-rec pp (step-switch z₂)

-- now, the actual Proposition 5.2.3
factorize-codomain-set : ∀ {i} {X : Type i} {Y : Type i} → (f : X → Y) → const f → is-set Y → factorizes f
factorize-codomain-set {i} {X} {Y} f c h = factorize-helper f P (λ _ → pp) fact-through-p where
  P : Type i
  P = Σ Y λ y → ∣∣ (Σ X λ x → f x == y) ∣∣

  pp : is-prop P
  pp = all-paths-is-prop all-paths where
    all-paths : has-all-paths P
    all-paths (y₁ , t₁) (y₂ , t₂) = pair= ys ts where
      ys = double-tr-rec {P = y₁ == y₂} (h _ _) (λ {(x₁ , p₁) (x₂ , p₂) → ! p₁ ∙ c _ _ ∙ p₂}) t₁ t₂
      ts = from-transp _ ys (prop-has-all-paths tr-is-prop _ _)

  fact-through-p : factorizes-through P f
  fact-through-p = f₁ , f₂ , q where
    f₁ : X → P
    f₁ x = f x , ∣ x , idp ∣
    f₂ : P → Y
    f₂ = fst
    q : (x : X) → f₂ (f₁ x) == f x
    q x = idp

-- Theorem 5.2.6
-- We need function extensionality and thus import
-- the following:
open import lib.types.Pi

-- A general auxiliary function which switches the second
-- and third component of a Σ-type with four components
-- (provided that it is possible).
-- We formulate this explicitly as we will need it several times:
switch23 : ∀ {i} {X : Type i} → {Y Z : X → Type i} → {W : (x : X) → (Y x) → (Z x) → Type i} →
  (Σ X λ x → Σ (Y x) λ y → Σ (Z x) λ z → (W x y z)) ≃
  (Σ X λ x → Σ (Z x) λ z → Σ (Y x) λ y → (W x y z))
switch23 = equiv (λ {(y , s , t , coh) → (y , t , s , coh)}) (λ {(y , t , s , coh) → (y , s , t , coh)}) (λ _ → idp) (λ _ → idp)

-- Theorem 5.2.6, with the 'equivalence reasoning' tactic:
module thm526 {i : ULevel} {Q R Y : Type i} (qq : is-prop Q) (rr : is-prop R) (f : Coprod Q R → Y) (c : const f) where

  P : Type i
  P = Σ Y λ y →
        Σ ((q : Q) → y == f(inl q)) λ s →
        Σ ((r : R) → y == f(inr r)) λ t →
          (q : Q) → (r : R) → ! (s q) ∙ (t r) == c (inl q) (inr r)

  -- This is going to be tedious: if q₀ : Q is given, we can show that P is equivalent to the Unit type.
  given-q-reduce-P : Q → P ≃ Unit
  given-q-reduce-P q₀ =

    P

                         ≃⟨ switch23 ⟩

    (Σ Y λ y →
        Σ ((r : R) → y == f(inr r)) λ t →
        Σ ((q : Q) → y == f(inl q)) λ s →
          (q : Q) → (r : R) → ! (s q) ∙ (t r) == c (inl q) (inr r))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → choice ⁻¹)) ⟩

    (Σ Y λ y →
        Σ ((r : R) → y == f(inr r)) λ t →
          (q : Q) → Σ (y == f(inl q)) λ s-reduced →
                      (r : R) → ! s-reduced ∙ (t r) == c (inl q) (inr r))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → Π₁-contr (q₀ , prop-has-all-paths qq q₀))) ⟩

    (Σ Y λ y →
        Σ ((r : R) → y == f(inr r)) λ t →
          Σ (y == f(inl q₀)) λ s-reduced →
            (r : R) → ! s-reduced ∙ (t r) == c (inl q₀) (inr r))

                         ≃⟨ switch23 ⟩

    (Σ Y λ y →
        Σ (y == f(inl q₀)) λ s-reduced →
          Σ ((r : R) → y == f(inr r)) λ t →
            (r : R) → ! s-reduced ∙ (t r) == c (inl q₀) (inr r))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → choice ⁻¹)) ⟩

    (Σ Y λ y →
        Σ (y == f(inl q₀)) λ s-reduced →
          (r : R) → Σ (y == f(inr r)) λ t-reduced →
                       ! s-reduced ∙ t-reduced == c (inl q₀) (inr r))

                         ≃⟨ Σ-assoc ⁻¹ ⟩

    (Σ (Σ Y λ y → (y == f(inl q₀))) λ {(y , s-reduced) →
       (r : R) → Σ (y == f(inr r)) λ t-reduced →
                   ! s-reduced ∙ t-reduced == c (inl q₀) (inr r)})

                         ≃⟨ Σ₁-contr (pathto-is-contr _) ⟩

    ((r : R) → Σ (f(inl q₀) == f(inr r)) λ t-reduced →
                 idp ∙ t-reduced == c (inl q₀) (inr r))

                         ≃⟨ Π₂-contr (λ r → pathto-is-contr _) ⟩

    Unit                 ≃∎

  given-r-reduce-P : R → P ≃ Unit
  given-r-reduce-P r₀ =

    P

                         ≃⟨ equiv-Σ-snd (λ _ → equiv-Σ-snd (λ _ → equiv-Σ-snd (λ _ → switch-args))) ⟩

    (Σ Y λ y →
        Σ ((q : Q) → y == f(inl q)) λ s →
        Σ ((r : R) → y == f(inr r)) λ t →
          (r : R) → (q : Q) → ! (s q) ∙ (t r) == c (inl q) (inr r))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ s → choice ⁻¹)) ⟩

    (Σ Y λ y →
        Σ ((q : Q) → y == f(inl q)) λ s →
          (r : R) → Σ (y == f(inr r)) λ t-reduced →
                      (q : Q) → ! (s q) ∙ t-reduced == c (inl q) (inr r))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → Π₁-contr (r₀ , prop-has-all-paths rr r₀))) ⟩

    (Σ Y λ y →
        Σ ((q : Q) → y == f(inl q)) λ s →
          Σ (y == f(inr r₀)) λ t-reduced →
            (q : Q) → ! (s q) ∙ t-reduced == c (inl q) (inr r₀))

                         ≃⟨ switch23 ⟩

    (Σ Y λ y →
        Σ (y == f(inr r₀)) λ t-reduced →
          Σ ((q : Q) → y == f(inl q)) λ s →
            (q : Q) → ! (s q) ∙ t-reduced == c (inl q) (inr r₀))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ s → choice ⁻¹)) ⟩

    (Σ Y λ y →
        Σ (y == f(inr r₀)) λ t-reduced →
          (q : Q) → Σ (y == f(inl q)) λ s-reduced →
                       ! s-reduced ∙ t-reduced == c (inl q) (inr r₀))

                         ≃⟨ Σ-assoc ⁻¹ ⟩

    (Σ (Σ Y λ y → (y == f(inr r₀))) λ {(y , t-reduced) →
       (q : Q) → Σ (y == f(inl q)) λ s-reduced →
                   ! s-reduced ∙ t-reduced == c (inl q) (inr r₀)})

                         ≃⟨ Σ₁-contr (pathto-is-contr _) ⟩

    ((q : Q) → Σ (f(inr r₀) == f(inl q)) λ s-reduced →
                  ! s-reduced ∙ idp == c (inl q) (inr r₀))

                         ≃⟨ equiv-Π-r (λ q → equiv-Σ-snd (λ proof →
                              ! proof ∙ idp == c (inl q) (inr r₀) ≃⟨ delete-idp _ _ ⟩
                              ! proof == c (inl q) (inr r₀) ≃⟨ reverse-paths _ _ ⟩
                              proof == ! (c (inl q) (inr r₀))   ≃∎
                         )) ⟩

    ((q : Q) → Σ (f(inr r₀) == f(inl q)) λ s-reduced →
                  s-reduced == ! (c (inl q) (inr r₀)))

                         ≃⟨ Π₂-contr (λ q → pathto-is-contr _) ⟩

    Unit                 ≃∎

  given-q+r-reduce-P : Coprod Q R → P ≃ Unit
  given-q+r-reduce-P (inl q) = given-q-reduce-P q
  given-q+r-reduce-P (inr r) = given-r-reduce-P r

  Q+R→P : Coprod Q R → P
  Q+R→P x = <– (given-q+r-reduce-P x) _

  P→Y : P → Y
  P→Y = fst

  open import lib.types.Unit

  -- Finally : the statement of Theorem 5.2.6
  factorize-f : factorizes f
  factorize-f = factorize-helper f P (λ x → equiv-preserves-level ((given-q+r-reduce-P x) ⁻¹) Unit-is-prop) (Q+R→P , P→Y , proof) where
    proof : (x : Coprod Q R) → P→Y (Q+R→P x) == f x
    proof (inl q) = idp
    proof (inr r) = idp

-- and Theorem 5.2.6 again (outside of a specialized module)
Theorem526 : ∀ {i} {Q R Y : Type i} → (is-prop Q) → (is-prop R) → (f : Coprod Q R → Y) → (const f) → factorizes f
Theorem526 = thm526.factorize-f

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Cubical.Core.Everything

private
  variable
    ℓ : Level
    A B : Type ℓ

data Maybe (A : Type ℓ) : Type ℓ where
  nothing : Maybe A
  just    : A → Maybe A

caseMaybe : (n j : B) → Maybe A → B
caseMaybe n _ nothing  = n
caseMaybe _ j (just _) = j

map-Maybe : (A → B) → Maybe A → Maybe B
map-Maybe _ nothing  = nothing
map-Maybe f (just x) = just (f x)

rec : B → (A → B) → Maybe A → B
rec n j nothing = n
rec n j (just a) = j a

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module nodcap.Norm where

open import Category.Monad
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Pos as ℕ⁺ using (ℕ⁺; suc; _+_)
open import Data.List as L using (List; []; _∷_; _++_)
open import Data.List.Any as LA using (Any; here; there)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_$_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open import Data.Environment
open import nodcap.Base
open import nodcap.Typing as FF using (⊢_)
open import nodcap.NF.Typing as NF using (⊢ⁿᶠ_)
import nodcap.NF.Axiom as NFA
import nodcap.NF.Cut as NFD
import nodcap.NF.CutND as NFND

private
  open module LM {ℓ} = RawMonadPlus (L.monadPlus {ℓ})

nf : {Γ : Environment} → ⊢ Γ → ⊢ⁿᶠ Γ
nf  FF.ax        = NFA.ax
nf (FF.cut  x y) = NFD.cut (nf x) (nf y)
nf (FF.send x y) = NF.send (nf x) (nf y)
nf (FF.recv x)   = NF.recv (nf x)
nf (FF.sel₁ x)   = NF.sel₁ (nf x)
nf (FF.sel₂ x)   = NF.sel₂ (nf x)
nf (FF.case x y) = NF.case (nf x) (nf y)
nf  FF.halt      = NF.halt
nf (FF.wait x)   = NF.wait (nf x)
nf  FF.loop      = NF.loop
nf (FF.mk?₁ x)   = NF.mk?₁ (nf x)
nf (FF.mk!₁ x)   = NF.mk!₁ (nf x)
nf (FF.cont x)   = NF.cont (nf x)
nf (FF.pool x y) = NF.pool (nf x) (nf y)
nf (FF.exch b x) = NF.exch b (nf x)

nfND : {Γ : Environment} → ⊢ Γ → List (⊢ⁿᶠ Γ)
nfND  FF.ax        = return NFA.ax
nfND (FF.cut  x y) = nfND x >>= λ x → nfND y >>= λ y → NFND.cutND x y
nfND (FF.send x y) = nfND x >>= λ x → nfND y >>= λ y → return $ NF.send x y
nfND (FF.recv x)   = nfND x >>= λ x → return $ NF.recv x
nfND (FF.sel₁ x)   = nfND x >>= λ x → return $ NF.sel₁ x
nfND (FF.sel₂ x)   = nfND x >>= λ x → return $ NF.sel₂ x
nfND (FF.case x y) = nfND x >>= λ x → nfND y >>= λ y → return $ NF.case x y
nfND  FF.halt      = return NF.halt
nfND (FF.wait x)   = nfND x >>= λ x → return (NF.wait x)
nfND  FF.loop      = return NF.loop
nfND (FF.mk?₁ x)   = nfND x >>= λ x → return $ NF.mk?₁ x
nfND (FF.mk!₁ x)   = nfND x >>= λ x → return $ NF.mk!₁ x
nfND (FF.cont x)   = nfND x >>= λ x → return $ NF.cont x
nfND (FF.pool x y) = nfND x >>= λ x → nfND y >>= λ y → return $ NF.pool x y
nfND (FF.exch b x) = nfND x >>= λ x → return $ NF.exch b x

-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
-- 2018-01-05, Jesper: having a `rewrite` after a `with` caused problems
-- because the patterns stripped by with-desugaring were not propagated
-- to the generated rewrite-clause. This should now be fixed.

open import Agda.Builtin.Equality

postulate
  lem : Set ≡ Set

simple-test : {A : Set₁} → A ≡ Set → Set₁
simple-test {A = A} refl with Set
simple-test {A = A} refl | _ rewrite lem = A

record ⊤ : Set where constructor tt

data G : Set → Set₁ where
  d : (A : Set) → G A → G A

postulate
  exists : (A : Set) → G A
  unique : (A : Set) (x : G A) → exists A ≡ x

test : (A : Set) → G A → ⊤
test _ (d A x) with unique A x
test _ (d A _) | refl rewrite refl {x = tt} = tt

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Curry5 where

open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst)
open import Function using (id)

lemma1 : {X Y : Set} → (X ≡ (X → Y)) → X
lemma1 p rewrite p = (λ x → let f = subst id p x in f x)

curry : {X Y : Set} → (X ≡ (X → Y)) → Y
curry p = (let f = subst id p (lemma1 p) in f (lemma1 p))


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

open import Agda.Primitive using (Level; _⊔_; Setω; lzero; lsuc)

module Issue4020b where

data _≡_ {ℓ : Level} {A : Set ℓ} (a : A) : A → Set ℓ where
  refl : a ≡ a

{-# BUILTIN REWRITE _≡_ #-}

ap : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {a₁ a₂} → a₁ ≡ a₂ → f a₁ ≡ f a₂
ap f refl = refl

ap-const-Pi : ∀ {a b} {A : Set a} {B : A → Set b} {a₁ a₂ : A} (p : a₁ ≡ a₂) → ap (\ _ → (x : A) → B x) p ≡ refl
ap-const-Pi refl = refl

{-# REWRITE ap-const-Pi #-}
{- /home/jason/bug2.agda:18,1-28
ap-const-Pi  is not a legal rewrite rule, since the following variables are not bound by the left hand side:  b
when checking the pragma REWRITE ap-const-Pi -}


text:
{-# OPTIONS --safe #-}
module Generics.Constructions.Show where

open import Generics.Prelude hiding (lookup)
open import Generics.Telescope
open import Generics.Desc
open import Generics.All
open import Generics.HasDesc
import Generics.Helpers as Helpers

import Data.Vec.Base as Vec
import Data.String   as String
open import Data.Maybe as Maybe
open import Data.These hiding (alignWith)

open String hiding (show)

record Show {l} (A : Set l) : Set l where field show : A → String
open Show ⦃...⦄ public

private
  dummyShow : ∀ {l} (A : Set l) → Show A
  dummyShow A .show _ = ""

  join : These String String → String
  join (this x) = x
  join (that x) = x
  join (these x y) = x ++ " , " ++ y

module _
  {P I ℓ} {A : Indexed P I ℓ} (H : HasDesc A)
  (open HasDesc H)
  (open Helpers P I Show (const ⊤) (λ _ → Liftω ⊤))
  where

  ShowHelpers : ∀ p → Setω
  ShowHelpers p = Helpers p D

  module _ {p} (helpers : ShowHelpers p) where

    variable
      V : ExTele P
      v : ⟦ V ⟧tel p
      i : ⟦ I ⟧tel p

    showData-wf : (x : ⟦ D ⟧Data A′ (p , i))
                → AllDataω Acc D x
                → Maybe String

    show-wf : (x : A′ (p , i)) → Acc x → Maybe String
    show-wf x (acc a) = showData-wf (split x) a

    showData-wf (k , x) a = just $
      Vec.lookup names k
      ++ fromMaybe "" (Maybe.map (λ x → " (" ++ x ++ ")")
                                 (showCon (lookupCon D k) (lookupHelper helpers k) x a))
      where
        showIndArg : (C : ConDesc P V I)
                     (x : ⟦ C ⟧IndArg A′ (p , v))
                   → AllIndArgω Acc C x
                   → Maybe String
        showIndArg (var _) x a = show-wf x a
        showIndArg (π ia S C) x a = just "?f"
        showIndArg (A ⊗ B) (xa , xb) (aa , ab)
          = alignWith join (showIndArg A xa aa) (showIndArg B xb ab)

        showCon : (C : ConDesc P V I)
                  (H : ConHelper p C)
                  (x : ⟦ C ⟧Con A′ (p , v , i))
                → AllConω Acc C x
                → Maybe String
        showCon ._ var refl tt = nothing
        showCon ._ (pi-irr ⦃ _ ⦄ ⦃ H ⦄) (s , x) a
          = alignWith join (just "._") (showCon _ H x a)
        showCon ._ (pi-rel ⦃ S ⦄ ⦃ H ⦄) (s , x) a
          = alignWith join (just (show ⦃ S ⦄ s)) (showCon _ H x a)
        showCon ._ (prod {A} {B} ⦃ HA ⦄ ⦃ HB ⦄) (xa , xb) (aa , ab)
          = alignWith join (showIndArg A xa aa) (showCon B HB xb ab)

    show′ : (x : A′ (p , i)) → Maybe String
    show′ x = show-wf x (wf x)

  deriveShow : ∀ {p} ⦃ SH : ShowHelpers p ⦄ {i} → Show (A′ (p , i))
  deriveShow ⦃ SH ⦄ .show = fromMaybe "" ∘ show′ SH

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
------------------------------------------------------------------------------
-- Natural numbers (added for the Collatz function example)
------------------------------------------------------------------------------

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

-- We don't want populate the FOTC library with more first-order logic
-- axioms.

module FOTC.Program.Collatz.Data.Nat where

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

infixr 8 _^_

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

postulate
  div     : D → D → D
  div-x<y : ∀ {m n} → n ≢ 0' → m < n → div m n ≡ zero
  div-x≥y : ∀ {m n} → n ≢ 0' → m ≥ n → div m n ≡ succ₁ (div (m ∸ n) n)
{-# ATP axioms div-x<y div-x≥y #-}

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

postulate
  even : D → D
  odd  : D → D

  even-0 : even zero            ≡ true
  even-S : ∀ n → even (succ₁ n) ≡ odd n

  odd-0 : odd zero            ≡ false
  odd-S : ∀ n → odd (succ₁ n) ≡ even n
{-# ATP axioms even-0 even-S odd-0 odd-S #-}

Even : D → Set
Even n = even n ≡ true
{-# ATP definition Even #-}

NotEven : D → Set
NotEven n = even n ≡ false
{-# ATP definition NotEven #-}

Odd : D → Set
Odd n = odd n ≡ true
{-# ATP definition Odd #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module plfa-code.Equality where

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

infix 4 _≡_

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -------
  → y ≡ x
sym refl = refl

trans : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -------
  → x ≡ z
trans refl refl = refl

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

cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B}
  → u ≡ x
  → v ≡ y
    ---------------
  → f u v ≡ f x y
cong₂ _ refl refl  =  refl

cong-app : ∀ {A B : Set} {f g : A → B}
  → f ≡ g
    ------------------------
  → ∀ (x : A) → f x ≡ g x
cong-app refl _ = refl

subst : ∀ {A : Set} {x y : A} (P : A → Set)
  → x ≡ y
    -----------
  → P x → P y
subst _ refl px = px

module ≡-Reasoning {A : Set} where

  infix  1 begin_
  infixr 2 _≡⟨⟩_ _≡⟨_⟩_
  infix  3 _∎

  begin_ : ∀ {x y : A}
    → x ≡ y
      -------
    → x ≡ y
  begin x≡y = x≡y

  _≡⟨⟩_ : ∀ (x : A) {y : A}
    → x ≡ y
      -------
    → x ≡ y
  x ≡⟨⟩ x≡y  =  x≡y

  _≡⟨_⟩_ : ∀ (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
      -------
    → x ≡ z
  x ≡⟨ x≡y ⟩ y≡z  =  trans x≡y y≡z

  _∎ : ∀ (x : A)
      ------
    → x ≡ x
  x ∎  = refl

open ≡-Reasoning

trans′ : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -------
  → x ≡ z
trans′ {A} {x} {y} {z} x≡y y≡z =
  begin
    x
  ≡⟨ x≡y ⟩
    y
  ≡⟨ y≡z ⟩
    z
  ∎

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

infixl 6 _+_

_+_ : ℕ → ℕ → ℕ
zero    + n  =  n
(suc m) + n  =  suc (m + n)

-- use postulate
postulate
  +-identity : ∀ (m : ℕ) → m + zero ≡ m
  +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identity m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      ---------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      --------------
    → suc m ≤ suc n

infix 4 _≤_

postulate
  ≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
  ≤-refl : ∀ {n : ℕ} → n ≤ n

≡→≤ : ∀ {x y} → x ≡ y → x ≤ y
≡→≤ refl = ≤-refl

module ≤-Reasoning where

  infix  1 ≤begin_
  infixr 2 _≤⟨⟩_ _≤⟨_⟩_ _≤[_]_
  infix  3 _≤∎

  ≤begin_ : ∀ {x y} → x ≤ y → x ≤ y
  ≤begin x≤y  =  x≤y

  _≤⟨⟩_ : ∀ (x) {y : ℕ} → x ≤ y → x ≤ y
  _ ≤⟨⟩ x≤y  =  x≤y

  _≤⟨_⟩_ : ∀ (x) {y z : ℕ} → x ≤ y → y ≤ z → x ≤ z
  x ≤⟨ x≤y ⟩ y≤z  =  ≤-trans x≤y y≤z

  _≤[_]_ : ∀ (x) {y z : ℕ} → x ≡ y → y ≤ z → x ≤ z
  x ≤[ x≡y ] y≤z = ≤-trans (≡→≤ x≡y) y≤z

  _≤∎ : ∀ x → x ≤ x
  _ ≤∎ = ≤-refl

open ≤-Reasoning

+-monoʳ-≤ : ∀ (n p q : ℕ) → p ≤ q → (n + p) ≤ (n + q)

+-monoʳ-≤ zero p q p≤q =
  ≤begin
    (zero + p)
  ≤⟨⟩
    p
  ≤⟨ p≤q ⟩
    q
  ≤⟨⟩
    zero + q
  ≤∎
+-monoʳ-≤ (suc n) p q p≤q =
  ≤begin
    suc n + p
  ≤⟨⟩
    suc (n + p)
  ≤⟨ s≤s (+-monoʳ-≤ _ _ _ p≤q) ⟩
    suc (n + q)
  ≤⟨⟩
    suc n + q
  ≤∎

+-monoˡ-≤ : ∀ (m n p : ℕ) → m ≤ n → (m + p) ≤ (n + p)
+-monoˡ-≤ m n p m≤n =
  ≤begin
    m + p
  ≤[ +-comm m p ]
    p + m
  ≤⟨ +-monoʳ-≤ p _ _ m≤n ⟩
    p + n
  ≤[ +-comm p n ]
    n + p
  ≤∎

+-mono-≤ : ∀ (m n p q : ℕ) → m ≤ n → p ≤ q → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q =
  ≤begin
    m + p
  ≤⟨ +-monoˡ-≤ _ _ _ m≤n ⟩
    n + p
  ≤⟨ +-monoʳ-≤ _ _ _ p≤q ⟩
    n + q
  ≤∎

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd n
      -------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even n
      ------------
    → odd (suc n)

{-# BUILTIN EQUALITY _≡_ #-}

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    -------------
  → even (n + m)
even-comm m n ev rewrite +-comm n m = ev

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ zero    n  rewrite +-identity n             =  refl
+-comm′ (suc m) n  rewrite +-suc n m | +-comm′ m n  =  refl

even-comm′ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm′ m n ev with   m + n  | +-comm m n
...                  | .(n + m) | refl       = ev

_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

refl-≐ : ∀ {A : Set} {x : A}
  → x ≐ x
refl-≐ P Px = Px

trans-≐ : ∀ {A : Set} {x y z : A}
  → x ≐ y
  → y ≐ z
    ------
  → x ≐ z
trans-≐ x≐y y≐z P Px  =  y≐z P (x≐y P Px)

sym-≐ : ∀ {A : Set} {x y : A}
  → x ≐ y
    ------
  → y ≐ x
sym-≐ {A} {x} {y} x≐y P  =  Qy
  where
    Q : A → Set
    Q z = P z → P x
    Qx : Q x
    Qx = refl-≐ P
    Qy : Q y
    Qy = x≐y Q Qx

≡-implies-≐ : ∀ {A : Set} {x y : A}
  → x ≡ y
    -------
  → x ≐ y
≡-implies-≐ x≡y P  =  subst P x≡y

≐-implies-≡ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -------
  → x ≡ y
≐-implies-≡ {A} {x} {y} x≐y = Qy
  where
    Q : A → Set
    Q z = x ≡ z
    Qx : Q x
    Qx = refl
    Qy : Q y
    Qy = x≐y Q Qx

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

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

sym′ : ∀ {ℓ : Level} {A : Set ℓ} {x y : A}
  → x ≡′ y
    --------
  → y ≡′ x
sym′ refl′ = refl′

_≐′_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
_≐′_ {ℓ} {A} x y = ∀ (P : A → Set ℓ) → P x → P y

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code


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

module Test where

open import Cubical.Core.Everything         using (_≡_; Level; Type; Σ; _,_; fst; snd; _≃_; ~_)
open import Cubical.Foundations.Prelude     using (refl; sym; _∙_; cong; transport; subst; funExt; transp; I; i0; i1)
open import Cubical.Foundations.Function    using (_∘_)
open import Cubical.Foundations.Univalence  using (ua)
open import Cubical.Foundations.Isomorphism using (iso; Iso; isoToPath; section; retract)

open import Data.Bool.Base using (Bool; true; false; _∧_)
open import Data.Nat.Base  using (ℕ; zero; suc)
open import Data.Product   using (_×_; proj₁; proj₂)

natrec : (P : ℕ → Type) → P 0 → ((n : ℕ) → P n → P (suc n)) → (n : ℕ) → P n
natrec P z s zero    = z
natrec P z s (suc n) = s n (natrec P z s n)

_+_ : ℕ → ℕ → ℕ
_+_ = λ m → λ n → natrec (λ _ → ℕ) n (λ _ → suc) m

0=0 : 0 ≡ 0
0=0 = refl

suc=suc : (m n : ℕ) → m ≡ n → suc m ≡ suc n
suc=suc m n e = cong suc e

0+n=n : (n : ℕ) → 0 + n ≡ n
0+n=n = natrec (λ k → 0 + k ≡ k) 0=0 (λ n e → suc=suc n n e)

n=0+n : (n : ℕ) → n + 0 ≡ n
n=0+n = natrec (λ k → k + 0 ≡ k) 0=0 λ n e → suc=suc (n + 0) n e

max_stars_repo_name: halfaya/Alae

max_issues_repo_name: halfaya/Alae

max_forks_repo_name: halfaya/Alae


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A generalisation of the arithmetic operations
------------------------------------------------------------------------

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

module Data.Nat.GeneralisedArithmetic where

open import Data.Nat
open import Data.Nat.Properties
open import Function using (_∘′_; _∘_; id)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

module _ {a} {A : Set a} where

  fold : A → (A → A) → ℕ → A
  fold z s zero    = z
  fold z s (suc n) = s (fold z s n)

  add : (0# : A) (1+ : A → A) → ℕ → A → A
  add 0# 1+ n z = fold z 1+ n

  mul : (0# : A) (1+ : A → A) → (+ : A → A → A) → (ℕ → A → A)
  mul 0# 1+ _+_ n x = fold 0# (λ s → x + s) n

-- Properties

module _ {a} {A : Set a} where

  fold-+ : ∀ {s : A → A} {z : A} →
           ∀ m {n} → fold z s (m + n) ≡ fold (fold z s n) s m
  fold-+ zero    = refl
  fold-+ {s = s} (suc m) = cong s (fold-+ m)

  fold-k : ∀ {s : A → A} {z : A} {k} m →
           fold k (s ∘′_) m z ≡ fold (k z) s m
  fold-k zero    = refl
  fold-k {s = s} (suc m) = cong s (fold-k m)

  fold-* : ∀ {s : A → A} {z : A} m {n} →
           fold z s (m * n) ≡ fold z (fold id (s ∘_) n) m
  fold-*  zero        = refl
  fold-* {s = s} {z} (suc m) {n} = let +n = fold id (s ∘′_) n in begin
    fold z s (n + m * n)        ≡⟨ fold-+ n ⟩
    fold (fold z s (m * n)) s n ≡⟨ cong (λ z → fold z s n) (fold-* m) ⟩
    fold (fold z +n m) s n      ≡⟨ sym (fold-k n) ⟩
    fold z +n (suc m)           ∎

  fold-pull : ∀ {s : A → A} {z : A} (g : A → A → A) (p : A)
              (eqz : g z p ≡ p)
              (eqs : ∀ l → s (g l p) ≡ g (s l) p) →
              ∀ m → fold p s m ≡ g (fold z s m) p
  fold-pull _ _ eqz _ zero    = sym eqz
  fold-pull {s = s} {z} g p eqz eqs (suc m) = begin
    s (fold p s m)       ≡⟨ cong s (fold-pull g p eqz eqs m) ⟩
    s (g (fold z s m) p) ≡⟨ eqs (fold z s m) ⟩
    g (s (fold z s m)) p ∎

id-is-fold : ∀ m → fold zero suc m ≡ m
id-is-fold zero    = refl
id-is-fold (suc m) = cong suc (id-is-fold m)

+-is-fold : ∀ m {n} → fold n suc m ≡ m + n
+-is-fold zero    = refl
+-is-fold (suc m) = cong suc (+-is-fold m)

*-is-fold : ∀ m {n} → fold zero (n +_) m ≡ m * n
*-is-fold zero        = refl
*-is-fold (suc m) {n} = cong (n +_) (*-is-fold m)

^-is-fold : ∀ {m} n → fold 1 (m *_) n ≡ m ^ n
^-is-fold     zero    = refl
^-is-fold {m} (suc n) = cong (m *_) (^-is-fold n)

*+-is-fold : ∀ m n {p} → fold p (n +_) m ≡ m * n + p
*+-is-fold m n {p} = begin
  fold p (n +_) m     ≡⟨ fold-pull _+_ p refl
                         (λ l → sym (+-assoc n l p)) m ⟩
  fold 0 (n +_) m + p ≡⟨ cong (_+ p) (*-is-fold m) ⟩
  m * n + p           ∎

^*-is-fold : ∀ m n {p} → fold p (m *_) n ≡ m ^ n * p
^*-is-fold m n {p} = begin
  fold p (m *_) n     ≡⟨ fold-pull _*_ p (*-identityˡ p)
                         (λ l → sym (*-assoc m l p)) n ⟩
  fold 1 (m *_) n * p ≡⟨ cong (_* p) (^-is-fold n) ⟩
  m ^ n * p           ∎


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- About the group structure of integers and bags for Nehemiah plugin.
------------------------------------------------------------------------

module Theorem.Groups-Nehemiah where

open import Structure.Bag.Nehemiah public

open import Relation.Binary.PropositionalEquality
open import Algebra.Structures

4-way-shuffle : ∀ {A : Set} {f} {z a b c d : A}
  {{comm-monoid : IsCommutativeMonoid _≡_ f z}} →
  f (f a b) (f c d) ≡ f (f a c) (f b d)
4-way-shuffle {f = f} {z = z} {a} {b} {c} {d} {{comm-monoid}} =
  let
    assoc = associative comm-monoid
    cmute = commutative comm-monoid
  in
    begin
      f (f a b) (f c d)
    ≡⟨ assoc a b (f c d) ⟩
      f a (f b (f c d))
    ≡⟨ cong (f a) (sym (assoc b c d)) ⟩
      f a (f (f b c) d)
    ≡⟨ cong (λ hole → f a (f hole d)) (cmute b c) ⟩
      f a (f (f c b) d)
    ≡⟨ cong (f a) (assoc c b d) ⟩
      f a (f c (f b d))
    ≡⟨ sym (assoc a c (f b d)) ⟩
      f (f a c) (f b d)
    ∎ where open ≡-Reasoning

module _ where
  open import Data.Nat
  -- Apologies for irregular name.
  ℕ-mn·pq=mp·nq : ∀ {m n p q : ℕ} →
    (m + n) + (p + q) ≡ (m + p) + (n + q)
  ℕ-mn·pq=mp·nq {m} {n} {p} {q} =
    4-way-shuffle {a = m} {n} {p} {q} {{comm-monoid-nat}}

open import Data.Integer

n+[m-n]=m : ∀ {n m} → n + (m - n) ≡ m
n+[m-n]=m {n} {m} =
  begin
    n + (m - n)
  ≡⟨ cong (λ hole → n + hole) (commutative-int m (- n)) ⟩
    n + (- n + m)
  ≡⟨ sym (associative-int n (- n) m) ⟩
    (n - n) + m
  ≡⟨ cong (λ hole → hole + m) (right-inv-int n) ⟩
    (+ 0) + m
  ≡⟨ left-id-int m ⟩
    m
  ∎ where open ≡-Reasoning

a++[b\\a]=b : ∀ {a b} → a ++ (b \\ a) ≡ b
a++[b\\a]=b {b} {d} = trans
  (cong (λ hole → b ++ hole) (commutative-bag d (negateBag b))) (trans
  (sym (associative-bag b (negateBag b) d)) (trans
  (cong (λ hole → hole ++ d) (right-inv-bag b))
  (left-id-bag d)))

ab·cd=ac·bd : ∀ {a b c d : Bag} →
  (a ++ b) ++ (c ++ d) ≡ (a ++ c) ++ (b ++ d)
ab·cd=ac·bd {a} {b} {c} {d} =
  4-way-shuffle {a = a} {b} {c} {d} {{comm-monoid-bag}}

mn·pq=mp·nq : ∀ {m n p q : ℤ} →
  (m + n) + (p + q) ≡ (m + p) + (n + q)
mn·pq=mp·nq {m} {n} {p} {q} =
  4-way-shuffle {a = m} {n} {p} {q} {{comm-monoid-int}}

inverse-unique : ∀ {A : Set} {f neg} {z a b : A}
  {{abelian : IsAbelianGroup _≡_ f z neg}} →
  f a b ≡ z → b ≡ neg a

inverse-unique {f = f} {neg} {z} {a} {b} {{abelian}} ab=z =
  let
    assoc = associative (IsAbelianGroup.isCommutativeMonoid abelian)
    cmute = commutative (IsAbelianGroup.isCommutativeMonoid abelian)
  in
    begin
      b
    ≡⟨ sym (left-identity abelian b) ⟩
      f z b
    ≡⟨ cong (λ hole → f hole b) (sym (left-inverse abelian a)) ⟩
      f (f (neg a) a) b
    ≡⟨ assoc (neg a) a b ⟩
      f (neg a) (f a b)
    ≡⟨ cong (f (neg a)) ab=z ⟩
      f (neg a) z
    ≡⟨ right-identity abelian (neg a) ⟩
      neg a
    ∎ where
      open ≡-Reasoning
      eq1 : f (neg a) (f a b) ≡ f (neg a) z
      eq1 rewrite ab=z = cong (f (neg a)) refl

distribute-neg : ∀ {A : Set} {f neg} {z a b : A}
  {{abelian : IsAbelianGroup _≡_ f z neg}} →
  f (neg a) (neg b) ≡ neg (f a b)
distribute-neg {f = f} {neg} {z} {a} {b} {{abelian}} = inverse-unique
  {{abelian}}
  (begin
    f (f a b) (f (neg a) (neg b))
  ≡⟨ 4-way-shuffle {{IsAbelianGroup.isCommutativeMonoid abelian}} ⟩
    f (f a (neg a)) (f b (neg b))
  ≡⟨ cong₂ f (inverse a) (inverse b) ⟩
    f z z
  ≡⟨ left-identity abelian z ⟩
    z
  ∎) where
     open ≡-Reasoning
     inverse = right-inverse abelian

-a·-b=-ab : ∀ {a b : Bag} →
  negateBag a ++ negateBag b ≡ negateBag (a ++ b)
-a·-b=-ab {a} {b} = distribute-neg {a = a} {b} {{abelian-bag}}

-m·-n=-mn : ∀ {m n : ℤ} →
  (- m) + (- n) ≡ - (m + n)
-m·-n=-mn {m} {n} = distribute-neg {a = m} {n} {{abelian-int}}

[a++b]\\a=b : ∀ {a b} → (a ++ b) \\ a ≡ b
[a++b]\\a=b {b} {d} =
  begin
    (b ++ d) \\ b
  ≡⟨ cong (λ hole → hole \\ b) (commutative-bag b d) ⟩
    (d ++ b) \\ b
  ≡⟨ associative-bag d b (negateBag b) ⟩
    d ++ (b \\ b)
  ≡⟨ cong (_++_ d) (right-inv-bag b) ⟩
    d ++ emptyBag
  ≡⟨ right-id-bag d ⟩
    d
  ∎ where open ≡-Reasoning

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------------
-- Properties related with the forest type
------------------------------------------------------------------------------

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

module FOTC.Program.Mirror.Forest.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesI
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
  using ( ++-leftCong
        ; ++-leftIdentity
        ; ++-rightCong
        ; mapCong₂
        ; revCong₁
        ; reverseCong
        ; reverse-[x]≡[x]
        )
open import FOTC.Program.Mirror.Forest.TotalityI
open import FOTC.Program.Mirror.Type

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

++-rightIdentity : ∀ {xs} → Forest xs → xs ++ [] ≡ xs
++-rightIdentity fnil                    = ++-leftIdentity []
++-rightIdentity (fcons {x} {xs} Tx Fxs) =
  (x ∷ xs) ++ []
     ≡⟨ ++-∷ x xs [] ⟩
  x ∷ (xs ++ [])
    ≡⟨ ∷-rightCong (++-rightIdentity Fxs) ⟩
  x ∷ xs ∎

++-assoc : ∀ {xs} → Forest xs → ∀ ys zs → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc fnil ys zs =
  ([] ++ ys) ++ zs
    ≡⟨ ++-leftCong (++-leftIdentity ys) ⟩
  ys ++ zs
     ≡⟨ sym (++-leftIdentity (ys ++ zs)) ⟩
  [] ++ ys ++ zs ∎

++-assoc (fcons {x} {xs} Tx Fxs) ys zs =
  ((x ∷ xs) ++ ys) ++ zs
    ≡⟨ ++-leftCong (++-∷ x xs ys) ⟩
  (x ∷ (xs ++ ys)) ++ zs
     ≡⟨ ++-∷ x (xs ++ ys) zs ⟩
  x ∷ ((xs ++ ys) ++ zs)
    ≡⟨ ∷-rightCong (++-assoc Fxs ys zs) ⟩
  x ∷ (xs ++ ys ++ zs)
    ≡⟨ sym (++-∷ x xs (ys ++ zs)) ⟩
  (x ∷ xs) ++ ys ++ zs ∎

map-++ : ∀ f {xs} → (∀ {x} → Tree x → Tree (f · x)) →
         Forest xs →
         ∀ ys → map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++ f h fnil ys =
  map f ([] ++ ys)
    ≡⟨ mapCong₂ (++-leftIdentity ys) ⟩
  map f ys
    ≡⟨ sym (++-leftIdentity (map f ys)) ⟩
  [] ++ map f ys
     ≡⟨ ++-leftCong (sym (map-[] f)) ⟩
  map f [] ++ map f ys ∎

map-++ f h (fcons {x} {xs} Tx Fxs) ys =
  map f ((x ∷ xs) ++ ys)
    ≡⟨ mapCong₂ (++-∷ x xs ys) ⟩
  map f (x ∷ xs ++ ys)
    ≡⟨ map-∷ f x (xs ++ ys) ⟩
  f · x ∷ map f (xs ++ ys)
    ≡⟨ ∷-rightCong (map-++ f h Fxs ys) ⟩
  f · x ∷ (map f xs ++ map f ys)
    ≡⟨ sym (++-∷ (f · x) (map f xs) (map f ys)) ⟩
  (f · x ∷ map f xs) ++ map f ys
     ≡⟨ ++-leftCong (sym (map-∷ f x xs)) ⟩
  map f (x ∷ xs) ++ map f ys ∎

rev-++ : ∀ {xs} → Forest xs → ∀ ys → rev xs ys ≡ rev xs [] ++ ys
rev-++ fnil ys =
  rev [] ys       ≡⟨ rev-[] ys ⟩
  ys              ≡⟨ sym (++-leftIdentity ys) ⟩
  [] ++ ys        ≡⟨ ++-leftCong (sym (rev-[] [])) ⟩
  rev [] [] ++ ys ∎

rev-++ (fcons {x} {xs} Tx Fxs) ys =
  rev (x ∷ xs) ys
    ≡⟨ rev-∷ x xs ys ⟩
  rev xs (x ∷ ys)
    ≡⟨ rev-++ Fxs (x ∷ ys) ⟩
  rev xs [] ++ x ∷ ys
    ≡⟨ ++-rightCong prf ⟩
  rev xs [] ++ (x ∷ []) ++ ys
    ≡⟨ sym (++-assoc (rev-Forest Fxs fnil) (x ∷ []) ys) ⟩
  (rev xs [] ++ (x ∷ [])) ++ ys
    ≡⟨ ++-leftCong (sym (rev-++ Fxs (x ∷ []))) ⟩
  rev xs (x ∷ []) ++ ys
    ≡⟨ ++-leftCong (sym (rev-∷ x xs [])) ⟩
  rev (x ∷ xs) [] ++ ys ∎
    where prf : x ∷ ys ≡ (x ∷ []) ++ ys
          prf = x ∷ ys         ≡⟨ ∷-rightCong (sym (++-leftIdentity ys)) ⟩
                x ∷ ([] ++ ys) ≡⟨ sym (++-∷ x [] ys) ⟩
                (x ∷ []) ++ ys ∎

reverse-++ : ∀ {xs ys} → Forest xs → Forest ys →
             reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++ {ys = ys} fnil Fys =
  reverse ([] ++ ys)
    ≡⟨ reverseCong (++-leftIdentity ys) ⟩
  reverse ys
    ≡⟨ sym (++-rightIdentity (reverse-Forest Fys)) ⟩
  reverse ys ++ []
    ≡⟨ ++-rightCong (sym (rev-[] [])) ⟩
  reverse ys ++ reverse [] ∎

reverse-++ (fcons {x} {xs} Tx Fxs) fnil =
  reverse ((x ∷ xs) ++ [])
    ≡⟨ reverseCong (++-rightIdentity (fcons Tx Fxs)) ⟩
  reverse (x ∷ xs)
    ≡⟨ sym (++-leftIdentity (reverse (x ∷ xs))) ⟩
  [] ++ reverse (x ∷ xs)
     ≡⟨ ++-leftCong (sym (rev-[] [])) ⟩
  reverse [] ++ reverse (x ∷ xs) ∎

reverse-++ (fcons {x} {xs} Tx Fxs) (fcons {y} {ys} Ty Fys) =
  rev ((x ∷ xs) ++ y ∷ ys) []
    ≡⟨ revCong₁ (++-∷ x xs (y ∷ ys)) ⟩
  rev (x ∷ (xs ++ y ∷ ys)) []
    ≡⟨ rev-∷ x (xs ++ y ∷ ys) [] ⟩
  rev (xs ++ y ∷ ys) (x ∷ [])
    ≡⟨ rev-++ (++-Forest Fxs (fcons Ty Fys)) (x ∷ []) ⟩
  rev (xs ++ y ∷ ys) [] ++ (x ∷ [])
    ≡⟨ ++-leftCong refl ⟩
  reverse (xs ++ y ∷ ys) ++ (x ∷ [])
    ≡⟨ ++-leftCong (reverse-++ Fxs (fcons Ty Fys)) ⟩
  (reverse (y ∷ ys) ++ reverse xs) ++ x ∷ []
    ≡⟨ ++-assoc (reverse-Forest (fcons Ty Fys))
                (reverse xs)
                (x ∷ [])
    ⟩
  reverse (y ∷ ys) ++ rev xs [] ++ x ∷ []
    ≡⟨ ++-rightCong (sym (rev-++ Fxs (x ∷ []))) ⟩
  reverse (y ∷ ys) ++ rev xs (x ∷ [])
    ≡⟨ ++-rightCong (sym (rev-∷ x xs [])) ⟩
  reverse (y ∷ ys) ++ reverse (x ∷ xs) ∎

reverse-∷ : ∀ {x ys} → Tree x → Forest ys →
            reverse (x ∷ ys) ≡ reverse ys ++ (x ∷ [])
reverse-∷ {x} Tx fnil =
  rev (x ∷ []) []
    ≡⟨ rev-∷ x [] [] ⟩
  rev [] (x ∷ [])
    ≡⟨ rev-[] (x ∷ []) ⟩
  x ∷ []
    ≡⟨ sym (++-leftIdentity (x ∷ [])) ⟩
  [] ++ x ∷ []
     ≡⟨ ++-leftCong (sym (rev-[] [])) ⟩
  rev [] [] ++ x ∷ [] ∎

reverse-∷ {x} Tx (fcons {y} {ys} Ty Fys) = sym (
  reverse (y ∷ ys) ++ x ∷ []
    ≡⟨ ++-rightCong (sym (reverse-[x]≡[x] x)) ⟩
  (reverse (y ∷ ys) ++ reverse (x ∷ []))
    ≡⟨ sym (reverse-++ (fcons Tx fnil) (fcons Ty Fys)) ⟩
  reverse ((x ∷ []) ++ (y ∷ ys))
     ≡⟨ reverseCong (++-∷ x [] (y ∷ ys)) ⟩
   reverse (x ∷ ([] ++ (y ∷ ys)))
     ≡⟨ reverseCong (∷-rightCong (++-leftIdentity (y ∷ ys))) ⟩
   reverse (x ∷ y ∷ ys) ∎
  )