text:
{-# OPTIONS --allow-unsolved-metas #-}
module Thesis.ANormalUntyped where

open import Agda.Primitive
open import Data.Empty
open import Data.Unit using (⊤)
open import Data.Product
open import Data.Nat
import Data.Integer.Base as I
open I using (ℤ)
open import Data.Integer.Base using (ℤ)
open import Relation.Binary.PropositionalEquality

{- Typed deBruijn indexes for untyped languages. -}

-- Using a record gives an eta rule saying that all types are equal.
record Type : Set where
  constructor Uni

record DType : Set where
  constructor DUni

open import Base.Syntax.Context Type public
import Base.Syntax.Context DType as DC

data Term (Γ : Context) : Set where
  var : (x : Var Γ Uni) →
    Term Γ
  lett : (f : Var Γ Uni) → (x : Var Γ Uni) → Term (Uni • Γ) → Term Γ

ΔΔ : Context → DC.Context
ΔΔ ∅ = ∅
ΔΔ (τ • Γ) = DUni • ΔΔ Γ

derive-dvar : ∀ {Δ} → (x : Var Δ Uni) → DC.Var (ΔΔ Δ) DUni
derive-dvar this = DC.this
derive-dvar (that x) = DC.that (derive-dvar x)

data DTerm : (Δ : Context) → Set where
  dvar : ∀ {Δ} (x : DC.Var (ΔΔ Δ) DUni) →
    DTerm Δ
  dlett : ∀ {Δ} →
    (f : Var Δ Uni) →
    (x : Var Δ Uni) →
    (t : Term (Uni • Δ)) →
    (df : DC.Var (ΔΔ Δ) DUni) →
    (dx : DC.Var (ΔΔ Δ) DUni) →
    (dt : DTerm (Uni • Δ)) →
    DTerm Δ

derive-dterm : ∀ {Δ} → (t : Term Δ) → DTerm Δ
derive-dterm (var x) = dvar (derive-dvar x)
derive-dterm (lett f x t) =
  dlett f x t (derive-dvar f) (derive-dvar x) (derive-dterm t)

{-
deriveC Δ (lett f x t) = dlett df x dx
-}

-- data ΔCTerm (Γ : Context) (τ : Type) (Δ : Context) : Set where
-- data ΔCTerm (Γ : Context) (τ : Type) (Δ : Context) : Set where
--   cvar : (x : Var Γ τ) Δ →
--     ΔCTerm Γ τ Δ
--   clett : ∀ {σ τ₁ κ} → (f : Var Γ (σ ⇒ τ₁)) → (x : Var Γ σ) →
--     ΔCTerm (τ₁ • Γ) τ (? • Δ) →
--     ΔCTerm Γ τ Δ

weaken-term : ∀ {Γ₁ Γ₂} →
  (Γ₁≼Γ₂ : Γ₁ ≼ Γ₂) →
  Term Γ₁ →
  Term Γ₂
weaken-term Γ₁≼Γ₂ (var x) = var (weaken-var Γ₁≼Γ₂ x)
weaken-term Γ₁≼Γ₂ (lett f x t) = lett (weaken-var Γ₁≼Γ₂ f) (weaken-var Γ₁≼Γ₂ x) (weaken-term (keep _ • Γ₁≼Γ₂) t)

-- I don't necessarily recommend having a separate syntactic category for
-- functions, but we should prove a fundamental lemma for them too, somehow.
-- I'll probably end up with some ANF allowing lambdas to do the semantics.
data Fun (Γ : Context) : Set where
  term : Term Γ → Fun Γ
  abs : ∀ {σ} → Fun (σ • Γ) → Fun Γ

data DFun (Δ : Context) : Set where
  dterm : DTerm Δ → DFun Δ
  dabs : DFun (Uni • Δ) → DFun Δ

derive-dfun : ∀ {Δ} → (t : Fun Δ) → DFun Δ
derive-dfun (term t) = dterm (derive-dterm t)
derive-dfun (abs f) = dabs (derive-dfun f)

weaken-fun : ∀ {Γ₁ Γ₂} →
  (Γ₁≼Γ₂ : Γ₁ ≼ Γ₂) →
  Fun Γ₁ →
  Fun Γ₂
weaken-fun Γ₁≼Γ₂ (term x) = term (weaken-term Γ₁≼Γ₂ x)
weaken-fun Γ₁≼Γ₂ (abs f) = abs (weaken-fun (keep _ • Γ₁≼Γ₂) f)

data Val : Type → Set
data DVal : DType → Set
-- data Val (τ : Type) : Set

open import Base.Denotation.Environment Type Val public
open import Base.Data.DependentList public

import Base.Denotation.Environment DType DVal as D

-- data Val (τ : Type) where
data Val where
  closure : ∀ {Γ} → (t : Fun (Uni • Γ)) → (ρ : ⟦ Γ ⟧Context) → Val Uni
  intV : ∀ (n : ℕ) → Val Uni

data DVal where
  dclosure : ∀ {Γ} → (dt : DFun (Uni • Γ)) → (ρ : ⟦ Γ ⟧Context) → (dρ : D.⟦ ΔΔ Γ ⟧Context) → DVal DUni
  dintV : ∀ (n : ℤ) → DVal DUni

ChΔ : ∀ (Δ : Context) → Set
ChΔ Δ = D.⟦ ΔΔ Δ ⟧Context

-- ⟦_⟧Term : ∀ {Γ τ} → Term Γ τ → ⟦ Γ ⟧Context → ⟦ τ ⟧Type
-- ⟦ var x ⟧Term ρ = ⟦ x ⟧Var ρ
-- ⟦ lett f x t ⟧Term ρ = ⟦ t ⟧Term (⟦ f ⟧Var ρ (⟦ x ⟧Var ρ) • ρ)

-- XXX separate syntax is a bit dangerous. Also, do I want to be so accurate relative to the original model?
data _⊢_↓[_]_ {Γ} (ρ : ⟦ Γ ⟧Context) : Term Γ → ℕ → Val Uni → Set

data _F⊢_↓[_]_ {Γ} (ρ : ⟦ Γ ⟧Context) : Fun Γ → ℕ → Val Uni → Set where
  abs : ∀ {t : Fun (Uni • Γ)} →
    ρ F⊢ abs t ↓[ 0 ] closure t ρ
  term : ∀ {v} n (t : Term Γ) →
    ρ ⊢ t ↓[ n ] v →
    ρ F⊢ term t ↓[ n ] v

data _⊢_↓[_]_ {Γ} (ρ : ⟦ Γ ⟧Context) where
  var : ∀ (x : Var Γ Uni) →
    ρ ⊢ var x ↓[ 0 ] (⟦ x ⟧Var ρ)
  lett : ∀ n1 n2 {Γ' ρ′ v1 v2 v3} {f x t t'}  →
    ρ ⊢ var f ↓[ 0 ] closure {Γ'} t' ρ′ →
    ρ ⊢ var x ↓[ 0 ] v1 →
    (v1 • ρ′) F⊢ t' ↓[ n1 ] v2 →
    (v2 • ρ) ⊢ t ↓[ n2 ] v3 →
    ρ ⊢ lett f x t ↓[ suc (suc (n1 + n2)) ] v3
  -- lit : ∀ n →
  --   ρ ⊢ const (lit n) ↓[ 0 ] intV n

-- data _D_⊢_↓[_]_ {Γ} (ρ : ⟦ Γ ⟧Context) (dρ : D.⟦ ΔΔ Γ ⟧Context) : DTerm Γ → ℕ → DVal DUni → Set where
--   dvar : ∀ (x : DC.Var (ΔΔ Γ) DUni) →
--     ρ D dρ ⊢ dvar x ↓[ 0 ] (D.⟦ x ⟧Var dρ)
--   dlett : ∀ n1 n2 n3 n4 {Γ' ρ′ ρ'' dρ' v1 v2 v3 dv1 dv2 dv3} {f x t df dx dt t' dt'}  →
--     ρ ⊢ var f ↓[ 0 ] closure {Γ'} t' ρ′ →
--     ρ ⊢ var x ↓[ 0 ] v1 →
--     (v1 • ρ′) F⊢ t' ↓[ n1 ] v2 →
--     (v2 • ρ) ⊢ t ↓[ n2 ] v3 →
--     -- With a valid input ρ' and ρ'' coincide? Varies among plausible validity
--     -- definitions.
--     ρ D dρ ⊢ dvar df ↓[ 0 ] dclosure {Γ'} dt' ρ'' dρ' →
--     ρ D dρ ⊢ dvar dx ↓[ 0 ] dv1 →
--     (v1 • ρ'') D (dv1 • dρ') F⊢ dt' ↓[ n3 ] dv2 →
--     (v2 • ρ) D (dv2 • dρ) ⊢ dt ↓[ n4 ] dv3 →
--     ρ D dρ ⊢ dlett f x t df dx dt ↓[ suc (suc (n1 + n2)) ] dv3

-- Do I need to damn count steps here? No.

data _D_⊢_↓_ {Γ} (ρ : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) : DTerm Γ → DVal DUni → Set

data _D_F⊢_↓_ {Γ} (ρ : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) : DFun Γ → DVal DUni → Set where
  dabs : ∀ {dt : DFun (Uni • Γ)} →
    ρ D dρ F⊢ dabs dt ↓ dclosure dt ρ dρ
  dterm : ∀ {dv} (dt : DTerm Γ) →
    ρ D dρ ⊢ dt ↓ dv →
    ρ D dρ F⊢ dterm dt ↓ dv

data _D_⊢_↓_ {Γ} (ρ : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) where
  dvar : ∀ (x : DC.Var (ΔΔ Γ) DUni) →
    ρ D dρ ⊢ dvar x ↓ (D.⟦ x ⟧Var dρ)
  dlett : ∀ n1 n2 {Γ' ρ′ ρ'' dρ' v1 v2 v3 dv1 dv2 dv3} {f x t df dx dt t' dt'}  →
    ρ ⊢ var f ↓[ 0 ] closure {Γ'} t' ρ′ →
    ρ ⊢ var x ↓[ 0 ] v1 →
    (v1 • ρ′) F⊢ t' ↓[ n1 ] v2 →
    (v2 • ρ) ⊢ t ↓[ n2 ] v3 →
    -- With a valid input ρ' and ρ'' coincide? Varies among plausible validity
    -- definitions.
    ρ D dρ ⊢ dvar df ↓ dclosure {Γ'} dt' ρ'' dρ' →
    ρ D dρ ⊢ dvar dx ↓ dv1 →
    (v1 • ρ'') D (dv1 • dρ') F⊢ dt' ↓ dv2 →
    (v2 • ρ) D (dv2 • dρ) ⊢ dt ↓ dv3 →
    ρ D dρ ⊢ dlett f x t df dx dt ↓ dv3

open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Relation.Binary hiding (_⇒_)

suc∸ : ∀ m n → n ≤ m → suc (m ∸ n) ≡ suc m ∸ n
suc∸ m zero z≤n = refl
suc∸ (suc m) (suc n) (s≤s n≤m) = suc∸ m n n≤m

suc∸suc : ∀ m n → n < m → suc (m ∸ suc n) ≡ m ∸ n
suc∸suc (suc m) zero (s≤s n<m) = refl
suc∸suc (suc m) (suc n) (s≤s n<m) = suc∸suc m n n<m

lemlt : ∀ j k → suc j < k → k ∸ suc j < k
lemlt j (suc k) (s≤s j<k) = s≤s (∸-mono {k} {k} {j} {0} ≤-refl z≤n)

lemlt′ : ∀ j k → suc j <′ k → k ∸ suc j <′ k
lemlt′ j k j<′k = ≤⇒≤′ (lemlt j k (≤′⇒≤ j<′k))

open import Induction.WellFounded
open import Induction.Nat
rrelT3-Type : ℕ → Set₁
rrelT3-Type n =
  ∀ {Γ} → (t1 : Fun Γ) (dt : DFun Γ) (t2 : Fun Γ)
  (ρ1 : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) (ρ2 : ⟦ Γ ⟧Context) → Set

rrelV3-Type : ℕ → Set₁
rrelV3-Type n = ∀ (v1 : Val Uni) (dv : DVal DUni) (v2 : Val Uni) → Set

rrelTV3-Type : ℕ → Set₁
rrelTV3-Type n = rrelT3-Type n × rrelV3-Type n

-- The type of the function availalbe for recursive calls.
rrelTV3-recSubCallsT : ℕ → Set₁
rrelTV3-recSubCallsT n = (k : ℕ) → k < n → rrelTV3-Type k

mutual
  -- Assemble together
  rrelTV3-step : ∀ n → rrelTV3-recSubCallsT n → rrelTV3-Type n
  rrelTV3-step n rec-rrelTV3 =
    let rrelV3-n = rrelV3-step n rec-rrelTV3
    in rrelT3-step n rec-rrelTV3 rrelV3-n , rrelV3-n
  rrelTV3 =  <-rec rrelTV3-Type rrelTV3-step
  rrelT3 : ∀ n → rrelT3-Type n
  rrelT3 n =  proj₁ (rrelTV3 n)
  rrelV3 : ∀ n → rrelV3-Type n
  rrelV3 n =  proj₂ (rrelTV3 n)

  s-rrelV3 :
    ∀ k → rrelTV3-recSubCallsT k → rrelV3-Type k →
    ∀ j → j < k → rrelV3-Type (k ∸ j)
  s-rrelV3 k rec-rrelTV3 rrelV3-k 0 _ = rrelV3-k
  s-rrelV3 k rec-rrelTV3 rrelV3-k (suc j) sucj<k = proj₂ (rec-rrelTV3 (k ∸ suc j) (lemlt j k sucj<k))
  -- Have the same context for t1, dt and t2? Yeah, good, that's what we want in the end...
  -- Though we might want more flexibility till when we have replacement
  -- changes.
  rrelT3-step : ∀ k → rrelTV3-recSubCallsT k →
    rrelV3-Type k →
    -- rrelV3-Type n
    ∀ {Γ} → (t1 : Fun Γ) (dt : DFun Γ) (t2 : Fun Γ)
      (ρ1 : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) (ρ2 : ⟦ Γ ⟧Context) → Set
  rrelT3-step k rec-rrelTV3 rrelV3-k =
    λ t1 dt t2 ρ1 dρ ρ2 →
    ∀ j (j<k : j < k) n2 →
    (v1 v2 : Val Uni) →
    (ρ1⊢t1↓[j]v1 : ρ1 F⊢ t1 ↓[ j ] v1) →
    (ρ2⊢t2↓[n2]v2 : ρ2 F⊢ t2 ↓[ n2 ] v2) →
    Σ[ dv ∈ DVal DUni ] Σ[ dn ∈ ℕ ]
    ρ1 D dρ F⊢ dt ↓ dv ×
    s-rrelV3 k rec-rrelTV3 rrelV3-k j j<k v1 dv v2
    -- where
    --   s-rrelV3 : ∀ j → j <′ k → rrelV3-Type (k ∸ j)
    --   -- If j = 0, we can't do a recursive call on (k - j) because that's not
    --   -- well-founded. Luckily, we don't need to, just use relV as defined at
    --   -- the same level.
    --   -- Yet, this will be a pain in proofs.
    --   s-rrelV3 0 _ = rrelV3-k
    --   s-rrelV3 (suc j) sucj<′k = proj₂ (rec-rrelTV3 (k ∸ suc j) (lemlt′ j k sucj<′k))

  rrelV3-step : ∀ n → rrelTV3-recSubCallsT n →
    -- rrelV3-Type n
    ∀ (v1 : Val Uni) (dv : DVal DUni) (v2 : Val Uni) → Set
  rrelV3-step n rec-rrelTV3 (intV v1) (dintV dv) (intV v2) = dv I.+ (I.+ v1) ≡ (I.+ v2)
  rrelV3-step n rec-rrelTV3 (intV v1) (dintV n₁) (closure t ρ) = ⊥
  rrelV3-step n rec-rrelTV3 (intV v1) (dclosure dt ρ dρ) c = ⊥
  rrelV3-step n rec-rrelTV3 (closure {Γ1} t1 ρ1) (dclosure {ΔΓ} dt ρ' dρ) (closure {Γ2} t2 ρ2) =
      -- Require a proof that the two contexts match:
      Σ ((Γ1 ≡ Γ2) × (Γ1 ≡ ΔΓ)) λ { (refl , refl) →
        ∀ (k : ℕ) (k<n : k < n) v1 dv v2 →
        proj₂ (rec-rrelTV3 k k<n) v1 dv v2 →
        proj₁ (rec-rrelTV3 k k<n)
          t1
          dt
          t2
          (v1 • ρ1)
          (dv • dρ)
          (v2 • ρ2)
      }
  rrelV3-step n rec-rrelTV3 (closure t ρ) (dclosure dt ρ₁ dρ) (intV n₁) = ⊥
  rrelV3-step n rec-rrelTV3 (closure t ρ) (dintV n₁) c = ⊥

open import Postulate.Extensionality
mutual
  rrelT3-equiv : ∀ k {Γ} {t1 : Fun Γ} {dt t2 ρ1 dρ ρ2} →
    rrelT3 k t1 dt t2 ρ1 dρ ρ2 ≡
    ∀ j (j<k : j < k) n2 →
    ∀ (v1 v2 : Val Uni) →
    (ρ1⊢t1↓[j]v1 : ρ1 F⊢ t1 ↓[ j ] v1) →
    (ρ2⊢t2↓[n2]v2 : ρ2 F⊢ t2 ↓[ n2 ] v2) →
    Σ[ dv ∈ DVal DUni ] Σ[ dn ∈ ℕ ]
    ρ1 D dρ F⊢ dt ↓ dv ×
    rrelV3 j v1 dv v2
  rrelT3-equiv k {Γ} {t1} {dt} {t2} {ρ1} {dρ} {ρ2} =
    cong (λ □ → ∀ j → □ j) (ext
      λ {
        zero -> cong {lsuc lzero} {lsuc lzero} {{!!}} {{!!}} {!!} {{!!}} {{! !}} {!cong!}
        -- cong {{!!}} {{!!}}
        -- (λ (□ : zero < k → ∀ (n2 : ℕ) (v1 v2 : Val Uni) (ρ1⊢t1↓[j]v1 : ρ1 F⊢ t1 ↓[ zero ] v1)  → {!(ρ2⊢t2↓[n2]v2 : ρ2 F⊢ t2 ↓[ n2 ] v2) → ? !})→
        --              ∀ (j<k : zero < k) n2 →
        --              (v1 v2 : Val Uni) →
        --              (ρ1⊢t1↓[j]v1 : ρ1 F⊢ t1 ↓[ zero ] v1) →
        --              (ρ2⊢t2↓[n2]v2 : ρ2 F⊢ t2 ↓[ n2 ] v2) →
        --              Σ-syntax (DVal DUni)
        --              λ dv → Σ-syntax ℕ λ dn → (ρ1 D dρ F⊢ dt ↓ dv) × □ j<k n2 v1 v2 ρ1⊢t1↓[j]v1 ρ2⊢t2↓[n2]v2)
        --           {!!}
        ;
        (suc j') -> {!!}})
    -- cong (λ □ →
    --      (j : ℕ) (j<k : j < k) (n2 : ℕ)
    --      (v1 v2 : Val Uni) →
    --      (ρ1⊢t1↓[j]v1 : ρ1 F⊢ t1 ↓[ j ] v1) →
    --      -- (ρ2⊢t2↓[n2]v2 : ρ2 F⊢ t2 ↓[ n2 ] v2) →
    --        □ j j<k n2 v1 v2 ρ1⊢t1↓[j]v1
    --     -- □ j<k n2 v1 v2 ρ1⊢t1↓[j]v1 ρ2⊢t2↓[n2]v2
    --     ) (ext³ λ j j<k n2 → {!ext³!})

  rrelV3-equiv : ∀ n {Γ1 Γ2 ΔΓ t1 dt t2 ρ1 ρ' dρ ρ2} →
    rrelV3 n (closure {Γ1} t1 ρ1) (dclosure {ΔΓ} dt ρ' dρ) (closure {Γ2} t2 ρ2) ≡ Σ ((Γ1 ≡ Γ2) × (Γ1 ≡ ΔΓ)) λ { (refl , refl) →
        ∀ (k : ℕ) (k<n : k <′ n) v1 dv v2 →
        rrelV3 k v1 dv v2 →
        rrelT3 k
          t1
          dt
          t2
          (v1 • ρ1)
          (dv • dρ)
          (v2 • ρ2)
      }
  rrelV3-equiv n = cong (λ □ → Σ (_ ≡ _ × _ ≡ _) □) (ext (λ { (eq1 , eq2) →
    cong
      (λ □ →
         (λ { (refl , refl)
                → ∀ (k : ℕ) (k<n : k <′ n) v1 dv v2 → □ k k<n v1 dv v2
            })
         eq1 eq2)
      (ext (λ x → ext {!!}))}))
  --
  -- cong (λ □ → ∀ k → (k<n : k <′ n) → □ k k<n)
  -- rrelV3-equiv k

rrelρ3 : ℕ → ∀ Γ (ρ1 : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) (ρ2 : ⟦ Γ ⟧Context) → Set
rrelρ3 n ∅ ∅ ∅ ∅ = ⊤
rrelρ3 n (Uni • Γ) (v1 • ρ1) (dv • dρ) (v2 • ρ2) = rrelV3 n v1 dv v2 × rrelρ3 n Γ ρ1 dρ ρ2

--
rfundamental3 : ∀ {Γ} (t : Fun Γ) → ∀ k ρ1 dρ ρ2 → (ρρ : rrelρ3 k Γ ρ1 dρ ρ2) → rrelT3 k t (derive-dfun t) t ρ1 dρ ρ2
rfundamental3 (term x) k ρ1 dρ ρ2 ρρ j j<k n2 v1 v2 ρ1⊢t1↓[j]v1 ρ2⊢t2↓[n2]v2 = {!!}
rfundamental3 {Γ} (abs t) k ρ1 dρ ρ2 ρρ .0 j<k .0 (closure .t .ρ1) (closure .t .ρ2) abs abs = dclosure (derive-dfun t) ρ1 dρ , 0 , dabs , (refl , refl) , {!body !}
  where
    body1 : ∀ k₁ (k₁<k : k₁ <′ k) → (v1 : Val Uni) (dv : DVal DUni) (v2 : Val Uni) → rrelV3 k₁ v1 dv v2 → rrelT3 k₁ t (derive-dfun t) t (v1 • ρ1) (dv • dρ) (v2 • ρ2)
    body1 = λ k₁ k₁<k v1 dv v2 x v3 v4 j n2 j<k₁ ρ1⊢t1↓[j]v1 ρ2⊢t2↓[n2]v2 → {!
    rfundamental3 {Uni • Γ} t k₁ (v1 • ρ1) (dv • dρ) (v2 • ρ2) ({!vv!} , {!ρρ!}) v3 v4 0 n2 {!j<k₁ !} {! ρ1⊢t1↓[j]v1 !} ρ2⊢t2↓[n2]v2
    !}
  -- λ
  -- { k₁ k<n v1 dv v2 vv v3 v4 0 n2 j<k₁ ρ1⊢t1↓[j]v1 ρ2⊢t2↓[n2]v2 → {!
  -- rfundamental3 {Uni • Γ} t k₁ (v1 • ρ1) (dv • dρ) (v2 • ρ2) ({!vv!} , {!ρρ!}) v3 v4 0 n2 {!j<k₁ !} {! ρ1⊢t1↓[j]v1 !} ρ2⊢t2↓[n2]v2
  -- !}
  -- -- (Some.wfRec-builder rrelTV3-Type rrelTV3-step k₁
  --                     -- (<-well-founded′ k k₁ k<n))

  -- -- All.wfRec-builder <-well-founded _ rrelTV3-Type rrelTV3-step k k₁ k<n : rrelTV3-Type k₁
  -- --
  -- ; k₁ k<n v1 dv v2 vv v3 v4 (suc j) n2 j<k₁ ρ1⊢t1↓[j]v1 ρ2⊢t2↓[n2]v2 → {!
  -- !}
  -- -- rfundamental3 t k₁ (v1 • ρ1) (dv • dρ) (v2 • ρ2) ({!vv!} , {!ρρ!}) v3 v4 {!suc j !} n2 {!j<k₁ !} {! ρ1⊢t1↓[j]v1 !} ρ2⊢t2↓[n2]v2
  -- }

  --   -- ∀ k → rrelTV3-recSubCallsT k → rrelV3-Type k →
  --   -- ∀ j → j <′ k → rrelV3-Type (k ∸ j)
  --   foo : s-rrelV3 k
  --     (All.wfRec-builder <-well-founded _ rrelTV3-Type rrelTV3-step k)
  --     (rrelV3-step k (All.wfRec-builder <-well-founded _ rrelTV3-Type rrelTV3-step k))
  --     j j<k v1 (dclosure (derive-dfun t) ρ1 dρ) v2
  --   foo with j
  --   ... | s = {!!}


text:
-----------------------------------------------------------------------------
-- Existential elimination
-----------------------------------------------------------------------------

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

module FOT.Common.FOL.Existential.Elimination where

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

postulate D : Set

module ∃₁ where
  -- Type theoretical version

  -- We add 3 to the fixities of the Agda standard library 0.8.1 (see
  -- Data/Product.agda).
  infixr 7 _,_

  -- The existential quantifier type on D.
  data ∃ (A : D → Set) : Set where
    _,_ : (x : D) → A x → ∃ A

  -- Sugar syntax for the existential quantifier.
  syntax ∃ (λ x → e) = ∃[ x ] e

  -- The existential proyections.
  ∃-proj₁ : ∀ {A} → ∃ A → D
  ∃-proj₁ (x , _) = x

  ∃-proj₂ : ∀ {A} → (h : ∃ A) → A (∃-proj₁ h)
  ∃-proj₂ (_ , Ax) = Ax

  -- Some examples

  -- The order of quantifiers of the same sort is irrelevant.
  ∃-ord : {A² : D → D → Set} → (∃[ x ] ∃[ y ] A² x y) → (∃[ y ] ∃[ x ] A² x y)
  ∃-ord (x , y , h) = y , x , h

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

module ∃₂ where
  -- First-order logic version

  -- We add 3 to the fixities of the Agda standard library 0.8.1 (see
  -- Data/Product.agda).
  infixr 7 _,_

  -- The existential quantifier type on D.
  data ∃ (A : D → Set) : Set where
    _,_ : (x : D) → A x → ∃ A

  -- Sugar syntax for the existential quantifier.
  syntax ∃ (λ x → e) = ∃[ x ] e

  -- Existential elimination
  --     ∃x.A(x)   A(x) → B
  --  ------------------------
  --             B

  -- NB. We do not use the usual type theory elimination with two
  -- projections because we are working in first-order logic where we
  -- do need extract a witness from an existence proof.
  ∃-elim : {A : D → Set}{B : Set} → ∃ A → ((x : D) → A x → B) → B
  ∃-elim (x , Ax) h = h x Ax

  -- Some examples

  -- The order of quantifiers of the same sort is irrelevant.
  ∃-ord : {A² : D → D → Set} → (∃[ x ] ∃[ y ] A² x y) → (∃[ y ] ∃[ x ] A² x y)
  ∃-ord h = ∃-elim h (λ x h₁ → ∃-elim h₁ (λ y prf → y , x , prf))

  -- A proof non-FOL valid
  non-FOL : {A : D → Set} → ∃ A → D
  non-FOL h = ∃-elim h (λ x _ → x)

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

module ∃₃ where
  -- First-order logic version

  -- A different version from the existential introduction
  --      A(x)
  --  ------------
  --     ∃x.A(x)

  -- The existential quantifier type on D.
  data ∃ (A : D → Set) : Set where
    ∃-intro : ((x : D) → A x) → ∃ A

  -- Sugar syntax for the existential quantifier.
  syntax ∃ (λ x → e) = ∃[ x ] e

  postulate d : D

  -- Existential elimination.
  -- NB. It is neccesary that D ≢ ∅.
  ∃-elim : {A : D → Set}{B : Set} → ∃ A → ((x : D) → A x → B) → B
  ∃-elim (∃-intro h₁) h₂ = h₂ d (h₁ d)

  -- Some examples

  -- Impossible
  -- thm : {A : D → Set} → ∃[ x ] A x → ∃[ y ] A y
  -- thm h = ∃-elim h (λ x prf → {!!})

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --show-implicit #-}

module _ where

postulate
  R : Set

module ModuleB where

  module NotRecordB (r : R) where
    postulate notfieldB : Set

  open module NotRecBI {{r : R}} = NotRecordB r public

  record RecordB : Set₁ where
    field
      fieldB : Set

  open module RecBI {{r : RecordB}} = RecordB r public

open module ModBA = ModuleB

postulate
  myRecB : RecordB
  myR    : R

test₀ : fieldB {{myRecB}}
test₀ = {!!}

test₁ : ModuleB.RecordB.fieldB myRecB
test₁ = {!!}

test₂ : notfieldB {{myR}}
test₂ = {!!}

test₃ : ModuleB.NotRecordB.notfieldB myR
test₃ = {!!}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

open import Definition.Typed.EqualityRelation

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

open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.Untyped using (Con ; Term)

open import Tools.Nat
open import Tools.Product

private
  variable
    n : Nat
    Γ : Con Term n

-- Weak head expansion of valid terms.
redSubstTermᵛ : ∀ {A t u l}
              → ([Γ] : ⊩ᵛ Γ)
              → Γ ⊩ᵛ t ⇒ u ∷ A / [Γ]
              → ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
              → Γ ⊩ᵛ⟨ l ⟩ u ∷ A / [Γ] / [A]
              → Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A]
              × Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A / [Γ] / [A]
redSubstTermᵛ [Γ] t⇒u [A] [u] =
  (λ ⊢Δ [σ] →
     let [σA] = proj₁ ([A] ⊢Δ [σ])
         [σt] , [σt≡σu] = redSubstTerm (t⇒u ⊢Δ [σ])
                                       (proj₁ ([A] ⊢Δ [σ]))
                                       (proj₁ ([u] ⊢Δ [σ]))
     in  [σt]
     ,   (λ [σ′] [σ≡σ′] →
            let [σ′A] = proj₁ ([A] ⊢Δ [σ′])
                [σA≡σ′A] = proj₂ ([A] ⊢Δ [σ]) [σ′] [σ≡σ′]
                [σ′t] , [σ′t≡σ′u] = redSubstTerm (t⇒u ⊢Δ [σ′])
                                                 (proj₁ ([A] ⊢Δ [σ′]))
                                                 (proj₁ ([u] ⊢Δ [σ′]))
            in  transEqTerm [σA] [σt≡σu]
                            (transEqTerm [σA] ((proj₂ ([u] ⊢Δ [σ])) [σ′] [σ≡σ′])
                                         (convEqTerm₂ [σA] [σ′A] [σA≡σ′A]
                                                      (symEqTerm [σ′A] [σ′t≡σ′u])))))
  , (λ ⊢Δ [σ] → proj₂ (redSubstTerm (t⇒u ⊢Δ [σ])
                                    (proj₁ ([A] ⊢Δ [σ]))
                                    (proj₁ ([u] ⊢Δ [σ]))))

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
{-# OPTIONS --no-termination-check #-}

module PragmasApplyOnlyToCurrentModule where

import Imports.NonTerminating

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.2GroupoidTruncation where

open import Cubical.HITs.2GroupoidTruncation.Base public
open import Cubical.HITs.2GroupoidTruncation.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Structures.Queue where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Functions.FunExtEquiv
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.SIP

open import Cubical.Structures.Axioms
open import Cubical.Structures.Macro
open import Cubical.Structures.Auto

open import Cubical.Data.Unit
open import Cubical.Data.Maybe as Maybe
open import Cubical.Data.Sigma
open import Cubical.Data.List

-- Developing Queues as a standard notion of structure, see
-- https://github.com/ecavallo/cubical/blob/queue/Cubical/Experiments/Queue.agda
-- for the original development

private
  variable
   ℓ ℓ' : Level

-- We start fixing a set A on which we define what it means for a type Q to have
-- a Queue structure (wrt. A)
module Queues-on (A : Type ℓ) (Aset : isSet A) where
 -- A Queue structure has three components, the empty Queue, an enqueue function and a dequeue function
 -- We first deal with enq and deq as separate structures

 -- deq as a structure
 -- First, a few preliminary results that we will need later
 deqMap : {X Y : Type ℓ} → (X → Y) → Maybe (X × A) → Maybe (Y × A)
 deqMap = map-Maybe ∘ map-fst

 deqMapId : {X : Type ℓ} → ∀ r → deqMap (idfun X) r ≡ r
 deqMapId = map-Maybe-id

 deqMap-∘ :{B C D : Type ℓ}
  (g : C → D) (f : B → C)
  → ∀ r → deqMap {X = C} g (deqMap f r) ≡ deqMap (λ b → g (f b)) r
 deqMap-∘ g f nothing = refl
 deqMap-∘ g f (just (b , a)) = refl

 -- Now we can do Queues:
 rawQueueDesc =
   autoDesc (λ (X : Type ℓ) → X × (A → X → X) × (X → Transp[ Maybe (X × A) ]))

 open Macro ℓ rawQueueDesc public renaming
   ( structure to RawQueueStructure
   ; equiv to RawQueueEquivStr
   ; univalent to rawQueueUnivalentStr
   )

 RawQueue : Type (ℓ-suc ℓ)
 RawQueue = TypeWithStr ℓ RawQueueStructure

 returnOrEnq : {Q : Type ℓ}
  → RawQueueStructure Q → A → Maybe (Q × A) → Q × A
 returnOrEnq (emp , enq , _) a qr =
   Maybe.rec (emp , a) (λ {(q , b) → enq a q , b}) qr

 QueueAxioms : (Q : Type ℓ) → RawQueueStructure Q → Type ℓ
 QueueAxioms Q S@(emp , enq , deq) =
   (isSet Q)
   × (deq emp ≡ nothing)
   × (∀ a q → deq (enq a q) ≡ just (returnOrEnq S a (deq q)))
   × (∀ a a' q q' → enq a q ≡ enq a' q' → (a ≡ a') × (q ≡ q'))
   × (∀ q q' → deq q ≡ deq q' → q ≡ q')

 isPropQueueAxioms : ∀ Q S → isProp (QueueAxioms Q S)
 isPropQueueAxioms Q S =
   isPropΣ isPropIsSet
           (λ Qset → isProp×3 (isOfHLevelDeq Qset _ _)
                              (isPropΠ2 λ _ _ → isOfHLevelDeq Qset _ _)
                              (isPropΠ3 λ _ _ _ → isPropΠ2 λ _ _ → isProp× (Aset _ _) (Qset _ _))
                              (isPropΠ3 λ _ _ _ → Qset _ _))
   where
   isOfHLevelDeq : isSet Q → isOfHLevel 2 (Maybe (Q × A))
   isOfHLevelDeq Qset = isOfHLevelMaybe 0 (isSet× Qset Aset)

 QueueStructure : Type ℓ → Type ℓ
 QueueStructure = AxiomsStructure RawQueueStructure QueueAxioms

 Queue : Type (ℓ-suc ℓ)
 Queue = TypeWithStr ℓ QueueStructure

 QueueEquivStr : StrEquiv QueueStructure ℓ
 QueueEquivStr = AxiomsEquivStr RawQueueEquivStr QueueAxioms

 queueUnivalentStr : UnivalentStr QueueStructure QueueEquivStr
 queueUnivalentStr = axiomsUnivalentStr RawQueueEquivStr isPropQueueAxioms rawQueueUnivalentStr

 FiniteQueueAxioms : (Q : Type ℓ) → QueueStructure Q → Type ℓ
 FiniteQueueAxioms Q ((emp , enq , _) , _) = isEquiv (foldr enq emp)

 isPropFiniteQueueAxioms : ∀ Q S → isProp (FiniteQueueAxioms Q S)
 isPropFiniteQueueAxioms Q S = isPropIsEquiv _

 FiniteQueueStructure : Type ℓ → Type ℓ
 FiniteQueueStructure = AxiomsStructure QueueStructure FiniteQueueAxioms

 FiniteQueue : Type (ℓ-suc ℓ)
 FiniteQueue = TypeWithStr ℓ FiniteQueueStructure

 FiniteQueueEquivStr : StrEquiv FiniteQueueStructure ℓ
 FiniteQueueEquivStr = AxiomsEquivStr QueueEquivStr FiniteQueueAxioms

 finiteQueueUnivalentStr : UnivalentStr FiniteQueueStructure FiniteQueueEquivStr
 finiteQueueUnivalentStr = axiomsUnivalentStr QueueEquivStr isPropFiniteQueueAxioms queueUnivalentStr


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
import Definition.Typed.Weakening as Twk
open import Definition.Typed.EqualityRelation
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
import Definition.LogicalRelation.Weakening as Lwk
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.Empty
-- open import Definition.LogicalRelation.Substitution.Introductions.Pi
-- open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.Introductions.Universe
open import Definition.LogicalRelation.Substitution.MaybeEmbed

open import Tools.Product
open import Tools.Empty
import Tools.Unit as TU
import Tools.PropositionalEquality as PE
import Data.Nat as Nat

module cast-ΠΠ-lemmas
       {Γ rF F F₁}
       (⊢Γ : ⊢ Γ)
       (⊢F : Γ ⊢ F ^ [ rF , ι ⁰ ])
       ([F] : ∀ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Δ ⊩⟨ ι ⁰ ⟩ wk ρ F ^ [ rF , ι ⁰ ])
       (⊢F₁    : Γ ⊢ F₁ ^ [ rF , ι ⁰ ])
       ([F₁] : ∀ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Δ ⊩⟨ ι ⁰ ⟩ wk ρ F₁ ^ [ rF , ι ⁰ ])
       (recursor : ∀ {x e ρ Δ}
         ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
         ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
         (⊢e : Δ ⊢ e ∷ Id (Univ rF ⁰) (wk ρ F₁) (wk ρ F) ^ [ % , ι ¹ ])
         → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk ρ F₁) (wk ρ F) e x ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
       (extrecursor : ∀ {ρ Δ x y e e′}
         → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
         → ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
         → ([y] : Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
         → ([x≡y] : Δ ⊩⟨ ι ⁰ ⟩ x ≡ y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
         → (⊢e : Δ ⊢ e ∷ Id (Univ rF ⁰) (wk ρ F₁) (wk ρ F) ^ [ % , ι ¹ ])
         → (⊢e′ : Δ ⊢ e′ ∷ Id (Univ rF ⁰) (wk ρ F₁) (wk ρ F) ^ [ % , ι ¹ ])
         → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk ρ F₁) (wk ρ F) e x ≡ cast ⁰ (wk ρ F₁) (wk ρ F) e′ y ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
  where
    b = λ ρ e x → cast ⁰ (wk ρ F₁) (wk ρ F) (Idsym (Univ rF ⁰) (wk ρ F) (wk ρ F₁) e) x

    [b] : ∀ {ρ Δ e x} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
        → (Δ ⊢ e ∷ Id (Univ rF ⁰) (wk ρ F) (wk ρ F₁) ^ [ % , ι ¹ ])
        → (Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
        → Δ ⊩⟨ ι ⁰ ⟩ b ρ e x ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ
    [b] [ρ] ⊢Δ ⊢e [x] =
      let
        ⊢e′ = Idsymⱼ (univ 0<1 ⊢Δ) (un-univ (escape ([F] [ρ] ⊢Δ)))
                     (un-univ (escape ([F₁] [ρ] ⊢Δ))) ⊢e
      in recursor [ρ] ⊢Δ [x] ⊢e′

    [bext] : ∀ {ρ Δ e e′ x y} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
        → (Δ ⊢ e ∷ Id (Univ rF ⁰) (wk ρ F) (wk ρ F₁) ^ [ % , ι ¹ ])
        → (Δ ⊢ e′ ∷ Id (Univ rF ⁰) (wk ρ F) (wk ρ F₁) ^ [ % , ι ¹ ])
        → (Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
        → (Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
        → (Δ ⊩⟨ ι ⁰ ⟩ x ≡ y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
        → Δ ⊩⟨ ι ⁰ ⟩ b ρ e x ≡ b ρ e′ y ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ
    [bext] [ρ] ⊢Δ ⊢e ⊢e′ [x] [y] [x≡y] =
      let
        ⊢syme = Idsymⱼ (univ 0<1 ⊢Δ) (un-univ (escape ([F] [ρ] ⊢Δ)))
          (un-univ (escape ([F₁] [ρ] ⊢Δ))) ⊢e
        ⊢syme′ = Idsymⱼ (univ 0<1 ⊢Δ) (un-univ (escape ([F] [ρ] ⊢Δ)))
          (un-univ (escape ([F₁] [ρ] ⊢Δ))) ⊢e′
      in extrecursor [ρ] ⊢Δ [x] [y] [x≡y] ⊢syme ⊢syme′

module cast-ΠΠ-lemmas-2
       {t e f Γ A B F rF G F₁ G₁}
       (⊢Γ : ⊢ Γ)
       (⊢A : Γ ⊢ A ^ [ ! , ι ⁰ ])
       (⊢ΠFG : Γ ⊢ Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (D : Γ ⊢ A ⇒* Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (⊢F : Γ ⊢ F ^ [ rF , ι ⁰ ])
       (⊢G : (Γ ∙ F ^ [ rF , ι ⁰ ]) ⊢ G ^ [ ! , ι ⁰ ])
       (A≡A : Γ ⊢ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) ≅ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) ^ [ ! , ι ⁰ ])
       ([F] : ∀ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Δ ⊩⟨ ι ⁰ ⟩ wk ρ F ^ [ rF , ι ⁰ ])
       ([G] : ∀ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F ^ [ rF , ι ⁰ ] / ([F] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G [ a ] ^ [ ! , ι ⁰ ]))
       (G-ext : ∀ {ρ} {Δ} {a} {b} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F ^ [ rF , ι ⁰ ] / ([F] [ρ] ⊢Δ))
          ([b] : Δ ⊩⟨ ι ⁰ ⟩ b ∷  wk ρ F ^ [ rF , ι ⁰ ] / ([F] [ρ] ⊢Δ))
          ([a≡b] : Δ ⊩⟨ ι ⁰ ⟩ a ≡ b ∷ wk ρ F ^ [ rF , ι ⁰ ] / ([F] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G [ a ] ≡ wk (lift ρ) G [ b ] ^ [ ! , ι ⁰ ] / ([G] [ρ] ⊢Δ [a])))
       (⊢B     : Γ ⊢ B ^ [ ! , ι ⁰ ])
       (⊢ΠF₁G₁ : Γ ⊢ Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (D₁     : Γ ⊢ B ⇒* Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (⊢F₁    : Γ ⊢ F₁ ^ [ rF , ι ⁰ ])
       (⊢G₁    : (Γ ∙ F₁ ^ [ rF , ι ⁰ ]) ⊢ G₁ ^ [ ! , ι ⁰ ])
       (A₁≡A₁  : Γ ⊢ (Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰) ≅ (Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰) ^ [ ! , ι ⁰ ])
       ([F₁] : ∀ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Δ ⊩⟨ ι ⁰ ⟩ wk ρ F₁ ^ [ rF , ι ⁰ ])
       ([G₁] : ∀ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F₁ ^ [ rF , ι ⁰ ] / ([F₁] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₁ [ a ] ^ [ ! , ι ⁰ ]))
       (G₁-ext : ∀ {ρ} {Δ} {a} {b} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F₁ ^ [ rF , ι ⁰ ] / ([F₁] [ρ] ⊢Δ))
          ([b] : Δ ⊩⟨ ι ⁰ ⟩ b ∷  wk ρ F₁ ^ [ rF , ι ⁰ ] / ([F₁] [ρ] ⊢Δ))
          ([a≡b] : Δ ⊩⟨ ι ⁰ ⟩ a ≡ b ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / ([F₁] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₁ [ a ] ≡ wk (lift ρ) G₁ [ b ] ^ [ ! , ι ⁰ ] / ([G₁] [ρ] ⊢Δ [a])))
       (⊢e : Γ ⊢ e ∷ Id (U ⁰) A B ^ [ % , ι ¹ ])
       (recursor : ∀ {ρ Δ x y t e}
          ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
          ([y] : Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
          ([t] : Δ ⊩⟨ ι ⁰ ⟩ t ∷ wk (lift ρ) G [ x ] ^ [ ! , ι ⁰ ] / [G] [ρ] ⊢Δ [x])
          (⊢e : Δ ⊢ e ∷ Id (U ⁰) (wk (lift ρ) G [ x ]) (wk (lift ρ) G₁ [ y ]) ^ [ % , ι ¹ ])
          → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk (lift ρ) G [ x ]) (wk (lift ρ) G₁ [ y ]) e t ∷ wk (lift ρ) G₁ [ y ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [y])
       (extrecursor : ∀ {ρ Δ x x′ y y′ t t′ e e′}
         → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
         → ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
         → ([x′] : Δ ⊩⟨ ι ⁰ ⟩ x′ ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
         → ([x≡x′] : Δ ⊩⟨ ι ⁰ ⟩ x ≡ x′ ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
         → ([y] : Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
         → ([y′] : Δ ⊩⟨ ι ⁰ ⟩ y′ ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
         → ([y≡y′] : Δ ⊩⟨ ι ⁰ ⟩ y ≡ y′ ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
         → ([t] : Δ ⊩⟨ ι ⁰ ⟩ t ∷ wk (lift ρ) G [ x ] ^ [ ! , ι ⁰ ] / [G] [ρ] ⊢Δ [x])
         → ([t′] : Δ ⊩⟨ ι ⁰ ⟩ t′ ∷ wk (lift ρ) G [ x′ ] ^ [ ! , ι ⁰ ] / [G] [ρ] ⊢Δ [x′])
         → ([t≡t′] : Δ ⊩⟨ ι ⁰ ⟩ t ≡ t′ ∷ wk (lift ρ) G [ x ] ^ [ ! , ι ⁰ ] / [G] [ρ] ⊢Δ [x])
         → (⊢e : Δ ⊢ e ∷ Id (U ⁰) (wk (lift ρ) G [ x ]) (wk (lift ρ) G₁ [ y ]) ^ [ % , ι ¹ ])
         → (⊢e′ : Δ ⊢ e′ ∷ Id (U ⁰) (wk (lift ρ) G [ x′ ]) (wk (lift ρ) G₁ [ y′ ]) ^ [ % , ι ¹ ])
         → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk (lift ρ) G [ x ]) (wk (lift ρ) G₁ [ y ]) e t ≡ cast ⁰ (wk (lift ρ) G [ x′ ]) (wk (lift ρ) G₁ [ y′ ]) e′ t′ ∷ wk (lift ρ) G₁ [ y ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [y])
       (⊢t : Γ ⊢ t ∷ Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (Df : Γ ⊢ t ⇒* f ∷ Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰ ^ ι ⁰)
       ([fext] : ∀ {ρ Δ a b} →
                ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
                ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
                ([b] : Δ ⊩⟨ ι ⁰ ⟩ b ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
                ([a≡b] : Δ ⊩⟨ ι ⁰ ⟩ a ≡ b ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
              → Δ ⊩⟨ ι ⁰ ⟩ wk ρ f ∘ a ^ ⁰ ≡ wk ρ f ∘ b ^ ⁰ ∷ wk (lift ρ) G [ a ] ^ [ ! , ι ⁰ ] / [G] [ρ] ⊢Δ [a])
       ([f] : ∀ {ρ Δ a}
              → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
              → ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
              → Δ ⊩⟨ ι ⁰ ⟩ wk ρ f ∘ a ^ ⁰ ∷ wk (lift ρ) G [ a ] ^ [ ! , ι ⁰ ] / [G] [ρ] ⊢Δ [a])
       ([b] : ∀ {ρ Δ e x}
                ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
                (⊢e : Δ ⊢ e ∷ Id (Univ rF ⁰) (wk ρ F) (wk ρ F₁) ^ [ % , ι ¹ ])
                ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
                → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk ρ F₁) (wk ρ F) (Idsym (Univ rF ⁰) (wk ρ F) (wk ρ F₁) e) x ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
       ([bext] : ∀ {ρ Δ e e′ x y} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
           → (Δ ⊢ e ∷ Id (Univ rF ⁰) (wk ρ F) (wk ρ F₁) ^ [ % , ι ¹ ])
           → (Δ ⊢ e′ ∷ Id (Univ rF ⁰) (wk ρ F) (wk ρ F₁) ^ [ % , ι ¹ ])
           → (Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
           → (Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
           → (Δ ⊩⟨ ι ⁰ ⟩ x ≡ y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
           → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk ρ F₁) (wk ρ F) (Idsym (Univ rF ⁰) (wk ρ F) (wk ρ F₁) e) x
             ≡ cast ⁰ (wk ρ F₁) (wk ρ F) (Idsym (Univ rF ⁰) (wk ρ F) (wk ρ F₁) e′) y ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
  where
    b = λ ρ e x → cast ⁰ (wk ρ F₁) (wk ρ F) (Idsym (Univ rF ⁰) (wk ρ F) (wk ρ F₁) e) x

    ⊢IdFF₁ : Γ ⊢ Id (Univ rF ⁰) F F₁ ^ [ % , ι ¹ ]
    ⊢IdFF₁ = univ (Idⱼ (univ 0<1 ⊢Γ) (un-univ ⊢F) (un-univ ⊢F₁))

    Δ₀ = Γ ∙ Id (Univ rF ⁰) F F₁ ^ [ % , ι ¹ ] ∙ wk1 F₁ ^ [ rF , ι ⁰ ]
    ρ₀ = (step (step id))

    ⊢IdG₁G : Γ ∙ Id (Univ rF ⁰) F F₁ ^ [ % , ι ¹ ] ⊢ Π (wk1 F₁) ^ rF ° ⁰ ▹ Id (U ⁰) ((wk1d G) [ b ρ₀ (var 1) (var 0) ]↑) (wk1d G₁) ° ¹ ° ¹ ^ [ % , ι ¹ ]
    ⊢IdG₁G =
      let
        ⊢Δ₀ : ⊢ Δ₀
        ⊢Δ₀ = ⊢Γ ∙ ⊢IdFF₁ ∙ univ (Twk.wkTerm (Twk.step Twk.id) (⊢Γ ∙ ⊢IdFF₁) (un-univ ⊢F₁))
        [ρ₀] : ρ₀ Twk.∷ Δ₀ ⊆ Γ
        [ρ₀] = Twk.step (Twk.step Twk.id)
        [0] : Δ₀ ⊩⟨ ι ⁰ ⟩ var 0 ∷ wk ρ₀ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ₀] ⊢Δ₀
        [0] = let x = (var ⊢Δ₀ (PE.subst (λ X → 0 ∷ X ^ [ rF , ι ⁰ ] ∈ Δ₀) (wk1-wk (step id) F₁) here)) in
          neuTerm ([F₁] [ρ₀] ⊢Δ₀) (var 0) x (~-var x)
        ⊢1 : Δ₀ ⊢ (var 1) ∷ Id (Univ rF ⁰) (wk ρ₀ F) (wk ρ₀ F₁) ^ [ % , ι ¹ ]
        ⊢1 = var ⊢Δ₀ (PE.subst₂ (λ X Y → 1 ∷ Id (Univ rF ⁰) X Y ^ [ % , ι ¹ ] ∈ Δ₀)
          (wk1-wk (step id) F) (wk1-wk (step id) F₁) (there here))
        ⊢G₀ : Δ₀ ⊢ wk (lift ρ₀) G [ b ρ₀ (var 1) (var 0) ] ^ [ ! , ι ⁰ ]
        ⊢G₀ = escape ([G] [ρ₀] ⊢Δ₀ ([b] [ρ₀] ⊢Δ₀ ⊢1 [0]))
        ⊢G₀′ = PE.subst (λ X → Δ₀ ⊢ X ^ [ ! , ι ⁰ ]) (PE.sym (cast-subst-lemma2 G (b ρ₀ (var 1) (var 0)))) ⊢G₀
        x₀ : Δ₀ ⊢ Id (U ⁰) ((wk1d G) [ b ρ₀ (var 1) (var 0) ]↑) (wk1d G₁) ∷ SProp ¹ ^ [ ! , ∞ ]
        x₀ = Idⱼ (univ 0<1 ⊢Δ₀) (un-univ ⊢G₀′)
            (un-univ (Twk.wk (Twk.lift (Twk.step Twk.id)) ⊢Δ₀ ⊢G₁))
        x₁ = Πⱼ <is≤ 0<1 ▹ ≡is≤ PE.refl ▹ Twk.wkTerm (Twk.step Twk.id) (⊢Γ ∙ ⊢IdFF₁) (un-univ ⊢F₁) ▹ x₀
      in univ x₁

    ⊢e′ : Γ ⊢ e ∷ ∃ (Id (Univ rF ⁰) F F₁) ▹ (Π (wk1 F₁) ^ rF ° ⁰ ▹ Id (U ⁰) ((wk1d G) [ b ρ₀ (var 1) (var 0) ]↑) (wk1d G₁) ° ¹ ° ¹) ^ [ % , ι ¹ ]
    ⊢e′ =
      let
        b₀ = cast ⁰ (wk1 (wk1 F₁)) (wk1 (wk1 F)) (Idsym (Univ rF ⁰) (wk1 (wk1 F)) (wk1 (wk1 F₁)) (var 1)) (var 0)
        b≡b₀ : b ρ₀ (var 1) (var 0) PE.≡ b₀
        b≡b₀ = PE.cong₂ (λ X Y → cast ⁰ Y X (Idsym (Univ rF ⁰) X Y (var 1)) (var 0))
          (PE.sym (wk1-wk (step id) F)) (PE.sym (wk1-wk (step id) F₁))
        x₀ = conv ⊢e (univ (Id-cong (refl (univ 0<1 ⊢Γ)) (un-univ≡ (subset* D)) (un-univ≡ (subset* D₁))))
        x₁ = conv x₀ (univ (Id-U-ΠΠ (un-univ ⊢F) (un-univ ⊢G) (un-univ ⊢F₁) (un-univ ⊢G₁)))
        x₂ = PE.subst (λ X → Γ ⊢ e ∷ ∃ (Id (Univ rF ⁰) F F₁) ▹ (Π (wk1 F₁) ^ rF ° ⁰ ▹ Id (U ⁰) ((wk1d G) [ X ]↑) (wk1d G₁) ° ¹ ° ¹) ^ [ % , ι ¹ ]) (PE.sym b≡b₀) x₁
      in x₂

    ⊢fste : Γ ⊢ fst e ∷ Id (Univ rF ⁰) F F₁ ^ [ % , ι ¹ ]
    ⊢fste = fstⱼ (un-univ ⊢IdFF₁) (un-univ ⊢IdG₁G) ⊢e′

    ⊢snde : Γ ⊢ snd e ∷ Π F₁ ^ rF ° ⁰ ▹ Id (U ⁰) (wk1d G [ b (step id) (fst (wk1 e)) (var 0) ]) G₁ ° ¹ ° ¹ ^ [ % , ι ¹ ]
    ⊢snde =
      let
        x₀ = sndⱼ (un-univ ⊢IdFF₁) (un-univ ⊢IdG₁G) ⊢e′
        x₁ = PE.subst₂ (λ X Y → Γ ⊢ snd e ∷ (Π X ^ rF ° ⁰ ▹ subst _ (Id (U ⁰) Y (wk1d G₁)) ° ¹ ° ¹) ^ [ % , ι ¹ ])
            (wk1-singleSubst F₁ (fst e)) (cast-subst-lemma2 G (b ρ₀ (var 1) (var 0))) x₀
        x₂ = PE.subst₂ (λ X Y → Γ ⊢ snd e ∷ Π F₁ ^ rF ° ⁰ ▹ Id (U ⁰) X Y ° ¹ ° ¹ ^ [ % , ι ¹ ])
          (singleSubstLift (wk (lift ρ₀) G) (b ρ₀ (var 1) (var 0))) (wk1d-singleSubst G₁ (fst e)) x₁
        σ = liftSubst (sgSubst (fst e))
        b≡b : subst σ (b ρ₀ (var 1) (var 0)) PE.≡ b (step id) (fst (wk1 e)) (var 0)
        b≡b = PE.trans (PE.cong (λ X → cast ⁰ (subst σ (wk ρ₀ F₁)) (subst σ (wk ρ₀ F)) X (var 0)) (subst-Idsym σ (Univ rF ⁰) (wk ρ₀ F) (wk ρ₀ F₁) (var 1)))
          (PE.cong₂ (λ X Y → cast ⁰ Y X (Idsym (Univ rF ⁰) X Y (fst (wk1 e))) (var 0)) (cast-subst-lemma5 F (fst e)) (cast-subst-lemma5 F₁ (fst e)))
        x₃ = PE.subst₂ (λ X Y → Γ ⊢ snd e ∷ Π F₁ ^ rF ° ⁰ ▹ Id (U ⁰) (X [ Y ]) G₁ ° ¹ ° ¹ ^ [ % , ι ¹ ])
          (cast-subst-lemma3 G (fst e)) b≡b x₂
     in x₃

    ⊢snde′ : ∀ {ρ Δ x} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
        → (⊢x : Δ ⊢ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ])
        → Δ ⊢ snd (wk ρ e) ∘ x ^ ¹ ∷ Id (U ⁰) (wk (lift ρ) G [ b ρ (fst (wk ρ e)) x ])
          (wk (lift ρ) G₁ [ x ]) ^ [ % , ι ¹ ]
    ⊢snde′ {ρ} {Δ} {x} [ρ] ⊢Δ ⊢x =
      let
        -- I should probably make some generic lemma about pushing weakening and subst in b
        y₀ = PE.trans (PE.cong (λ X → X [ x ]) (wk-Idsym (lift ρ) (Univ rF ⁰) (wk1 F) (wk1 F₁) (fst (wk1 e))))
          (PE.trans (subst-Idsym (sgSubst x) (Univ rF ⁰) (wk (lift ρ) (wk1 F)) (wk (lift ρ) (wk1 F₁)) (fst (wk (lift ρ) (wk1 e))))
          (PE.cong₃ (λ X Y Z → Idsym (Univ rF ⁰) X Y (fst Z)) (irrelevant-subst′ ρ F x) (irrelevant-subst′ ρ F₁ x) (irrelevant-subst′ ρ e x)))
        y₁ : wk (lift ρ) (b (step id) (fst (wk1 e)) (var 0)) [ x ] PE.≡ b ρ (fst (wk ρ e)) x
        y₁ = PE.cong₃ (λ X Y Z → cast ⁰ X Y Z x) (irrelevant-subst′ ρ F₁ x) (irrelevant-subst′ ρ F x) y₀
        x₀ : Δ ⊢ (wk ρ (snd e)) ∘ x ^ ¹ ∷ Id (U ⁰) (wk (lift ρ) (wk1d G [ b (step id) (fst (wk1 e)) (var 0) ]) [ x ]) (wk (lift ρ) G₁ [ x ]) ^ [ % , ι ¹ ]
        x₀ = Twk.wkTerm [ρ] ⊢Δ ⊢snde ∘ⱼ ⊢x
        x₁ = PE.cong₂ (λ X Y → X [ Y ]) (cast-subst-lemma4 ρ x G) y₁
        x₂ = PE.trans (singleSubstLift (wk (lift (lift ρ)) (wk1d G))
          (wk (lift ρ) (b (step id) (fst (wk1 e)) (var 0)))) x₁
        x₃ = PE.trans (PE.cong (λ X → X [ x ]) (wk-β {a = b (step id) (fst (wk1 e)) (var 0)} (wk1d G))) x₂
        x₄ = PE.subst (λ X → Δ ⊢ snd (wk ρ e) ∘ x ^ ¹ ∷ Id (U ⁰) X (wk (lift ρ) G₁ [ x ]) ^ [ % , ι ¹ ]) x₃ x₀
      in x₄

    g = λ ρ x → cast ⁰ (wk (lift ρ) G [ b ρ (fst (wk ρ e)) x ]) (wk (lift ρ) G₁ [ x ])
      ((snd (wk ρ e)) ∘ x ^ ¹) ((wk ρ t) ∘ (b ρ (fst (wk ρ e)) x) ^ ⁰)

    [g] : ∀ {ρ Δ x} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
        → ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
        → Δ ⊩⟨ ι ⁰ ⟩ g ρ x ∷ wk (lift ρ) G₁ [ x ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [x]
    [g] {ρ} {Δ} {x} [ρ] ⊢Δ [x] =
      let
        [b]′ = [b] [ρ] ⊢Δ (Twk.wkTerm [ρ] ⊢Δ ⊢fste) [x]
        [t] = proj₁ (redSubst*Term (appRed* (escapeTerm ([F] [ρ] ⊢Δ) [b]′) (Twk.wkRed*Term [ρ] ⊢Δ Df))
          ([G] [ρ] ⊢Δ [b]′) ([f] [ρ] ⊢Δ [b]′))
      in recursor [ρ] ⊢Δ [b]′ [x] [t] (⊢snde′ [ρ] ⊢Δ (escapeTerm ([F₁] [ρ] ⊢Δ) [x]))

    [gext] : ∀ {ρ Δ x y} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
        → ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
        → ([y] : Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
        → ([x≡y] : Δ ⊩⟨ ι ⁰ ⟩ x ≡ y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
        → Δ ⊩⟨ ι ⁰ ⟩ g ρ x ≡ g ρ y ∷ wk (lift ρ) G₁ [ x ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [x]
    [gext] {ρ} {Δ} {x} {y} [ρ] ⊢Δ [x] [y] [x≡y] =
      let
        [b₁] = [b] [ρ] ⊢Δ (Twk.wkTerm [ρ] ⊢Δ ⊢fste) [x]
        [b₂] = [b] [ρ] ⊢Δ (Twk.wkTerm [ρ] ⊢Δ ⊢fste) [y]
        [b₁≡b₂] = [bext] [ρ] ⊢Δ (Twk.wkTerm [ρ] ⊢Δ ⊢fste) (Twk.wkTerm [ρ] ⊢Δ ⊢fste) [x] [y] [x≡y]
        D₁ = (appRed* (escapeTerm ([F] [ρ] ⊢Δ) [b₁]) (Twk.wkRed*Term [ρ] ⊢Δ Df))
        D₂ = (appRed* (escapeTerm ([F] [ρ] ⊢Δ) [b₂]) (Twk.wkRed*Term [ρ] ⊢Δ Df))
        [t₁] = proj₁ (redSubst*Term D₁ ([G] [ρ] ⊢Δ [b₁]) ([f] [ρ] ⊢Δ [b₁]))
        [t₂] = proj₁ (redSubst*Term D₂ ([G] [ρ] ⊢Δ [b₂]) ([f] [ρ] ⊢Δ [b₂]))
        [t₁≡t₂] = redSubst*EqTerm D₁ D₂ ([G] [ρ] ⊢Δ [b₁]) ([G] [ρ] ⊢Δ [b₂]) (G-ext [ρ] ⊢Δ [b₁] [b₂] [b₁≡b₂])
          ([f] [ρ] ⊢Δ [b₁]) ([f] [ρ] ⊢Δ [b₂]) ([fext] [ρ] ⊢Δ [b₁] [b₂] [b₁≡b₂])
      in extrecursor [ρ] ⊢Δ [b₁] [b₂] [b₁≡b₂] [x] [y] [x≡y] [t₁] [t₂] [t₁≡t₂] (⊢snde′ [ρ] ⊢Δ (escapeTerm ([F₁] [ρ] ⊢Δ) [x])) (⊢snde′ [ρ] ⊢Δ (escapeTerm ([F₁] [ρ] ⊢Δ) [y]))

    Δ₁ = Γ ∙ F₁ ^ [ rF , ι ⁰ ]
    ⊢Δ₁ : ⊢ Δ₁
    ⊢Δ₁ = ⊢Γ ∙ ⊢F₁
    ρ₁ = (step id)
    [ρ₁] : ρ₁ Twk.∷ Δ₁ ⊆ Γ
    [ρ₁] = Twk.step Twk.id
    [0] : Δ₁ ⊩⟨ ι ⁰ ⟩ var 0 ∷ wk ρ₁ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ₁] ⊢Δ₁
    [0] = neuTerm ([F₁] [ρ₁] ⊢Δ₁) (var 0) (var ⊢Δ₁ here) (~-var (var ⊢Δ₁ here))

    ⊢g0 = PE.subst (λ X → Δ₁ ⊢ g (step id) (var 0) ∷ X ^ [ ! , ι ⁰ ]) (wkSingleSubstId G₁) (escapeTerm ([G₁] [ρ₁] ⊢Δ₁ [0]) ([g] [ρ₁] ⊢Δ₁ [0]))
    ⊢λg : Γ ⊢ lam F₁ ▹ g (step id) (var 0) ^ ⁰ ∷ Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ]
    ⊢λg = lamⱼ (≡is≤ PE.refl) (≡is≤ PE.refl) ⊢F₁ ⊢g0

    Dg : Γ ⊢ cast ⁰ A B e t :⇒*: (lam F₁ ▹ g (step id) (var 0) ^ ⁰) ∷ Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰ ^ ι ⁰
    Dg =
      let
        g0 = lam F₁ ▹ cast ⁰ (G [ b (step id) (fst (wk1 e)) (var 0) ]↑) G₁
          ((snd (wk1 e)) ∘ (var 0) ^ ¹) ((wk1 t) ∘ (b (step id) (fst (wk1 e)) (var 0)) ^ ⁰) ^ ⁰
        g≡g : g0 PE.≡ lam F₁ ▹ g (step id) (var 0) ^ ⁰
        g≡g = PE.cong₂ (λ X Y → lam F₁ ▹ cast ⁰ X Y ((snd (wk1 e)) ∘ (var 0) ^ ¹) ((wk1 t) ∘ (b (step id) (fst (wk1 e)) (var 0)) ^ ⁰) ^ ⁰)
          (wk1d[]-[]↑ G (b (step id) (fst (wk1 e)) (var 0))) (PE.sym (wkSingleSubstId G₁))
        ⊢e′ = conv ⊢e (univ (Id-cong (refl (univ 0<1 ⊢Γ))
          (un-univ≡ (subset* D)) (refl (un-univ ⊢B))))
        ⊢e″ = conv ⊢e (univ (Id-cong (refl (univ 0<1 ⊢Γ))
          (un-univ≡ (subset* D)) (un-univ≡ (subset* D₁))))
      in [[ conv (castⱼ (un-univ ⊢A) (un-univ ⊢B) ⊢e (conv ⊢t (sym (subset* D)))) (subset* D₁)
         , ⊢λg
         , (conv* (CastRed*Term′ ⊢B ⊢e (conv ⊢t (sym (subset* D))) D
           ⇨∷* castΠRed* ⊢F ⊢G ⊢e′ ⊢t D₁) (subset* D₁))
           ⇨∷* (PE.subst (λ X → Γ ⊢ cast ⁰ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) (Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰) e t ⇒ X ∷ Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰ ^ ι ⁰) g≡g
           (cast-Π (un-univ ⊢F) (un-univ ⊢G) (un-univ ⊢F₁) (un-univ ⊢G₁) ⊢e″ ⊢t) ⇨ (id ⊢λg)) ]]

    g≡g : Γ ⊢ (lam F₁ ▹ g (step id) (var 0) ^ ⁰) ≅ (lam F₁ ▹ g (step id) (var 0) ^ ⁰) ∷ Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ]
    g≡g =
      let
        ⊢F₁′ = Twk.wk (Twk.step Twk.id) ⊢Δ₁ ⊢F₁
        ⊢g0 = escapeTerm ([G₁] [ρ₁] ⊢Δ₁ [0]) ([g] [ρ₁] ⊢Δ₁ [0])
        ⊢g0′ = (PE.subst (λ X → Δ₁ ⊢ g (step id) (var 0) ∷ X ^ [ ! , ι ⁰ ]) (wkSingleSubstId G₁) ⊢g0)
        ⊢g0″ = Twk.wkTerm (Twk.lift (Twk.step Twk.id)) (⊢Δ₁ ∙ ⊢F₁′) ⊢g0′
        D : Δ₁ ⊢ (lam (wk1 F₁) ▹ wk1d (g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ⇒* g (step id) (var 0) ∷ wk1d G₁ [ var 0 ] ^ ι ⁰
        D = PE.subst (λ X → Δ₁ ⊢ (lam (wk1 F₁) ▹ wk1d (g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ⇒ X ∷ wk1d G₁ [ var 0 ] ^ ι ⁰) (wkSingleSubstId (g (step id) (var 0)))
          (β-red (≡is≤ PE.refl) (≡is≤ PE.refl) ⊢F₁′ ⊢g0″ (var ⊢Δ₁ here))
          ⇨ id ⊢g0
        [g0] : Δ₁ ⊩⟨ ι ⁰ ⟩ (lam (wk1 F₁) ▹ wk1d (g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ∷ wk1d G₁ [ var 0 ] ^ [ ! , ι ⁰ ] / [G₁] [ρ₁] ⊢Δ₁ [0]
        [g0] = proj₁ (redSubst*Term D ([G₁] [ρ₁] ⊢Δ₁ [0]) ([g] [ρ₁] ⊢Δ₁ [0]))
        x₀ = escapeEqReflTerm ([G₁] [ρ₁] ⊢Δ₁ [0]) [g0]
        x₁ = PE.subst (λ X → Δ₁ ⊢ (lam (wk1 F₁) ▹ wk1d (g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ≅ (lam (wk1 F₁) ▹ wk1d (g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ∷ X ^ [ ! , ι ⁰ ]) (wkSingleSubstId G₁) x₀
      in ≅-η-eq (≡is≤ PE.refl) (≡is≤ PE.refl) ⊢F₁ ⊢λg ⊢λg lamₙ lamₙ x₁

    g∘a≡ga : ∀ {ρ Δ a}
      → ([ρ] : ρ Twk.∷ Δ ⊆ Γ)
      → (⊢Δ : ⊢ Δ)
      → ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
      → Δ ⊢ wk ρ (lam F₁ ▹ g (step id) (var 0) ^ ⁰) ∘ a ^ ⁰ ⇒* g ρ a ∷ wk (lift ρ) G₁ [ a ] ^ ι ⁰
    g∘a≡ga {ρ} {Δ} {a} [ρ] ⊢Δ [a] =
      let
        ⊢F₁′ = (Twk.wk [ρ] ⊢Δ ⊢F₁)
        -- this lemma is already in ⊢snde′. maybe refactor?
        x₀ : wk (lift ρ) (b (step id) (fst (wk1 e)) (var 0)) [ a ] PE.≡ b ρ (fst (wk ρ e)) a
        x₀ = PE.trans
          (PE.cong (λ X → cast ⁰ (wk (lift ρ) (wk1 F₁) [ a ]) (wk (lift ρ) (wk1 F) [ a ]) X a)
            (PE.trans (PE.cong (λ X → X [ a ]) (wk-Idsym (lift ρ) (Univ rF ⁰) (wk1 F) (wk1 F₁) (fst (wk1 e))))
              (subst-Idsym (sgSubst a) (Univ rF ⁰) (wk (lift ρ) (wk1 F)) (wk (lift ρ) (wk1 F₁)) (fst (wk (lift ρ) (wk1 e))))))
          (PE.cong₃ (λ X Y Z → cast ⁰ Y X (Idsym (Univ rF ⁰) X Y (fst Z)) a) (irrelevant-subst′ ρ F a) (irrelevant-subst′ ρ F₁ a) (irrelevant-subst′ ρ e a))
        x₁ : wk (lift ρ) (g (step id) (var 0)) [ a ] PE.≡ g ρ a
        x₁ = PE.cong₄ (λ X Y Z T → cast ⁰ X Y Z T)
          (PE.trans (cast-subst-lemma6 ρ G _ a) (PE.cong (λ X → wk (lift ρ) G [ X ]) x₀))
          (PE.cong (λ X → wk (lift ρ) X [ a ]) (wkSingleSubstId G₁))
          (PE.cong (λ X → snd X ∘ a ^ ¹) (irrelevant-subst′ ρ e a))
          (PE.cong₂ (λ X Y → X ∘ Y ^ ⁰) (irrelevant-subst′ ρ t a) x₀)
        x₂ : Δ ∙ (wk ρ F₁) ^ [ rF , ι ⁰ ] ⊢  wk (lift ρ) (g (step id) (var 0)) ∷ wk (lift ρ) G₁ ^ [ ! , ι ⁰ ]
        x₂ = Twk.wkTerm (Twk.lift [ρ]) (⊢Δ ∙ ⊢F₁′) ⊢g0
      in PE.subst (λ X → Δ ⊢ wk ρ (lam F₁ ▹ g (step id) (var 0) ^ ⁰) ∘ a ^ ⁰ ⇒ X ∷ wk (lift ρ) G₁ [ a ] ^ ι ⁰) x₁
        (β-red (≡is≤ PE.refl) (≡is≤ PE.refl) ⊢F₁′ x₂ (escapeTerm ([F₁] [ρ] ⊢Δ) [a]))
        ⇨ id (escapeTerm ([G₁] [ρ] ⊢Δ [a]) ([g] [ρ] ⊢Δ [a]))

    [castΠΠ] : Γ ⊩⟨ ι ⁰ ⟩ cast ⁰ A B e t ∷ B ^ [ ! , ι ⁰ ] / (Πᵣ′ rF ⁰ ⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢B , ⊢ΠF₁G₁ , D₁ ]] ⊢F₁ ⊢G₁ A₁≡A₁ [F₁] [G₁] G₁-ext)
    [castΠΠ] = ((lam F₁ ▹ g (step id) (var 0) ^ ⁰) , Dg , lamₙ , g≡g
        , (λ [ρ] ⊢Δ [a] [a′] [a≡a′] → redSubst*EqTerm (g∘a≡ga [ρ] ⊢Δ [a]) (g∘a≡ga [ρ] ⊢Δ [a′])
             ([G₁] [ρ] ⊢Δ [a]) ([G₁] [ρ] ⊢Δ [a′]) (G₁-ext [ρ] ⊢Δ [a] [a′] [a≡a′])
             ([g] [ρ] ⊢Δ [a]) ([g] [ρ] ⊢Δ [a′]) ([gext] [ρ] ⊢Δ [a] [a′] [a≡a′]))
        , (λ [ρ] ⊢Δ [a] → proj₁ (redSubst*Term (g∘a≡ga [ρ] ⊢Δ [a]) ([G₁] [ρ] ⊢Δ [a]) ([g] [ρ] ⊢Δ [a]))))

module cast-ΠΠ-lemmas-3
       {Γ A₁ A₂ A₃ A₄ F₁ F₂ F₃ F₄ rF G₁ G₂ G₃ G₄ e₁₃ e₂₄ t₁ f₁ t₂ f₂}
       (⊢Γ : ⊢ Γ)

       (⊢A₁ : Γ ⊢ A₁ ^ [ ! , ι ⁰ ])
       (⊢ΠF₁G₁ : Γ ⊢ Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (D₁     : Γ ⊢ A₁ ⇒* Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (⊢F₁    : Γ ⊢ F₁ ^ [ rF , ι ⁰ ])
       (⊢G₁    : (Γ ∙ F₁ ^ [ rF , ι ⁰ ]) ⊢ G₁ ^ [ ! , ι ⁰ ])
       (A₁≡A₁  : Γ ⊢ (Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰) ≅ (Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰) ^ [ ! , ι ⁰ ])
       ([F₁] : ∀ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Δ ⊩⟨ ι ⁰ ⟩ wk ρ F₁ ^ [ rF , ι ⁰ ])
       ([G₁] : ∀ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F₁ ^ [ rF , ι ⁰ ] / ([F₁] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₁ [ a ] ^ [ ! , ι ⁰ ]))
       (G₁-ext : ∀ {ρ} {Δ} {a} {b} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F₁ ^ [ rF , ι ⁰ ] / ([F₁] [ρ] ⊢Δ))
          ([b] : Δ ⊩⟨ ι ⁰ ⟩ b ∷  wk ρ F₁ ^ [ rF , ι ⁰ ] / ([F₁] [ρ] ⊢Δ))
          ([a≡b] : Δ ⊩⟨ ι ⁰ ⟩ a ≡ b ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / ([F₁] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₁ [ a ] ≡ wk (lift ρ) G₁ [ b ] ^ [ ! , ι ⁰ ] / ([G₁] [ρ] ⊢Δ [a])))

       (⊢A₂ : Γ ⊢ A₂ ^ [ ! , ι ⁰ ])
       (⊢ΠF₂G₂ : Γ ⊢ Π F₂ ^ rF ° ⁰ ▹ G₂ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (D₂     : Γ ⊢ A₂ ⇒* Π F₂ ^ rF ° ⁰ ▹ G₂ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (⊢F₂    : Γ ⊢ F₂ ^ [ rF , ι ⁰ ])
       (⊢G₂    : (Γ ∙ F₂ ^ [ rF , ι ⁰ ]) ⊢ G₂ ^ [ ! , ι ⁰ ])
       (A₂≡A₂  : Γ ⊢ (Π F₂ ^ rF ° ⁰ ▹ G₂ ° ⁰ ° ⁰) ≅ (Π F₂ ^ rF ° ⁰ ▹ G₂ ° ⁰ ° ⁰) ^ [ ! , ι ⁰ ])
       ([F₂] : ∀ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Δ ⊩⟨ ι ⁰ ⟩ wk ρ F₂ ^ [ rF , ι ⁰ ])
       ([G₂] : ∀ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F₂ ^ [ rF , ι ⁰ ] / ([F₂] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₂ [ a ] ^ [ ! , ι ⁰ ]))
       (G₂-ext : ∀ {ρ} {Δ} {a} {b} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F₂ ^ [ rF , ι ⁰ ] / ([F₂] [ρ] ⊢Δ))
          ([b] : Δ ⊩⟨ ι ⁰ ⟩ b ∷  wk ρ F₂ ^ [ rF , ι ⁰ ] / ([F₂] [ρ] ⊢Δ))
          ([a≡b] : Δ ⊩⟨ ι ⁰ ⟩ a ≡ b ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / ([F₂] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₂ [ a ] ≡ wk (lift ρ) G₂ [ b ] ^ [ ! , ι ⁰ ] / ([G₂] [ρ] ⊢Δ [a])))

       (⊢A₃ : Γ ⊢ A₃ ^ [ ! , ι ⁰ ])
       (⊢ΠF₃G₃ : Γ ⊢ Π F₃ ^ rF ° ⁰ ▹ G₃ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (D₃     : Γ ⊢ A₃ ⇒* Π F₃ ^ rF ° ⁰ ▹ G₃ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (⊢F₃    : Γ ⊢ F₃ ^ [ rF , ι ⁰ ])
       (⊢G₃    : (Γ ∙ F₃ ^ [ rF , ι ⁰ ]) ⊢ G₃ ^ [ ! , ι ⁰ ])
       (A₃≡A₃  : Γ ⊢ (Π F₃ ^ rF ° ⁰ ▹ G₃ ° ⁰ ° ⁰) ≅ (Π F₃ ^ rF ° ⁰ ▹ G₃ ° ⁰ ° ⁰) ^ [ ! , ι ⁰ ])
       ([F₃] : ∀ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Δ ⊩⟨ ι ⁰ ⟩ wk ρ F₃ ^ [ rF , ι ⁰ ])
       ([G₃] : ∀ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F₃ ^ [ rF , ι ⁰ ] / ([F₃] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₃ [ a ] ^ [ ! , ι ⁰ ]))
       (G₃-ext : ∀ {ρ} {Δ} {a} {b} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F₃ ^ [ rF , ι ⁰ ] / ([F₃] [ρ] ⊢Δ))
          ([b] : Δ ⊩⟨ ι ⁰ ⟩ b ∷  wk ρ F₃ ^ [ rF , ι ⁰ ] / ([F₃] [ρ] ⊢Δ))
          ([a≡b] : Δ ⊩⟨ ι ⁰ ⟩ a ≡ b ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / ([F₃] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₃ [ a ] ≡ wk (lift ρ) G₃ [ b ] ^ [ ! , ι ⁰ ] / ([G₃] [ρ] ⊢Δ [a])))

       (⊢A₄ : Γ ⊢ A₄ ^ [ ! , ι ⁰ ])
       (⊢ΠF₄G₄ : Γ ⊢ Π F₄ ^ rF ° ⁰ ▹ G₄ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (D₄     : Γ ⊢ A₄ ⇒* Π F₄ ^ rF ° ⁰ ▹ G₄ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (⊢F₄    : Γ ⊢ F₄ ^ [ rF , ι ⁰ ])
       (⊢G₄    : (Γ ∙ F₄ ^ [ rF , ι ⁰ ]) ⊢ G₄ ^ [ ! , ι ⁰ ])
       (A₄≡A₄  : Γ ⊢ (Π F₄ ^ rF ° ⁰ ▹ G₄ ° ⁰ ° ⁰) ≅ (Π F₄ ^ rF ° ⁰ ▹ G₄ ° ⁰ ° ⁰) ^ [ ! , ι ⁰ ])
       ([F₄] : ∀ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Δ ⊩⟨ ι ⁰ ⟩ wk ρ F₄ ^ [ rF , ι ⁰ ])
       ([G₄] : ∀ {ρ} {Δ} {a} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F₄ ^ [ rF , ι ⁰ ] / ([F₄] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₄ [ a ] ^ [ ! , ι ⁰ ]))
       (G₄-ext : ∀ {ρ} {Δ} {a} {b} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷  wk ρ F₄ ^ [ rF , ι ⁰ ] / ([F₄] [ρ] ⊢Δ))
          ([b] : Δ ⊩⟨ ι ⁰ ⟩ b ∷  wk ρ F₄ ^ [ rF , ι ⁰ ] / ([F₄] [ρ] ⊢Δ))
          ([a≡b] : Δ ⊩⟨ ι ⁰ ⟩ a ≡ b ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / ([F₄] [ρ] ⊢Δ))
          → (Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₄ [ a ] ≡ wk (lift ρ) G₄ [ b ] ^ [ ! , ι ⁰ ] / ([G₄] [ρ] ⊢Δ [a])))

       (A₁≡A₂ : Γ ⊢ Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰ ≅ Π F₂ ^ rF ° ⁰ ▹ G₂ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (A₃≡A₄ : Γ ⊢ Π F₃ ^ rF ° ⁰ ▹ G₃ ° ⁰ ° ⁰ ≅ Π F₄ ^ rF ° ⁰ ▹ G₄ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       ([F₁≡F₂] : ∀ {ρ Δ} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Δ ⊩⟨ ι ⁰ ⟩ wk ρ F₁ ≡ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
       ([F₃≡F₄] : ∀ {ρ Δ} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Δ ⊩⟨ ι ⁰ ⟩ wk ρ F₃ ≡ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
       ([G₁≡G₂] : ∀ {ρ Δ a} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
                  → ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
                  → Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₁ [ a ] ≡ wk (lift ρ) G₂ [ a ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [a])
       ([G₃≡G₄] : ∀ {ρ Δ a} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
                  → ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
                  → Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₃ [ a ] ≡ wk (lift ρ) G₄ [ a ] ^ [ ! , ι ⁰ ] / [G₃] [ρ] ⊢Δ [a])

       (⊢e₁₃ : Γ ⊢ e₁₃ ∷ Id (U ⁰) A₁ A₃ ^ [ % , ι ¹ ])
       (⊢e₂₄ : Γ ⊢ e₂₄ ∷ Id (U ⁰) A₂ A₄ ^ [ % , ι ¹ ])

       (⊢t₁ : Γ ⊢ t₁ ∷ Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (Df₁ : Γ ⊢ t₁ ⇒* f₁ ∷ Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰ ^ ι ⁰)
       ([f₁ext] : ∀ {ρ Δ a b} →
                ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
                ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
                ([b] : Δ ⊩⟨ ι ⁰ ⟩ b ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
                ([a≡b] : Δ ⊩⟨ ι ⁰ ⟩ a ≡ b ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
              → Δ ⊩⟨ ι ⁰ ⟩ wk ρ f₁ ∘ a ^ ⁰ ≡ wk ρ f₁ ∘ b ^ ⁰ ∷ wk (lift ρ) G₁ [ a ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [a])
       ([f₁] : ∀ {ρ Δ a}
              → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
              → ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
              → Δ ⊩⟨ ι ⁰ ⟩ wk ρ f₁ ∘ a ^ ⁰ ∷ wk (lift ρ) G₁ [ a ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [a])

       (⊢t₂ : Γ ⊢ t₂ ∷ Π F₂ ^ rF ° ⁰ ▹ G₂ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ])
       (Df₂ : Γ ⊢ t₂ ⇒* f₂ ∷ Π F₂ ^ rF ° ⁰ ▹ G₂ ° ⁰ ° ⁰ ^ ι ⁰)
       ([f₂ext] : ∀ {ρ Δ a b} →
                ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
                ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
                ([b] : Δ ⊩⟨ ι ⁰ ⟩ b ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
                ([a≡b] : Δ ⊩⟨ ι ⁰ ⟩ a ≡ b ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
              → Δ ⊩⟨ ι ⁰ ⟩ wk ρ f₂ ∘ a ^ ⁰ ≡ wk ρ f₂ ∘ b ^ ⁰ ∷ wk (lift ρ) G₂ [ a ] ^ [ ! , ι ⁰ ] / [G₂] [ρ] ⊢Δ [a])
       ([f₂] : ∀ {ρ Δ a}
              → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
              → ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
              → Δ ⊩⟨ ι ⁰ ⟩ wk ρ f₂ ∘ a ^ ⁰ ∷ wk (lift ρ) G₂ [ a ] ^ [ ! , ι ⁰ ] / [G₂] [ρ] ⊢Δ [a])

       ([f₁≡f₂] : ∀ {ρ Δ a} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
          → Δ ⊩⟨ ι ⁰ ⟩ wk ρ f₁ ∘ a ^ ⁰ ≡ wk ρ f₂ ∘ a ^ ⁰ ∷ wk (lift ρ) G₁ [ a ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [a])

       (recursor₁ : ∀ {ρ Δ x y t e}
          ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
          ([y] : Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
          ([t] : Δ ⊩⟨ ι ⁰ ⟩ t ∷ wk (lift ρ) G₁ [ x ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [x])
          (⊢e : Δ ⊢ e ∷ Id (U ⁰) (wk (lift ρ) G₁ [ x ]) (wk (lift ρ) G₃ [ y ]) ^ [ % , ι ¹ ])
          → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk (lift ρ) G₁ [ x ]) (wk (lift ρ) G₃ [ y ]) e t ∷ wk (lift ρ) G₃ [ y ] ^ [ ! , ι ⁰ ] / [G₃] [ρ] ⊢Δ [y])
       (recursor₂ : ∀ {ρ Δ x y t e}
          ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
          ([y] : Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
          ([t] : Δ ⊩⟨ ι ⁰ ⟩ t ∷ wk (lift ρ) G₂ [ x ] ^ [ ! , ι ⁰ ] / [G₂] [ρ] ⊢Δ [x])
          (⊢e : Δ ⊢ e ∷ Id (U ⁰) (wk (lift ρ) G₂ [ x ]) (wk (lift ρ) G₄ [ y ]) ^ [ % , ι ¹ ])
          → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk (lift ρ) G₂ [ x ]) (wk (lift ρ) G₄ [ y ]) e t ∷ wk (lift ρ) G₄ [ y ] ^ [ ! , ι ⁰ ] / [G₄] [ρ] ⊢Δ [y])
       (extrecursor₁ : ∀ {ρ Δ x x′ y y′ t t′ e e′}
         → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
         → ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
         → ([x′] : Δ ⊩⟨ ι ⁰ ⟩ x′ ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
         → ([x≡x′] : Δ ⊩⟨ ι ⁰ ⟩ x ≡ x′ ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
         → ([y] : Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
         → ([y′] : Δ ⊩⟨ ι ⁰ ⟩ y′ ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
         → ([y≡y′] : Δ ⊩⟨ ι ⁰ ⟩ y ≡ y′ ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
         → ([t] : Δ ⊩⟨ ι ⁰ ⟩ t ∷ wk (lift ρ) G₁ [ x ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [x])
         → ([t′] : Δ ⊩⟨ ι ⁰ ⟩ t′ ∷ wk (lift ρ) G₁ [ x′ ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [x′])
         → ([t≡t′] : Δ ⊩⟨ ι ⁰ ⟩ t ≡ t′ ∷ wk (lift ρ) G₁ [ x ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [x])
         → (⊢e : Δ ⊢ e ∷ Id (U ⁰) (wk (lift ρ) G₁ [ x ]) (wk (lift ρ) G₃ [ y ]) ^ [ % , ι ¹ ])
         → (⊢e′ : Δ ⊢ e′ ∷ Id (U ⁰) (wk (lift ρ) G₁ [ x′ ]) (wk (lift ρ) G₃ [ y′ ]) ^ [ % , ι ¹ ])
         → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk (lift ρ) G₁ [ x ]) (wk (lift ρ) G₃ [ y ]) e t ≡ cast ⁰ (wk (lift ρ) G₁ [ x′ ]) (wk (lift ρ) G₃ [ y′ ]) e′ t′ ∷ wk (lift ρ) G₃ [ y ] ^ [ ! , ι ⁰ ] / [G₃] [ρ] ⊢Δ [y])
       (extrecursor₂ : ∀ {ρ Δ x x′ y y′ t t′ e e′}
         → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
         → ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
         → ([x′] : Δ ⊩⟨ ι ⁰ ⟩ x′ ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
         → ([x≡x′] : Δ ⊩⟨ ι ⁰ ⟩ x ≡ x′ ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
         → ([y] : Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
         → ([y′] : Δ ⊩⟨ ι ⁰ ⟩ y′ ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
         → ([y≡y′] : Δ ⊩⟨ ι ⁰ ⟩ y ≡ y′ ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
         → ([t] : Δ ⊩⟨ ι ⁰ ⟩ t ∷ wk (lift ρ) G₂ [ x ] ^ [ ! , ι ⁰ ] / [G₂] [ρ] ⊢Δ [x])
         → ([t′] : Δ ⊩⟨ ι ⁰ ⟩ t′ ∷ wk (lift ρ) G₂ [ x′ ] ^ [ ! , ι ⁰ ] / [G₂] [ρ] ⊢Δ [x′])
         → ([t≡t′] : Δ ⊩⟨ ι ⁰ ⟩ t ≡ t′ ∷ wk (lift ρ) G₂ [ x ] ^ [ ! , ι ⁰ ] / [G₂] [ρ] ⊢Δ [x])
         → (⊢e : Δ ⊢ e ∷ Id (U ⁰) (wk (lift ρ) G₂ [ x ]) (wk (lift ρ) G₄ [ y ]) ^ [ % , ι ¹ ])
         → (⊢e′ : Δ ⊢ e′ ∷ Id (U ⁰) (wk (lift ρ) G₂ [ x′ ]) (wk (lift ρ) G₄ [ y′ ]) ^ [ % , ι ¹ ])
         → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk (lift ρ) G₂ [ x ]) (wk (lift ρ) G₄ [ y ]) e t ≡ cast ⁰ (wk (lift ρ) G₂ [ x′ ]) (wk (lift ρ) G₄ [ y′ ]) e′ t′ ∷ wk (lift ρ) G₄ [ y ] ^ [ ! , ι ⁰ ] / [G₄] [ρ] ⊢Δ [y])
       (eqrecursor : ∀ {ρ Δ x₁ x₂ x₃ x₄ t₁ t₂ e₁₃ e₂₄}
         → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
         → ([x₁] : Δ ⊩⟨ ι ⁰ ⟩ x₁ ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
         → ([x₂] : Δ ⊩⟨ ι ⁰ ⟩ x₂ ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
         → ([G₁x₁≡G₂x₂] : Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₁ [ x₁ ] ≡ wk (lift ρ) G₂ [ x₂ ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [x₁])
         → ([x₃] : Δ ⊩⟨ ι ⁰ ⟩ x₃ ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
         → ([x₄] : Δ ⊩⟨ ι ⁰ ⟩ x₄ ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
         → ([G₃x₃≡G₄x₄] : Δ ⊩⟨ ι ⁰ ⟩ wk (lift ρ) G₃ [ x₃ ] ≡ wk (lift ρ) G₄ [ x₄ ] ^ [ ! , ι ⁰ ] / [G₃] [ρ] ⊢Δ [x₃])
         → ([t₁] : Δ ⊩⟨ ι ⁰ ⟩ t₁ ∷ wk (lift ρ) G₁ [ x₁ ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [x₁])
         → ([t₂] : Δ ⊩⟨ ι ⁰ ⟩ t₂ ∷ wk (lift ρ) G₂ [ x₂ ] ^ [ ! , ι ⁰ ] / [G₂] [ρ] ⊢Δ [x₂])
         → ([t₁≡t₂] : Δ ⊩⟨ ι ⁰ ⟩ t₁ ≡ t₂ ∷ wk (lift ρ) G₁ [ x₁ ] ^ [ ! , ι ⁰ ] / [G₁] [ρ] ⊢Δ [x₁])
         → (⊢e₁₃ : Δ ⊢ e₁₃ ∷ Id (U ⁰) (wk (lift ρ) G₁ [ x₁ ]) (wk (lift ρ) G₃ [ x₃ ]) ^ [ % , ι ¹ ])
         → (⊢e₂₄ : Δ ⊢ e₂₄ ∷ Id (U ⁰) (wk (lift ρ) G₂ [ x₂ ]) (wk (lift ρ) G₄ [ x₄ ]) ^ [ % , ι ¹ ])
         → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk (lift ρ) G₁ [ x₁ ]) (wk (lift ρ) G₃ [ x₃ ]) e₁₃ t₁ ≡ cast ⁰ (wk (lift ρ) G₂ [ x₂ ]) (wk (lift ρ) G₄ [ x₄ ]) e₂₄ t₂ ∷ wk (lift ρ) G₃ [ x₃ ] ^ [ ! , ι ⁰ ] / [G₃] [ρ] ⊢Δ [x₃])

       ([b₁] : ∀ {ρ Δ e x}
                ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
                (⊢e : Δ ⊢ e ∷ Id (Univ rF ⁰) (wk ρ F₁) (wk ρ F₃) ^ [ % , ι ¹ ])
                ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
                → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk ρ F₃) (wk ρ F₁) (Idsym (Univ rF ⁰) (wk ρ F₁) (wk ρ F₃) e) x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
       ([bext₁] : ∀ {ρ Δ e e′ x y} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
           → (Δ ⊢ e ∷ Id (Univ rF ⁰) (wk ρ F₁) (wk ρ F₃) ^ [ % , ι ¹ ])
           → (Δ ⊢ e′ ∷ Id (Univ rF ⁰) (wk ρ F₁) (wk ρ F₃) ^ [ % , ι ¹ ])
           → (Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
           → (Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
           → (Δ ⊩⟨ ι ⁰ ⟩ x ≡ y ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
           → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk ρ F₃) (wk ρ F₁) (Idsym (Univ rF ⁰) (wk ρ F₁) (wk ρ F₃) e) x
             ≡ cast ⁰ (wk ρ F₃) (wk ρ F₁) (Idsym (Univ rF ⁰) (wk ρ F₁) (wk ρ F₃) e′) y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
       ([b₂] : ∀ {ρ Δ e x}
                ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
                (⊢e : Δ ⊢ e ∷ Id (Univ rF ⁰) (wk ρ F₂) (wk ρ F₄) ^ [ % , ι ¹ ])
                ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
                → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk ρ F₄) (wk ρ F₂) (Idsym (Univ rF ⁰) (wk ρ F₂) (wk ρ F₄) e) x ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
       ([bext₂] : ∀ {ρ Δ e e′ x y} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
           → (Δ ⊢ e ∷ Id (Univ rF ⁰) (wk ρ F₂) (wk ρ F₄) ^ [ % , ι ¹ ])
           → (Δ ⊢ e′ ∷ Id (Univ rF ⁰) (wk ρ F₂) (wk ρ F₄) ^ [ % , ι ¹ ])
           → (Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
           → (Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
           → (Δ ⊩⟨ ι ⁰ ⟩ x ≡ y ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
           → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk ρ F₄) (wk ρ F₂) (Idsym (Univ rF ⁰) (wk ρ F₂) (wk ρ F₄) e) x
             ≡ cast ⁰ (wk ρ F₄) (wk ρ F₂) (Idsym (Univ rF ⁰) (wk ρ F₂) (wk ρ F₄) e′) y ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
       ([b₁≡b₂] : ∀ {ρ Δ e₁₃ e₂₄ x₃ x₄} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
            → (Δ ⊢ e₁₃ ∷ Id (Univ rF ⁰) (wk ρ F₁) (wk ρ F₃) ^ [ % , ι ¹ ])
            → (Δ ⊢ e₂₄ ∷ Id (Univ rF ⁰) (wk ρ F₂) (wk ρ F₄) ^ [ % , ι ¹ ])
            → (Δ ⊩⟨ ι ⁰ ⟩ x₃ ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
            → (Δ ⊩⟨ ι ⁰ ⟩ x₄ ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
            → (Δ ⊩⟨ ι ⁰ ⟩ x₃ ≡ x₄ ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
            → Δ ⊩⟨ ι ⁰ ⟩ cast ⁰ (wk ρ F₃) (wk ρ F₁) (Idsym (Univ rF ⁰) (wk ρ F₁) (wk ρ F₃) e₁₃) x₃
              ≡ cast ⁰ (wk ρ F₄) (wk ρ F₂) (Idsym (Univ rF ⁰) (wk ρ F₂) (wk ρ F₄) e₂₄) x₄ ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)

  where
    module g₁ = cast-ΠΠ-lemmas-2 ⊢Γ ⊢A₁ ⊢ΠF₁G₁ D₁ ⊢F₁ ⊢G₁ A₁≡A₁ [F₁] [G₁] G₁-ext ⊢A₃ ⊢ΠF₃G₃ D₃ ⊢F₃ ⊢G₃ A₃≡A₃ [F₃] [G₃] G₃-ext ⊢e₁₃
                          recursor₁ extrecursor₁ ⊢t₁ Df₁ [f₁ext] [f₁] [b₁] [bext₁]
    module g₂ = cast-ΠΠ-lemmas-2 ⊢Γ ⊢A₂ ⊢ΠF₂G₂ D₂ ⊢F₂ ⊢G₂ A₂≡A₂ [F₂] [G₂] G₂-ext ⊢A₄ ⊢ΠF₄G₄ D₄ ⊢F₄ ⊢G₄ A₄≡A₄ [F₄] [G₄] G₄-ext ⊢e₂₄
                          recursor₂ extrecursor₂ ⊢t₂ Df₂ [f₂ext] [f₂] [b₂] [bext₂]

    [g₁≡g₂] : ∀ {ρ Δ x₃ x₄} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
        → ([x₃] : Δ ⊩⟨ ι ⁰ ⟩ x₃ ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
        → ([x₄] : Δ ⊩⟨ ι ⁰ ⟩ x₄ ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
        → ([x₃≡x₄] : Δ ⊩⟨ ι ⁰ ⟩ x₃ ≡ x₄ ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
        → Δ ⊩⟨ ι ⁰ ⟩ g₁.g ρ x₃ ≡ g₂.g ρ x₄ ∷ wk (lift ρ) G₃ [ x₃ ] ^ [ ! , ι ⁰ ] / [G₃] [ρ] ⊢Δ [x₃]
    [g₁≡g₂] {ρ} {Δ} {x₃} {x₄} [ρ] ⊢Δ [x₃] [x₄] [x₃≡x₄] =
      let
        [b₁] = [b₁] [ρ] ⊢Δ (Twk.wkTerm [ρ] ⊢Δ g₁.⊢fste) [x₃]
        [b₂] = [b₂] [ρ] ⊢Δ (Twk.wkTerm [ρ] ⊢Δ g₂.⊢fste) [x₄]
        [b₁≡b₂]′ = [b₁≡b₂] [ρ] ⊢Δ (Twk.wkTerm [ρ] ⊢Δ g₁.⊢fste) (Twk.wkTerm [ρ] ⊢Δ g₂.⊢fste) [x₃] [x₄] [x₃≡x₄]
        [b₁:F₂] = convTerm₁ ([F₁] [ρ] ⊢Δ) ([F₂] [ρ] ⊢Δ) ([F₁≡F₂] [ρ] ⊢Δ) [b₁]
        [b₁≡b₂:F₂] = convEqTerm₁ ([F₁] [ρ] ⊢Δ) ([F₂] [ρ] ⊢Δ) ([F₁≡F₂] [ρ] ⊢Δ) [b₁≡b₂]′
        [G₁b₁≡G₂b₂] = transEq ([G₁] [ρ] ⊢Δ [b₁]) ([G₂] [ρ] ⊢Δ [b₁:F₂]) ([G₂] [ρ] ⊢Δ [b₂])
          ([G₁≡G₂] [ρ] ⊢Δ [b₁]) (G₂-ext [ρ] ⊢Δ [b₁:F₂] [b₂] [b₁≡b₂:F₂])
        [x₃:F₄] = convTerm₁ ([F₃] [ρ] ⊢Δ) ([F₄] [ρ] ⊢Δ) ([F₃≡F₄] [ρ] ⊢Δ) [x₃]
        [x₃≡x₄:F₄] = convEqTerm₁ ([F₃] [ρ] ⊢Δ) ([F₄] [ρ] ⊢Δ) ([F₃≡F₄] [ρ] ⊢Δ) [x₃≡x₄]
        [G₃x₃≡G₄x₄] = transEq ([G₃] [ρ] ⊢Δ [x₃]) ([G₄] [ρ] ⊢Δ [x₃:F₄]) ([G₄] [ρ] ⊢Δ [x₄])
          ([G₃≡G₄] [ρ] ⊢Δ [x₃]) (G₄-ext [ρ] ⊢Δ [x₃:F₄] [x₄] [x₃≡x₄:F₄])
        [t₁] , [t₁≡f₁b₁] = redSubst*Term (appRed* (escapeTerm ([F₁] [ρ] ⊢Δ) [b₁]) (Twk.wkRed*Term [ρ] ⊢Δ Df₁))
          ([G₁] [ρ] ⊢Δ [b₁]) ([f₁] [ρ] ⊢Δ [b₁])
        [t₂] , [t₂≡f₂b₂] = redSubst*Term (appRed* (escapeTerm ([F₂] [ρ] ⊢Δ) [b₂]) (Twk.wkRed*Term [ρ] ⊢Δ Df₂))
          ([G₂] [ρ] ⊢Δ [b₂]) ([f₂] [ρ] ⊢Δ [b₂])
        [t₁≡f₂b₁] = transEqTerm ([G₁] [ρ] ⊢Δ [b₁]) [t₁≡f₁b₁] ([f₁≡f₂] [ρ] ⊢Δ [b₁])
        [f₂b₁≡t₂] = symEqTerm ([G₂] [ρ] ⊢Δ [b₂]) (transEqTerm ([G₂] [ρ] ⊢Δ [b₂]) [t₂≡f₂b₂] ([f₂ext] [ρ] ⊢Δ [b₂] [b₁:F₂] (symEqTerm ([F₂] [ρ] ⊢Δ) [b₁≡b₂:F₂])))
        [t₁≡t₂] = transEqTerm ([G₁] [ρ] ⊢Δ [b₁]) [t₁≡f₂b₁] (convEqTerm₂ ([G₁] [ρ] ⊢Δ [b₁]) ([G₂] [ρ] ⊢Δ [b₂]) [G₁b₁≡G₂b₂] [f₂b₁≡t₂])
        x = eqrecursor [ρ] ⊢Δ [b₁] [b₂] [G₁b₁≡G₂b₂] [x₃] [x₄] [G₃x₃≡G₄x₄] [t₁] [t₂] [t₁≡t₂]
                       (g₁.⊢snde′ [ρ] ⊢Δ (escapeTerm ([F₃] [ρ] ⊢Δ) [x₃])) (g₂.⊢snde′ [ρ] ⊢Δ (escapeTerm ([F₄] [ρ] ⊢Δ) [x₄]))
      in x

    g₁≡g₂ : Γ ⊢ (lam F₃ ▹ g₁.g (step id) (var 0) ^ ⁰) ≅ (lam F₄ ▹ g₂.g (step id) (var 0) ^ ⁰) ∷ Π F₃ ^ rF ° ⁰ ▹ G₃ ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ]
    g₁≡g₂ =
      let
        Δ₁ = g₁.Δ₁
        ⊢Δ₁ = g₁.⊢Δ₁
        [ρ₁] = g₁.[ρ₁]
        ⊢F₃′ = Twk.wk (Twk.step Twk.id) ⊢Δ₁ ⊢F₃
        ⊢g₁0 = escapeTerm ([G₃] [ρ₁] ⊢Δ₁ g₁.[0]) (g₁.[g] [ρ₁] ⊢Δ₁ g₁.[0])
        ⊢g₁0′ = (PE.subst (λ X → Δ₁ ⊢ g₁.g (step id) (var 0) ∷ X ^ [ ! , ι ⁰ ]) (wkSingleSubstId G₃) ⊢g₁0)
        ⊢g₁0″ = Twk.wkTerm (Twk.lift (Twk.step Twk.id)) (⊢Δ₁ ∙ ⊢F₃′) ⊢g₁0′
        ⊢F₄′ = Twk.wk (Twk.step Twk.id) ⊢Δ₁ ⊢F₄
        ⊢g₂0 = escapeTerm ([G₄] g₂.[ρ₁] g₂.⊢Δ₁ g₂.[0]) (g₂.[g] g₂.[ρ₁] g₂.⊢Δ₁ g₂.[0])
        ⊢g₂0′ = (PE.subst (λ X → g₂.Δ₁ ⊢ g₂.g (step id) (var 0) ∷ X ^ [ ! , ι ⁰ ]) (wkSingleSubstId G₄) ⊢g₂0)
        ⊢g₂0″ = Twk.wkTerm (Twk.lift (Twk.step Twk.id)) (⊢Δ₁ ∙ ⊢F₄′) ⊢g₂0′
        D₁ : Δ₁ ⊢ (lam (wk1 F₃) ▹ wk1d (g₁.g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ⇒* g₁.g (step id) (var 0) ∷ wk1d G₃ [ var 0 ] ^ ι ⁰
        D₁ = PE.subst (λ X → Δ₁ ⊢ (lam (wk1 F₃) ▹ wk1d (g₁.g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ⇒ X ∷ wk1d G₃ [ var 0 ] ^ ι ⁰)
          (wkSingleSubstId (g₁.g (step id) (var 0))) (β-red (≡is≤ PE.refl) (≡is≤ PE.refl) ⊢F₃′ ⊢g₁0″ (var ⊢Δ₁ here))
          ⇨ id ⊢g₁0
        F₃≡F₄ = escapeEq ([F₃] [ρ₁] ⊢Δ₁) ([F₃≡F₄] [ρ₁] ⊢Δ₁)
        [0:F₄] : Δ₁ ⊩⟨ ι ⁰ ⟩ var 0 ∷ wk (step id) F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ₁] ⊢Δ₁
        [0:F₄] = neuTerm ([F₄] [ρ₁] ⊢Δ₁) (var 0) (conv (var ⊢Δ₁ here) (≅-eq F₃≡F₄)) (~-var (conv (var ⊢Δ₁ here) (≅-eq F₃≡F₄)))
        D₂ : Δ₁ ⊢ (lam (wk1 F₄) ▹ wk1d (g₂.g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ⇒* g₂.g (step id) (var 0) ∷ wk1d G₄ [ var 0 ] ^ ι ⁰
        D₂ = PE.subst (λ X → Δ₁ ⊢ (lam (wk1 F₄) ▹ wk1d (g₂.g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ⇒ X ∷ wk1d G₄ [ var 0 ] ^ ι ⁰)
          (wkSingleSubstId (g₂.g (step id) (var 0))) (β-red (≡is≤ PE.refl) (≡is≤ PE.refl) ⊢F₄′ ⊢g₂0″ (conv (var ⊢Δ₁ here) (≅-eq F₃≡F₄)))
          ⇨ id (escapeTerm ([G₄] [ρ₁] ⊢Δ₁ [0:F₄]) (g₂.[g] [ρ₁] ⊢Δ₁ [0:F₄]))
        [g₁0≡g₁] : Δ₁ ⊩⟨ ι ⁰ ⟩ (lam (wk1 F₃) ▹ wk1d (g₁.g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ≡ g₁.g (step id) (var 0) ∷ wk1d G₃ [ var 0 ] ^ [ ! , ι ⁰ ] / [G₃] [ρ₁] ⊢Δ₁ g₁.[0]
        [g₁0≡g₁] = proj₂ (redSubst*Term D₁ ([G₃] [ρ₁] ⊢Δ₁ g₁.[0]) (g₁.[g] [ρ₁] ⊢Δ₁ g₁.[0]))
        [g₂0≡g₂] : Δ₁ ⊩⟨ ι ⁰ ⟩ (lam (wk1 F₄) ▹ wk1d (g₂.g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ≡ g₂.g (step id) (var 0) ∷ wk1d G₄ [ var 0 ] ^ [ ! , ι ⁰ ] / [G₄] [ρ₁] ⊢Δ₁ [0:F₄]
        [g₂0≡g₂] = proj₂ (redSubst*Term D₂ ([G₄] [ρ₁] ⊢Δ₁ [0:F₄]) (g₂.[g] [ρ₁] ⊢Δ₁ [0:F₄]))
        [g₁≡g₂]′ : Δ₁ ⊩⟨ ι ⁰ ⟩ g₁.g (step id) (var 0) ≡ g₂.g (step id) (var 0) ∷ wk1d G₃ [ var 0 ] ^ [ ! , ι ⁰ ] / [G₃] [ρ₁] ⊢Δ₁ g₁.[0]
        [g₁≡g₂]′ = [g₁≡g₂] [ρ₁] ⊢Δ₁ g₁.[0] (convTerm₁ ([F₃] [ρ₁] ⊢Δ₁) ([F₄] [ρ₁] ⊢Δ₁) ([F₃≡F₄] [ρ₁] ⊢Δ₁) g₁.[0]) (reflEqTerm ([F₃] [ρ₁] ⊢Δ₁) g₁.[0])
        [g₁0≡g₂0] = transEqTerm ([G₃] [ρ₁] ⊢Δ₁ g₁.[0]) (transEqTerm ([G₃] [ρ₁] ⊢Δ₁ g₁.[0]) [g₁0≡g₁] [g₁≡g₂]′)
          (convEqTerm₂ ([G₃] [ρ₁] ⊢Δ₁ g₁.[0]) ([G₄] [ρ₁] ⊢Δ₁ [0:F₄]) ([G₃≡G₄] [ρ₁] ⊢Δ₁ g₁.[0]) (symEqTerm ([G₄] [ρ₁] ⊢Δ₁ [0:F₄]) [g₂0≡g₂]))
        x₀ = escapeTermEq ([G₃] [ρ₁] ⊢Δ₁ g₁.[0]) [g₁0≡g₂0]
        x₁ = PE.subst (λ X → Δ₁ ⊢ (lam (wk1 F₃) ▹ wk1d (g₁.g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ≅ (lam (wk1 F₄) ▹ wk1d (g₂.g (step id) (var 0)) ^ ⁰) ∘ (var 0) ^ ⁰ ∷ X ^ [ ! , ι ⁰ ]) (wkSingleSubstId G₃) x₀
      in ≅-η-eq (≡is≤ PE.refl) (≡is≤ PE.refl) ⊢F₃ g₁.⊢λg (conv g₂.⊢λg (sym (≅-eq A₃≡A₄))) lamₙ lamₙ x₁

    [g₁a≡g₂a] : ∀ {ρ Δ a} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
        → ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
        → (Δ ⊩⟨ ι ⁰ ⟩ wk ρ (lam F₃ ▹ g₁.g (step id) (var 0) ^ ⁰) ∘ a ^ ⁰ ≡ wk ρ (lam F₄ ▹ g₂.g (step id) (var 0) ^ ⁰) ∘ a ^ ⁰
            ∷ wk (lift ρ) G₃ [ a ] ^ [ ! , ι ⁰ ] / [G₃] [ρ] ⊢Δ [a])
    [g₁a≡g₂a] [ρ] ⊢Δ [a] =
      let
        [a]′ = convTerm₁ ([F₃] [ρ] ⊢Δ) ([F₄] [ρ] ⊢Δ) ([F₃≡F₄] [ρ] ⊢Δ) [a]
        [a≡a] = reflEqTerm ([F₃] [ρ] ⊢Δ) [a]
      in redSubst*EqTerm (g₁.g∘a≡ga [ρ] ⊢Δ [a]) (g₂.g∘a≡ga [ρ] ⊢Δ [a]′)
         ([G₃] [ρ] ⊢Δ [a]) ([G₄] [ρ] ⊢Δ [a]′) ([G₃≡G₄] [ρ] ⊢Δ [a])
         (g₁.[g] [ρ] ⊢Δ [a]) (g₂.[g] [ρ] ⊢Δ [a]′) ([g₁≡g₂] [ρ] ⊢Δ [a] [a]′ [a≡a])

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
------------------------------------------------------------------------
-- Universe levels
------------------------------------------------------------------------

module Imports.Level where

open import Agda.Primitive using (Level; _⊔_) renaming (lzero to zero; lsuc to suc)


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
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.Introductions.SingleSubst

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Application of valid terms.
appᵛ : ∀ {F G t u Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
       ([ΠFG] : Γ ⊩ᵛ⟨ l ⟩ Π F ▹ G / [Γ])
       ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ Π F ▹ G / [Γ] / [ΠFG])
       ([u] : Γ ⊩ᵛ⟨ l ⟩ u ∷ F / [Γ] / [F])
     → Γ ⊩ᵛ⟨ l ⟩ t ∘ u ∷ G [ u ] / [Γ] / substSΠ {F} {G} {u} [Γ] [F] [ΠFG] [u]
appᵛ {F} {G} {t} {u} [Γ] [F] [ΠFG] [t] [u] {σ = σ} ⊢Δ [σ] =
  let [G[u]] = substSΠ {F} {G} {u} [Γ] [F] [ΠFG] [u]
      [σF] = proj₁ ([F] ⊢Δ [σ])
      [σΠFG] = proj₁ ([ΠFG] ⊢Δ [σ])
      [σt] = proj₁ ([t] ⊢Δ [σ])
      [σu] = proj₁ ([u] ⊢Δ [σ])
      [σG[u]]  = proj₁ ([G[u]] ⊢Δ [σ])
      [σG[u]]′ = irrelevance′ (singleSubstLift G u) [σG[u]]
  in  irrelevanceTerm′ (PE.sym (singleSubstLift G u))
                       [σG[u]]′ [σG[u]]
                       (appTerm [σF] [σG[u]]′ [σΠFG] [σt] [σu])
  ,   (λ [σ′] [σ≡σ′] →
         let [σu′] = convTerm₂ [σF] (proj₁ ([F] ⊢Δ [σ′]))
                               (proj₂ ([F] ⊢Δ [σ]) [σ′] [σ≡σ′])
                               (proj₁ ([u] ⊢Δ [σ′]))
         in  irrelevanceEqTerm′ (PE.sym (singleSubstLift G u))
                                [σG[u]]′ [σG[u]]
                                (app-congTerm [σF] [σG[u]]′ [σΠFG]
                                              (proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′])
                                              [σu] [σu′]
                                              (proj₂ ([u] ⊢Δ [σ]) [σ′] [σ≡σ′])))

-- Application congurence of valid terms.
app-congᵛ : ∀ {F G t u a b Γ l}
            ([Γ] : ⊩ᵛ Γ)
            ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
            ([ΠFG] : Γ ⊩ᵛ⟨ l ⟩ Π F ▹ G / [Γ])
            ([t≡u] : Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ Π F ▹ G / [Γ] / [ΠFG])
            ([a] : Γ ⊩ᵛ⟨ l ⟩ a ∷ F / [Γ] / [F])
            ([b] : Γ ⊩ᵛ⟨ l ⟩ b ∷ F / [Γ] / [F])
            ([a≡b] : Γ ⊩ᵛ⟨ l ⟩ a ≡ b ∷ F / [Γ] / [F])
          → Γ ⊩ᵛ⟨ l ⟩ t ∘ a ≡ u ∘ b ∷ G [ a ] / [Γ]
              / substSΠ {F} {G} {a} [Γ] [F] [ΠFG] [a]
app-congᵛ {F} {G} {a = a} [Γ] [F] [ΠFG] [t≡u] [a] [b] [a≡b] ⊢Δ [σ] =
  let [σF] = proj₁ ([F] ⊢Δ [σ])
      [G[a]]  = proj₁ (substSΠ {F} {G} {a} [Γ] [F] [ΠFG] [a] ⊢Δ [σ])
      [G[a]]′ = irrelevance′ (singleSubstLift G a) [G[a]]
      [σΠFG] = proj₁ ([ΠFG] ⊢Δ [σ])
      [σa] = proj₁ ([a] ⊢Δ [σ])
      [σb] = proj₁ ([b] ⊢Δ [σ])
  in  irrelevanceEqTerm′ (PE.sym (singleSubstLift G a)) [G[a]]′ [G[a]]
                         (app-congTerm [σF] [G[a]]′ [σΠFG] ([t≡u] ⊢Δ [σ])
                                       [σa] [σb] ([a≡b] ⊢Δ [σ]))

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:
open import Agda.Builtin.Char
open import Agda.Builtin.Sigma

CC = Σ Char λ _ → Char

Test : (c : Char) → Set
Test 'a' = CC
Test _   = CC

test : (c : Char) → Test c
test 'a' .fst = 'a'

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2011-04-07

module IrrelevantFin where

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

data Fin : Nat -> Set where
  zero : .(n : Nat) -> Fin (suc n)
  suc  : .(n : Nat) -> Fin n -> Fin (suc n)
-- this should not type check, since irrelevant n cannot appear in Fin n
-- or Fin (suc c)
-- note: this is possible in ICC*, but not in Agda!

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Proofs where

-- Various general lemmas

open import Level using (Level)

open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; cong)
open import Data.Sum using (inj₁; inj₂)
open import Data.Empty

open import Data.Nat.Properties.Simple using ()

----------------------------------------------
-- re-open some sub-files 'public'
open import FiniteFunctions public
open import VectorLemmas public
open import SubstLemmas public
open import LeqLemmas public
open import FinNatLemmas public
open import PathLemmas public

---------------------------------------------
-- Some generally useful functions

-- From Alan Jeffrey's post to Agda list

_⊨_⇒_≡_ : ∀ {I : Set} (F : I → Set) {i j} →
  (i ≡ j) → (F i) → (F j) → Set
(F ⊨ refl ⇒ x ≡ y) = (x ≡ y)

xcong : ∀ {I J F G} (f : I → J) (g : ∀ {i} → F i → G (f i)) →
  ∀ {i j} (i≡j : i ≡ j) {x y} →
    (F ⊨ i≡j ⇒ x ≡ y) → (G ⊨ cong f i≡j ⇒ g x ≡ g y)
xcong f g refl refl = refl

congD! : {a b : Level} {A : Set a} {B : A → Set b}
         (f : (x : A) → B x) → {x₁ x₂ : A} → (x₂≡x₁ : x₂ ≡ x₁) →
         subst B x₂≡x₁ (f x₂) ≡ f x₁
congD! f refl = refl

-- Courtesy of Wolfram Kahl, a dependent cong₂

cong₂D! : {a b c : Level} {A : Set a} {B : A → Set b} {C : Set c}
         (f : (x : A) → B x → C)
       → {x₁ x₂ : A} {y₁ : B x₁} {y₂ : B x₂}
       → (x₂≡x₁ : x₂ ≡ x₁) → subst B x₂≡x₁ y₂ ≡ y₁ → f x₁ y₁ ≡ f x₂ y₂
cong₂D! f refl refl = refl

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

inj-injective : ∀ {A B : Set} {a : A} {b : B} → inj₁ a ≡ inj₂ b → ⊥
inj-injective ()

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness #-}

module Agda.Builtin.Reflection where

open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Word
open import Agda.Builtin.List
open import Agda.Builtin.String
open import Agda.Builtin.Char
open import Agda.Builtin.Float
open import Agda.Builtin.Int
open import Agda.Builtin.Sigma

-- Names --

postulate Name : Set
{-# BUILTIN QNAME Name #-}

primitive
  primQNameEquality : Name → Name → Bool
  primQNameLess     : Name → Name → Bool
  primShowQName     : Name → String

-- Fixity --

data Associativity : Set where
  left-assoc  : Associativity
  right-assoc : Associativity
  non-assoc   : Associativity

data Precedence : Set where
  related   : Int → Precedence
  unrelated : Precedence

data Fixity : Set where
  fixity : Associativity → Precedence → Fixity

{-# BUILTIN ASSOC      Associativity #-}
{-# BUILTIN ASSOCLEFT  left-assoc    #-}
{-# BUILTIN ASSOCRIGHT right-assoc   #-}
{-# BUILTIN ASSOCNON   non-assoc     #-}

{-# BUILTIN PRECEDENCE    Precedence #-}
{-# BUILTIN PRECRELATED   related    #-}
{-# BUILTIN PRECUNRELATED unrelated  #-}

{-# BUILTIN FIXITY       Fixity #-}
{-# BUILTIN FIXITYFIXITY fixity #-}

{-# COMPILE GHC Associativity = data MAlonzo.RTE.Assoc (MAlonzo.RTE.LeftAssoc | MAlonzo.RTE.RightAssoc | MAlonzo.RTE.NonAssoc) #-}
{-# COMPILE GHC Precedence    = data MAlonzo.RTE.Precedence (MAlonzo.RTE.Related | MAlonzo.RTE.Unrelated) #-}
{-# COMPILE GHC Fixity        = data MAlonzo.RTE.Fixity (MAlonzo.RTE.Fixity) #-}

{-# COMPILE JS Associativity  = function (x,v) { return v[x](); } #-}
{-# COMPILE JS left-assoc     = "left-assoc"  #-}
{-# COMPILE JS right-assoc    = "right-assoc" #-}
{-# COMPILE JS non-assoc      = "non-assoc"   #-}

{-# COMPILE JS Precedence     =
  function (x,v) {
    if (x === "unrelated") { return v[x](); } else { return v["related"](x); }} #-}
{-# COMPILE JS related        = function(x) { return x; } #-}
{-# COMPILE JS unrelated      = "unrelated"               #-}

{-# COMPILE JS Fixity         = function (x,v) { return v["fixity"](x["assoc"], x["prec"]); } #-}
{-# COMPILE JS fixity         = function (x) { return function (y) { return { "assoc": x, "prec": y}; }; } #-}

primitive
  primQNameFixity : Name → Fixity

-- Metavariables --

postulate Meta : Set
{-# BUILTIN AGDAMETA Meta #-}

primitive
  primMetaEquality : Meta → Meta → Bool
  primMetaLess     : Meta → Meta → Bool
  primShowMeta     : Meta → String

-- Arguments --

-- Arguments can be (visible), {hidden}, or {{instance}}.
data Visibility : Set where
  visible hidden instance′ : Visibility

{-# BUILTIN HIDING   Visibility #-}
{-# BUILTIN VISIBLE  visible    #-}
{-# BUILTIN HIDDEN   hidden     #-}
{-# BUILTIN INSTANCE instance′  #-}

-- Arguments can be relevant or irrelevant.
data Relevance : Set where
  relevant irrelevant : Relevance

{-# BUILTIN RELEVANCE  Relevance  #-}
{-# BUILTIN RELEVANT   relevant   #-}
{-# BUILTIN IRRELEVANT irrelevant #-}

data ArgInfo : Set where
  arg-info : (v : Visibility) (r : Relevance) → ArgInfo

data Arg (A : Set) : Set where
  arg : (i : ArgInfo) (x : A) → Arg A

{-# BUILTIN ARGINFO    ArgInfo  #-}
{-# BUILTIN ARGARGINFO arg-info #-}
{-# BUILTIN ARG        Arg      #-}
{-# BUILTIN ARGARG     arg      #-}

-- Name abstraction --

data Abs (A : Set) : Set where
  abs : (s : String) (x : A) → Abs A

{-# BUILTIN ABS    Abs #-}
{-# BUILTIN ABSABS abs #-}

-- Literals --

data Literal : Set where
  nat    : (n : Nat)    → Literal
  word64 : (n : Word64) → Literal
  float  : (x : Float)  → Literal
  char   : (c : Char)   → Literal
  string : (s : String) → Literal
  name   : (x : Name)   → Literal
  meta   : (x : Meta)   → Literal

{-# BUILTIN AGDALITERAL   Literal #-}
{-# BUILTIN AGDALITNAT    nat     #-}
{-# BUILTIN AGDALITWORD64 word64  #-}
{-# BUILTIN AGDALITFLOAT  float   #-}
{-# BUILTIN AGDALITCHAR   char    #-}
{-# BUILTIN AGDALITSTRING string  #-}
{-# BUILTIN AGDALITQNAME  name    #-}
{-# BUILTIN AGDALITMETA   meta    #-}

-- Patterns --

data Pattern : Set where
  con    : (c : Name) (ps : List (Arg Pattern)) → Pattern
  dot    : Pattern
  var    : (s : String)  → Pattern
  lit    : (l : Literal) → Pattern
  proj   : (f : Name)    → Pattern
  absurd : Pattern

{-# BUILTIN AGDAPATTERN   Pattern #-}
{-# BUILTIN AGDAPATCON    con     #-}
{-# BUILTIN AGDAPATDOT    dot     #-}
{-# BUILTIN AGDAPATVAR    var     #-}
{-# BUILTIN AGDAPATLIT    lit     #-}
{-# BUILTIN AGDAPATPROJ   proj    #-}
{-# BUILTIN AGDAPATABSURD absurd  #-}

-- Terms --

data Sort   : Set
data Clause : Set
data Term   : Set
Type = Term

data Term where
  var       : (x : Nat) (args : List (Arg Term)) → Term
  con       : (c : Name) (args : List (Arg Term)) → Term
  def       : (f : Name) (args : List (Arg Term)) → Term
  lam       : (v : Visibility) (t : Abs Term) → Term
  pat-lam   : (cs : List Clause) (args : List (Arg Term)) → Term
  pi        : (a : Arg Type) (b : Abs Type) → Term
  agda-sort : (s : Sort) → Term
  lit       : (l : Literal) → Term
  meta      : (x : Meta) → List (Arg Term) → Term
  unknown   : Term

data Sort where
  set     : (t : Term) → Sort
  lit     : (n : Nat) → Sort
  unknown : Sort

data Clause where
  clause        : (ps : List (Arg Pattern)) (t : Term) → Clause
  absurd-clause : (ps : List (Arg Pattern)) → Clause

{-# BUILTIN AGDASORT    Sort   #-}
{-# BUILTIN AGDATERM    Term   #-}
{-# BUILTIN AGDACLAUSE  Clause #-}

{-# BUILTIN AGDATERMVAR         var       #-}
{-# BUILTIN AGDATERMCON         con       #-}
{-# BUILTIN AGDATERMDEF         def       #-}
{-# BUILTIN AGDATERMMETA        meta      #-}
{-# BUILTIN AGDATERMLAM         lam       #-}
{-# BUILTIN AGDATERMEXTLAM      pat-lam   #-}
{-# BUILTIN AGDATERMPI          pi        #-}
{-# BUILTIN AGDATERMSORT        agda-sort #-}
{-# BUILTIN AGDATERMLIT         lit       #-}
{-# BUILTIN AGDATERMUNSUPPORTED unknown   #-}

{-# BUILTIN AGDASORTSET         set     #-}
{-# BUILTIN AGDASORTLIT         lit     #-}
{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}

{-# BUILTIN AGDACLAUSECLAUSE clause        #-}
{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}

-- Definitions --

data Definition : Set where
  function    : (cs : List Clause) → Definition
  data-type   : (pars : Nat) (cs : List Name) → Definition
  record-type : (c : Name) (fs : List (Arg Name)) → Definition
  data-cons   : (d : Name) → Definition
  axiom       : Definition
  prim-fun    : Definition

{-# BUILTIN AGDADEFINITION                Definition  #-}
{-# BUILTIN AGDADEFINITIONFUNDEF          function    #-}
{-# BUILTIN AGDADEFINITIONDATADEF         data-type   #-}
{-# BUILTIN AGDADEFINITIONRECORDDEF       record-type #-}
{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR data-cons   #-}
{-# BUILTIN AGDADEFINITIONPOSTULATE       axiom       #-}
{-# BUILTIN AGDADEFINITIONPRIMITIVE       prim-fun    #-}

-- Errors --

data ErrorPart : Set where
  strErr  : String → ErrorPart
  termErr : Term → ErrorPart
  nameErr : Name → ErrorPart

{-# BUILTIN AGDAERRORPART       ErrorPart #-}
{-# BUILTIN AGDAERRORPARTSTRING strErr    #-}
{-# BUILTIN AGDAERRORPARTTERM   termErr   #-}
{-# BUILTIN AGDAERRORPARTNAME   nameErr   #-}

-- TC monad --

postulate
  TC            : ∀ {a} → Set a → Set a
  returnTC      : ∀ {a} {A : Set a} → A → TC A
  bindTC        : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
  unify         : Term → Term → TC ⊤
  typeError     : ∀ {a} {A : Set a} → List ErrorPart → TC A
  inferType     : Term → TC Type
  checkType     : Term → Type → TC Term
  normalise     : Term → TC Term
  reduce        : Term → TC Term
  catchTC       : ∀ {a} {A : Set a} → TC A → TC A → TC A
  quoteTC       : ∀ {a} {A : Set a} → A → TC Term
  unquoteTC     : ∀ {a} {A : Set a} → Term → TC A
  getContext    : TC (List (Arg Type))
  extendContext : ∀ {a} {A : Set a} → Arg Type → TC A → TC A
  inContext     : ∀ {a} {A : Set a} → List (Arg Type) → TC A → TC A
  freshName     : String → TC Name
  declareDef    : Arg Name → Type → TC ⊤
  declarePostulate  : Arg Name → Type → TC ⊤
  defineFun     : Name → List Clause → TC ⊤
  getType       : Name → TC Type
  getDefinition : Name → TC Definition
  blockOnMeta   : ∀ {a} {A : Set a} → Meta → TC A
  commitTC      : TC ⊤
  isMacro       : Name → TC Bool

  -- If the argument is 'true' makes the following primitives also normalise
  -- their results: inferType, checkType, quoteTC, getType, and getContext
  withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A

  -- Prints the third argument if the corresponding verbosity level is turned
  -- on (with the -v flag to Agda).
  debugPrint : String → Nat → List ErrorPart → TC ⊤

  -- Fail if the given computation gives rise to new, unsolved
  -- "blocking" constraints.
  noConstraints : ∀ {a} {A : Set a} → TC A → TC A

  -- Run the given TC action and return the first component. Resets to
  -- the old TC state if the second component is 'false', or keep the
  -- new TC state if it is 'true'.
  runSpeculative : ∀ {a} {A : Set a} → TC (Σ A λ _ → Bool) → TC A

{-# BUILTIN AGDATCM              TC            #-}
{-# BUILTIN AGDATCMRETURN        returnTC      #-}
{-# BUILTIN AGDATCMBIND          bindTC        #-}
{-# BUILTIN AGDATCMUNIFY         unify         #-}
{-# BUILTIN AGDATCMTYPEERROR     typeError     #-}
{-# BUILTIN AGDATCMINFERTYPE     inferType     #-}
{-# BUILTIN AGDATCMCHECKTYPE     checkType     #-}
{-# BUILTIN AGDATCMNORMALISE     normalise     #-}
{-# BUILTIN AGDATCMREDUCE        reduce        #-}
{-# BUILTIN AGDATCMCATCHERROR    catchTC       #-}
{-# BUILTIN AGDATCMQUOTETERM     quoteTC       #-}
{-# BUILTIN AGDATCMUNQUOTETERM   unquoteTC     #-}
{-# BUILTIN AGDATCMGETCONTEXT    getContext    #-}
{-# BUILTIN AGDATCMEXTENDCONTEXT extendContext #-}
{-# BUILTIN AGDATCMINCONTEXT     inContext     #-}
{-# BUILTIN AGDATCMFRESHNAME     freshName     #-}
{-# BUILTIN AGDATCMDECLAREDEF    declareDef    #-}
{-# BUILTIN AGDATCMDECLAREPOSTULATE declarePostulate #-}
{-# BUILTIN AGDATCMDEFINEFUN     defineFun     #-}
{-# BUILTIN AGDATCMGETTYPE       getType       #-}
{-# BUILTIN AGDATCMGETDEFINITION getDefinition #-}
{-# BUILTIN AGDATCMBLOCKONMETA   blockOnMeta   #-}
{-# BUILTIN AGDATCMCOMMIT        commitTC      #-}
{-# BUILTIN AGDATCMISMACRO       isMacro       #-}
{-# BUILTIN AGDATCMWITHNORMALISATION withNormalisation #-}
{-# BUILTIN AGDATCMDEBUGPRINT    debugPrint    #-}
{-# BUILTIN AGDATCMNOCONSTRAINTS noConstraints #-}
{-# BUILTIN AGDATCMRUNSPECULATIVE runSpeculative #-}

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
module Where where

{-
id : Set -> Set
id a = a
-}

-- x : (_ : _) -> _
x = id Set3000
  where id = \x -> x

y = False
  where data False : Set where

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


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

open import HoTT
open import homotopy.CircleHSpace
open import homotopy.JoinAssocCubical
open import homotopy.JoinSusp

module homotopy.Hopf where

import homotopy.HopfConstruction
module Hopf = homotopy.HopfConstruction S¹-conn ⊙S¹-hSpace

Hopf : S² → Type₀
Hopf = Hopf.H.f

Hopf-fiber : Hopf north == S¹
Hopf-fiber = idp

-- TODO Turn [Hopf.theorem] into an equivalence
Hopf-total : Σ _ Hopf ≃ S³
Hopf-total =
  Σ _ Hopf       ≃⟨ coe-equiv Hopf.theorem ⟩
  S¹ * S¹        ≃⟨ *-Susp-l S⁰ S¹ ⟩
  Susp (S⁰ * S¹) ≃⟨ Susp-emap (*-Bool-l S¹) ⟩
  S³ ≃∎

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Relations where

open import Agda.Builtin.Equality
open import Natural

data _≤_ : ℕ → ℕ → Set where
    z≤n : ∀ {n : ℕ} →
        zero ≤ n
    s≤s : ∀ {m n : ℕ} →
        m ≤ n →
        (suc m) ≤ (suc n)

infix 4 _≤_

-- example : finished by auto mode
_ : 3 ≤ 5
_ = s≤s {2} {4} (s≤s {1} {3} (s≤s {0} {2} (z≤n {2})))

inv-s≤s : ∀ {m n : ℕ}
    → suc m ≤ suc n
    → m ≤ n
inv-s≤s (s≤s m≤n) = m≤n

inv-z≤n : ∀ {m : ℕ}
    → m ≤ zero
    → m ≡ zero
inv-z≤n z≤n = refl

max_stars_repo_name: kands-code/agda-exercise

max_issues_repo_name: kands-code/agda-exercise

max_forks_repo_name: kands-code/agda-exercise


text:
-- cj-xu and fredriknordvallforsberg, 2018-04-30

open import Common.IO

data Bool : Set where
  true false : Bool

data MyUnit : Set where
  tt : MyUnit -- no eta!

HiddenFunType : MyUnit -> Set
HiddenFunType tt = Bool -> Bool

notTooManyArgs : (x : MyUnit) -> HiddenFunType x
notTooManyArgs tt b = b

{- This should not happen when compiling notTooManyArgs:

    • Couldn't match expected type ‘GHC.Prim.Any’
                  with actual type ‘a0 -> b0’
      The type variables ‘b0’, ‘a0’ are ambiguous
    • The equation(s) for ‘d10’ have two arguments,
      but its type ‘T2 -> AgdaAny’ has only one
-}

main : IO MyUnit
main = return tt


text:
module Data.Num.Nat where

open import Data.Num.Core renaming
    (   carry to carry'
    ;   carry-lower-bound to carry-lower-bound'
    ;   carry-upper-bound to carry-upper-bound'
    )
open import Data.Num.Maximum
open import Data.Num.Bounded
open import Data.Num.Next
open import Data.Num.Increment
open import Data.Num.Continuous

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra
open import Data.Nat.DM

open import Data.Fin as Fin
    using (Fin; fromℕ≤; inject≤)
    renaming (zero to z; suc to s)

open import Data.Fin.Properties using (toℕ-fromℕ≤; bounded)
open import Data.Product
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)

open import Function
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

-- left-bounded infinite interval of natural number
data Nat : ℕ → Set where
    from : ∀ offset   → Nat offset
    suc  : ∀ {offset} → Nat offset → Nat offset

Nat-toℕ : ∀ {offset} → Nat offset → ℕ
Nat-toℕ (from offset) = offset
Nat-toℕ (suc n)       = suc (Nat-toℕ n)

Nat-fromℕ : ∀ offset
    → (n : ℕ)
    → .(offset ≤ n)
    → Nat offset
Nat-fromℕ offset n       p with offset ≟ n
Nat-fromℕ offset n       p | yes eq = from offset
Nat-fromℕ offset zero    p | no ¬eq = from offset
Nat-fromℕ offset (suc n) p | no ¬eq = suc (Nat-fromℕ offset n (≤-pred (≤∧≢⇒< p ¬eq)))

Nat-fromℕ-toℕ : ∀ offset
    → (n : ℕ)
    → (p : offset ≤ n)
    → Nat-toℕ (Nat-fromℕ offset n p) ≡ n
Nat-fromℕ-toℕ offset n       p with offset ≟ n
Nat-fromℕ-toℕ offset n       p | yes eq = eq
Nat-fromℕ-toℕ .0      zero z≤n | no ¬eq = refl
Nat-fromℕ-toℕ offset (suc n) p | no ¬eq =
    begin
        suc (Nat-toℕ (Nat-fromℕ offset n (≤-pred (≤∧≢⇒< p ¬eq))))
    ≡⟨ cong suc (Nat-fromℕ-toℕ offset n (≤-pred (≤∧≢⇒< p ¬eq))) ⟩
        suc n
    ∎

fromNat : ∀ {b d o}
    → {cont : True (Continuous? b (suc d) o)}
    → Nat o
    → Num b (suc d) o
fromNat               (from offset) = z ∙
fromNat {cont = cont} (suc nat)     = 1+ {cont = cont} (fromNat {cont = cont} nat)

toℕ-fromNat : ∀ b d o
    → (cont : True (Continuous? b (suc d) o))
    → (n : ℕ)
    → (p : o ≤ n)
    → ⟦ fromNat {b} {d} {o} {cont = cont} (Nat-fromℕ o n p) ⟧ ≡ n
toℕ-fromNat b d o cont n       p with o ≟ n
toℕ-fromNat b d o cont n       p | yes eq = cong (_+_ zero) eq
toℕ-fromNat b d .0 cont zero z≤n | no ¬eq = refl
toℕ-fromNat b d o cont (suc n) p | no ¬eq =
    begin
        ⟦ 1+ {b} {cont = cont} (fromNat (Nat-fromℕ o n (≤-pred (≤∧≢⇒< p ¬eq)))) ⟧
    ≡⟨ 1+-toℕ {b} (fromNat {cont = cont} (Nat-fromℕ o n (≤-pred (≤∧≢⇒< p ¬eq)))) ⟩
        suc ⟦ fromNat {cont = cont} (Nat-fromℕ o n (≤-pred (≤∧≢⇒< p ¬eq))) ⟧
    -- mysterious agda bug, this refl must stay here
    ≡⟨ refl ⟩
        suc ⟦ fromNat {cont = cont} (Nat-fromℕ o n (≤-pred (≤∧≢⇒< p ¬eq))) ⟧
    ≡⟨ cong suc (toℕ-fromNat b d o cont n (≤-pred (≤∧≢⇒< p ¬eq))) ⟩
        suc n
    ∎
-- -- a partial function that only maps ℕ to Continuous Nums
-- fromℕ : ∀ {b d o}
--     → {cond : N+Closed b d o}
--     → ℕ
--     → Num b (suc d) o
-- fromℕ {cond = cond} zero = z ∙
-- fromℕ {cond = cond} (suc n) = {!   !}

-- fromℕ {cont = cont} zero = z ∙
-- fromℕ {cont = cont} (suc n) = 1+ {cont = cont} (fromℕ {cont = cont} n)

-- toℕ-fromℕ : ∀ {b d o}
--     → {cont : True (Continuous? b (suc d) o)}
--     → (n : ℕ)
--     → ⟦ fromℕ {cont = cont} n ⟧ ≡ n + o
-- toℕ-fromℕ {_} {_} {_} {cont} zero = refl
-- toℕ-fromℕ {b} {d} {o} {cont} (suc n) =
--     begin
--         ⟦ 1+ {cont = cont} (fromℕ {cont = cont} n) ⟧
--     ≡⟨ 1+-toℕ {cont = cont} (fromℕ {cont = cont} n) ⟩
--         suc ⟦ fromℕ {cont = cont} n ⟧
--     ≡⟨ cong suc (toℕ-fromℕ {cont = cont} n) ⟩
--         suc (n + o)
--     ∎

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.BagAndSetEquality directly.
------------------------------------------------------------------------

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

module Data.List.Relation.BagAndSetEquality where

open import Data.List.Relation.Binary.BagAndSetEquality public

{-# WARNING_ON_IMPORT
"Data.List.Relation.BagAndSetEquality was deprecated in v1.0.
Use Data.List.Relation.Binary.BagAndSetEquality instead."
#-}


text:
open import Categories
open import Monads

module Monads.EM.Functors {a b}{C : Cat {a}{b}}(M : Monad C) where

open import Library
open import Functors
open import Monads.EM M

open Cat C
open Fun
open Monad M
open Alg
open AlgMorph

EML : Fun C EM
EML = record {
  OMap = λ X → record {
    acar  = T X;
    astr  = λ _ → bind;
    alaw1 = sym law2;
    alaw2 = law3};
  HMap = λ f → record {
    amor = bind (comp η f);
    ahom = λ {Z} {g} →
      proof
      comp (bind (comp η f)) (bind g)
      ≅⟨ sym law3 ⟩
      bind (comp (bind (comp η f)) g)
      ∎};
  fid = AlgMorphEq (
    proof
    bind (comp η iden)
    ≅⟨ cong bind idr ⟩
    bind η
    ≅⟨ law1 ⟩
    iden ∎);
  fcomp = λ {_}{_}{_}{f}{g} →
    AlgMorphEq (
      proof
      bind (comp η (comp f g))
      ≅⟨ cong bind (sym ass) ⟩
      bind (comp (comp η f) g)
      ≅⟨ cong (λ f → bind (comp f g)) (sym law2) ⟩
      bind (comp (comp (bind (comp η f)) η) g)
      ≅⟨ cong bind ass ⟩
      bind (comp (bind (comp η f)) (comp η g))
      ≅⟨ law3 ⟩
      comp (bind (comp η f)) (bind (comp η g))
      ∎)}

EMR : Fun EM C
EMR  = record {
  OMap  = acar;
  HMap  = amor;
  fid   = refl;
  fcomp = refl}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --no-positivity-check #-}
open import Prelude

module Implicits.Resolution.Undecidable.Resolution where

open import Data.Fin.Substitution
open import Implicits.Syntax
open import Implicits.Syntax.MetaType
open import Implicits.Substitutions
open import Extensions.ListFirst

infixl 4 _⊢ᵣ_ _⊢_↓_ _⟨_⟩=_

mutual
  data _⊢_↓_ {ν} (Δ : ICtx ν) : Type ν → SimpleType ν → Set where
    i-simp : ∀ a → Δ ⊢ simpl a ↓ a
    i-iabs : ∀ {ρ₁ ρ₂ a} → Δ ⊢ᵣ ρ₁ → Δ ⊢ ρ₂ ↓ a → Δ ⊢ ρ₁ ⇒ ρ₂ ↓ a
    i-tabs : ∀ {ρ a} b → Δ ⊢ ρ tp[/tp b ] ↓ a → Δ ⊢ ∀' ρ ↓ a

  -- implicit resolution is simply the first rule in the implicit context
  -- that yields the queried type
  _⟨_⟩=_ : ∀ {ν} → ICtx ν → SimpleType ν → Type ν → Set
  Δ ⟨ a ⟩= r = first r ∈ Δ ⇔ (λ r' → Δ ⊢ r' ↓ a)

  data _⊢ᵣ_ {ν} (Δ : ICtx ν) : Type ν → Set where
    r-simp : ∀ {τ ρ} → Δ ⟨ τ ⟩= ρ → Δ ⊢ᵣ simpl τ
    r-iabs : ∀ ρ₁ {ρ₂} → ρ₁ List.∷ Δ ⊢ᵣ ρ₂ → Δ ⊢ᵣ ρ₁ ⇒ ρ₂
    r-tabs : ∀ {ρ} → ictx-weaken Δ ⊢ᵣ ρ → Δ ⊢ᵣ ∀' ρ

_⊢ᵣ[_] : ∀ {ν} → (Δ : ICtx ν) → List (Type ν) → Set
_⊢ᵣ[_] Δ ρs = All (λ r → Δ ⊢ᵣ r) ρs


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Data.Natural where

open import Light.Level using (Level ; Setω)
open import Light.Library.Arithmetic using (Arithmetic)
open import Light.Package using (Package)
open import Light.Library.Relation.Binary
      using (SelfTransitive ; SelfSymmetric ; Reflexive)
open import Light.Library.Relation.Binary.Decidable using (DecidableSelfBinary)
import Light.Library.Relation.Decidable
open import Light.Library.Relation.Binary.Equality as ≈ using (_≈_)
open import Light.Library.Relation.Binary.Equality.Decidable using (DecidableSelfEquality)
open import Light.Library.Relation using (False)

record Dependencies : Setω where

record Library (dependencies : Dependencies) : Setω where
      field
            ℓ : Level
            ℕ : Set ℓ
            ⦃ equals ⦄ : DecidableSelfEquality ℕ
            zero : ℕ
            successor : ℕ → ℕ
            predecessor : ∀ (a : ℕ) ⦃ a‐≉‐0 : False (a ≈ zero) ⦄ → ℕ
            _+_ _∗_ _//_ _∸_ : ℕ → ℕ → ℕ
            ⦃ ≈‐transitive ⦄ : SelfTransitive (≈.self‐relation ℕ)
            ⦃ ≈‐symmetric ⦄ : SelfSymmetric (≈.self‐relation ℕ)
            ⦃ ≈‐reflexive ⦄ : Reflexive (≈.self‐relation ℕ)

      instance arithmetic : Arithmetic ℕ
      arithmetic = record { _+_ = _+_ ; _∗_ = _∗_ }
open Library ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An either-or-both data type
------------------------------------------------------------------------

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

module Data.These where

open import Level
open import Data.Maybe.Base using (Maybe; just; nothing; maybe′)
open import Data.Sum.Base using (_⊎_; [_,_]′)
open import Function

------------------------------------------------------------------------
-- Re-exporting the datatype and its operations

open import Data.These.Base public

private
  variable
    a b : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Additional operations

-- projections

fromThis : These A B → Maybe A
fromThis = fold just (const nothing) (const ∘′ just)

fromThat : These A B → Maybe B
fromThat = fold (const nothing) just (const just)

leftMost : These A A → A
leftMost = fold id id const

rightMost : These A A → A
rightMost = fold id id (flip const)

mergeThese : (A → A → A) → These A A → A
mergeThese = fold id id

-- deletions

deleteThis : These A B → Maybe (These A B)
deleteThis = fold (const nothing) (just ∘′ that) (const (just ∘′ that))

deleteThat : These A B → Maybe (These A B)
deleteThat = fold (just ∘′ this) (const nothing) (const ∘′ just ∘′ this)