module Section3 where

open import Section1 public


-- 3. The calculus of proof trees
-- ==============================
--
-- We define the set of proof trees of implicational logic in the ordinary style Γ  la Church,
-- except that we use explicit substitutions.


-- 3.1. Definition of types
-- ------------------------
--
-- The types we have are base type and function types.  The set of types `𝒯 : Set` is introduced
-- by:

infixr 7 _βŠƒ_
data 𝒯 : Set where
  β€’   : 𝒯
  _βŠƒ_ : 𝒯 β†’ 𝒯 β†’ 𝒯

-- Types are denoted by `A`, `B`.  (…)
--
-- We write `β€’` for the base type and `A βŠƒ B` for the function type.

module _ where
  injβ‚βŠƒ : βˆ€ {A Aβ€² B Bβ€²} β†’ A βŠƒ B ≑ Aβ€² βŠƒ Bβ€² β†’ A ≑ Aβ€²
  injβ‚βŠƒ refl = refl

  injβ‚‚βŠƒ : βˆ€ {A Aβ€² B Bβ€²} β†’ A βŠƒ B ≑ Aβ€² βŠƒ Bβ€² β†’ B ≑ Bβ€²
  injβ‚‚βŠƒ refl = refl

  _β‰Ÿπ’―_ : (A Aβ€² : 𝒯) β†’ Dec (A ≑ Aβ€²)
  β€’       β‰Ÿπ’― β€’         = yes refl
  β€’       β‰Ÿπ’― (Aβ€² βŠƒ Bβ€²) = no Ξ» ()
  (A βŠƒ B) β‰Ÿπ’― β€’         = no Ξ» ()
  (A βŠƒ B) β‰Ÿπ’― (Aβ€² βŠƒ Bβ€²) with A β‰Ÿπ’― Aβ€² | B β‰Ÿπ’― Bβ€²
  …                   | yes refl | yes refl = yes refl
  …                   | yes refl | no Bβ‰’Bβ€²  = no (Ξ» p β†’ injβ‚‚βŠƒ p β†― Bβ‰’Bβ€²)
  …                   | no Aβ‰’Aβ€²  | _        = no (Ξ» p β†’ injβ‚βŠƒ p β†― Aβ‰’Aβ€²)


-- 3.2. Definition of contexts
-- ---------------------------
--
-- Suppose a countably infinite set, `Name`, with names together with a decidable equality on it.
-- The set of contexts `π’ž` is mutually defined with a boolean-valued function `fresh` which describes
-- when a name is fresh in a context.  (…)
--
-- Ordinarily, the freshness condition is written as a side-condition, but since we are to
-- formalise the proof trees, this information must be represented, too.
--
-- We write `[]` for the empty context and `[ Ξ“ , x ∷ A ]` for adding an element to a context,
-- hence when we write `[ Ξ“ , x ∷ A ]`
-- it is implicit that we also have a proof that `x` is fresh in `Ξ“` (when `[ Ξ“ , x ∷ A ]` occurs in the
-- conclusion of a statement, then it is implicit that `T (fresh x Ξ“)` is an assumption.)  The
-- function `fresh` is defined by induction on the context as:

mutual
  data π’ž : Set where
    []      : π’ž
    [_,_∷_] : (Ξ“ : π’ž) (x : Name) {{_ : T (fresh x Ξ“)}} β†’ 𝒯 β†’ π’ž

  fresh : Name β†’ π’ž β†’ Bool
  fresh x []            = true
  fresh x [ Ξ“ , y ∷ A ] = and (x β‰  y) (fresh x Ξ“)

-- We use `Ξ“`, `Ξ”` and `Θ` for contexts.
--
-- The predicate `Ξ“ βˆ‹ x ∷ A` is true when a name with its type occurs in a context.
--
-- The introduction rules are:

data _βˆ‹_∷_ : π’ž β†’ Name β†’ 𝒯 β†’ Set where
  zero : βˆ€ {Ξ“ A x} {{_ : T (fresh x Ξ“)}} β†’
           [ Ξ“ , x ∷ A ] βˆ‹ x ∷ A
  suc  : βˆ€ {Ξ“ A B x y} {{_ : T (fresh y Ξ“)}} β†’
           Ξ“ βˆ‹ x ∷ A β†’
           [ Ξ“ , y ∷ B ] βˆ‹ x ∷ A

module _ where
  injsuc : βˆ€ {Ξ“ A B x y} {{_ : T (fresh y Ξ“)}} {i iβ€² : Ξ“ βˆ‹ x ∷ A} β†’
             suc {B = B} {y = y} i ≑ suc iβ€² β†’ i ≑ iβ€²
  injsuc refl = refl

  _β‰Ÿβˆ‹_ : βˆ€ {Ξ“ A x} β†’ (i iβ€² : Ξ“ βˆ‹ x ∷ A) β†’ Dec (i ≑ iβ€²)
  zero  β‰Ÿβˆ‹ zero   = yes refl
  zero  β‰Ÿβˆ‹ suc iβ€² = no (Ξ» ())
  suc i β‰Ÿβˆ‹ zero   = no (Ξ» ())
  suc i β‰Ÿβˆ‹ suc iβ€² with i β‰Ÿβˆ‹ iβ€²
  …              | yes refl = yes refl
  …              | no iβ‰’iβ€²  = no (Ξ» p β†’ injsuc p β†― iβ‰’iβ€²)

module _ where
  _∌_∷_ : π’ž β†’ Name β†’ 𝒯 β†’ Set
  Ξ“ ∌ x ∷ A = Β¬ (Ξ“ βˆ‹ x ∷ A)

  freshβ†’βˆŒ : βˆ€ {x Ξ“ A} {{_ : T (fresh x Ξ“)}} β†’ Ξ“ ∌ x ∷ A
  freshβ†’βˆŒ {x} {{Ο†}}  zero             with x β‰Ÿ x
  freshβ†’βˆŒ {x} {{()}} zero             | yes refl
  freshβ†’βˆŒ {x} {{Ο†}}  zero             | no xβ‰’x   = refl β†― xβ‰’x
  freshβ†’βˆŒ {x} {{Ο†}}  (suc {y = y}  i) with x β‰Ÿ y
  freshβ†’βˆŒ {x} {{()}} (suc {y = .x} i) | yes refl
  freshβ†’βˆŒ {x} {{Ο†}}  (suc {y = y}  i) | no xβ‰’y   = i β†― freshβ†’βˆŒ

  freshlem₁ : βˆ€ {bβ€²} β†’ (x : Name) β†’ Β¬ (T (and (x β‰  x) bβ€²))
  freshlem₁ x p with x β‰Ÿ x
  …            | yes refl = p
  …            | no xβ‰’x   = refl β†― xβ‰’x

  freshlemβ‚‚ : βˆ€ {bβ€²} β†’ (x {y} : Name) β†’ T (and (x β‰  y) bβ€²) β†’ T bβ€²
  freshlemβ‚‚ x {y} p with x β‰Ÿ y
  …              | yes refl = elimβŠ₯ p
  …              | no xβ‰’y   = p

-- We also define the relation that describes when a context contains another.
--
-- We use the notational convention `Ξ“ βŠ‡ Ξ”` for `Ξ“` being greater than `Ξ”`.
-- The set `_βŠ‡_` has the constructors:

infix 3 _βŠ‡_
data _βŠ‡_ : π’ž β†’ π’ž β†’ Set where
  done : βˆ€ {Ξ“} β†’
           Ξ“ βŠ‡ []
  step : βˆ€ {Ξ“ Ξ” A x} {{_ : T (fresh x Ξ”)}} β†’
           Ξ“ βŠ‡ Ξ” β†’ Ξ“ βˆ‹ x ∷ A β†’
           Ξ“ βŠ‡ [ Ξ” , x ∷ A ]

module _ where
  inj₁step : βˆ€ {Ξ“ Ξ” A x} {{_ : T (fresh x Ξ”)}} {c cβ€² : Ξ“ βŠ‡ Ξ”} {i iβ€² : Ξ“ βˆ‹ x ∷ A} β†’
               step c i ≑ step cβ€² iβ€² β†’ c ≑ cβ€²
  inj₁step refl = refl

  injβ‚‚step : βˆ€ {Ξ“ Ξ” A x} {{_ : T (fresh x Ξ”)}} {c cβ€² : Ξ“ βŠ‡ Ξ”} {i iβ€² : Ξ“ βˆ‹ x ∷ A} β†’
               step c i ≑ step cβ€² iβ€² β†’ i ≑ iβ€²
  injβ‚‚step refl = refl

  _β‰ŸβŠ‡_ : βˆ€ {Ξ“ Ξ”} β†’ (c cβ€² : Ξ“ βŠ‡ Ξ”) β†’ Dec (c ≑ cβ€²)
  done     β‰ŸβŠ‡ done       = yes refl
  step c i β‰ŸβŠ‡ step cβ€² iβ€² with c β‰ŸβŠ‡ cβ€² | i β‰Ÿβˆ‹ iβ€²
  …                     | yes refl | yes refl = yes refl
  …                     | yes refl | no iβ‰’iβ€²  = no (Ξ» p β†’ injβ‚‚step p β†― iβ‰’iβ€²)
  …                     | no cβ‰’cβ€²  | _        = no (Ξ» p β†’ inj₁step p β†― cβ‰’cβ€²)

-- The following lemmas are easy to prove:

-- Lemma 1.
extβŠ‡ : βˆ€ {Ξ” Ξ“} β†’ (βˆ€ {A x} β†’ Ξ” βˆ‹ x ∷ A β†’ Ξ“ βˆ‹ x ∷ A) β†’ Ξ“ βŠ‡ Ξ”
extβŠ‡ {[]}            f = done
extβŠ‡ {[ Ξ” , x ∷ A ]} f = step (extβŠ‡ (Ξ» i β†’ f (suc i))) (f zero)

-- Lemma 2.
module _ where
  β†‘βŸ¨_βŸ©βˆ‹ : βˆ€ {Ξ“ Ξ” A x} β†’ Ξ” βŠ‡ Ξ“ β†’ Ξ“ βˆ‹ x ∷ A β†’ Ξ” βˆ‹ x ∷ A
  β†‘βŸ¨ done βŸ©βˆ‹     ()
  β†‘βŸ¨ step c i βŸ©βˆ‹ zero    = i
  β†‘βŸ¨ step c i βŸ©βˆ‹ (suc j) = β†‘βŸ¨ c βŸ©βˆ‹ j

  instance
    raiseβˆ‹ : βˆ€ {A x} β†’ Raiseable (_βˆ‹ x ∷ A)
    raiseβˆ‹ = record { β†‘βŸ¨_⟩ = β†‘βŸ¨_βŸ©βˆ‹ }

-- Lemma 3.
reflβŠ‡ : βˆ€ {Ξ“} β†’ Ξ“ βŠ‡ Ξ“
reflβŠ‡ = extβŠ‡ id

-- Lemma 4.
module _ where
  _β—‹_ : βˆ€ {Ξ“ Ξ” Θ} β†’ Ξ“ βŠ‡ Ξ” β†’ Θ βŠ‡ Ξ“ β†’ Θ βŠ‡ Ξ”
  c β—‹ cβ€² = extβŠ‡ (Ξ» i β†’ β†‘βŸ¨ cβ€² ⟩ (β†‘βŸ¨ c ⟩ i))

  transβŠ‡ : βˆ€ {Ξ“ Ξ” Θ} β†’ Θ βŠ‡ Ξ“ β†’ Ξ“ βŠ‡ Ξ” β†’ Θ βŠ‡ Ξ”
  transβŠ‡ = flip _β—‹_

-- Lemma 5.
weakβŠ‡ : βˆ€ {Ξ“ A x} {{_ : T (fresh x Ξ“)}} β†’ [ Ξ“ , x ∷ A ] βŠ‡ Ξ“
weakβŠ‡ = extβŠ‡ suc

-- Lemma 6.
uniqβˆ‹ : βˆ€ {Ξ“ A x} β†’ (i iβ€² : Ξ“ βˆ‹ x ∷ A) β†’ i ≑ iβ€²
uniqβˆ‹ zero    zero     = refl
uniqβˆ‹ zero    (suc iβ€²) = iβ€² β†― freshβ†’βˆŒ
uniqβˆ‹ (suc i) zero     = i β†― freshβ†’βˆŒ
uniqβˆ‹ (suc i) (suc iβ€²) = cong suc (uniqβˆ‹ i iβ€²)

-- Lemma 7.
uniqβŠ‡ : βˆ€ {Ξ“ Ξ”} β†’ (c cβ€² : Ξ“ βŠ‡ Ξ”) β†’ c ≑ cβ€²
uniqβŠ‡ done       done         = refl
uniqβŠ‡ (step c i) (step cβ€² iβ€²) = congΒ² step (uniqβŠ‡ c cβ€²) (uniqβˆ‹ i iβ€²)

-- `extβŠ‡`, `β†‘βŸ¨_βŸ©βˆ‹` and `uniqβŠ‡` are proven by induction on `Ξ”` and `uniqβˆ‹` is proven by
-- induction on `Ξ“`.  `reflβŠ‡` and `weakβŠ‡` are direct consequences of `extβŠ‡` and for `transβŠ‡`
-- we also use `β†‘βŸ¨_βŸ©βˆ‹`.  (…)
--
-- The last two lemmas may seem slightly strange: they are used for guaranteeing independence
-- of the proofs of `_βˆ‹_∷_` and `_βŠ‡_`.  For example, `uniqβˆ‹` says that if it can be shown that
-- `x ∷ A` occurs in a context `Ξ“`, then there is a unique proof of this fact.  The need to prove
-- independence of proofs might point to a problem in using type theory for formalising proofs.  On
-- the other hand, as we shall see, proof objects can also be useful: the present formalisation
-- heavily uses the possibilities to perform case analysis on proof objects, which reduces the
-- number of cases to consider.

module _ where
  id₁○ : βˆ€ {Ξ“ Ξ”} β†’ (c : Ξ“ βŠ‡ Ξ“) (cβ€² : Ξ” βŠ‡ Ξ“) β†’ c β—‹ cβ€² ≑ cβ€²
  id₁○ c cβ€² = uniqβŠ‡ (c β—‹ cβ€²) cβ€²

  idβ‚‚β—‹ : βˆ€ {Ξ“ Ξ”} β†’ (c : Ξ” βŠ‡ Ξ“) (cβ€² : Ξ” βŠ‡ Ξ”) β†’ c β—‹ cβ€² ≑ c
  idβ‚‚β—‹ c cβ€² = uniqβŠ‡ (c β—‹ cβ€²) c

  assocβ—‹ : βˆ€ {Ξ“ Ξ” Θ Ξ©} β†’ (c : Ξ” βŠ‡ Ξ“) (cβ€² : Θ βŠ‡ Ξ”) (cβ€³ : Ξ© βŠ‡ Θ) β†’
             c β—‹ (cβ€² β—‹ cβ€³) ≑ (c β—‹ cβ€²) β—‹ cβ€³
  assocβ—‹ c cβ€² cβ€³ = uniqβŠ‡ (c β—‹ (cβ€² β—‹ cβ€³)) ((c β—‹ cβ€²) β—‹ cβ€³)

  compβ—‹ : βˆ€ {Ξ“ Ξ” Θ} β†’ (c : Ξ” βŠ‡ Ξ“) (cβ€² : Θ βŠ‡ Ξ”) (cβ€³ : Θ βŠ‡ Ξ“) β†’
            c β—‹ cβ€² ≑ cβ€³
  compβ—‹ c cβ€² cβ€³ = uniqβŠ‡ (c β—‹ cβ€²) cβ€³


-- 3.3. Definition of proof trees
-- ------------------------------
--
-- Proof trees and substitutions are mutually inductively defined.  (…)
--
-- We use the notational convention `Ξ“ ⊒ A` and `Ξ” β‹™ Ξ“` for a proof of `A` in context `Ξ“` and
-- a substitution of `Ξ“` by `Ξ”`, respectively.
--
-- A substitution of type `Ξ” β‹™ Ξ“` intuitively is a list that associates to each `x ∷ A` in `Ξ“` a unique
-- proof tree of type `Ξ” ⊒ A`.
--
-- The proof trees are defined by the following rules.
--
-- We recall that hidden assumptions in the definition above are implicitly universally defined
-- and that the notation `[ Ξ“ , x ∷ A ]` implies that `x` is fresh in `Ξ“`.  (…)
--
-- In the definition of variables we can see that a proof of occurrence is part of the proof
-- tree.  The advantage is that we can do case-analysis on this proof to find out where in the
-- context `x ∷ A` occurs.  The disadvantage is that we need to prove that two variables are the
-- same even if they have two possibly different proofs of occurrence of `x ∷ A` (by Lemma 6 we
-- know that the proofs are the same).

mutual
  infix 3 _⊒_
  data _⊒_ : π’ž β†’ 𝒯 β†’ Set where
    Ξ½   : βˆ€ {Ξ“ A} β†’
            (x : Name) β†’ Ξ“ βˆ‹ x ∷ A β†’
            Ξ“ ⊒ A
    Ζ›   : βˆ€ {Ξ“ A B} β†’
            (x : Name) {{_ : T (fresh x Ξ“)}} β†’ [ Ξ“ , x ∷ A ] ⊒ B β†’
            Ξ“ ⊒ A βŠƒ B
    _βˆ™_ : βˆ€ {Ξ“ A B} β†’
            Ξ“ ⊒ A βŠƒ B β†’ Ξ“ ⊒ A β†’
            Ξ“ ⊒ B
    _β–Ά_ : βˆ€ {Ξ“ Ξ” A} β†’
            Ξ“ ⊒ A β†’ Ξ” β‹™ Ξ“ β†’
            Ξ” ⊒ A

  infix 3 _β‹™_
  data _β‹™_ : π’ž β†’ π’ž β†’ Set where
    Ο€βŸ¨_⟩    : βˆ€ {Ξ“ Ξ”} β†’
                Ξ” βŠ‡ Ξ“ β†’
                Ξ” β‹™ Ξ“
    _●_     : βˆ€ {Ξ“ Ξ” Θ} β†’
                Ξ“ β‹™ Ξ” β†’ Θ β‹™ Ξ“ β†’
                Θ β‹™ Ξ”
    [_,_≔_] : βˆ€ {Ξ“ Ξ” A} β†’
                Ξ” β‹™ Ξ“ β†’ (x : Name) {{_ : T (fresh x Ξ“)}} β†’ Ξ” ⊒ A β†’
                Ξ” β‹™ [ Ξ“ , x ∷ A ]

-- Explicit substitutions are built from a projection map, update and composition (see below
-- for a discussion on the projection map).
--
-- We use the following notational conventions:
--
-- -   `Ξ½ x`           for referencing the occurrence `x`, where `x : Ξ“ βˆ‹ x ∷ A`
-- -   `M β–Ά Ξ³`         for applying the substitution `Ξ³` to the term `M`
-- -   `Ζ› x M`         for abstracting the occurrence `x` from the term `M`, where `M : [ Ξ“ , x ∷ A ] ⊒ B`
-- -   `M βˆ™ N`         for applying the term `M` to the term `N`
-- -   `Ο€βŸ¨ c ⟩`        for projecting the inclusion `c` as a substitution
-- -   `[ Ξ³ , x ≔ M ]` for updating the substitution `Ξ³` with the term `M` for the occurrence `x`
-- -   `Ξ³ ● Ξ΄`         for composing the substitution `Ξ΄` with the substitution `Ξ³`
--
-- Proof trees and substitutions are named `M, N` and `Ξ³, Ξ΄, ΞΈ` respectively.
--
-- The substitution `Ο€βŸ¨_⟩` is not a standard primitive for explicit substitutions.  Often one rather
-- has an identity substitution (in `Ξ“ β‹™ Ξ“`) [1, 13] or the empty substitution (in `Ξ“ β‹™ []`) [5].
-- Instead we have taken `Ο€βŸ¨_⟩` as primitive.  If `c : Ξ“ βŠ‡ Ξ“`, then `Ο€βŸ¨ c ⟩` is the identity substitution and
-- if `c : Ξ“ βŠ‡ []`, then `Ο€βŸ¨ c ⟩` is the empty substitution.  Abadi et al. [1] use a substitution `↑` that
-- corresponds to a shift on substitutions; the same substitution is here defined as `Ο€βŸ¨ c ⟩` where
-- `c : [ Ξ“ , x ∷ A ] βŠ‡ Ξ“`.  In Martin-LΓΆf’s substitution calculus [13, 20] we have as primitives also
-- thinning rules (i.e., if a term is well-typed in a given context, then it is also well-typed in a
-- larger context and likewise for substitutions.)  Here, thinning is achieved using `Ο€βŸ¨_⟩`, since if,
-- for example, `M : Ξ“ ⊒ A` and `c : Ξ” βŠ‡ Ξ“`, then `M β–Ά Ο€βŸ¨ c ⟩ : Ξ” ⊒ A`.
--
-- The first version of our work used combinators for the thinning rules, since we wanted it to
-- be a start for a complete mechanical analysis of Martin-LΓΆf’s substitution calculus [13, 20].
-- The set of conversion rules we obtained using these combinators suggested the use of `Ο€βŸ¨_⟩`,
-- which gives fewer conversion rules.  There might be other advantages in using `Ο€βŸ¨_⟩`: if a proof
-- tree is of the form `M β–Ά Ο€βŸ¨_⟩` we know which are the possible free variables of the term `M`,
-- information that might be used in a computation.

module _ where
  β†‘βŸ¨_⟩⊒ : βˆ€ {Ξ“ Ξ” A} β†’ Ξ” βŠ‡ Ξ“ β†’ Ξ“ ⊒ A β†’ Ξ” ⊒ A
  β†‘βŸ¨ c ⟩⊒ M = M β–Ά Ο€βŸ¨ c ⟩

  β†‘βŸ¨_βŸ©β‹™ : βˆ€ {Ξ“ Ξ” Θ} β†’ Ξ” βŠ‡ Ξ“ β†’ Ξ“ β‹™ Θ β†’ Ξ” β‹™ Θ
  β†‘βŸ¨ c βŸ©β‹™ Ξ΄ = Ξ΄ ● Ο€βŸ¨ c ⟩

  β†“βŸ¨_βŸ©β‹™ : βˆ€ {Ξ“ Ξ” Θ} β†’ Ξ” βŠ‡ Ξ“ β†’ Θ β‹™ Ξ” β†’ Θ β‹™ Ξ“
  β†“βŸ¨ c βŸ©β‹™ Ξ΄ = Ο€βŸ¨ c ⟩ ● Ξ΄

  reflβ‹™ : βˆ€ {Ξ“} β†’ Ξ“ β‹™ Ξ“
  reflβ‹™ = Ο€βŸ¨ reflβŠ‡ ⟩

  transβ‹™ : βˆ€ {Ξ“ Ξ” Θ} β†’ Θ β‹™ Ξ“ β†’ Ξ“ β‹™ Ξ” β†’ Θ β‹™ Ξ”
  transβ‹™ = flip _●_

  weakβ‹™ : βˆ€ {Ξ“ A x} {{_ : T (fresh x Ξ“)}} β†’ [ Ξ“ , x ∷ A ] β‹™ Ξ“
  weakβ‹™ = Ο€βŸ¨ weakβŠ‡ ⟩

  instance
    raise⊒ : βˆ€ {A} β†’ Raiseable (_⊒ A)
    raise⊒ = record { β†‘βŸ¨_⟩ = β†‘βŸ¨_⟩⊒ }

    raiseβ‹™ : βˆ€ {Ξ“} β†’ Raiseable (_β‹™ Ξ“)
    raiseβ‹™ = record { β†‘βŸ¨_⟩ = β†‘βŸ¨_βŸ©β‹™ }

    lowerβ‹™ : βˆ€ {Ξ”} β†’ Lowerable (Ξ” β‹™_)
    lowerβ‹™ = record { β†“βŸ¨_⟩ = β†“βŸ¨_βŸ©β‹™ }


-- 3.4. Convertibility of proof trees
-- ----------------------------------
--
-- The rules for conversion between proof trees and substitutions are inductively defined.
--
-- We use the notational convention `M β‰… N` and `Ξ³ β‰…β‚› Ξ΄` for convertibility on proof trees and
-- on substitutions respectively.  (…)
--
-- The conversion rules for proof trees are the reflexivity, symmetry, transitivity, congruence
-- rules and the following rules:

mutual
  infix 3 _β‰…_
  data _β‰…_ : βˆ€ {Ξ“ A} β†’ Ξ“ ⊒ A β†’ Ξ“ ⊒ A β†’ Set where
    reflβ‰…  : βˆ€ {Ξ“ A} {M : Ξ“ ⊒ A} β†’
               M β‰… M
    symβ‰…   : βˆ€ {Ξ“ A} {M Mβ€² : Ξ“ ⊒ A} β†’
               M β‰… Mβ€² β†’
               Mβ€² β‰… M
    transβ‰… : βˆ€ {Ξ“ A} {M Mβ€² Mβ€³ : Ξ“ ⊒ A} β†’
               M β‰… Mβ€² β†’ Mβ€² β‰… Mβ€³ β†’
               M β‰… Mβ€³

    congΖ›β‰… : βˆ€ {Ξ“ A B x} {{_ : T (fresh x Ξ“)}} {M Mβ€² : [ Ξ“ , x ∷ A ] ⊒ B} β†’
               M β‰… Mβ€² β†’
               Ζ› x M β‰… Ζ› x Mβ€²
    congβˆ™β‰… : βˆ€ {Ξ“ A B} {M Mβ€² : Ξ“ ⊒ A βŠƒ B} {N Nβ€² : Ξ“ ⊒ A} β†’
               M β‰… Mβ€² β†’ N β‰… Nβ€² β†’
               M βˆ™ N β‰… Mβ€² βˆ™ Nβ€²
    congβ–Άβ‰… : βˆ€ {Ξ“ Ξ” A} {M Mβ€² : Ξ“ ⊒ A} {Ξ³ Ξ³β€² : Ξ” β‹™ Ξ“} β†’
               M β‰… Mβ€² β†’ Ξ³ β‰…β‚› Ξ³β€² β†’
               M β–Ά Ξ³ β‰… Mβ€² β–Ά Ξ³β€²

    conv₁≅ : βˆ€ {Ξ“ Ξ” A B x} {{_ : T (fresh x Ξ“)}} β†’
               (M : [ Ξ“ , x ∷ A ] ⊒ B) (N : Ξ” ⊒ A) (Ξ³ : Ξ” β‹™ Ξ“) β†’
               (Ζ› x M β–Ά Ξ³) βˆ™ N β‰… M β–Ά [ Ξ³ , x ≔ N ]
    convβ‚‚β‰… : βˆ€ {Ξ“ A B x} {{_ : T (fresh x Ξ“)}} β†’
               (c : [ Ξ“ , x ∷ A ] βŠ‡ Ξ“) (M : Ξ“ ⊒ A βŠƒ B) β†’
               M β‰… Ζ› x ((M β–Ά Ο€βŸ¨ c ⟩) βˆ™ Ξ½ x zero)
    conv₃≅ : βˆ€ {Ξ“ Ξ” A x} {{_ : T (fresh x Ξ“)}} β†’
               (M : Ξ” ⊒ A) (Ξ³ : Ξ” β‹™ Ξ“) β†’
               Ξ½ x zero β–Ά [ Ξ³ , x ≔ M ] β‰… M
    convβ‚„β‰… : βˆ€ {Ξ“ Ξ” A x} β†’
               (c : Ξ” βŠ‡ Ξ“) (i : Ξ“ βˆ‹ x ∷ A) (j : Ξ” βˆ‹ x ∷ A) β†’
               Ξ½ x i β–Ά Ο€βŸ¨ c ⟩ β‰… Ξ½ x j
    convβ‚…β‰… : βˆ€ {Ξ“ A} β†’
               (c : Ξ“ βŠ‡ Ξ“) (M : Ξ“ ⊒ A) β†’
               M β–Ά Ο€βŸ¨ c ⟩ β‰… M
    conv₆≅ : βˆ€ {Ξ“ Ξ” A B} β†’
               (M : Ξ“ ⊒ A βŠƒ B) (N : Ξ“ ⊒ A) (Ξ³ : Ξ” β‹™ Ξ“) β†’
               (M βˆ™ N) β–Ά Ξ³ β‰… (M β–Ά Ξ³) βˆ™ (N β–Ά Ξ³)
    conv₇≅ : βˆ€ {Ξ“ Ξ” Θ A} β†’
               (M : Ξ“ ⊒ A) (Ξ³ : Ξ” β‹™ Ξ“) (Ξ΄ : Θ β‹™ Ξ”) β†’
               (M β–Ά Ξ³) β–Ά Ξ΄ β‰… M β–Ά (Ξ³ ● Ξ΄)

  infix 3 _β‰…β‚›_
  data _β‰…β‚›_ : βˆ€ {Ξ“ Ξ”} β†’ Ξ” β‹™ Ξ“ β†’ Ξ” β‹™ Ξ“ β†’ Set where
    reflβ‰…β‚›  : βˆ€ {Ξ“ Ξ”} {Ξ³ : Ξ” β‹™ Ξ“} β†’
                Ξ³ β‰…β‚› Ξ³
    symβ‰…β‚›   : βˆ€ {Ξ“ Ξ”} {Ξ³ Ξ³β€² : Ξ” β‹™ Ξ“} β†’
                Ξ³ β‰…β‚› Ξ³β€² β†’
                Ξ³β€² β‰…β‚› Ξ³
    transβ‰…β‚› : βˆ€ {Ξ“ Ξ”} {Ξ³ Ξ³β€² Ξ³β€³ : Ξ” β‹™ Ξ“} β†’
                Ξ³ β‰…β‚› Ξ³β€² β†’ Ξ³β€² β‰…β‚› Ξ³β€³ β†’
                Ξ³ β‰…β‚› Ξ³β€³

    cong●≅ₛ : βˆ€ {Ξ“ Ξ” Θ} {Ξ³ Ξ³β€² : Ξ” β‹™ Ξ“} {Ξ΄ Ξ΄β€² : Θ β‹™ Ξ”} β†’
                Ξ³ β‰…β‚› Ξ³β€² β†’ Ξ΄ β‰…β‚› Ξ΄β€² β†’
                Ξ³ ● Ξ΄ β‰…β‚› Ξ³β€² ● Ξ΄β€²
    cong≔≅ₛ : βˆ€ {Ξ“ Ξ” A x} {{_ : T (fresh x Ξ“)}} {Ξ³ Ξ³β€² : Ξ” β‹™ Ξ“} {M Mβ€² : Ξ” ⊒ A} β†’
                Ξ³ β‰…β‚› Ξ³β€² β†’ M β‰… Mβ€² β†’
                [ Ξ³ , x ≔ M ] β‰…β‚› [ Ξ³β€² , x ≔ Mβ€² ]

    conv₁≅ₛ : βˆ€ {Ξ“ Ξ” Θ Ξ©} β†’
                (Ξ³ : Ξ” β‹™ Ξ“) (Ξ΄ : Θ β‹™ Ξ”) (ΞΈ : Ξ© β‹™ Θ) β†’
                (Ξ³ ● Ξ΄) ● ΞΈ β‰…β‚› Ξ³ ● (Ξ΄ ● ΞΈ)
    convβ‚‚β‰…β‚› : βˆ€ {Ξ“ Ξ” Θ A x} {{_ : T (fresh x Ξ“)}} β†’
                (M : Ξ” ⊒ A) (Ξ³ : Ξ” β‹™ Ξ“) (Ξ΄ : Θ β‹™ Ξ”) β†’
                [ Ξ³ , x ≔ M ] ● Ξ΄ β‰…β‚› [ Ξ³ ● Ξ΄ , x ≔ M β–Ά Ξ΄ ]
    conv₃≅ₛ : βˆ€ {Ξ“ Ξ” A x} {{_ : T (fresh x Ξ“)}} β†’
                (c : [ Ξ“ , x ∷ A ] βŠ‡ Ξ“) (M : Ξ” ⊒ A) (Ξ³ : Ξ” β‹™ Ξ“) β†’
                Ο€βŸ¨ c ⟩ ● [ Ξ³ , x ≔ M ] β‰…β‚› Ξ³
    convβ‚„β‰…β‚› : βˆ€ {Ξ“ Ξ” Θ} β†’
                (c : Θ βŠ‡ Ξ“) (cβ€² : Ξ” βŠ‡ Ξ“) (cβ€³ : Θ βŠ‡ Ξ”) β†’
                Ο€βŸ¨ cβ€² ⟩ ● Ο€βŸ¨ cβ€³ ⟩ β‰…β‚› Ο€βŸ¨ c ⟩
    convβ‚…β‰…β‚› : βˆ€ {Ξ“ Ξ”} β†’
                (c : Ξ” βŠ‡ Ξ”) (Ξ³ : Ξ” β‹™ Ξ“) β†’
                Ξ³ ● Ο€βŸ¨ c ⟩ β‰…β‚› Ξ³
    conv₆≅ₛ : βˆ€ {Ξ“} β†’
                (c : Ξ“ βŠ‡ []) (Ξ³ : Ξ“ β‹™ []) β†’
                Ξ³ β‰…β‚› Ο€βŸ¨ c ⟩
    conv₇≅ₛ : βˆ€ {Ξ“ Ξ” A x} {{_ : T (fresh x Ξ“)}} β†’
                (c : [ Ξ“ , x ∷ A ] βŠ‡ Ξ“) (Ξ³ : Ξ” β‹™ [ Ξ“ , x ∷ A ]) (i : [ Ξ“ , x ∷ A ] βˆ‹ x ∷ A) β†’
                Ξ³ β‰…β‚› [ Ο€βŸ¨ c ⟩ ● Ξ³ , x ≔ Ξ½ x i β–Ά Ξ³ ]

-- The first two `conv≅` rules correspond to the ordinary β- and η-rules, the next three define the effect
-- of substitutions and the last two rules can be seen as the correspondence of the Ξ·-rule for
-- substitutions.  The remaining `conv≅ₛ` rules define how the substitutions distribute.

module _ where
  ≑→≅ : βˆ€ {Ξ“ A} {M Mβ€² : Ξ“ ⊒ A} β†’ M ≑ Mβ€² β†’ M β‰… Mβ€²
  ≑→≅ refl = reflβ‰…

  module β‰…-Reasoning where
    infix 1 begin_
    begin_ : βˆ€ {Ξ“ A} {M Mβ€² : Ξ“ ⊒ A} β†’ M β‰… Mβ€² β†’ M β‰… Mβ€²
    begin p = p

    infixr 2 _β‰…βŸ¨βŸ©_
    _β‰…βŸ¨βŸ©_ : βˆ€ {Ξ“ A} (M {Mβ€²} : Ξ“ ⊒ A) β†’ M β‰… Mβ€² β†’ M β‰… Mβ€²
    M β‰…βŸ¨βŸ© p = p

    infixr 2 _β‰…βŸ¨_⟩_
    _β‰…βŸ¨_⟩_ : βˆ€ {Ξ“ A} (M {Mβ€² Mβ€³} : Ξ“ ⊒ A) β†’ M β‰… Mβ€² β†’ Mβ€² β‰… Mβ€³ β†’ M β‰… Mβ€³
    M β‰…βŸ¨ p ⟩ pβ€² = transβ‰… p pβ€²

    infixr 2 _β‰‘βŸ¨βŸ©_
    _β‰‘βŸ¨βŸ©_ : βˆ€ {Ξ“ A} (M {Mβ€²} : Ξ“ ⊒ A) β†’ M β‰… Mβ€² β†’ M β‰… Mβ€²
    M β‰‘βŸ¨βŸ© p = p

    infixr 2 _β‰‘βŸ¨_⟩_
    _β‰‘βŸ¨_⟩_ : βˆ€ {Ξ“ A} (M {Mβ€² Mβ€³} : Ξ“ ⊒ A) β†’ M ≑ Mβ€² β†’ Mβ€² β‰… Mβ€³ β†’ M β‰… Mβ€³
    M β‰‘βŸ¨ p ⟩ pβ€² = transβ‰… (≑→≅ p) pβ€²

    infix 3 _∎
    _∎ : βˆ€ {Ξ“ A} (M : Ξ“ ⊒ A) β†’ M β‰… M
    M ∎ = reflβ‰…

  ≑→≅ₛ : βˆ€ {Ξ“ Ξ”} {Ξ³ Ξ³β€² : Ξ” β‹™ Ξ“} β†’ Ξ³ ≑ Ξ³β€² β†’ Ξ³ β‰…β‚› Ξ³β€²
  ≑→≅ₛ refl = reflβ‰…β‚›

  module β‰…β‚›-Reasoning where
    infix 1 begin_
    begin_ : βˆ€ {Ξ“ Ξ”} {Ξ³ Ξ³β€² : Ξ” β‹™ Ξ“} β†’ Ξ³ β‰…β‚› Ξ³β€² β†’ Ξ³ β‰…β‚› Ξ³β€²
    begin p = p

    infixr 2 _β‰…β‚›βŸ¨βŸ©_
    _β‰…β‚›βŸ¨βŸ©_ : βˆ€ {Ξ“ Ξ”} (Ξ³ {Ξ³β€²} : Ξ” β‹™ Ξ“) β†’ Ξ³ β‰…β‚› Ξ³β€² β†’ Ξ³ β‰…β‚› Ξ³β€²
    Ξ³ β‰…β‚›βŸ¨βŸ© p = p

    infixr 2 _β‰…β‚›βŸ¨_⟩_
    _β‰…β‚›βŸ¨_⟩_ : βˆ€ {Ξ“ Ξ”} (Ξ³ {Ξ³β€² Ξ³β€³} : Ξ” β‹™ Ξ“) β†’ Ξ³ β‰…β‚› Ξ³β€² β†’ Ξ³β€² β‰…β‚› Ξ³β€³ β†’ Ξ³ β‰…β‚› Ξ³β€³
    Ξ³ β‰…β‚›βŸ¨ p ⟩ pβ€² = transβ‰…β‚› p pβ€²

    infixr 2 _β‰‘βŸ¨βŸ©_
    _β‰‘βŸ¨βŸ©_ : βˆ€ {Ξ“ Ξ”} (Ξ³ {Ξ³β€²} : Ξ” β‹™ Ξ“) β†’ Ξ³ β‰…β‚› Ξ³β€² β†’ Ξ³ β‰…β‚› Ξ³β€²
    Ξ³ β‰‘βŸ¨βŸ© p = p

    infixr 2 _β‰‘βŸ¨_⟩_
    _β‰‘βŸ¨_⟩_ : βˆ€ {Ξ“ Ξ”} (Ξ³ {Ξ³β€² Ξ³β€³} : Ξ” β‹™ Ξ“) β†’ Ξ³ ≑ Ξ³β€² β†’ Ξ³β€² β‰…β‚› Ξ³β€³ β†’ Ξ³ β‰…β‚› Ξ³β€³
    Ξ³ β‰‘βŸ¨ p ⟩ pβ€² = transβ‰…β‚› (≑→≅ₛ p) pβ€²

    infix 3 _∎
    _∎ : βˆ€ {Ξ“ Ξ”} (Ξ³ : Ξ” β‹™ Ξ“) β†’ Ξ³ β‰…β‚› Ξ³
    Ξ³ ∎ = reflβ‰…β‚›