```------------------------------------------------------------------------
-- Inductively defined beta-eta-equality
------------------------------------------------------------------------

import Level
open import Data.Universe

(Uni₀ : Universe Level.zero Level.zero)
where

open import Data.Product renaming (curry to c)
open import Function hiding (_∋_)
import README.DependentlyTyped.Term as Term; open Term Uni₀
import README.DependentlyTyped.Term.Substitution as S; open S Uni₀
import Relation.Binary.PropositionalEquality as P

open P.≡-Reasoning

-- βη-equality.

infixl 9 _·_
infix  4 _≈_
infixr 2 _≈⟨_⟩_

data _≈_ : ∀ {Γ₁ σ₁} → Γ₁ ⊢ σ₁ → ∀ {Γ₂ σ₂} → Γ₂ ⊢ σ₂ → Set where

-- β and η.

β : ∀ {Γ sp₁ sp₂} {σ : IType Γ (π sp₁ sp₂)}
(t₁ : Γ ▻ fst σ ⊢ snd σ) (t₂ : Γ ⊢ fst σ) →
ƛ t₁ · t₂ ≈ t₁ /⊢ sub t₂
η : ∀ {Γ sp₁ sp₂ σ} (t : Γ ⊢ (π sp₁ sp₂ , σ)) →
ƛ ((t /⊢ wk[ fst σ ]) · var zero) ≈ t

-- The relation is an equivalence (reflexivity is proved below).

sym    : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁}
{Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂}
(t₁≈t₂ : t₁ ≈ t₂) → t₂ ≈ t₁
_≈⟨_⟩_ : ∀ {Γ₁ σ₁} (t₁ : Γ₁ ⊢ σ₁)
{Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂}
{Γ₃ σ₃} {t₃ : Γ₃ ⊢ σ₃}
(t₁≈t₂ : t₁ ≈ t₂) (t₂≈t₃ : t₂ ≈ t₃) → t₁ ≈ t₃

-- The relation is a congruence.

var : ∀ {Γ₁ σ₁} {x₁ : Γ₁ ∋ σ₁}
{Γ₂ σ₂} {x₂ : Γ₂ ∋ σ₂}
(x₁≅x₂ : x₁ ≅-∋ x₂) → var x₁ ≈ var x₂
ƛ   : ∀ {Γ₁ σ₁ τ₁} {t₁ : Γ₁ ▻ σ₁ ⊢ τ₁}
{Γ₂ σ₂ τ₂} {t₂ : Γ₂ ▻ σ₂ ⊢ τ₂}
(t₁≈t₂ : t₁ ≈ t₂) → ƛ t₁ ≈ ƛ t₂
_·_ : ∀ {Γ₁ sp₁₁ sp₂₁ σ₁}
{t₁₁ : Γ₁ ⊢ π sp₁₁ sp₂₁ , σ₁} {t₂₁ : Γ₁ ⊢ fst σ₁}
{Γ₂ sp₁₂ sp₂₂ σ₂}
{t₁₂ : Γ₂ ⊢ π sp₁₂ sp₂₂ , σ₂} {t₂₂ : Γ₂ ⊢ fst σ₂}
(t₁₁≈t₁₂ : t₁₁ ≈ t₁₂) (t₂₁≈t₂₂ : t₂₁ ≈ t₂₂) →
t₁₁ · t₂₁ ≈ t₁₂ · t₂₂

-- Reflexivity.

infix 3 _□

_□ : ∀ {Γ σ} (t : Γ ⊢ σ) → t ≈ t
var x   □ = var P.refl
ƛ t     □ = ƛ (t □)
t₁ · t₂ □ = (t₁ □) · (t₂ □)

abstract

-- βη-equal terms have the same semantics.

≈-sound : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁} {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
t₁ ≈ t₂ → ⟦ t₁ ⟧ ≅-Value ⟦ t₂ ⟧
≈-sound (β t₁ t₂) = begin
[ c ⟦ t₁ ⟧ ˢ ⟦ t₂ ⟧ ]  ≡⟨ corresponds (app (sub t₂)) t₁ ⟩
[ ⟦ t₁ /⊢ sub t₂ ⟧  ]  ∎
≈-sound (η t) = begin
[ c (⟦ t /⊢ wk ⟧     ˢ lookup zero) ]  ≡⟨ curry-cong \$ ˢ-cong (P.sym \$ corresponds (app wk) t)
(P.refl {x = [ lookup zero ]}) ⟩
[ c ((⟦ t ⟧ /̂Val ŵk) ˢ lookup zero) ]  ≡⟨ P.refl ⟩
[ ⟦ t ⟧                             ]  ∎
≈-sound (sym t₁≈t₂)           = P.sym \$ ≈-sound t₁≈t₂
≈-sound (t₁ ≈⟨ t₁≈t₂ ⟩ t₂≈t₃) = P.trans (≈-sound t₁≈t₂) (≈-sound t₂≈t₃)
≈-sound (var P.refl)          = P.refl
≈-sound (ƛ t₁≈t₂)             = curry-cong (≈-sound t₁≈t₂)
≈-sound (t₁₁≈t₁₂ · t₂₁≈t₂₂)   = ˢ-cong (≈-sound t₁₁≈t₁₂) (≈-sound t₂₁≈t₂₂)

-- βη-equal terms have identical contexts.

≈-⇒-≅-Ctxt : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁} {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
t₁ ≈ t₂ → Γ₁ ≅-Ctxt Γ₂
≈-⇒-≅-Ctxt t₁≈t₂ = P.cong [Value].Γ \$ ≈-sound t₁≈t₂

-- βη-equal terms have identical types.

≈-⇒-≅-Type : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁} {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
t₁ ≈ t₂ → σ₁ ≅-Type σ₂
≈-⇒-≅-Type {t₁ = t₁} {t₂ = t₂} t₁≈t₂
with ⟦ t₂ ⟧ | ≈-sound t₁≈t₂
... | .(⟦ t₁ ⟧) | P.refl = P.refl
```