text:
-- simply-typed labelled λ-calculus w/ DeBruijn indices

-- {-# OPTIONS --show-implicit #-}

module LLC where

open import Agda.Primitive
open import Agda.Builtin.Bool
open import Data.Bool.Properties hiding (≤-trans ; <-trans ; ≤-refl ; <-irrefl)
open import Data.Empty
open import Data.Nat renaming (_+_ to _+ᴺ_ ; _≤_ to _≤ᴺ_ ; _≥_ to _≥ᴺ_ ; _<_ to _<ᴺ_ ; _>_ to _>ᴺ_ ; _≟_ to _≟ᴺ_)
open import Data.Nat.Properties renaming (_<?_ to _<ᴺ?_)
open import Data.Integer renaming (_+_ to _+ᶻ_ ; _≤_ to _≤ᶻ_ ; _≥_ to _≥ᶻ_ ; _<_ to _<ᶻ_ ; _>_ to _>ᶻ_)
open import Data.Integer.Properties using (⊖-≥ ; 0≤n⇒+∣n∣≡n ; +-monoˡ-≤)
open import Data.List
open import Data.List.Relation.Unary.All
open import Relation.Unary using (Decidable)
open import Data.Vec.Relation.Unary.Any
open import Data.Vec.Base hiding (length ; _++_ ; foldr)
open import Relation.Binary.PropositionalEquality renaming (trans to ≡-trans)
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation
open import Data.Fin
open import Data.Fin.Subset renaming (∣_∣ to ∣_∣ˢ)
open import Data.Fin.Subset.Properties using (anySubset?)
open import Data.Fin.Properties using (any?)
open import Data.Product
open import Data.Sum
open import Function

open import Extensionality
open import Auxiliary

module defs where
  data Exp {n : ℕ} : Set where
    Var : ℕ → Exp {n}
    Abs : Exp {n} → Exp {n}
    App : Exp {n} → Exp {n} → Exp {n}
    LabI : Fin n → Exp {n}
    LabE : {s : Subset n} → (f : ∀ l → l ∈ s → Exp {n}) → Exp {n} → Exp {n}

  data Ty {n : ℕ} : Set where
    Fun : Ty {n} → Ty {n} → Ty
    Label : Subset n → Ty

  -- shifting and substitution

  -- shifting, required to avoid variable-capturing in substitution
  -- see Pierce 2002, pg. 78/79
  ↑ᴺ_,_[_] : ℤ → ℕ → ℕ → ℕ
  ↑ᴺ d , c [ x ]
    with (x <ᴺ? c)
  ...  | yes p = x
  ...  | no ¬p = ∣ ℤ.pos x +ᶻ d ∣

  ↑_,_[_] : ∀ {n} → ℤ → ℕ → Exp {n} → Exp
  ↑ d , c [ Var x ] = Var (↑ᴺ d , c [ x ])
  ↑ d , c [ Abs t ] = Abs (↑ d , (ℕ.suc c) [ t ])
  ↑ d , c [ App t t₁ ] = App (↑ d , c [ t ]) (↑ d , c [ t₁ ])
  ↑ d , c [ LabI x ] = LabI x
  ↑ d , c [ LabE f e ] = LabE (λ l x → ↑ d , c [ (f l x) ]) (↑ d , c [ e ])

  -- shorthands
  ↑¹[_] : ∀ {n} → Exp {n} → Exp
  ↑¹[ e ] = ↑ (ℤ.pos 1) , 0 [ e ]

  ↑⁻¹[_] : ∀ {n} → Exp {n} → Exp
  ↑⁻¹[ e ] = ↑ (ℤ.negsuc 0) , 0 [ e ]

  -- substitution
  -- see Pierce 2002, pg. 80
  [_↦_]_ : ∀ {n} → ℕ → Exp {n} → Exp → Exp
  [ k ↦ s ] Var x
    with (_≟ᴺ_ x k)
  ...  | yes p = s
  ...  | no ¬p = Var x
  [ k ↦ s ] Abs t = Abs ([ ℕ.suc k ↦ ↑¹[ s ] ] t)
  [ k ↦ s ] App t t₁ = App ([ k ↦ s ] t) ([ k ↦ s ] t₁)
  [ k ↦ s ] LabI ins = LabI ins
  [ k ↦ s ] LabE f e = LabE (λ l x → [ k ↦ s ] (f l x)) ([ k ↦ s ] e)

  -- variable in expression
  data _∈`_ {N : ℕ} : ℕ → Exp {N} → Set where
    in-Var : {n : ℕ} → n ∈` Var n
    in-Abs : {n : ℕ} {e : Exp} → (ℕ.suc n) ∈` e → n ∈` Abs e
    in-App : {n : ℕ} {e e' : Exp} → n ∈` e ⊎ n ∈` e' → n ∈` App e e'
    in-LabE : {n : ℕ} {s : Subset N} {f : (∀ l → l ∈ s → Exp {N})} {e : Exp {N}} → (∃₂ λ l i → n ∈` (f l i)) ⊎ n ∈` e → n ∈` LabE {N} {s} f e

  -- typing

  Env : {ℕ} → Set
  Env {n} = List (Ty {n})

  data _∶_∈_ {n : ℕ} : ℕ → Ty {n} → Env {n} → Set where
    here : {T : Ty} {Γ : Env} → 0 ∶ T ∈ (T ∷ Γ)
    there : {n : ℕ} {T₁ T₂ : Ty} {Γ : Env} → n ∶ T₁ ∈ Γ → (ℕ.suc n) ∶ T₁ ∈ (T₂ ∷ Γ)

  data _⊢_∶_ {n : ℕ} : Env {n} → Exp {n} → Ty {n} → Set where
    TVar : {m : ℕ} {Γ : Env} {T : Ty} → m ∶ T ∈ Γ → Γ ⊢ (Var m) ∶ T
    TAbs : {Γ : Env} {T₁ T₂ : Ty} {e : Exp} → (T₁ ∷ Γ) ⊢ e ∶ T₂ → Γ ⊢ (Abs e) ∶ (Fun T₁ T₂)
    TApp : {Γ : Env} {T₁ T₂ : Ty} {e₁ e₂ : Exp} → Γ ⊢ e₁ ∶ (Fun T₁ T₂) → Γ ⊢ e₂ ∶ T₁ → Γ ⊢ (App e₁ e₂) ∶ T₂
    TLabI : {Γ : Env} {x : Fin n} {s : Subset n} → (ins : x ∈ s) → Γ ⊢ LabI x ∶ Label {n} s
    TLabEl : {Γ : Env} {T : Ty} {s : Subset n} {x : Fin n} {ins : x ∈ s} {f : ∀ l → l ∈ s → Exp} {scopecheck : ∀ l i n → n ∈` (f l i) → n <ᴺ length Γ}
                                                                                → Γ ⊢ f x ins ∶ T
                                                                                → Γ ⊢ LabI {n} x ∶ Label {n} s
                                                                                → Γ ⊢ LabE {n} {s} f (LabI {n} x) ∶ T
    TLabEx : {Γ : Env} {T : Ty} {m : ℕ} {s : Subset n} {f : ∀ l → l ∈ s → Exp} → (f' : ∀ l i → (Γ ⊢ [ m ↦ (LabI l) ] (f l i) ∶ T))
                                                                               → Γ ⊢ Var m ∶ Label {n} s
                                                                               → Γ ⊢ LabE {n} {s} f (Var m) ∶ T

-- denotational semantics
module denotational where
  open defs

  Val : {n : ℕ} → Ty {n} → Set
  Val (Fun Ty₁ Ty₂) = (Val Ty₁) → (Val Ty₂)
  Val {n} (Label s) = Σ (Fin n) (λ x → x ∈ s)

  access : {n m : ℕ} {Γ : Env {n}} {T : Ty {n}} → m ∶ T ∈ Γ → All Val Γ → Val T
  access here (V ∷ Γ) = V
  access (there J) (V ∷ Γ) = access J Γ

  eval : {n : ℕ} {Γ : Env {n}} {T : Ty {n}} {e : Exp {n}} → Γ ⊢ e ∶ T → All Val Γ → Val T
  eval (TVar c) Val-Γ = access c Val-Γ
  eval (TAbs TJ) Val-Γ = λ V → eval TJ (V ∷ Val-Γ)
  eval (TApp TJ TJ₁) Val-Γ = (eval TJ Val-Γ) (eval TJ₁ Val-Γ)
  eval (TLabI {x = x} ins) Val-Γ = x , ins
  eval (TLabEl {x = x}{ins = ins}{f = f} j j') Val-Γ = eval j Val-Γ
  eval (TLabEx {m = m}{s}{f} f' j) Val-Γ
    with eval j Val-Γ    -- evaluate variable
  ... | x , ins = eval (f' x ins) Val-Γ

-- operational semantics (call-by-value)
module operational where
  open defs

  data Val {n : ℕ} : Exp {n} → Set where
    VFun : {e : Exp} → Val (Abs e)
    VLab : {x : Fin n} → Val (LabI x)

  -- reduction relation
  data _⇒_ {n : ℕ} : Exp {n} → Exp {n} → Set where
    ξ-App1 : {e₁ e₁' e₂ : Exp} → e₁ ⇒ e₁' → App e₁ e₂ ⇒ App e₁' e₂
    ξ-App2 : {e e' v : Exp} → Val v → e ⇒ e' → App v e ⇒ App v e'
    β-App : {e v : Exp} → Val v → (App (Abs e) v) ⇒ (↑⁻¹[ ([ 0 ↦ ↑¹[ v ] ] e) ])
    β-LabE : {s : Subset n} {f : ∀ l → l ∈ s → Exp} {x : Fin n} → (ins : x ∈ s) → LabE f (LabI x) ⇒ f x ins

  ---- properties & lemmas

  --- properties of shifting

  --  ∣ + x +ᶻ k ∣ +ᴺ m ≡ ∣ + (x +ᴺ m) +ᶻ k ∣
  aux-calc-1 : {x m : ℕ} {k : ℤ} → k >ᶻ + 0 → ∣ + x +ᶻ k ∣ +ᴺ m ≡ ∣ + (x +ᴺ m) +ᶻ k ∣
  aux-calc-1 {x} {m} {+_ n} ge
    rewrite (+-assoc x n m)
          | (+-comm n m)
          | (sym (+-assoc x m n))
          = refl

  ↑ᴺk,l[x]+m≡↑ᴺk,l+m[x+m] : {k : ℤ} {l x m : ℕ} → k >ᶻ + 0 → ↑ᴺ k , l [ x ] +ᴺ m ≡ ↑ᴺ k , l +ᴺ m [ x +ᴺ m ]
  ↑ᴺk,l[x]+m≡↑ᴺk,l+m[x+m] {k} {l} {x} {m} ge
    with x <ᴺ? l
  ...  | yes p
       with x +ᴺ m <ᴺ? l +ᴺ m
  ...     | yes q = refl
  ...     | no ¬q = contradiction (+-monoˡ-< m p) ¬q
  ↑ᴺk,l[x]+m≡↑ᴺk,l+m[x+m] {k} {l} {x} {m} ge
       | no ¬p
       with x +ᴺ m <ᴺ? l +ᴺ m
  ...     | yes q = contradiction q (<⇒≱ (+-monoˡ-< m (≰⇒> ¬p)))
  ...     | no ¬q = aux-calc-1 ge

  -- corollary for suc
  suc[↑ᴺk,l[x]]≡↑ᴺk,sucl[sucx] : {k : ℤ} {l x : ℕ} → k >ᶻ + 0 → ℕ.suc (↑ᴺ k , l [ x ]) ≡ ↑ᴺ k , ℕ.suc l [ ℕ.suc x ]
  suc[↑ᴺk,l[x]]≡↑ᴺk,sucl[sucx] {k} {l} {x} ge
    with  (↑ᴺk,l[x]+m≡↑ᴺk,l+m[x+m] {k} {l} {x} {1} ge)
  ...  | w
       rewrite (n+1≡sucn{↑ᴺ k , l [ x ]})
             | (n+1≡sucn{x})
             | (n+1≡sucn{l})
             = w

  ↑-var-refl : {n : ℕ} {d : ℤ} {c : ℕ} {x : ℕ} {le : ℕ.suc x ≤ᴺ c} → ↑ d , c [ Var {n} x ] ≡ Var x
  ↑-var-refl {n} {d} {c} {x} {le}
    with (x <ᴺ? c)
  ...  | no ¬p = contradiction le ¬p
  ...  | yes p = refl

  ↑¹-var : {n x : ℕ} → ↑¹[ Var {n} x ] ≡ Var (ℕ.suc x)
  ↑¹-var {n} {zero} = refl
  ↑¹-var {n} {ℕ.suc x}
    rewrite (sym (n+1≡sucn{x +ᴺ 1}))
          | (sym (n+1≡sucn{x}))
          = cong ↑¹[_] (↑¹-var{n}{x})

  ↑⁻¹ₖ[↑¹ₖ[s]]≡s : {n : ℕ} {e : Exp {n} } {k : ℕ} → ↑ -[1+ 0 ] , k [ ↑ + 1 , k [ e ] ] ≡ e
  ↑⁻¹ₖ[↑¹ₖ[s]]≡s {n} {Var x} {k}
    with (x <ᴺ? k)
  -- x < k
  --  => ↑⁻¹ₖ(↑¹ₖ(Var n)) = ↑⁻¹ₖ(Var n) = Var n
  ...  | yes p = ↑-var-refl{n}{ -[1+ 0 ]}{k}{x}{p}
  -- x ≥ k
  --  => ↑⁻¹ₖ(↑¹ₖ(Var n)) = ↑⁻¹ₖ(Var |n + 1|) = Var (||n + 1| - 1|) = Var n
  ...  | no ¬p
       with (¬[x≤k]⇒¬[sucx≤k] ¬p)
  ...     | ¬p'
          with (x +ᴺ 1) <ᴺ? k
  ...        | yes pp = contradiction pp ¬p'
  ...        | no ¬pp
             rewrite (∣nℕ+1⊖1∣≡n{x})
                   = refl
  ↑⁻¹ₖ[↑¹ₖ[s]]≡s {n} {Abs e} {k} = cong Abs ↑⁻¹ₖ[↑¹ₖ[s]]≡s
  ↑⁻¹ₖ[↑¹ₖ[s]]≡s {n} {App e e₁} = cong₂ App ↑⁻¹ₖ[↑¹ₖ[s]]≡s ↑⁻¹ₖ[↑¹ₖ[s]]≡s
  ↑⁻¹ₖ[↑¹ₖ[s]]≡s {n} {LabI ins} = refl
  ↑⁻¹ₖ[↑¹ₖ[s]]≡s {n} {LabE f e} = cong₂ LabE (f-ext (λ x → f-ext (λ ins →  ↑⁻¹ₖ[↑¹ₖ[s]]≡s)))  ↑⁻¹ₖ[↑¹ₖ[s]]≡s

  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] : {n : ℕ} {k l : ℤ} {c : ℕ} {s : Exp {n}} → l ≥ᶻ +0 → ↑ k , c [ ↑ l , c [ s ] ] ≡ ↑ (l +ᶻ k) , c [ s ]
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {n} {k} {l} {c} {Var x} ge
    with x <ᴺ? c
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {n} {k} {l} {c} {Var x} ge | no ¬p
      with ∣ + x +ᶻ l ∣ <ᴺ? c
  ...    | yes q = contradiction q (<⇒≱ (n≤m⇒n<sucm (≤-trans (≮⇒≥ ¬p) (m≥0⇒∣n+m∣≥n ge))))
  ...    | no ¬q
         rewrite (0≤n⇒+∣n∣≡n{+ x +ᶻ l} (m≥0⇒n+m≥0 ge))
               | (Data.Integer.Properties.+-assoc (+_ x) l k)
               = refl
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {n} {k} {l} {c} {Var x} ge | yes p
      with x <ᴺ? c
  ...    | yes p' = refl
  ...    | no ¬p' = contradiction p ¬p'
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {n} {k} {l} {c} {Abs s} le = cong Abs (↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s]{n}{k}{l}{ℕ.suc c}{s} le)
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {n} {k} {l} {c} {App s s₁} le = cong₂ App  (↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s]{n}{k}{l}{c}{s} le)  (↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s]{n}{k}{l}{c}{s₁} le)
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {n} {k} {l} {c} {LabI ins} le = refl
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {n} {k} {l} {c} {LabE f e} le = cong₂ LabE (f-ext (λ x → f-ext (λ ins → ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {n} {k} {l} {c} {f x ins} le))) ( ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {n} {k} {l} {c} {e} le)

  ↑k,q[↑l,c[s]]≡↑l+k,c[s] : {n : ℕ} {k l : ℤ} {q c : ℕ} {s : Exp {n}} →  + q ≤ᶻ + c +ᶻ l → c ≤ᴺ q → ↑ k , q [ ↑ l , c [ s ] ] ≡ ↑ (l +ᶻ k) , c [ s ]
  ↑k,q[↑l,c[s]]≡↑l+k,c[s] {n} {k} {l} {q} {c} {Var x} ge₁ ge₂
    with x <ᴺ? c
  ... | yes p
      with x <ᴺ? q
  ...    | yes p' = refl
  ...    | no ¬p' = contradiction (≤-trans p ge₂) ¬p'
  ↑k,q[↑l,c[s]]≡↑l+k,c[s] {n} {k} {l} {q} {c} {Var x} ge₁ ge₂
      | no ¬p
      with ∣ + x +ᶻ l ∣ <ᴺ? q
  ...    | yes p' = contradiction p' (≤⇒≯ (+a≤b⇒a≤∣b∣{q}{+ x +ᶻ l} (Data.Integer.Properties.≤-trans ge₁ ((Data.Integer.Properties.+-monoˡ-≤ l (+≤+ (≮⇒≥ ¬p)))))))
  ...    | no ¬p'
         rewrite (0≤n⇒+∣n∣≡n{+ x +ᶻ l} (Data.Integer.Properties.≤-trans (+≤+ z≤n) ((Data.Integer.Properties.≤-trans ge₁ ((Data.Integer.Properties.+-monoˡ-≤ l (+≤+ (≮⇒≥ ¬p))))))))
               | (Data.Integer.Properties.+-assoc (+_ x) l k)
               = refl
  ↑k,q[↑l,c[s]]≡↑l+k,c[s] {n} {k} {l} {q} {c} {Abs s} ge₁ ge₂ = cong Abs (↑k,q[↑l,c[s]]≡↑l+k,c[s] {n} {k} {l} {ℕ.suc q} {ℕ.suc c} {s} (+q≤+c+l⇒+1q≤+1c+l{q}{c}{l} ge₁) (s≤s ge₂))
  ↑k,q[↑l,c[s]]≡↑l+k,c[s] {n} {k} {l} {q} {c} {App s s₁} ge₁ ge₂ = cong₂ App (↑k,q[↑l,c[s]]≡↑l+k,c[s] {n} {k} {l} {q} {c} {s} ge₁ ge₂) (↑k,q[↑l,c[s]]≡↑l+k,c[s]{n} {k} {l} {q} {c} {s₁} ge₁ ge₂)
  ↑k,q[↑l,c[s]]≡↑l+k,c[s] {n} {k} {l} {q} {c} {LabI e} ge₁ ge₂ = refl
  ↑k,q[↑l,c[s]]≡↑l+k,c[s] {n} {k} {l} {q} {c} {LabE f e} ge₁ ge₂ = cong₂ LabE (f-ext (λ x → f-ext (λ ins → ↑k,q[↑l,c[s]]≡↑l+k,c[s] {n} {k} {l} {q} {c} {f x ins} ge₁ ge₂))) (↑k,q[↑l,c[s]]≡↑l+k,c[s] {n} {k} {l} {q} {c} {e} ge₁ ge₂)

  aux-calc-2 : {x l : ℕ} {k : ℤ} → k >ᶻ + 0 → ∣ + (x +ᴺ l) +ᶻ k ∣ ≡ ∣ + x +ᶻ k ∣ +ᴺ l
  aux-calc-2 {x} {l} {+_ n} ge
    rewrite (+-assoc x l n)
          | (+-comm l n)
          | (+-assoc x n l)
          = refl

  ↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] : {n : ℕ} {k : ℤ} {q c l : ℕ} {s : Exp {n}} → c ≤ᴺ q → + 0 <ᶻ k →  ↑ k , q +ᴺ l [ ↑ + l , c [ s ] ] ≡ ↑ + l , c [ ↑ k , q [ s ] ]
  ↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {q} {c} {l} {Var x} le le'
    with x <ᴺ? q
  ...  | yes p
       with x <ᴺ? c
  ...     | yes p'
          with x <ᴺ? q +ᴺ l
  ...        | yes p'' = refl
  ...        | no ¬p'' = contradiction (≤-stepsʳ l p) ¬p''
  ↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {q} {c} {l} {Var x} le le'
       | yes p
          | no ¬p'
          with x +ᴺ l <ᴺ? q +ᴺ l
  ...        | yes p'' = refl
  ...        | no ¬p'' = contradiction (Data.Nat.Properties.+-monoˡ-≤ l p) ¬p''
  ↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {q} {c} {l} {Var x} le le'
       | no ¬p
       with x <ᴺ? c
  ...     | yes p' = contradiction p' (<⇒≱ (a≤b<c⇒a<c le (≰⇒> ¬p)))
  ...     | no ¬p'
          with x +ᴺ l <ᴺ? q +ᴺ l
             | ∣ + x +ᶻ k ∣ <ᴺ? c
  ...        | _ | yes p''' = contradiction p''' (<⇒≱ (a≤b<c⇒a<c (≰⇒≥ ¬p') (s≤s (m>0⇒∣n+m∣>n {x} {k} le'))))
  ...        | yes p'' | _ = contradiction p'' (<⇒≱ (+-monoˡ-< l (≰⇒> ¬p)))
  ...        | no ¬p'' | no ¬p''' = cong Var (aux-calc-2 {x} {l} {k} le')
  ↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {q} {c} {l} {Abs s} le le' = cong Abs (↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {ℕ.suc q} {ℕ.suc c} {l} {s} (s≤s le) le')
  ↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {q} {c} {l} {App s s₁} le le' = cong₂ App (↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {q} {c} {l} {s} le le') (↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {q} {c} {l} {s₁} le le')
  ↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {q} {c} {l} {LabI x} le le' = refl
  ↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {q} {c} {l} {LabE f s} le le' = cong₂ LabE (f-ext (λ x → f-ext (λ ins → ↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {q} {c} {l} {f x ins} le le'))) (↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]] {n} {k} {q} {c} {l} {s} le le')

  -- corollary
  ↑k,sucq[↑1,c[s]]≡↑1,c[↑k,q[s]] : {n : ℕ} {k : ℤ} {q c : ℕ} {s : Exp {n}} → c ≤ᴺ q → + 0 <ᶻ k →  ↑ k , ℕ.suc q [ ↑ + 1 , c [ s ] ] ≡ ↑ + 1 , c [ ↑ k , q [ s ] ]
  ↑k,sucq[↑1,c[s]]≡↑1,c[↑k,q[s]] {n} {k} {q} {c} {s} le le'
    rewrite (sym (n+1≡sucn{q}))
          = ↑k,q+l[↑l,c[s]]≡↑l,c[↑k,q[s]]{n}{k}{q}{c}{1}{s} le le'

  ↑Lab-triv : {n : ℕ} {l : Fin n} (k : ℤ) (q : ℕ) → LabI l ≡ ↑ k , q [ LabI l ]
  ↑Lab-triv {n} {l} k q = refl

  ↑ᴺ-triv : {m : ℤ} {n x : ℕ} → x ≥ᴺ n → ↑ᴺ m , n [ x ] ≡ ∣ + x +ᶻ m ∣
  ↑ᴺ-triv {m} {n} {x} ge
    with x <ᴺ? n
  ... | yes p = contradiction p (≤⇒≯ ge)
  ... | no ¬p = refl

  ↑ᴺ⁰-refl : {n : ℕ} {c : ℕ} {x : ℕ} → ↑ᴺ + 0 , c [ x ] ≡ x
  ↑ᴺ⁰-refl {n} {c} {x}
    with x <ᴺ? c
  ...  | yes p = refl
  ...  | no ¬p = +-identityʳ x

  ↑⁰-refl : {n : ℕ} {c : ℕ} {e : Exp {n}} → ↑ + 0 , c [ e ] ≡ e
  ↑⁰-refl {n} {c} {Var x} = cong Var (↑ᴺ⁰-refl{n}{c}{x})
  ↑⁰-refl {n} {c} {Abs e} = cong Abs (↑⁰-refl{n}{ℕ.suc c}{e})
  ↑⁰-refl {n} {c} {App e e₁} = cong₂ App (↑⁰-refl{n}{c}{e}) (↑⁰-refl{n}{c}{e₁})
  ↑⁰-refl {n} {c} {LabI x} = refl
  ↑⁰-refl {n} {c} {LabE x e} = cong₂ LabE (f-ext (λ l → f-ext λ i → ↑⁰-refl{n}{c}{x l i})) (↑⁰-refl{n}{c}{e})

  --- properties of substitution

  subst-trivial : {n : ℕ} {x : ℕ} {s : Exp {n}} → [ x ↦ s ] Var x ≡ s
  subst-trivial {n} {x} {s}
    with x Data.Nat.≟ x
  ...  | no ¬p = contradiction refl ¬p
  ...  | yes p = refl

  var-subst-refl : {N n m : ℕ} {neq : n ≢ m} {e : Exp {N}} → [ n ↦ e ] (Var m) ≡ (Var m)
  var-subst-refl {N} {n} {m} {neq} {e}
    with _≟ᴺ_ n m
       | map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (Data.Bool.Properties.T? (m ≡ᵇ n))
  ...  | yes p | _ = contradiction p neq
  ...  | no ¬p | yes q = contradiction q (≢-sym ¬p)
  ...  | no ¬p | no ¬q = refl

  -- inversive lemma for variable in expression relation
  inv-in-var : {N n m : ℕ} → _∈`_ {N} n (Var m) → n ≡ m
  inv-in-var {N} {n} {.n} in-Var = refl
  inv-in-abs : {N n : ℕ} {e : Exp {N}} → _∈`_ {N} n (Abs e) → (ℕ.suc n) ∈` e
  inv-in-abs {N} {n} {e} (in-Abs i) = i
  inv-in-app : {N n : ℕ} {e e' : Exp {N}} → _∈`_ {N} n (App e e') → (_∈`_ n e ⊎ _∈`_ n e')
  inv-in-app {N} {n} {e} {e'} (in-App d) = d
  inv-in-labe : {N n : ℕ} {s : Subset N} {f : (∀ l → l ∈ s → Exp {N})} {e : Exp {N}} → _∈`_ {N} n (LabE {N} {s} f e) → (∃₂ λ l i → n ∈` (f l i)) ⊎ n ∈` e
  inv-in-labe {N} {n} {s} {f} {e} (in-LabE d) = d

  notin-shift : {N n k q : ℕ} {e : Exp {N}} → n ≥ᴺ q → ¬ n ∈` e → ¬ ((n +ᴺ k) ∈` ↑ + k , q [ e ])
  notin-shift {N} {n} {k} {q} {Var x} geq j z
    with x <ᴺ? q
  ...  | no ¬p
       with x ≟ᴺ n
  ...     | yes p' rewrite p' = contradiction in-Var j
  ...     | no ¬p'
          with cong (_∸ k) (inv-in-var z)
  ...        | w
             rewrite (m+n∸n≡m n k)
                   | (m+n∸n≡m x k)
                   = contradiction (sym w) ¬p'
  notin-shift {N} {n} {k} {q} {Var .(n +ᴺ k)} geq j in-Var
       | yes p = contradiction geq (<⇒≱ (≤-trans (s≤s (m≤m+n n k)) p))  -- q ≤ n VS ℕ.suc (n + k) ≤ n
  notin-shift {N} {n} {k} {q} {Abs e} geq j (in-Abs x) = notin-shift (s≤s geq) (λ x₁ → contradiction (in-Abs x₁) j) x
  notin-shift {N} {n} {k} {q} {App e e₁} geq j z
    with dm2 (contraposition in-App j) | (inv-in-app z)
  ...  | fst , snd | inj₁ x = notin-shift geq fst x
  ...  | fst , snd | inj₂ y = notin-shift geq snd y
  notin-shift {N} {n} {k} {q} {LabI x} geq j ()
  notin-shift {N} {n} {k} {q} {LabE f e} geq j z
    with dm2 (contraposition in-LabE j) | (inv-in-labe z)
  ...  | fst , snd | inj₂ y = notin-shift geq snd y
  ...  | fst , snd | inj₁ (fst₁ , fst₂ , snd₁) = notin-shift geq (¬∃⟶∀¬ (¬∃⟶∀¬ fst fst₁) fst₂) snd₁

  -- corollary
  notin-shift-one : {N n : ℕ} {e : Exp{N}} → ¬ n ∈` e → ¬ (ℕ.suc n ∈` ↑¹[ e ])
  notin-shift-one {N} {n} {e} nin rewrite (sym (n+1≡sucn{n})) = notin-shift{N}{n}{1} z≤n nin

  -- if n ∉ fv(e), then substitution of n does not do anything
  subst-refl-notin : {N n : ℕ} {e e' : Exp {N}} → ¬ n ∈` e → [ n ↦ e' ] e ≡ e
  subst-refl-notin {N} {n} {Var x} {e'} nin
    with x ≟ᴺ n
  ...  | yes p rewrite p = contradiction in-Var nin
  ...  | no ¬p = refl
  subst-refl-notin {N} {n} {Abs e} {e'} nin = cong Abs (subst-refl-notin (contraposition in-Abs nin))
  subst-refl-notin {N} {n} {App e e₁} {e'} nin
    with dm2 (contraposition in-App nin)
  ...  | fst , snd = cong₂ App (subst-refl-notin fst) (subst-refl-notin snd)
  subst-refl-notin {N} {n} {LabI x} {e'} nin = refl
  subst-refl-notin {N} {n} {LabE x e} {e'} nin
    with dm2 (contraposition in-LabE nin)
  ...  | fst , snd = cong₂ LabE (f-ext (λ l → f-ext (λ x₁ → subst-refl-notin{e' = e'} (¬∃⟶∀¬ (¬∃⟶∀¬ (fst) l) x₁)))) (subst-refl-notin (snd))

  notin-subst : {N n : ℕ} {e e' : Exp {N}} → ¬ n ∈` e' → ¬ (n ∈` ([ n ↦ e' ] e))
  notin-subst {N} {n} {Var x} {e'} nin
    with x ≟ᴺ n
  ...  | yes p = nin
  ...  | no ¬p = λ x₁ → contradiction (inv-in-var x₁) (≢-sym ¬p)
  notin-subst {N} {n} {Abs e} {e'} nin
    with notin-shift{k = 1} z≤n nin
  ...  | w rewrite (n+1≡sucn{n}) = λ x → notin-subst {n = ℕ.suc n} {e = e} {e' = ↑¹[ e' ]} w  (inv-in-abs x)
  notin-subst {N} {n} {App e e₁} {e'} nin (in-App z)
    with z
  ... | inj₁ x = notin-subst{e = e} nin x
  ... | inj₂ y = notin-subst{e = e₁} nin y
  notin-subst {N} {n} {LabI x} {e'} nin = λ ()
  notin-subst {N} {n} {LabE f e} {e'} nin (in-LabE z)
    with z
  ...  | inj₁ (fst , fst₁ , snd) = notin-subst{e = f fst fst₁} nin snd
  ...  | inj₂ y = notin-subst{e = e} nin y

  subst2-refl-notin : {N n : ℕ} {e e' s : Exp {N}} → ¬ n ∈` e' → [ n ↦ e ] ([ n ↦ e' ] s) ≡ [ n ↦ e' ] s
  subst2-refl-notin {N} {n} {e} {e'} {s} nin = subst-refl-notin (notin-subst{e = s} nin)

  -- if n ∈ [ m ↦ s ] e, n ∉ s, then n ≢ m
  subst-in-neq : {N n m : ℕ} {e s : Exp{N}} → ¬ n ∈` s → n ∈` ([ m ↦ s ] e) → n ≢ m
  subst-in-neq {N} {n} {m} {Var x} {s} nin ins
    with x ≟ᴺ m
  ...  | yes p = contradiction ins nin
  subst-in-neq {N} {.x} {m} {Var x} {s} nin in-Var | no ¬p = ¬p
  subst-in-neq {N} {n} {m} {Abs e} {s} nin (in-Abs ins) = sucn≢sucm⇒n≢m (subst-in-neq{e = e} (notin-shift-one nin) ins)
  subst-in-neq {N} {n} {m} {App e e₁} {s} nin (in-App (inj₁ x)) = subst-in-neq{e = e} nin x
  subst-in-neq {N} {n} {m} {App e e₁} {s} nin (in-App (inj₂ y)) = subst-in-neq{e = e₁} nin y
  subst-in-neq {N} {n} {m} {LabE f e} {s} nin (in-LabE (inj₁ (fst , fst₁ , snd))) = subst-in-neq{e = f fst fst₁} nin snd
  subst-in-neq {N} {n} {m} {LabE f e} {s} nin (in-LabE (inj₂ y)) = subst-in-neq{e = e} nin y

  -- if n ≢ m, n ∈` e, then n ∈` [ m ↦ e' ] e
  subst-in : {N n m : ℕ} {e e' : Exp {N}} → n ≢ m → n ∈` e → n ∈` ([ m ↦ e' ] e)
  subst-in {N} {n} {m} {Var x} {e'} neq (in-Var)
    with n ≟ᴺ m
  ...  | yes p = contradiction p neq
  ...  | no ¬p = in-Var
  subst-in {N} {n} {m} {Abs e} {e'} neq (in-Abs j) = in-Abs (subst-in (n≢m⇒sucn≢sucm neq) j)
  subst-in {N} {n} {m} {App e e₁} {e'} neq (in-App z)
    with z
  ...  | inj₁ x = in-App (inj₁ (subst-in neq x))
  ...  | inj₂ y = in-App (inj₂ (subst-in neq y))
  subst-in {N} {n} {m} {LabE f e} {e'} neq (in-LabE z)
    with z
  ...  | inj₁ (fst , fst₁ , snd) = in-LabE (inj₁ (fst , (fst₁ , (subst-in neq snd))))
  ...  | inj₂ y = in-LabE (inj₂ (subst-in neq y))

  -- if n ≢ m, n ∉ e', n ∈ [ m ↦ e' ] e, then n ∈ e
  subst-in-reverse : {N n m : ℕ} {e e' : Exp {N}} → n ≢ m → ¬ (n ∈` e') → n ∈` ([ m ↦ e' ] e) → n ∈` e
  subst-in-reverse {N} {n} {m} {Var x} {e'} neq nin ins
    with x ≟ᴺ m
  ...  | yes p = contradiction ins nin
  ...  | no ¬p = ins
  subst-in-reverse {N} {n} {m} {Abs e} {e'} neq nin (in-Abs ins) = in-Abs (subst-in-reverse (n≢m⇒sucn≢sucm neq) (notin-shift-one{N}{n}{e'} nin) ins)
  subst-in-reverse {N} {n} {m} {App e e₁} {e'} neq nin (in-App (inj₁ x)) = in-App (inj₁ (subst-in-reverse neq nin x))
  subst-in-reverse {N} {n} {m} {App e e₁} {e'} neq nin (in-App (inj₂ y)) = in-App (inj₂ (subst-in-reverse neq nin y))
  subst-in-reverse {N} {n} {m} {LabE f e} {e'} neq nin (in-LabE (inj₁ (fst , fst₁ , snd))) = in-LabE (inj₁ (fst , (fst₁ , subst-in-reverse{e = f fst fst₁} neq nin snd)))
  subst-in-reverse {N} {n} {m} {LabE f e} {e'} neq nin (in-LabE (inj₂ y)) = in-LabE (inj₂ (subst-in-reverse neq nin y))

  var-env-< : {N : ℕ} {Γ : Env {N}} {T : Ty} {n : ℕ} (j : n ∶ T ∈ Γ) → n <ᴺ (length Γ)
  var-env-< {N} {.(T ∷ _)} {T} {.0} here = s≤s z≤n
  var-env-< {N} {.(_ ∷ _)} {T} {.(ℕ.suc _)} (there j) = s≤s (var-env-< j)

  -- variables contained in a term are < length of env.
  free-vars-env-< : {N : ℕ} {e : Exp {N}} {Γ : Env} {T : Ty {N}} → Γ ⊢ e ∶ T → (∀ n → n ∈` e → n <ᴺ length Γ)
  free-vars-env-< {N} {.(Var n)} {Γ} {T} (TVar x) n in-Var = var-env-< x
  free-vars-env-< {N} {.(Abs _)} {Γ} {(Fun T₁ T₂)} (TAbs j) n (in-Abs ins)
    rewrite (length[A∷B]≡suc[length[B]] {lzero} {Ty} {T₁} {Γ})
          = ≤-pred (free-vars-env-< j (ℕ.suc n) ins)
  free-vars-env-< {N} {App e e'} {Γ} {T} (TApp j j') n (in-App z)
    with z
  ...  | inj₁ x = free-vars-env-< j n x
  ...  | inj₂ y = free-vars-env-< j' n y
--   free-vars-env-< {N} {LabE f (LabI l)} {Γ} {T} (TLabEl{scopecheck = s} j j')
  free-vars-env-< {N} {LabE f (LabI l)} {Γ} {T} (TLabEl{scopecheck = s} j j') n (in-LabE z)
    with z
  ...  | inj₁ (fst , fst₁ , snd) = s fst fst₁ n snd
  ...  | inj₂ ()
  free-vars-env-< {N} {LabE f (Var m)} {Γ} {T} (TLabEx f' (TVar j)) n (in-LabE z)
    with n ≟ᴺ m
  ...  | yes p rewrite p = var-env-< j
  ...  | no ¬p
       with z
  ...     | inj₁ (fst , fst₁ , snd) = free-vars-env-< (f' fst fst₁) n (subst-in ¬p snd)
  ...     | inj₂ (in-Var) = var-env-< j

  -- closed expressions have no free variables
  closed-free-vars : {N : ℕ} {e : Exp {N}} {T : Ty {N}} → [] ⊢ e ∶ T → (∀ n → ¬ (n ∈` e))
  closed-free-vars {N} {Var x} {T} (TVar ())
  closed-free-vars {N} {LabI x} {T} j n ()
  closed-free-vars {N} {Abs e} {.(Fun _ _)} (TAbs j) n (in-Abs x) = contradiction (free-vars-env-< j (ℕ.suc n) x) (≤⇒≯ (s≤s z≤n))
  closed-free-vars {N} {e} {T} j n x = contradiction (free-vars-env-< j n x) (≤⇒≯ z≤n)  -- App & LabE have the same proof

  -- shifting with a threshold above number of free variables has no effect
  shift-env-size : {n : ℕ} {k : ℤ} {q : ℕ} {e : Exp {n}} → (∀ n → n ∈` e → n <ᴺ q) → ↑ k , q [ e ] ≡ e
  shift-env-size {n} {k} {q} {Var x} lmap
    with x <ᴺ? q
  ...  | yes p = refl
  ...  | no ¬p = contradiction (lmap x in-Var) ¬p
  shift-env-size {n} {k} {q} {Abs e} lmap = cong Abs (shift-env-size (extr lmap))
    where extr : (∀ n → n ∈` Abs e → n <ᴺ q) → (∀ n → n ∈` e → n <ᴺ ℕ.suc q)
          extr lmap zero ins = s≤s z≤n
          extr lmap (ℕ.suc n) ins = s≤s (lmap n (in-Abs ins))
  shift-env-size {n} {k} {q} {App e e'} lmap = cong₂ App (shift-env-size (extr lmap)) (shift-env-size(extr' lmap))
    where extr : (∀ n → n ∈` App e e' → n <ᴺ q) → (∀ n → n ∈` e → n <ᴺ q)
          extr lmap n ins = lmap n (in-App (inj₁ ins))
          extr' : (∀ n → n ∈` App e e' → n <ᴺ q) → (∀ n → n ∈` e' → n <ᴺ q)
          extr' lmap n ins = lmap n (in-App (inj₂ ins))
  shift-env-size {n} {k} {q} {LabI x} lmap = refl
  shift-env-size {n} {k} {q} {LabE{s = s} f e} lmap = cong₂ LabE (f-ext λ l' → (f-ext λ x → shift-env-size (extr lmap l' x))) (shift-env-size (extr' lmap))
    where extr : (∀ n → n ∈` LabE f e → n <ᴺ q) → (l : Fin n) → (x : l ∈ s) → (∀ n → n ∈` f l x → n <ᴺ q)
          extr lmap l x n ins = lmap n (in-LabE (inj₁ (l , (x , ins))))
          extr' : (∀ n → n ∈` LabE f e → n <ᴺ q) → (∀ n → n ∈` e → n <ᴺ q)
          extr' lmap n ins = lmap n (in-LabE (inj₂ ins))

  -- shifting has no effect on closed terms (corollary of shift-env-size)
  closed-no-shift : {n : ℕ} {k : ℤ} {q : ℕ} {e : Exp {n}} {T : Ty {n}} → [] ⊢ e ∶ T → ↑ k , q [ e ] ≡ e
  closed-no-shift {n} {k} {zero} {e} {T} j = shift-env-size (free-vars-env-< j)
  closed-no-shift {n} {k} {ℕ.suc q} {e} {T} j = shift-env-size λ n i → <-trans (free-vars-env-< j n i) (s≤s z≤n)

  --
  subst-change-in : {N n m : ℕ} {e s s' : Exp{N}} → ¬ (n ∈` s) × ¬ (n ∈` s') → n ∈` ([ m ↦ s ] e) → n ∈` ([ m ↦ s' ] e)
  subst-change-in {N} {n} {m} {Var x} {s} {s'} (fst , snd) ins
    with x ≟ᴺ m
  ...  | yes eq = contradiction ins fst
  ...  | no ¬eq = ins
  subst-change-in {N} {n} {m} {Abs e} {s} {s'} (fst , snd) (in-Abs ins) = in-Abs (subst-change-in{N}{ℕ.suc n}{ℕ.suc m}{e} (notin-shift-one{N}{n}{s} fst , notin-shift-one{N}{n}{s'} snd) ins)
  subst-change-in {N} {n} {m} {App e e₁} {s} {s'} p (in-App (inj₁ x)) = in-App (inj₁ (subst-change-in{N}{n}{m}{e} p x))
  subst-change-in {N} {n} {m} {App e e₁} {s} {s'} p (in-App (inj₂ y)) = in-App (inj₂ (subst-change-in{N}{n}{m}{e₁} p y))
  subst-change-in {N} {n} {m} {LabE f e} {s} {s'} p (in-LabE (inj₁ (fst , fst₁ , snd))) = in-LabE (inj₁ (fst , (fst₁ , (subst-change-in{N}{n}{m}{f fst fst₁}{s}{s'} p snd))))
  subst-change-in {N} {n} {m} {LabE f e} {s} {s'} p (in-LabE (inj₂ y)) = in-LabE (inj₂ (subst-change-in {N} {n} {m} {e} p y))

  -- swapping of substitutions A & B if variables of A are not free in substitution term of B and vice versa
  subst-subst-swap : {N n m : ℕ} {e e' s : Exp {N}} → n ≢ m → ¬ n ∈` e' → ¬ m ∈` e → [ n ↦ e ] ([ m ↦ e' ] s) ≡ [ m ↦ e' ] ([ n ↦ e ] s)
  subst-subst-swap {N} {n} {m} {e} {e'} {Var x} neq nin nin'
    with x ≟ᴺ m | x ≟ᴺ n
  ...  | yes p | yes p' = contradiction (≡-trans (sym p') p) neq
  ...  | yes p | no ¬p'
       with x ≟ᴺ m
  ...     | yes p'' = subst-refl-notin nin
  ...     | no ¬p'' = contradiction p ¬p''
  subst-subst-swap {N} {n} {m} {e} {e'} {Var x} neq nin nin'
       | no ¬p | yes p'
       with x ≟ᴺ n
  ...     | yes p'' = sym (subst-refl-notin nin')
  ...     | no ¬p'' = contradiction p' ¬p''
  subst-subst-swap {N} {n} {m} {e} {e'} {Var x} neq nin nin'
       | no ¬p | no ¬p'
       with x ≟ᴺ n | x ≟ᴺ m
  ...     | yes p'' | _ = contradiction p'' ¬p'
  ...     | _       | yes p''' = contradiction p''' ¬p
  ...     | no p''  | no ¬p''' = refl
  subst-subst-swap {N} {n} {m} {e} {e'} {Abs s} neq nin nin'
    with (notin-shift{n = n}{1}{0} z≤n nin) | (notin-shift{n = m}{1}{0} z≤n nin')
  ...  | w | w' rewrite (n+1≡sucn{n}) | (n+1≡sucn{m}) = cong Abs (subst-subst-swap{s = s} (n≢m⇒sucn≢sucm neq) w w')
  subst-subst-swap {N} {n} {m} {e} {e'} {App s s₁} neq nin nin' = cong₂ App (subst-subst-swap{s = s} neq nin nin') (subst-subst-swap{s = s₁} neq nin nin')
  subst-subst-swap {N} {n} {m} {e} {e'} {LabI x} neq nin nin' = refl
  subst-subst-swap {N} {n} {m} {e} {e'} {LabE f s} neq nin nin' = cong₂ LabE (f-ext (λ l → f-ext (λ x → subst-subst-swap{s = f l x} neq nin nin' ))) (subst-subst-swap{s = s} neq nin nin')

  -- this should be true for all k, but limiting to positive k makes the proof simpler
  aux-calc-3 : {m x : ℕ} {k : ℤ} → k >ᶻ + 0 → ∣ + m +ᶻ k ∣ ≡ ∣ + x +ᶻ k ∣ → m ≡ x
  aux-calc-3 {m} {x} {+_ n} gt eqv = +-cancelʳ-≡ m x eqv

  aux-calc-4 : {m x : ℕ} {k : ℤ} → k >ᶻ + 0 → m ≤ᴺ x → m <ᴺ ∣ + x +ᶻ k ∣
  aux-calc-4 {m} {x} {+_ zero} (+<+ ())
  aux-calc-4 {m} {x} {+[1+ n ]} (+<+ (s≤s z≤n)) leq = a≤b<c⇒a<c leq (m<m+n x {ℕ.suc n} (s≤s z≤n))

  subst-shift-swap : {n : ℕ} {k : ℤ} {x q : ℕ} {s e : Exp {n}} → k >ᶻ + 0 → ↑ k , q [ [ x ↦ e ] s ] ≡ [ ↑ᴺ k , q [ x ] ↦ ↑ k , q [ e ] ] ↑ k , q [ s ]
  subst-shift-swap {n} {k} {x} {q} {Var m} {e} gt
    with m ≟ᴺ x
  ...  | yes p
       with m <ᴺ? q | x <ᴺ? q
  ...     | yes p' | yes p''
          with m ≟ᴺ x
  ...        | yes p''' = refl
  ...        | no ¬p''' = contradiction p ¬p'''
  subst-shift-swap {n} {k} {x} {q} {Var m} {e} gt
       | yes p | yes p' | no ¬p'' rewrite (cong ℕ.suc p) = contradiction p' ¬p''
  subst-shift-swap {n} {k} {x} {q} {Var m} {e} gt
       | yes p | no ¬p' | yes p'' rewrite (cong ℕ.suc p) = contradiction p'' ¬p'
  subst-shift-swap {n} {k} {x} {q} {Var m} {e} gt
       | yes p | no ¬p' | no ¬p''
       with ∣ + m +ᶻ k ∣ ≟ᴺ ∣ + x +ᶻ k ∣
  ...     | yes p''' = refl
  ...     | no ¬p''' rewrite p = contradiction refl ¬p'''
  subst-shift-swap {n} {k} {x} {q} {Var m} {e} gt
       | no ¬p
       with m <ᴺ? q | x <ᴺ? q
  ...     | yes p' | yes p''
          with m ≟ᴺ x
  ...        | yes p''' = contradiction p''' ¬p
  ...        | no ¬p''' = refl
  subst-shift-swap {n} {k} {x} {q} {Var m} {e} gt
      | no ¬p | yes p' | no ¬p''
      with m ≟ᴺ ∣ + x +ᶻ k ∣
  ...    | yes p''' = contradiction p''' (<⇒≢ (aux-calc-4 gt (≤-pred (≤-trans p' (≰⇒≥ ¬p'')))))
  ...    | no ¬p''' = refl
  subst-shift-swap {n} {k} {x} {q} {Var m} {e} gt
      | no ¬p | no ¬p' | yes p''
      with ∣ + m +ᶻ k ∣ ≟ᴺ x
  ...    | yes p''' = contradiction p''' (≢-sym (<⇒≢ (aux-calc-4{x}{m}{k} gt (≤-pred (≤-trans p'' (≰⇒≥ ¬p'))))))
  ...    | no ¬p''' = refl
  subst-shift-swap {n} {k} {x} {q} {Var m} {e} gt
      | no ¬p | no ¬p' | no ¬p''
      with ∣ + m +ᶻ k ∣ ≟ᴺ ∣ + x +ᶻ k ∣
  ...    | yes p''' = contradiction p''' (contraposition (aux-calc-3 gt) ¬p)
  ...    | no ¬p''' = refl
  subst-shift-swap {n} {k} {x} {q} {Abs s} {e} gt
    with (subst-shift-swap{n}{k}{ℕ.suc x}{ℕ.suc q}{s}{↑¹[ e ]} gt)
  ...  | w
       rewrite (↑k,sucq[↑1,c[s]]≡↑1,c[↑k,q[s]] {n} {k} {q} {0} {e} z≤n gt)
             | (suc[↑ᴺk,l[x]]≡↑ᴺk,sucl[sucx] {k} {q} {x} gt)
             = cong Abs w
  subst-shift-swap {n} {k} {x} {q} {App s₁ s₂} {e} gt = cong₂ App (subst-shift-swap {n} {k} {x} {q} {s₁} {e} gt) (subst-shift-swap {n} {k} {x} {q} {s₂} {e} gt)
  subst-shift-swap {n} {k} {x} {q} {LabI ins} {e} gt = refl
  subst-shift-swap {n} {k} {x} {q} {LabE f s} {e} gt = cong₂ LabE (f-ext (λ l → f-ext (λ ins → subst-shift-swap {n} {k} {x} {q} {f l ins} {e} gt))) (subst-shift-swap {n} {k} {x} {q} {s} {e} gt)

  --- properties and manipulation of environments

  -- type to determine whether var type judgement in env. (Δ ++ Γ) is in Δ or Γ
  data extract-env-or {n : ℕ} {Δ Γ : Env {n}} {T : Ty} {x : ℕ} : Set where
    in-Δ : x ∶ T ∈ Δ → extract-env-or
    -- x ≥ length Δ makes sure that x really is in Γ; e.g.
    -- x = 1, Δ = (S ∷ T), Γ = (T ∷ Γ'); here 1 ∶ T ∈ Δ as well as (1 ∸ 2) ≡ 0 ∶ T ∈ Γ
    in-Γ : (x ≥ᴺ length Δ) → (x ∸ length Δ) ∶ T ∈ Γ → extract-env-or

  extract : {n : ℕ} {Δ Γ : Env {n}} {T : Ty} {x : ℕ} (j : x ∶ T ∈ (Δ ++ Γ)) → extract-env-or{n}{Δ}{Γ}{T}{x}
  extract {n} {[]} {Γ} {T} {x} j = in-Γ z≤n j
  extract {n} {x₁ ∷ Δ} {Γ} {.x₁} {.0} here = in-Δ here
  extract {n} {x₁ ∷ Δ} {Γ} {T} {ℕ.suc x} (there j)
    with extract {n} {Δ} {Γ} {T} {x} j
  ...  | in-Δ j'  = in-Δ (there j')
  ...  | in-Γ ge j'' = in-Γ (s≤s ge) j''

  ext-behind : {n : ℕ} {Δ Γ : Env {n}} {T : Ty} {x : ℕ} → x ∶ T ∈ Δ → x ∶ T ∈ (Δ ++ Γ)
  ext-behind here = here
  ext-behind (there j) = there (ext-behind j)

  ext-front : {N n : ℕ} {Γ Δ : Env{N}} {S : Ty} → n ∶ S ∈ Γ → (n +ᴺ (length Δ)) ∶ S ∈ (Δ ++ Γ)
  ext-front {N} {n} {Γ} {[]} {S} j
    rewrite (n+length[]≡n{A = Ty {N}}{n = n})
          = j
  ext-front {N} {n} {Γ} {T ∷ Δ} {S} j
    rewrite (+-suc n (foldr (λ _ → ℕ.suc) 0 Δ))
          = there (ext-front j)

  swap-env-behind : {n : ℕ} {Γ Δ : Env {n}} {T : Ty} → 0 ∶ T ∈ (T ∷ Γ) → 0 ∶ T ∈ (T ∷ Δ)
  swap-env-behind {n}{Γ} {Δ} {T} j = here

  swap-type : {n : ℕ} {Δ ∇ Γ : Env {n}} {T : Ty} → (length Δ) ∶ T ∈ (Δ ++ T ∷ ∇ ++ Γ) → (length Δ +ᴺ length ∇) ∶ T ∈ (Δ ++ ∇ ++ T ∷ Γ)
  swap-type {n} {Δ} {∇} {Γ} {T} j
    with extract{n}{Δ}{T ∷ ∇ ++ Γ} j
  ...  | in-Δ x = contradiction (var-env-< {n}{Δ} {T} x) (<-irrefl refl)
  ...  | in-Γ le j'
       with extract{n}{T ∷ ∇}{Γ} j'
  ...     | in-Δ j''
          rewrite (n∸n≡0 (length Δ))
                | (sym (length[A++B]≡length[A]+length[B]{lzero}{Ty}{Δ}{∇}))
                | (sym (++-assoc{lzero}{Ty}{Δ}{∇}{T ∷ Γ}))
                = ext-front{n}{0}{T ∷ Γ}{Δ ++ ∇}{T} (swap-env-behind{n}{∇}{Γ}{T} j'')
  ...     | in-Γ le' j''
          rewrite (length[A∷B]≡suc[length[B]]{lzero}{Ty}{T}{∇})
                | (n∸n≡0 (length Δ))
                = contradiction le' (<⇒≱ (s≤s z≤n))

  env-pred : {n : ℕ} {Γ : Env {n}} {S T : Ty} {y : ℕ} {gt : y ≢ 0} → y ∶ T ∈ (S ∷ Γ) → ∣ y ⊖ 1 ∣ ∶ T ∈ Γ
  env-pred {n} {Γ} {S} {.S} {.0} {gt} here = contradiction refl gt
  env-pred {n} {Γ} {S} {T} {.(ℕ.suc _)} {gt} (there j) = j

  env-type-equiv-here : {n : ℕ} {Γ : Env {n}} {S T : Ty} → 0 ∶ T ∈ (S ∷ Γ) → T ≡ S
  env-type-equiv-here {n} {Γ} {S} {.S} here = refl

  env-type-uniq : {N n : ℕ} {Γ : Env {N}} {S T : Ty} → n ∶ T ∈ Γ → n ∶ S ∈ Γ → T ≡ S
  env-type-uniq {N} {.0} {.(S ∷ _)} {S} {.S} here here = refl
  env-type-uniq {N} {(ℕ.suc n)} {(A ∷ Γ)} {S} {T} (there j) (there j') = env-type-uniq {N} {n} {Γ} {S} {T} j j'

  env-type-equiv : {n : ℕ} {Δ ∇ : Env {n}} {S T : Ty} → length Δ ∶ T ∈ (Δ ++ S ∷ ∇) → T ≡ S
  env-type-equiv {n} {Δ} {∇} {S} {T} j
    with extract{n}{Δ}{S ∷ ∇} j
  ...  | in-Δ x = contradiction (var-env-< x) (≤⇒≯ ≤-refl)
  ...  | in-Γ x j'
       rewrite (n∸n≡0 (length Δ))
             = env-type-equiv-here {n} {∇} {S} {T} j'

  env-type-equiv-j : {N : ℕ} {Γ : Env {N}} {S T : Ty} {n : ℕ} → T ≡ S → n ∶ T ∈ Γ → n ∶ S ∈ Γ
  env-type-equiv-j {N} {Γ} {S} {T} {n} eq j
    rewrite eq
          = j

  -- extension of environment

  -- lemma required for ∈`
  ext-∈` : {N m k q : ℕ} {e : Exp {N}} → (∀ n → n ∈` e → n <ᴺ m) → (∀ n → n ∈` ↑ + k , q [ e ] → n <ᴺ m +ᴺ k)
  ext-∈` {N} {m} {k} {q} {Var x} f n ins
    with x <ᴺ? q
  ...  | yes p = ≤-trans (f n ins) (≤-stepsʳ{m}{m} k ≤-refl)
  ext-∈` {N} {m} {k} {q} {Var x} f .(x +ᴺ k) in-Var | no ¬p = Data.Nat.Properties.+-monoˡ-≤ k (f x in-Var)
  ext-∈` {N} {m} {k} {q} {Abs e} f n (in-Abs ins) = ≤-pred (ext-∈` {N} {ℕ.suc m} {k} {ℕ.suc q} {e = e} (extr f) (ℕ.suc n) ins)
    where extr : (∀ n → n ∈` Abs e → n <ᴺ m) → (∀ n → n ∈` e → n <ᴺ ℕ.suc m)
          extr f zero ins = s≤s z≤n
          extr f (ℕ.suc n) ins = s≤s (f n (in-Abs ins))
  ext-∈` {N} {m} {k} {q} {App e e₁} f n (in-App (inj₁ x)) = ext-∈`{N}{m}{k}{q}{e} (extr f) n x
    where extr : (∀ n → n ∈` App e e₁ → n <ᴺ m) → (∀ n → n ∈` e → n <ᴺ m)
          extr f n ins = f n (in-App (inj₁ ins))
  ext-∈` {N} {m} {k} {q} {App e e₁} f n (in-App (inj₂ y)) = ext-∈`{N}{m}{k}{q}{e₁} (extr f) n y
    where extr : (∀ n → n ∈` App e e₁ → n <ᴺ m) → (∀ n → n ∈` e₁ → n <ᴺ m)
          extr f n ins = f n (in-App (inj₂ ins))
  ext-∈` {N} {m} {k} {q} {LabE f₁ e} f n (in-LabE (inj₁ (fst , fst₁ , snd))) = ext-∈`{N}{m}{k}{q}{f₁ fst fst₁} (extr f) n snd
    where extr : (∀ n → n ∈` LabE f₁ e → n <ᴺ m) → (∀ n → n ∈` f₁ fst fst₁ → n <ᴺ m)
          extr f n ins = f n (in-LabE (inj₁ (fst , (fst₁ , ins))))
  ext-∈` {N} {m} {k} {q} {LabE f₁ e} f n (in-LabE (inj₂ y)) = ext-∈`{N}{m}{k}{q}{e} (extr f) n y
    where extr : (∀ n → n ∈` LabE f₁ e → n <ᴺ m) → (∀ n → n ∈` e → n <ᴺ m)
          extr f n ins = f n (in-LabE (inj₂ ins))

  ext : {N : ℕ} {Γ Δ ∇ : Env {N}} {S : Ty} {s : Exp} → (∇ ++ Γ) ⊢ s ∶ S → (∇ ++ Δ ++ Γ) ⊢ ↑ (ℤ.pos (length Δ)) , length ∇ [ s ] ∶ S
  ext {N} {Γ} {Δ} {∇} (TVar {m = n} x)
    with extract{N}{∇}{Γ} x
  ... | in-Δ x₁
      with n <ᴺ? length ∇
  ...    | yes p = TVar (ext-behind x₁)
  ...    | no ¬p = contradiction (var-env-< x₁) ¬p
  ext {N} {Γ} {Δ} {∇} (TVar {m = n} x)
      | in-Γ x₁ x₂
      with n <ᴺ? length ∇
  ...    | yes p = contradiction x₁ (<⇒≱ p)
  ...    | no ¬p
         with (ext-front{N}{n ∸ length ∇}{Γ}{∇ ++ Δ} x₂)
  ...       | w
            rewrite (length[A++B]≡length[A]+length[B]{lzero}{Ty}{∇}{Δ})
                  | (sym (+-assoc (n ∸ length ∇) (length ∇) (length Δ)))
                  | (m∸n+n≡m{n}{length ∇} (≮⇒≥ ¬p))
                  | (++-assoc{lzero}{Ty}{∇}{Δ}{Γ})
                  = TVar w
  ext {N} {Γ} {Δ} {∇} {Fun T₁ T₂} {Abs e} (TAbs j) = TAbs (ext{N}{Γ}{Δ}{T₁ ∷ ∇} j)
  ext {N} {Γ} {Δ} {∇} {S} {App s₁ s₂} (TApp{T₁ = T₁} j₁ j₂) = TApp (ext{N}{Γ}{Δ}{∇}{Fun T₁ S} j₁) (ext{N}{Γ}{Δ}{∇}{T₁} j₂)
  ext {N} {Γ} {Δ} {∇} {S} {LabI l} (TLabI{x = x}{s} ins) = TLabI{x = x}{s} ins
  ext {N} {Γ} {Δ} {∇} {S} {LabE f e} (TLabEl{ins = ins}{f = .f}{scopecheck = s} j j') = TLabEl{ins = ins}
                                                                                {scopecheck = λ l i n x₁ → rw n (ext-∈`{N}{length (∇ ++ Γ)}{length Δ}{length ∇}{f l i} (s l i) n x₁)}
                                                                                (ext{N}{Γ}{Δ}{∇} j) (ext{N}{Γ}{Δ}{∇} j')
    where rw : ∀ n → n <ᴺ length (∇ ++ Γ) +ᴺ length Δ → n <ᴺ length (∇ ++ Δ ++ Γ)
          rw n a rewrite (length[A++B]≡length[A]+length[B]{lzero}{Ty}{∇}{Γ})
                       | (+-assoc (length ∇) (length Γ) (length Δ))
                       | (+-comm (length Γ) (length Δ))
                       | sym (length[A++B]≡length[A]+length[B]{lzero}{Ty}{Δ}{Γ})
                       | sym (length[A++B]≡length[A]+length[B]{lzero}{Ty}{∇}{Δ ++ Γ}) = a
  ext {N} {Γ} {[]} {∇} {S} {LabE f .(Var m)} (TLabEx {s = s} {f = .f} f' (TVar {m = m} x))
    rewrite (↑ᴺ⁰-refl{N}{length ∇}{m})
          | (f-ext (λ l → f-ext (λ i → ↑⁰-refl{N}{length ∇}{f l i})))
          = TLabEx f' (TVar x)
  -- required lemma needs length Δ > 0, hence the case split
  ext {N} {Γ} {t ∷ Δ} {∇} {S} {LabE f .(Var m)} (TLabEx {s = s} {f = .f} f' (TVar {m = m} x))
    with extract{N}{∇}{Γ} x
  ...  | in-Δ x₁
       with m <ᴺ? length ∇
  ...     | no ¬p = contradiction (var-env-< x₁) ¬p
  ...     | yes p
          with (λ l i → ext{N}{Γ}{t ∷ Δ}{∇} (f' l i))
  ...        | w = TLabEx (rw w) (TVar (ext-behind x₁)) -- if m < k, [ m → ↑ₖ x ] (↑ₖ s) ≡ ↑ₖ ([ m ↦ x ] s)

          where rw : ((l : Fin N) → (i : l ∈ s) → (∇ ++ (t ∷ Δ) ++ Γ) ⊢ ↑ + length (t ∷ Δ) , length ∇ [ [ m ↦ LabI l ] (f l i) ] ∶ S)
                   → ((l : Fin N) → (i : l ∈ s) → (∇ ++ (t ∷ Δ) ++ Γ) ⊢ [ m ↦ LabI l ] ↑ + length (t ∷ Δ) , length ∇ [ f l i ] ∶ S)
                rw q l i
                  with q l i
                ...  | w
                     rewrite (subst-shift-swap{N}{+ length (t ∷ Δ)}{m}{length ∇}{f l i}{LabI l} (+<+ (s≤s z≤n)))
                     with m <ᴺ? length ∇
                ...     | yes p = w
                ...     | no ¬p = contradiction p ¬p
  ext {N} {Γ} {t ∷ Δ} {∇} {S} {LabE f .(Var _)} (TLabEx {s = s}{f = .f} f' (TVar{m = m} x))
       | in-Γ x₁ x₂
       with m <ᴺ? length ∇
  ...     | yes p = contradiction x₁ (<⇒≱ p)
  ...     | no ¬p
          with (λ l i → (ext{N}{Γ}{t ∷ Δ}{∇} (f' l i))) | (ext-front{N}{m ∸ length ∇}{Γ}{∇ ++ (t ∷ Δ)} x₂)
  ...        | w | w'
             rewrite (length[A++B]≡length[A]+length[B]{lzero}{Ty}{∇}{t ∷ Δ})
                   | (sym (+-assoc (m ∸ length ∇) (length ∇) (length (t ∷ Δ))))
                   | (m∸n+n≡m{m}{length ∇} (≮⇒≥ ¬p))
                   | (++-assoc{lzero}{Ty}{∇}{t ∷ Δ}{Γ})
                  = TLabEx (rw w) (TVar w')

             where rw : ((l : Fin N) → (i : l ∈ s) → ((∇ ++ (t ∷ Δ) ++ Γ) ⊢ ↑ + length (t ∷ Δ) , length ∇ [ [ m ↦ LabI l ] f l i ] ∶ S))
                      → ((l : Fin N) → (i : l ∈ s) → ((∇ ++ (t ∷ Δ) ++ Γ) ⊢ [ m +ᴺ length (t ∷ Δ) ↦ LabI l ] ↑ + length (t ∷ Δ) , length ∇ [ f l i ] ∶ S))
                   rw q l i
                     with q l i
                   ...  | w
                        rewrite (subst-shift-swap {N} {+ length (t ∷ Δ)} {m} {length ∇} {f l i} {LabI l} (+<+ (s≤s z≤n)))
                        with m <ᴺ? length ∇
                   ...     | yes p = contradiction x₁ (<⇒≱ p)
                   ...     | no ¬p =  w

  ext-empty : {N : ℕ} {Γ : Env {N}} {T : Ty} {e : Exp} → [] ⊢ e ∶ T → Γ ⊢ e ∶ T
  ext-empty {N} {Γ} {T} {e} j
    with ext{N}{[]}{Γ}{[]} j
  ...  | w rewrite (closed-no-shift{N}{+ length Γ}{0}{e}{T} j)
                 | (A++[]≡A{lzero}{Ty}{Γ})
                 = w

  -- uniqueness of ∈
  ∈-eq : {N : ℕ} {s : Subset N} {l : Fin N} → (ins : l ∈ s) → (ins' : l ∈ s) → ins ≡ ins'
  ∈-eq {ℕ.suc n} {.(true ∷ _)} {zero} here here = refl
  ∈-eq {ℕ.suc n} {(x ∷ s)} {Fin.suc l} (there j) (there j') = cong there (∈-eq j j')

  --- general typing properties

  subset-eq : {n : ℕ} {s s' : Subset n} → Label s ≡ Label s' → s ≡ s'
  subset-eq {n} {s} {.s} refl = refl

  ---- progress and preservation

  -- progress theorem, i.e. a well-typed closed expression is either a value
  -- or can be reduced further
  data Progress {n : ℕ} (e : Exp {n}) {T : Ty} {j : [] ⊢ e ∶ T} : Set where
    step : {e' : Exp{n}} → e ⇒ e' → Progress e
    value : Val e → Progress e

  progress : {n : ℕ} (e : Exp {n}) {T : Ty} {j : [] ⊢ e ∶ T} → Progress e {T} {j}
  progress (Var x) {T} {TVar ()}
  progress (Abs e) = value VFun
  progress (App e e₁) {T} {TApp{T₁ = T₁}{T₂ = .T} j j₁}
    with progress e {Fun T₁ T} {j}
  ...  | step x = step (ξ-App1 x)
  ...  | value VFun
       with progress e₁ {T₁} {j₁}
  ...     | step x₁ = step (ξ-App2 VFun x₁)
  ...     | value x₁ = step (β-App x₁)
  progress (LabI ins) {Label s} {TLabI l} = value VLab
  progress (LabE f (LabI l)) {T} {j = TLabEl{ins = ins} f' j} = step (β-LabE ins)
  progress {n} (LabE f (Var m)) {T} {TLabEx f' (TVar ())}

  ---

  preserve-subst' : {n : ℕ} {T S : Ty {n} } {Δ : Env {n}} {e s : Exp {n}} {v : Val s} (j : (Δ ++ S ∷ []) ⊢ e ∶ T) (j' : [] ⊢ s ∶ S)
                                                                           → Δ ⊢ [ length Δ ↦ s ] e ∶ T
  preserve-subst' {n} {T} {S} {Δ} {(Var m)} {s} {v} (TVar{m} x) j'
    with extract{n}{Δ}{S ∷ []}{T}{m} x
  ...  | in-Δ x₁
       with m ≟ᴺ length Δ
  ...     | yes p = contradiction p (<⇒≢ (var-env-< x₁))
  ...     | no ¬p
          with m <ᴺ? length Δ
  ...        | yes p' = TVar x₁
  ...        | no ¬p' = contradiction (var-env-< x₁) ¬p'
  preserve-subst' {n} {T} {S} {Δ} {(Var m)} {s} {v} (TVar{m} x) j'
       | in-Γ x₁ x₂
       with m ≟ᴺ length Δ
  ...     | yes p
          with ext{n}{[]}{Δ} j'
  ...        | w
               rewrite p
                   | (env-type-equiv x)
                   | (closed-no-shift {n} {+ length Δ} {0} {s} j')
                   | (A++[]≡A{lzero}{Ty}{Δ})
                   = w
  preserve-subst' {n} {T} {S} {Δ} {(Var m)} {s} {v} (TVar{m} x) j'
      | in-Γ x₁ x₂ | no ¬p
          with m <ᴺ? length Δ
  ...        | yes p' = contradiction x₁ (<⇒≱ p')
  ...        | no ¬p'
             with (<⇒≱ (≤∧≢⇒< (≤-step (≤∧≢⇒< (≮⇒≥ ¬p') (≢-sym ¬p))) (≢-sym (n≢m⇒sucn≢sucm ¬p))))
  ...           | w  = contradiction (var-env-< x) (aux w)
             where aux : ¬ (ℕ.suc m ≤ᴺ ℕ.suc (length Δ)) → ¬ (ℕ.suc m ≤ᴺ length (Δ ++ S ∷ []))
                   aux t rewrite (length[A++B]≡length[A]+length[B]{A = Δ}{B = S ∷ []}) | (n+1≡sucn{length Δ})  = t
  preserve-subst' {n} {.(Fun _ _)} {S} {Δ} {(Abs e')} {s} {v} (TAbs{T₁ = T₁}{T₂} j) j'
    with preserve-subst'{n}{T₂}{S}{T₁ ∷ Δ}{e'}{s}{v} j j'
  ...  | w
       rewrite (closed-no-shift {n} {+ 1} {0} {s} j')
             = TAbs w
  preserve-subst' {n} {T} {S} {Δ} {(App e e')} {s} {v} (TApp j j₁) j' = TApp (preserve-subst'{v = v} j j') (preserve-subst'{v = v} j₁ j')
  preserve-subst' {n} {T} {S} {Δ} {LabI x} {s} {v} (TLabI ins) j' = TLabI ins
  preserve-subst' {n} {T} {S} {Δ} {LabE{s = s'} f (LabI x)} {s} {v} (TLabEl{ins = ins}{scopecheck = sc} j j') j'' = TLabEl{ins = ins}{scopecheck = scopecheck} (preserve-subst'{v = v} j j'') (TLabI ins)
    where scopecheck : (l : Fin n) (i : l ∈ s') (n' : ℕ) → n' ∈` ([ length Δ ↦ s ] f l i) → n' <ᴺ length Δ
          scopecheck l i n' ins
            with subst-in-neq{n}{n'}{length Δ}{f l i}{s} (closed-free-vars j'' n') ins
          ...  | w
               with (sc l i n' (subst-in-reverse{n}{n'}{length Δ}{e' = s} w (closed-free-vars j'' n') ins))
          ...     | w'
                  rewrite (length[A++B∷[]]≡suc[length[A]]{lzero}{Ty}{Δ}{S}) = ≤∧≢⇒< (≤-pred w') w
  preserve-subst' {n} {T} {.(Fun _ _)} {Δ} {LabE f (Var m)} {Abs e} {VFun} (TLabEx f' (TVar{T = Label s} z)) (TAbs j')
    with m ≟ᴺ length Δ | preserve-subst'{v = VFun} (TVar z) (TAbs j')
  ...  | yes p | _ rewrite p = contradiction (env-type-equiv z) λ ()
  ...  | no ¬p | w = TLabEx (rw (λ l i → preserve-subst'{v = VFun} (f' l i) (TAbs j'))) w
       where rw : ((l : Fin n) (i : l ∈ s) → Δ ⊢ [ length Δ ↦ Abs e ] ([ m ↦ LabI l ] f l i) ∶ T)
                → ((l : Fin n) (i : l ∈ s) → Δ ⊢ [ m ↦ LabI l ] ([ length Δ ↦ Abs e ] f l i) ∶ T)
             rw ρ l i
               with ρ l i
             ...  | w
                  rewrite sym (subst-subst-swap{n}{length Δ}{m}{Abs e}{LabI l}{f l i} (≢-sym ¬p) (λ ()) (closed-free-vars (TAbs j') m)) = w
  preserve-subst' {n} {T} {(Label s')} {Δ} {LabE f (Var m)} {LabI x} {VLab} (TLabEx f' (TVar{T = Label s} z)) (TLabI{s = s'} ins)
    with m ≟ᴺ length Δ | preserve-subst'{v = VLab} (TVar z) (TLabI ins)
  ...  | yes p | w
       rewrite p
             | subset-eq (env-type-equiv z)
             =  TLabEl{f = λ l i → [ length Δ ↦ LabI x ] (f l i)}{scopecheck } (rw{e = f x ins} (preserve-subst'{v = VLab} (f' x ins) (TLabI{s = s'} ins))) w
       where
             -- agda didn't let me rewrite this directly
             rw :  {e : Exp} →  (Δ ⊢ [ length Δ ↦ LabI x ] ([ length Δ ↦ LabI x ] e) ∶ T)
                             → ( Δ ⊢ [ length Δ ↦ LabI x ] e ∶ T)
             rw {e} j
               rewrite sym (subst2-refl-notin{n}{length Δ}{LabI x}{LabI x}{e} (λ ())) = j
             -- if n ∈` [length Δ ↦ LabI x] (f l i), then also n ∈` [length Δ ↦ LabI l] (f l i), since both LabI l and LabI x are closed
             -- if n ∈` [length Δ ↦ LabI l] (f l i), then n < length (Δ ++ (S ∷ [])), we get this from f' ((Δ ++ S ∷ []) ⊢ [length Δ ↦ LabI l] (f l i) ∶ T) and free-vars-env-<
             -- if n ∈` [length Δ ↦ LabI l] (f l i), then also n ≢ (length Δ), since LabI closed
             -- hence n < length (Δ ++ (S ∷ [])) = length Δ + 1 ⇒ n ≤ length Δ, n ≤ length Δ and n ≢ length Δ implies n < length Δ
             scopecheck : (l : Fin n) (i : l ∈ s') (n' : ℕ) → n' ∈` ([ length Δ ↦ LabI x ] f l i) → n' <ᴺ length Δ
             scopecheck l i n' ins
               with (free-vars-env-< (f' l i) n' (subst-change-in{n}{n'}{length Δ}{f l i}{LabI x}{LabI l} ((λ ()) , (λ ())) ins))
             ...  | w
                  rewrite (length[A++B∷[]]≡suc[length[A]]{lzero}{Ty}{Δ}{Label s'})= ≤∧≢⇒< (≤-pred w) (subst-in-neq{n}{n'}{length Δ}{f l i}{LabI x} (λ ()) ins)
  ...  | no ¬p | w = TLabEx (rw λ l i → preserve-subst'{v = VLab} (f' l i) (TLabI ins)) w
       where rw : ((l : Fin n) (i : l ∈ s) → Δ ⊢ [ length Δ ↦ LabI x ] ([ m ↦ LabI l ] f l i) ∶ T)
                → ((l : Fin n) (i : l ∈ s) → Δ ⊢ [ m ↦ LabI l ] ([ length Δ ↦ LabI x ] f l i) ∶ T)
             rw ρ l i
               with ρ l i
             ...  | w
                  rewrite sym (subst-subst-swap{n}{length Δ}{m}{LabI x}{LabI l}{f l i} (≢-sym ¬p) (λ ()) (closed-free-vars (TLabI ins) m)) = w

  preserve' : {n : ℕ} {T : Ty {n}} (e e' : Exp) (j : [] ⊢ e ∶ T) (r : e ⇒ e') → [] ⊢ e' ∶ T
  preserve' {n} {T} .(App e₁ _) .(App e₁' _) (TApp j j') (ξ-App1 {e₁ = e₁} {e₁' = e₁'} r) = TApp (preserve' e₁ e₁' j r) j'
  preserve' {n} {T} .(App _ _) .(App _ _) (TApp j j') (ξ-App2{e = e}{e' = e'} x r) = TApp j (preserve' e e' j' r)
  preserve' {n} {T} (App (Abs e) s') .(↑ -[1+ 0 ] , 0 [ [ 0 ↦ ↑ + 1 , 0 [ s' ] ] e ]) (TApp (TAbs j) j₁) (β-App x)
    rewrite (closed-no-shift {n} {+ 1} {0} {s'} j₁)
          | (closed-no-shift {n} { -[1+ 0 ]} {0} {[ 0 ↦ s' ] e} (preserve-subst'{Δ = []}{v = x} j j₁))
          = preserve-subst'{Δ = []}{v = x} j j₁
  preserve' {n} {T} (LabE f (LabI l)) .(f x ins) (TLabEl{ins = ins'} j j') (β-LabE {x = x} ins) rewrite (∈-eq ins ins') = j

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
{-

This file contains:
  - Path lemmas used in the colimit-equivalence proof.

Verbose, indeed. But should be simple. The length mainly thanks to:
  - Degenerate cubes that seem "obvious", but have to be constructed manually;
  - J rule is cubersome to use, especially when iteratively applied,
    also it is overcomplicated to construct JRefl in nested cases.

-}
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.HITs.James.Inductive.Coherence where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Function

private
  variable
    ℓ ℓ' : Level

-- Lots of degenerate cubes used as intial input to J rule

private
  module _
    {A : Type ℓ}(a : A) where

    degenerate1 : (i j k : I) → A
    degenerate1 i j k =
      hfill (λ k → λ
        { (i = i0) → a
        ; (i = i1) → doubleCompPath-filler (refl {x = a}) refl refl k j
        ; (j = i0) → a
        ; (j = i1) → a})
      (inS a) k

    degenerate1' : (i j k : I) → A
    degenerate1' i j k =
      hfill (λ k → λ
        { (i = i0) → a
        ; (i = i1) → compPath-filler (refl {x = a}) refl k j
        ; (j = i0) → a
        ; (j = i1) → a})
      (inS a) k

    degenerate1'' : (i j k : I) → A
    degenerate1'' i j k =
      hfill (λ k → λ
        { (i = i0) → a
        ; (i = i1) → compPath-filler (refl {x = a}) (refl ∙ refl) k j
        ; (j = i0) → a
        ; (j = i1) → degenerate1 i k i1})
      (inS a) k

    module _
      {B : Type ℓ'}(f : A → B) where

      degenerate2 : (i j k : I) → B
      degenerate2 i j k =
        hfill (λ k → λ
          { (i = i0) → f a
          ; (i = i1) → doubleCompPath-filler (refl {x = f a}) refl refl k j
          ; (j = i0) → f a
          ; (j = i1) → f a })
        (inS (f a)) k

      degenerate3 : (i j k : I) → B
      degenerate3 i j k =
        hfill (λ k → λ
          { (i = i0) → f (doubleCompPath-filler (refl {x = a}) refl refl k j)
          ; (i = i1) → doubleCompPath-filler (refl {x = f a}) refl refl k j
          ; (j = i0) → f a
          ; (j = i1) → f a })
        (inS (f a)) k

      someCommonDegenerateCube : (i j k : I) → B
      someCommonDegenerateCube i j k =
        hcomp (λ l → λ
          { (i = i0) → f a
          ; (i = i1) → degenerate3 k j l
          ; (j = i0) → f a
          ; (j = i1) → f a
          ; (k = i0) → f (degenerate1 i j l)
          ; (k = i1) → degenerate2 i j l })
        (f a)

    degenerate4 : (i j k : I) → A
    degenerate4 i j k =
      hfill (λ k → λ
        { (i = i0) → compPath-filler (refl {x = a}) (refl ∙∙ refl ∙∙ refl) k j
        ; (i = i1) → doubleCompPath-filler (refl {x = a}) refl refl j k
        ; (j = i0) → a
        ; (j = i1) → (refl {x = a} ∙∙ refl ∙∙ refl) k })
      (inS a) k

    degenerate5 : (i j k : I) → A
    degenerate5 i j k =
      hcomp (λ l → λ
        { (i = i0) → compPath-filler (refl {x = a}) (refl ∙∙ refl ∙∙ refl) k j
        ; (i = i1) → doubleCompPath-filler (refl {x = a}) refl refl (j ∧ ~ l) k
        ; (j = i0) → a
        ; (j = i1) → doubleCompPath-filler (refl {x = a}) refl refl (~ i ∨ ~ l) k
        ; (k = i0) → a
        ; (k = i1) → degenerate4 i j i1 })
      (degenerate4 i j k)

    degenerate5' : (i j k : I) → A
    degenerate5' i j k =
      hfill (λ k → λ
        { (i = i0) → doubleCompPath-filler (refl {x = a}) refl (refl ∙ refl) k j
        ; (i = i1) → a
        ; (j = i0) → a
        ; (j = i1) → compPath-filler (refl {x = a}) refl (~ i) k })
      (inS a) k

-- Cubes of which mostly are constructed by J rule

module _
  {A : Type ℓ}{a : A} where

  coh-helper-refl :
    (q' : a ≡ a)(h : refl ≡ q')
    → refl ≡ refl ∙∙ refl ∙∙ q'
  coh-helper-refl q' h i j =
    hcomp (λ k → λ
      { (i = i0) → a
      ; (i = i1) → doubleCompPath-filler refl refl q' k j
      ; (j = i0) → a
      ; (j = i1) → h i k })
    a

  coh-helper' :
    (b : A)(p : a ≡ b)
    (c : A)(q : b ≡ c)
    (q' : b ≡ c)(r : PathP (λ i → p i ≡ q i) p q')
    → refl ≡ (sym q) ∙∙ refl ∙∙ q'
  coh-helper' = J> J> coh-helper-refl

  coh-helper'-Refl1 : coh-helper' _ refl ≡ J> coh-helper-refl
  coh-helper'-Refl1 = transportRefl _

  coh-helper'-Refl2 : coh-helper' _ refl _ refl ≡ coh-helper-refl
  coh-helper'-Refl2 = (λ i → coh-helper'-Refl1 i _ refl) ∙ transportRefl _

  coh-helper :
    {b c : A}(p : a ≡ b)(q q' : b ≡ c)
    (h : PathP (λ i → p i ≡ q i) p q')
    → refl ≡ (sym q) ∙∙ refl ∙∙ q'
  coh-helper p = coh-helper' _ p _

  coh-helper-Refl : coh-helper-refl ≡ coh-helper refl refl
  coh-helper-Refl = sym coh-helper'-Refl2

module _
  {A : Type ℓ}{B : Type ℓ'}{a b c d : A} where

  doubleCompPath-cong-filler :
    {a' b' c' d' : B} (f : A → B)
    {pa : f a ≡ a'}{pb : f b ≡ b'}{pc : f c ≡ c'}{pd : f d ≡ d'}
    (p : a ≡ b)(q : b ≡ c)(r : c ≡ d)
    {p' : a' ≡ b'}{q' : b' ≡ c'}{r' : c' ≡ d'}
    (h   : PathP (λ i → pa i ≡ pb i) (cong f p) p')
    (h'  : PathP (λ i → pb i ≡ pc i) (cong f q) q')
    (h'' : PathP (λ i → pc i ≡ pd i) (cong f r) r')
    → (i j k : I) → B
  doubleCompPath-cong-filler f p q r {p' = p'} {q' = q'} {r' = r'}  h h' h'' i j k =
    hfill (λ k → λ
      { (i = i0) → f (doubleCompPath-filler p q r k j)
      ; (i = i1) → doubleCompPath-filler p' q' r' k j
      ; (j = i0) → h   i (~ k)
      ; (j = i1) → h'' i  k })
    (inS (h' i j)) k

  doubleCompPath-cong : (f : A → B)
    (p : a ≡ b)(q : b ≡ c)(r : c ≡ d)
    → cong f (p ∙∙ q ∙∙ r) ≡ cong f p ∙∙ cong f q ∙∙ cong f r
  doubleCompPath-cong f p q r i j =
    doubleCompPath-cong-filler f
      {pa = refl} {pb = refl} {pc = refl} {pd = refl}
      p q r refl refl refl i j i1

module _
  {A : Type ℓ}{a b c : A} where

  comp-cong-square' :
    (p : a ≡ b)(q : a ≡ c)
    (r : b ≡ c)(h : r ≡ sym p ∙∙ refl ∙∙ q)
    → p ∙ r ≡ q
  comp-cong-square' p q r h i j =
    hcomp (λ k → λ
      { (i = i0) → compPath-filler p r k j
      ; (i = i1) → doubleCompPath-filler (sym p) refl q j k
      ; (j = i0) → a
      ; (j = i1) → h i k })
    (p j)

  module _
    {B : Type ℓ'} where

    comp-cong-square : (f : A → B)
      (p : a ≡ b)(q : b ≡ c)
      → cong f (p ∙ q) ≡ cong f p ∙ cong f q
    comp-cong-square f p q i j =
      hcomp (λ k → λ
        { (i = i0) → f (compPath-filler p q k j)
        ; (i = i1) → compPath-filler (cong f p) (cong f q) k j
        ; (j = i0) → f a
        ; (j = i1) → f (q k) })
      (f (p j))

module _
  {A : Type ℓ}{B : Type ℓ'}{a b c : A}
  (f : A → B)(p : a ≡ b)
  (q : f a ≡ f c)(r : b ≡ c)
  (h : cong f r ≡ sym (cong f p) ∙∙ refl ∙∙ q) where

  comp-cong-helper-filler : (i j k : I) → B
  comp-cong-helper-filler i j k =
    hfill (λ k → λ
      { (i = i0) → comp-cong-square f p r (~ k) j
      ; (i = i1) → q j
      ; (j = i0) → f a
      ; (j = i1) → f c })
    (inS (comp-cong-square' _ _ _ h i j)) k

  comp-cong-helper : cong f (p ∙ r) ≡ q
  comp-cong-helper i j =
    comp-cong-helper-filler i j i1

module _
  {A : Type ℓ}{a : A} where

  push-helper-refl :
    (q' : a ≡ a)(h : refl ≡ q')
    → refl ≡ refl ∙ q'
  push-helper-refl q' h i j =
    hcomp (λ k → λ
      { (i = i0) → a
      ; (i = i1) → compPath-filler refl q' k j
      ; (j = i0) → a
      ; (j = i1) → h i k })
    a

  push-helper' :
    (b : A)(p : a ≡ b)
    (c : A)(q : b ≡ c)
    (q' : c ≡ c)(h : refl ≡ q')
    → PathP (λ i → p i ≡ q i) p (q ∙ q')
  push-helper' = J> J> push-helper-refl

  push-helper'-Refl1 : push-helper' _ refl ≡ J> push-helper-refl
  push-helper'-Refl1 = transportRefl _

  push-helper'-Refl2 : push-helper' _ refl _ refl ≡ push-helper-refl
  push-helper'-Refl2 = (λ i → push-helper'-Refl1 i _ refl) ∙ transportRefl _

  push-helper : {b c : A}
    (p : a ≡ b)(q : b ≡ c)(q' : c ≡ c)(h : refl ≡ q')
    → PathP (λ i → p i ≡ q i) p (q ∙ q')
  push-helper p = push-helper' _ p _

  push-helper-Refl : push-helper-refl ≡ push-helper refl refl
  push-helper-Refl = sym push-helper'-Refl2

module _
  {A : Type ℓ}{B : Type ℓ'}{a : A}(f : A → B) where

  push-helper-cong-Type : {b c : A}
    (p : a ≡ b)(q : b ≡ c)
    (q' : c ≡ c)(sqr : refl ≡ q')
    → Type _
  push-helper-cong-Type p q q' sqr =
    SquareP
      (λ i j → f (push-helper p q _ sqr i j)
          ≡ push-helper (cong f p) (cong f q) _ (λ i j → f (sqr i j)) i j)
      (λ i j → f (p i))
      (λ i j → comp-cong-square f q q' j i)
      (λ i j → f (p i)) (λ i j → f (q i))

  push-helper-cong-refl : push-helper-cong-Type refl refl refl refl
  push-helper-cong-refl =
    transport (λ t →
      SquareP
        (λ i j → f (push-helper-Refl t _ (λ i j → a) i j)
          ≡ push-helper-Refl t _ (λ i j → f a) i j)
        (λ i j → f a)
        (λ i j → comp-cong-square f (refl {x = a}) refl j i)
        (λ i j → f a) (λ i j → f a))
        (λ i j k → someCommonDegenerateCube a f i j k)

  push-helper-cong' :
    (b : A)(p : a ≡ b)
    (c : A)(q : b ≡ c)
    (q' : c ≡ c)(sqr : refl ≡ q')
    → push-helper-cong-Type p q q' sqr
  push-helper-cong' = J> J> J> push-helper-cong-refl

  push-helper-cong : ∀ {b c} p q q' sqr → push-helper-cong-Type {b = b} {c = c} p q q' sqr
  push-helper-cong p = push-helper-cong' _ p _

module _
  {A : Type ℓ}{a : A} where

  push-coh-helper-Type : {b c : A}
    (p : a ≡ b)(q q' : b ≡ c)
    (sqr : PathP (λ i → p i ≡ q i) p q')
    → Type _
  push-coh-helper-Type p q q' sqr =
    SquareP
      (λ i j → push-helper p q _ (coh-helper _ _ _ sqr) i j ≡ sqr i j)
      (λ i j → p i)
      (λ i j → comp-cong-square' q q' _ refl j i)
      (λ i j → p i) (λ i j → q i)

  push-coh-helper-refl' :
    SquareP
      (λ i j → push-helper-refl _ (coh-helper-refl _ (λ i j → a)) i j ≡ a)
      (λ i j → a)
      (λ i j → comp-cong-square' (refl {x = a}) refl _ refl j i)
      (λ i j → a)
      (λ i j → a)
  push-coh-helper-refl' i j k =
    hcomp (λ l → λ
      { (i = i0) → a
      ; (i = i1) → degenerate5 a k j l
      ; (j = i0) → a
      ; (j = i1) → degenerate1 a i l (~ k)
      ; (k = i0) → degenerate1'' a i j l
      ; (k = i1) → a })
    a

  push-coh-helper-refl : push-coh-helper-Type refl refl refl refl
  push-coh-helper-refl =
    transport (λ t →
      SquareP
      (λ i j → push-helper-Refl t _ (coh-helper-Refl t _ (λ i j → a)) i j ≡ a)
      (λ i j → a)
      (λ i j → comp-cong-square' (refl {x = a}) refl _ refl j i)
      (λ i j → a) (λ i j → a)) push-coh-helper-refl'

  push-coh-helper' :
    (b : A)(p : a ≡ b)
    (c : A)(q : b ≡ c)
    (q' : b ≡ c)(sqr : PathP (λ i → p i ≡ q i) p q')
    → push-coh-helper-Type p q q' sqr
  push-coh-helper' = J> J> J> push-coh-helper-refl

  push-coh-helper : ∀ {b c} p q q' sqr → push-coh-helper-Type {b = b} {c = c} p q q' sqr
  push-coh-helper p q q' sqr = push-coh-helper' _ p _ q q' sqr

module _
  {A : Type ℓ}{a : A} where

  push-square-helper-refl :
    refl ∙∙ refl ∙∙ (refl ∙ refl) ≡ refl {x = a}
  push-square-helper-refl i j = degenerate5' a i j i1

  push-square-helper' :
    (b : A)(q  : a ≡ b)
    (c : A)(q' : b ≡ c)
    → sym q ∙∙ refl ∙∙ (q ∙ q') ≡ q'
  push-square-helper' = J> J> push-square-helper-refl

  push-square-helper'-Refl1 : push-square-helper' _ refl ≡ J> push-square-helper-refl
  push-square-helper'-Refl1 = transportRefl _

  push-square-helper'-Refl2 : push-square-helper' _ refl _ refl ≡ push-square-helper-refl
  push-square-helper'-Refl2 = (λ i → push-square-helper'-Refl1 i _ refl) ∙ transportRefl _

  push-square-helper : {b c : A}
    (q : a ≡ b)(q' : b ≡ c)
    → sym q ∙∙ refl ∙∙ (q ∙ q') ≡ q'
  push-square-helper p = push-square-helper' _ p _

  push-square-helper-Refl : push-square-helper-refl ≡ push-square-helper refl refl
  push-square-helper-Refl = sym push-square-helper'-Refl2

module _
  {A : Type ℓ}{a : A} where

  coh-cube-helper-Type :
    {b c : A}(p : a ≡ b)(q : b ≡ c)
    (q' : c ≡ c)(sqr : refl ≡ q')
    → Type _
  coh-cube-helper-Type {c = c} p q q' sqr =
    SquareP
      (λ i j → coh-helper _ _ _ (push-helper p q q' sqr) i j ≡ sqr i j)
      (λ i j → c)
      (λ i j → push-square-helper q q' j i)
      (λ i j → c) (λ i j → c)

  coh-cube-helper-refl' :
    SquareP
      (λ i j → coh-helper-refl _ (push-helper-refl refl (λ i j → a)) i j ≡ a)
      (λ i j → a)
      (λ i j → push-square-helper-refl {a = a} j i)
      (λ i j → a) (λ i j → a)
  coh-cube-helper-refl' i j k =
    hcomp (λ l → λ
      { (i = i0) → a
      ; (i = i1) → degenerate5' a k j l
      ; (j = i0) → a
      ; (j = i1) → degenerate1' a i l (~ k)
      ; (k = i0) → degenerate1'' a i j l
      ; (k = i1) → a })
    a

  coh-cube-helper-refl : coh-cube-helper-Type refl refl refl refl
  coh-cube-helper-refl =
    transport (λ t →
      SquareP
      (λ i j → coh-helper-Refl t _ (push-helper-Refl t refl (λ i j → a)) i j ≡ a)
      (λ i j → a)
      (λ i j → push-square-helper-Refl {a = a} t j i)
      (λ i j → a) (λ i j → a)) coh-cube-helper-refl'

  coh-cube-helper' :
    (b : A)(p : a ≡ b)
    (c : A)(q : b ≡ c)
    (q' : c ≡ c)(sqr : refl ≡ q')
    → coh-cube-helper-Type p q q' sqr
  coh-cube-helper' = J> J> J> coh-cube-helper-refl

  coh-cube-helper : ∀ {b c} p q q' sqr → coh-cube-helper-Type {b = b} {c = c} p q q' sqr
  coh-cube-helper p q q' sqr = coh-cube-helper' _ p _ q q' sqr

module _
  {A : Type ℓ}{B : Type ℓ'}{a : A}(f : A → B) where

  coh-helper-cong-Type : {b c : A}{a' b' c' : B}
    (pa : f a ≡ a')(pb : f b ≡ b')(pc : f c ≡ c')
    {p  : a  ≡ b }(q  r  : b  ≡ c )
    {p' : a' ≡ b'}{q' r' : b' ≡ c'}
    (h   : PathP (λ i → pa i ≡ pb i) (cong f p) p')
    (h'  : PathP (λ i → pb i ≡ pc i) (cong f q) q')
    (h'' : PathP (λ i → pb i ≡ pc i) (cong f r) r')
    (sqr  : PathP (λ i → p  i ≡ q  i) p  r)
    (sqr' : PathP (λ i → p' i ≡ q' i) p' r')
    → Type _
  coh-helper-cong-Type pa pb pc q r h h' h'' sqr sqr' =
    SquareP
      (λ i j → f (coh-helper _ _ _ sqr i j) ≡ coh-helper _ _ _ (λ i j → sqr' i j) i j)
      (λ i j → pc j)
      (λ i j → doubleCompPath-cong-filler f (sym q) refl r (λ i j → h' i (~ j)) (λ i j → pb i) h'' j i i1)
      (λ i j → pc j) (λ i j → pc j)

  coh-helper-cong-refl : coh-helper-cong-Type refl refl refl refl refl refl refl refl refl refl
  coh-helper-cong-refl =
    transport (λ t →
      SquareP
      (λ i j → f (coh-helper-Refl t _ (λ i j → a) i j) ≡ coh-helper-Refl t _ (λ i j → f a) i j)
      (λ i j → f a)
      (λ i j → doubleCompPath-cong-filler f refl refl refl (λ i j → f a) (λ i j → f a) (λ i j → f a) j i i1)
      (λ i j → f a) (λ i j → f a))
      (λ i j k → someCommonDegenerateCube a f i j k)

  coh-helper-cong' :
    (b : A)(p : a ≡ b)
    (c : A)(q : b ≡ c)
    (a' : B)(pa : f a ≡ a')
    (b' : B)(pb : f b ≡ b')
    (c' : B)(pc : f c ≡ c')
    (r : b ≡ c)(sqr  : PathP (λ i → p  i ≡ q  i) p r)
    (p' : a' ≡ b')(h   : PathP (λ i → pa i ≡ pb i) (cong f p) p')
    (q' : b' ≡ c')(h'  : PathP (λ i → pb i ≡ pc i) (cong f q) q')
    (r' : b' ≡ c')(h'' : PathP (λ i → pb i ≡ pc i) (cong f r) r')
    (sqr' : PathP (λ i → p' i ≡ q' i) p' r')
    (hsqr : SquareP (λ i j → h i j ≡ h' i j) (λ i j → f (sqr i j)) sqr' h h'')
    → coh-helper-cong-Type pa pb pc q r h h' h'' sqr sqr'
  coh-helper-cong' = J> J> J> J> J> J> J> J> J> J> coh-helper-cong-refl

  coh-helper-cong :
    ∀ {b c a' b' c' pa pb pc} p q r {p' q' r' h h' h''} sqr {sqr'}
    (hsqr : SquareP (λ i j → f (sqr i j) ≡ sqr' i j)
      (λ i j → h j i) (λ i j → h'' j i) (λ i j → h j i) (λ i j → h' j i))
    → coh-helper-cong-Type {b = b} {c = c} {a' = a'} {b' = b'} {c' = c'}
        pa pb pc q r {p' = p'} {q' = q'} {r' = r'} h h' h'' sqr sqr'
  coh-helper-cong p q r sqr hsqr =
    coh-helper-cong' _ p _ q _ _ _ _ _ _ r sqr _ _ _ _ _ _ _ (λ i j k → hsqr j k i)

ext: agda

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Data.Option.Setoid where

import      Lvl
open import Data
open import Data.Option
open import Functional
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type

private variable ℓ ℓₑ ℓₑₐ : Lvl.Level
private variable A : Type{ℓ}

instance
  Option-equiv : ⦃ equiv : Equiv{ℓₑ}(A) ⦄ → Equiv{ℓₑ}(Option A)
  Equiv._≡_ Option-equiv None     None     = Unit
  Equiv._≡_ Option-equiv None     (Some _) = Empty
  Equiv._≡_ Option-equiv (Some _) None     = Empty
  Equiv._≡_ Option-equiv (Some x) (Some y) = x ≡ y
  Reflexivity.proof  (Equivalence.reflexivity  (Equiv.equivalence Option-equiv)) {None}   = <>
  Reflexivity.proof  (Equivalence.reflexivity  (Equiv.equivalence Option-equiv)) {Some _} = reflexivity(_≡_)
  Symmetry.proof     (Equivalence.symmetry     (Equiv.equivalence Option-equiv)) {None}   {None}   = const(<>)
  Symmetry.proof     (Equivalence.symmetry     (Equiv.equivalence Option-equiv)) {Some _} {Some _} = symmetry(_≡_)
  Transitivity.proof (Equivalence.transitivity (Equiv.equivalence Option-equiv)) {None}   {None}   {None}   = const(const(<>))
  Transitivity.proof (Equivalence.transitivity (Equiv.equivalence Option-equiv)) {Some _} {Some _} {Some _} = transitivity(_≡_)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Nat
open import Prelude
open import core
open import contexts
open import htype-decidable
open import lemmas-matching
open import disjointness

module elaborability where
  mutual
    elaborability-synth : {Γ : tctx} {e : hexp} {τ : htyp} →
                          Γ ⊢ e => τ →
                          Σ[ d ∈ ihexp ] Σ[ Δ ∈ hctx ]
                            (Γ ⊢ e ⇒ τ ~> d ⊣ Δ)
    elaborability-synth SConst = _ , _ , ESConst
    elaborability-synth (SAsc {τ = τ} wt)
      with elaborability-ana wt
    ... | _ , _ , τ' , D  = _ , _ , ESAsc D
    elaborability-synth (SVar x) = _ , _ , ESVar x
    elaborability-synth (SAp dis wt1 m wt2)
      with elaborability-ana (ASubsume wt1 (match-consist m)) | elaborability-ana wt2
    ... | _ , _ , _ , D1 | _ , _ , _ , D2 = _ , _ , ESAp dis (elab-ana-disjoint dis D1 D2) wt1 m D1 D2
    elaborability-synth SEHole = _ , _ , ESEHole
    elaborability-synth (SNEHole new wt)
      with elaborability-synth wt
    ... | d' , Δ' , wt' = _ , _ , ESNEHole (elab-new-disjoint-synth new wt') wt'
    elaborability-synth (SLam x₁ wt)
      with elaborability-synth wt
    ... | d' , Δ' , wt' = _ , _ , ESLam x₁ wt'

    elaborability-ana : {Γ : tctx} {e : hexp} {τ : htyp} →
                         Γ ⊢ e <= τ →
                          Σ[ d ∈ ihexp ] Σ[ Δ ∈ hctx ] Σ[ τ' ∈ htyp ]
                            (Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ)
    elaborability-ana {e = e} (ASubsume D x₁)
      with elaborability-synth D
    -- these cases just pass through, but we need to pattern match so we can prove things aren't holes
    elaborability-ana {e = c} (ASubsume D x₁)                    | _ , _ , D' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) D' x₁
    elaborability-ana {e = e ·: x} (ASubsume D x₁)               | _ , _ , D' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) D' x₁
    elaborability-ana {e = X x} (ASubsume D x₁)                  | _ , _ , D' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) D' x₁
    elaborability-ana {e = ·λ x e} (ASubsume D x₁)               | _ , _ , D' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) D' x₁
    elaborability-ana {e = ·λ x [ x₁ ] e} (ASubsume D x₂)        | _ , _ , D' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) D' x₂
    elaborability-ana {e = e1 ∘ e2} (ASubsume D x₁)              | _ , _ , D' = _ , _ , _ , EASubsume (λ _ ()) (λ _ _ ()) D' x₁
    -- the two holes are special-cased
    elaborability-ana {e = ⦇-⦈[ x ]} (ASubsume _ _ )                   | _ , _ , _  = _ , _ , _ , EAEHole
    elaborability-ana {Γ} {⦇⌜ e ⌟⦈[ x ]} (ASubsume (SNEHole new wt) x₂) | _ , _ , ESNEHole x₁ D' with elaborability-synth wt
    ... | w , y , z =  _ , _ , _ , EANEHole (elab-new-disjoint-synth new z) z
    -- the lambda cases
    elaborability-ana (ALam x₁ m wt)
      with elaborability-ana wt
    ... | _ , _ , _ , D' = _ , _ , _ , EALam x₁ m D'

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
open import Agda.Builtin.Char
open import Agda.Builtin.Coinduction
open import Agda.Builtin.IO
open import Agda.Builtin.List
open import Agda.Builtin.Unit
open import Agda.Builtin.String

data Colist {a} (A : Set a) : Set a where
  []  : Colist A
  _∷_ : A → ∞ (Colist A) → Colist A

{-# FOREIGN GHC
  data Colist a    = Nil | Cons a (MAlonzo.RTE.Inf (Colist a))
  type Colist' l a = Colist a

  fromColist :: Colist a -> [a]
  fromColist Nil         = []
  fromColist (Cons x xs) = x : fromColist (MAlonzo.RTE.flat xs)
  #-}

{-# COMPILE GHC Colist = data Colist' (Nil | Cons) #-}

to-colist : ∀ {a} {A : Set a} → List A → Colist A
to-colist []       = []
to-colist (x ∷ xs) = x ∷ ♯ to-colist xs

a-definition-that-uses-♭ :
  ∀ {a} {A : Set a} → Colist A → Colist A
a-definition-that-uses-♭ []       = []
a-definition-that-uses-♭ (x ∷ xs) =
  x ∷ ♯ a-definition-that-uses-♭ (♭ xs)

postulate
  putStr : Colist Char → IO ⊤

{-# COMPILE GHC putStr = putStr . fromColist #-}

main : IO ⊤
main = putStr (a-definition-that-uses-♭
         (to-colist (primStringToList "apa\n")))

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text: module Categories.Comonad.Cofree where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, 2011-10-06
module Issue483c where

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

record _×_ (A B : Set) : Set where
  constructor _,_
  field fst : A
        snd : B

postulate
  A : Set
  f : .A → A

-- this succeeds
test : let X : .A → A
           X = _
       in .(x : A) → (X ≡ f) × (X (f x) ≡ f x)
test x = refl , refl

-- so this should also succeed
test2 : let X : .A → A
            X = _
        in .(x : A) → (X (f x) ≡ f x) × (X ≡ f)
test2 x = refl , refl

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Alpha-equivalence
------------------------------------------------------------------------

open import Atom

module Alpha-equivalence (atoms : χ-atoms) where

open import Equality.Propositional
open import Prelude hiding (const)

open import Bag-equivalence equality-with-J using (_∈_)
import Nat equality-with-J as Nat

open import Chi            atoms
open import Free-variables atoms

open χ-atoms atoms

private
  variable
    A                          : Type
    b₁ b₂                      : Br
    bs₁ bs₂                    : List Br
    c c₁ c₂                    : Const
    e e₁ e₂ e₃ e₁₁ e₁₂ e₂₁ e₂₂ : Exp
    es₁ es₂                    : List Exp
    R R₁ R₂                    : A → A → Type
    x x₁ x₁′ x₂ x₂′ y          : A
    xs xs₁ xs₂                 : List A

------------------------------------------------------------------------
-- The definition of α-equivalence

-- R [ x ∼ y ] relates x to y, and for pairs of variables x′, y′ such
-- that x is distinct from x′ and y is distinct from y′ it behaves
-- like R.

infix 5 _[_∼_]

_[_∼_] : (Var → Var → Type) → Var → Var → (Var → Var → Type)
(R [ x ∼ y ]) x′ y′ =
  x ≡ x′ × y ≡ y′
    ⊎
  x ≢ x′ × y ≢ y′ × R x′ y′

-- Alpha-⋆ lifts a binary relation to lists.

infixr 5 _∷_

data Alpha-⋆ (R : A → A → Type) : List A → List A → Type where
  []  : Alpha-⋆ R [] []
  _∷_ : R x₁ x₂ →
        Alpha-⋆ R xs₁ xs₂ →
        Alpha-⋆ R (x₁ ∷ xs₁) (x₂ ∷ xs₂)

-- Alpha R is α-equivalence up to R: free variables are related if
-- they are related by R.

mutual

  data Alpha (R : Var → Var → Type) : Exp → Exp → Type where
    apply :
      Alpha R e₁₁ e₁₂ → Alpha R e₂₁ e₂₂ →
      Alpha R (apply e₁₁ e₂₁) (apply e₁₂ e₂₂)

    lambda :
      Alpha (R [ x₁ ∼ x₂ ]) e₁ e₂ →
      Alpha R (lambda x₁ e₁) (lambda x₂ e₂)

    case :
      Alpha R e₁ e₂ →
      Alpha-⋆ (Alpha-Br R) bs₁ bs₂ →
      Alpha R (case e₁ bs₁) (case e₂ bs₂)

    rec :
      Alpha (R [ x₁ ∼ x₂ ]) e₁ e₂ →
      Alpha R (rec x₁ e₁) (rec x₂ e₂)

    var : R x₁ x₂ → Alpha R (var x₁) (var x₂)

    const :
      Alpha-⋆ (Alpha R) es₁ es₂ →
      Alpha R (const c es₁) (const c es₂)

  data Alpha-Br (R : Var → Var → Type) : Br → Br → Type where
    nil :
      Alpha R e₁ e₂ →
      Alpha-Br R (branch c [] e₁) (branch c [] e₂)
    cons :
      Alpha-Br (R [ x₁ ∼ x₂ ]) (branch c xs₁ e₁) (branch c xs₂ e₂) →
      Alpha-Br R (branch c (x₁ ∷ xs₁) e₁) (branch c (x₂ ∷ xs₂) e₂)

-- The α-equivalence relation.

infix 4 _≈α_

_≈α_ : Exp → Exp → Type
_≈α_ = Alpha _≡_

------------------------------------------------------------------------
-- Some properties related to reflexivity

-- If R y y holds assuming that y is distinct from x, then
-- (R [ x ∼ x ]) y y holds.

[≢→[∼]]→[∼] :
  ∀ R →
  (y ≢ x → R y y) →
  (R [ x ∼ x ]) y y
[≢→[∼]]→[∼] {y = y} {x = x} _ r = case x V.≟ y of λ where
  (yes x≡y) → inj₁ (x≡y , x≡y)
  (no  x≢y) → inj₂ ( x≢y , x≢y
                   , r (x≢y ∘ sym)
                   )

-- Alpha R is reflexive for expressions for which R x x holds for
-- every free variable x.

mutual

  refl-Alpha :
    ∀ e → (∀ x → x ∈FV e → R x x) → Alpha R e e

  refl-Alpha (apply e₁ e₂) r =
    apply (refl-Alpha e₁ λ x x∈e₁ → r x (apply-left  x∈e₁))
          (refl-Alpha e₂ λ x x∈e₂ → r x (apply-right x∈e₂))

  refl-Alpha {R = R} (lambda x e) r =
    lambda (refl-Alpha e λ y y∈e → [≢→[∼]]→[∼] R λ y≢x →
              r y (lambda y≢x y∈e))

  refl-Alpha (case e bs) r =
    case
      (refl-Alpha e λ x x∈e →
         r x (case-head x∈e))
      (refl-Alpha-B⋆ bs λ x ∈bs x∉xs x∈ →
         r x (case-body x∈ ∈bs x∉xs))

  refl-Alpha {R = R} (rec x e) r =
    rec (refl-Alpha e λ y y∈e → [≢→[∼]]→[∼] R λ y≢x →
           r y (rec y≢x y∈e))

  refl-Alpha (var x) r =
    var (r x (var refl))

  refl-Alpha (const c es) r =
    const (refl-Alpha-⋆ es λ x e e∈es x∈e →
             r x (const x∈e e∈es))

  refl-Alpha-B :
    ∀ c xs e →
    (∀ x → ¬ x ∈ xs → x ∈FV e → R x x) →
    Alpha-Br R (branch c xs e) (branch c xs e)
  refl-Alpha-B c [] e r =
    nil (refl-Alpha e λ x x∈e →
           r x (λ ()) x∈e)
  refl-Alpha-B {R = R} c (x ∷ xs) e r =
    cons (refl-Alpha-B c xs e λ y y∉xs y∈e → [≢→[∼]]→[∼] R λ y≢x →
            r y [ y≢x , y∉xs ] y∈e)

  refl-Alpha-⋆ :
    ∀ es → (∀ x e → e ∈ es → x ∈FV e → R x x) →
    Alpha-⋆ (Alpha R) es es
  refl-Alpha-⋆ []       _ = []
  refl-Alpha-⋆ (e ∷ es) r =
    refl-Alpha e (λ x x∈e → r x e (inj₁ refl) x∈e) ∷
    refl-Alpha-⋆ es (λ x e e∈es x∈e → r x e (inj₂ e∈es) x∈e)

  refl-Alpha-B⋆ :
    ∀ bs →
    (∀ x {c xs e} → branch c xs e ∈ bs → ¬ x ∈ xs → x ∈FV e → R x x) →
    Alpha-⋆ (Alpha-Br R) bs bs
  refl-Alpha-B⋆ []                   r = []
  refl-Alpha-B⋆ (branch c xs e ∷ bs) r =
    refl-Alpha-B c xs e (λ x x∉xs x∈e → r x (inj₁ refl) x∉xs x∈e) ∷
    refl-Alpha-B⋆ bs (λ x ∈bs x∉xs x∈ → r x (inj₂ ∈bs) x∉xs x∈)

-- The α-equivalence relation is reflexive.

refl-α : e ≈α e
refl-α = refl-Alpha _ (λ _ _ → refl)

-- Equational reasoning combinators.

infix  -1 finally-α _∎α
infixr -2 step-≡-≈α step-≈α-≡ _≡⟨⟩α_

_∎α : ∀ e → e ≈α e
_ ∎α = refl-α

step-≡-≈α : ∀ e₁ → e₂ ≈α e₃ → e₁ ≡ e₂ → e₁ ≈α e₃
step-≡-≈α _ e₂≈e₃ e₁≡e₂ = subst (_≈α _) (sym e₁≡e₂) e₂≈e₃

syntax step-≡-≈α e₁ e₂≈e₃ e₁≡e₂ = e₁ ≡⟨ e₁≡e₂ ⟩α e₂≈e₃

step-≈α-≡ : ∀ e₁ → e₂ ≡ e₃ → e₁ ≈α e₂ → e₁ ≈α e₃
step-≈α-≡ _ e₂≡e₃ e₁≈e₂ = subst (_ ≈α_) e₂≡e₃ e₁≈e₂

syntax step-≈α-≡ e₁ e₂≡e₃ e₁≈e₂ = e₁ ≈⟨ e₁≈e₂ ⟩α e₂≡e₃

_≡⟨⟩α_ : ∀ e₁ → e₁ ≈α e₂ → e₁ ≈α e₂
_ ≡⟨⟩α e₁≈e₂ = e₁≈e₂

finally-α : ∀ e₁ e₂ → e₁ ≈α e₂ → e₁ ≈α e₂
finally-α _ _ e₁≈e₂ = e₁≈e₂

syntax finally-α e₁ e₂ e₁≈e₂ = e₁ ≈⟨ e₁≈e₂ ⟩α∎ e₂ ∎

------------------------------------------------------------------------
-- A map function

-- A kind of map function for _[_∼_].

map-[∼] :
  ∀ R₁ → (∀ {x₁ x₂} → R₁ x₁ x₂ → R₂ x₁ x₂) →
  (R₁ [ x₁ ∼ x₂ ]) x₁′ x₂′ →
  (R₂ [ x₁ ∼ x₂ ]) x₁′ x₂′
map-[∼] _ r = ⊎-map id (Σ-map id (Σ-map id r))

-- A kind of map function for Alpha.

mutual

  map-Alpha :
    (∀ {x₁ x₂} → R₁ x₁ x₂ → R₂ x₁ x₂) →
    Alpha R₁ e₁ e₂ → Alpha R₂ e₁ e₂

  map-Alpha r (var Rx₁x₂) = var (r Rx₁x₂)

  map-Alpha {R₁ = R₁} r (lambda e₁≈e₂) =
    lambda (map-Alpha (map-[∼] R₁ r) e₁≈e₂)

  map-Alpha {R₁ = R₁} r (rec e₁≈e₂) =
    rec (map-Alpha (map-[∼] R₁ r) e₁≈e₂)

  map-Alpha r (apply e₁₁≈e₁₂ e₂₁≈e₂₂) =
    apply (map-Alpha r e₁₁≈e₁₂) (map-Alpha r e₂₁≈e₂₂)

  map-Alpha r (const es₁≈es₂) =
    const (map-Alpha-⋆ r es₁≈es₂)

  map-Alpha r (case e₁≈e₂ bs₁≈bs₂) =
    case (map-Alpha r e₁≈e₂)
         (map-Alpha-Br-⋆ r bs₁≈bs₂)

  map-Alpha-Br :
    (∀ {x₁ x₂} → R₁ x₁ x₂ → R₂ x₁ x₂) →
    Alpha-Br R₁ b₁ b₂ → Alpha-Br R₂ b₁ b₂
  map-Alpha-Br r (nil e₁≈e₂) =
    nil (map-Alpha r e₁≈e₂)
  map-Alpha-Br {R₁ = R₁} r (cons b₁≈b₂) =
    cons (map-Alpha-Br (map-[∼] R₁ r) b₁≈b₂)

  map-Alpha-⋆ :
    (∀ {x₁ x₂} → R₁ x₁ x₂ → R₂ x₁ x₂) →
    Alpha-⋆ (Alpha R₁) es₁ es₂ → Alpha-⋆ (Alpha R₂) es₁ es₂
  map-Alpha-⋆ _ []                = []
  map-Alpha-⋆ r (e₁≈e₂ ∷ es₁≈es₂) =
    map-Alpha r e₁≈e₂ ∷ map-Alpha-⋆ r es₁≈es₂

  map-Alpha-Br-⋆ :
    (∀ {x₁ x₂} → R₁ x₁ x₂ → R₂ x₁ x₂) →
    Alpha-⋆ (Alpha-Br R₁) bs₁ bs₂ → Alpha-⋆ (Alpha-Br R₂) bs₁ bs₂
  map-Alpha-Br-⋆ _ []                = []
  map-Alpha-Br-⋆ r (b₁≈b₂ ∷ bs₁≈bs₂) =
    map-Alpha-Br r b₁≈b₂ ∷ map-Alpha-Br-⋆ r bs₁≈bs₂

------------------------------------------------------------------------
-- Symmetry

-- A kind of symmetry holds for _[_∼_].

sym-[∼] :
  ∀ R →
  (R [ x₁ ∼ x₂ ]) x₁′ x₂′ →
  (flip R [ x₂ ∼ x₁ ]) x₂′ x₁′
sym-[∼] _ =
  ⊎-map Prelude.swap
        (λ (x₁≢x₁′ , x₂≢x₂′ , R₁x₁′x₂′) →
           x₂≢x₂′ , x₁≢x₁′ , R₁x₁′x₂′)

-- A kind of symmetry holds for Alpha.

mutual

  sym-Alpha : Alpha R e₁ e₂ → Alpha (flip R) e₂ e₁

  sym-Alpha (var Rx₁x₂) = var Rx₁x₂

  sym-Alpha {R = R} (lambda e₁≈e₂) =
    lambda (map-Alpha (sym-[∼] R) (sym-Alpha e₁≈e₂))

  sym-Alpha {R = R} (rec e₁≈e₂) =
    rec (map-Alpha (sym-[∼] R) (sym-Alpha e₁≈e₂))

  sym-Alpha (apply e₁₁≈e₁₂ e₂₁≈e₂₂) =
    apply (sym-Alpha e₁₁≈e₁₂) (sym-Alpha e₂₁≈e₂₂)

  sym-Alpha (const es₁≈es₂) =
    const (sym-Alpha-⋆ es₁≈es₂)

  sym-Alpha (case e₁≈e₂ bs₁≈bs₂) =
    case (sym-Alpha e₁≈e₂)
         (sym-Alpha-Br-⋆ bs₁≈bs₂)

  sym-Alpha-Br :
    Alpha-Br R b₁ b₂ → Alpha-Br (flip R) b₂ b₁
  sym-Alpha-Br (nil e₁≈e₂) =
    nil (sym-Alpha e₁≈e₂)
  sym-Alpha-Br {R = R} (cons b₁≈b₂) =
    cons (map-Alpha-Br (sym-[∼] R) (sym-Alpha-Br b₁≈b₂))

  sym-Alpha-⋆ :
    Alpha-⋆ (Alpha R) es₁ es₂ → Alpha-⋆ (Alpha (flip R)) es₂ es₁
  sym-Alpha-⋆ []                = []
  sym-Alpha-⋆ (e₁≈e₂ ∷ es₁≈es₂) =
    sym-Alpha e₁≈e₂ ∷ sym-Alpha-⋆ es₁≈es₂

  sym-Alpha-Br-⋆ :
    Alpha-⋆ (Alpha-Br R) bs₁ bs₂ → Alpha-⋆ (Alpha-Br (flip R)) bs₂ bs₁
  sym-Alpha-Br-⋆ []                = []
  sym-Alpha-Br-⋆ (b₁≈b₂ ∷ bs₁≈bs₂) =
    sym-Alpha-Br b₁≈b₂ ∷ sym-Alpha-Br-⋆ bs₁≈bs₂

-- The α-equivalence relation is symmetric.

sym-α : e₁ ≈α e₂ → e₂ ≈α e₁
sym-α = map-Alpha sym ∘ sym-Alpha

------------------------------------------------------------------------
-- Several things respect α-equivalence

-- The free variable relation respects α-equivalence.

mutual

  Alpha-∈ :
    Alpha R e₁ e₂ → x₁ ∈FV e₁ → ∃ λ x₂ → R x₁ x₂ × x₂ ∈FV e₂
  Alpha-∈ {R = R} (var Ry₁y₂) (var x₁≡y₁) =
    _ , subst (flip R _) (sym x₁≡y₁) Ry₁y₂ , var refl

  Alpha-∈ (lambda e₁≈e₂) (lambda x₁≢y₁ x₁∈)
    with Alpha-∈ e₁≈e₂ x₁∈
  … | x₂ , inj₂ (_ , y₂≢x₂ , Rx₁x₂) , x₂∈ =
    x₂ , Rx₁x₂ , lambda (y₂≢x₂ ∘ sym) x₂∈
  … | _ , inj₁ (y₁≡x₁ , _) , _ =
    ⊥-elim $ x₁≢y₁ (sym y₁≡x₁)

  Alpha-∈ (rec e₁≈e₂) (rec x₁≢y₁ x₁∈)
    with Alpha-∈ e₁≈e₂ x₁∈
  … | x₂ , inj₂ (_ , y₂≢x₂ , Rx₁x₂) , x₂∈ =
    x₂ , Rx₁x₂ , rec (y₂≢x₂ ∘ sym) x₂∈
  … | _ , inj₁ (y₁≡x₁ , _) , _ =
    ⊥-elim $ x₁≢y₁ (sym y₁≡x₁)

  Alpha-∈ (apply e₁₁≈e₁₂ e₂₁≈e₂₂) (apply-left x₁∈) =
    Σ-map id (Σ-map id apply-left) $ Alpha-∈ e₁₁≈e₁₂ x₁∈
  Alpha-∈ (apply e₁₁≈e₁₂ e₂₁≈e₂₂) (apply-right x₁∈) =
    Σ-map id (Σ-map id apply-right) $ Alpha-∈ e₂₁≈e₂₂ x₁∈

  Alpha-∈ (const es₁≈es₂) (const x₁∈ ∈es₁) =
    Σ-map id (Σ-map id $ uncurry λ _ → uncurry const) $
    Alpha-⋆-∈ es₁≈es₂ x₁∈ ∈es₁

  Alpha-∈ (case e₁≈e₂ bs₁≈bs₂) (case-head x₁∈) =
    Σ-map id (Σ-map id case-head) $
    Alpha-∈ e₁≈e₂ x₁∈

  Alpha-∈ (case e₁≈e₂ bs₁≈bs₂) (case-body x₁∈ ∈bs₁ ∉xs₁) =
    Σ-map id (Σ-map id λ (_ , _ , _ , x₂∈ , ∈bs₂ , ∉xs₂) →
                case-body x₂∈ ∈bs₂ ∉xs₂) $
    Alpha-Br-⋆-∈ bs₁≈bs₂ x₁∈ ∈bs₁ ∉xs₁

  Alpha-Br-∈ :
    Alpha-Br R (branch c₁ xs₁ e₁) (branch c₂ xs₂ e₂) →
    x₁ ∈FV e₁ → ¬ x₁ ∈ xs₁ →
    ∃ λ x₂ → R x₁ x₂ × x₂ ∈FV e₂ × ¬ x₂ ∈ xs₂
  Alpha-Br-∈ (nil e₁≈e₂) x₁∈ _ =
    Σ-map id (Σ-map id (_, λ ())) $
    Alpha-∈ e₁≈e₂ x₁∈
  Alpha-Br-∈ (cons {x₁ = y₁} {x₂ = y₂} bs₁≈bs₂) x₁∈ x₁∉
    with Alpha-Br-∈ bs₁≈bs₂ x₁∈ (x₁∉ ∘ inj₂)
  … | x₂ , inj₂ (_ , y₂≢x₂ , Rx₁x₂) , x₂∈ , x₂∉ =
    x₂ , Rx₁x₂ , x₂∈ , [ y₂≢x₂ ∘ sym , x₂∉ ]
  … | _ , inj₁ (y₁≡x₁ , _) , _ =
    ⊥-elim $ x₁∉ (inj₁ (sym y₁≡x₁))

  Alpha-⋆-∈ :
    Alpha-⋆ (Alpha R) es₁ es₂ →
    x₁ ∈FV e₁ → e₁ ∈ es₁ →
    ∃ λ x₂ → R x₁ x₂ × ∃ λ e₂ → x₂ ∈FV e₂ × e₂ ∈ es₂
  Alpha-⋆-∈ (e₁≈e₂ ∷ es₁≈es₂) x₁∈ (inj₁ ≡e₁) =
    Σ-map id (Σ-map id λ x₂∈ → _ , x₂∈ , inj₁ refl) $
    Alpha-∈ e₁≈e₂ (subst (_ ∈FV_) ≡e₁ x₁∈)
  Alpha-⋆-∈ (e₁≈e₂ ∷ es₁≈es₂) x₁∈ (inj₂ ∈es₁) =
    Σ-map id (Σ-map id (Σ-map id (Σ-map id inj₂))) $
    Alpha-⋆-∈ es₁≈es₂ x₁∈ ∈es₁

  Alpha-Br-⋆-∈ :
    Alpha-⋆ (Alpha-Br R) bs₁ bs₂ →
    x₁ ∈FV e₁ → branch c₁ xs₁ e₁ ∈ bs₁ → ¬ x₁ ∈ xs₁ →
    ∃ λ x₂ → R x₁ x₂ × ∃ λ c₂ → ∃ λ xs₂ → ∃ λ e₂ →
      x₂ ∈FV e₂ × branch c₂ xs₂ e₂ ∈ bs₂ × ¬ x₂ ∈ xs₂
  Alpha-Br-⋆-∈
    (_∷_ {x₁ = branch _ _ _} {x₂ = branch _ _ _} b₁≈b₂ bs₁≈bs₂)
    x₁∈ (inj₁ ≡b₁) x₁∉
    with
      Alpha-Br-∈
        b₁≈b₂
        (subst (_ ∈FV_) (cong (λ { (branch _ _ e) → e }) ≡b₁) x₁∈)
        (x₁∉ ∘
         subst (_ ∈_) (cong (λ { (branch _ xs _) → xs }) (sym ≡b₁)))
  … | x₂ , Rx₁x₂ , x₂∈ , x₂∉ =
    x₂ , Rx₁x₂ , _ , _ , _ , x₂∈ , inj₁ refl , x₂∉
  Alpha-Br-⋆-∈ (b₁≈b₂ ∷ bs₁≈bs₂) x₁∈ (inj₂ ∈bs₁) x₁∉ =
    (Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id $
     Σ-map inj₂ id) $
    Alpha-Br-⋆-∈ bs₁≈bs₂ x₁∈ ∈bs₁ x₁∉

α-∈ : e₁ ≈α e₂ → x ∈FV e₁ → x ∈FV e₂
α-∈ e₁≈e₂ x∈ with Alpha-∈ e₁≈e₂ x∈
… | x′ , x≡x′ , x′∈ = subst (_∈FV _) (sym x≡x′) x′∈

-- The predicate Closed′ respects α-equivalence.

α-closed′ : e₁ ≈α e₂ → Closed′ xs e₁ → Closed′ xs e₂
α-closed′ e₁≈e₂ cl x x∉ x∈ =
  cl x x∉ (α-∈ (sym-α e₁≈e₂) x∈)

-- The predicate Closed respects α-equivalence.

α-closed : e₁ ≈α e₂ → Closed e₁ → Closed e₂
α-closed = α-closed′

-- Substitution does not necessarily respect α-equivalence.

¬-subst-α :
  ¬ (∀ {x₁ x₂ e₁ e₂ e₁′ e₂′} →
     Alpha (_≡_ [ x₁ ∼ x₂ ]) e₁ e₂ →
     e₁′ ≈α e₂′ →
     e₁ [ x₁ ← e₁′ ] ≈α e₂ [ x₂ ← e₂′ ])
¬-subst-α subst-α =
  not-equal (subst-α e¹≈e² e′≈e′)
  where
  x¹ = V.name 0
  x² = V.name 1
  z  = V.name 2

  e¹ = lambda x¹ (var z)
  e² = lambda x² (var z)

  e′ = var x¹

  e¹≈e² : Alpha (_≡_ [ z ∼ z ]) e¹ e²
  e¹≈e² =
    lambda (var (inj₂ ( V.distinct-codes→distinct-names (λ ())
                      , V.distinct-codes→distinct-names (λ ())
                      , inj₁ (refl , refl)
                      )))

  e′≈e′ : e′ ≈α e′
  e′≈e′ = refl-α

  not-equal : ¬ e¹ [ z ← e′ ] ≈α e² [ z ← e′ ]
  not-equal _ with z V.≟ x¹ | z V.≟ x² | z V.≟ z
  not-equal (lambda (var (inj₁ (_ , x²≡x¹)))) | no _ | no _ | yes _ =
    from-⊎ (1 Nat.≟ 0) (V.name-injective x²≡x¹)
  not-equal (lambda (var (inj₂ (x¹≢x¹ , _)))) | no _ | no _ | yes _ =
    x¹≢x¹ refl
  not-equal _ | yes z≡x¹ | _ | _ =
    from-⊎ (2 Nat.≟ 0) (V.name-injective z≡x¹)
  not-equal _ | _ | yes z≡x² | _ =
    from-⊎ (2 Nat.≟ 1) (V.name-injective z≡x²)
  not-equal _ | _ | _ | no z≢z = z≢z refl

-- TODO: Does substitution of closed terms respect α-equivalence? Does
-- the semantics respect α-equivalence for closed terms?

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
-- {-# OPTIONS -v tc.term.exlam:100 -v extendedlambda:100 -v int2abs.reifyterm:100 -v tc.with:100 -v tc.mod.apply:100 #-}
module Issue778b (Param : Set) where

open import Issue778M Param

data D : (Nat → Nat) → Set where
  d : D pred → D pred

test : (f : Nat → Nat) → D f → Nat
test .pred (d x) = bla
  where bla : Nat
        bla with x
        ... | (d y) = test pred y

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Groups.Definition
open import Setoids.Setoids
open import Groups.Subgroups.Definition

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

module Groups.Subgroups.Normal.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where

normalSubgroup : {c : _} {pred : A → Set c} (sub : Subgroup G pred) → Set (a ⊔ c)
normalSubgroup {pred = pred} sub = {g k : A} → pred k → pred (g + (k + Group.inverse G g))


text:
------------------------------------------------------------------------------
-- Distributive laws on a binary operation: Lemma 3
------------------------------------------------------------------------------

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

module DistributiveLaws.Lemma3-ATP where

open import DistributiveLaws.Base

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

postulate lemma₃ : ∀ x y z → (x · y) · (z · z) ≡ (x · y) · z
{-# ATP prove lemma₃ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module nat-tests where

open import eq
open import nat
open import nat-division
open import nat-to-string
open import product

{- you can prove x + 0 ≡ x and 0 + x ≡ x without induction, if you
   use this more verbose definition of addition: -}
_+a_ : ℕ → ℕ → ℕ
0 +a 0 = 0
(suc x) +a 0 = (suc x)
0 +a (suc y) = (suc y)
(suc x) +a (suc y) = suc (suc (x +a y))

0+a : ∀ (x : ℕ) → x +a 0 ≡ x
0+a 0 = refl
0+a (suc y) = refl

+a0 : ∀ (x : ℕ) → 0 +a x ≡ x
+a0 0 = refl
+a0 (suc y) = refl

8-div-3-lem : (8 ÷ 3 !! refl) ≡ (2 , 2)
8-div-3-lem = refl

23-div-5-lem : (23 ÷ 5 !! refl) ≡ (4 , 3)
23-div-5-lem = refl

ℕ-to-string-lem : ℕ-to-string 237 ≡ "237"
ℕ-to-string-lem = refl

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL