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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Natrec {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
import Definition.LogicalRelation.Substitution.Irrelevance as S
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Weakening
open import Definition.LogicalRelation.Substitution.Introductions.Nat
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst

open import Tools.Embedding
open import Tools.Product
open import Tools.Empty
import Tools.PropositionalEquality as PE

-- Natural recursion closure reduction (requires reducible terms and equality).
natrec-subst* : ∀ {Γ C c g n n′ l} → Γ ∙ ℕ ⊢ C → Γ ⊢ c ∷ C [ zero ]
              → Γ ⊢ g ∷ Π ℕ ▹ (C ▹▹ C [ suc (var 0) ]↑)
              → Γ ⊢ n ⇒* n′ ∷ ℕ
              → ([ℕ] : Γ ⊩⟨ l ⟩ ℕ)
              → Γ ⊩⟨ l ⟩ n′ ∷ ℕ / [ℕ]
              → (∀ {t t′} → Γ ⊩⟨ l ⟩ t  ∷ ℕ / [ℕ]
                          → Γ ⊩⟨ l ⟩ t′ ∷ ℕ / [ℕ]
                          → Γ ⊩⟨ l ⟩ t ≡ t′ ∷ ℕ / [ℕ]
                          → Γ ⊢ C [ t ] ≡ C [ t′ ])
              → Γ ⊢ natrec C c g n ⇒* natrec C c g n′ ∷ C [ n ]
natrec-subst* C c g (id x) [ℕ] [n′] prop = id (natrecⱼ C c g x)
natrec-subst* C c g (x ⇨ n⇒n′) [ℕ] [n′] prop =
  let q , w = redSubst*Term n⇒n′ [ℕ] [n′]
      a , s = redSubstTerm x [ℕ] q
  in  natrec-subst C c g x ⇨ conv* (natrec-subst* C c g n⇒n′ [ℕ] [n′] prop)
                   (prop q a (symEqTerm [ℕ] s))

-- Helper functions for construction of valid type for the successor case of natrec.

sucCase₃ : ∀ {Γ l} ([Γ] : ⊩ᵛ Γ)
           ([ℕ] : Γ ⊩ᵛ⟨ l ⟩ ℕ / [Γ])
         → Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ suc (var 0) ∷ ℕ / [Γ] ∙″ [ℕ]
                 / (λ {Δ} {σ} → wk1ᵛ {ℕ} {ℕ} [Γ] [ℕ] [ℕ] {Δ} {σ})
sucCase₃ {Γ} {l} [Γ] [ℕ] {Δ} {σ} =
  sucᵛ {n = var 0} {l = l} (_∙″_ {A = ℕ} [Γ] [ℕ])
       (λ {Δ} {σ} → wk1ᵛ {ℕ} {ℕ} [Γ] [ℕ] [ℕ] {Δ} {σ})
       (λ ⊢Δ [σ] → proj₂ [σ] , (λ [σ′] [σ≡σ′] → proj₂ [σ≡σ′])) {Δ} {σ}

sucCase₂ : ∀ {F Γ l} ([Γ] : ⊩ᵛ Γ)
           ([ℕ] : Γ ⊩ᵛ⟨ l ⟩ ℕ / [Γ])
           ([F] : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F / ([Γ] ∙″ [ℕ]))
         → Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F [ suc (var 0) ]↑ / ([Γ] ∙″ [ℕ])
sucCase₂ {F} {Γ} {l} [Γ] [ℕ] [F] =
  subst↑S {ℕ} {F} {suc (var 0)} [Γ] [ℕ] [F]
          (λ {Δ} {σ} → sucCase₃ [Γ] [ℕ] {Δ} {σ})

sucCase₁ : ∀ {F Γ l} ([Γ] : ⊩ᵛ Γ)
           ([ℕ] : Γ ⊩ᵛ⟨ l ⟩ ℕ / [Γ])
           ([F] : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F / ([Γ] ∙″ [ℕ]))
         → Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F ▹▹ F [ suc (var 0) ]↑ / ([Γ] ∙″ [ℕ])
sucCase₁ {F} {Γ} {l} [Γ] [ℕ] [F] =
  ▹▹ᵛ {F} {F [ suc (var 0) ]↑} (_∙″_ {A = ℕ} [Γ] [ℕ]) [F]
      (sucCase₂ {F} [Γ] [ℕ] [F])

-- Construct a valid type for the successor case of natrec.
sucCase : ∀ {F Γ l} ([Γ] : ⊩ᵛ Γ)
          ([ℕ] : Γ ⊩ᵛ⟨ l ⟩ ℕ / [Γ])
          ([F] : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F / ([Γ] ∙″ [ℕ]))
        → Γ ⊩ᵛ⟨ l ⟩ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑) / [Γ]
sucCase {F} {Γ} {l} [Γ] [ℕ] [F] =
  Πᵛ {ℕ} {F ▹▹ F [ suc (var 0) ]↑} [Γ] [ℕ]
     (sucCase₁ {F} [Γ] [ℕ] [F])

-- Construct a valid type equality for the successor case of natrec.
sucCaseCong : ∀ {F F′ Γ l} ([Γ] : ⊩ᵛ Γ)
              ([ℕ] : Γ ⊩ᵛ⟨ l ⟩ ℕ / [Γ])
              ([F] : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F / ([Γ] ∙″ [ℕ]))
              ([F′] : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F′ / ([Γ] ∙″ [ℕ]))
              ([F≡F′] : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F ≡ F′ / [Γ] ∙″ [ℕ] / [F])
        → Γ ⊩ᵛ⟨ l ⟩ Π ℕ ▹ (F  ▹▹ F  [ suc (var 0) ]↑)
                  ≡ Π ℕ ▹ (F′ ▹▹ F′ [ suc (var 0) ]↑)
                  / [Γ] / sucCase {F} [Γ] [ℕ] [F]
sucCaseCong {F} {F′} {Γ} {l} [Γ] [ℕ] [F] [F′] [F≡F′] =
  Π-congᵛ {ℕ} {F ▹▹ F [ suc (var 0) ]↑} {ℕ} {F′ ▹▹ F′ [ suc (var 0) ]↑}
          [Γ] [ℕ] (sucCase₁ {F} [Γ] [ℕ] [F]) [ℕ] (sucCase₁ {F′} [Γ] [ℕ] [F′])
          (reflᵛ {ℕ} [Γ] [ℕ])
          (▹▹-congᵛ {F} {F′} {F [ suc (var 0) ]↑} {F′ [ suc (var 0) ]↑}
             (_∙″_ {A = ℕ} [Γ] [ℕ]) [F] [F′] [F≡F′]
             (sucCase₂ {F} [Γ] [ℕ] [F]) (sucCase₂ {F′} [Γ] [ℕ] [F′])
             (subst↑SEq {ℕ} {F} {F′} {suc (var 0)} {suc (var 0)}
                        [Γ] [ℕ] [F] [F′] [F≡F′]
                        (λ {Δ} {σ} → sucCase₃ [Γ] [ℕ] {Δ} {σ})
                        (λ {Δ} {σ} → sucCase₃ [Γ] [ℕ] {Δ} {σ})
                        (λ {Δ} {σ} →
                           reflᵗᵛ {ℕ} {suc (var 0)} (_∙″_ {A = ℕ} [Γ] [ℕ])
                                  (λ {Δ} {σ} → wk1ᵛ {ℕ} {ℕ} [Γ] [ℕ] [ℕ] {Δ} {σ})
                                  (λ {Δ} {σ} → sucCase₃ [Γ] [ℕ] {Δ} {σ})
                           {Δ} {σ})))

-- Reducibility of natural recursion under a valid substitution.
natrecTerm : ∀ {F z s n Γ Δ σ l}
             ([Γ]  : ⊩ᵛ Γ)
             ([F]  : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F / _∙″_ {l = l} [Γ] (ℕᵛ [Γ]))
             ([F₀] : Γ ⊩ᵛ⟨ l ⟩ F [ zero ] / [Γ])
             ([F₊] : Γ ⊩ᵛ⟨ l ⟩ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑) / [Γ])
             ([z]  : Γ ⊩ᵛ⟨ l ⟩ z ∷ F [ zero ] / [Γ] / [F₀])
             ([s]  : Γ ⊩ᵛ⟨ l ⟩ s ∷ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
                       / [Γ] / [F₊])
             (⊢Δ   : ⊢ Δ)
             ([σ]  : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
             ([σn] : Δ ⊩⟨ l ⟩ n ∷ ℕ / ℕᵣ (idRed:*: (ℕⱼ ⊢Δ)))
           → Δ ⊩⟨ l ⟩ natrec (subst (liftSubst σ) F) (subst σ z) (subst σ s) n
               ∷ subst (liftSubst σ) F [ n ]
               / irrelevance′ (PE.sym (singleSubstComp n σ F))
                              (proj₁ ([F] ⊢Δ ([σ] , [σn])))
natrecTerm {F} {z} {s} {n} {Γ} {Δ} {σ} {l} [Γ] [F] [F₀] [F₊] [z] [s] ⊢Δ [σ]
           (ιx (ℕₜ .(suc m) d n≡n (sucᵣ {m} [m]))) =
  let [ℕ] = ℕᵛ {l = l} [Γ]
      [σℕ] = proj₁ ([ℕ] ⊢Δ [σ])
      ⊢ℕ = escape (proj₁ ([ℕ] ⊢Δ [σ]))
      ⊢F = escape (proj₁ ([F] (⊢Δ ∙ ⊢ℕ) (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ])))
      ⊢z = PE.subst (λ x → _ ⊢ _ ∷ x) (singleSubstLift F zero)
                    (escapeTerm (proj₁ ([F₀] ⊢Δ [σ])) (proj₁ ([z] ⊢Δ [σ])))
      ⊢s = PE.subst (λ x → Δ ⊢ subst σ s ∷ x) (natrecSucCase σ F)
                    (escapeTerm (proj₁ ([F₊] ⊢Δ [σ])) (proj₁ ([s] ⊢Δ [σ])))
      ⊢m = escapeTerm {l = l} [σℕ] (ιx [m])
      [σsm] = irrelevanceTerm {l = l} (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ))) [σℕ]
                              (ιx (ℕₜ (suc m) (idRedTerm:*: (sucⱼ ⊢m)) n≡n (sucᵣ [m])))
      [σn] = ℕₜ (suc m) d n≡n (sucᵣ [m])
      [σn]′ , [σn≡σsm] = redSubst*Term (redₜ d) [σℕ] [σsm]
      [σFₙ]′ = proj₁ ([F] ⊢Δ ([σ] , ιx [σn]))
      [σFₙ] = irrelevance′ (PE.sym (singleSubstComp n σ F)) [σFₙ]′
      [σFₛₘ] = irrelevance′ (PE.sym (singleSubstComp (suc m) σ F))
                            (proj₁ ([F] ⊢Δ ([σ] , [σsm])))
      [Fₙ≡Fₛₘ] = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                 (PE.sym (singleSubstComp (suc m) σ F))
                                 [σFₙ]′ [σFₙ]
                                 (proj₂ ([F] ⊢Δ ([σ] , ιx [σn])) ([σ] , [σsm])
                                        (reflSubst [Γ] ⊢Δ [σ] , [σn≡σsm]))
      [σFₘ] = irrelevance′ (PE.sym (PE.trans (substCompEq F)
                                             (substSingletonComp F)))
                           (proj₁ ([F] ⊢Δ ([σ] , ιx [m])))
      [σFₛₘ]′ = irrelevance′ (natrecIrrelevantSubst F z s m σ)
                             (proj₁ ([F] ⊢Δ ([σ] , [σsm])))
      [σF₊ₘ] = substSΠ₁ (proj₁ ([F₊] ⊢Δ [σ])) [σℕ] (ιx [m])
      natrecM = appTerm [σFₘ] [σFₛₘ]′ [σF₊ₘ]
                        (appTerm [σℕ] [σF₊ₘ]
                                 (proj₁ ([F₊] ⊢Δ [σ]))
                                 (proj₁ ([s] ⊢Δ [σ])) (ιx [m]))
                        (natrecTerm {F} {z} {s} {m} {σ = σ}
                                    [Γ] [F] [F₀] [F₊] [z] [s] ⊢Δ [σ] (ιx [m]))
      natrecM′ = irrelevanceTerm′ (PE.trans
                                    (PE.sym (natrecIrrelevantSubst F z s m σ))
                                    (PE.sym (singleSubstComp (suc m) σ F)))
                                  [σFₛₘ]′ [σFₛₘ] natrecM
      reduction = natrec-subst* ⊢F ⊢z ⊢s (redₜ d) [σℕ] [σsm]
                    (λ {t} {t′} [t] [t′] [t≡t′] →
                       PE.subst₂ (λ x y → _ ⊢ x ≡ y)
                                 (PE.sym (singleSubstComp t σ F))
                                 (PE.sym (singleSubstComp t′ σ F))
                                 (≅-eq (escapeEq (proj₁ ([F] ⊢Δ ([σ] , [t])))
                                              (proj₂ ([F] ⊢Δ ([σ] , [t]))
                                                     ([σ] , [t′])
                                                     (reflSubst [Γ] ⊢Δ [σ] ,
                                                                [t≡t′])))))
                  ⇨∷* (conv* (natrec-suc ⊢m ⊢F ⊢z ⊢s
                              ⇨ id (escapeTerm [σFₛₘ] natrecM′))
                             (sym (≅-eq (escapeEq [σFₙ] [Fₙ≡Fₛₘ]))))
  in  proj₁ (redSubst*Term reduction [σFₙ]
                           (convTerm₂ [σFₙ] [σFₛₘ] [Fₙ≡Fₛₘ] natrecM′))
natrecTerm {F} {z} {s} {n} {Γ} {Δ} {σ} {l} [Γ] [F] [F₀] [F₊] [z] [s] ⊢Δ [σ]
           (ιx (ℕₜ .zero d n≡n zeroᵣ)) =
  let [ℕ] = ℕᵛ {l = l} [Γ]
      [σℕ] = proj₁ ([ℕ] ⊢Δ [σ])
      ⊢ℕ = escape (proj₁ ([ℕ] ⊢Δ [σ]))
      [σF] = proj₁ ([F] (⊢Δ ∙ ⊢ℕ) (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ]))
      ⊢F = escape [σF]
      ⊢z = PE.subst (λ x → _ ⊢ _ ∷ x) (singleSubstLift F zero)
                    (escapeTerm (proj₁ ([F₀] ⊢Δ [σ])) (proj₁ ([z] ⊢Δ [σ])))
      ⊢s = PE.subst (λ x → Δ ⊢ subst σ s ∷ x) (natrecSucCase σ F)
                    (escapeTerm (proj₁ ([F₊] ⊢Δ [σ])) (proj₁ ([s] ⊢Δ [σ])))
      [σ0] = irrelevanceTerm {l = l} (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ))) [σℕ]
                             (ιx (ℕₜ zero (idRedTerm:*: (zeroⱼ ⊢Δ)) n≡n zeroᵣ))
      [σn]′ , [σn≡σ0] = redSubst*Term (redₜ d) (proj₁ ([ℕ] ⊢Δ [σ])) [σ0]
      [σn] = ιx (ℕₜ zero d n≡n zeroᵣ)
      [σFₙ]′ = proj₁ ([F] ⊢Δ ([σ] , [σn]))
      [σFₙ] = irrelevance′ (PE.sym (singleSubstComp n σ F)) [σFₙ]′
      [Fₙ≡F₀]′ = proj₂ ([F] ⊢Δ ([σ] , [σn])) ([σ] , [σ0])
                       (reflSubst [Γ] ⊢Δ [σ] , [σn≡σ0])
      [Fₙ≡F₀] = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                (PE.sym (substCompEq F))
                                [σFₙ]′ [σFₙ] [Fₙ≡F₀]′
      [Fₙ≡F₀]″ = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                  (PE.trans (substConcatSingleton′ F)
                                            (PE.sym (singleSubstComp zero σ F)))
                                  [σFₙ]′ [σFₙ] [Fₙ≡F₀]′
      [σz] = proj₁ ([z] ⊢Δ [σ])
      reduction = natrec-subst* ⊢F ⊢z ⊢s (redₜ d) (proj₁ ([ℕ] ⊢Δ [σ])) [σ0]
                    (λ {t} {t′} [t] [t′] [t≡t′] →
                       PE.subst₂ (λ x y → _ ⊢ x ≡ y)
                                 (PE.sym (singleSubstComp t σ F))
                                 (PE.sym (singleSubstComp t′ σ F))
                                 (≅-eq (escapeEq (proj₁ ([F] ⊢Δ ([σ] , [t])))
                                              (proj₂ ([F] ⊢Δ ([σ] , [t]))
                                                     ([σ] , [t′])
                                                     (reflSubst [Γ] ⊢Δ [σ] ,
                                                                [t≡t′])))))
                  ⇨∷* (conv* (natrec-zero ⊢F ⊢z ⊢s ⇨ id ⊢z)
                             (sym (≅-eq (escapeEq [σFₙ] [Fₙ≡F₀]″))))
  in  proj₁ (redSubst*Term reduction [σFₙ]
                           (convTerm₂ [σFₙ] (proj₁ ([F₀] ⊢Δ [σ])) [Fₙ≡F₀] [σz]))
natrecTerm {F} {z} {s} {n} {Γ} {Δ} {σ} {l} [Γ] [F] [F₀] [F₊] [z] [s] ⊢Δ [σ]
           (ιx (ℕₜ m d n≡n (ne (neNfₜ neM ⊢m m≡m)))) =
  let [ℕ] = ℕᵛ {l = l} [Γ]
      [σℕ] = proj₁ ([ℕ] ⊢Δ [σ])
      ⊢ℕ = escape (proj₁ ([ℕ] ⊢Δ [σ]))
      [σn] = ιx (ℕₜ m d n≡n (ne (neNfₜ neM ⊢m m≡m)))
      [σF] = proj₁ ([F] (⊢Δ ∙ ⊢ℕ) (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ]))
      ⊢F = escape [σF]
      ⊢F≡F = escapeEq [σF] (reflEq [σF])
      ⊢z = PE.subst (λ x → _ ⊢ _ ∷ x) (singleSubstLift F zero)
                    (escapeTerm (proj₁ ([F₀] ⊢Δ [σ])) (proj₁ ([z] ⊢Δ [σ])))
      ⊢z≡z = PE.subst (λ x → _ ⊢ _ ≅ _ ∷ x) (singleSubstLift F zero)
                      (escapeTermEq (proj₁ ([F₀] ⊢Δ [σ]))
                                        (reflEqTerm (proj₁ ([F₀] ⊢Δ [σ]))
                                                    (proj₁ ([z] ⊢Δ [σ]))))
      ⊢s = PE.subst (λ x → Δ ⊢ subst σ s ∷ x) (natrecSucCase σ F)
                    (escapeTerm (proj₁ ([F₊] ⊢Δ [σ])) (proj₁ ([s] ⊢Δ [σ])))
      ⊢s≡s = PE.subst (λ x → Δ ⊢ subst σ s ≅ subst σ s ∷ x) (natrecSucCase σ F)
                      (escapeTermEq (proj₁ ([F₊] ⊢Δ [σ]))
                                        (reflEqTerm (proj₁ ([F₊] ⊢Δ [σ]))
                                                    (proj₁ ([s] ⊢Δ [σ]))))
      [σm] = neuTerm [σℕ] neM ⊢m m≡m
      [σn]′ , [σn≡σm] = redSubst*Term (redₜ d) [σℕ] [σm]
      [σFₙ]′ = proj₁ ([F] ⊢Δ ([σ] , [σn]))
      [σFₙ] = irrelevance′ (PE.sym (singleSubstComp n σ F)) [σFₙ]′
      [σFₘ] = irrelevance′ (PE.sym (singleSubstComp m σ F))
                           (proj₁ ([F] ⊢Δ ([σ] , [σm])))
      [Fₙ≡Fₘ] = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                (PE.sym (singleSubstComp m σ F)) [σFₙ]′ [σFₙ]
                                ((proj₂ ([F] ⊢Δ ([σ] , [σn]))) ([σ] , [σm])
                                        (reflSubst [Γ] ⊢Δ [σ] , [σn≡σm]))
      natrecM = neuTerm [σFₘ] (natrecₙ neM) (natrecⱼ ⊢F ⊢z ⊢s ⊢m)
                        (~-natrec ⊢F≡F ⊢z≡z ⊢s≡s m≡m)
      reduction = natrec-subst* ⊢F ⊢z ⊢s (redₜ d) [σℕ] [σm]
                    (λ {t} {t′} [t] [t′] [t≡t′] →
                       PE.subst₂ (λ x y → _ ⊢ x ≡ y)
                                 (PE.sym (singleSubstComp t σ F))
                                 (PE.sym (singleSubstComp t′ σ F))
                                 (≅-eq (escapeEq (proj₁ ([F] ⊢Δ ([σ] , [t])))
                                              (proj₂ ([F] ⊢Δ ([σ] , [t]))
                                                     ([σ] , [t′])
                                                     (reflSubst [Γ] ⊢Δ [σ] ,
                                                                [t≡t′])))))
  in  proj₁ (redSubst*Term reduction [σFₙ]
                           (convTerm₂ [σFₙ] [σFₘ] [Fₙ≡Fₘ] natrecM))

-- Reducibility of natural recursion congurence under a valid substitution equality.
natrec-congTerm : ∀ {F F′ z z′ s s′ n m Γ Δ σ σ′ l}
                  ([Γ]      : ⊩ᵛ Γ)
                  ([F]      : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F / _∙″_ {l = l} [Γ] (ℕᵛ [Γ]))
                  ([F′]     : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F′ / _∙″_ {l = l} [Γ] (ℕᵛ [Γ]))
                  ([F≡F′]   : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F ≡ F′ / _∙″_ {l = l} [Γ] (ℕᵛ [Γ])
                                    / [F])
                  ([F₀]     : Γ ⊩ᵛ⟨ l ⟩ F [ zero ] / [Γ])
                  ([F′₀]    : Γ ⊩ᵛ⟨ l ⟩ F′ [ zero ] / [Γ])
                  ([F₀≡F′₀] : Γ ⊩ᵛ⟨ l ⟩ F [ zero ] ≡ F′ [ zero ] / [Γ] / [F₀])
                  ([F₊]     : Γ ⊩ᵛ⟨ l ⟩ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
                                / [Γ])
                  ([F′₊]    : Γ ⊩ᵛ⟨ l ⟩ Π ℕ ▹ (F′ ▹▹ F′ [ suc (var 0) ]↑)
                                / [Γ])
                  ([F₊≡F₊′] : Γ ⊩ᵛ⟨ l ⟩ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
                                ≡ Π ℕ ▹ (F′ ▹▹ F′ [ suc (var 0) ]↑)
                                / [Γ] / [F₊])
                  ([z]      : Γ ⊩ᵛ⟨ l ⟩ z ∷ F [ zero ] / [Γ] / [F₀])
                  ([z′]     : Γ ⊩ᵛ⟨ l ⟩ z′ ∷ F′ [ zero ] / [Γ] / [F′₀])
                  ([z≡z′]   : Γ ⊩ᵛ⟨ l ⟩ z ≡ z′ ∷ F [ zero ] / [Γ] / [F₀])
                  ([s]      : Γ ⊩ᵛ⟨ l ⟩ s ∷ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
                                / [Γ] / [F₊])
                  ([s′]     : Γ ⊩ᵛ⟨ l ⟩ s′
                                ∷ Π ℕ ▹ (F′ ▹▹ F′ [ suc (var 0) ]↑)
                                / [Γ] / [F′₊])
                  ([s≡s′]   : Γ ⊩ᵛ⟨ l ⟩ s ≡ s′
                                ∷ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
                                / [Γ] / [F₊])
                  (⊢Δ       : ⊢ Δ)
                  ([σ]      : Δ ⊩ˢ σ  ∷ Γ / [Γ] / ⊢Δ)
                  ([σ′]     : Δ ⊩ˢ σ′ ∷ Γ / [Γ] / ⊢Δ)
                  ([σ≡σ′]   : Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ])
                  ([σn]     : Δ ⊩⟨ l ⟩ n ∷ ℕ / ℕᵣ (idRed:*: (ℕⱼ ⊢Δ)))
                  ([σm]     : Δ ⊩⟨ l ⟩ m ∷ ℕ / ℕᵣ (idRed:*: (ℕⱼ ⊢Δ)))
                  ([σn≡σm]  : Δ ⊩⟨ l ⟩ n ≡ m ∷ ℕ / ℕᵣ (idRed:*: (ℕⱼ ⊢Δ)))
                → Δ ⊩⟨ l ⟩ natrec (subst (liftSubst σ) F)
                                  (subst σ z) (subst σ s) n
                    ≡ natrec (subst (liftSubst σ′) F′)
                             (subst σ′ z′) (subst σ′ s′) m
                    ∷ subst (liftSubst σ) F [ n ]
                    / irrelevance′ (PE.sym (singleSubstComp n σ F))
                                   (proj₁ ([F] ⊢Δ ([σ] , [σn])))
natrec-congTerm {F} {F′} {z} {z′} {s} {s′} {n} {m} {Γ} {Δ} {σ} {σ′} {l}
                [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                (ιx (ℕₜ .(suc n′) d n≡n (sucᵣ {n′} [n′])))
                (ιx (ℕₜ .(suc m′) d′ m≡m (sucᵣ {m′} [m′])))
                (ιx (ℕₜ₌ .(suc n″) .(suc m″) d₁ d₁′
                     t≡u (sucᵣ {n″} {m″} [n″≡m″]))) =
  let n″≡n′ = suc-PE-injectivity (whrDet*Term (redₜ d₁ , sucₙ) (redₜ d , sucₙ))
      m″≡m′ = suc-PE-injectivity (whrDet*Term (redₜ d₁′ , sucₙ) (redₜ d′ , sucₙ))
      [ℕ] = ℕᵛ {l = l} [Γ]
      [σℕ] = proj₁ ([ℕ] ⊢Δ [σ])
      [σ′ℕ] = proj₁ ([ℕ] ⊢Δ [σ′])
      [n′≡m′] = irrelevanceEqTerm″ n″≡n′ m″≡m′ PE.refl [σℕ] [σℕ] (ιx [n″≡m″])
      [σn] = ℕₜ (suc n′) d n≡n (sucᵣ [n′])
      [σ′m] = ℕₜ (suc m′) d′ m≡m (sucᵣ [m′])
      [σn≡σ′m] = ℕₜ₌ (suc n″) (suc m″) d₁ d₁′ t≡u (sucᵣ [n″≡m″])
      ⊢ℕ = escape [σℕ]
      ⊢F = escape (proj₁ ([F] (⊢Δ ∙ ⊢ℕ) (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ])))
      ⊢z = PE.subst (λ x → _ ⊢ _ ∷ x) (singleSubstLift F zero)
                    (escapeTerm (proj₁ ([F₀] ⊢Δ [σ])) (proj₁ ([z] ⊢Δ [σ])))
      ⊢s = PE.subst (λ x → Δ ⊢ subst σ s ∷ x) (natrecSucCase σ F)
                    (escapeTerm (proj₁ ([F₊] ⊢Δ [σ])) (proj₁ ([s] ⊢Δ [σ])))
      ⊢n′ = escapeTerm {l = l} [σℕ] (ιx [n′])
      ⊢ℕ′ = escape [σ′ℕ]
      ⊢F′ = escape (proj₁ ([F′] (⊢Δ ∙ ⊢ℕ′)
                      (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ′])))
      ⊢z′ = PE.subst (λ x → _ ⊢ _ ∷ x) (singleSubstLift F′ zero)
                     (escapeTerm (proj₁ ([F′₀] ⊢Δ [σ′]))
                                    (proj₁ ([z′] ⊢Δ [σ′])))
      ⊢s′ = PE.subst (λ x → Δ ⊢ subst σ′ s′ ∷ x) (natrecSucCase σ′ F′)
                     (escapeTerm (proj₁ ([F′₊] ⊢Δ [σ′]))
                                    (proj₁ ([s′] ⊢Δ [σ′])))
      ⊢m′ = escapeTerm {l = l} [σ′ℕ] (ιx [m′])
      [σsn′] = irrelevanceTerm {l = l} (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ))) [σℕ]
                               (ιx (ℕₜ (suc n′) (idRedTerm:*: (sucⱼ ⊢n′)) n≡n (sucᵣ [n′])))
      [σn]′ , [σn≡σsn′] = redSubst*Term (redₜ d) [σℕ] [σsn′]
      [σFₙ]′ = proj₁ ([F] ⊢Δ ([σ] , ιx [σn]))
      [σFₙ] = irrelevance′ (PE.sym (singleSubstComp n σ F)) [σFₙ]′
      [σFₛₙ′] = irrelevance′ (PE.sym (singleSubstComp (suc n′) σ F))
                             (proj₁ ([F] ⊢Δ ([σ] , [σsn′])))
      [Fₙ≡Fₛₙ′] = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                  (PE.sym (singleSubstComp (suc n′) σ F))
                                  [σFₙ]′ [σFₙ]
                                  (proj₂ ([F] ⊢Δ ([σ] , ιx [σn])) ([σ] , [σsn′])
                                         (reflSubst [Γ] ⊢Δ [σ] , [σn≡σsn′]))
      [Fₙ≡Fₛₙ′]′ = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                   (natrecIrrelevantSubst F z s n′ σ)
                                   [σFₙ]′ [σFₙ]
                                   (proj₂ ([F] ⊢Δ ([σ] , ιx [σn])) ([σ] , [σsn′])
                                          (reflSubst [Γ] ⊢Δ [σ] , [σn≡σsn′]))
      [σFₙ′] = irrelevance′ (PE.sym (PE.trans (substCompEq F)
                                              (substSingletonComp F)))
                            (proj₁ ([F] ⊢Δ ([σ] , ιx [n′])))
      [σFₛₙ′]′ = irrelevance′ (natrecIrrelevantSubst F z s n′ σ)
                              (proj₁ ([F] ⊢Δ ([σ] , [σsn′])))
      [σF₊ₙ′] = substSΠ₁ (proj₁ ([F₊] ⊢Δ [σ])) [σℕ] (ιx [n′])
      [σ′sm′] = irrelevanceTerm {l = l} (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ))) [σ′ℕ]
                                (ιx (ℕₜ (suc m′) (idRedTerm:*: (sucⱼ ⊢m′)) m≡m (sucᵣ [m′])))
      [σ′m]′ , [σ′m≡σ′sm′] = redSubst*Term (redₜ d′) [σ′ℕ] [σ′sm′]
      [σ′F′ₘ]′ = proj₁ ([F′] ⊢Δ ([σ′] , ιx [σ′m]))
      [σ′F′ₘ] = irrelevance′ (PE.sym (singleSubstComp m σ′ F′)) [σ′F′ₘ]′
      [σ′Fₘ]′ = proj₁ ([F] ⊢Δ ([σ′] , ιx [σ′m]))
      [σ′Fₘ] = irrelevance′ (PE.sym (singleSubstComp m σ′ F)) [σ′Fₘ]′
      [σ′F′ₛₘ′] = irrelevance′ (PE.sym (singleSubstComp (suc m′) σ′ F′))
                               (proj₁ ([F′] ⊢Δ ([σ′] , [σ′sm′])))
      [F′ₘ≡F′ₛₘ′] = irrelevanceEq″ (PE.sym (singleSubstComp m σ′ F′))
                                    (PE.sym (singleSubstComp (suc m′) σ′ F′))
                                    [σ′F′ₘ]′ [σ′F′ₘ]
                                    (proj₂ ([F′] ⊢Δ ([σ′] , ιx [σ′m]))
                                           ([σ′] , [σ′sm′])
                                           (reflSubst [Γ] ⊢Δ [σ′] , [σ′m≡σ′sm′]))
      [σ′Fₘ′] = irrelevance′ (PE.sym (PE.trans (substCompEq F)
                                               (substSingletonComp F)))
                             (proj₁ ([F] ⊢Δ ([σ′] , ιx [m′])))
      [σ′F′ₘ′] = irrelevance′ (PE.sym (PE.trans (substCompEq F′)
                                                (substSingletonComp F′)))
                              (proj₁ ([F′] ⊢Δ ([σ′] , ιx [m′])))
      [σ′F′ₛₘ′]′ = irrelevance′ (natrecIrrelevantSubst F′ z′ s′ m′ σ′)
                                (proj₁ ([F′] ⊢Δ ([σ′] , [σ′sm′])))
      [σ′F′₊ₘ′] = substSΠ₁ (proj₁ ([F′₊] ⊢Δ [σ′])) [σ′ℕ] (ιx [m′])
      [σFₙ′≡σ′Fₘ′] = irrelevanceEq″ (PE.sym (singleSubstComp n′ σ F))
                                     (PE.sym (singleSubstComp m′ σ′ F))
                                     (proj₁ ([F] ⊢Δ ([σ] , ιx [n′]))) [σFₙ′]
                                     (proj₂ ([F] ⊢Δ ([σ] , ιx [n′]))
                                            ([σ′] , ιx [m′]) ([σ≡σ′] , [n′≡m′]))
      [σ′Fₘ′≡σ′F′ₘ′] = irrelevanceEq″ (PE.sym (singleSubstComp m′ σ′ F))
                                       (PE.sym (singleSubstComp m′ σ′ F′))
                                       (proj₁ ([F] ⊢Δ ([σ′] , ιx [m′])))
                                       [σ′Fₘ′] ([F≡F′] ⊢Δ ([σ′] , ιx [m′]))
      [σFₙ′≡σ′F′ₘ′] = transEq [σFₙ′] [σ′Fₘ′] [σ′F′ₘ′] [σFₙ′≡σ′Fₘ′] [σ′Fₘ′≡σ′F′ₘ′]
      [σFₙ≡σ′Fₘ] = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                   (PE.sym (singleSubstComp m σ′ F))
                                   (proj₁ ([F] ⊢Δ ([σ] , ιx [σn]))) [σFₙ]
                                   (proj₂ ([F] ⊢Δ ([σ] , ιx [σn]))
                                          ([σ′] , ιx [σ′m]) ([σ≡σ′] , ιx [σn≡σ′m]))
      [σ′Fₘ≡σ′F′ₘ] = irrelevanceEq″ (PE.sym (singleSubstComp m σ′ F))
                                     (PE.sym (singleSubstComp m σ′ F′))
                                     [σ′Fₘ]′ [σ′Fₘ] ([F≡F′] ⊢Δ ([σ′] , ιx [σ′m]))
      [σFₙ≡σ′F′ₘ] = transEq [σFₙ] [σ′Fₘ] [σ′F′ₘ] [σFₙ≡σ′Fₘ] [σ′Fₘ≡σ′F′ₘ]
      natrecN = appTerm [σFₙ′] [σFₛₙ′]′ [σF₊ₙ′]
                        (appTerm [σℕ] [σF₊ₙ′] (proj₁ ([F₊] ⊢Δ [σ]))
                                 (proj₁ ([s] ⊢Δ [σ])) (ιx [n′]))
                        (natrecTerm {F} {z} {s} {n′} {σ = σ}
                                    [Γ] [F] [F₀] [F₊] [z] [s] ⊢Δ [σ] (ιx [n′]))
      natrecN′ = irrelevanceTerm′ (PE.trans (PE.sym (natrecIrrelevantSubst F z s n′ σ))
                                            (PE.sym (singleSubstComp (suc n′) σ F)))
                                  [σFₛₙ′]′ [σFₛₙ′] natrecN
      natrecM = appTerm [σ′F′ₘ′] [σ′F′ₛₘ′]′ [σ′F′₊ₘ′]
                        (appTerm [σ′ℕ] [σ′F′₊ₘ′] (proj₁ ([F′₊] ⊢Δ [σ′]))
                                 (proj₁ ([s′] ⊢Δ [σ′])) (ιx [m′]))
                        (natrecTerm {F′} {z′} {s′} {m′} {σ = σ′}
                                    [Γ] [F′] [F′₀] [F′₊] [z′] [s′] ⊢Δ [σ′] (ιx [m′]))
      natrecM′ = irrelevanceTerm′ (PE.trans (PE.sym (natrecIrrelevantSubst F′ z′ s′ m′ σ′))
                                            (PE.sym (singleSubstComp (suc m′) σ′ F′)))
                                  [σ′F′ₛₘ′]′ [σ′F′ₛₘ′] natrecM
      [σs≡σ′s] = proj₂ ([s] ⊢Δ [σ]) [σ′] [σ≡σ′]
      [σ′s≡σ′s′] = convEqTerm₂ (proj₁ ([F₊] ⊢Δ [σ])) (proj₁ ([F₊] ⊢Δ [σ′]))
                               (proj₂ ([F₊] ⊢Δ [σ]) [σ′] [σ≡σ′]) ([s≡s′] ⊢Δ [σ′])
      [σs≡σ′s′] = transEqTerm (proj₁ ([F₊] ⊢Δ [σ])) [σs≡σ′s] [σ′s≡σ′s′]
      appEq = convEqTerm₂ [σFₙ] [σFₛₙ′]′ [Fₙ≡Fₛₙ′]′
                (app-congTerm [σFₙ′] [σFₛₙ′]′ [σF₊ₙ′]
                  (app-congTerm [σℕ] [σF₊ₙ′] (proj₁ ([F₊] ⊢Δ [σ])) [σs≡σ′s′]
                                (ιx [n′]) (ιx [m′]) [n′≡m′])
                  (natrecTerm {F} {z} {s} {n′} {σ = σ}
                              [Γ] [F] [F₀] [F₊] [z] [s] ⊢Δ [σ] (ιx [n′]))
                  (convTerm₂ [σFₙ′] [σ′F′ₘ′] [σFₙ′≡σ′F′ₘ′]
                             (natrecTerm {F′} {z′} {s′} {m′} {σ = σ′}
                                         [Γ] [F′] [F′₀] [F′₊] [z′] [s′]
                                         ⊢Δ [σ′] (ιx [m′])))
                  (natrec-congTerm {F} {F′} {z} {z′} {s} {s′} {n′} {m′} {σ = σ}
                                   [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀]
                                   [F₊] [F′₊] [F₊≡F′₊] [z] [z′] [z≡z′]
                                   [s] [s′] [s≡s′]
                                   ⊢Δ [σ] [σ′] [σ≡σ′] (ιx [n′]) (ιx [m′]) [n′≡m′]))
      reduction₁ = natrec-subst* ⊢F ⊢z ⊢s (redₜ d) [σℕ] [σsn′]
                     (λ {t} {t′} [t] [t′] [t≡t′] →
                        PE.subst₂ (λ x y → _ ⊢ x ≡ y)
                                  (PE.sym (singleSubstComp t σ F))
                                  (PE.sym (singleSubstComp t′ σ F))
                                  (≅-eq (escapeEq (proj₁ ([F] ⊢Δ ([σ] , [t])))
                                               (proj₂ ([F] ⊢Δ ([σ] , [t]))
                                                      ([σ] , [t′])
                                                      (reflSubst [Γ] ⊢Δ [σ] , [t≡t′])))))
                   ⇨∷* (conv* (natrec-suc ⊢n′ ⊢F ⊢z ⊢s
                   ⇨   id (escapeTerm [σFₛₙ′] natrecN′))
                          (sym (≅-eq (escapeEq [σFₙ] [Fₙ≡Fₛₙ′]))))
      reduction₂ = natrec-subst* ⊢F′ ⊢z′ ⊢s′ (redₜ d′) [σ′ℕ] [σ′sm′]
                     (λ {t} {t′} [t] [t′] [t≡t′] →
                        PE.subst₂ (λ x y → _ ⊢ x ≡ y)
                                  (PE.sym (singleSubstComp t σ′ F′))
                                  (PE.sym (singleSubstComp t′ σ′ F′))
                                  (≅-eq (escapeEq (proj₁ ([F′] ⊢Δ ([σ′] , [t])))
                                               (proj₂ ([F′] ⊢Δ ([σ′] , [t]))
                                                      ([σ′] , [t′])
                                                      (reflSubst [Γ] ⊢Δ [σ′] , [t≡t′])))))
                   ⇨∷* (conv* (natrec-suc ⊢m′ ⊢F′ ⊢z′ ⊢s′
                   ⇨   id (escapeTerm [σ′F′ₛₘ′] natrecM′))
                          (sym (≅-eq (escapeEq [σ′F′ₘ] [F′ₘ≡F′ₛₘ′]))))
      eq₁ = proj₂ (redSubst*Term reduction₁ [σFₙ]
                                 (convTerm₂ [σFₙ] [σFₛₙ′]
                                            [Fₙ≡Fₛₙ′] natrecN′))
      eq₂ = proj₂ (redSubst*Term reduction₂ [σ′F′ₘ]
                                 (convTerm₂ [σ′F′ₘ] [σ′F′ₛₘ′]
                                            [F′ₘ≡F′ₛₘ′] natrecM′))
  in  transEqTerm [σFₙ] eq₁
                  (transEqTerm [σFₙ] appEq
                               (convEqTerm₂ [σFₙ] [σ′F′ₘ] [σFₙ≡σ′F′ₘ]
                                            (symEqTerm [σ′F′ₘ] eq₂)))
natrec-congTerm {F} {F′} {z} {z′} {s} {s′} {n} {m} {Γ} {Δ} {σ} {σ′} {l}
                [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                (ιx (ℕₜ .zero d n≡n zeroᵣ)) (ιx (ℕₜ .zero d₁ m≡m zeroᵣ))
                (ιx (ℕₜ₌ .zero .zero d₂ d′ t≡u zeroᵣ)) =
  let [ℕ] = ℕᵛ {l = l} [Γ]
      [σℕ] = proj₁ ([ℕ] ⊢Δ [σ])
      ⊢ℕ = escape (proj₁ ([ℕ] ⊢Δ [σ]))
      ⊢F = escape (proj₁ ([F] {σ = liftSubst σ} (⊢Δ ∙ ⊢ℕ)
                                 (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ])))
      ⊢z = PE.subst (λ x → _ ⊢ _ ∷ x) (singleSubstLift F zero)
                    (escapeTerm (proj₁ ([F₀] ⊢Δ [σ])) (proj₁ ([z] ⊢Δ [σ])))
      ⊢s = PE.subst (λ x → Δ ⊢ subst σ s ∷ x) (natrecSucCase σ F)
                    (escapeTerm (proj₁ ([F₊] ⊢Δ [σ])) (proj₁ ([s] ⊢Δ [σ])))
      ⊢F′ = escape (proj₁ ([F′] {σ = liftSubst σ′} (⊢Δ ∙ ⊢ℕ)
                                   (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ′])))
      ⊢z′ = PE.subst (λ x → _ ⊢ _ ∷ x) (singleSubstLift F′ zero)
                     (escapeTerm (proj₁ ([F′₀] ⊢Δ [σ′])) (proj₁ ([z′] ⊢Δ [σ′])))
      ⊢s′ = PE.subst (λ x → Δ ⊢ subst σ′ s′ ∷ x) (natrecSucCase σ′ F′)
                     (escapeTerm (proj₁ ([F′₊] ⊢Δ [σ′])) (proj₁ ([s′] ⊢Δ [σ′])))
      [σ0] = irrelevanceTerm {l = l} (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ))) (proj₁ ([ℕ] ⊢Δ [σ]))
                             (ιx (ℕₜ zero (idRedTerm:*: (zeroⱼ ⊢Δ)) n≡n zeroᵣ))
      [σ′0] = irrelevanceTerm {l = l} (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ))) (proj₁ ([ℕ] ⊢Δ [σ′]))
                              (ιx (ℕₜ zero (idRedTerm:*: (zeroⱼ ⊢Δ)) m≡m zeroᵣ))
      [σn]′ , [σn≡σ0] = redSubst*Term (redₜ d) (proj₁ ([ℕ] ⊢Δ [σ])) [σ0]
      [σ′m]′ , [σ′m≡σ′0] = redSubst*Term (redₜ d′) (proj₁ ([ℕ] ⊢Δ [σ′])) [σ′0]
      [σn] = ιx (ℕₜ zero d n≡n zeroᵣ)
      [σ′m] = ιx (ℕₜ zero d′ m≡m zeroᵣ)
      [σn≡σ′m] = ιx (ℕₜ₌ zero zero d₂ d′ t≡u zeroᵣ)
      [σn≡σ′0] = transEqTerm [σℕ] [σn≡σ′m] [σ′m≡σ′0]
      [σFₙ]′ = proj₁ ([F] ⊢Δ ([σ] , [σn]))
      [σFₙ] = irrelevance′ (PE.sym (singleSubstComp n σ F)) [σFₙ]′
      [σ′Fₘ]′ = proj₁ ([F] ⊢Δ ([σ′] , [σ′m]))
      [σ′Fₘ] = irrelevance′ (PE.sym (singleSubstComp m σ′ F)) [σ′Fₘ]′
      [σ′F′ₘ]′ = proj₁ ([F′] ⊢Δ ([σ′] , [σ′m]))
      [σ′F′ₘ] = irrelevance′ (PE.sym (singleSubstComp m σ′ F′)) [σ′F′ₘ]′
      [σFₙ≡σ′Fₘ] = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                   (PE.sym (singleSubstComp m σ′ F))
                                   [σFₙ]′ [σFₙ]
                                   (proj₂ ([F] ⊢Δ ([σ] , [σn])) ([σ′] , [σ′m])
                                          ([σ≡σ′] , [σn≡σ′m]))
      [σ′Fₘ≡σ′F′ₘ] = irrelevanceEq″ (PE.sym (singleSubstComp m σ′ F))
                                     (PE.sym (singleSubstComp m σ′ F′))
                                     [σ′Fₘ]′ [σ′Fₘ] ([F≡F′] ⊢Δ ([σ′] , [σ′m]))
      [σFₙ≡σ′F′ₘ] = transEq [σFₙ] [σ′Fₘ] [σ′F′ₘ] [σFₙ≡σ′Fₘ] [σ′Fₘ≡σ′F′ₘ]
      [Fₙ≡F₀]′ = proj₂ ([F] ⊢Δ ([σ] , [σn])) ([σ] , [σ0]) (reflSubst [Γ] ⊢Δ [σ] , [σn≡σ0])
      [Fₙ≡F₀] = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                (PE.sym (substCompEq F))
                                [σFₙ]′ [σFₙ] [Fₙ≡F₀]′
      [σFₙ≡σ′F₀]′ = proj₂ ([F] ⊢Δ ([σ] , [σn])) ([σ′] , [σ′0]) ([σ≡σ′] , [σn≡σ′0])
      [σFₙ≡σ′F₀] = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                (PE.sym (substCompEq F))
                                [σFₙ]′ [σFₙ] [σFₙ≡σ′F₀]′
      [F′ₘ≡F′₀]′ = proj₂ ([F′] ⊢Δ ([σ′] , [σ′m])) ([σ′] , [σ′0])
                         (reflSubst [Γ] ⊢Δ [σ′] , [σ′m≡σ′0])
      [F′ₘ≡F′₀] = irrelevanceEq″ (PE.sym (singleSubstComp m σ′ F′))
                                  (PE.sym (substCompEq F′))
                                  [σ′F′ₘ]′ [σ′F′ₘ] [F′ₘ≡F′₀]′
      [Fₙ≡F₀]″ = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                  (PE.trans (substConcatSingleton′ F)
                                            (PE.sym (singleSubstComp zero σ F)))
                                  [σFₙ]′ [σFₙ] [Fₙ≡F₀]′
      [F′ₘ≡F′₀]″ = irrelevanceEq″ (PE.sym (singleSubstComp m σ′ F′))
                                    (PE.trans (substConcatSingleton′ F′)
                                              (PE.sym (singleSubstComp zero σ′ F′)))
                                    [σ′F′ₘ]′ [σ′F′ₘ] [F′ₘ≡F′₀]′
      [σz] = proj₁ ([z] ⊢Δ [σ])
      [σ′z′] = proj₁ ([z′] ⊢Δ [σ′])
      [σz≡σ′z] = convEqTerm₂ [σFₙ] (proj₁ ([F₀] ⊢Δ [σ])) [Fₙ≡F₀]
                             (proj₂ ([z] ⊢Δ [σ]) [σ′] [σ≡σ′])
      [σ′z≡σ′z′] = convEqTerm₂ [σFₙ] (proj₁ ([F₀] ⊢Δ [σ′])) [σFₙ≡σ′F₀]
                               ([z≡z′] ⊢Δ [σ′])
      [σz≡σ′z′] = transEqTerm [σFₙ] [σz≡σ′z] [σ′z≡σ′z′]
      reduction₁ = natrec-subst* ⊢F ⊢z ⊢s (redₜ d) (proj₁ ([ℕ] ⊢Δ [σ])) [σ0]
                    (λ {t} {t′} [t] [t′] [t≡t′] →
                       PE.subst₂ (λ x y → _ ⊢ x ≡ y)
                                 (PE.sym (singleSubstComp t σ F))
                                 (PE.sym (singleSubstComp t′ σ F))
                                 (≅-eq (escapeEq (proj₁ ([F] ⊢Δ ([σ] , [t])))
                                              (proj₂ ([F] ⊢Δ ([σ] , [t]))
                                                     ([σ] , [t′])
                                                     (reflSubst [Γ] ⊢Δ [σ] , [t≡t′])))))
                  ⇨∷* (conv* (natrec-zero ⊢F ⊢z ⊢s ⇨ id ⊢z)
                             (sym (≅-eq (escapeEq [σFₙ] [Fₙ≡F₀]″))))
      reduction₂ = natrec-subst* ⊢F′ ⊢z′ ⊢s′ (redₜ d′) (proj₁ ([ℕ] ⊢Δ [σ′])) [σ′0]
                    (λ {t} {t′} [t] [t′] [t≡t′] →
                       PE.subst₂ (λ x y → _ ⊢ x ≡ y)
                                 (PE.sym (singleSubstComp t σ′ F′))
                                 (PE.sym (singleSubstComp t′ σ′ F′))
                                 (≅-eq (escapeEq (proj₁ ([F′] ⊢Δ ([σ′] , [t])))
                                              (proj₂ ([F′] ⊢Δ ([σ′] , [t]))
                                                     ([σ′] , [t′])
                                                     (reflSubst [Γ] ⊢Δ [σ′] , [t≡t′])))))
                  ⇨∷* (conv* (natrec-zero ⊢F′ ⊢z′ ⊢s′ ⇨ id ⊢z′)
                             (sym (≅-eq (escapeEq [σ′F′ₘ] [F′ₘ≡F′₀]″))))
      eq₁ = proj₂ (redSubst*Term reduction₁ [σFₙ]
                                 (convTerm₂ [σFₙ] (proj₁ ([F₀] ⊢Δ [σ]))
                                            [Fₙ≡F₀] [σz]))
      eq₂ = proj₂ (redSubst*Term reduction₂ [σ′F′ₘ]
                                 (convTerm₂ [σ′F′ₘ] (proj₁ ([F′₀] ⊢Δ [σ′]))
                                            [F′ₘ≡F′₀] [σ′z′]))
  in  transEqTerm [σFₙ] eq₁
                  (transEqTerm [σFₙ] [σz≡σ′z′]
                               (convEqTerm₂ [σFₙ] [σ′F′ₘ] [σFₙ≡σ′F′ₘ]
                                            (symEqTerm [σ′F′ₘ] eq₂)))
natrec-congTerm {F} {F′} {z} {z′} {s} {s′} {n} {m} {Γ} {Δ} {σ} {σ′} {l}
                [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                (ιx (ℕₜ n′ d n≡n (ne (neNfₜ neN′ ⊢n′ n≡n₁))))
                (ιx (ℕₜ m′ d′ m≡m (ne (neNfₜ neM′ ⊢m′ m≡m₁))))
                (ιx (ℕₜ₌ n″ m″ d₁ d₁′ t≡u (ne (neNfₜ₌ x₂ x₃ prop₂)))) =
  let n″≡n′ = whrDet*Term (redₜ d₁ , ne x₂) (redₜ d , ne neN′)
      m″≡m′ = whrDet*Term (redₜ d₁′ , ne x₃) (redₜ d′ , ne neM′)
      [ℕ] = ℕᵛ {l = l} [Γ]
      [σℕ] = proj₁ ([ℕ] ⊢Δ [σ])
      [σ′ℕ] = proj₁ ([ℕ] ⊢Δ [σ′])
      [σn] = ℕₜ n′ d n≡n (ne (neNfₜ neN′ ⊢n′ n≡n₁))
      [σ′m] = ℕₜ m′ d′ m≡m (ne (neNfₜ neM′ ⊢m′ m≡m₁))
      [σn≡σ′m] = ℕₜ₌ n″ m″ d₁ d₁′ t≡u (ne (neNfₜ₌ x₂ x₃ prop₂))
      ⊢ℕ = escape (proj₁ ([ℕ] ⊢Δ [σ]))
      [σF] = proj₁ ([F] (⊢Δ ∙ ⊢ℕ) (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ]))
      [σ′F] = proj₁ ([F] (⊢Δ ∙ ⊢ℕ) (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ′]))
      [σ′F′] = proj₁ ([F′] (⊢Δ ∙ ⊢ℕ) (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ′]))
      ⊢F = escape [σF]
      ⊢F≡F = escapeEq [σF] (reflEq [σF])
      ⊢z = PE.subst (λ x → _ ⊢ _ ∷ x) (singleSubstLift F zero)
                    (escapeTerm (proj₁ ([F₀] ⊢Δ [σ])) (proj₁ ([z] ⊢Δ [σ])))
      ⊢z≡z = PE.subst (λ x → _ ⊢ _ ≅ _ ∷ x) (singleSubstLift F zero)
                      (escapeTermEq (proj₁ ([F₀] ⊢Δ [σ]))
                                        (reflEqTerm (proj₁ ([F₀] ⊢Δ [σ]))
                                                    (proj₁ ([z] ⊢Δ [σ]))))
      ⊢s = PE.subst (λ x → Δ ⊢ subst σ s ∷ x) (natrecSucCase σ F)
                    (escapeTerm (proj₁ ([F₊] ⊢Δ [σ])) (proj₁ ([s] ⊢Δ [σ])))
      ⊢s≡s = PE.subst (λ x → Δ ⊢ subst σ s ≅ subst σ s ∷ x) (natrecSucCase σ F)
                      (escapeTermEq (proj₁ ([F₊] ⊢Δ [σ]))
                                        (reflEqTerm (proj₁ ([F₊] ⊢Δ [σ]))
                                                    (proj₁ ([s] ⊢Δ [σ]))))
      ⊢F′ = escape [σ′F′]
      ⊢F′≡F′ = escapeEq [σ′F′] (reflEq [σ′F′])
      ⊢z′ = PE.subst (λ x → _ ⊢ _ ∷ x) (singleSubstLift F′ zero)
                     (escapeTerm (proj₁ ([F′₀] ⊢Δ [σ′])) (proj₁ ([z′] ⊢Δ [σ′])))
      ⊢z′≡z′ = PE.subst (λ x → _ ⊢ _ ≅ _ ∷ x) (singleSubstLift F′ zero)
                        (escapeTermEq (proj₁ ([F′₀] ⊢Δ [σ′]))
                                          (reflEqTerm (proj₁ ([F′₀] ⊢Δ [σ′]))
                                                      (proj₁ ([z′] ⊢Δ [σ′]))))
      ⊢s′ = PE.subst (λ x → Δ ⊢ subst σ′ s′ ∷ x) (natrecSucCase σ′ F′)
                     (escapeTerm (proj₁ ([F′₊] ⊢Δ [σ′])) (proj₁ ([s′] ⊢Δ [σ′])))
      ⊢s′≡s′ = PE.subst (λ x → Δ ⊢ subst σ′ s′ ≅ subst σ′ s′ ∷ x) (natrecSucCase σ′ F′)
                      (escapeTermEq (proj₁ ([F′₊] ⊢Δ [σ′]))
                                        (reflEqTerm (proj₁ ([F′₊] ⊢Δ [σ′]))
                                                    (proj₁ ([s′] ⊢Δ [σ′]))))
      ⊢σF≡σ′F = escapeEq [σF] (proj₂ ([F] {σ = liftSubst σ} (⊢Δ ∙ ⊢ℕ)
                                           (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ]))
                                      {σ′ = liftSubst σ′}
                                      (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ′])
                                      (liftSubstSEq {F = ℕ} [Γ] ⊢Δ [ℕ] [σ] [σ≡σ′]))
      ⊢σz≡σ′z = PE.subst (λ x → _ ⊢ _ ≅ _ ∷ x) (singleSubstLift F zero)
                         (escapeTermEq (proj₁ ([F₀] ⊢Δ [σ]))
                                          (proj₂ ([z] ⊢Δ [σ]) [σ′] [σ≡σ′]))
      ⊢σs≡σ′s = PE.subst (λ x → Δ ⊢ subst σ s ≅ subst σ′ s ∷ x)
                         (natrecSucCase σ F)
                         (escapeTermEq (proj₁ ([F₊] ⊢Δ [σ]))
                                          (proj₂ ([s] ⊢Δ [σ]) [σ′] [σ≡σ′]))
      ⊢σ′F≡⊢σ′F′ = escapeEq [σ′F] ([F≡F′] (⊢Δ ∙ ⊢ℕ)
                               (liftSubstS {F = ℕ} [Γ] ⊢Δ [ℕ] [σ′]))
      ⊢σ′z≡⊢σ′z′ = PE.subst (λ x → _ ⊢ _ ≅ _ ∷ x)
                            (singleSubstLift F zero)
                            (≅-conv (escapeTermEq (proj₁ ([F₀] ⊢Δ [σ′]))
                                                   ([z≡z′] ⊢Δ [σ′]))
                                  (sym (≅-eq (escapeEq (proj₁ ([F₀] ⊢Δ [σ]))
                                                    (proj₂ ([F₀] ⊢Δ [σ]) [σ′] [σ≡σ′])))))
      ⊢σ′s≡⊢σ′s′ = PE.subst (λ x → Δ ⊢ subst σ′ s ≅ subst σ′ s′ ∷ x)
                            (natrecSucCase σ F)
                            (≅-conv (escapeTermEq (proj₁ ([F₊] ⊢Δ [σ′]))
                                                   ([s≡s′] ⊢Δ [σ′]))
                                  (sym (≅-eq (escapeEq (proj₁ ([F₊] ⊢Δ [σ]))
                                                    (proj₂ ([F₊] ⊢Δ [σ]) [σ′] [σ≡σ′])))))
      ⊢F≡F′ = ≅-trans ⊢σF≡σ′F ⊢σ′F≡⊢σ′F′
      ⊢z≡z′ = ≅ₜ-trans ⊢σz≡σ′z ⊢σ′z≡⊢σ′z′
      ⊢s≡s′ = ≅ₜ-trans ⊢σs≡σ′s ⊢σ′s≡⊢σ′s′
      [σn′] = neuTerm [σℕ] neN′ ⊢n′ n≡n₁
      [σn]′ , [σn≡σn′] = redSubst*Term (redₜ d) [σℕ] [σn′]
      [σFₙ]′ = proj₁ ([F] ⊢Δ ([σ] , ιx [σn]))
      [σFₙ] = irrelevance′ (PE.sym (singleSubstComp n σ F)) [σFₙ]′
      [σFₙ′] = irrelevance′ (PE.sym (singleSubstComp n′ σ F))
                            (proj₁ ([F] ⊢Δ ([σ] , [σn′])))
      [Fₙ≡Fₙ′] = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                (PE.sym (singleSubstComp n′ σ F)) [σFₙ]′ [σFₙ]
                                ((proj₂ ([F] ⊢Δ ([σ] , ιx [σn])))
                                        ([σ] , [σn′])
                                        (reflSubst [Γ] ⊢Δ [σ] , [σn≡σn′]))
      [σ′m′] = neuTerm [σ′ℕ] neM′ ⊢m′ m≡m₁
      [σ′m]′ , [σ′m≡σ′m′] = redSubst*Term (redₜ d′) [σ′ℕ] [σ′m′]
      [σ′F′ₘ]′ = proj₁ ([F′] ⊢Δ ([σ′] , ιx [σ′m]))
      [σ′F′ₘ] = irrelevance′ (PE.sym (singleSubstComp m σ′ F′)) [σ′F′ₘ]′
      [σ′Fₘ]′ = proj₁ ([F] ⊢Δ ([σ′] , ιx [σ′m]))
      [σ′Fₘ] = irrelevance′ (PE.sym (singleSubstComp m σ′ F)) [σ′Fₘ]′
      [σ′F′ₘ′] = irrelevance′ (PE.sym (singleSubstComp m′ σ′ F′))
                              (proj₁ ([F′] ⊢Δ ([σ′] , [σ′m′])))
      [F′ₘ≡F′ₘ′] = irrelevanceEq″ (PE.sym (singleSubstComp m σ′ F′))
                                   (PE.sym (singleSubstComp m′ σ′ F′))
                                   [σ′F′ₘ]′ [σ′F′ₘ]
                                   ((proj₂ ([F′] ⊢Δ ([σ′] , ιx [σ′m])))
                                           ([σ′] , [σ′m′])
                                           (reflSubst [Γ] ⊢Δ [σ′] , [σ′m≡σ′m′]))
      [σFₙ≡σ′Fₘ] = irrelevanceEq″ (PE.sym (singleSubstComp n σ F))
                                   (PE.sym (singleSubstComp m σ′ F))
                                   [σFₙ]′ [σFₙ]
                                   (proj₂ ([F] ⊢Δ ([σ] , ιx [σn])) ([σ′] , ιx [σ′m])
                                          ([σ≡σ′] , ιx [σn≡σ′m]))
      [σ′Fₘ≡σ′F′ₘ] = irrelevanceEq″ (PE.sym (singleSubstComp m σ′ F))
                                     (PE.sym (singleSubstComp m σ′ F′))
                                     (proj₁ ([F] ⊢Δ ([σ′] , ιx [σ′m])))
                                     [σ′Fₘ] ([F≡F′] ⊢Δ ([σ′] , ιx [σ′m]))
      [σFₙ≡σ′F′ₘ] = transEq [σFₙ] [σ′Fₘ] [σ′F′ₘ] [σFₙ≡σ′Fₘ] [σ′Fₘ≡σ′F′ₘ]
      [σFₙ′≡σ′Fₘ′] = transEq [σFₙ′] [σFₙ] [σ′F′ₘ′] (symEq [σFₙ] [σFₙ′] [Fₙ≡Fₙ′])
                             (transEq [σFₙ] [σ′F′ₘ] [σ′F′ₘ′] [σFₙ≡σ′F′ₘ] [F′ₘ≡F′ₘ′])
      natrecN = neuTerm [σFₙ′] (natrecₙ neN′) (natrecⱼ ⊢F ⊢z ⊢s ⊢n′)
                        (~-natrec ⊢F≡F ⊢z≡z ⊢s≡s n≡n₁)
      natrecM = neuTerm [σ′F′ₘ′] (natrecₙ neM′) (natrecⱼ ⊢F′ ⊢z′ ⊢s′ ⊢m′)
                        (~-natrec ⊢F′≡F′ ⊢z′≡z′ ⊢s′≡s′ m≡m₁)
      natrecN≡M =
        convEqTerm₂ [σFₙ] [σFₙ′] [Fₙ≡Fₙ′]
          (neuEqTerm [σFₙ′] (natrecₙ neN′) (natrecₙ neM′)
                     (natrecⱼ ⊢F ⊢z ⊢s ⊢n′)
                     (conv (natrecⱼ ⊢F′ ⊢z′ ⊢s′ ⊢m′)
                            (sym (≅-eq (escapeEq [σFₙ′] [σFₙ′≡σ′Fₘ′]))))
                     (~-natrec ⊢F≡F′ ⊢z≡z′ ⊢s≡s′
                               (PE.subst₂ (λ x y → _ ⊢ x ~ y ∷ _)
                                          n″≡n′ m″≡m′ prop₂)))
      reduction₁ = natrec-subst* ⊢F ⊢z ⊢s (redₜ d) [σℕ] [σn′]
                     (λ {t} {t′} [t] [t′] [t≡t′] →
                        PE.subst₂ (λ x y → _ ⊢ x ≡ y)
                                  (PE.sym (singleSubstComp t σ F))
                                  (PE.sym (singleSubstComp t′ σ F))
                                  (≅-eq (escapeEq (proj₁ ([F] ⊢Δ ([σ] , [t])))
                                               (proj₂ ([F] ⊢Δ ([σ] , [t]))
                                                      ([σ] , [t′])
                                                      (reflSubst [Γ] ⊢Δ [σ] , [t≡t′])))))
      reduction₂ = natrec-subst* ⊢F′ ⊢z′ ⊢s′ (redₜ d′) [σ′ℕ] [σ′m′]
                     (λ {t} {t′} [t] [t′] [t≡t′] →
                        PE.subst₂ (λ x y → _ ⊢ x ≡ y)
                                  (PE.sym (singleSubstComp t σ′ F′))
                                  (PE.sym (singleSubstComp t′ σ′ F′))
                                  (≅-eq (escapeEq (proj₁ ([F′] ⊢Δ ([σ′] , [t])))
                                               (proj₂ ([F′] ⊢Δ ([σ′] , [t]))
                                                      ([σ′] , [t′])
                                                      (reflSubst [Γ] ⊢Δ [σ′] , [t≡t′])))))
      eq₁ = proj₂ (redSubst*Term reduction₁ [σFₙ]
                                 (convTerm₂ [σFₙ] [σFₙ′] [Fₙ≡Fₙ′] natrecN))
      eq₂ = proj₂ (redSubst*Term reduction₂ [σ′F′ₘ]
                                 (convTerm₂ [σ′F′ₘ] [σ′F′ₘ′] [F′ₘ≡F′ₘ′] natrecM))
  in  transEqTerm [σFₙ] eq₁
                  (transEqTerm [σFₙ] natrecN≡M
                               (convEqTerm₂ [σFₙ] [σ′F′ₘ] [σFₙ≡σ′F′ₘ]
                                            (symEqTerm [σ′F′ₘ] eq₂)))
-- Refuting cases
natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                [σn] (ιx (ℕₜ _ d₁ _ zeroᵣ))
                (ιx (ℕₜ₌ _ _ d₂ d′ t≡u (sucᵣ prop₂))) =
  ⊥-elim (zero≢suc (whrDet*Term (redₜ d₁ , zeroₙ) (redₜ d′ , sucₙ)))
natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                [σn] (ιx (ℕₜ n d₁ _ (ne (neNfₜ neK ⊢k k≡k))))
                (ιx (ℕₜ₌ _ _ d₂ d′ t≡u (sucᵣ prop₂))) =
  ⊥-elim (suc≢ne neK (whrDet*Term (redₜ d′ , sucₙ) (redₜ d₁ , ne neK)))
natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                (ιx (ℕₜ _ d _ zeroᵣ)) [σm]
                (ιx (ℕₜ₌ _ _ d₁ d′ t≡u (sucᵣ prop₂))) =
  ⊥-elim (zero≢suc (whrDet*Term (redₜ d , zeroₙ) (redₜ d₁ , sucₙ)))
natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                (ιx (ℕₜ n d _ (ne (neNfₜ neK ⊢k k≡k)))) [σm]
                (ιx (ℕₜ₌ _ _ d₁ d′ t≡u (sucᵣ prop₂))) =
  ⊥-elim (suc≢ne neK (whrDet*Term (redₜ d₁ , sucₙ) (redₜ d , ne neK)))

natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                (ιx (ℕₜ _ d _ (sucᵣ prop))) [σm]
                (ιx (ℕₜ₌ _ _ d₂ d′ t≡u zeroᵣ)) =
  ⊥-elim (zero≢suc (whrDet*Term (redₜ d₂ , zeroₙ) (redₜ d , sucₙ)))
natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                [σn] (ιx (ℕₜ _ d₁ _ (sucᵣ prop₁)))
                (ιx (ℕₜ₌ _ _ d₂ d′ t≡u zeroᵣ)) =
  ⊥-elim (zero≢suc (whrDet*Term (redₜ d′ , zeroₙ) (redₜ d₁ , sucₙ)))
natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                [σn] (ιx (ℕₜ n d₁ _ (ne (neNfₜ neK ⊢k k≡k))))
                (ιx (ℕₜ₌ _ _ d₂ d′ t≡u zeroᵣ)) =
  ⊥-elim (zero≢ne neK (whrDet*Term (redₜ d′ , zeroₙ) (redₜ d₁ , ne neK)))
natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                (ιx (ℕₜ n d _ (ne (neNfₜ neK ⊢k k≡k)))) [σm]
                (ιx (ℕₜ₌ _ _ d₂ d′ t≡u zeroᵣ)) =
  ⊥-elim (zero≢ne neK (whrDet*Term (redₜ d₂ , zeroₙ) (redₜ d , ne neK)))

natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                (ιx (ℕₜ _ d _ (sucᵣ prop))) [σm]
                (ιx (ℕₜ₌ n₁ n′ d₂ d′ t≡u (ne (neNfₜ₌ x x₁ prop₂)))) =
  ⊥-elim (suc≢ne x (whrDet*Term (redₜ d , sucₙ) (redₜ d₂ , ne x)))
natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                (ιx (ℕₜ _ d _ zeroᵣ)) [σm]
                (ιx (ℕₜ₌ n₁ n′ d₂ d′ t≡u (ne (neNfₜ₌ x x₁ prop₂)))) =
  ⊥-elim (zero≢ne x (whrDet*Term (redₜ d , zeroₙ) (redₜ d₂ , ne x)))
natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                [σn] (ιx (ℕₜ _ d₁ _ (sucᵣ prop₁)))
                (ιx (ℕₜ₌ n₁ n′ d₂ d′ t≡u (ne (neNfₜ₌ x₁ x₂ prop₂)))) =
  ⊥-elim (suc≢ne x₂ (whrDet*Term (redₜ d₁ , sucₙ) (redₜ d′ , ne x₂)))
natrec-congTerm [Γ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
                [z] [z′] [z≡z′] [s] [s′] [s≡s′] ⊢Δ [σ] [σ′] [σ≡σ′]
                [σn] (ιx (ℕₜ _ d₁ _ zeroᵣ))
                (ιx (ℕₜ₌ n₁ n′ d₂ d′ t≡u (ne (neNfₜ₌ x₁ x₂ prop₂)))) =
  ⊥-elim (zero≢ne x₂ (whrDet*Term (redₜ d₁ , zeroₙ) (redₜ d′ , ne x₂)))

-- Validity of natural recursion.
natrecᵛ : ∀ {F z s n Γ l} ([Γ] : ⊩ᵛ Γ)
          ([ℕ]  : Γ ⊩ᵛ⟨ l ⟩ ℕ / [Γ])
          ([F]  : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F / ([Γ] ∙′ [ℕ]))
          ([F₀] : Γ ⊩ᵛ⟨ l ⟩ F [ zero ] / [Γ])
          ([F₊] : Γ ⊩ᵛ⟨ l ⟩ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑) / [Γ])
          ([Fₙ] : Γ ⊩ᵛ⟨ l ⟩ F [ n ] / [Γ])
        → Γ ⊩ᵛ⟨ l ⟩ z ∷ F [ zero ] / [Γ] / [F₀]
        → Γ ⊩ᵛ⟨ l ⟩ s ∷ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑) / [Γ] / [F₊]
        → ([n] : Γ ⊩ᵛ⟨ l ⟩ n ∷ ℕ / [Γ] / [ℕ])
        → Γ ⊩ᵛ⟨ l ⟩ natrec F z s n ∷ F [ n ] / [Γ] / [Fₙ]
natrecᵛ {F} {z} {s} {n} {l = l} [Γ] [ℕ] [F] [F₀] [F₊] [Fₙ] [z] [s] [n]
        {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [F]′ = S.irrelevance {A = F} (_∙″_ {A = ℕ} [Γ] [ℕ])
                           (_∙″_ {l = l} [Γ] (ℕᵛ [Γ])) [F]
      [σn]′ = irrelevanceTerm {l′ = l} (proj₁ ([ℕ] ⊢Δ [σ]))
                              (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ))) (proj₁ ([n] ⊢Δ [σ]))
      n′ = subst σ n
      eqPrf = PE.trans (singleSubstComp n′ σ F)
                       (PE.sym (PE.trans (substCompEq F)
                               (substConcatSingleton′ F)))
  in  irrelevanceTerm′ eqPrf (irrelevance′ (PE.sym (singleSubstComp n′ σ F))
                                           (proj₁ ([F]′ ⊢Δ ([σ] , [σn]′))))
                        (proj₁ ([Fₙ] ⊢Δ [σ]))
                   (natrecTerm {F} {z} {s} {n′} {σ = σ} [Γ]
                               [F]′
                               [F₀] [F₊] [z] [s] ⊢Δ [σ]
                               [σn]′)
 ,   (λ {σ′} [σ′] [σ≡σ′] →
        let [σ′n]′ = irrelevanceTerm {l′ = l} (proj₁ ([ℕ] ⊢Δ [σ′]))
                                     (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ)))
                                     (proj₁ ([n] ⊢Δ [σ′]))
            [σn≡σ′n] = irrelevanceEqTerm {l′ = l} (proj₁ ([ℕ] ⊢Δ [σ]))
                                         (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ)))
                                         (proj₂ ([n] ⊢Δ [σ]) [σ′] [σ≡σ′])
        in  irrelevanceEqTerm′ eqPrf
              (irrelevance′ (PE.sym (singleSubstComp n′ σ F))
                            (proj₁ ([F]′ ⊢Δ ([σ] , [σn]′))))
              (proj₁ ([Fₙ] ⊢Δ [σ]))
              (natrec-congTerm {F} {F} {z} {z} {s} {s} {n′} {subst σ′ n} {σ = σ}
                               [Γ] [F]′ [F]′ (reflᵛ {F} (_∙″_ {A = ℕ} {l = l}
                               [Γ] (ℕᵛ [Γ])) [F]′) [F₀] [F₀]
                               (reflᵛ {F [ zero ]} [Γ] [F₀]) [F₊] [F₊]
                               (reflᵛ {Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)}
                                      [Γ] [F₊])
                               [z] [z] (reflᵗᵛ {F [ zero ]} {z} [Γ] [F₀] [z])
                               [s] [s]
                               (reflᵗᵛ {Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)} {s}
                                       [Γ] [F₊] [s])
                               ⊢Δ [σ] [σ′] [σ≡σ′] [σn]′ [σ′n]′ [σn≡σ′n]))

-- Validity of natural recursion congurence.
natrec-congᵛ : ∀ {F F′ z z′ s s′ n n′ Γ l} ([Γ] : ⊩ᵛ Γ)
          ([ℕ]  : Γ ⊩ᵛ⟨ l ⟩ ℕ / [Γ])
          ([F]  : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F / ([Γ] ∙″ [ℕ]))
          ([F′]  : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F′ / ([Γ] ∙″ [ℕ]))
          ([F≡F′]  : Γ ∙ ℕ ⊩ᵛ⟨ l ⟩ F ≡ F′ / [Γ] ∙″ [ℕ] / [F])
          ([F₀] : Γ ⊩ᵛ⟨ l ⟩ F [ zero ] / [Γ])
          ([F′₀] : Γ ⊩ᵛ⟨ l ⟩ F′ [ zero ] / [Γ])
          ([F₀≡F′₀] : Γ ⊩ᵛ⟨ l ⟩ F [ zero ] ≡ F′ [ zero ] / [Γ] / [F₀])
          ([F₊] : Γ ⊩ᵛ⟨ l ⟩ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑) / [Γ])
          ([F′₊] : Γ ⊩ᵛ⟨ l ⟩ Π ℕ ▹ (F′ ▹▹ F′ [ suc (var 0) ]↑) / [Γ])
          ([F₊≡F′₊] : Γ ⊩ᵛ⟨ l ⟩ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
                              ≡ Π ℕ ▹ (F′ ▹▹ F′ [ suc (var 0) ]↑) / [Γ]
                              / [F₊])
          ([Fₙ] : Γ ⊩ᵛ⟨ l ⟩ F [ n ] / [Γ])
          ([z] : Γ ⊩ᵛ⟨ l ⟩ z ∷ F [ zero ] / [Γ] / [F₀])
          ([z′] : Γ ⊩ᵛ⟨ l ⟩ z′ ∷ F′ [ zero ] / [Γ] / [F′₀])
          ([z≡z′] : Γ ⊩ᵛ⟨ l ⟩ z ≡ z′ ∷ F [ zero ] / [Γ] / [F₀])
          ([s] : Γ ⊩ᵛ⟨ l ⟩ s ∷ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑) / [Γ] / [F₊])
          ([s′] : Γ ⊩ᵛ⟨ l ⟩ s′ ∷ Π ℕ ▹ (F′ ▹▹ F′ [ suc (var 0) ]↑) / [Γ]
                           / [F′₊])
          ([s≡s′] : Γ ⊩ᵛ⟨ l ⟩ s ≡ s′ ∷ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
                             / [Γ] / [F₊])
          ([n] : Γ ⊩ᵛ⟨ l ⟩ n ∷ ℕ / [Γ] / [ℕ])
          ([n′] : Γ ⊩ᵛ⟨ l ⟩ n′ ∷ ℕ / [Γ] / [ℕ])
          ([n≡n′] : Γ ⊩ᵛ⟨ l ⟩ n ≡ n′ ∷ ℕ / [Γ] / [ℕ])
        → Γ ⊩ᵛ⟨ l ⟩ natrec F z s n ≡ natrec F′ z′ s′ n′ ∷ F [ n ] / [Γ] / [Fₙ]
natrec-congᵛ {F} {F′} {z} {z′} {s} {s′} {n} {n′} {l = l}
             [Γ] [ℕ] [F] [F′] [F≡F′] [F₀] [F′₀] [F₀≡F′₀] [F₊] [F′₊] [F₊≡F′₊]
             [Fₙ] [z] [z′] [z≡z′] [s] [s′] [s≡s′] [n] [n′]
             [n≡n′] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [F]′ = S.irrelevance {A = F} (_∙″_ {A = ℕ} [Γ] [ℕ])
                           (_∙″_ {l = l} [Γ] (ℕᵛ [Γ])) [F]
      [F′]′ = S.irrelevance {A = F′} (_∙″_ {A = ℕ} [Γ] [ℕ])
                            (_∙″_ {l = l} [Γ] (ℕᵛ [Γ])) [F′]
      [F≡F′]′ = S.irrelevanceEq {A = F} {B = F′} (_∙″_ {A = ℕ} [Γ] [ℕ])
                                (_∙″_ {l = l} [Γ] (ℕᵛ [Γ])) [F] [F]′ [F≡F′]
      [σn]′ = irrelevanceTerm {l′ = l} (proj₁ ([ℕ] ⊢Δ [σ]))
                              (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ))) (proj₁ ([n] ⊢Δ [σ]))
      [σn′]′ = irrelevanceTerm {l′ = l} (proj₁ ([ℕ] ⊢Δ [σ]))
                               (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ))) (proj₁ ([n′] ⊢Δ [σ]))
      [σn≡σn′]′ = irrelevanceEqTerm {l′ = l} (proj₁ ([ℕ] ⊢Δ [σ]))
                                    (ℕᵣ (idRed:*: (ℕⱼ ⊢Δ))) ([n≡n′] ⊢Δ [σ])
      [Fₙ]′ = irrelevance′ (PE.sym (singleSubstComp (subst σ n) σ F))
                           (proj₁ ([F]′ ⊢Δ ([σ] , [σn]′)))
  in  irrelevanceEqTerm′ (PE.sym (singleSubstLift F n))
                         [Fₙ]′ (proj₁ ([Fₙ] ⊢Δ [σ]))
                         (natrec-congTerm {F} {F′} {z} {z′} {s} {s′}
                                          {subst σ n} {subst σ n′}
                                          [Γ] [F]′ [F′]′ [F≡F′]′
                                          [F₀] [F′₀] [F₀≡F′₀]
                                          [F₊] [F′₊] [F₊≡F′₊]
                                          [z] [z′] [z≡z′]
                                          [s] [s′] [s≡s′] ⊢Δ
                                          [σ] [σ] (reflSubst [Γ] ⊢Δ [σ])
                                          [σn]′ [σn′]′ [σn≡σn′]′)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module Element where

open import OscarPrelude

record Element : Set
 where
  constructor ⟨_⟩
  field
    element : Nat

open Element public

instance EqElement : Eq Element
Eq._==_ EqElement ⟨ ε₁ ⟩ ⟨ ε₂ ⟩ with ε₁ ≟ ε₂
Eq._==_ EqElement ⟨ _ ⟩  ⟨ _ ⟩ | yes refl = yes refl
Eq._==_ EqElement ⟨ _ ⟩  ⟨ _ ⟩ | no ε₁≢ε₂ = no λ {refl → ε₁≢ε₂ refl}

ext: agda


text:
{-# OPTIONS --type-in-type #-}
module Selective.Theorems where

open import Prelude.Equality
open import Selective

-- Now let's typecheck some theorems

cong-handle : ∀ {A B}  {F : Set → Set} {{_ : Selective F}}
              {x y : F (Either A B)} {f : F (A → B)} →
              x ≡ y → handle x f ≡ handle y f
cong-handle refl = {!!}

cong-handle-handler : ∀ {A B}  {F : Set → Set} {{_ : Selective F}}
                      {x : F (Either A B)} {f g : F (A → B)} →
                      f ≡ g → handle x f ≡ handle x g
cong-handle-handler refl = {!!}

cong-ap-right : ∀ {A B} {F : Set → Set} {{_ : Applicative F}}
                {x y : F A} {f : F (A → B)} →
                x ≡ y → f <*> x ≡ f <*> y
cong-ap-right refl = refl

-- lemma : ∀ {A B} {F : Set → Set} {{_ : Applicative F}}
--         {x : F A} {f : A → B} →
--         pure (_$_) <*> pure f <*> x ≡ (pure f) <*> x
-- lemma = refl

-- Identity: pure id <*> v = v
t1 : ∀ {A : Set} {F : Set → Set} {{_ : Selective F}} →
     (v : F A) → (apS (pure id) v) ≡ v
t1 v = apS (pure id) v
         ≡⟨ refl ⟩                           -- Definition of 'apS'
       handle (left <$> pure id) (flip (_$_) <$> v)
         ≡⟨ cong-handle fmap-pure-ap ⟩
       handle (pure left <*> pure id) (flip (_$_) <$> v)
         ≡⟨  cong-handle ap-homomorphism ⟩   -- Push 'left' inside 'pure'
       handle (pure (left id)) (flip (_$_) <$> v)
         ≡⟨ p2 ⟩                             -- Apply P2
       (_$ id) <$> (flip (_$_) <$> v)
         ≡⟨ refl ⟩                      let f = (_$ id)
                                            g = flip (_$_) in
       f <$> (g <$> v)
         ≡⟨ fmap-pure-ap ⟩
       pure f <*> (g <$> v)
         ≡⟨ cong-ap-right fmap-pure-ap ⟩
       pure f <*> (pure g <*> v)
          ≡⟨ refl ⟩
       pure (_$ id) <*> (pure g <*> v)
          ≡⟨ {!?!} ⟩ -- ap-interchange
       (pure g <*> v) <*> pure id
          ≡⟨ refl ⟩
       pure (λ x f -> f x) <*> v <*> pure id
          ≡⟨ {!!} ⟩
       -- (f <$> g) <$> v
       --   ≡⟨ refl ⟩
       -- (f ∘ g) <$> v
       --   ≡⟨ refl ⟩
       -- ((_$ id) ∘ flip (_$_)) <$> v
       --   ≡⟨ refl ⟩                           -- Simplify
       pure id <*> v
         ≡⟨ fmap-pure-ap ⟩
       id <$> v
         ≡⟨ fmap-id ⟩                        -- Functor identity: fmap id = id
       v ∎

t1' : ∀ {A : Set} {F : Set → Set} {{_ : Selective F}} →
     (v : F A) → (apS (pure id) v) ≡ v
t1' v = apS (pure id) v
         ≡⟨ refl ⟩                           -- Definition of 'apS'
       handle (left <$> pure id) (flip (_$_) <$> v)
         ≡⟨ cong-handle fmap-pure-ap ⟩
       handle (pure left <*> pure id) (flip (_$_) <$> v)
         ≡⟨  cong-handle ap-homomorphism ⟩   -- Push 'left' inside 'pure'
       handle (pure (left id)) (flip (_$_) <$> v)
         ≡⟨ p2 ⟩                             -- Apply P2
       (_$ id) <$> (flip (_$_) <$> v)
         ≡⟨ refl ⟩
                                        let f = (_$ id)
                                            g = flip (_$_) in
       f <$> (g <$> v)
          ≡⟨ {!!} ⟩
       (f ∘ g) <$> v
         ≡⟨ refl ⟩
       ((_$ id) ∘ flip (_$_)) <$> v
         ≡⟨ refl ⟩                           -- Simplify
       id <$> v
         ≡⟨ fmap-id ⟩                        -- Functor identity: fmap id = id
       v ∎

-- Homomorphism: pure f <*> pure x = pure (f x)
t2 : ∀ {A B : Set} {F : Set → Set} {{_ : Selective F}}
     (f : A → B) (x : A) →
     (apS (pure {F} f) (pure x)) ≡ pure (f x)
t2 f x = apS (pure f) (pure x)
            ≡⟨ refl ⟩ -- Definition of 'apS'
         handle (left <$> pure f) (flip (_$_) <$> pure x)
           ≡⟨ cong-handle fmap-pure-ap ⟩  -- Push 'Left' inside 'pure'
         handle (pure left <*> pure f) (flip (_$_) <$> pure x)
           ≡⟨ cong-handle ap-homomorphism ⟩
         handle (pure (left f)) (flip (_$_) <$> pure x)
           ≡⟨ p2 ⟩    -- Apply P2
         (_$ f) <$> (flip (_$_) <$> pure x)
           ≡⟨ {!?!} ⟩ -- Simplify
         f <$> pure x
           ≡⟨ fmap-pure-ap ⟩
         pure f <*> pure x
           ≡⟨ ap-homomorphism ⟩
         pure (f x) ∎

-- Interchange: u <*> pure y = pure ($y) <*> u
t3 : ∀ {A B : Set} {F : Set → Set} {{_ : Selective F}}
     (f : F (A → B)) (x : A) →
      apS f (pure x) ≡ apS (pure (_$ x)) f
t3 f x = {!!}

    -- === -- Express right-hand side of the theorem using 'apS'
    -- apS (pure ($y)) u
    -- === -- Definition of 'apS'
    -- handle (Left <$> pure ($y)) (flip ($) <$> u)
    -- === -- Push 'Left' inside 'pure'
    -- handle (pure (Left ($y))) (flip ($) <$> u)
    -- === -- Apply P2
    -- ($($y)) <$> (flip ($) <$> u)
    -- === -- Simplify, obtaining (#)
    -- ($y) <$> u

either-left-lemma : ∀ {A B C : Set} {x : A} {f : A → C} {g : B → C} →
  either f g (left x) ≡ f x
either-left-lemma = refl

either-left-lemma1 : ∀ {A B C : Set}
   {F : Set → Set} {{_ : Functor F}} →
   {x : F A} {f : A → C} {g : B → C} →
  (either f g <$> (fmap {F = F} left x)) ≡ (f <$> x)
either-left-lemma1 = {!!}

t3-lhs-lemma : ∀ {A B : Set} {F : Set → Set} {{_ : Selective F}}
               (f : F (A → B)) (x : A) →
               apS f (pure x) ≡ ((_$ x) <$> f)
t3-lhs-lemma {A} {B} f x =
  apS f (pure x)
    ≡⟨ refl ⟩ -- Definition of 'apS'
  handle (left <$> f) (flip (_$_) <$> pure x)
    ≡⟨ cong-handle-handler fmap-pure-ap ⟩ -- Rewrite to have a pure handler
  handle (left <$> f) (pure (flip (_$_)) <*> pure x)
    ≡⟨ cong-handle-handler ap-homomorphism ⟩
  handle (left <$> f) (pure (flip (_$_) x))
    ≡⟨ cong-handle-handler refl ⟩
  handle (left <$> f) (pure (_$ x))
    ≡⟨ p1 ⟩   -- Apply P1
  either (_$ x) id <$> (left <$> f)
    ≡⟨ {!!} ⟩
  (_$ x) <$> f ∎
    -- -- Express the lefthand side using 'apS'
    -- apS u (pure y)
    -- === -- Definition of 'apS'
    -- handle (Left <$> u) (flip ($) <$> pure y)
    -- === -- Rewrite to have a pure handler
    -- handle (Left <$> u) (pure ($y))
    -- === -- Apply P1
    -- either ($y) id <$> (Left <$> u)
    -- === -- Simplify, obtaining (#)
    -- ($y) <$> u

max_stars_repo_name: tuura/selective-theory-agda

max_issues_repo_name: tuura/selective-theory-agda

max_forks_repo_name: tuura/selective-theory-agda


text:
open import Prelude hiding (_≤_)
open import Data.Nat.Properties
open import Induction.Nat

module Implicits.Resolution.GenericFinite.Examples.Haskell
  where

open import Implicits.Resolution.GenericFinite.TerminationCondition
open import Implicits.Resolution.GenericFinite.Resolution
open import Implicits.Resolution.GenericFinite.Algorithm
open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Implicits.Resolution.Termination
open import Implicits.Substitutions

haskellCondition : TerminationCondition
haskellCondition = record
  { TCtx = ∃ Type
  ; _<_  = _hρ<_
  ; _<?_  = λ { (_ , x) (_ , y) → x hρ<? y }
  ; step = λ Φ Δ a b τ → , a
  ; wf-< = hρ<-well-founded
  }

open ResolutionRules haskellCondition public
open ResolutionAlgorithm haskellCondition public

module Deterministic⊆HaskellFinite where
  open import Implicits.Resolution.Deterministic.Resolution as D
  open import Data.Nat hiding (_<_)
  open import Data.Nat.Properties
  open import Relation.Binary using (module DecTotalOrder)
  open import Extensions.ListFirst
  open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)
  module F = ResolutionRules haskellCondition
  module M = MetaTypeMetaSubst

  lem₆ : ∀ {ν μ} (a : Type ν) (b : Type (suc μ)) c → (, a) hρ< (, b) → (, a) hρ< (, b tp[/tp c ])
  lem₆ a b c p = ≤-trans p (h||a/s|| b (TypeSubst.sub c))
    where open SubstSizeLemmas

  lem₅ : ∀ {ν μ} {Δ : ICtx ν} {b τ} (a : Type μ) → Δ ⊢ b ↓ τ → (, a) hρ< (, b) → (, a) hρ< (, simpl τ)
  lem₅ {τ = τ} a (i-simp .τ) q = q
  lem₅ a (i-iabs _ p) q = lem₅ a p q
  lem₅ a (i-tabs {ρ = b} c p) q = lem₅ a p (lem₆ a b c q)

  -- Oliveira's termination condition is part of the well-formdness of types
  -- So we assume here that ⊢term x holds for all types x
  mutual
    lem : ∀ {ν} {Δ : ICtx ν} {a r g} →
          (∀ {ν} (a : Type ν) → ⊢term a) →
          (, simpl a) hρ≤ g → Δ D.⊢ r ↓ a → Δ F., g ⊢ r ↓ a
    lem all-⊢term q (i-simp a) = i-simp a
    lem {a = a} {g = g}all-⊢term q (i-iabs {ρ₁ = ρ₁} {ρ₂ = ρ₂} ⊢ρ₁ ρ₂↓a) with all-⊢term (ρ₁ ⇒ ρ₂)
    lem {a = a} {g = g} all-⊢term q (i-iabs {ρ₁ = ρ₁} {ρ₂ = ρ₂} ⊢ρ₁ ρ₂↓a) | term-iabs _ _ a-hρ<-b _ =
      i-iabs ρ₁<g (complete' (, ρ₁) all-⊢term ⊢ρ₁ ≤-refl) (lem all-⊢term q ρ₂↓a)
      where
        ρ₁<g : (, ρ₁) hρ< g
        ρ₁<g = ≤-trans (lem₅ ρ₁ ρ₂↓a a-hρ<-b) q
    lem all-⊢term q (i-tabs b p) = i-tabs b (lem all-⊢term q p)

    complete' : ∀ {ν} {a : Type ν} {Δ : ICtx ν} → (g : ∃ Type) →
              (∀ {ν} (a : Type ν) → ⊢term a) → Δ D.⊢ᵣ a → (, a) hρ≤ g →
              Δ F., g ⊢ᵣ a
    complete' g all-⊢term (r-simp x p) q = r-simp (proj₁ $ first⟶∈ x) (lem all-⊢term q p)
    complete' g all-⊢term (r-iabs ρ₁ p) q = r-iabs ρ₁ (complete' g all-⊢term p q)
    complete' g all-⊢term (r-tabs p) q = r-tabs (complete' g all-⊢term p q)

  complete : ∀ {ν} {a : Type ν} {Δ : ICtx ν} →
            (∀ {ν} (a : Type ν) → ⊢term a) → Δ D.⊢ᵣ a → Δ F., (, a) ⊢ᵣ a
  complete all-⊢term p = complete' _ all-⊢term p ≤-refl


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

open import LogicalFormulae
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Groups.Definition

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

open import Groups.Subgroups.Definition G
open import Groups.Lemmas G

open Group G
open Setoid S
open Equivalence eq

trivialSubgroupPred : A → Set b
trivialSubgroupPred a = (a ∼ 0G)

trivialSubgroup : Subgroup trivialSubgroupPred
Subgroup.isSubset trivialSubgroup x=y x=0 = transitive (symmetric x=y) x=0
Subgroup.closedUnderPlus trivialSubgroup x=0 y=0 = transitive (+WellDefined x=0 y=0) identLeft
Subgroup.containsIdentity trivialSubgroup = reflexive
Subgroup.closedUnderInverse trivialSubgroup x=0 = transitive (inverseWellDefined x=0) invIdent

improperSubgroupPred : A → Set
improperSubgroupPred a = True

improperSubgroup : Subgroup improperSubgroupPred
Subgroup.isSubset improperSubgroup _ _ = record {}
Subgroup.closedUnderPlus improperSubgroup _ _ = record {}
Subgroup.containsIdentity improperSubgroup = record {}
Subgroup.closedUnderInverse improperSubgroup _ = record {}


text:
module nat where

data N : Set where
  zero : N
  suc  : N -> N

_+_ : N -> N -> N
n + zero = n
n + (suc m) = suc (n + m)

_*_ : N -> N -> N
n * zero = zero
n * (suc m) = (m * n) + m

max_stars_repo_name: uedatakumi/nat

max_issues_repo_name: uedatakumi/nat

max_forks_repo_name: uedatakumi/nat


text:
module _ where

module N (_ : Set₁) where

  data D : Set₁ where
    c : Set → D

open N Set using (D) renaming (module D to MD)

open import Common.Equality

-- No longer two ways to qualify
twoWaysToQualify : D.c ≡ MD.c
twoWaysToQualify = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Cubical.Data.Strict2Group.Explicit.Notation where

open import Cubical.Foundations.Prelude hiding (comp)
open import Cubical.Data.Group.Base

module S2GBaseNotation {ℓ : Level} (C₀ C₁ : Group ℓ) (s t : morph C₁ C₀) (i : morph C₀ C₁) (∘ : (g f : Group.type C₁) → (s .fst) g ≡ (t .fst f) → Group.type C₁) where

  -- group operations of the object group
  TC₀ = Group.type C₀
  1₀ = isGroup.id (Group.groupStruc C₀)
  _∙₀_ = isGroup.comp (Group.groupStruc C₀)
  C₀⁻¹ = isGroup.inv (Group.groupStruc C₀)
  rUnit₀ = isGroup.rUnit (Group.groupStruc C₀)
  lUnit₀ = isGroup.lUnit (Group.groupStruc C₀)
  assoc₀ = isGroup.assoc (Group.groupStruc C₀)
  lCancel₀ = isGroup.lCancel (Group.groupStruc C₀)
  rCancel₀ = isGroup.lCancel (Group.groupStruc C₀)

  -- group operation of the morphism group
  TC₁ = Group.type C₁
  1₁ = isGroup.id (Group.groupStruc C₁)
  C₁⁻¹ = isGroup.inv (Group.groupStruc C₁)
  _∙₁_ = isGroup.comp (Group.groupStruc C₁)
  rUnit₁ = isGroup.rUnit (Group.groupStruc C₁)
  lUnit₁ = isGroup.lUnit (Group.groupStruc C₁)
  assoc₁ = isGroup.assoc (Group.groupStruc C₁)
  lCancel₁ = isGroup.lCancel (Group.groupStruc C₁)
  rCancel₁ = isGroup.lCancel (Group.groupStruc C₁)

  -- interface for source, target and identity map
  src = fst s
  src∙₁ = snd s
  tar = fst t
  tar∙₁ = snd t
  id = fst i
  id∙₀ = snd i

  ∙c : {g f g' f' : Group.type C₁} → (coh1 : s .fst g ≡ t .fst f) → (coh2 : s .fst g' ≡ t .fst f') → s .fst (g ∙₁ g') ≡ t .fst (f ∙₁ f')
  ∙c {g} {f} {g'} {f'} coh1 coh2 = (s .snd g g') ∙ ((cong (_∙₀ (s .fst g')) coh1) ∙ (cong ((t .fst f) ∙₀_) coh2) ∙ (sym (t .snd f f')))

  -- for two morphisms the condition for them to be composable
  CohCond : (g f : TC₁) → Type ℓ
  CohCond g f = src g ≡ tar f

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------
-- Application of substitutions
------------------------------------------------------------------------

-- Given an operation which applies a substitution to a term, subject
-- to some conditions, more operations and lemmas are defined/proved.

-- (This module reexports various other modules.)

open import Data.Universe.Indexed

module deBruijn.Substitution.Data.Application
  {i u e} {Uni : IndexedUniverse i u e} where

import deBruijn.Substitution.Data.Application.Application
open deBruijn.Substitution.Data.Application.Application
  {_} {_} {_} {Uni} public
import deBruijn.Substitution.Data.Application.Application21
open deBruijn.Substitution.Data.Application.Application21
  {_} {_} {_} {Uni} public
import deBruijn.Substitution.Data.Application.Application22
open deBruijn.Substitution.Data.Application.Application22
  {_} {_} {_} {Uni} public
import deBruijn.Substitution.Data.Application.Application1
open deBruijn.Substitution.Data.Application.Application1
  {_} {_} {_} {Uni} public

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
----------------------------------------------------------------------------
-- Well-founded induction on the natural numbers
----------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.Induction.NonAcc.WF-I where

open import FOTC.Base

open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesI
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- Well-founded induction
postulate
  <-wfind₁ : (A : D → Set) →
             (∀ {n} → N n → (∀ {m} → N m → m < n → A m) → A n) →
             ∀ {n} → N n → A n

postulate PN : ∀ {n m} → N n → m < n → N m

-- Well-founded induction removing N m from the second line.
<-wfind₂ : (A : D → Set) →
           (∀ {n} → N n → (∀ {m} → m < n → A m) → A n) →
           ∀ {n} → N n → A n
<-wfind₂ A h = <-wfind₁ A (λ Nn' h' → h Nn' (λ p → h' (PN Nn' p) p))

-- Well-founded induction removing N n from the second line.
<-wfind₃ : (A : D → Set) →
           (∀ {n} → (∀ {m} → N m → m < n → A m) → A n) →
           ∀ {n} → N n → A n
<-wfind₃ A h = <-wfind₁ A (λ Nn' h' → h h')

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Property that elements are grouped
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Grouped where

open import Data.List using (List; []; _∷_; map)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_; all)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_)
open import Relation.Binary as B using (REL; Rel)
open import Relation.Unary as U using (Pred)
open import Relation.Nullary using (¬_; yes)
open import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Sum using (_⊎-dec_)
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Nullary.Negation using (¬?)
open import Level using (_⊔_)

infixr 5 _∷≉_ _∷≈_

data Grouped {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) : Pred (List A) (a ⊔ ℓ) where
  [] : Grouped _≈_ []
  _∷≉_ : ∀ {x xs} → All (λ y → ¬ (x ≈ y)) xs → Grouped _≈_ xs → Grouped _≈_ (x ∷ xs)
  _∷≈_ : ∀ {x y xs} → x ≈ y → Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs)

module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
  grouped? : B.Decidable _≈_ → U.Decidable (Grouped _≈_)
  grouped? _≟_ [] = yes []
  grouped? _≟_ (x ∷ []) = yes ([] ∷≉ [])
  grouped? _≟_ (x ∷ y ∷ xs) = map′ from to ((x ≟ y ⊎-dec all (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs))) where
    from : ((x ≈ y) ⊎ All (λ z → ¬ (x ≈ z)) (y ∷ xs)) × Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs)
    from (inj₁ x≈y          , grouped[y∷xs]) = x≈y          ∷≈ grouped[y∷xs]
    from (inj₂ all[x≉,y∷xs] , grouped[y∷xs]) = all[x≉,y∷xs] ∷≉ grouped[y∷xs]
    to : Grouped _≈_ (x ∷ y ∷ xs) → ((x ≈ y) ⊎ All (λ z → ¬ (x ≈ z)) (y ∷ xs)) × Grouped _≈_ (y ∷ xs)
    to (all[x≉,y∷xs] ∷≉ grouped[y∷xs]) = inj₂ all[x≉,y∷xs] , grouped[y∷xs]
    to (x≈y          ∷≈ grouped[y∷xs]) = inj₁ x≈y , grouped[y∷xs]


text:
-- Convert between `X` and `X-Bool`

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

module Constructive.Axiom.Properties.Bool where

-- agda-stdlib
open import Level renaming (suc to lsuc; zero to lzero)
open import Data.Empty
open import Data.Unit using (⊤; tt)
open import Data.Bool using (Bool; true; false; not)
open import Data.Sum as Sum
open import Data.Product as Prod
open import Function.Base
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; refl; subst; sym; cong)

-- agda-misc
open import Constructive.Axiom
open import Constructive.Combinators
open import Constructive.Common

private
  toBool : ∀ {a p} {A : Set a} {P : A → Set p} →
           DecU P → (A → Bool)
  toBool P? x = ⌊ dec⊎⇒dec (P? x) ⌋

  toDecU : ∀ {a} p {A : Set a} (P : A → Bool) →
           DecU (λ x → lift {ℓ = p} (P x) ≡ lift true)
  toDecU p P x with P x
  ... | false = inj₂ (λ ())
  ... | true  = inj₁ refl

  lift-injective : ∀ {a ℓ} {A : Set a} {x y : A} →
                   lift {ℓ = ℓ} x ≡ lift y → x ≡ y
  lift-injective refl = refl

  lift-injective′ : ∀ {a ℓ} {A : Set a} {P : A → Bool} →
                    ∃ (λ x → lift {ℓ = ℓ} (P x) ≡ lift true) →
                    ∃ (λ x → P x ≡ true)
  lift-injective′ = Prod.map₂ lift-injective

  lift-cong′ : ∀ {a p} {A : Set a} {P : A → Bool} →
               ∃ (λ x → P x ≡ true) → ∃ (λ x → lift (P x) ≡ lift true)
  lift-cong′ {p = p} (x , y) = x , cong (lift {ℓ = p}) y

  module _ {a p} {A : Set a} {P : A → Set p} (P? : DecU P) where
    from-eq : ∀ x → toBool P? x ≡ true → P x
    from-eq x eq with P? x
    from-eq x eq | inj₁ Px = Px
    from-eq x () | inj₂ ¬Px

    equal-refl : (∃P : ∃ P) → toBool P? (proj₁ ∃P) ≡ true
    equal-refl (x , Px) with P? x
    ... | inj₁ _   = refl
    ... | inj₂ ¬Px = ⊥-elim $ ¬Px Px

    ∃eq⇒∃P : (∃ λ x → toBool P? x ≡ true) → ∃ P
    ∃eq⇒∃P (x , eq) = x , from-eq x eq

    ∃P⇒∃eq : ∃ P → ∃ λ x → toBool P? x ≡ true
    ∃P⇒∃eq ∃P@(x , Px) = x , equal-refl ∃P

-- LPO <=> LPO-Bool
lpo⇒lpo-Bool : ∀ {a p} {A : Set a} → LPO A p → LPO-Bool A
lpo⇒lpo-Bool {a} {p} lpo P =
  Sum.map lift-injective′ (contraposition lift-cong′) $ lpo (toDecU p P)

lpo-Bool⇒lpo : ∀ {a} p {A : Set a} → LPO-Bool A → LPO A p
lpo-Bool⇒lpo p lpo-Bool P? =
  Sum.map (∃eq⇒∃P P?) (contraposition (∃P⇒∃eq P?)) $
          lpo-Bool (toBool P?)

-- LLPO <=> LLPO-Bool
llpo⇒llpo-Bool : ∀ {a p} {A : Set a} → LLPO A p → LLPO-Bool A
llpo⇒llpo-Bool {a} {p} llpo P Q h =
  Sum.map (contraposition lift-cong′) (contraposition lift-cong′) $
          llpo (toDecU p P) (toDecU p Q)
          (contraposition (Prod.map lift-injective′ lift-injective′) h)

llpo-Bool⇒llpo : ∀ {a} p {A : Set a} → LLPO-Bool A → LLPO A p
llpo-Bool⇒llpo p llpo-Bool P? Q? ¬[∃P×∃Q] =
  Sum.map (contraposition (∃P⇒∃eq P?)) (contraposition (∃P⇒∃eq Q?)) $
          llpo-Bool (toBool P?) (toBool Q?)
                    (contraposition (Prod.map (∃eq⇒∃P P?) (∃eq⇒∃P Q?)) ¬[∃P×∃Q])

-- MP⊎ <=> MP⊎-Bool
mp⊎⇒mp⊎-Bool : ∀ {a p} {A : Set a} → MP⊎ A p → MP⊎-Bool A
mp⊎⇒mp⊎-Bool {a} {p} mp⊎ P Q ¬[¬∃Peq×¬∃Qeq] =
  Sum.map
    (DN-map lift-injective′) (DN-map lift-injective′) $ mp⊎
      (toDecU p P) (toDecU p Q) (contraposition (λ {(u , v) →
      contraposition lift-cong′ u , contraposition lift-cong′ v}) ¬[¬∃Peq×¬∃Qeq])

mp⊎-Bool⇒mp⊎ : ∀ {a} p {A : Set a} → MP⊎-Bool A → MP⊎ A p
mp⊎-Bool⇒mp⊎ p mp⊎-Bool P? Q? ¬[¬∃P×¬Q] =
  Sum.map (DN-map (∃eq⇒∃P P?)) (DN-map (∃eq⇒∃P Q?)) $
          mp⊎-Bool (toBool P?) (toBool Q?) (contraposition (Prod.map
            (contraposition (∃P⇒∃eq P?)) (contraposition (∃P⇒∃eq Q?))) ¬[¬∃P×¬Q])

-- LPO-Bool <=> LPO-Bool-Alt
private
  not-injective : ∀ {x y} → not x ≡ not y → x ≡ y
  not-injective {false} {false} refl = refl
  not-injective {false} {true}  ()
  not-injective {true}  {false} ()
  not-injective {true}  {true}  refl = refl

  x≡false⇒x≢true : ∀ {x} → x ≡ false → x ≢ true
  x≡false⇒x≢true {false} refl ()

  not[x]≢true⇒x≡true : ∀ {x} → not x ≢ true → x ≡ true
  not[x]≢true⇒x≡true {false} neq = ⊥-elim $ neq refl
  not[x]≢true⇒x≡true {true}  _   = refl

  not[x]≡true→x≢true : ∀ {x} → not x ≡ true → x ≢ true
  not[x]≡true→x≢true notx≡true = x≡false⇒x≢true (not-injective notx≡true)

  x≢true⇒x≡false : ∀ {x} → x ≢ true → x ≡ false
  x≢true⇒x≡false {false} neq = refl
  x≢true⇒x≡false {true}  neq = ⊥-elim $ neq refl

lpo-Bool⇒lpo-Bool-Alt : ∀ {a} {A : Set a} → LPO-Bool A → LPO-Bool-Alt A
lpo-Bool⇒lpo-Bool-Alt lpo-Bool P =
  Sum.map (Prod.map₂ not-injective)
          (λ ¬∃notPx≡true x → not[x]≢true⇒x≡true $ ¬∃P→∀¬P ¬∃notPx≡true x) $
            lpo-Bool (not ∘ P)

lpo-Bool-Alt⇒lpo-Bool : ∀ {a} {A : Set a} → LPO-Bool-Alt A → LPO-Bool A
lpo-Bool-Alt⇒lpo-Bool lpo-Bool-Alt P =
  Sum.map (Prod.map₂ not-injective)
          (λ ∀x→notPx≡true → ∀¬P→¬∃P λ x → not[x]≡true→x≢true $ ∀x→notPx≡true x) $
            lpo-Bool-Alt (not ∘ P)


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

open import Agda.Builtin.Cubical.Path

data D : Set where
  c : D

data E : Set where
  c : (x y : E) → x ≡ y

postulate
  A : Set
  f : (x y : E) → x ≡ y → (u v : A) → u ≡ v

works : E → A
works (c x y i) = f x y (E.c x y) (works x) (works y) i

fails : E → A
fails (c x y i) = f x y (  c x y) (fails x) (fails y) i

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module Selective.Examples.TestCall where

open import Selective.Libraries.Call
open import Prelude

AddReplyMessage : MessageType
AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ

AddReply : InboxShape
AddReply = [ AddReplyMessage ]ˡ

AddMessage : MessageType
AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ

Calculator : InboxShape
Calculator = [ AddMessage ]ˡ

calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift (lsuc lzero) ⊤) [] (λ _ → [])
calculatorActor .force = receive ∞>>= λ {
  (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force →
    (Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ)) ∞>> (do
    strengthen []
    calculatorActor)
  ; (Msg (S ()) _)
  }

TestBox : InboxShape
TestBox = AddReply

calltestActor : ∀{i} → ∞ActorM i TestBox (Lift (lsuc lzero) ℕ) [] (λ _ → [])
calltestActor .force = spawn∞ calculatorActor ∞>> do
    x ← call Z Z 0
         ((lift 10) ∷ [ lift 32 ]ᵃ)
         ⊆-refl Z
    strengthen []
    return-result x
  where
    return-result : SelectedMessage {TestBox} (call-select 0 [ Z ]ᵐ Z) →
                    ∀ {i} → ∞ActorM i TestBox (Lift (lsuc lzero) ℕ) [] (λ _ → [])
    return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
    return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
open import Common.Level
open import Common.Prelude
open import Common.Reflection
open import Common.Equality

postulate
  a b : Level

data Check : Set where
  check : (x y : Term) → x ≡ y → Check

pattern _==_ x y = check x y refl

pattern `a = def (quote a) []
pattern `b = def (quote b) []
pattern `suc x = def (quote lsuc) (vArg x ∷ [])
pattern _`⊔_ x y = def (quote _⊔_) (vArg x ∷ vArg y ∷ [])

t₀ = quoteTerm Set₃ == sort (lit 3)
t₁ = quoteTerm (Set a) == sort (set `a)
t₂ = quoteTerm (Set (lsuc b)) == sort (set (`suc `b))
t₃  = quoteTerm (Set (a ⊔ b)) == sort (set (`a `⊔ `b))

max_forks_repo_name: Agda-zh/agda


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

module Cubical.Categories.Instances.Sets where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation

open Category

module _ ℓ where
  SET : Category (ℓ-suc ℓ) ℓ
  ob SET = hSet ℓ
  Hom[_,_] SET (A , _) (B , _) = A → B
  id SET x = x
  _⋆_ SET f g x = g (f x)
  ⋆IdL SET f = refl
  ⋆IdR SET f = refl
  ⋆Assoc SET f g h = refl
  isSetHom SET {A} {B} = isSetΠ (λ _ → snd B)

private
  variable
    ℓ ℓ' : Level

open Functor

-- Hom functors
_[-,_] : (C : Category ℓ ℓ') → (c : C .ob) → Functor (C ^op) (SET ℓ')
(C [-, c ]) .F-ob x    = (C [ x , c ]) , C .isSetHom
(C [-, c ]) .F-hom f k = f ⋆⟨ C ⟩ k
(C [-, c ]) .F-id      = funExt λ _ → C .⋆IdL _
(C [-, c ]) .F-seq _ _ = funExt λ _ → C .⋆Assoc _ _ _

_[_,-] : (C : Category ℓ ℓ') → (c : C .ob)→ Functor C (SET ℓ')
(C [ c ,-]) .F-ob x    = (C [ c , x ]) , C .isSetHom
(C [ c ,-]) .F-hom f k = k ⋆⟨ C ⟩ f
(C [ c ,-]) .F-id      = funExt λ _ → C .⋆IdR _
(C [ c ,-]) .F-seq _ _ = funExt λ _ → sym (C .⋆Assoc _ _ _)

module _ {C : Category ℓ ℓ'} {F : Functor C (SET ℓ')} where
  open NatTrans

  -- natural transformations by pre/post composition
  preComp : {x y : C .ob}
          → (f : C [ x , y ])
          → C [ x ,-] ⇒ F
          → C [ y ,-] ⇒ F
  preComp f α .N-ob c k = (α ⟦ c ⟧) (f ⋆⟨ C ⟩ k)
  preComp f α .N-hom {x = c} {d} k
    = (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ (l ⋆⟨ C ⟩ k)))
    ≡[ i ]⟨ (λ l → (α ⟦ d ⟧) (⋆Assoc C f l k (~ i))) ⟩
      (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ l ⋆⟨ C ⟩ k))
    ≡[ i ]⟨ (λ l → (α .N-hom k) i (f ⋆⟨ C ⟩ l)) ⟩
      (λ l → (F ⟪ k ⟫) ((α ⟦ c ⟧) (f ⋆⟨ C ⟩ l)))
    ∎

-- properties
-- TODO: move to own file
open CatIso renaming (inv to cInv)
open Iso

Iso→CatIso : ∀ {A B : (SET ℓ) .ob}
           → Iso (fst A) (fst B)
           → CatIso (SET ℓ) A B
Iso→CatIso is .mor = is .fun
Iso→CatIso is .cInv = is .inv
Iso→CatIso is .sec = funExt λ b → is .rightInv b -- is .rightInv
Iso→CatIso is .ret = funExt λ b → is .leftInv b -- is .rightInv

max_stars_repo_name: mzeuner/cubical

max_issues_repo_name: mzeuner/cubical

max_forks_repo_name: mzeuner/cubical


text:
------------------------------------------------------------------------
-- Another implementation of the Fibonacci sequence using tail, along
-- with some other examples
------------------------------------------------------------------------

module ArbitraryChunks where

open import Codata.Musical.Notation
open import Codata.Musical.Stream as S using (Stream; _≈_; _∷_)
open import Data.Bool
open import Data.Nat
open import Data.Vec as V using (Vec; []; _∷_)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; [_])

------------------------------------------------------------------------
-- Stream programs

-- StreamP m n A encodes programs generating streams in chunks of size
-- (at least) m, where the first chunk has size (at least) n.

infixr 5 _∷_

data StreamP (m : ℕ) : ℕ → Set → Set₁ where
  [_]     : ∀ {A} (xs : ∞ (StreamP m m A)) → StreamP m 0 A
  _∷_     : ∀ {n A} (x : A) (xs : StreamP m n A) → StreamP m (suc n) A
  forget  : ∀ {n A} (xs : StreamP m (suc n) A) → StreamP m n A
  tail    : ∀ {n A} (xs : StreamP m (suc n) A) → StreamP m n A
  zipWith : ∀ {n A B C} (f : A → B → C)
            (xs : StreamP m n A) (ys : StreamP m n B) → StreamP m n C
  map     : ∀ {n A B} (f : A → B) (xs : StreamP m n A) → StreamP m n B

data StreamW (m : ℕ) : ℕ → Set → Set₁ where
  [_] : ∀ {A} (xs : StreamP m m A) → StreamW m 0 A
  _∷_ : ∀ {n A} (x : A) (xs : StreamW m n A) → StreamW m (suc n) A

forgetW : ∀ {m n A} → StreamW (suc m) (suc n) A → StreamW (suc m) n A
forgetW {n = zero}  (x ∷ [ xs ]) = [ x ∷ forget xs ]
forgetW {n = suc n} (x ∷ xs)     = x ∷ forgetW xs

tailW : ∀ {m n A} → StreamW m (suc n) A → StreamW m n A
tailW (x ∷ xs) = xs

zipWithW : ∀ {m n A B C} → (A → B → C) →
           StreamW m n A → StreamW m n B → StreamW m n C
zipWithW f [ xs ]   [ ys ]   = [ zipWith f xs ys ]
zipWithW f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWithW f xs ys

mapW : ∀ {m n A B} → (A → B) → StreamW m n A → StreamW m n B
mapW f [ xs ]   = [ map f xs ]
mapW f (x ∷ xs) = f x ∷ mapW f xs

whnf : ∀ {m n A} → StreamP (suc m) n A → StreamW (suc m) n A
whnf [ xs ]            = [ ♭ xs ]
whnf (x ∷ xs)          = x ∷ whnf xs
whnf (forget xs)       = forgetW (whnf xs)
whnf (tail xs)         = tailW (whnf xs)
whnf (zipWith f xs ys) = zipWithW f (whnf xs) (whnf ys)
whnf (map f xs)        = mapW f (whnf xs)

mutual

  ⟦_⟧W : ∀ {m n A} → StreamW (suc m) (suc n) A → Stream A
  ⟦ x ∷ [ xs ]   ⟧W = x ∷ ♯ ⟦ xs ⟧P
  ⟦ x ∷ (y ∷ xs) ⟧W = x ∷ ♯ ⟦ y ∷ xs ⟧W

  ⟦_⟧P : ∀ {m n A} → StreamP (suc m) (suc n) A → Stream A
  ⟦ xs ⟧P = ⟦ whnf xs ⟧W

------------------------------------------------------------------------
-- Some examples

-- The Fibonacci sequence.

fib : StreamP 1 1 ℕ
fib = 0 ∷ [ ♯ (1 ∷ zipWith _+_ (forget fib) (tail fib)) ]

-- Some sequence which is defined using (tail ∘ tail).

someSequence : StreamP 2 2 ℕ
someSequence =
  0 ∷ 1 ∷ [ ♯ (1 ∷ 2 ∷ zipWith _+_ (tail (tail someSequence))
                                   (forget (forget someSequence))) ]

------------------------------------------------------------------------
-- The definition of fib is correct

-- ⟦_⟧ is homomorphic with respect to zipWith/S.zipWith.

mutual

  zipWithW-hom :
    ∀ {m n A B C} (_∙_ : A → B → C)
    (xs : StreamW (suc m) (suc n) A) ys →
    ⟦ zipWithW _∙_ xs ys ⟧W ≈ S.zipWith _∙_ ⟦ xs ⟧W ⟦ ys ⟧W
  zipWithW-hom _∙_ (x ∷ [ xs ]) (y ∷ [ ys ])   =
    refl ∷ ♯ zipWith-hom _∙_ xs ys
  zipWithW-hom _∙_ (x ∷ x′ ∷ xs) (y ∷ y′ ∷ ys) =
    refl ∷ ♯ zipWithW-hom _∙_ (x′ ∷ xs) (y′ ∷ ys)

  zipWith-hom : ∀ {m n A B C} (_∙_ : A → B → C)
                (xs : StreamP (suc m) (suc n) A) ys →
                ⟦ zipWith _∙_ xs ys ⟧P ≈ S.zipWith _∙_ ⟦ xs ⟧P ⟦ ys ⟧P
  zipWith-hom _∙_ xs ys = zipWithW-hom _∙_ (whnf xs) (whnf ys)

-- forget is the identity on streams.

open import MapIterate using (_≈P_; _∷_; _≈⟨_⟩_; _∎; soundP)

mutual

  forgetW-lemma : ∀ {m n A} x (xs : StreamW (suc m) (suc n) A) →
                  ⟦ x ∷ forgetW xs ⟧W ≈P x ∷ ♯ ⟦ xs ⟧W
  forgetW-lemma x (x′ ∷ [ xs ])  = x ∷ ♯ (_ ≈⟨ forget-lemma x′ xs ⟩ x′ ∷ ♯ (_ ∎))
  forgetW-lemma x (x′ ∷ x″ ∷ xs) = x ∷ ♯ (_ ≈⟨ forgetW-lemma x′ (x″ ∷ xs) ⟩ x′ ∷ ♯ (_ ∎) )

  forget-lemma : ∀ {m n A} x (xs : StreamP (suc m) (suc n) A) →
                 ⟦ x ∷ forget xs ⟧P ≈P x ∷ ♯ ⟦ xs ⟧P
  forget-lemma x xs with whnf xs | P.inspect whnf xs
  ... | y ∷ y′ ∷ ys | [ eq ] = x ∷ ♯ helper eq
    where
    helper : whnf xs ≡ y ∷ y′ ∷ ys →
             ⟦ y ∷ forgetW (y′ ∷ ys) ⟧W ≈P ⟦ xs ⟧P
    helper eq rewrite eq = _ ≈⟨ forgetW-lemma y (y′ ∷ ys) ⟩ y ∷ ♯ (_ ∎)
  ... | y ∷ [ ys ]  | [ eq ] = x ∷ ♯ helper eq
    where
    helper : whnf xs ≡ y ∷ [ ys ] →
             ⟦ y ∷ forget ys ⟧P ≈P ⟦ xs ⟧P
    helper eq rewrite eq = _ ≈⟨ forget-lemma y ys ⟩ y ∷ ♯ (_ ∎)

-- The stream ⟦ fib ⟧P satisfies its intended defining equation.

open import Relation.Binary
module SS {A : Set} = Setoid (S.setoid A)

fib-correct :
  ⟦ fib ⟧P ≈ 0 ∷ ♯ (1 ∷ ♯ S.zipWith _+_ ⟦ fib ⟧P (S.tail ⟦ fib ⟧P))
fib-correct =
  refl ∷ ♯ (refl ∷ ♯ SS.trans
    (zipWith-hom _+_ (0 ∷ forget fib′) fib′)
    (S.zipWith-cong _+_ (SS.trans (soundP (forget-lemma 0 fib′))
                                  (refl ∷ ♯ SS.refl)) SS.refl))
  where fib′ = 1 ∷ zipWith _+_ (forget fib) (tail fib)

------------------------------------------------------------------------
-- map₂

-- A variant of S.map which processes streams in chunks of size 2.

map₂ : {A B : Set} → (A → B) → Stream A → Stream B
map₂ f (x ∷ xs) with ♭ xs
map₂ f (x ∷ xs) | y ∷ ys = f x ∷ ♯ (f y ∷ ♯ map₂ f (♭ ys))

-- This function is extensionally equal to S.map.

map≈map₂ : ∀ {A B} →
           (f : A → B) → (xs : Stream A) → S.map f xs ≈ map₂ f xs
map≈map₂ f (x ∷ xs) with ♭ xs | P.inspect ♭ xs
map≈map₂ f (x ∷ xs) | y ∷ ys | [ eq ] = refl ∷ ♯ helper eq
  where
  map-f-y∷ys = _

  helper : ∀ {xs} → xs ≡ y ∷ ys → S.map f xs ≈ map-f-y∷ys
  helper refl = refl ∷ ♯ map≈map₂ f (♭ ys)

-- However, as explained in "Beating the Productivity Checker Using
-- Embedded Languages", the two functions are not interchangeable
-- (assuming that pattern matching is evaluated strictly). Let us see
-- what happens when we use the language above. We can define the
-- stream of natural numbers using chunks of size 1 and 2.

nats : StreamP 1 1 ℕ
nats = 0 ∷ [ ♯ map suc nats ]

nats₂ : StreamP 2 2 ℕ
nats₂ = 0 ∷ 1 ∷ [ ♯ map suc nats₂ ]

-- The first use of map corresponds to S.map, and the second to map₂.
-- If we try to use map₂ in the first definition, then we get a type
-- error. The following code is not accepted.

-- nats : StreamP 2 1 ℕ
-- nats = 0 ∷ [ ♯ map suc nats ]

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Terms that operate on changes with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Change.Term where

open import Data.Integer

open import Nehemiah.Syntax.Type public
open import Nehemiah.Syntax.Term public
open import Nehemiah.Change.Type public

import Parametric.Change.Term Const ΔBase as ChangeTerm

apply-base : ChangeTerm.ApplyStructure
apply-base {base-int} = absV 2 (λ Δx x → add x Δx)
apply-base {base-bag} = absV 2 (λ Δx x → union x Δx)

diff-base : ChangeTerm.DiffStructure
diff-base {base-int} = absV 2 (λ x y → add x (minus y))
diff-base {base-bag} = absV 2 (λ x y → union x (negate y))

nil-base : ChangeTerm.NilStructure
nil-base {base-int} = absV 1 (λ x → intlit (+ 0))
nil-base {base-bag} = absV 1 (λ x → empty)

open ChangeTerm.Structure apply-base diff-base nil-base public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module Numeral.Finite.Equiv where

open import Numeral.Finite
open import Relator.Equals.Proofs.Equiv
open import Structure.Setoid

instance
  𝕟-equiv : ∀{n} → Equiv(𝕟(n))
  𝕟-equiv = [≡]-equiv

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Algebra
open import Bundles
open import Structures

module Properties.RingWithoutOne {r₁ r₂} (R : RingWithoutOne r₁ r₂) where

open RingWithoutOne R

import Algebra.Properties.AbelianGroup as AbelianGroupProperties
open import Function.Base using (_$_)
open import Relation.Binary.Reasoning.Setoid setoid


text:
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

postulate
  A B : Set
  @0 a : A

tac : Term → TC ⊤
tac = unify (def (quote a) [])

postulate
  f : {@0 @(tactic tac) x : A} → B

test : B
test = f

max_stars_repo_name: sseefried/agda