text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Field.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP
open import Cubical.Relation.Nullary

open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Data.Empty

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring
  hiding (_$_)
open import Cubical.Algebra.CommRing

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open Iso

private
  variable
    ℓ ℓ' : Level

record IsField {R : Type ℓ}
                  (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
                  (_[_]⁻¹ : (x : R) → ¬ (x ≡ 0r) → R) : Type ℓ where

  constructor isfield

  field
    isCommRing : IsCommRing 0r 1r _+_ _·_ -_
    ·⁻¹≡1      : (x : R) (≢0 : ¬ (x ≡ 0r)) → x · (x [ ≢0 ]⁻¹) ≡ 1r
    0≢1        : ¬ (0r ≡ 1r)

  open IsCommRing isCommRing public

record FieldStr (A : Type ℓ) : Type (ℓ-suc ℓ) where

  constructor fieldstr

  field
    0r         : A
    1r         : A
    _+_        : A → A → A
    _·_        : A → A → A
    -_         : A → A
    _[_]⁻¹     : (x : A) → ¬ (x ≡ 0r) → A
    isField    : IsField 0r 1r _+_ _·_ -_ _[_]⁻¹

  infix  8 -_
  infixl 7 _·_
  infixl 6 _+_

  open IsField isField public

Field : ∀ ℓ → Type (ℓ-suc ℓ)
Field ℓ = TypeWithStr ℓ FieldStr

isSetField : (R : Field ℓ) → isSet ⟨ R ⟩
isSetField R = R .snd .FieldStr.isField .IsField.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

makeIsField : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R}
                 {_[_]⁻¹ : (x : R) → ¬ (x ≡ 0r) → R}
                 (is-setR : isSet R)
                 (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
                 (+-rid : (x : R) → x + 0r ≡ x)
                 (+-rinv : (x : R) → x + (- x) ≡ 0r)
                 (+-comm : (x y : R) → x + y ≡ y + x)
                 (·-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
                 (·-rid : (x : R) → x · 1r ≡ x)
                 (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
                 (·-comm : (x y : R) → x · y ≡ y · x)
                 (·⁻¹≡1 : (x : R) (≢0 : ¬ (x ≡ 0r)) → x · (x [ ≢0 ]⁻¹) ≡ 1r)
                 (0≢1 : ¬ (0r ≡ 1r))
               → IsField 0r 1r _+_ _·_ -_ _[_]⁻¹
makeIsField {_+_ = _+_} is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-rdist-+ ·-comm ·⁻¹≡1 0≢1 =
  isfield (makeIsCommRing is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-rdist-+ ·-comm) ·⁻¹≡1 0≢1

makeField : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) (_[_]⁻¹ : (x : R) → ¬ (x ≡ 0r) → R)
                 (is-setR : isSet R)
                 (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
                 (+-rid : (x : R) → x + 0r ≡ x)
                 (+-rinv : (x : R) → x + (- x) ≡ 0r)
                 (+-comm : (x y : R) → x + y ≡ y + x)
                 (·-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
                 (·-rid : (x : R) → x · 1r ≡ x)
                 (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
                 (·-comm : (x y : R) → x · y ≡ y · x)
                 (·⁻¹≡1 : (x : R) (≢0 : ¬ (x ≡ 0r)) → x · (x [ ≢0 ]⁻¹) ≡ 1r)
                 (0≢1 : ¬ (0r ≡ 1r))
               → Field ℓ
makeField 0r 1r _+_ _·_ -_ _[_]⁻¹ is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-rdist-+ ·-comm ·⁻¹≡1 0≢1 =
  _ , fieldstr _ _ _ _ _ _ (makeIsField is-setR +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-rdist-+ ·-comm ·⁻¹≡1 0≢1)

FieldStr→CommRingStr : {A : Type ℓ} → FieldStr A → CommRingStr A
FieldStr→CommRingStr (fieldstr _ _ _ _ _ _ H) = commringstr _ _ _ _ _ (IsField.isCommRing H)

Field→CommRing : Field ℓ → CommRing ℓ
Field→CommRing (_ , fieldstr _ _ _ _ _ _ H) = _ , commringstr _ _ _ _ _ (IsField.isCommRing H)

record IsFieldHom {A : Type ℓ} {B : Type ℓ'} (R : FieldStr A) (f : A → B) (S : FieldStr B)
  : Type (ℓ-max ℓ ℓ')
  where

  -- Shorter qualified names
  private
    module R = FieldStr R
    module S = FieldStr S

  field
    pres0  : f R.0r ≡ S.0r
    pres1  : f R.1r ≡ S.1r
    pres+  : (x y : A) → f (x R.+ y) ≡ f x S.+ f y
    pres·  : (x y : A) → f (x R.· y) ≡ f x S.· f y
    pres-  : (x : A) → f (R.- x) ≡ S.- (f x)
    pres⁻¹ : (x : A) (≢0 : ¬ (x ≡ R.0r)) (f≢0 : ¬ (f x ≡ S.0r))  → f (x R.[ ≢0 ]⁻¹) ≡ ((f x) S.[ f≢0 ]⁻¹)

unquoteDecl IsFieldHomIsoΣ = declareRecordIsoΣ IsFieldHomIsoΣ (quote IsFieldHom)

FieldHom : (R : Field ℓ) (S : Field ℓ') → Type (ℓ-max ℓ ℓ')
FieldHom R S = Σ[ f ∈ (⟨ R ⟩ → ⟨ S ⟩) ] IsFieldHom (R .snd) f (S .snd)

IsFieldEquiv : {A : Type ℓ} {B : Type ℓ'}
  (R : FieldStr A) (e : A ≃ B) (S : FieldStr B) → Type (ℓ-max ℓ ℓ')
IsFieldEquiv R e S = IsFieldHom R (e .fst) S

FieldEquiv : (R : Field ℓ) (S : Field ℓ') → Type (ℓ-max ℓ ℓ')
FieldEquiv R S = Σ[ e ∈ (R .fst ≃ S .fst) ] IsFieldEquiv (R .snd) e (S .snd)

_$_ : {R S : Field ℓ} → (φ : FieldHom R S) → (x : ⟨ R ⟩) → ⟨ S ⟩
φ $ x = φ .fst x

FieldEquiv→FieldHom : {A B : Field ℓ} → FieldEquiv A B → FieldHom A B
FieldEquiv→FieldHom (e , eIsHom) = e .fst , eIsHom

isPropIsField : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) (_[_]⁻¹ : (x : R) → ¬ (x ≡ 0r) → R)
             → isProp (IsField 0r 1r _+_ _·_ -_ _[_]⁻¹)
isPropIsField 0r 1r _+_ _·_ -_ _[_]⁻¹ (isfield RR RC RD) (isfield SR SC SD) =
  λ i → isfield (isPropIsCommRing _ _ _ _ _ RR SR i)
                   (isPropInv RC SC i) (isProp→⊥ RD SD i)
  where
  isSetR : isSet _
  isSetR =  RR .IsCommRing.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropInv : isProp ((x : _) → (≢0 : ¬ (x ≡ 0r)) → x · (x [ ≢0 ]⁻¹) ≡ 1r)
  isPropInv = isPropΠ2 λ _ _ → isSetR _ _

  isProp→⊥ : ∀ {A : Type ℓ} → isProp (A → ⊥)
  isProp→⊥ = isPropΠ λ _ → isProp⊥

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
module Data.Vec.Any {a} {A : Set a} where
  open import Level using (_⊔_)
  open import Relation.Nullary
  open import Data.Fin
  open import Data.Nat as ℕ hiding (_⊔_)
  open import Data.Vec as Vec using (Vec; _∷_; [])
  open import Relation.Unary renaming (_⊆_ to _⋐_) using (Decidable)
  open import Function.Inverse using (_↔_)
  open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
  import Relation.Binary.PropositionalEquality as P
  open import Relation.Nullary using (¬_; yes; no)
  import Relation.Nullary.Decidable as Dec
  open import Data.Empty using (⊥-elim)
  open import Data.Product using (∃ ; ,_ )
  import Data.List.Any as ListAny

  data Any {p}(P : A → Set p) : ∀ {n} → Vec A n → Set (a ⊔ p) where
    here  : ∀ {n x}{xs : Vec A n} → P x → Any P (x ∷ xs)
    there : ∀ {n x}{xs : Vec A n} → Any P xs → Any P (x ∷ xs)
  open Any public

  map : ∀ {p q} {P : A → Set p} {Q : A → Set q} {n} {xs : Vec A n} →
    P ⋐ Q → Any P xs → Any Q xs
  map g (here px) =   here (g px)
  map g (there pxs) = there (map g pxs)

  tail : ∀ {p} {P : A → Set p}{x n} {xs : Vec A n} → ¬ P x → Any P (x ∷ xs) → Any P xs
  tail ¬px (here px) = ⊥-elim (¬px px)
  tail ¬px (there pxs) = pxs

  any :  ∀ {p} {P : A → Set p} → Decidable P → ∀ {n} → Decidable (Any P {n})
  any p [] = no λ()
  any p (x ∷ xs) with p x
  any p (x ∷ xs) | yes px = yes (here px)
  any p (x ∷ xs) | no ¬px = Dec.map′ there (tail ¬px) (any p xs)

  index : ∀ {p}{P : A → Set p}{n}{xs : Vec A n} → Any P xs → Fin n
  index (here px) = zero
  index (there pxs) = suc (index pxs)

  satisfied : ∀ {p}{P : A → Set p}{n}{xs : Vec A n} → Any P xs → ∃ P
  satisfied (here px) = , px
  satisfied (there pxs) = satisfied pxs

  Any↔ListAny : ∀ {p}{P : A → Set p}{n}{xs : Vec A n} →
    Any P xs ↔ ListAny.Any P (Vec.toList xs)
  Any↔ListAny {P = P} = record {
        to = P.→-to-⟶ to
      ; from =  P.→-to-⟶ from
      ; inverse-of = record {
            left-inverse-of = left-inverse
          ; right-inverse-of = right-inverse
        }
    }
    where
      to : ∀ {n}{xs : Vec A n} → Any P xs → ListAny.Any P (Vec.toList xs)
      to (here px) = ListAny.here px
      to (there pxs) = ListAny.there (to pxs)

      from : ∀ {n}{xs : Vec A n} → ListAny.Any P (Vec.toList xs) → Any P xs
      from {xs = []} ()
      from {xs = x ∷ xs} (ListAny.here px) = here px
      from {xs = x ∷ xs} (ListAny.there pxs) = there (from pxs)

      left-inverse : ∀ {n}{xs : Vec A n}(p : Any P xs) → from (to p) P.≡ p
      left-inverse (here px) = P.refl
      left-inverse (there pxs) = P.cong there (left-inverse pxs)

      right-inverse : ∀ {n}{xs : Vec A n}(p : ListAny.Any P (Vec.toList xs)) → to (from p) P.≡ p
      right-inverse {xs = []} ()
      right-inverse {xs = x ∷ xs} (ListAny.here px) = P.refl
      right-inverse {xs = x ∷ xs} (ListAny.there pxs) = P.cong ListAny.there (right-inverse pxs)

ext: agda

max_stars_repo_name: tizmd/agda-vector-any

max_issues_repo_name: tizmd/agda-vector-any

max_forks_repo_name: tizmd/agda-vector-any


text:
------------------------------------------------------------------------
-- Well-typed substitutions
------------------------------------------------------------------------

module Data.Fin.Substitution.Typed where

open import Data.Fin using (Fin; zero; suc)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Unit using (⊤; tt)
open import Data.Vec as Vec using (Vec; []; _∷_; map)
open import Data.Vec.All as All
  using (All; All₂; []; _∷_; map₂)
open import Data.Vec.All.Properties
  using (gmap; gmap₂; gmap₂₁; gmap₂₂)
open import Data.Vec.Properties using (lookup-map)
open import Function as Fun using (_∘_; flip)
open import Relation.Binary.PropositionalEquality as PropEq hiding (trans)
open PropEq.≡-Reasoning

------------------------------------------------------------------------
-- Abstract typing contexts and well-typedness relations

-- Abstract typing contexts over T-types.
--
-- A typing context Ctx T n maps n free variables to T-types
-- containing up to n free variables each.
module Context (T : ℕ → Set) where

  infixr 5 _∷_

  -- Typing contexts.
  data Ctx : ℕ → Set where
    []  :                       Ctx 0
    _∷_ : ∀ {n} → T n → Ctx n → Ctx (1 + n)

  -- Operations on contexts that require weakening of types.
  record WeakenOps : Set where

    -- Weakening of types.
    field weaken : ∀ {n} → T n → T (1 + n)

    -- Convert a context to its vector representation.
    toVec : ∀ {n} → Ctx n → Vec (T n) n
    toVec []      = []
    toVec (a ∷ Γ) = weaken a ∷ map weaken (toVec Γ)

    -- Lookup the type of a variable in a context.
    lookup : ∀ {n} → Fin n → Ctx n → T n
    lookup x = Vec.lookup x ∘ toVec

open Context

-- Abstract typings.
--
-- An abtract typing _⊢_∈_ : Typing Tp₁ Tm Tp₂ is a ternary relation
-- which, in a given Tp₁-context, relates Tm-terms to their Tp₂-types.
Typing : (ℕ → Set) → (ℕ → Set) → (ℕ → Set) → Set₁
Typing Tp₁ Tm Tp₂ = ∀ {n} → Ctx Tp₁ n → Tm n → Tp₂ n → Set

-- Abstract well-formedness.
--
-- An abtract well-formedness relation _⊢_wf : Wf Tp is a binary
-- relation which, in a given Tp-context, asserts the well-formedness
-- of Tp-types.
Wf : (ℕ → Set) → Set₁
Wf Tp = ∀ {n} → Ctx Tp n → Tp n → Set

-- Well-formed contexts.
--
-- A well-formed typing context (Γ wf) is a context Γ in which every
-- participating T-type is well-formed.
module WellFormedContext {T} (_⊢_wf : Wf T) where
  infix  4 _wf
  infixr 5 _∷_

  -- Well-formed typing contexts.
  data _wf : ∀ {n} → Ctx T n → Set where
    []  :                                              [] wf
    _∷_ : ∀ {n a} {Γ : Ctx T n} → Γ ⊢ a wf → Γ wf → a ∷ Γ wf

  -- Inversions.

  wf-∷₁ : ∀ {n} {Γ : Ctx T n} {a} → a ∷ Γ wf → Γ ⊢ a wf
  wf-∷₁ (a-wf ∷ _) = a-wf

  wf-∷₂ : ∀ {n} {Γ : Ctx T n} {a} → a ∷ Γ wf → Γ wf
  wf-∷₂ (_ ∷ Γ-wf) = Γ-wf

  -- Operations on well-formed contexts that require weakening of
  -- well-formedness judgments.
  record WfWeakenOps (weakenOps : WeakenOps T) : Set₁ where
    private module W = WeakenOps weakenOps

    field
      -- Weakening of well-formedness judgments.
      weaken : ∀ {n} {Γ : Ctx T n} {a b} → Γ ⊢ a wf → Γ ⊢ b wf →
               (a ∷ Γ) ⊢ W.weaken b wf

    -- Convert a well-formed context to its All representation.
    toAll : ∀ {n} {Γ : Ctx T n} → Γ wf → All (λ a → Γ ⊢ a wf) (W.toVec Γ)
    toAll []         = []
    toAll (a-wf ∷ Γ) = weaken a-wf a-wf ∷ gmap (weaken  a-wf) (toAll Γ)

    -- Lookup the well-formedness proof of a variable in a context.
    lookup : ∀ {n} {Γ : Ctx T n} → (x : Fin n) → Γ wf → Γ ⊢ (W.lookup x Γ) wf
    lookup x = All.lookup x ∘ toAll

-- Trivial well-formedness.
--
-- This module provides a trivial well-formedness relation and the
-- corresponding trivially well-formed contexts.  This is useful when
-- implmenting typed substitutions on types that either lack or do not
-- necessitate a notion well-formedness.
module ⊤-WellFormed {T} (weakenOps : WeakenOps T) where

  infix  4 _⊢_wf

  -- Trivial well-formedness.
  _⊢_wf : Wf T
  _ ⊢ _ wf = ⊤

  open WellFormedContext _⊢_wf public

  -- Trivial well-formedness of contexts.
  ctx-wf : ∀ {n} (Γ : Ctx T n) → Γ wf
  ctx-wf []      = []
  ctx-wf (a ∷ Γ) = tt ∷ ctx-wf Γ

  module ⊤-WfWeakenOps  where

    wfWeakenOps : WfWeakenOps weakenOps
    wfWeakenOps = record { weaken = λ _ _ → tt }

    open WfWeakenOps public

------------------------------------------------------------------------
-- Abstract well-typed substitutions (i.e. substitution lemmas)

-- Abstract typed substitutions.
record TypedSub (Tp₁ Tp₂ Tm : ℕ → Set) : Set₁ where

  infix 4 _⊢_∈_ _⊢_wf

  field
    _⊢_∈_ : Typing Tp₂ Tm Tp₁   -- the associated typing
    _⊢_wf : Wf Tp₂              -- Tp₂-well-formedness

    -- Application of Tm-substitutions to (source) Tp₁-types
    application : Application Tp₁ Tm

    -- Operations on the contexts.
    weakenOps : WeakenOps Tp₁

  open Application       application       public using (_/_)
  open WeakenOps         weakenOps                using (toVec)
  open WellFormedContext _⊢_wf             public

  infix  4 _⇒_⊢_
  infixr 4 _,_

  -- Typed substitutions.
  --
  -- A typed substitution Γ ⇒ Δ ⊢ σ is a substitution σ which, when
  -- applied to something that is well-typed in a source context Γ,
  -- yields something well-typed in a well-formed target context Δ.
  data _⇒_⊢_ {m n} (Γ : Ctx Tp₁ m) (Δ : Ctx Tp₂ n) : Sub Tm m n → Set where
    _,_ : ∀ {σ} → All₂ (λ t a → Δ ⊢ t ∈ (a / σ)) σ (toVec Γ) → Δ wf → Γ ⇒ Δ ⊢ σ

  -- Project out the first component of a typed substitution.
  proj₁ : ∀ {m n} {Γ : Ctx Tp₁ m} {Δ : Ctx Tp₂ n} {σ : Sub Tm m n} →
          Γ ⇒ Δ ⊢ σ → All₂ (λ t a → Δ ⊢ t ∈ (a / σ)) σ (toVec Γ)
  proj₁ (σ-wt , _) = σ-wt

-- Abstract extensions of substitutions.
record ExtensionTyped {Tp₁ Tp₂ Tm} (extension : Extension Tm)
                      (typedSub : TypedSub Tp₁ Tp₂ Tm) : Set where

  open TypedSub typedSub
  private
    module E  = Extension extension
    module C  = WeakenOps weakenOps

  field

    -- Weakens well-typed Tm-terms.
    weaken : ∀ {n} {Δ : Ctx Tp₂ n} {t a b} → Δ ⊢ a wf → Δ ⊢ t ∈ b →
             a ∷ Δ ⊢ E.weaken t ∈ C.weaken b

    -- Weakening commutes with other substitutions.
    weaken-/ : ∀ {m n} {σ : Sub Tm m n} {t} a →
               C.weaken (a / σ) ≡ C.weaken a / (t E./∷ σ)

    -- Well-typedness implies well-formedness of contexts.
    wt-wf : ∀ {n} {Γ : Ctx Tp₂ n} {t a} → Γ ⊢ t ∈ a → Γ wf

  infixr 5 _/∷_

  -- Extension by a typed term.
  _/∷_ : ∀ {m n} {Γ : Ctx Tp₁ m} {Δ : Ctx Tp₂ n} {t a b σ} →
         b ∷ Δ ⊢ t ∈ C.weaken (a / σ) → Γ ⇒ Δ ⊢ σ →
         a ∷ Γ ⇒ b ∷ Δ ⊢ (t E./∷ σ)
  t∈a/σ /∷ (σ-wt , _) = σ-wt′ , wt-wf t∈a/σ
    where
      b∷Δ-wf = wt-wf t∈a/σ
      b-wf   = wf-∷₁ b∷Δ-wf
      t∈a/σ′ = subst (_⊢_∈_ _ _) (weaken-/ _) t∈a/σ
      σ-wt′  =
        t∈a/σ′ ∷ gmap₂ (subst (_⊢_∈_ _ _) (weaken-/ _) ∘ weaken b-wf) σ-wt

-- Abstract simple typed substitutions.
record SimpleTyped {Tp Tm} (simple : Simple Tm)
                   (typedSub : TypedSub Tp Tp Tm) : Set where

  open TypedSub typedSub
  private
    module S  = SimpleExt simple
    module L₀ = Lemmas₀   (record { simple = simple })
    module C  = WeakenOps weakenOps

  field
    extensionTyped : ExtensionTyped (record { weaken = S.weaken }) typedSub

    -- Takes variables to well-typed Tms.
    var : ∀ {n} {Γ : Ctx Tp n} (x : Fin n) → Γ wf → Γ ⊢ S.var x ∈ C.lookup x Γ

    -- Types are invariant under the identity substitution.
    id-vanishes : ∀ {n} (a : Tp n) → a / S.id ≡ a

    -- Relates weakening of types to weakening of Tms.
    /-wk : ∀ {n} {a : Tp n} → a / S.wk ≡ C.weaken a

    -- Single-variable substitution is a left-inverse of weakening.
    wk-sub-vanishes : ∀ {n t} (a : Tp n) → a / S.wk / S.sub t ≡ a

    -- Well-formedness of types implies well-formedness of contexts.
    wf-wf : ∀ {n} {Γ : Ctx Tp n} {a} → Γ ⊢ a wf → Γ wf

  open ExtensionTyped extensionTyped public

  infixl 10 _↑_

  -- Lifting.
  _↑_ : ∀ {m n} {Γ : Ctx Tp m} {Δ : Ctx Tp n} {σ} → Γ ⇒ Δ ⊢ σ →
        ∀ {a} → Δ ⊢ a / σ wf → a ∷ Γ ⇒ a / σ ∷ Δ ⊢ σ S.↑
  (σ-wt , Δ-wf) ↑ a/σ-wf = var zero (a/σ-wf ∷ Δ-wf) /∷ (σ-wt , Δ-wf)

  -- The identity substitution.
  id : ∀ {n} {Γ : Ctx Tp n} → Γ wf → Γ ⇒ Γ ⊢ S.id
  id             []            = [] , []
  id {Γ = a ∷ Γ} (a-wf ∷ Γ-wf) =
    subst₂ (λ Δ σ → a ∷ Γ ⇒ Δ ⊢ σ)
           (cong (flip _∷_ Γ) (id-vanishes a)) (L₀.id-↑⋆ 1)
           (id Γ-wf ↑ subst (_⊢_wf Γ) (sym (id-vanishes a)) a-wf)

  -- The first component of the identity substitution.
  private
    id₁ : ∀ {n} {Γ : Ctx Tp n} → Γ wf →
          All₂ (λ t a → Γ ⊢ t ∈ (a / S.id)) S.id (C.toVec Γ)
    id₁ = proj₁ ∘ id

  -- Weakening.
  wk : ∀ {n} {Γ : Ctx Tp n} {a} → Γ ⊢ a wf → Γ ⇒ a ∷ Γ ⊢ S.wk
  wk a-wf =
    gmap₂₁ (weaken′ a-wf ∘ subst (_⊢_∈_ _ _) (id-vanishes _)) (id₁ Γ-wf) ,
      a-wf ∷ Γ-wf
    where
      weaken′ : ∀ {n} {Γ : Ctx Tp n} {t a b} → Γ ⊢ a wf → Γ ⊢ t ∈ b →
                a ∷ Γ ⊢ S.weaken t ∈ b / S.wk
      weaken′ a-wf = subst (_⊢_∈_ _ _) (sym /-wk) ∘ weaken a-wf

      Γ-wf = wf-wf a-wf

  -- Some helper lemmas.
  private
    wk-sub-vanishes′ : ∀ {n a} {t : Tm n} → a ≡ C.weaken a / S.sub t
    wk-sub-vanishes′ {a = a} {t} = begin
      a                      ≡⟨ sym (wk-sub-vanishes a) ⟩
      a / S.wk / S.sub t     ≡⟨ cong (flip _/_ _) /-wk ⟩
      C.weaken a / S.sub t   ∎

    id-wk-sub-vanishes : ∀ {n a} {t : Tm n} →
                         a / S.id ≡ C.weaken a / S.sub t
    id-wk-sub-vanishes {a = a} {t} = begin
      a / S.id               ≡⟨ id-vanishes a ⟩
      a                      ≡⟨ wk-sub-vanishes′ ⟩
      C.weaken a / S.sub t   ∎

  -- A substitution which only replaces the first variable.
  sub : ∀ {n} {Γ : Ctx Tp n} {t a} → Γ ⊢ t ∈ a → a ∷ Γ ⇒ Γ ⊢ S.sub t
  sub t∈a =
    t∈a′ ∷ gmap₂₂ (subst (_⊢_∈_ _ _) id-wk-sub-vanishes) (id₁ Γ-wf) , Γ-wf
    where
      Γ-wf = wt-wf t∈a
      t∈a′ = subst (_⊢_∈_ _ _) wk-sub-vanishes′ t∈a

  -- A substitution which only changes the type of the first variable.
  tsub : ∀ {n} {Γ : Ctx Tp n} {a b} → b ∷ Γ ⊢ S.var zero ∈ C.weaken a →
         a ∷ Γ ⇒ b ∷ Γ ⊢ S.id
  tsub z∈a = z∈a′ /∷ id (wf-∷₂ (wt-wf z∈a))
    where
      z∈a′ = subst (_⊢_∈_ _ _) (cong C.weaken (sym (id-vanishes _))) z∈a

-- Abstract typed liftings from Tm₁ to Tm₂.
record LiftTyped {Tp Tm₁ Tm₂} (l : Lift Tm₁ Tm₂)
                 (typedSub : TypedSub Tp Tp Tm₁)
                 (_⊢₂_∈_   : Typing Tp Tm₂ Tp)   : Set where

  open TypedSub typedSub renaming (_⊢_∈_ to _⊢₁_∈_)
  private module L = Lift l

  -- The underlying well-typed simple Tm₁-substitutions.
  field simpleTyped : SimpleTyped L.simple typedSub

  open SimpleTyped simpleTyped public

  -- Lifts well-typed Tm₁-terms to well-typed Tm₂-terms.
  field lift : ∀ {n} {Γ : Ctx Tp n} {t a} → Γ ⊢₁ t ∈ a → Γ ⊢₂ (L.lift t) ∈ a

-- Abstract variable typings.
module VarTyping {Tp} (weakenOps : WeakenOps Tp) (_⊢_wf : Wf Tp) where
  open WeakenOps weakenOps
  open WellFormedContext _⊢_wf

  infix 4 _⊢Var_∈_

  -- Abstract reflexive variable typings.
  data _⊢Var_∈_ {n} (Γ : Ctx Tp n) : Fin n → Tp n → Set where
    var : ∀ x → Γ wf → Γ ⊢Var x ∈ lookup x Γ

-- Abstract typed variable substitutions (renamings).
record TypedVarSubst {Tp} (_⊢_wf : Wf Tp) : Set where
  field
    application : Application Tp Fin
    weakenOps   : WeakenOps Tp

  open WellFormedContext   _⊢_wf
  open VarTyping weakenOps _⊢_wf public

  typedSub : TypedSub Tp Tp Fin
  typedSub = record
    { _⊢_∈_       = _⊢Var_∈_
    ; _⊢_wf       = _⊢_wf
    ; application = application
    ; weakenOps   = weakenOps
    }

  open TypedSub typedSub public using () renaming (_⇒_⊢_ to _⇒_⊢Var_)

  open Application application       using (_/_)
  open Lemmas₄     VarLemmas.lemmas₄ using (id; wk; _⊙_)
  private module C = WeakenOps weakenOps

  field
    /-wk        : ∀ {n} {a : Tp n} → a / wk ≡ C.weaken a
    id-vanishes : ∀ {n} (a : Tp n) → a / id ≡ a
    /-⊙         : ∀ {m n k} {σ₁ : Sub Fin m n} {σ₂ : Sub Fin n k} a →
                  a / σ₁ ⊙ σ₂ ≡ a / σ₁ / σ₂
    wf-wf       : ∀ {n} {Γ : Ctx Tp n} {a} → Γ ⊢ a wf → Γ wf

  appLemmas : AppLemmas Tp Fin
  appLemmas = record
    { application = application
    ; lemmas₄     = VarLemmas.lemmas₄
    ; id-vanishes = id-vanishes
    ; /-⊙         = /-⊙
    }

  open ExtAppLemmas appLemmas using (wk-commutes; wk-sub-vanishes)
  open SimpleExt VarLemmas.simple using (extension; _/∷_)

  -- Extensions of renamings.
  extensionTyped : ExtensionTyped extension typedSub
  extensionTyped = record
    { weaken   = weaken
    ; weaken-/ = weaken-/
    ; wt-wf    = wt-wf
    }
    where
      weaken : ∀ {n} {Γ : Ctx Tp n} {x a b} → Γ ⊢ a wf → Γ ⊢Var x ∈ b →
               a ∷ Γ ⊢Var suc x ∈ C.weaken b
      weaken a-wf (var x Γ-wf) =
        subst (_⊢Var_∈_ _ _) (lookup-map x _ _)
              (var (suc x) (a-wf ∷ Γ-wf))

      weaken-/ : ∀ {m n} {σ : Sub Fin m n} {t} a →
                 C.weaken (a / σ) ≡ C.weaken a / (t /∷ σ)
      weaken-/ {σ = σ} {t} a = begin
        C.weaken (a / σ)        ≡⟨ sym /-wk ⟩
        a / σ / wk              ≡⟨ wk-commutes a ⟩
        a / wk / (t /∷ σ)       ≡⟨ cong₂ _/_ /-wk refl ⟩
        C.weaken a / (t /∷ σ)   ∎

      wt-wf : ∀ {n} {Γ : Ctx Tp n} {x a} → Γ ⊢Var x ∈ a → Γ wf
      wt-wf (var x Γ-wf) = Γ-wf

  -- Simple typed renamings.
  simpleTyped : SimpleTyped VarLemmas.simple typedSub
  simpleTyped = record
    { extensionTyped  = extensionTyped
    ; var             = var
    ; id-vanishes     = id-vanishes
    ; /-wk            = /-wk
    ; wk-sub-vanishes = wk-sub-vanishes
    ; wf-wf           = wf-wf
    }

  open SimpleTyped simpleTyped public
    hiding (extensionTyped; var; /-wk; id-vanishes; wk-sub-vanishes; wf-wf)

max_stars_repo_name: asr/pts-agda

max_issues_repo_name: asr/pts-agda

max_forks_repo_name: asr/pts-agda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Idlemmas {{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.MaybeEmbed
open import Definition.LogicalRelation.Substitution.Introductions.Cast
-- open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.Introductions.Universe

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

[proj₁cast] : ∀ {A B Γ r}
         (⊢Γ : ⊢ Γ)
         ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ [ r , ι ⁰ ])
         ([B] : Γ ⊩⟨ ι ⁰ ⟩ B ^ [ r , ι ⁰ ])
       → (∀ {t e} → ([t] : Γ ⊩⟨ ι ⁰ ⟩ t ∷ A ^ [ r , ι ⁰ ] / [A]) → (⊢e : Γ ⊢ e ∷ Id (Univ r ⁰) A B ^ [ % , ι ¹ ]) → Γ ⊩⟨ ι ⁰ ⟩ cast ⁰ A B e t ∷ B ^ [ r , ι ⁰ ] / [B])
[proj₁cast] ⊢Γ [A] [B] = proj₁ ([cast] ⊢Γ [A] [B])

[proj₁castext] : ∀ {A A′ B B′ Γ r}
         (⊢Γ : ⊢ Γ)
         ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ [ r , ι ⁰ ])
         ([A′] : Γ ⊩⟨ ι ⁰ ⟩ A′ ^ [ r , ι ⁰ ])
         ([A≡A′] : Γ ⊩⟨ ι ⁰ ⟩ A ≡ A′ ^ [ r , ι ⁰ ] / [A])
         ([B] : Γ ⊩⟨ ι ⁰ ⟩ B ^ [ r , ι ⁰ ])
         ([B′] : Γ ⊩⟨ ι ⁰ ⟩ B′ ^ [ r , ι ⁰ ])
         ([B≡B′] : Γ ⊩⟨ ι ⁰ ⟩ B ≡ B′ ^ [ r , ι ⁰ ] / [B])
       → (∀ {t t′ e e′} → ([t] : Γ ⊩⟨ ι ⁰ ⟩ t ∷ A ^ [ r , ι ⁰ ] / [A])
                        → ([t′] : Γ ⊩⟨ ι ⁰ ⟩ t′ ∷ A′ ^ [ r , ι ⁰ ] / [A′])
                        → ([t≡t′] : Γ ⊩⟨ ι ⁰ ⟩ t ≡ t′ ∷ A ^ [ r , ι ⁰ ] / [A])
                        → (⊢e : Γ ⊢ e ∷ Id (Univ r ⁰) A B ^ [ % , ι ¹ ])
                        → (⊢e′ : Γ ⊢ e′ ∷ Id (Univ r ⁰) A′ B′ ^ [ % , ι ¹ ])
                        → Γ ⊩⟨ ι ⁰ ⟩ cast ⁰ A B e t ≡ cast ⁰ A′ B′ e′ t′ ∷ B ^ [ r , ι ⁰ ] / [B])
[proj₁castext] ⊢Γ [A] [A′] [A≡A′] [B] [B′] [B≡B′] = proj₁ ([castext] ⊢Γ [A] [A′] [A≡A′] [B] [B′] [B≡B′])

[nondep] : ∀ {Γ A B l} → Γ ⊩⟨ l ⟩ B ^ [ % , l ]
  → ([A] : ∀ {ρ} {Δ} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ) → Δ ⊩⟨ l ⟩ wk ρ A ^ [ % , l ])
  → ∀ {ρ} {Δ} {a} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ)
  → ([a] : Δ ⊩⟨ l ⟩ a ∷ wk ρ A ^ [ % , l ] / [A] [ρ] ⊢Δ)
  → Δ ⊩⟨ l ⟩ wk (lift ρ) (wk1 B) [ a ] ^ [ % , l ]
[nondep] {Γ} {A} {B} {l} [B] [A] {ρ} {Δ} {a} [ρ] ⊢Δ [a] = PE.subst (λ X → Δ ⊩⟨ l ⟩ X ^ [ % , l ]) (Id-subst-lemma ρ B a) (Lwk.wk [ρ] ⊢Δ [B])

[nondepext] : ∀ {Γ A B l} → ([B] : Γ ⊩⟨ l ⟩ B ^ [ % , l ])
  → ([A] : ∀ {ρ} {Δ} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ) → Δ ⊩⟨ l ⟩ wk ρ A ^ [ % , l ])
  → ∀ {ρ} {Δ} {a} {b} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ)
  → ([a] : Δ ⊩⟨ l ⟩ a ∷ wk ρ A ^ [ % , l ] / [A] [ρ] ⊢Δ)
  → ([b] : Δ ⊩⟨ l ⟩ b ∷ wk ρ A ^ [ % , l ] / [A] [ρ] ⊢Δ)
  → ([a≡b] : Δ ⊩⟨ l ⟩ a ≡ b ∷ wk ρ A ^ [ % , l ] / [A] [ρ] ⊢Δ)
  → Δ ⊩⟨ l ⟩ wk (lift ρ) (wk1 B) [ a ] ≡ wk (lift ρ) (wk1 B) [ b ] ^ [ % , l ] / [nondep] [B] [A] [ρ] ⊢Δ [a]
[nondepext] {Γ} {A} {B} {l} [B] [A] {ρ} {Δ} {a} {b} [ρ] ⊢Δ [a] [b] [a≡b] =
  irrelevanceEq″ (Id-subst-lemma ρ B a) (Id-subst-lemma ρ B b) PE.refl PE.refl
    (Lwk.wk [ρ] ⊢Δ [B]) ([nondep] [B] [A] [ρ] ⊢Δ [a]) (reflEq (Lwk.wk [ρ] ⊢Δ [B]))

[nondepext'] : ∀ {Γ A A' B B' l}
  → ([B] : Γ ⊩⟨ l ⟩ B ^ [ % , l ])
  → ([B'] : Γ ⊩⟨ l ⟩ B' ^ [ % , l ])
  → ([B≡B'] : Γ ⊩⟨ l ⟩ B ≡ B' ^ [ % , l ] / [B])
  → ([A] : ∀ {ρ} {Δ} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ) → Δ ⊩⟨ l ⟩ wk ρ A ^ [ % , l ])
  → ([A'] : ∀ {ρ} {Δ} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ) → Δ ⊩⟨ l ⟩ wk ρ A' ^ [ % , l ])
  → ∀ {ρ} {Δ} {a} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ)
  → ([a] : Δ ⊩⟨ l ⟩ a ∷ wk ρ A ^ [ % , l ] / [A] [ρ] ⊢Δ)
  → Δ ⊩⟨ l ⟩ wk (lift ρ) (wk1 B) [ a ] ≡ wk (lift ρ) (wk1 B') [ a ] ^ [ % , l ] / [nondep] [B] [A] [ρ] ⊢Δ [a]
[nondepext'] {Γ} {A} {A'} {B} {B'} {l} [B] [B'] [B≡B'] [A] [A'] {ρ} {Δ} {a} [ρ] ⊢Δ [a] =
  irrelevanceEq″ (Id-subst-lemma ρ B a) (Id-subst-lemma ρ B' a) PE.refl PE.refl
    (Lwk.wk [ρ] ⊢Δ [B]) ([nondep] [B] [A] [ρ] ⊢Δ [a]) (Lwk.wkEq [ρ] ⊢Δ [B] [B≡B'])

module IdTypeU-lemmas
       {Γ rF A B F 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₁ ^ [ ! , ι ⁰ ])
       (B≡B  : Γ ⊢ (Π 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])))
       (recursor₁ : ∀ {ρ Δ}
          ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          → Δ ⊩⟨ ι ¹ ⟩ Id (Univ rF ⁰) (wk ρ F) (wk ρ F₁) ^ [ % , ι ¹ ])
       (recursor₂ : ∀ {ρ Δ x y}
          ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F ^ [ rF , ι ⁰ ] / [F] [ρ] ⊢Δ)
          ([y] : Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
          → Δ ⊩⟨ ι ¹ ⟩ Id (U ⁰) (wk (lift ρ) G [ x ]) (wk (lift ρ) G₁ [ y ]) ^ [ % , ι ¹ ])
       (extrecursor : ∀ {ρ Δ x y x′ y′}
          ([ρ] : ρ 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₁] [ρ] ⊢Δ)
          → Δ ⊩⟨ ι ¹ ⟩ Id (U ⁰) (wk (lift ρ) G [ x ]) (wk (lift ρ) G₁ [ y ]) ≡ Id (U ⁰) (wk (lift ρ) G [ x′ ]) (wk (lift ρ) G₁ [ y′ ]) ^ [ % , ι ¹ ] / recursor₂ [ρ] ⊢Δ [x] [y])
  where
    ⊢IdFF₁ : Γ ⊢ Id (Univ rF ⁰) F F₁ ^ [ % , ι ¹ ]
    ⊢IdFF₁ = univ (Idⱼ (univ 0<1 ⊢Γ) (un-univ ⊢F) (un-univ ⊢F₁))

    [IdFF₁] : ∀ {ρ Δ} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ) → Δ ⊩⟨ ι ¹ ⟩ wk ρ (Id (Univ rF ⁰) F F₁) ^ [ % , ι ¹ ]
    [IdFF₁] [ρ] ⊢Δ = recursor₁ [ρ] ⊢Δ

    b = λ ρ e x → cast ⁰ (wk ρ F₁) (wk ρ F) (Idsym (Univ rF ⁰) (wk ρ F) (wk ρ F₁) e) x
    IdGG₁ = λ ρ e → Π (wk ρ F₁) ^ rF ° ⁰ ▹ Id (U ⁰) (wk (lift (step ρ)) G [ b (step ρ) (wk1 e) (var 0) ]) (wk (lift ρ) G₁) ° ¹ ° ¹

    abstract
      IdTel₂-prettify : ∀ ρ₁ ρ e a → wk (lift ρ₁) (Id (U ⁰) (wk (lift (step ρ)) G [ b (step ρ) (wk1 e) (var 0) ]) (wk (lift ρ) G₁)) [ a ]
        PE.≡ Id (U ⁰) (wk (lift (ρ₁ • ρ)) G [ b (ρ₁ • ρ) (wk ρ₁ e) a ]) (wk (lift (ρ₁ • ρ)) G₁ [ a ])
      IdTel₂-prettify ρ₁ ρ e a = let
          x₂ = PE.trans (PE.cong (subst (sgSubst a)) (wk-Idsym (lift ρ₁) (Univ rF ⁰) (wk (step ρ) F) (wk (step ρ) F₁) (wk1 e)))
            (PE.trans (subst-Idsym (sgSubst a) (Univ rF ⁰) (wk _ (wk (step ρ) F)) (wk _ (wk (step ρ) F₁)) (wk _ (wk1 e)))
              (PE.cong₃ (λ X Y Z → Idsym (Univ rF ⁰) X Y Z) (Id-subst-lemma4 ρ ρ₁ F a) (Id-subst-lemma4 ρ ρ₁ F₁ a) (irrelevant-subst′ ρ₁ e a)))
          x₁ = PE.cong₂ (λ X Y → X [ Y ]) (Id-subst-lemma3 ρ ρ₁ G a) (PE.cong₃ (λ X Y Z → cast ⁰ X Y Z a) (Id-subst-lemma4 ρ ρ₁ F₁ a) ((Id-subst-lemma4 ρ ρ₁ F a)) x₂)
          x = PE.trans (PE.cong (λ X → X [ a ]) (wk-β (wk (lift (step ρ)) G)))
            (PE.trans (singleSubstLift (wk (lift (lift ρ₁)) (wk (lift (step ρ)) G)) (wk (lift ρ₁) (b (step ρ) (wk1 e) (var 0)))) x₁)
        in PE.cong₂ (λ X Y → Id (U ⁰) X Y) x (PE.cong (λ X → X [ a ]) (wk-comp (lift ρ₁) (lift ρ) G₁))

    abstract
      [Id] : ∀ {ρ Δ e} →([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ)
        → ([e] : Δ ⊩⟨ ι ¹ ⟩ e ∷ wk ρ (Id (Univ rF ⁰) F F₁) ^ [ % , ι ¹ ] / [IdFF₁] [ρ] ⊢Δ)
        → ∀ {ρ₁ Δ₁ a} → ([ρ₁] : ρ₁ Twk.∷ Δ₁ ⊆ Δ) → (⊢Δ₁ : ⊢ Δ₁)
        → ([a] : Δ₁ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ₁ (wk ρ F₁) ^ [ rF , ι ⁰ ] / (Lwk.wk [ρ₁] ⊢Δ₁ ([F₁] [ρ] ⊢Δ)))
        → Δ₁ ⊩⟨ ι ¹ ⟩ wk (lift ρ₁) (Id (U ⁰) (wk (lift (step ρ)) G [ b (step ρ) (wk1 e) (var 0) ]) (wk (lift ρ) G₁)) [ a ] ^ [ % , ι ¹ ]
      [Id] {ρ} {Δ} {e} [ρ] ⊢Δ [e] {ρ₁} {Δ₁} {a} [ρ₁] ⊢Δ₁ [a] =
        let
          [a] : Δ₁ ⊩⟨ ι ⁰ ⟩ a ∷ wk (ρ₁ • ρ) F₁ ^ [ rF , ι ⁰ ] / [F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁
          [a] = irrelevanceTerm′ (wk-comp ρ₁ ρ F₁) PE.refl PE.refl (Lwk.wk [ρ₁] ⊢Δ₁ ([F₁] [ρ] ⊢Δ)) ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) [a]
          ⊢e″ = PE.subst (λ X → Δ₁ ⊢ wk ρ₁ e ∷ X ^ [ % , ι ¹ ]) (wk-comp ρ₁ ρ _) (Twk.wkTerm [ρ₁] ⊢Δ₁ (escapeTerm ([IdFF₁] [ρ] ⊢Δ) [e]))
          ⊢e′ = Idsymⱼ (univ 0<1 ⊢Δ₁) (un-univ (escape ([F] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁))) (un-univ (escape ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁))) ⊢e″
          [b] : Δ₁ ⊩⟨ ι ⁰ ⟩ b (ρ₁ • ρ) (wk ρ₁ e) a ∷ wk (ρ₁ • ρ) F ^ [ rF , ι ⁰ ] / [F] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁
          [b] = [proj₁cast] ⊢Δ₁ ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) ([F] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) [a] ⊢e′
          x = recursor₂ ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁ [b] [a]
        in PE.subst (λ X → Δ₁ ⊩⟨ ι ¹ ⟩ X ^ [ % , ι ¹ ]) (PE.sym (IdTel₂-prettify ρ₁ ρ e a)) x

    abstract
      [Idext] : ∀ {ρ Δ e e′} →([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ)
        → ([e] : Δ ⊩⟨ ι ¹ ⟩ e ∷ wk ρ (Id (Univ rF ⁰) F F₁) ^ [ % , ι ¹ ] / [IdFF₁] [ρ] ⊢Δ)
        → ([e′] : Δ ⊩⟨ ι ¹ ⟩ e′ ∷ wk ρ (Id (Univ rF ⁰) F F₁) ^ [ % , ι ¹ ] / [IdFF₁] [ρ] ⊢Δ)
        → ∀ {ρ₁ Δ₁ a a′} → ([ρ₁] : ρ₁ Twk.∷ Δ₁ ⊆ Δ) → (⊢Δ₁ : ⊢ Δ₁)
        → ([a] : Δ₁ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ₁ (wk ρ F₁) ^ [ rF , ι ⁰ ] / (Lwk.wk [ρ₁] ⊢Δ₁ ([F₁] [ρ] ⊢Δ)))
        → ([a′] : Δ₁ ⊩⟨ ι ⁰ ⟩ a′ ∷ wk ρ₁ (wk ρ F₁) ^ [ rF , ι ⁰ ] / (Lwk.wk [ρ₁] ⊢Δ₁ ([F₁] [ρ] ⊢Δ)))
        → ([a≡a′] : Δ₁ ⊩⟨ ι ⁰ ⟩ a ≡ a′ ∷ wk ρ₁ (wk ρ F₁) ^ [ rF , ι ⁰ ] / (Lwk.wk [ρ₁] ⊢Δ₁ ([F₁] [ρ] ⊢Δ)))
        → Δ₁ ⊩⟨ ι ¹ ⟩ wk (lift ρ₁) (Id (U ⁰) (wk (lift (step ρ)) G [ b (step ρ) (wk1 e) (var 0) ]) (wk (lift ρ) G₁)) [ a ]
             ≡ wk (lift ρ₁) (Id (U ⁰) (wk (lift (step ρ)) G [ b (step ρ) (wk1 e′) (var 0) ]) (wk (lift ρ) G₁)) [ a′ ] ^ [ % , ι ¹ ]
             / [Id] [ρ] ⊢Δ [e] [ρ₁] ⊢Δ₁ [a]
      [Idext] {ρ} {Δ} {e} {e′} [ρ] ⊢Δ [e] [e′] {ρ₁} {Δ₁} {a} {a′} [ρ₁] ⊢Δ₁ [a] [a′] [a≡a′] =
        let
          [a]₁ : Δ₁ ⊩⟨ ι ⁰ ⟩ a ∷ wk (ρ₁ • ρ) F₁ ^ [ rF , ι ⁰ ] / [F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁
          [a]₁ = irrelevanceTerm′ (wk-comp ρ₁ ρ F₁) PE.refl PE.refl (Lwk.wk [ρ₁] ⊢Δ₁ ([F₁] [ρ] ⊢Δ)) ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) [a]
          [a′] = irrelevanceTerm′ (wk-comp ρ₁ ρ F₁) PE.refl PE.refl (Lwk.wk [ρ₁] ⊢Δ₁ ([F₁] [ρ] ⊢Δ)) ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) [a′]
          [a≡a′] = irrelevanceEqTerm′ (wk-comp ρ₁ ρ F₁) PE.refl PE.refl (Lwk.wk [ρ₁] ⊢Δ₁ ([F₁] [ρ] ⊢Δ)) ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) [a≡a′]
          ⊢e₂ = PE.subst (λ X → Δ₁ ⊢ wk ρ₁ e ∷ X ^ [ % , ι ¹ ]) (wk-comp ρ₁ ρ _) (Twk.wkTerm [ρ₁] ⊢Δ₁ (escapeTerm ([IdFF₁] [ρ] ⊢Δ) [e]))
          ⊢e₁ = Idsymⱼ (univ 0<1 ⊢Δ₁) (un-univ (escape ([F] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁))) (un-univ (escape ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁))) ⊢e₂
          ⊢e′₂ = PE.subst (λ X → Δ₁ ⊢ wk ρ₁ e′ ∷ X ^ [ % , ι ¹ ]) (wk-comp ρ₁ ρ _) (Twk.wkTerm [ρ₁] ⊢Δ₁ (escapeTerm ([IdFF₁] [ρ] ⊢Δ) [e′]))
          ⊢e′₁ = Idsymⱼ (univ 0<1 ⊢Δ₁) (un-univ (escape ([F] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁))) (un-univ (escape ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁))) ⊢e′₂
          [b] : Δ₁ ⊩⟨ ι ⁰ ⟩ b (ρ₁ • ρ) (wk ρ₁ e) a ∷ wk (ρ₁ • ρ) F ^ [ rF , ι ⁰ ] / [F] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁
          [b] = [proj₁cast] ⊢Δ₁ ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) ([F] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) [a]₁ ⊢e₁
          [b′] = [proj₁cast] ⊢Δ₁ ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) ([F] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) [a′] ⊢e′₁
          [b≡b′] = [proj₁castext] ⊢Δ₁ ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) (reflEq ([F₁] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁))
            ([F] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) ([F] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁) (reflEq ([F] ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁))
            [a]₁ [a′] [a≡a′] ⊢e₁ ⊢e′₁
          x₁ = recursor₂ ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁ [b] [a]₁
          x = extrecursor ([ρ₁] Twk.•ₜ [ρ]) ⊢Δ₁ [b] [b′] [b≡b′] [a]₁ [a′] [a≡a′]
        in irrelevanceEq″ (PE.sym (IdTel₂-prettify ρ₁ ρ e a)) (PE.sym (IdTel₂-prettify ρ₁ ρ e′ a′)) PE.refl PE.refl x₁ ([Id] [ρ] ⊢Δ [e] [ρ₁] ⊢Δ₁ [a]) x

    [IdGG₁] : ∀ {ρ Δ e} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ)
      → ([e] : Δ ⊩⟨ ι ¹ ⟩ e ∷ wk ρ (Id (Univ rF ⁰) F F₁) ^ [ % , ι ¹ ] / [IdFF₁] [ρ] ⊢Δ)
      → Δ ⊩⟨ ι ¹ ⟩ IdGG₁ ρ e ^ [ % , ι ¹ ]
    [IdGG₁] {ρ} {Δ} {e} [ρ] ⊢Δ [e] =
      let
        ⊢wkF₁ = escape ([F₁] [ρ] ⊢Δ)
        [0] = let ⊢0 = (var (⊢Δ ∙ ⊢wkF₁) here) in
          neuTerm (Lwk.wk (Twk.step Twk.id) (⊢Δ ∙ escape ([F₁] [ρ] ⊢Δ)) ([F₁] [ρ] ⊢Δ)) (var 0) ⊢0 (~-var ⊢0)
        x : Δ ∙ wk ρ F₁ ^ [ rF , ι ⁰ ] ⊩⟨ ι ¹ ⟩ Id (U ⁰) (wk (lift (step ρ)) G [ b (step ρ) (wk1 e) (var 0) ]) (wk (lift ρ) G₁) ^ [ % , ι ¹ ]
        x = PE.subst (λ X → Δ ∙ wk ρ F₁ ^ [ rF , ι ⁰ ] ⊩⟨ ι ¹ ⟩ X ^ [ % , ι ¹ ]) (wkSingleSubstId _) ([Id] [ρ] ⊢Δ [e] (Twk.step Twk.id) (⊢Δ ∙ ⊢wkF₁) [0])
        ⊢Id = escape x
      in
      Πᵣ′ rF ⁰ ¹ (<is≤ 0<1) (≡is≤ PE.refl) (wk ρ F₁) (Id (U ⁰) (wk (lift (step ρ)) G [ b (step ρ) (wk1 e) (var 0) ]) (wk (lift ρ) G₁))
        (idRed:*: (univ (Πⱼ <is≤ 0<1 ▹ ≡is≤ PE.refl ▹ un-univ ⊢wkF₁ ▹ un-univ ⊢Id)))
        ⊢wkF₁ ⊢Id (≅-univ (≅ₜ-Π-cong (<is≤ 0<1) (≡is≤ PE.refl) ⊢wkF₁ (≅-un-univ (escapeEqRefl ([F₁] [ρ] ⊢Δ))) (≅-un-univ (escapeEqRefl x))))
        (λ [ρ₁] ⊢Δ₁ → emb emb< (Lwk.wk [ρ₁] ⊢Δ₁ ([F₁] [ρ] ⊢Δ))) ([Id] [ρ] ⊢Δ [e]) ([Idext] [ρ] ⊢Δ [e] [e])

    abstract
      [IdGG₁-ext] : ∀ {ρ Δ e e′} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ)
        → ([e] : Δ ⊩⟨ ι ¹ ⟩ e ∷ wk ρ (Id (Univ rF ⁰) F F₁) ^ [ % , ι ¹ ] / [IdFF₁] [ρ] ⊢Δ)
        → ([e′] : Δ ⊩⟨ ι ¹ ⟩ e′ ∷ wk ρ (Id (Univ rF ⁰) F F₁) ^ [ % , ι ¹ ] / [IdFF₁] [ρ] ⊢Δ)
        → ([e≡e′] : Δ ⊩⟨ ι ¹ ⟩ e ≡ e′ ∷ wk ρ (Id (Univ rF ⁰) F F₁) ^ [ % , ι ¹ ] / [IdFF₁] [ρ] ⊢Δ)
        → Δ ⊩⟨ ι ¹ ⟩ IdGG₁ ρ e ≡ IdGG₁ ρ e′ ^ [ % , ι ¹ ] / [IdGG₁] [ρ] ⊢Δ [e]
      [IdGG₁-ext] {ρ} {Δ} {e} {e′} [ρ] ⊢Δ [e] [e′] _ =
        let
          ⊢wkF₁ = escape ([F₁] [ρ] ⊢Δ)
          [0] = let ⊢0 = (var (⊢Δ ∙ ⊢wkF₁) here) in
            neuTerm (Lwk.wk (Twk.step Twk.id) (⊢Δ ∙ escape ([F₁] [ρ] ⊢Δ)) ([F₁] [ρ] ⊢Δ)) (var 0) ⊢0 (~-var ⊢0)
          x = [Id] [ρ] ⊢Δ [e′] (Twk.step Twk.id) (⊢Δ ∙ ⊢wkF₁) [0]
          ⊢x = PE.subst (λ X → Δ ∙ wk ρ F₁ ^ [ rF , ι ⁰ ] ⊢ X ^ [ % , ι ¹ ]) (wkSingleSubstId _) (escape x)
          x₁ = [Idext] [ρ] ⊢Δ [e′] [e] (Twk.step Twk.id) (⊢Δ ∙ ⊢wkF₁) [0] [0] (reflEqTerm (Lwk.wk (Twk.step Twk.id) (⊢Δ ∙ escape ([F₁] [ρ] ⊢Δ)) ([F₁] [ρ] ⊢Δ)) [0])
          ⊢x₁ = PE.subst₂ (λ X Y → Δ ∙ wk ρ F₁ ^ [ rF , ι ⁰ ] ⊢ X ≅ Y ^ [ % , ι ¹ ]) (wkSingleSubstId _) (wkSingleSubstId _) (escapeEq x x₁)
        in
        Π₌ (wk ρ F₁) (Id (U ⁰) (wk (lift (step ρ)) G [ b (step ρ) (wk1 e′) (var 0) ]) (wk (lift ρ) G₁))
           (id (univ (Πⱼ <is≤ 0<1 ▹ ≡is≤ PE.refl ▹ un-univ ⊢wkF₁ ▹ un-univ ⊢x)))
           (≅-univ (≅ₜ-Π-cong (<is≤ 0<1) (≡is≤ PE.refl) ⊢wkF₁ (≅-un-univ (escapeEqRefl ([F₁] [ρ] ⊢Δ))) (≅-un-univ (≅-sym ⊢x₁))))
           (λ [ρ]₁ ⊢Δ₁ → reflEq (Lwk.wk [ρ]₁ ⊢Δ₁ ([F₁] [ρ] ⊢Δ)))
           (λ [ρ₁] ⊢Δ₁ [a] → [Idext] [ρ] ⊢Δ [e] [e′] [ρ₁] ⊢Δ₁ [a] [a] (reflEqTerm (Lwk.wk [ρ₁] ⊢Δ₁ ([F₁] [ρ] ⊢Δ)) [a]))

    abstract
      IdTel≡IdUΠΠ : ∃ Id (Univ rF ⁰) F F₁ ▹ (IdGG₁ (step id) (var 0)) PE.≡
        ∃ (Id (Univ rF ⁰) F F₁) ▹ (Π (wk1 F₁) ^ rF ° ⁰ ▹
          Id (U ⁰) ((wk1d G) [ cast ⁰ (wk1 (wk1 F₁)) (wk1 (wk1 F)) (Idsym (Univ rF ⁰) (wk1 (wk1 F)) (wk1 (wk1 F₁)) (var 1)) (var 0) ]↑) (wk1d G₁) ° ¹ ° ¹)
      IdTel≡IdUΠΠ = PE.cong (λ X → ∃ Id (Univ rF ⁰) F F₁ ▹ Π (wk1 F₁) ^ rF ° ⁰ ▹ Id (U ⁰) X (wk1d G₁) ° ¹ ° ¹)
        (PE.trans
          (PE.cong₃ (λ X Y Z → X [ cast ⁰ Z Y (Idsym (Univ rF ⁰) Y Z (var 1)) (var 0) ])
            (PE.sym (wk-comp (lift (step id)) (lift (step id)) G))
            (PE.sym (wk-comp (step id) (step id) F))
            (PE.sym (wk-comp (step id) (step id) F₁)))
          (PE.sym (wk1d[]-[]↑ (wk1d G) _)))

    abstract
      wksubst-IdTel : ∀ ρ e → wk (lift ρ) (IdGG₁ (step id) (var 0)) [ e ] PE.≡ IdGG₁ ρ e
      wksubst-IdTel ρ e =
        let
          x₃ = PE.trans (PE.cong (subst (liftSubst (sgSubst e))) (wk-Idsym (lift (lift ρ)) (Univ rF ⁰) (wk (step (step id)) F) (wk (step (step id)) F₁) (var 1)))
            (PE.trans (subst-Idsym (liftSubst (sgSubst e)) (Univ rF ⁰) (wk _ (wk (step (step id)) F)) (wk _ (wk (step (step id)) F₁)) (var 1))
              (PE.cong₂ (λ X Y → Idsym (Univ rF ⁰) X Y (wk1 e)) (Id-subst-lemma1 ρ F e) (Id-subst-lemma1 ρ F₁ e)))
          x₂ = PE.cong₃ (λ X Y Z → cast ⁰ X Y Z (var 0)) (Id-subst-lemma1 ρ F₁ e) (Id-subst-lemma1 ρ F e) x₃
          x₁ = PE.cong₂ (λ X Y → X [ Y ]) (Id-subst-lemma2 ρ G e) x₂
          x₀ = (PE.trans (PE.cong (subst (liftSubst (sgSubst e))) (wk-β (wk (lift (step (step id))) G)))
            (PE.trans (singleSubstLift (wk (lift (lift (lift ρ))) (wk (lift (step (step id))) G)) (wk (lift (lift ρ)) (b (step (step id)) (var 1) (var 0)))) x₁))
        in PE.cong₃ (λ X Y Z → Π X ^ rF ° ⁰ ▹ Id (U ⁰) Y Z ° ¹ ° ¹) (irrelevant-subst′ ρ F₁ e) x₀ (cast-subst-lemma4 ρ e G₁)

    [IdGG₁0] : Γ ∙ Id (Univ rF ⁰) F F₁ ^ [ % , ι ¹ ] ⊩⟨ ι ¹ ⟩ IdGG₁ (step id) (var 0) ^ [ % , ι ¹ ]
    [IdGG₁0] = let
        ⊢0 = var (⊢Γ ∙ ⊢IdFF₁) here
        [0] = neuTerm ([IdFF₁] (Twk.step Twk.id) (⊢Γ ∙ ⊢IdFF₁)) (var 0) ⊢0 (~-var ⊢0)
      in [IdGG₁] (Twk.step Twk.id) (⊢Γ ∙ ⊢IdFF₁) [0]

    ⊢IdGG₁ : Γ ∙ Id (Univ rF ⁰) F F₁ ^ [ % , ι ¹ ] ⊢ IdGG₁ (step id) (var 0) ^ [ % , ι ¹ ]
    ⊢IdGG₁ = escape [IdGG₁0]

    ⊢∃ : Γ ⊢ ∃ Id (Univ rF ⁰) F F₁ ▹ IdGG₁ (step id) (var 0) ^ [ % , ι ¹ ]
    ⊢∃ = univ (∃ⱼ un-univ ⊢IdFF₁ ▹ un-univ ⊢IdGG₁)

    ∃≡∃ : Γ ⊢ ∃ Id (Univ rF ⁰) F F₁ ▹ IdGG₁ (step id) (var 0) ≅ ∃ Id (Univ rF ⁰) F F₁ ▹ IdGG₁ (step id) (var 0) ^ [ % , ι ¹ ]
    ∃≡∃ = (≅-univ (≅ₜ-∃-cong
      ⊢IdFF₁
      (≅-un-univ (escapeEqRefl (PE.subst (λ X → Γ ⊩⟨ ι ¹ ⟩ X ^ [ % , ι ¹ ]) (wk-id (Id (Univ rF ⁰) F F₁)) ([IdFF₁] Twk.id ⊢Γ))))
      (≅-un-univ (escapeEqRefl [IdGG₁0]))))

    D∃ : Γ ⊢ Id (U ⁰) A B ⇒* ∃ Id (Univ rF ⁰) F F₁ ▹ IdGG₁ (step id) (var 0) ^ [ % , ι ¹ ]
    D∃ = univ⇒* (IdURed*Term′ (un-univ ⊢A) (un-univ ⊢ΠFG) (un-univ⇒* D) (un-univ ⊢B)
      ⇨∷* IdUΠRed*Term′ (un-univ ⊢F) (un-univ ⊢G) (un-univ ⊢B) (un-univ ⊢ΠF₁G₁) (un-univ⇒* D₁))
      ⇨* PE.subst (λ X → Γ ⊢ Id (U ⁰) (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) (Π F₁ ^ rF ° ⁰ ▹ G₁ ° ⁰ ° ⁰) ⇒* X ^ [ % , ι ¹ ]) (PE.sym IdTel≡IdUΠΠ)
        (univ (Id-U-ΠΠ (un-univ ⊢F) (un-univ ⊢G) (un-univ ⊢F₁) (un-univ ⊢G₁))
      ⇨ id (PE.subst (λ X → Γ ⊢ X ^ [ % , ι ¹ ]) IdTel≡IdUΠΠ ⊢∃))

module IdTypeU-lemmas-2
       {Γ rF A₁ A₂ A₃ A₄ F₁ F₂ F₃ F₄ G₁ G₂ G₃ G₄}
       (⊢Γ : ⊢ Γ)

       (⊢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])

       (recursor₁ : ∀ {ρ Δ}
          ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          → Δ ⊩⟨ ι ¹ ⟩ Id (Univ rF ⁰) (wk ρ F₁) (wk ρ F₃) ^ [ % , ι ¹ ])
       (recursor₂ : ∀ {ρ Δ x y}
          ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₁ ^ [ rF , ι ⁰ ] / [F₁] [ρ] ⊢Δ)
          ([y] : Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ] ⊢Δ)
          → Δ ⊩⟨ ι ¹ ⟩ Id (U ⁰) (wk (lift ρ) G₁ [ x ]) (wk (lift ρ) G₃ [ y ]) ^ [ % , ι ¹ ])
       (recursor₃ : ∀ {ρ Δ}
          ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          → Δ ⊩⟨ ι ¹ ⟩ Id (Univ rF ⁰) (wk ρ F₂) (wk ρ F₄) ^ [ % , ι ¹ ])
       (recursor₄ : ∀ {ρ Δ x y}
          ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          ([x] : Δ ⊩⟨ ι ⁰ ⟩ x ∷ wk ρ F₂ ^ [ rF , ι ⁰ ] / [F₂] [ρ] ⊢Δ)
          ([y] : Δ ⊩⟨ ι ⁰ ⟩ y ∷ wk ρ F₄ ^ [ rF , ι ⁰ ] / [F₄] [ρ] ⊢Δ)
          → Δ ⊩⟨ ι ¹ ⟩ Id (U ⁰) (wk (lift ρ) G₂ [ x ]) (wk (lift ρ) G₄ [ y ]) ^ [ % , ι ¹ ])
       (extrecursor₁ : ∀ {ρ Δ x y x′ y′}
          ([ρ] : ρ 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₃] [ρ] ⊢Δ)
          → Δ ⊩⟨ ι ¹ ⟩ Id (U ⁰) (wk (lift ρ) G₁ [ x ]) (wk (lift ρ) G₃ [ y ]) ≡ Id (U ⁰) (wk (lift ρ) G₁ [ x′ ]) (wk (lift ρ) G₃ [ y′ ]) ^ [ % , ι ¹ ] / recursor₂ [ρ] ⊢Δ [x] [y])
       (extrecursor₂ : ∀ {ρ Δ x y x′ y′}
          ([ρ] : ρ 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₄] [ρ] ⊢Δ)
          → Δ ⊩⟨ ι ¹ ⟩ Id (U ⁰) (wk (lift ρ) G₂ [ x ]) (wk (lift ρ) G₄ [ y ]) ≡ Id (U ⁰) (wk (lift ρ) G₂ [ x′ ]) (wk (lift ρ) G₄ [ y′ ]) ^ [ % , ι ¹ ] / recursor₄ [ρ] ⊢Δ [x] [y])
       (eqrecursor₁ : ∀ {ρ Δ}
          ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
          → Δ ⊩⟨ ι ¹ ⟩ Id (Univ rF ⁰) (wk ρ F₁) (wk ρ F₃) ≡ Id (Univ rF ⁰) (wk ρ F₂) (wk ρ F₄) ^ [ % , ι ¹ ] / recursor₁ [ρ] ⊢Δ)
       (eqrecursor₂ : ∀ {ρ Δ x₁ x₂ x₃ x₄}
          → ([ρ] : ρ 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₃])
          → Δ ⊩⟨ ι ¹ ⟩ Id (U ⁰) (wk (lift ρ) G₁ [ x₁ ]) (wk (lift ρ) G₃ [ x₃ ]) ≡ Id (U ⁰) (wk (lift ρ) G₂ [ x₂ ]) (wk (lift ρ) G₄ [ x₄ ]) ^ [ % , ι ¹ ] / recursor₂ [ρ] ⊢Δ [x₁] [x₃])
  where
    module E₁ = IdTypeU-lemmas ⊢Γ ⊢A₁ ⊢ΠF₁G₁ D₁ ⊢F₁ ⊢G₁ A₁≡A₁ [F₁] [G₁] G₁-ext ⊢A₃ ⊢ΠF₃G₃ D₃ ⊢F₃ ⊢G₃ A₃≡A₃ [F₃] [G₃] G₃-ext
      recursor₁ recursor₂ extrecursor₁
    module E₂ = IdTypeU-lemmas ⊢Γ ⊢A₂ ⊢ΠF₂G₂ D₂ ⊢F₂ ⊢G₂ A₂≡A₂ [F₂] [G₂] G₂-ext ⊢A₄ ⊢ΠF₄G₄ D₄ ⊢F₄ ⊢G₄ A₄≡A₄ [F₄] [G₄] G₄-ext
      recursor₃ recursor₄ extrecursor₂

    [IdFF₁≡IdFF₂] : ∀ {ρ Δ} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ)
      → Δ ⊩⟨ ι ¹ ⟩ wk ρ (Id (Univ rF ⁰) F₁ F₃) ≡ wk ρ (Id (Univ rF ⁰) F₂ F₄) ^ [ % , ι ¹ ] / E₁.[IdFF₁] [ρ] ⊢Δ
    [IdFF₁≡IdFF₂] = (λ [ρ] ⊢Δ → irrelevanceEq (recursor₁ [ρ] ⊢Δ) (E₁.[IdFF₁] [ρ] ⊢Δ) (eqrecursor₁ [ρ] ⊢Δ))

    abstract
      [Ideq] : ∀ {ρ Δ e} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ)
        → ([e] : Δ ⊩⟨ ι ¹ ⟩ e ∷ wk ρ (Id (Univ rF ⁰) F₁ F₃) ^ [ % , ι ¹ ] / E₁.[IdFF₁] [ρ] ⊢Δ)
        → ∀ {ρ₁ Δ₁ a} → ([ρ₁] : ρ₁ Twk.∷ Δ₁ ⊆ Δ) → (⊢Δ₁ : ⊢ Δ₁)
        → ([a] : Δ₁ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ₁ (wk ρ F₃) ^ [ rF , ι ⁰ ] / (Lwk.wk [ρ₁] ⊢Δ₁ ([F₃] [ρ] ⊢Δ)))
        → Δ₁ ⊩⟨ ι ¹ ⟩ wk (lift ρ₁) (Id (U ⁰) (wk (lift (step ρ)) G₁ [ E₁.b (step ρ) (wk1 e) (var 0) ]) (wk (lift ρ) G₃)) [ a ]
             ≡ wk (lift ρ₁) (Id (U ⁰) (wk (lift (step ρ)) G₂ [ E₂.b (step ρ) (wk1 e) (var 0) ]) (wk (lift ρ) G₄)) [ a ] ^ [ % , ι ¹ ]
             / E₁.[Id] [ρ] ⊢Δ [e] [ρ₁] ⊢Δ₁ [a]
      [Ideq] {ρ} {Δ} {e} [ρ] ⊢Δ [e] {ρ₁} {Δ₁} {a} [ρ₁] ⊢Δ₁ [a] =
        let
          ρ′ = ρ₁ • ρ
          [ρ′] : ρ′ Twk.∷ Δ₁ ⊆ Γ
          [ρ′] = [ρ₁] Twk.•ₜ [ρ]
          [a₃] : Δ₁ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ′ F₃ ^ [ rF , ι ⁰ ] / [F₃] [ρ′] ⊢Δ₁
          [a₃] = irrelevanceTerm′ (wk-comp ρ₁ ρ F₃) PE.refl PE.refl (Lwk.wk [ρ₁] ⊢Δ₁ ([F₃] [ρ] ⊢Δ)) ([F₃] [ρ′] ⊢Δ₁) [a]
          [a₄] = convTerm₁ ([F₃] [ρ′] ⊢Δ₁) ([F₄] [ρ′] ⊢Δ₁) ([F₃≡F₄] [ρ′] ⊢Δ₁) [a₃]
          [a₃≡a₄] = reflEqTerm ([F₃] [ρ′] ⊢Δ₁) [a₃]
          ⊢e′ = PE.subst (λ X → Δ₁ ⊢ wk ρ₁ e ∷ X ^ [ % , ι ¹ ]) (wk-comp ρ₁ ρ _) (Twk.wkTerm [ρ₁] ⊢Δ₁ (escapeTerm (E₁.[IdFF₁] [ρ] ⊢Δ) [e]))
          ⊢e₁ = Idsymⱼ (univ 0<1 ⊢Δ₁) (un-univ (escape ([F₁] [ρ′] ⊢Δ₁))) (un-univ (escape ([F₃] [ρ′] ⊢Δ₁))) ⊢e′
          ⊢e″ = conv ⊢e′ (≅-eq (escapeEq (E₁.[IdFF₁] [ρ′] ⊢Δ₁) ([IdFF₁≡IdFF₂] [ρ′] ⊢Δ₁)))
          ⊢e₂ = Idsymⱼ (univ 0<1 ⊢Δ₁) (un-univ (escape ([F₂] [ρ′] ⊢Δ₁))) (un-univ (escape ([F₄] [ρ′] ⊢Δ₁))) ⊢e″
          [b₁] = [proj₁cast] ⊢Δ₁ ([F₃] [ρ′] ⊢Δ₁) ([F₁] [ρ′] ⊢Δ₁) [a₃] ⊢e₁
          [b₂] = [proj₁cast] ⊢Δ₁ ([F₄] [ρ′] ⊢Δ₁) ([F₂] [ρ′] ⊢Δ₁) [a₄] ⊢e₂
          [b₁≡b₂] = [proj₁castext] ⊢Δ₁ ([F₃] [ρ′] ⊢Δ₁) ([F₄] [ρ′] ⊢Δ₁) ([F₃≡F₄] [ρ′] ⊢Δ₁)
            ([F₁] [ρ′] ⊢Δ₁) ([F₂] [ρ′] ⊢Δ₁) ([F₁≡F₂] [ρ′] ⊢Δ₁)
            [a₃] [a₄] [a₃≡a₄] ⊢e₁ ⊢e₂
          [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₂])
          [a₃≡a₄:F₄] = convEqTerm₁ ([F₃] [ρ′] ⊢Δ₁) ([F₄] [ρ′] ⊢Δ₁) ([F₃≡F₄] [ρ′] ⊢Δ₁) [a₃≡a₄]
          [G₃a₃≡G₄a₄] = transEq ([G₃] [ρ′] ⊢Δ₁ [a₃]) ([G₄] [ρ′] ⊢Δ₁ [a₄]) ([G₄] [ρ′] ⊢Δ₁ [a₄])
            ([G₃≡G₄] [ρ′] ⊢Δ₁ [a₃]) (G₄-ext [ρ′] ⊢Δ₁ [a₄] [a₄] [a₃≡a₄:F₄])
          x₁ = recursor₂ [ρ′] ⊢Δ₁ [b₁] [a₃]
          x = eqrecursor₂ [ρ′] ⊢Δ₁ [b₁] [b₂] [G₁b₁≡G₂b₂] [a₃] [a₄] [G₃a₃≡G₄a₄]
        in irrelevanceEq″ (PE.sym (E₁.IdTel₂-prettify ρ₁ ρ e a)) (PE.sym (E₂.IdTel₂-prettify ρ₁ ρ e a)) PE.refl PE.refl x₁ (E₁.[Id] [ρ] ⊢Δ [e] [ρ₁] ⊢Δ₁ [a]) x

    abstract
      [IdGG₁≡IdGG₂] : ∀ {ρ Δ e} → ([ρ] : ρ Twk.∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ)
          → ([e] : Δ ⊩⟨ ι ¹ ⟩ e ∷ wk ρ (Id (Univ rF ⁰) F₁ F₃) ^ [ % , ι ¹ ] / E₁.[IdFF₁] [ρ] ⊢Δ)
          → Δ ⊩⟨ ι ¹ ⟩ E₁.IdGG₁ ρ e ≡ E₂.IdGG₁ ρ e ^ [ % , ι ¹ ] / E₁.[IdGG₁] [ρ] ⊢Δ [e]
      [IdGG₁≡IdGG₂] {ρ} {Δ} {e} [ρ] ⊢Δ [e] = let
          [e]′ = convTerm₁ (E₁.[IdFF₁] [ρ] ⊢Δ) (E₂.[IdFF₁] [ρ] ⊢Δ) ([IdFF₁≡IdFF₂] [ρ] ⊢Δ) [e]
          ⊢wkF₃ = escape ([F₃] [ρ] ⊢Δ)
          ⊢wkF₄ = escape ([F₄] [ρ] ⊢Δ)
          [0:F₃] : Δ ∙ wk ρ F₃ ^ [ rF , ι ⁰ ] ⊩⟨ ι ⁰ ⟩ var 0 ∷ wk1 (wk ρ F₃) ^ [ rF , ι ⁰ ] / (Lwk.wk (Twk.step Twk.id) (⊢Δ ∙ ⊢wkF₃) ([F₃] [ρ] ⊢Δ))
          [0:F₃] = let ⊢0 = (var (⊢Δ ∙ ⊢wkF₃) here) in
            neuTerm (Lwk.wk (Twk.step Twk.id) (⊢Δ ∙ ⊢wkF₃) ([F₃] [ρ] ⊢Δ)) (var 0) ⊢0 (~-var ⊢0)
          [0:F₄] = let ⊢0 = (var (⊢Δ ∙ ⊢wkF₄) here) in
            neuTerm (Lwk.wk (Twk.step Twk.id) (⊢Δ ∙ ⊢wkF₄) ([F₄] [ρ] ⊢Δ)) (var 0) ⊢0 (~-var ⊢0)
          x = E₁.[Id] [ρ] ⊢Δ [e] (Twk.step Twk.id) (⊢Δ ∙ ⊢wkF₃) [0:F₃]
          x₁ = [Ideq] [ρ] ⊢Δ [e] (Twk.step Twk.id) (⊢Δ ∙ ⊢wkF₃) [0:F₃]
          ⊢x₁ = PE.subst₂ (λ X Y → Δ ∙ wk ρ F₃ ^ [ rF , ι ⁰ ] ⊢ X ≅ Y ^ [ % , ι ¹ ]) (wkSingleSubstId _) (wkSingleSubstId _) (escapeEq x x₁)
          x₂ = E₂.[Id] [ρ] ⊢Δ [e]′ (Twk.step Twk.id) (⊢Δ ∙ ⊢wkF₄) [0:F₄]
          ⊢x₂ = PE.subst (λ X → Δ ∙ wk ρ F₄ ^ [ rF , ι ⁰ ] ⊢ X ^ [ % , ι ¹ ]) (wkSingleSubstId _) (escape x₂)
        in Π₌ (wk ρ F₄) (Id (U ⁰) (wk (lift (step ρ)) G₂ [ E₂.b (step ρ) (wk1 e) (var 0) ]) (wk (lift ρ) G₄))
          (id (univ (Πⱼ <is≤ 0<1 ▹ ≡is≤ PE.refl ▹ un-univ ⊢wkF₄ ▹ un-univ ⊢x₂)))
          (≅-univ (≅ₜ-Π-cong (<is≤ 0<1) (≡is≤ PE.refl) ⊢wkF₃ (≅-un-univ (escapeEq ([F₃] [ρ] ⊢Δ) ([F₃≡F₄] [ρ] ⊢Δ))) (≅-un-univ ⊢x₁)))
          (λ [ρ₁] ⊢Δ₁ → Lwk.wkEq [ρ₁] ⊢Δ₁ ([F₃] [ρ] ⊢Δ) ([F₃≡F₄] [ρ] ⊢Δ))
          (λ [ρ₁] ⊢Δ₁ [a] → [Ideq] [ρ] ⊢Δ [e] [ρ₁] ⊢Δ₁ [a])

    [IdGG₁≡IdGG₂0] : Γ ∙ Id (Univ rF ⁰) F₁ F₃ ^ [ % , ι ¹ ] ⊩⟨ ι ¹ ⟩ E₁.IdGG₁ (step id) (var 0) ≡ E₂.IdGG₁ (step id) (var 0) ^ [ % , ι ¹ ] / E₁.[IdGG₁0]
    [IdGG₁≡IdGG₂0] = let
        ⊢0 = var (⊢Γ ∙ E₁.⊢IdFF₁) here
        [0] = neuTerm (E₁.[IdFF₁] (Twk.step Twk.id) (⊢Γ ∙ E₁.⊢IdFF₁)) (var 0) ⊢0 (~-var ⊢0)
      in [IdGG₁≡IdGG₂] (Twk.step Twk.id) (⊢Γ ∙ E₁.⊢IdFF₁) [0]

    ∃₁≡∃₂ : Γ ⊢ ∃ Id (Univ rF ⁰) F₁ F₃ ▹ E₁.IdGG₁ (step id) (var 0) ≅ ∃ Id (Univ rF ⁰) F₂ F₄ ▹ E₂.IdGG₁ (step id) (var 0) ^ [ % , ι ¹ ]
    ∃₁≡∃₂ = (≅-univ (≅ₜ-∃-cong
      E₁.⊢IdFF₁
      (≅-un-univ (PE.subst₂ (λ X Y → Γ ⊢ X ≅ Y ^ [ % , ι ¹ ]) (wk-id (Id (Univ rF ⁰) F₁ F₃)) (wk-id (Id (Univ rF ⁰) F₂ F₄)) (escapeEq (E₁.[IdFF₁] Twk.id ⊢Γ) ([IdFF₁≡IdFF₂] Twk.id ⊢Γ))))
      (≅-un-univ (escapeEq E₁.[IdGG₁0] [IdGG₁≡IdGG₂0]))))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
module Numeral.Natural where

import      Lvl
open import Type

-- The set of natural numbers (0,..).
-- Positive integers including zero.
data ℕ : Type{Lvl.𝟎} where
  𝟎 : ℕ      -- Zero
  𝐒 : ℕ → ℕ -- Successor function (Intuitively: 𝐒(n) = n+1)
{-# BUILTIN NATURAL ℕ #-}

pattern 𝟏 = ℕ.𝐒(𝟎)
{-# DISPLAY ℕ.𝐒(𝟎) = 𝟏 #-}

-- Limited predecessor function
-- Intuitively: 𝐏(n) = max(0,n-1)
𝐏 : ℕ → ℕ
𝐏(𝟎)    = 𝟎
𝐏(𝐒(n)) = n

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- Abstract typing contexts
------------------------------------------------------------------------

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

module Data.Context where

open import Data.Fin using (Fin)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Relation.Unary using (Pred)

------------------------------------------------------------------------
-- Abstract typing contexts and context extensions.

infixr 5 _∷_

-- Typing contexts.
--
-- A |Ctx T n| is an indexed sequences of T-typed bindings mapping n
-- variables to T-types with 0 to (n - 1) free variables each.  Like
-- lists (Data.List) and vectors (Data.Vec), contexts are cons
-- sequences, i.e. new bindings are added to the front (rather than
-- the back, as is more common in the literature).  For example, a
-- typing context Γ represented in the usual notation as
--
--   Γ  =  xᵢ: Aᵢ, ..., x₁: A₁, x₀: A₀
--
-- is represented here by a term |Γ : Ctx Type i| of the form
--
--   Γ  =  A₀ ∷ A₁ ∷ ... ∷ Aᵢ
--
-- which is consistent with A₀ being the 0-th element of Γ, and with
-- the de Bruijn convention that the 0-th variable corresponds to the
-- closest binding.

data Ctx {ℓ} (T : Pred ℕ ℓ) : ℕ → Set ℓ where
  []  :                         Ctx T zero
  _∷_ : ∀ {n} → T n → Ctx T n → Ctx T (suc n)

module _ {ℓ} {T : Pred ℕ ℓ} where

  head : ∀ {n} → Ctx T (suc n) → T n
  head (t ∷ ts) = t

  tail : ∀ {n} → Ctx T (suc n) → Ctx T n
  tail (t ∷ ts) = ts

  -- Drop the m innermost elements of a context Γ.

  drop : ∀ {n} m → Ctx T (m + n) → Ctx T n
  drop zero         Γ  = Γ
  drop (suc m) (_ ∷ Γ) = drop m Γ

-- A map function that changes the entries in a context pointwise.

map : ∀ {ℓ₁ ℓ₂} {T₁ : Pred ℕ ℓ₁} {T₂ : Pred ℕ ℓ₂} {n} →
      (∀ {k} → T₁ k → T₂ k) → Ctx T₁ n → Ctx T₂ n
map f []      = []
map f (t ∷ Γ) = f t ∷ map f Γ

-- Extensions of typing contexts.
--
-- Context extensions are indexed sequences of bindings that can be
-- concatenated to the front of a typing context.  A |CtxExt T m n| is
-- an extension mapping n variables to T-types with m to (n + m - 1)
-- free variables each.
--
-- NOTE. It is tempting to define contexts as just a special case of
-- context extensions, i.e. as
--
--   Ctx T n  =  CtxExt T zero n
--
-- But this leads to problems when defining e.g. concatenation because
-- of the way context extensions are indexed.  This could be remedied
-- by indexing context extensions differently, but then the definition
-- of |mapExt| below becomes difficult.  An earlier version of this
-- module contained two different (but equivalent) representations for
-- context extensions, but this complicated (rather than simplified)
-- the development overall.

data CtxExt {ℓ} (T : Pred ℕ ℓ) (m : ℕ) : ℕ → Set ℓ where
  []  :                                    CtxExt T m zero
  _∷_ : ∀ {l} → T (l + m) → CtxExt T m l → CtxExt T m (suc l)

infixr 5 _++_

-- Concatenation of context extensions with contexts.

_++_ : ∀ {ℓ} {T : Pred ℕ ℓ} {m n} → CtxExt T m n → Ctx T m → Ctx T (n + m)
[]      ++ Γ = Γ
(t ∷ Δ) ++ Γ = t ∷ (Δ ++ Γ)

-- A map function that point-wise re-indexes and changes the entries
-- in a context extension.

mapExt : ∀ {ℓ₁ ℓ₂} {T₁ : Pred ℕ ℓ₁} {T₂ : Pred ℕ ℓ₂} {m n k} →
         (∀ l → T₁ (l + m) → T₂ (l + n)) → CtxExt T₁ m k → CtxExt T₂ n k
mapExt f []            = []
mapExt f (_∷_ {l} t Γ) = f l t ∷ mapExt (λ l → f l) Γ

-- Operations on contexts that require weakening of types.

module WeakenOps {ℓ} {T : Pred ℕ ℓ} (extension : Extension T) where

  -- Weakening of types.

  open Extension extension public

  -- Convert a context or context extension to its vector representation.

  toVec : ∀ {n} → Ctx T n → Vec (T n) n
  toVec []      = []
  toVec (t ∷ Γ) = weaken t /∷ toVec Γ

  extToVec : ∀ {k m n} → CtxExt T m n → Vec (T m) k → Vec (T (n + m)) (n + k)
  extToVec []      ts = ts
  extToVec (t ∷ Γ) ts = weaken t /∷ extToVec Γ ts

  -- Lookup the type of a variable in a context or context extension.

  lookup : ∀ {n} → Ctx T n → Fin n → T n
  lookup Γ x = Vec.lookup (toVec Γ) x

  extLookup : ∀ {k m n} → CtxExt T m n → Vec (T m) k → Fin (n + k) → T (n + m)
  extLookup Δ ts x = Vec.lookup (extToVec Δ ts) x

-- Operations on contexts that require substitutions in types.

module SubstOps {ℓ₁ ℓ₂} {T₁ : Pred ℕ ℓ₁} {T₂ : Pred ℕ ℓ₂}
                (application : Application T₁ T₂)
                (simple      : Simple T₂)
                where

  open Application application public -- Application of T′ substitutions to Ts.
  open Simple      simple      public -- Simple T′ substitutions.

  -- Application of substitutions to context extensions.

  _E/_ : ∀ {k m n} → CtxExt T₁ m k → Sub T₂ m n → CtxExt T₁ n k
  Γ E/ σ = mapExt (λ l t → t / σ ↑⋆ l) Γ

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


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

module Data.Nat.PredExp2 where

open import Data.Nat
open import Data.Nat.Properties

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; module ≡-Reasoning)

open import Data.Nat.Log2 using (⌈log₂_⌉)

pred[2^_] : ℕ → ℕ
pred[2^ n ] = pred (2 ^ n)

lemma/2^suc : ∀ n → 2 ^ n + 2 ^ n ≡ 2 ^ suc n
lemma/2^suc n =
  begin
    2 ^ n + 2 ^ n
  ≡˘⟨ Eq.cong ((2 ^ n) +_) (*-identityˡ (2 ^ n)) ⟩
    2 ^ n + (2 ^ n + 0)
  ≡⟨⟩
    2 ^ n + (2 ^ n + 0 * (2 ^ n))
  ≡⟨⟩
    2 * (2 ^ n)
  ≡⟨⟩
    2 ^ suc n
  ∎
    where open ≡-Reasoning

private
  lemma/1≤2^n : ∀ n → 1 ≤ 2 ^ n
  lemma/1≤2^n zero    = ≤-refl {1}
  lemma/1≤2^n (suc n) =
    begin
      1
    ≤⟨ s≤s z≤n ⟩
      1 + 1
    ≤⟨ +-mono-≤ (lemma/1≤2^n n) (lemma/1≤2^n n) ⟩
      2 ^ n + 2 ^ n
    ≡⟨ lemma/2^suc n ⟩
      2 ^ suc n
    ∎
      where open ≤-Reasoning

  lemma/2^n≢0 : ∀ n → 2 ^ n ≢ zero
  lemma/2^n≢0 n 2^n≡0 with 2 ^ n | lemma/1≤2^n n
  ... | zero | ()

pred[2^]-mono : pred[2^_] Preserves _≤_ ⟶ _≤_
pred[2^]-mono m≤n = pred-mono (2^-mono m≤n)
  where
    2^-mono : (2 ^_) Preserves _≤_ ⟶ _≤_
    2^-mono {y = y} z≤n = lemma/1≤2^n y
    2^-mono (s≤s m≤n) = *-monoʳ-≤ 2 (2^-mono m≤n)

pred[2^suc[n]] : (n : ℕ) → suc (pred[2^ n ] + pred[2^ n ]) ≡ pred[2^ suc n ]
pred[2^suc[n]] n =
  begin
    suc (pred[2^ n ] + pred[2^ n ])
  ≡⟨⟩
    suc (pred (2 ^ n) + pred (2 ^ n))
  ≡˘⟨ +-suc (pred (2 ^ n)) (pred (2 ^ n)) ⟩
    pred (2 ^ n) + suc (pred (2 ^ n))
  ≡⟨ Eq.cong (pred (2 ^ n) +_) (suc[pred[n]]≡n (lemma/2^n≢0 n)) ⟩
    pred (2 ^ n) + 2 ^ n
  ≡⟨ lemma/pred-+ (2 ^ n) (2 ^ n) (lemma/2^n≢0 n) ⟩
    pred (2 ^ n + 2 ^ n)
  ≡⟨ Eq.cong pred (lemma/2^suc n) ⟩
    pred (2 ^ suc n)
  ≡⟨⟩
    pred[2^ suc n ]
  ∎
    where
      open ≡-Reasoning

      lemma/pred-+ : ∀ m n → m ≢ zero → pred m + n ≡ pred (m + n)
      lemma/pred-+ zero    n m≢zero = contradiction refl m≢zero
      lemma/pred-+ (suc m) n m≢zero = refl

pred[2^log₂] : (n : ℕ) → pred[2^ ⌈log₂ suc ⌈ n /2⌉ ⌉ ] ≤ n
pred[2^log₂] n = strong-induction n n ≤-refl
  where
    strong-induction : (n m : ℕ) → m ≤ n → pred[2^ ⌈log₂ suc ⌈ m /2⌉ ⌉ ] ≤ m
    strong-induction n zero    h = z≤n
    strong-induction n (suc zero) h = s≤s z≤n
    strong-induction (suc (suc n)) (suc (suc m)) (s≤s (s≤s h)) =
      begin
        pred[2^ ⌈log₂ suc ⌈ suc (suc m) /2⌉ ⌉ ]
      ≡⟨⟩
        pred[2^ suc ⌈log₂ ⌈ suc ⌈ suc (suc m) /2⌉ /2⌉ ⌉ ]
      ≡˘⟨ pred[2^suc[n]] ⌈log₂ ⌈ suc ⌈ suc (suc m) /2⌉ /2⌉ ⌉ ⟩
        suc (pred[2^ ⌈log₂ ⌈ suc ⌈ suc (suc m) /2⌉ /2⌉ ⌉ ] + pred[2^ ⌈log₂ ⌈ suc ⌈ suc (suc m) /2⌉ /2⌉ ⌉ ])
      ≡⟨⟩
        suc (pred[2^ ⌈log₂ ⌈ suc (suc ⌈ m /2⌉) /2⌉ ⌉ ] + pred[2^ ⌈log₂ ⌈ suc (suc ⌈ m /2⌉) /2⌉ ⌉ ])
      ≡⟨⟩
        suc (pred[2^ ⌈log₂ suc ⌈ ⌈ m /2⌉ /2⌉ ⌉ ] + pred[2^ ⌈log₂ suc ⌈ ⌈ m /2⌉ /2⌉ ⌉ ])
      ≤⟨
        s≤s (
          +-mono-≤
            (strong-induction (suc n) ⌈ m /2⌉ (≤-trans (⌊n/2⌋≤n (suc m)) (s≤s h)))
            (strong-induction (suc n) ⌈ m /2⌉ (≤-trans (⌊n/2⌋≤n (suc m)) (s≤s h)))
        )
      ⟩
        suc (⌈ m /2⌉ + ⌈ m /2⌉)
      ≡⟨⟩
        suc (⌊ suc m /2⌋ + ⌈ m /2⌉)
      ≤⟨ s≤s (+-monoʳ-≤ ⌊ suc m /2⌋ (⌈n/2⌉-mono (n≤1+n m))) ⟩
        suc (⌊ suc m /2⌋ + ⌈ suc m /2⌉)
      ≡⟨ Eq.cong suc (⌊n/2⌋+⌈n/2⌉≡n (suc m)) ⟩
        suc (suc m)
      ∎
        where open ≤-Reasoning

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties of reflexive closures which rely on the K rule
------------------------------------------------------------------------

{-# OPTIONS --safe --with-K #-}

module Relation.Binary.Construct.Closure.Reflexive.Properties.WithK where

open import Data.Empty.Irrelevant using (⊥-elim)
open import Data.Product as Prod
open import Data.Sum.Base as Sum
open import Relation.Binary
open import Relation.Binary.Construct.Closure.Reflexive
open import Relation.Binary.Construct.Closure.Reflexive.Properties public
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong)
open import Relation.Nullary.Negation using (contradiction)

module _ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} where

  irrel : Irrelevant _∼_ → Irreflexive _≡_ _∼_ → Irrelevant (Refl _∼_)
  irrel irrel irrefl [ x∼y₁ ] [ x∼y₂ ] = cong [_] (irrel x∼y₁ x∼y₂)
  irrel irrel irrefl [ x∼y ]  refl     = contradiction x∼y (irrefl refl)
  irrel irrel irrefl refl     [ x∼y ]  = contradiction x∼y (irrefl refl)
  irrel irrel irrefl refl     refl     = refl


text:
module Setoids where

open import Eq
open import Prelude

record Setoid : Set1 where
  field
    carrier : Set
    _≈_     : carrier -> carrier -> Set
    equiv   : Equiv _≈_

record Datoid : Set1 where
  field
    setoid : Setoid
    _≟_    : forall x y -> Dec (Setoid._≈_ setoid x y)

Setoid-≡ : Set -> Setoid
Setoid-≡ a = record { carrier = a; _≈_ = _≡_; equiv = Equiv-≡ }

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
head : #$\forall$# {A n} → Vec A (1 + n) → A

zip : #$\forall$# {A B n} → Vec A n → Vec B n → Vec (A × B) n

take : #$\forall$# {A} m {n} → Vec A (m + n) → Vec A m

max_stars_repo_name: matt-noonan/gdp-talk

max_issues_repo_name: matt-noonan/gdp-talk

max_forks_repo_name: matt-noonan/gdp-talk


text:
-- Andreas, 2013-02-18 problem with 'with'-display, see also issue 295
-- {-# OPTIONS -v tc.with:50 #-}
module Issue800 where

  data ⊤ : Set where
    tt : ⊤

  data I⊤ : ⊤ → Set where
    itt : ∀ r → I⊤ r

  bug : ∀ l → ∀ k → I⊤ l → ⊤
  bug .l k (itt l) with itt k
  ... | foo = {! foo!}

{-
Current rewriting:
  bug .l l (itt k) | itt .k = ?

Desired rewriting:
  bug .l k (itt l) | itt .k = ?
-}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda