------------------------------------------------------------------------
-- Typing and reduction relations
------------------------------------------------------------------------

open import Definition.Typed.Restrictions
open import Graded.Modality

module Definition.Typed
  {ā„“} {M : Set ā„“}
  {š•„ : Modality M}
  (R : Type-restrictions š•„)
  where

open Type-restrictions R

open import Definition.Typed.Variant

open import Definition.Untyped M
import Definition.Untyped.Erased š•„ as Erased
open import Definition.Untyped.Whnf M type-variant

open import Tools.Fin
open import Tools.Nat
open import Tools.Product
import Tools.PropositionalEquality as PE
open import Tools.Relation
import Tools.Vec as Vec

infix 24 āˆ™_

private
  variable
    m n l lā‚ lā‚‚ Ī± : Nat
    āˆ‡ āˆ‡ā€² : DCon (Term 0) _
    Ļ† Ļ†ā€² : Unfolding _
    Ļ‰ : Opacity _
    Ī“ : Con Term _
    A Aā‚ Aā‚‚ Aā€² B Bā‚ Bā‚‚ C E F Fā€² G H : Term _
    a f g nā€² s sā€² t tā‚ tā‚‚ tā€² u uā‚ uā‚‚ uā€² v vā‚ vā‚‚ vā€² w wā‚ wā‚‚ wā€² z zā€² :
      Term _
    Ļƒ Ļƒā€² : Subst _ _
    x : Fin _
    p pā€² q qā€² r : M
    b : BinderMode
    k : Strength

-- Well-typed variables
data _āˆ·_āˆˆ_ : (x : Fin n) (A : Term n) (Ī“ : Con Term n) ā†’ Set ā„“ where
  here  :                 x0 āˆ· wk1 A āˆˆ Ī“ āˆ™ A
  there : x āˆ· A āˆˆ Ī“ ā†’ (x +1) āˆ· wk1 A āˆˆ Ī“ āˆ™ B

opaque
  unfolding _āŠ”įµ’_

  infixl 5 _āŠ”įµ’įµ—_

  -- Definition context unfolding.

  _āŠ”įµ’įµ—_ : Unfolding n ā†’ Unfolding n ā†’ Unfolding n
  _āŠ”įµ’įµ—_ with unfolding-mode
  ā€¦ | explicit   = Ī» Ļ† _ ā†’ Ļ†
  ā€¦ | transitive = _āŠ”įµ’_

opaque

  -- Transparentisation.

  Trans : Unfolding n ā†’ DCon (Term 0) n ā†’ DCon (Term 0) n
  Trans _ Īµ =
    Īµ
  Trans Ļ† (āˆ‡ āˆ™āŸØ tra āŸ©[ t āˆ· A ]) =
    Trans (Vec.tail Ļ†) āˆ‡ āˆ™āŸØ tra āŸ©[ t āˆ· A ]
  Trans (Ļ† ā°) (āˆ‡ āˆ™āŸØ Ļ‰ āŸ©[ t āˆ· A ]) =
    Trans Ļ† āˆ‡ āˆ™āŸØ Ļ‰ āŸ©[ t āˆ· A ]
  Trans (Ļ† Ā¹) (āˆ‡ āˆ™āŸØ opa Ļ†ā€² āŸ©[ t āˆ· A ]) =
    Trans (Ļ† āŠ”įµ’įµ— Ļ†ā€²) āˆ‡ āˆ™āŸØ tra āŸ©[ t āˆ· A ]

mutual

  -- Well-formed definition contexts.

  infix 4 Ā»_

  data Ā»_ : DCon (Term 0) m ā†’ Set ā„“ where
    Īµ          : Ā» Īµ
    āˆ™įµ’āŸØ_āŸ©[_āˆ·_] : Opacity-allowed
               ā†’ Trans Ļ† āˆ‡ Ā» Īµ āŠ¢ t āˆ· A
               ā†’ āˆ‡ Ā» Īµ āŠ¢ A
               ā†’ Ā» āˆ‡ āˆ™āŸØ opa Ļ† āŸ©[ t āˆ· A ]
    āˆ™įµ—[_]      : āˆ‡ Ā» Īµ āŠ¢ t āˆ· A
               ā†’ Ā» āˆ‡ āˆ™āŸØ tra āŸ©[ t āˆ· A ]

  -- Well-formed contexts.

  infix 4 _Ā»āŠ¢_

  data _Ā»āŠ¢_ (āˆ‡ : DCon (Term 0) m) : Con Term n ā†’ Set ā„“ where
    Īµ  : Ā» āˆ‡       ā†’ āˆ‡ Ā»āŠ¢ Īµ
    āˆ™_ : āˆ‡ Ā» Ī“ āŠ¢ A ā†’ āˆ‡ Ā»āŠ¢ Ī“ āˆ™ A

  pattern ĪµĪµ = Īµ Īµ

  -- A variant of _Ā»āŠ¢_.

  infix 4 āŠ¢_

  āŠ¢_ : Cons m n ā†’ Set ā„“
  āŠ¢ āˆ‡ Ā» Ī“ = āˆ‡ Ā»āŠ¢ Ī“

  -- Well-formed types.

  infix 4 _āŠ¢_

  data _āŠ¢_ (Ī“ : Cons m n) : Term n ā†’ Set ā„“ where
    Uā±¼     : āŠ¢ Ī“ ā†’ Ī“ āŠ¢ U l
    univ   : Ī“ āŠ¢ A āˆ· U l
           ā†’ Ī“ āŠ¢ A
    Emptyā±¼ : āŠ¢ Ī“ ā†’ Ī“ āŠ¢ Empty
    Unitā±¼  : āŠ¢ Ī“ ā†’ Unit-allowed k ā†’ Ī“ āŠ¢ Unit k l
    Ī Ī£ā±¼    : Ī“ Ā»āˆ™ A āŠ¢ B
           ā†’ Ī Ī£-allowed b p q
           ā†’ Ī“ āŠ¢ Ī Ī£āŸØ b āŸ© p , q ā–· A ā–¹ B
    ā„•ā±¼     : āŠ¢ Ī“ ā†’ Ī“ āŠ¢ ā„•
    Idā±¼    : Ī“ āŠ¢ A
           ā†’ Ī“ āŠ¢ t āˆ· A
           ā†’ Ī“ āŠ¢ u āˆ· A
           ā†’ Ī“ āŠ¢ Id A t u

  -- Well-typed terms.

  infix 4 _āŠ¢_āˆ·_

  data _āŠ¢_āˆ·_ (Ī“ : Cons m n) : Term n ā†’ Term n ā†’ Set ā„“ where
    conv      : Ī“ āŠ¢ t āˆ· A
              ā†’ Ī“ āŠ¢ A ā‰” B
              ā†’ Ī“ āŠ¢ t āˆ· B

    var       : āŠ¢ Ī“
              ā†’ x āˆ· A āˆˆ Ī“ .vars
              ā†’ Ī“ āŠ¢ var x āˆ· A
    defn      : āŠ¢ Ī“
              ā†’ Ī± ā†¦āˆ· Aā€² āˆˆ Ī“ .defs
              ā†’ A PE.ā‰” wk wkā‚€ Aā€²
              ā†’ Ī“ āŠ¢ defn Ī± āˆ· A

    Uā±¼        : āŠ¢ Ī“ ā†’ Ī“ āŠ¢ U l āˆ· U (1+ l)

    Emptyā±¼    : āŠ¢ Ī“ ā†’ Ī“ āŠ¢ Empty āˆ· U 0
    emptyrecā±¼ : Ī“ āŠ¢ A ā†’ Ī“ āŠ¢ t āˆ· Empty ā†’ Ī“ āŠ¢ emptyrec p A t āˆ· A

    Unitā±¼     : āŠ¢ Ī“ ā†’ Unit-allowed k ā†’ Ī“ āŠ¢ Unit k l āˆ· U l
    starā±¼     : āŠ¢ Ī“ ā†’ Unit-allowed k ā†’ Ī“ āŠ¢ star k l āˆ· Unit k l
    unitrecā±¼  : Ī“ Ā»āˆ™ UnitŹ· l āŠ¢ A
              ā†’ Ī“ āŠ¢ t āˆ· UnitŹ· l
              ā†’ Ī“ āŠ¢ u āˆ· A [ starŹ· l ]ā‚€
              ā†’ UnitŹ·-allowed
              ā†’ Ī“ āŠ¢ unitrec l p q A t u āˆ· A [ t ]ā‚€

    Ī Ī£ā±¼       : Ī“ āŠ¢ F āˆ· U lā‚
              ā†’ Ī“ Ā»āˆ™ F āŠ¢ G āˆ· U lā‚‚
              ā†’ Ī Ī£-allowed b p q
              ā†’ Ī“ āŠ¢ Ī Ī£āŸØ b āŸ© p , q ā–· F ā–¹ G āˆ· U (lā‚ āŠ”įµ˜ lā‚‚)

    lamā±¼      : Ī“ Ā»āˆ™ F āŠ¢ G
              ā†’ Ī“ Ā»āˆ™ F āŠ¢ t āˆ· G
              ā†’ Ī -allowed p q
              ā†’ Ī“ āŠ¢ lam p t āˆ· Ī  p , q ā–· F ā–¹ G
    _āˆ˜ā±¼_      : Ī“ āŠ¢ t āˆ· Ī  p , q ā–· F ā–¹ G
              ā†’ Ī“ āŠ¢ u āˆ· F
              ā†’ Ī“ āŠ¢ t āˆ˜āŸØ p āŸ© u āˆ· G [ u ]ā‚€

    prodā±¼     : Ī“ Ā»āˆ™ F āŠ¢ G
              ā†’ Ī“ āŠ¢ t āˆ· F
              ā†’ Ī“ āŠ¢ u āˆ· G [ t ]ā‚€
              ā†’ Ī£-allowed k p q
              ā†’ Ī“ āŠ¢ prod k p t u āˆ· Ī£āŸØ k āŸ© p , q ā–· F ā–¹ G
    fstā±¼      : Ī“ Ā»āˆ™ F āŠ¢ G
              ā†’ Ī“ āŠ¢ t āˆ· Ī£Ė¢ p , q ā–· F ā–¹ G
              ā†’ Ī“ āŠ¢ fst p t āˆ· F
    sndā±¼      : Ī“ Ā»āˆ™ F āŠ¢ G
              ā†’ Ī“ āŠ¢ t āˆ· Ī£Ė¢ p , q ā–· F ā–¹ G
              ā†’ Ī“ āŠ¢ snd p t āˆ· G [ fst p t ]ā‚€
    prodrecā±¼  : Ī“ Ā»āˆ™ (Ī£Ź· p , qā€² ā–· F ā–¹ G) āŠ¢ A
              ā†’ Ī“ āŠ¢ t āˆ· Ī£Ź· p , qā€² ā–· F ā–¹ G
              ā†’ Ī“ Ā»āˆ™ F Ā»āˆ™ G āŠ¢ u āˆ· A [ prodŹ· p (var x1) (var x0) ]ā†‘Ā²
              ā†’ Ī£Ź·-allowed p qā€²
              ā†’ Ī“ āŠ¢ prodrec r p q A t u āˆ· A [ t ]ā‚€

    ā„•ā±¼        : āŠ¢ Ī“ ā†’ Ī“ āŠ¢ ā„• āˆ· U 0
    zeroā±¼     : āŠ¢ Ī“
              ā†’ Ī“ āŠ¢ zero āˆ· ā„•
    sucā±¼      : āˆ€ {n}
              ā†’ Ī“ āŠ¢     n āˆ· ā„•
              ā†’ Ī“ āŠ¢ suc n āˆ· ā„•
    natrecā±¼   : āˆ€ {n}
              ā†’ Ī“ āŠ¢ z āˆ· A [ zero ]ā‚€
              ā†’ Ī“ Ā»āˆ™ ā„• Ā»āˆ™ A āŠ¢ s āˆ· A [ suc (var x1) ]ā†‘Ā²
              ā†’ Ī“ āŠ¢ n āˆ· ā„•
              ā†’ Ī“ āŠ¢ natrec p q r A z s n āˆ· A [ n ]ā‚€

    Idā±¼       : Ī“ āŠ¢ A āˆ· U l
              ā†’ Ī“ āŠ¢ t āˆ· A
              ā†’ Ī“ āŠ¢ u āˆ· A
              ā†’ Ī“ āŠ¢ Id A t u āˆ· U l
    rflā±¼      : Ī“ āŠ¢ t āˆ· A
              ā†’ Ī“ āŠ¢ rfl āˆ· Id A t t
    Jā±¼        : Ī“ āŠ¢ t āˆ· A
              ā†’ Ī“ Ā»āˆ™ A Ā»āˆ™ Id (wk1 A) (wk1 t) (var x0) āŠ¢ B
              ā†’ Ī“ āŠ¢ u āˆ· B [ t , rfl ]ā‚ā‚€
              ā†’ Ī“ āŠ¢ v āˆ· A
              ā†’ Ī“ āŠ¢ w āˆ· Id A t v
              ā†’ Ī“ āŠ¢ J p q A t B u v w āˆ· B [ v , w ]ā‚ā‚€
    Kā±¼        : Ī“ Ā»āˆ™ Id A t t āŠ¢ B
              ā†’ Ī“ āŠ¢ u āˆ· B [ rfl ]ā‚€
              ā†’ Ī“ āŠ¢ v āˆ· Id A t t
              ā†’ K-allowed
              ā†’ Ī“ āŠ¢ K p A t B u v āˆ· B [ v ]ā‚€
    []-congā±¼  : Ī“ āŠ¢ A
              ā†’ Ī“ āŠ¢ t āˆ· A
              ā†’ Ī“ āŠ¢ u āˆ· A
              ā†’ Ī“ āŠ¢ v āˆ· Id A t u
              ā†’ []-cong-allowed k
              ā†’ let open Erased k in
                Ī“ āŠ¢ []-cong k A t u v āˆ·
                  Id (Erased A) ([ t ]) ([ u ])

  -- Type equality.

  infix 4 _āŠ¢_ā‰”_

  data _āŠ¢_ā‰”_ (Ī“ : Cons m n) : Term n ā†’ Term n ā†’ Set ā„“ where
    refl   : Ī“ āŠ¢ A
           ā†’ Ī“ āŠ¢ A ā‰” A
    sym    : Ī“ āŠ¢ A ā‰” B
           ā†’ Ī“ āŠ¢ B ā‰” A
    trans  : Ī“ āŠ¢ A ā‰” B
           ā†’ Ī“ āŠ¢ B ā‰” C
           ā†’ Ī“ āŠ¢ A ā‰” C
    univ   : Ī“ āŠ¢ A ā‰” B āˆ· U l
           ā†’ Ī“ āŠ¢ A ā‰” B
    Ī Ī£-cong
           : Ī“ āŠ¢ F ā‰” H
           ā†’ Ī“ Ā»āˆ™ F āŠ¢ G ā‰” E
           ā†’ Ī Ī£-allowed b p q
           ā†’ Ī“ āŠ¢ Ī Ī£āŸØ b āŸ© p , q ā–· F ā–¹ G ā‰” Ī Ī£āŸØ b āŸ© p , q ā–· H ā–¹ E
    Id-cong
           : Ī“ āŠ¢ Aā‚ ā‰” Aā‚‚
           ā†’ Ī“ āŠ¢ tā‚ ā‰” tā‚‚ āˆ· Aā‚
           ā†’ Ī“ āŠ¢ uā‚ ā‰” uā‚‚ āˆ· Aā‚
           ā†’ Ī“ āŠ¢ Id Aā‚ tā‚ uā‚ ā‰” Id Aā‚‚ tā‚‚ uā‚‚

  -- Term equality.

  infix 4 _āŠ¢_ā‰”_āˆ·_

  data _āŠ¢_ā‰”_āˆ·_ (Ī“ : Cons m n) : Term n ā†’ Term n ā†’ Term n ā†’ Set ā„“ where
    conv          : Ī“ āŠ¢ t ā‰” u āˆ· A
                  ā†’ Ī“ āŠ¢ A ā‰” B
                  ā†’ Ī“ āŠ¢ t ā‰” u āˆ· B

    refl          : Ī“ āŠ¢ t āˆ· A
                  ā†’ Ī“ āŠ¢ t ā‰” t āˆ· A
    sym           : Ī“ āŠ¢ A
                  ā†’ Ī“ āŠ¢ t ā‰” u āˆ· A
                  ā†’ Ī“ āŠ¢ u ā‰” t āˆ· A
    trans         : Ī“ āŠ¢ t ā‰” u āˆ· A
                  ā†’ Ī“ āŠ¢ u ā‰” v āˆ· A
                  ā†’ Ī“ āŠ¢ t ā‰” v āˆ· A

    Ī“-red         : āŠ¢ Ī“
                  ā†’ Ī± ā†¦ tā€² āˆ· Aā€² āˆˆ Ī“ .defs
                  ā†’ A PE.ā‰” wk wkā‚€ Aā€²
                  ā†’ t PE.ā‰” wk wkā‚€ tā€²
                  ā†’ Ī“ āŠ¢ defn Ī± ā‰” t āˆ· A

    emptyrec-cong : Ī“ āŠ¢ A ā‰” B
                  ā†’ Ī“ āŠ¢ t ā‰” u āˆ· Empty
                  ā†’ Ī“ āŠ¢ emptyrec p A t ā‰” emptyrec p B u āˆ· A

    Ī·-unit        : Ī“ āŠ¢ t āˆ· Unit k l
                  ā†’ Ī“ āŠ¢ tā€² āˆ· Unit k l
                  ā†’ Unit-with-Ī· k
                  ā†’ Ī“ āŠ¢ t ā‰” tā€² āˆ· Unit k l

    unitrec-cong  : Ī“ Ā»āˆ™ UnitŹ· l āŠ¢ A ā‰” Aā€²
                  ā†’ Ī“ āŠ¢ t ā‰” tā€² āˆ· UnitŹ· l
                  ā†’ Ī“ āŠ¢ u ā‰” uā€² āˆ· A [ starŹ· l ]ā‚€
                  ā†’ UnitŹ·-allowed
                  ā†’ Ā¬ UnitŹ·-Ī·
                  ā†’ Ī“ āŠ¢ unitrec l p q A t u ā‰” unitrec l p q Aā€² tā€² uā€² āˆ·
                      A [ t ]ā‚€
    unitrec-Ī²     : Ī“ Ā»āˆ™ UnitŹ· l āŠ¢ A
                  ā†’ Ī“ āŠ¢ u āˆ· A [ starŹ· l ]ā‚€
                  ā†’ UnitŹ·-allowed
                  ā†’ Ā¬ UnitŹ·-Ī·
                  ā†’ Ī“ āŠ¢ unitrec l p q A (starŹ· l) u ā‰” u āˆ· A [ starŹ· l ]ā‚€
    unitrec-Ī²-Ī·   : Ī“ Ā»āˆ™ UnitŹ· l āŠ¢ A
                  ā†’ Ī“ āŠ¢ t āˆ· UnitŹ· l
                  ā†’ Ī“ āŠ¢ u āˆ· A [ starŹ· l ]ā‚€
                  ā†’ UnitŹ·-allowed
                  ā†’ UnitŹ·-Ī·
                  ā†’ Ī“ āŠ¢ unitrec l p q A t u ā‰” u āˆ· A [ t ]ā‚€

    Ī Ī£-cong       : Ī“ āŠ¢ F ā‰” H āˆ· U lā‚
                  ā†’ Ī“ Ā»āˆ™ F āŠ¢ G ā‰” E āˆ· U lā‚‚
                  ā†’ Ī Ī£-allowed b p q
                  ā†’ Ī“ āŠ¢ Ī Ī£āŸØ b āŸ© p , q ā–· F ā–¹ G ā‰” Ī Ī£āŸØ b āŸ© p , q ā–· H ā–¹ E āˆ·
                      U (lā‚ āŠ”įµ˜ lā‚‚)

    app-cong      : āˆ€ {b}
                  ā†’ Ī“ āŠ¢ f ā‰” g āˆ· Ī  p , q ā–· F ā–¹ G
                  ā†’ Ī“ āŠ¢ a ā‰” b āˆ· F
                  ā†’ Ī“ āŠ¢ f āˆ˜āŸØ p āŸ© a ā‰” g āˆ˜āŸØ p āŸ© b āˆ· G [ a ]ā‚€
    Ī²-red         : Ī“ Ā»āˆ™ F āŠ¢ G
                  ā†’ Ī“ Ā»āˆ™ F āŠ¢ t āˆ· G
                  ā†’ Ī“ āŠ¢ a āˆ· F
                  ā†’ p PE.ā‰” pā€²
                  ā†’ -- Note that q can be chosen arbitrarily.
                    Ī -allowed p q
                  ā†’ Ī“ āŠ¢ lam p t āˆ˜āŸØ pā€² āŸ© a ā‰” t [ a ]ā‚€ āˆ· G [ a ]ā‚€
    Ī·-eq          : Ī“ Ā»āˆ™ F āŠ¢ G
                  ā†’ Ī“ āŠ¢ f āˆ· Ī  p , q ā–· F ā–¹ G
                  ā†’ Ī“ āŠ¢ g āˆ· Ī  p , q ā–· F ā–¹ G
                  ā†’ Ī“ Ā»āˆ™ F āŠ¢ wk1 f āˆ˜āŸØ p āŸ© var x0 ā‰” wk1 g āˆ˜āŸØ p āŸ© var x0 āˆ· G
                  ā†’ Ī -allowed p q
                  ā†’ Ī“ āŠ¢ f ā‰” g āˆ· Ī  p , q ā–· F ā–¹ G

    prod-cong     : Ī“ Ā»āˆ™ F āŠ¢ G
                  ā†’ Ī“ āŠ¢ t ā‰” tā€² āˆ· F
                  ā†’ Ī“ āŠ¢ u ā‰” uā€² āˆ· G [ t ]ā‚€
                  ā†’ Ī£-allowed k p q
                  ā†’ Ī“ āŠ¢ prod k p t u ā‰” prod k p tā€² uā€² āˆ· Ī£āŸØ k āŸ© p , q ā–· F ā–¹ G

    fst-cong      : Ī“ Ā»āˆ™ F āŠ¢ G
                  ā†’ Ī“ āŠ¢ t ā‰” tā€² āˆ· Ī£Ė¢ p , q ā–· F ā–¹ G
                  ā†’ Ī“ āŠ¢ fst p t ā‰” fst p tā€² āˆ· F
    Ī£-Ī²ā‚          : Ī“ Ā»āˆ™ F āŠ¢ G
                  ā†’ Ī“ āŠ¢ t āˆ· F
                  ā†’ Ī“ āŠ¢ u āˆ· G [ t ]ā‚€
                  ā†’ p PE.ā‰” pā€²
                  ā†’ -- Note that q can be chosen arbitrarily.
                    Ī£Ė¢-allowed p q
                  ā†’ Ī“ āŠ¢ fst p (prodĖ¢ pā€² t u) ā‰” t āˆ· F
    snd-cong      : Ī“ Ā»āˆ™ F āŠ¢ G
                  ā†’ Ī“ āŠ¢ t ā‰” u āˆ· Ī£Ė¢ p , q ā–· F ā–¹ G
                  ā†’ Ī“ āŠ¢ snd p t ā‰” snd p u āˆ· G [ fst p t ]ā‚€
    Ī£-Ī²ā‚‚          : Ī“ Ā»āˆ™ F āŠ¢ G
                  ā†’ Ī“ āŠ¢ t āˆ· F
                  ā†’ Ī“ āŠ¢ u āˆ· G [ t ]ā‚€
                  ā†’ p PE.ā‰” pā€²
                  ā†’ -- Note that q can be chosen arbitrarily.
                    Ī£Ė¢-allowed p q
                  ā†’ Ī“ āŠ¢ snd p (prodĖ¢ pā€² t u) ā‰” u āˆ· G [ fst p (prodĖ¢ pā€² t u) ]ā‚€
    Ī£-Ī·           : Ī“ Ā»āˆ™ F āŠ¢ G
                  ā†’ Ī“ āŠ¢ t āˆ· Ī£Ė¢ p , q ā–· F ā–¹ G
                  ā†’ Ī“ āŠ¢ u āˆ· Ī£Ė¢ p , q ā–· F ā–¹ G
                  ā†’ Ī“ āŠ¢ fst p t ā‰” fst p u āˆ· F
                  ā†’ Ī“ āŠ¢ snd p t ā‰” snd p u āˆ· G [ fst p t ]ā‚€
                  ā†’ Ī£Ė¢-allowed p q
                  ā†’ Ī“ āŠ¢ t ā‰” u āˆ· Ī£Ė¢ p , q ā–· F ā–¹ G

    prodrec-cong  : Ī“ Ā»āˆ™ Ī£Ź· p , qā€² ā–· F ā–¹ G āŠ¢ A ā‰” Aā€²
                  ā†’ Ī“ āŠ¢ t ā‰” tā€² āˆ· Ī£Ź· p , qā€² ā–· F ā–¹ G
                  ā†’ Ī“ Ā»āˆ™ F Ā»āˆ™ G āŠ¢ u ā‰” uā€² āˆ·
                      A [ prodŹ· p (var x1) (var x0) ]ā†‘Ā²
                  ā†’ Ī£Ź·-allowed p qā€²
                  ā†’ Ī“ āŠ¢ prodrec r p q A t u ā‰” prodrec r p q Aā€² tā€² uā€² āˆ· A [ t ]ā‚€
    prodrec-Ī²     : Ī“ Ā»āˆ™ Ī£Ź· p , qā€² ā–· F ā–¹ G āŠ¢ A
                  ā†’ Ī“ āŠ¢ t āˆ· F
                  ā†’ Ī“ āŠ¢ tā€² āˆ· G [ t ]ā‚€
                  ā†’ Ī“ Ā»āˆ™ F Ā»āˆ™ G āŠ¢ u āˆ· A [ prodŹ· p (var x1) (var x0) ]ā†‘Ā²
                  ā†’ p PE.ā‰” pā€²
                  ā†’ Ī£Ź·-allowed p qā€²
                  ā†’ Ī“ āŠ¢ prodrec r p q A (prodŹ· pā€² t tā€²) u ā‰”
                        u [ t , tā€² ]ā‚ā‚€ āˆ· A [ prodŹ· pā€² t tā€² ]ā‚€

    suc-cong      : āˆ€ {n}
                  ā†’ Ī“ āŠ¢ t ā‰” n āˆ· ā„•
                  ā†’ Ī“ āŠ¢ suc t ā‰” suc n āˆ· ā„•
    natrec-cong   : āˆ€ {n}
                  ā†’ Ī“ Ā»āˆ™ ā„• āŠ¢ A ā‰” Aā€²
                  ā†’ Ī“ āŠ¢ z ā‰” zā€² āˆ· A [ zero ]ā‚€
                  ā†’ Ī“ Ā»āˆ™ ā„• Ā»āˆ™ A āŠ¢ s ā‰” sā€² āˆ· A [ suc (var x1) ]ā†‘Ā²
                  ā†’ Ī“ āŠ¢ n ā‰” nā€² āˆ· ā„•
                  ā†’ Ī“ āŠ¢ natrec p q r A z s n ā‰”
                      natrec p q r Aā€² zā€² sā€² nā€² āˆ· A [ n ]ā‚€
    natrec-zero   : Ī“ āŠ¢ z āˆ· A [ zero ]ā‚€
                  ā†’ Ī“ Ā»āˆ™ ā„• Ā»āˆ™ A āŠ¢ s āˆ· A [ suc (var x1) ]ā†‘Ā²
                  ā†’ Ī“ āŠ¢ natrec p q r A z s zero ā‰” z āˆ· A [ zero ]ā‚€
    natrec-suc    : āˆ€ {n}
                  ā†’ Ī“ āŠ¢ z āˆ· A [ zero ]ā‚€
                  ā†’ Ī“ Ā»āˆ™ ā„• Ā»āˆ™ A āŠ¢ s āˆ· A [ suc (var x1) ]ā†‘Ā²
                  ā†’ Ī“ āŠ¢ n āˆ· ā„•
                  ā†’ Ī“ āŠ¢ natrec p q r A z s (suc n) ā‰”
                      s [ n , natrec p q r A z s n ]ā‚ā‚€ āˆ· A [ suc n ]ā‚€

    Id-cong       : Ī“ āŠ¢ Aā‚ ā‰” Aā‚‚ āˆ· U l
                  ā†’ Ī“ āŠ¢ tā‚ ā‰” tā‚‚ āˆ· Aā‚
                  ā†’ Ī“ āŠ¢ uā‚ ā‰” uā‚‚ āˆ· Aā‚
                  ā†’ Ī“ āŠ¢ Id Aā‚ tā‚ uā‚ ā‰” Id Aā‚‚ tā‚‚ uā‚‚ āˆ· U l
    J-cong        : Ī“ āŠ¢ Aā‚ ā‰” Aā‚‚
                  ā†’ Ī“ āŠ¢ tā‚ āˆ· Aā‚
                  ā†’ Ī“ āŠ¢ tā‚ ā‰” tā‚‚ āˆ· Aā‚
                  ā†’ Ī“ Ā»āˆ™ Aā‚ Ā»āˆ™ Id (wk1 Aā‚) (wk1 tā‚) (var x0) āŠ¢ Bā‚ ā‰” Bā‚‚
                  ā†’ Ī“ āŠ¢ uā‚ ā‰” uā‚‚ āˆ· Bā‚ [ tā‚ , rfl ]ā‚ā‚€
                  ā†’ Ī“ āŠ¢ vā‚ ā‰” vā‚‚ āˆ· Aā‚
                  ā†’ Ī“ āŠ¢ wā‚ ā‰” wā‚‚ āˆ· Id Aā‚ tā‚ vā‚
                  ā†’ Ī“ āŠ¢ J p q Aā‚ tā‚ Bā‚ uā‚ vā‚ wā‚ ā‰”
                        J p q Aā‚‚ tā‚‚ Bā‚‚ uā‚‚ vā‚‚ wā‚‚ āˆ· Bā‚ [ vā‚ , wā‚ ]ā‚ā‚€
    J-Ī²           : Ī“ āŠ¢ t āˆ· A
                  ā†’ Ī“ Ā»āˆ™ A Ā»āˆ™ Id (wk1 A) (wk1 t) (var x0) āŠ¢ B
                  ā†’ Ī“ āŠ¢ u āˆ· B [ t , rfl ]ā‚ā‚€
                  ā†’ t PE.ā‰” tā€²
                  ā†’ Ī“ āŠ¢ J p q A t B u tā€² rfl ā‰” u āˆ· B [ t , rfl ]ā‚ā‚€
    K-cong        : Ī“ āŠ¢ Aā‚ ā‰” Aā‚‚
                  ā†’ Ī“ āŠ¢ tā‚ ā‰” tā‚‚ āˆ· Aā‚
                  ā†’ Ī“ Ā»āˆ™ Id Aā‚ tā‚ tā‚ āŠ¢ Bā‚ ā‰” Bā‚‚
                  ā†’ Ī“ āŠ¢ uā‚ ā‰” uā‚‚ āˆ· Bā‚ [ rfl ]ā‚€
                  ā†’ Ī“ āŠ¢ vā‚ ā‰” vā‚‚ āˆ· Id Aā‚ tā‚ tā‚
                  ā†’ K-allowed
                  ā†’ Ī“ āŠ¢ K p Aā‚ tā‚ Bā‚ uā‚ vā‚ ā‰” K p Aā‚‚ tā‚‚ Bā‚‚ uā‚‚ vā‚‚ āˆ·
                      Bā‚ [ vā‚ ]ā‚€
    K-Ī²           : Ī“ Ā»āˆ™ Id A t t āŠ¢ B
                  ā†’ Ī“ āŠ¢ u āˆ· B [ rfl ]ā‚€
                  ā†’ K-allowed
                  ā†’ Ī“ āŠ¢ K p A t B u rfl ā‰” u āˆ· B [ rfl ]ā‚€
    []-cong-cong  : Ī“ āŠ¢ Aā‚ ā‰” Aā‚‚
                  ā†’ Ī“ āŠ¢ tā‚ ā‰” tā‚‚ āˆ· Aā‚
                  ā†’ Ī“ āŠ¢ uā‚ ā‰” uā‚‚ āˆ· Aā‚
                  ā†’ Ī“ āŠ¢ vā‚ ā‰” vā‚‚ āˆ· Id Aā‚ tā‚ uā‚
                  ā†’ []-cong-allowed k
                  ā†’ let open Erased k in
                    Ī“ āŠ¢ []-cong k Aā‚ tā‚ uā‚ vā‚ ā‰” []-cong k Aā‚‚ tā‚‚ uā‚‚ vā‚‚ āˆ·
                      Id (Erased Aā‚) ([ tā‚ ]) ([ uā‚ ])
    []-cong-Ī²     : Ī“ āŠ¢ t āˆ· A
                  ā†’ t PE.ā‰” tā€²
                  ā†’ []-cong-allowed k
                  ā†’ let open Erased k in
                    Ī“ āŠ¢ []-cong k A t tā€² rfl ā‰” rfl āˆ·
                      Id (Erased A) ([ t ]) ([ tā€² ])
    equality-reflection
                  : Equality-reflection
                  ā†’ Ī“ āŠ¢ Id A t u
                  ā†’ Ī“ āŠ¢ v āˆ· Id A t u
                  ā†’ Ī“ āŠ¢ t ā‰” u āˆ· A

-- Term reduction.

infix 4 _āŠ¢_ā‡’_āˆ·_

data _āŠ¢_ā‡’_āˆ·_ (Ī“ : Cons m n) : Term n ā†’ Term n ā†’ Term n ā†’ Set ā„“ where
  conv           : Ī“ āŠ¢ t ā‡’ u āˆ· A
                 ā†’ Ī“ āŠ¢ A ā‰” B
                 ā†’ Ī“ āŠ¢ t ā‡’ u āˆ· B

  Ī“-red          : āŠ¢ Ī“
                 ā†’ Ī± ā†¦ tā€² āˆ· Aā€² āˆˆ Ī“ .defs
                 ā†’ A PE.ā‰” wk wkā‚€ Aā€²
                 ā†’ t PE.ā‰” wk wkā‚€ tā€²
                 ā†’ Ī“ āŠ¢ defn Ī± ā‡’ t āˆ· A

  emptyrec-subst : āˆ€ {n}
                 ā†’ Ī“ āŠ¢ A
                 ā†’ Ī“     āŠ¢ n ā‡’ nā€² āˆ· Empty
                 ā†’ Ī“     āŠ¢ emptyrec p A n ā‡’ emptyrec p A nā€² āˆ· A

  unitrec-subst : Ī“ Ā»āˆ™ UnitŹ· l āŠ¢ A
                ā†’ Ī“ āŠ¢ u āˆ· A [ starŹ· l ]ā‚€
                ā†’ Ī“ āŠ¢ t ā‡’ tā€² āˆ· UnitŹ· l
                ā†’ UnitŹ·-allowed
                ā†’ Ā¬ UnitŹ·-Ī·
                ā†’ Ī“ āŠ¢ unitrec l p q A t u ā‡’ unitrec l p q A tā€² u āˆ·
                    A [ t ]ā‚€
  unitrec-Ī²     : Ī“ Ā»āˆ™ UnitŹ· l āŠ¢ A
                ā†’ Ī“ āŠ¢ u āˆ· A [ starŹ· l ]ā‚€
                ā†’ UnitŹ·-allowed
                ā†’ Ā¬ UnitŹ·-Ī·
                ā†’ Ī“ āŠ¢ unitrec l p q A (starŹ· l) u ā‡’ u āˆ· A [ starŹ· l ]ā‚€
  unitrec-Ī²-Ī·   : Ī“ Ā»āˆ™ UnitŹ· l āŠ¢ A
                ā†’ Ī“ āŠ¢ t āˆ· UnitŹ· l
                ā†’ Ī“ āŠ¢ u āˆ· A [ starŹ· l ]ā‚€
                ā†’ UnitŹ·-allowed
                ā†’ UnitŹ·-Ī·
                ā†’ Ī“ āŠ¢ unitrec l p q A t u ā‡’ u āˆ· A [ t ]ā‚€

  app-subst      : Ī“ āŠ¢ t ā‡’ u āˆ· Ī  p , q ā–· F ā–¹ G
                 ā†’ Ī“ āŠ¢ a āˆ· F
                 ā†’ Ī“ āŠ¢ t āˆ˜āŸØ p āŸ© a ā‡’ u āˆ˜āŸØ p āŸ© a āˆ· G [ a ]ā‚€
  Ī²-red          : Ī“ Ā»āˆ™ F āŠ¢ G
                 ā†’ Ī“ Ā»āˆ™ F āŠ¢ t āˆ· G
                 ā†’ Ī“ āŠ¢ a āˆ· F
                 ā†’ p PE.ā‰” pā€²
                 ā†’ -- Note that q can be chosen arbitrarily.
                   Ī -allowed p q
                 ā†’ Ī“ āŠ¢ lam p t āˆ˜āŸØ pā€² āŸ© a ā‡’ t [ a ]ā‚€ āˆ· G [ a ]ā‚€

  fst-subst      : Ī“ Ā»āˆ™ F āŠ¢ G
                 ā†’ Ī“ āŠ¢ t ā‡’ u āˆ· Ī£Ė¢ p , q ā–· F ā–¹ G
                 ā†’ Ī“ āŠ¢ fst p t ā‡’ fst p u āˆ· F
  Ī£-Ī²ā‚           : Ī“ Ā»āˆ™ F āŠ¢ G
                 ā†’ Ī“ āŠ¢ t āˆ· F
                 ā†’ Ī“ āŠ¢ u āˆ· G [ t ]ā‚€
                 ā†’ p PE.ā‰” pā€²
                 ā†’ -- Note that q can be chosen arbitrarily.
                   Ī£Ė¢-allowed p q
                 ā†’ Ī“ āŠ¢ fst p (prodĖ¢ pā€² t u) ā‡’ t āˆ· F
  snd-subst      : Ī“ Ā»āˆ™ F āŠ¢ G
                 ā†’ Ī“ āŠ¢ t ā‡’ u āˆ· Ī£Ė¢ p , q ā–· F ā–¹ G
                 ā†’ Ī“ āŠ¢ snd p t ā‡’ snd p u āˆ· G [ fst p t ]ā‚€
  Ī£-Ī²ā‚‚           : Ī“ Ā»āˆ™ F āŠ¢ G
                 ā†’ Ī“ āŠ¢ t āˆ· F
                 ā†’ Ī“ āŠ¢ u āˆ· G [ t ]ā‚€
                 ā†’ p PE.ā‰” pā€²
                 ā†’ -- Note that q can be chosen arbitrarily.
                   Ī£Ė¢-allowed p q
                 ā†’ Ī“ āŠ¢ snd p (prodĖ¢ pā€² t u) ā‡’ u āˆ· G [ fst p (prodĖ¢ pā€² t u) ]ā‚€

  prodrec-subst  : Ī“ Ā»āˆ™ Ī£Ź· p , qā€² ā–· F ā–¹ G āŠ¢ A
                 ā†’ Ī“ Ā»āˆ™ F Ā»āˆ™ G āŠ¢ u āˆ· A [ prodŹ· p (var x1) (var x0) ]ā†‘Ā²
                 ā†’ Ī“ āŠ¢ t ā‡’ tā€² āˆ· Ī£Ź· p , qā€² ā–· F ā–¹ G
                 ā†’ Ī£Ź·-allowed p qā€²
                 ā†’ Ī“ āŠ¢ prodrec r p q A t u ā‡’ prodrec r p q A tā€² u āˆ· A [ t ]ā‚€
  prodrec-Ī²      : Ī“ Ā»āˆ™ Ī£Ź· p , qā€² ā–· F ā–¹ G āŠ¢ A
                 ā†’ Ī“ āŠ¢ t āˆ· F
                 ā†’ Ī“ āŠ¢ tā€² āˆ· G [ t ]ā‚€
                 ā†’ Ī“ Ā»āˆ™ F Ā»āˆ™ G āŠ¢ u āˆ· A [ prodŹ· p (var x1) (var x0) ]ā†‘Ā²
                 ā†’ p PE.ā‰” pā€²
                 ā†’ Ī£Ź·-allowed p qā€²
                 ā†’ Ī“ āŠ¢ prodrec r p q A (prodŹ· pā€² t tā€²) u ā‡’
                       u [ t , tā€² ]ā‚ā‚€ āˆ· A [ prodŹ· pā€² t tā€² ]ā‚€

  natrec-subst   : āˆ€ {n}
                 ā†’ Ī“ āŠ¢ z āˆ· A [ zero ]ā‚€
                 ā†’ Ī“ Ā»āˆ™ ā„• Ā»āˆ™ A āŠ¢ s āˆ· A [ suc (var x1) ]ā†‘Ā²
                 ā†’ Ī“ āŠ¢ n ā‡’ nā€² āˆ· ā„•
                 ā†’ Ī“ āŠ¢ natrec p q r A z s n ā‡’ natrec p q r A z s nā€² āˆ·
                     A [ n ]ā‚€
  natrec-zero    : Ī“ āŠ¢ z āˆ· A [ zero ]ā‚€
                 ā†’ Ī“ Ā»āˆ™ ā„• Ā»āˆ™ A āŠ¢ s āˆ· A [ suc (var x1) ]ā†‘Ā²
                 ā†’ Ī“ āŠ¢ natrec p q r A z s zero ā‡’ z āˆ· A [ zero ]ā‚€
  natrec-suc     : āˆ€ {n}
                 ā†’ Ī“ āŠ¢ z āˆ· A [ zero ]ā‚€
                 ā†’ Ī“ Ā»āˆ™ ā„• Ā»āˆ™ A āŠ¢ s āˆ· A [ suc (var x1) ]ā†‘Ā²
                 ā†’ Ī“ āŠ¢ n āˆ· ā„•
                 ā†’ Ī“ āŠ¢ natrec p q r A z s (suc n) ā‡’
                     s [ n , natrec p q r A z s n ]ā‚ā‚€ āˆ· A [ suc n ]ā‚€

  J-subst        : Ī“ āŠ¢ t āˆ· A
                 ā†’ Ī“ Ā»āˆ™ A Ā»āˆ™ Id (wk1 A) (wk1 t) (var x0) āŠ¢ B
                 ā†’ Ī“ āŠ¢ u āˆ· B [ t , rfl ]ā‚ā‚€
                 ā†’ Ī“ āŠ¢ v āˆ· A
                 ā†’ Ī“ āŠ¢ wā‚ ā‡’ wā‚‚ āˆ· Id A t v
                 ā†’ Ī“ āŠ¢ J p q A t B u v wā‚ ā‡’ J p q A t B u v wā‚‚ āˆ·
                     B [ v , wā‚ ]ā‚ā‚€
  J-Ī²            : Ī“ āŠ¢ t āˆ· A
                 ā†’ Ī“ āŠ¢ tā€² āˆ· A
                 ā†’ Ī“ āŠ¢ t ā‰” tā€² āˆ· A
                 ā†’ Ī“ Ā»āˆ™ A Ā»āˆ™ Id (wk1 A) (wk1 t) (var x0) āŠ¢ B
                 ā†’ Ī“ āŠ¢ B [ t , rfl ]ā‚ā‚€ ā‰” B [ tā€² , rfl ]ā‚ā‚€
                 ā†’ Ī“ āŠ¢ u āˆ· B [ t , rfl ]ā‚ā‚€
                 ā†’ Ī“ āŠ¢ J p q A t B u tā€² rfl ā‡’ u āˆ· B [ t , rfl ]ā‚ā‚€
  K-subst        : Ī“ Ā»āˆ™ Id A t t āŠ¢ B
                 ā†’ Ī“ āŠ¢ u āˆ· B [ rfl ]ā‚€
                 ā†’ Ī“ āŠ¢ vā‚ ā‡’ vā‚‚ āˆ· Id A t t
                 ā†’ K-allowed
                 ā†’ Ī“ āŠ¢ K p A t B u vā‚ ā‡’ K p A t B u vā‚‚ āˆ· B [ vā‚ ]ā‚€
  K-Ī²            : Ī“ Ā»āˆ™ Id A t t āŠ¢ B
                 ā†’ Ī“ āŠ¢ u āˆ· B [ rfl ]ā‚€
                 ā†’ K-allowed
                 ā†’ Ī“ āŠ¢ K p A t B u rfl ā‡’ u āˆ· B [ rfl ]ā‚€
  []-cong-subst  : Ī“ āŠ¢ A
                 ā†’ Ī“ āŠ¢ t āˆ· A
                 ā†’ Ī“ āŠ¢ u āˆ· A
                 ā†’ Ī“ āŠ¢ vā‚ ā‡’ vā‚‚ āˆ· Id A t u
                 ā†’ []-cong-allowed k
                 ā†’ let open Erased k in
                   Ī“ āŠ¢ []-cong k A t u vā‚ ā‡’ []-cong k A t u vā‚‚ āˆ·
                     Id (Erased A) ([ t ]) ([ u ])
  []-cong-Ī²      : Ī“ āŠ¢ A
                 ā†’ Ī“ āŠ¢ t āˆ· A
                 ā†’ Ī“ āŠ¢ tā€² āˆ· A
                 ā†’ Ī“ āŠ¢ t ā‰” tā€² āˆ· A
                 ā†’ []-cong-allowed k
                 ā†’ let open Erased k in
                   Ī“ āŠ¢ []-cong k A t tā€² rfl ā‡’ rfl āˆ·
                     Id (Erased A) ([ t ]) ([ tā€² ])

-- Type reduction.

infix 4 _āŠ¢_ā‡’_

data _āŠ¢_ā‡’_ (Ī“ : Cons m n) : Term n ā†’ Term n ā†’ Set ā„“ where
  univ   : Ī“ āŠ¢ A ā‡’ B āˆ· U l
         ā†’ Ī“ āŠ¢ A ā‡’ B

-- A kind of reflexive transitive closure for _āŠ¢_ā‡’_āˆ·_.

infix 4 _āŠ¢_ā‡’*_āˆ·_

data _āŠ¢_ā‡’*_āˆ·_ (Ī“ : Cons m n) : Term n ā†’ Term n ā†’ Term n ā†’ Set ā„“ where
  id  : Ī“ āŠ¢ t āˆ· A
      ā†’ Ī“ āŠ¢ t ā‡’* t āˆ· A
  _ā‡Ø_ : Ī“ āŠ¢ t  ā‡’  tā€² āˆ· A
      ā†’ Ī“ āŠ¢ tā€² ā‡’* u  āˆ· A
      ā†’ Ī“ āŠ¢ t  ā‡’* u  āˆ· A

-- A kind of reflexive transitive closure for _āŠ¢_ā‡’_.

infix 4 _āŠ¢_ā‡’*_

data _āŠ¢_ā‡’*_ (Ī“ : Cons m n) : Term n ā†’ Term n ā†’ Set ā„“ where
  id  : Ī“ āŠ¢ A
      ā†’ Ī“ āŠ¢ A ā‡’* A
  _ā‡Ø_ : Ī“ āŠ¢ A  ā‡’  Aā€²
      ā†’ Ī“ āŠ¢ Aā€² ā‡’* B
      ā†’ Ī“ āŠ¢ A  ā‡’* B

-- Reduction of types to WHNF.

infix 4 _āŠ¢_ā†˜_

_āŠ¢_ā†˜_ : Cons m n ā†’ Term n ā†’ Term n ā†’ Set ā„“
Ī“ āŠ¢ A ā†˜ B = Ī“ āŠ¢ A ā‡’* B Ɨ Whnf (Ī“ .defs) B

-- Reduction of terms to WHNF.

infix 4 _āŠ¢_ā†˜_āˆ·_

_āŠ¢_ā†˜_āˆ·_ : Cons m n ā†’ Term n ā†’ Term n ā†’ Term n ā†’ Set ā„“
Ī“ āŠ¢ t ā†˜ u āˆ· A = Ī“ āŠ¢ t ā‡’* u āˆ· A Ɨ Whnf (Ī“ .defs) u

-- A context pair Ī“ is consistent if the empty type is not inhabited
-- inĀ Ī“.

Consistent : Cons m n ā†’ Set ā„“
Consistent Ī“ = āˆ€ t ā†’ Ā¬ Ī“ āŠ¢ t āˆ· Empty