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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.IdUniv {{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.ShapeView
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.Idlemmas
open import Definition.LogicalRelation.Substitution.MaybeEmbed
-- 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

[Id]SProp : ∀ {t u Γ}
         (⊢Γ : ⊢ Γ)
         ([t] : Γ ⊩⟨ ι ⁰ ⟩ t ^ [ % , ι ⁰ ])
         ([u] : Γ ⊩⟨ ι ⁰ ⟩ u ^ [ % , ι ⁰ ])
         → Γ ⊩⟨ ι ¹ ⟩ Id (SProp ⁰) t u ^ [ % , ι ¹ ]
[Id]SProp {t} {u} {Γ} ⊢Γ [t] [u] =
  let
    ⊢t = escape [t]
    ⊢u = escape [u]
    ⊢wkt = Twk.wk (Twk.step Twk.id) (⊢Γ ∙ ⊢u) ⊢t
    ⊢wku = Twk.wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t) ⊢u
    [wkt] = λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wk [ρ] ⊢Δ [t]
    [wku] = λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wk [ρ] ⊢Δ [u]

    [t▹u] : Γ ⊩⟨ ι ⁰ ⟩ t ^ % ° ⁰ ▹▹ u ° ⁰ ° ¹ ^ [ % , ι ¹ ]
    [t▹u] = Πᵣ′ % ⁰ ⁰ (<is≤ 0<1) (<is≤ 0<1) t (wk1 u)
      (idRed:*: (univ (Πⱼ <is≤ 0<1 ▹ <is≤ 0<1 ▹ un-univ ⊢t ▹ un-univ ⊢wku))) ⊢t ⊢wku
      (≅-univ (≅ₜ-Π-cong (<is≤ 0<1) (<is≤ 0<1) ⊢t (≅-un-univ (escapeEqRefl [t])) (≅-un-univ (≅-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t) (escapeEqRefl [u])))))
      [wkt] ([nondep] [u] [wkt]) ([nondepext] [u] [wkt])
    [u▹t] : Γ ⊩⟨ ι ⁰ ⟩ u ^ % ° ⁰ ▹▹ t ° ⁰ ° ¹ ^ [ % , ι ¹ ]
    [u▹t] = Πᵣ′ % ⁰ ⁰ (<is≤ 0<1) (<is≤ 0<1) u (wk1 t)
      (idRed:*: (univ (Πⱼ <is≤ 0<1 ▹ <is≤ 0<1 ▹ un-univ ⊢u ▹ un-univ ⊢wkt))) ⊢u ⊢wkt
      (≅-univ (≅ₜ-Π-cong (<is≤ 0<1) (<is≤ 0<1) ⊢u (≅-un-univ (escapeEqRefl [u])) (≅-un-univ (≅-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢u) (escapeEqRefl [t])))))
      [wku] ([nondep] [t] [wku]) ([nondepext] [t] [wku])
    [wkt▹u] = λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wk [ρ] ⊢Δ (emb emb< [t▹u])
    ⊢t▹u = escape [t▹u]
    ⊢u▹t = Twk.wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t▹u) (escape [u▹t])

    ⊢Id = univ (Idⱼ (univ 0<1 ⊢Γ) (un-univ ⊢t) (un-univ ⊢u))
    ⊢Eq = univ (∃ⱼ un-univ ⊢t▹u ▹ un-univ ⊢u▹t)
  in ∃ᵣ′ (t ^ % ° ⁰ ▹▹ u ° ⁰ ° ¹) (wk1 (u ^ % ° ⁰ ▹▹ t ° ⁰ ° ¹))
    [[ ⊢Id , ⊢Eq , univ (Id-SProp (un-univ ⊢t) (un-univ ⊢u)) ⇨ id ⊢Eq ]] ⊢t▹u ⊢u▹t
    (≅-univ (≅ₜ-∃-cong ⊢t▹u (≅-un-univ (escapeEqRefl [t▹u])) (≅-un-univ (≅-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t▹u) (escapeEqRefl [u▹t])))))
    [wkt▹u] ([nondep] (emb emb< [u▹t]) [wkt▹u]) ([nondepext] (emb emb< [u▹t]) [wkt▹u])

[IdExt]SProp : ∀ {t t′ u u′ Γ}
         (⊢Γ : ⊢ Γ)
         ([t] : Γ ⊩⟨ ι ⁰ ⟩ t ^ [ % , ι ⁰ ])
         ([t′] : Γ ⊩⟨ ι ⁰ ⟩ t′ ^ [ % , ι ⁰ ])
         ([t≡t′] : Γ ⊩⟨ ι ⁰ ⟩ t ≡ t′ ^ [ % , ι ⁰ ] / [t])
         ([u] : Γ ⊩⟨ ι ⁰ ⟩ u ^ [ % , ι ⁰ ])
         ([u′] : Γ ⊩⟨ ι ⁰ ⟩ u′ ^ [ % , ι ⁰ ])
         ([u≡u′] : Γ ⊩⟨ ι ⁰ ⟩ u ≡ u′ ^ [ % , ι ⁰ ] / [u])
         → Γ ⊩⟨ ι ¹ ⟩ Id (SProp ⁰) t u ≡ Id (SProp ⁰) t′ u′ ^ [ % , ι ¹ ] / [Id]SProp ⊢Γ [t] [u]
[IdExt]SProp {t} {t′} {u} {u′} {Γ} ⊢Γ [t] [t′] [t≡t′] [u] [u′] [u≡u′] =
  let ⊢t = escape [t]
      ⊢t′ = escape [t′]
      ⊢u = escape [u]
      ⊢u′ = escape [u′]
      ⊢t≡t′ = ≅-un-univ (escapeEq [t] [t≡t′])
      ⊢u≡u′ = ≅-un-univ (escapeEq [u] [u≡u′])

      ⊢wkt = Twk.wk (Twk.step Twk.id) (⊢Γ ∙ ⊢u) ⊢t
      ⊢wku = Twk.wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t) ⊢u
      [wkt] = λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wk [ρ] ⊢Δ [t]
      [wku] = λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wk [ρ] ⊢Δ [u]

      ⊢wkt′ = Twk.wk (Twk.step Twk.id) (⊢Γ ∙ ⊢u′) ⊢t′
      ⊢wku′ = Twk.wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t′) ⊢u′
      [wkt′] = λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wk [ρ] ⊢Δ [t′]
      [wku′] = λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wk [ρ] ⊢Δ [u′]

      [t▹u] : Γ ⊩⟨ ι ⁰ ⟩ t ^ % ° ⁰ ▹▹ u ° ⁰ ° ¹ ^ [ % , ι ¹ ]
      [t▹u] = Πᵣ′ % ⁰ ⁰ (<is≤ 0<1) (<is≤ 0<1) t (wk1 u)
        (idRed:*: (univ (Πⱼ <is≤ 0<1 ▹ <is≤ 0<1 ▹ un-univ ⊢t ▹ un-univ ⊢wku))) ⊢t ⊢wku
        (≅-univ (≅ₜ-Π-cong (<is≤ 0<1) (<is≤ 0<1) ⊢t (≅-un-univ (escapeEqRefl [t])) (≅-un-univ (≅-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t) (escapeEqRefl [u])))))
        [wkt] ([nondep] [u] [wkt]) ([nondepext] [u] [wkt])
      [u▹t] : Γ ⊩⟨ ι ⁰ ⟩ u ^ % ° ⁰ ▹▹ t ° ⁰ ° ¹ ^ [ % , ι ¹ ]
      [u▹t] = Πᵣ′ % ⁰ ⁰ (<is≤ 0<1) (<is≤ 0<1) u (wk1 t)
        (idRed:*: (univ (Πⱼ <is≤ 0<1 ▹ <is≤ 0<1 ▹ un-univ ⊢u ▹ un-univ ⊢wkt))) ⊢u ⊢wkt
        (≅-univ (≅ₜ-Π-cong (<is≤ 0<1) (<is≤ 0<1) ⊢u (≅-un-univ (escapeEqRefl [u])) (≅-un-univ (≅-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢u) (escapeEqRefl [t])))))
        [wku] ([nondep] [t] [wku]) ([nondepext] [t] [wku])

      [t▹u′] : Γ ⊩⟨ ι ⁰ ⟩ t′ ^ % ° ⁰ ▹▹ u′ ° ⁰ ° ¹ ^ [ % , ι ¹ ]
      [t▹u′] = Πᵣ′ % ⁰ ⁰ (<is≤ 0<1) (<is≤ 0<1) t′ (wk1 u′)
        (idRed:*: (univ (Πⱼ <is≤ 0<1 ▹ <is≤ 0<1 ▹ un-univ ⊢t′ ▹ un-univ ⊢wku′))) ⊢t′ ⊢wku′
        (≅-univ (≅ₜ-Π-cong (<is≤ 0<1) (<is≤ 0<1) ⊢t′ (≅-un-univ (escapeEqRefl [t′])) (≅-un-univ (≅-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t′) (escapeEqRefl [u′])))))
        [wkt′] ([nondep] [u′] [wkt′]) ([nondepext] [u′] [wkt′])
      [u▹t′] : Γ ⊩⟨ ι ⁰ ⟩ u′ ^ % ° ⁰ ▹▹ t′ ° ⁰ ° ¹ ^ [ % , ι ¹ ]
      [u▹t′] = Πᵣ′ % ⁰ ⁰ (<is≤ 0<1) (<is≤ 0<1) u′ (wk1 t′)
        (idRed:*: (univ (Πⱼ <is≤ 0<1 ▹ <is≤ 0<1 ▹ un-univ ⊢u′ ▹ un-univ ⊢wkt′)))
        ⊢u′ ⊢wkt′
        (≅-univ (≅ₜ-Π-cong (<is≤ 0<1) (<is≤ 0<1) ⊢u′ (≅-un-univ (escapeEqRefl [u′])) (≅-un-univ (≅-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢u′) (escapeEqRefl [t′])))))
        [wku′] ([nondep] [t′] [wku′]) ([nondepext] [t′] [wku′])

      [t▹u≡t▹u′] : Γ ⊩⟨ ι ⁰ ⟩ t ^ % ° ⁰ ▹▹ u ° ⁰ ° ¹  ≡ t′ ^ % ° ⁰ ▹▹ u′ ° ⁰ ° ¹  ^ [ % , ι ¹ ] / [t▹u]
      [t▹u≡t▹u′] = Π₌ t′ (wk1 u′) (id (univ (Πⱼ <is≤ 0<1 ▹ <is≤ 0<1 ▹ un-univ ⊢t′ ▹ un-univ ⊢wku′)))
                      (≅-univ (≅ₜ-Π-cong (<is≤ 0<1) (<is≤ 0<1) ⊢t ⊢t≡t′ (≅ₜ-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t) ⊢u≡u′)))
                      (λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wkEq [ρ] ⊢Δ (emb emb< [t]) [t≡t′])
                      ([nondepext'] [u] [u′] [u≡u′] [wkt] [wkt′])

      [u▹t≡u▹t′] : Γ ⊩⟨ ι ⁰ ⟩ u ^ % ° ⁰ ▹▹ t ° ⁰ ° ¹  ≡ u′ ^ % ° ⁰ ▹▹ t′ ° ⁰ ° ¹  ^ [ % , ι ¹ ] / [u▹t]
      [u▹t≡u▹t′] = Π₌ u′ (wk1 t′) (id (univ (Πⱼ <is≤ 0<1 ▹ <is≤ 0<1 ▹ un-univ ⊢u′ ▹ un-univ ⊢wkt′)))
                      (≅-univ (≅ₜ-Π-cong (<is≤ 0<1) (<is≤ 0<1) ⊢u ⊢u≡u′ (≅ₜ-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢u) ⊢t≡t′)))
                      (λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wkEq [ρ] ⊢Δ (emb emb< [u]) [u≡u′])
                      ([nondepext'] [t] [t′] [t≡t′] [wku] [wku′])

      ⊢t▹u = escape [t▹u]

  in ∃₌ {l′ = ¹} (t′ ^ % ° ⁰ ▹▹ u′ ° ⁰ ° ¹ ) (wk1 (u′ ^ % ° ⁰ ▹▹ t′ ° ⁰ ° ¹ ))
        (univ (Id-SProp (un-univ ⊢t′) (un-univ ⊢u′)) ⇨ id (univ (××ⱼ (▹▹ⱼ <is≤ 0<1 ▹ <is≤ 0<1 ▹ un-univ ⊢t′ ▹ un-univ ⊢u′) ▹
                                                                     (▹▹ⱼ <is≤ 0<1 ▹ <is≤ 0<1 ▹ un-univ ⊢u′ ▹ un-univ ⊢t′))))
        (≅-univ (≅ₜ-∃-cong ⊢t▹u
                           (≅ₜ-Π-cong (<is≤ 0<1) (<is≤ 0<1) ⊢t ⊢t≡t′ (≅ₜ-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t) ⊢u≡u′))
                           (≅ₜ-Π-cong (<is≤ 0<1) (<is≤ 0<1) (Twk.wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t▹u) ⊢u)
                                      (≅ₜ-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t▹u) ⊢u≡u′)
                                      (≅ₜ-wk (Twk.lift (Twk.step Twk.id)) ((⊢Γ ∙ ⊢t▹u) ∙
                                                       (Twk.wk (Twk.step Twk.id) (⊢Γ ∙ ⊢t▹u) ⊢u))
                                             (≅ₜ-wk (Twk.step Twk.id) (⊢Γ ∙ ⊢u) ⊢t≡t′)) )))
        (λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wkEq [ρ] ⊢Δ [t▹u] [t▹u≡t▹u′])
        ([nondepext'] (emb emb< [u▹t]) (emb emb< [u▹t′]) [u▹t≡u▹t′]
                      (λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wk [ρ] ⊢Δ (emb emb< [t▹u]))
                      (λ {ρ} {Δ} ([ρ] : ρ Twk.∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ) → Lwk.wk [ρ] ⊢Δ (emb emb< [t▹u′])))

[Id]U : ∀ {A B Γ}
         (⊢Γ : ⊢ Γ)
         ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ [ ! , ι ⁰ ])
         ([B] : Γ ⊩⟨ ι ⁰ ⟩ B ^ [ ! , ι ⁰ ])
         → Γ ⊩⟨ ι ¹ ⟩ Id (U ⁰) A B ^ [ % , ι ¹ ]
[IdExtShape]U : ∀ {A A′ B B′ Γ}
         (⊢Γ : ⊢ Γ)
         ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ [ ! , ι ⁰ ])
         ([A′] : Γ ⊩⟨ ι ⁰ ⟩ A′ ^ [ ! , ι ⁰ ])
         (ShapeA : ShapeView Γ (ι ⁰) (ι ⁰) A A′ [ ! , ι ⁰ ] [ ! , ι ⁰ ] [A] [A′])
         ([A≡A′] : Γ ⊩⟨ ι ⁰ ⟩ A ≡ A′ ^ [ ! , ι ⁰ ] / [A])
         ([B] : Γ ⊩⟨ ι ⁰ ⟩ B ^ [ ! , ι ⁰ ])
         ([B′] : Γ ⊩⟨ ι ⁰ ⟩ B′ ^ [ ! , ι ⁰ ])
         (ShapeB : ShapeView Γ (ι ⁰) (ι ⁰) B B′ [ ! , ι ⁰ ] [ ! , ι ⁰ ] [B] [B′])
         ([B≡B′] : Γ ⊩⟨ ι ⁰ ⟩ B ≡ B′ ^ [ ! , ι ⁰ ] / [B])
         → Γ ⊩⟨ ι ¹ ⟩ Id (U ⁰) A B ≡ Id (U ⁰) A′ B′ ^ [ % , ι ¹ ] / [Id]U ⊢Γ [A] [B]
[IdExt]U : ∀ {A A′ B B′ Γ}
         (⊢Γ : ⊢ Γ)
         ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ [ ! , ι ⁰ ])
         ([A′] : Γ ⊩⟨ ι ⁰ ⟩ A′ ^ [ ! , ι ⁰ ])
         ([A≡A′] : Γ ⊩⟨ ι ⁰ ⟩ A ≡ A′ ^ [ ! , ι ⁰ ] / [A])
         ([B] : Γ ⊩⟨ ι ⁰ ⟩ B ^ [ ! , ι ⁰ ])
         ([B′] : Γ ⊩⟨ ι ⁰ ⟩ B′ ^ [ ! , ι ⁰ ])
         ([B≡B′] : Γ ⊩⟨ ι ⁰ ⟩ B ≡ B′ ^ [ ! , ι ⁰ ] / [B])
         → Γ ⊩⟨ ι ¹ ⟩ Id (U ⁰) A B ≡ Id (U ⁰) A′ B′ ^ [ % , ι ¹ ] / [Id]U ⊢Γ [A] [B]

[Id]U {A} {B} ⊢Γ (ne′ K D neK K≡K) [B] =
  let ⊢B = escape [B]
      B≡B = escapeEqRefl [B]
  in ne (ne (Id (U ⁰) K B) (univ:⇒*: (IdURed*Term (un-univ:⇒*: D) (un-univ ⊢B))) (IdUₙ neK) (~-IdU ⊢Γ K≡K (≅-un-univ B≡B)))

[Id]U ⊢Γ (ℕᵣ [[ ⊢A , ⊢K , D ]]) (ℕᵣ [[ ⊢B , ⊢L , D₁ ]]) =
  let
    ⊢tA = (subset* D)
  in proj₁ (redSubst* (trans⇒* (univ⇒* (IdURed*Term′ (un-univ ⊢A) (un-univ ⊢K) (un-univ⇒* D) (un-univ ⊢B)))
                        (trans⇒* (univ⇒* (IdUℕRed*Term′ (un-univ ⊢B) (un-univ ⊢L) (un-univ⇒* D₁))) (univ (Id-U-ℕℕ ⊢Γ) ⇨ id (univ (Unitⱼ ⊢Γ))))) (UnitType ⊢Γ))

[Id]U ⊢Γ (ℕᵣ D) (ne′ K D₁ neK K≡K) =
  let [B] = ne′ K D₁ neK K≡K
      ⊢B = escape {l = ι ¹} [B]
  in ne′ (Id (U ⁰) ℕ K) (univ:⇒*: (transTerm:⇒:* (IdURed*Term (un-univ:⇒*: D) (un-univ ⊢B) ) (IdUℕRed*Term (un-univ:⇒*: D₁))))
         (IdUℕₙ neK) (~-IdUℕ ⊢Γ K≡K)

[Id]U ⊢Γ (ℕᵣ [[ ⊢A , ⊢ℕ , D ]]) (Πᵣ′ rF lF lG (≡is≤ PE.refl) (≡is≤ PE.refl) F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  let [B] = Πᵣ′ rF lF lG (≡is≤ PE.refl) (≡is≤ PE.refl) F G D′ ⊢F ⊢G A≡A [F] [G] G-ext
      ⊢B = escape [B]
  in proj₁ (redSubst* (trans⇒* (univ⇒* (IdURed*Term′ (un-univ ⊢A) (un-univ ⊢ℕ) (un-univ⇒* D) (un-univ ⊢B)))
                        (trans⇒* (univ⇒* (IdUℕRed*Term′ (un-univ ⊢B) (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ (un-univ ⊢F) ▹ (un-univ ⊢G)) (un-univ⇒* (red D′))))
                                 (univ (Id-U-ℕΠ (un-univ ⊢F) (un-univ ⊢G)) ⇨ id (univ (Emptyⱼ ⊢Γ))))) (EmptyType ⊢Γ))

[Id]U ⊢Γ (Πᵣ′ rF lF lG (≡is≤ PE.refl) (≡is≤ PE.refl) F G [[ ⊢A , ⊢Π , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) (ℕᵣ [[ ⊢B , ⊢ℕ , D' ]]) =
  proj₁ (redSubst* (trans⇒* (univ⇒* (IdURed*Term′ (un-univ ⊢A) (un-univ ⊢Π) (un-univ⇒* D) (un-univ ⊢B)))
                        (trans⇒* (univ⇒* (IdUΠRed*Term′ (un-univ ⊢F) (un-univ ⊢G) (un-univ ⊢B) (un-univ ⊢ℕ) (un-univ⇒* D')))
                                 (univ (Id-U-Πℕ (un-univ ⊢F) (un-univ ⊢G)) ⇨ id (univ (Emptyⱼ ⊢Γ))))) (EmptyType ⊢Γ))

[Id]U ⊢Γ (Πᵣ′ rF lF lG (≡is≤ PE.refl) (≡is≤ PE.refl) F G D ⊢F ⊢G A≡A [F] [G] G-ext) (ne′ K D₁ neK K≡K) =
  let [B] = ne′ K D₁ neK K≡K
      ⊢B = escape {l = ι ¹} [B]
      -- [F]' = PE.subst (λ X → _  ⊩⟨ _ ⟩ X ^ [ _ , _ ]) (wk-id F) ([F] Twk.id ⊢Γ)
      -- ⊢F≅F = ≅-un-univ (escapeEqRefl [F]')
      -- [G]' = PE.subst (λ X → _  ⊩⟨ _ ⟩ X ^ [ _ , _ ]) (wkSingleSubstId G) ([G] {a = var 0} (Twk.step Twk.id) (⊢Γ ∙ ⊢F) {!!})
      -- ⊢G≅G = ≅-un-univ (escapeEqRefl [G]')
  in ne′ (Id (U ⁰) (Π F ^ rF ° lF ▹ G ° lG ° ⁰) K)
         (univ:⇒*: (transTerm:⇒:* (IdURed*Term (un-univ:⇒*: D) (un-univ ⊢B) ) (IdUΠRed*Term (un-univ ⊢F) (un-univ ⊢G) (un-univ:⇒*: D₁))))
         (IdUΠₙ neK) (~-IdUΠ (≅-un-univ A≡A) K≡K)

[Id]U {A} {B} {Γ} ⊢Γ (Πᵣ′ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F G [[ ⊢A , ⊢ΠFG , D ]] ⊢F ⊢G A≡A [F] [G] G-ext)
  (Πᵣ′ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢B , ⊢ΠF₁G₁ , D₁ ]] ⊢F₁ ⊢G₁ B≡B [F₁] [G₁] G₁-ext) =
  ∃ᵣ′ (Id (U ⁰) F F₁) (IdGG₁ (step id) (var 0))
    [[ (univ (Idⱼ (univ 0<1 ⊢Γ) (un-univ ⊢A) (un-univ ⊢B))) , ⊢∃ , D∃ ]]
    ⊢IdFF₁ ⊢IdGG₁ ∃≡∃ [IdFF₁]
    (λ {ρ} {Δ} {a} [ρ] ⊢Δ [a] → PE.subst (λ X → Δ ⊩⟨ ι ¹ ⟩ X ^ [ % , ι ¹ ]) (PE.sym (wksubst-IdTel ρ a)) ([IdGG₁] [ρ] ⊢Δ [a]))
    (λ {ρ} {Δ} {a} {b} [ρ] ⊢Δ [a] [b] [a≡b] → irrelevanceEq″ (PE.sym (wksubst-IdTel ρ a)) (PE.sym (wksubst-IdTel ρ b)) PE.refl PE.refl
      ([IdGG₁] [ρ] ⊢Δ [a]) (PE.subst (λ X → Δ ⊩⟨ ι ¹ ⟩ X ^ [ % , ι ¹ ]) (PE.sym (wksubst-IdTel ρ a)) ([IdGG₁] [ρ] ⊢Δ [a]))
      ([IdGG₁-ext] [ρ] ⊢Δ [a] [b] [a≡b]))
  where
    open IdTypeU-lemmas ⊢Γ ⊢A ⊢ΠFG D ⊢F ⊢G A≡A [F] [G] G-ext ⊢B ⊢ΠF₁G₁ D₁ ⊢F₁ ⊢G₁ B≡B [F₁] [G₁] G₁-ext
      (λ [ρ] ⊢Δ → [Id]U ⊢Δ ([F] [ρ] ⊢Δ) ([F₁] [ρ] ⊢Δ))
      (λ [ρ] ⊢Δ [x] [y] → [Id]U ⊢Δ ([G] [ρ] ⊢Δ [x]) ([G₁] [ρ] ⊢Δ [y]))
      (λ [ρ] ⊢Δ [x] [x′] [x≡x′] [y] [y′] [y≡y′] →
        [IdExt]U ⊢Δ ([G] [ρ] ⊢Δ [x]) ([G] [ρ] ⊢Δ [x′]) (G-ext [ρ] ⊢Δ [x] [x′] [x≡x′]) ([G₁] [ρ] ⊢Δ [y]) ([G₁] [ρ] ⊢Δ [y′]) (G₁-ext [ρ] ⊢Δ [y] [y′] [y≡y′]))

[Id]U {A} {B} {Γ} ⊢Γ (Πᵣ′ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F G [[ ⊢A , ⊢ΠFG , D ]] ⊢F ⊢G A≡A [F] [G] G-ext)
  (Πᵣ′ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢B , ⊢ΠF₁G₁ , D₁ ]] ⊢F₁ ⊢G₁ B≡B [F₁] [G₁] G₁-ext) =
  ∃ᵣ′ (Id (SProp ⁰) F F₁) (IdGG₁ (step id) (var 0))
    [[ (univ (Idⱼ (univ 0<1 ⊢Γ) (un-univ ⊢A) (un-univ ⊢B))) , ⊢∃ , D∃ ]]
    ⊢IdFF₁ ⊢IdGG₁ ∃≡∃ [IdFF₁]
    (λ {ρ} {Δ} {a} [ρ] ⊢Δ [a] → PE.subst (λ X → Δ ⊩⟨ ι ¹ ⟩ X ^ [ % , ι ¹ ]) (PE.sym (wksubst-IdTel ρ a)) ([IdGG₁] [ρ] ⊢Δ [a]))
    (λ {ρ} {Δ} {a} {b} [ρ] ⊢Δ [a] [b] [a≡b] → irrelevanceEq″ (PE.sym (wksubst-IdTel ρ a)) (PE.sym (wksubst-IdTel ρ b)) PE.refl PE.refl
      ([IdGG₁] [ρ] ⊢Δ [a]) (PE.subst (λ X → Δ ⊩⟨ ι ¹ ⟩ X ^ [ % , ι ¹ ]) (PE.sym (wksubst-IdTel ρ a)) ([IdGG₁] [ρ] ⊢Δ [a]))
      ([IdGG₁-ext] [ρ] ⊢Δ [a] [b] [a≡b]))
  where
    open IdTypeU-lemmas ⊢Γ ⊢A ⊢ΠFG D ⊢F ⊢G A≡A [F] [G] G-ext ⊢B ⊢ΠF₁G₁ D₁ ⊢F₁ ⊢G₁ B≡B [F₁] [G₁] G₁-ext
      (λ [ρ] ⊢Δ → [Id]SProp ⊢Δ ([F] [ρ] ⊢Δ) ([F₁] [ρ] ⊢Δ))
      (λ [ρ] ⊢Δ [x] [y] → [Id]U ⊢Δ ([G] [ρ] ⊢Δ [x]) ([G₁] [ρ] ⊢Δ [y]))
      (λ [ρ] ⊢Δ [x] [x′] [x≡x′] [y] [y′] [y≡y′] →
        [IdExt]U ⊢Δ ([G] [ρ] ⊢Δ [x]) ([G] [ρ] ⊢Δ [x′]) (G-ext [ρ] ⊢Δ [x] [x′] [x≡x′]) ([G₁] [ρ] ⊢Δ [y]) ([G₁] [ρ] ⊢Δ [y′]) (G₁-ext [ρ] ⊢Δ [y] [y′] [y≡y′]))

[Id]U ⊢Γ (Πᵣ′ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F G [[ ⊢A , ⊢ΠFG , D ]] ⊢F ⊢G A≡A [F] [G] G-ext)
         (Πᵣ′ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢B , ⊢ΠF₁G₁ , D' ]] ⊢F₁ ⊢G₁ B≡B [F₁] [G₁] G₁-ext) =
    proj₁ (redSubst* (trans⇒* (univ⇒* (IdURed*Term′ (un-univ ⊢A) (un-univ ⊢ΠFG) (un-univ⇒* D) (un-univ ⊢B)))
                        (trans⇒* (univ⇒* (IdUΠRed*Term′ (un-univ ⊢F) (un-univ ⊢G) (un-univ ⊢B) (un-univ ⊢ΠF₁G₁) (un-univ⇒* D')))
                                 (univ (Id-U-ΠΠ!% !≢% (un-univ ⊢F) (un-univ ⊢G) (un-univ ⊢F₁) (un-univ ⊢G₁)) ⇨ id (univ (Emptyⱼ ⊢Γ))))) (EmptyType ⊢Γ))

[Id]U ⊢Γ (Πᵣ′ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F G [[ ⊢A , ⊢ΠFG , D ]] ⊢F ⊢G A≡A [F] [G] G-ext)
  (Πᵣ′ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢B , ⊢ΠF₁G₁ , D' ]] ⊢F₁ ⊢G₁ B≡B [F₁] [G₁] G₁-ext) =
    proj₁ (redSubst* (trans⇒* (univ⇒* (IdURed*Term′ (un-univ ⊢A) (un-univ ⊢ΠFG) (un-univ⇒* D) (un-univ ⊢B)))
                       (trans⇒* (univ⇒* (IdUΠRed*Term′ (un-univ ⊢F) (un-univ ⊢G) (un-univ ⊢B) (un-univ ⊢ΠF₁G₁) (un-univ⇒* D')))
                                 (univ (Id-U-ΠΠ!% (λ e → !≢% (PE.sym e)) (un-univ ⊢F) (un-univ ⊢G) (un-univ ⊢F₁) (un-univ ⊢G₁)) ⇨ id (univ (Emptyⱼ ⊢Γ))))) (EmptyType ⊢Γ))

[IdExtShape]U ⊢Γ _ _ (ℕᵥ ℕA [[ ⊢A , ⊢K , D ]]) [A≡A′] _ _ (ℕᵥ NB [[ ⊢B , ⊢L , D₁ ]]) [B≡B′] =
  Π₌ (Empty _) (Empty _)
    (trans⇒* (univ⇒* (IdURed*Term′ (un-univ ⊢A) (un-univ ⊢K) (un-univ⇒* D) (un-univ ⊢B)))
                        (trans⇒* (univ⇒* (IdUℕRed*Term′ (un-univ ⊢B) (un-univ ⊢L) (un-univ⇒* D₁))) (univ (Id-U-ℕℕ ⊢Γ) ⇨ id (univ (Unitⱼ ⊢Γ)))))
                        (≅-univ (Unit≡Unit ⊢Γ))
    (λ [ρ] ⊢Δ → id (univ (Emptyⱼ ⊢Δ)))
    λ [ρ] ⊢Δ [a] → id (univ (Emptyⱼ ⊢Δ))

[IdExtShape]U ⊢Γ _ _ (ℕᵥ ℕA D) [A≡A′] _ _ (ne neB neB') (ne₌ M D′ neM K≡M) =
  let [[ ⊢B , _ ,  _ ]] = D′
  in ne₌ (Id (U ⁰) ℕ M) (univ:⇒*: (transTerm:⇒:* (IdURed*Term (un-univ:⇒*: D) (un-univ ⊢B) ) (IdUℕRed*Term (un-univ:⇒*: D′))))
         (IdUℕₙ neM) (~-IdUℕ ⊢Γ K≡M)

[IdExtShape]U ⊢Γ _ _ (ℕᵥ [[ ⊢A , ⊢ℕ , D ]] [[ ⊢A' , ⊢ℕ' , D' ]]) [A≡A′] _ _
                     (Πᵥ (Πᵣ rF lF lG (≡is≤ PE.refl) (≡is≤ PE.refl) F G D′ ⊢F ⊢G A≡A [F] [G] G-ext)
                         (Πᵣ rF' lF' lG' (≡is≤ PE.refl) (≡is≤ PE.refl) F' G' D′' ⊢F' ⊢G' A≡A' [F]' [G]' G-ext')) [B≡B′] =
  let [B]' = Πᵣ′ rF' lF' lG' (≡is≤ PE.refl) (≡is≤ PE.refl) F' G' D′' ⊢F' ⊢G' A≡A' [F]' [G]' G-ext'
      ⊢B' = escape [B]'
  in trans⇒* (univ⇒* (IdURed*Term′ (un-univ ⊢A') (un-univ ⊢ℕ') (un-univ⇒* D') (un-univ ⊢B')))
                        (trans⇒* (univ⇒* (IdUℕRed*Term′ (un-univ ⊢B') (Πⱼ ≡is≤ PE.refl ▹ ≡is≤ PE.refl ▹ (un-univ ⊢F') ▹ (un-univ ⊢G')) (un-univ⇒* (red D′'))))
                                 (univ (Id-U-ℕΠ (un-univ ⊢F') (un-univ ⊢G')) ⇨ id (univ (Emptyⱼ ⊢Γ))))

[IdExtShape]U {A} {A′} {B} {B′} ⊢Γ _ _ (ne neA neA') (ne₌ M D neM K≡M) [B] [B'] [ShapeB] [B≡B′] =
  let ⊢B' = escape [B']
      B≡B' = escapeEq [B] [B≡B′]
  in ne₌ (Id (U ⁰) M B′) (univ:⇒*: (IdURed*Term (un-univ:⇒*: D) (un-univ ⊢B')))
         (IdUₙ neM) (~-IdU ⊢Γ K≡M (≅-un-univ B≡B'))

[IdExtShape]U ⊢Γ _ _ (Πᵥ (Πᵣ rF lF lG (≡is≤ PE.refl) (≡is≤ PE.refl) F G D′ ⊢F ⊢G A≡A [F] [G] G-ext)
                         (Πᵣ rF' lF' lG' (≡is≤ PE.refl) (≡is≤ PE.refl) F' G' [[ ⊢A' , ⊢Π' , DΠ' ]] ⊢F' ⊢G' A≡A' [F]' [G]' G-ext')) [A≡A′] _ _
                     (ℕᵥ [[ ⊢A , ⊢ℕ , D ]] [[ ⊢B' , ⊢ℕ' , D' ]]) [B≡B′] =
   trans⇒* (univ⇒* (IdURed*Term′ (un-univ ⊢A') (un-univ ⊢Π') (un-univ⇒* DΠ') (un-univ ⊢B')))
                        (trans⇒* (univ⇒* (IdUΠRed*Term′ (un-univ ⊢F') (un-univ ⊢G') (un-univ ⊢B') (un-univ ⊢ℕ') (un-univ⇒* D')))
                                 (univ (Id-U-Πℕ (un-univ ⊢F') (un-univ ⊢G')) ⇨ id (univ (Emptyⱼ ⊢Γ))))

[IdExtShape]U ⊢Γ _ _ (Πᵥ (Πᵣ rF' .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F' G' De' ⊢F' ⊢G' A≡A' [F]' [G]' G-ext')
                         (Πᵣ rF .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (Π₌ F′ G′ D′₁ A≡B [F≡F′] [G≡G′])
                 _ _ (ne neA neB) (ne₌ M D′ neM K≡M) =
  let [[ ⊢B , _ ,  _ ]] = D′
      Π≡Π = whrDet* (red D , Whnf.Πₙ) (D′₁ , Whnf.Πₙ)
      F≡F' , rF≡rF' , _ , G≡G' , _  = Π-PE-injectivity Π≡Π
  in ne₌ (Id (U ⁰) (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) M)
         (univ:⇒*: (transTerm:⇒:* (IdURed*Term (un-univ:⇒*: D) (un-univ ⊢B) ) (IdUΠRed*Term (un-univ ⊢F) (un-univ ⊢G) (un-univ:⇒*: D′))))
         (IdUΠₙ neM) (PE.subst (λ X → _  ⊢ Id (U ⁰) (Π F' ^ rF' ° ⁰ ▹ G' ° ⁰ ° ⁰) _ ~ Id (U ⁰) (Π F ^ X ° ⁰ ▹ G ° ⁰ ° ⁰) M ∷ SProp _ ^ _) (PE.sym rF≡rF')
                               (~-IdUΠ (≅-un-univ
                                 (PE.subst (λ X → _ ⊢ Π F' ^ rF' ° ⁰ ▹ G' ° ⁰ ° ⁰ ≅  Π F ^ rF' ° ⁰ ▹ X ° ⁰ ° ⁰ ^ _ ) (PE.sym G≡G')
                                   (PE.subst (λ X → _ ⊢ Π F' ^ rF' ° ⁰ ▹ G' ° ⁰ ° ⁰ ≅  Π X ^ rF' ° ⁰ ▹ G′ ° ⁰ ° ⁰ ^ _ ) (PE.sym F≡F') A≡B))) K≡M))

[IdExtShape]U ⊢Γ _ _ (Πᵥ (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢A₁ , ⊢ΠF₁G₁ , D₁ ]] ⊢F₁ ⊢G₁ A₁≡A₁ [F₁] [G₁] G₁-ext)
                         (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₂ G₂ [[ ⊢A₂ , ⊢ΠF₂G₂ , D₂ ]] ⊢F₂ ⊢G₂ A₂≡A₂ [F₂] [G₂] G₂-ext))
                      (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
                 _ _ (Πᵥ _ _) (Π₌ F′₁ G′₁ D′₁ A≡B₁ [F≡F′]₁ [G≡G′]₁) =
  let ΠFG′≡ΠFG′₁ = whrDet* (D₂ , Πₙ) (D′ , Πₙ)
      F′≡F′₁ , rF≡rF′ , _ , G′≡G′₁ , _  = Π-PE-injectivity ΠFG′≡ΠFG′₁
  in ⊥-elim (!≢% rF≡rF′)

[IdExtShape]U ⊢Γ _ _ (Πᵥ (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢A₁ , ⊢ΠF₁G₁ , D₁ ]] ⊢F₁ ⊢G₁ A₁≡A₁ [F₁] [G₁] G₁-ext)
                         (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₂ G₂ [[ ⊢A₂ , ⊢ΠF₂G₂ , D₂ ]] ⊢F₂ ⊢G₂ A₂≡A₂ [F₂] [G₂] G₂-ext))
                      (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
                 _ _ (Πᵥ _ _) (Π₌ F′₁ G′₁ D′₁ A≡B₁ [F≡F′]₁ [G≡G′]₁) =
  let ΠFG′≡ΠFG′₁ = whrDet* (D₂ , Πₙ) (D′ , Πₙ)
      F′≡F′₁ , rF≡rF′ , _ , G′≡G′₁ , _  = Π-PE-injectivity ΠFG′≡ΠFG′₁
  in ⊥-elim (!≢% (PE.sym rF≡rF′))

[IdExtShape]U ⊢Γ _ _ (Πᵥ _ _)
                      (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
                 _ _ (Πᵥ (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢A₁ , ⊢ΠF₁G₁ , D₁ ]] ⊢F₁ ⊢G₁ A₁≡A₁ [F₁] [G₁] G₁-ext)
                         (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₂ G₂ [[ ⊢A₂ , ⊢ΠF₂G₂ , D₂ ]] ⊢F₂ ⊢G₂ A₂≡A₂ [F₂] [G₂] G₂-ext)) (Π₌ F′₁ G′₁ D′₁ A≡B₁ [F≡F′]₁ [G≡G′]₁) =
  let ΠFG′≡ΠFG′₁ = whrDet* (D₂ , Πₙ) (D′₁ , Πₙ)
      F′≡F′₁ , rF≡rF′ , _ , G′≡G′₁ , _  = Π-PE-injectivity ΠFG′≡ΠFG′₁
  in ⊥-elim (!≢% rF≡rF′)

[IdExtShape]U ⊢Γ _ _ (Πᵥ _ _)
                      (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
                 _ _ (Πᵥ (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢A₁ , ⊢ΠF₁G₁ , D₁ ]] ⊢F₁ ⊢G₁ A₁≡A₁ [F₁] [G₁] G₁-ext)
                         (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₂ G₂ [[ ⊢A₂ , ⊢ΠF₂G₂ , D₂ ]] ⊢F₂ ⊢G₂ A₂≡A₂ [F₂] [G₂] G₂-ext)) (Π₌ F′₁ G′₁ D′₁ A≡B₁ [F≡F′]₁ [G≡G′]₁) =
  let ΠFG′≡ΠFG′₁ = whrDet* (D₂ , Πₙ) (D′₁ , Πₙ)
      F′≡F′₁ , rF≡rF′ , _ , G′≡G′₁ , _  = Π-PE-injectivity ΠFG′≡ΠFG′₁
  in ⊥-elim (!≢% (PE.sym rF≡rF′))

[IdExtShape]U ⊢Γ _ _ (Πᵥ (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢A₁ , ⊢ΠF₁G₁ , D₁ ]] ⊢F₁ ⊢G₁ A₁≡A₁ [F₁] [G₁] G₁-ext)
                         (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₂ G₂ [[ ⊢A₂ , ⊢ΠF₂G₂ , D₂ ]] ⊢F₂ ⊢G₂ A₂≡A₂ [F₂] [G₂] G₂-ext))
                      (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
                 _ _ (Πᵥ (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₃ G₃ [[ ⊢A₃ , ⊢ΠF₃G₃ , D₃ ]] ⊢F₃ ⊢G₃ A₃≡A₃ [F₃] [G₃] G₃-ext)
                         (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₄ G₄ [[ ⊢A₄ , ⊢ΠF₄G₄ , D₄ ]] ⊢F₄ ⊢G₄ A₄≡A₄ [F₄] [G₄] G₄-ext)) (Π₌ F′₁ G′₁ D′₁ A≡B₁ [F≡F′]₁ [G≡G′]₁) =
  trans⇒* (univ⇒* (IdURed*Term′ (un-univ ⊢A₂) (un-univ ⊢ΠF₂G₂) (un-univ⇒* D₂) (un-univ ⊢A₄)))
                        (trans⇒* (univ⇒* (IdUΠRed*Term′ (un-univ ⊢F₂) (un-univ ⊢G₂) (un-univ ⊢A₄) (un-univ ⊢ΠF₄G₄) (un-univ⇒* D₄)))
                                 (univ (Id-U-ΠΠ!% !≢% (un-univ ⊢F₂) (un-univ ⊢G₂) (un-univ ⊢F₄) (un-univ ⊢G₄)) ⇨ id (univ (Emptyⱼ ⊢Γ))))

[IdExtShape]U ⊢Γ _ _ (Πᵥ (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢A₁ , ⊢ΠF₁G₁ , D₁ ]] ⊢F₁ ⊢G₁ A₁≡A₁ [F₁] [G₁] G₁-ext)
                         (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₂ G₂ [[ ⊢A₂ , ⊢ΠF₂G₂ , D₂ ]] ⊢F₂ ⊢G₂ A₂≡A₂ [F₂] [G₂] G₂-ext))
                      (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
                 _ _ (Πᵥ (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₃ G₃ [[ ⊢A₃ , ⊢ΠF₃G₃ , D₃ ]] ⊢F₃ ⊢G₃ A₃≡A₃ [F₃] [G₃] G₃-ext)
                         (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₄ G₄ [[ ⊢A₄ , ⊢ΠF₄G₄ , D₄ ]] ⊢F₄ ⊢G₄ A₄≡A₄ [F₄] [G₄] G₄-ext)) (Π₌ F′₁ G′₁ D′₁ A≡B₁ [F≡F′]₁ [G≡G′]₁) =
  trans⇒* (univ⇒* (IdURed*Term′ (un-univ ⊢A₂) (un-univ ⊢ΠF₂G₂) (un-univ⇒* D₂) (un-univ ⊢A₄)))
                        (trans⇒* (univ⇒* (IdUΠRed*Term′ (un-univ ⊢F₂) (un-univ ⊢G₂) (un-univ ⊢A₄) (un-univ ⊢ΠF₄G₄) (un-univ⇒* D₄)))
                                 (univ (Id-U-ΠΠ!% (λ e → !≢% (PE.sym e)) (un-univ ⊢F₂) (un-univ ⊢G₂) (un-univ ⊢F₄) (un-univ ⊢G₄)) ⇨ id (univ (Emptyⱼ ⊢Γ))))

[IdExtShape]U {A₁} {A₂} {A₃} {A₄} {Γ}  ⊢Γ _ _
                   (Πᵥ (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢A₁ , ⊢ΠF₁G₁ , D₁ ]] ⊢F₁ ⊢G₁ A₁≡A₁ [F₁] [G₁] G₁-ext)
                   (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₂ G₂ [[ ⊢A₂ , ⊢ΠF₂G₂ , D₂ ]] ⊢F₂ ⊢G₂ A₂≡A₂ [F₂] [G₂] G₂-ext))
                   (Π₌ F₂′ G₂′ D₂′ A₁≡A₂′ [F₁≡F₂′] [G₁≡G₂′])
               _ _ (Πᵥ (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₃ G₃ [[ ⊢A₃ , ⊢ΠF₃G₃ , D₃ ]] ⊢F₃ ⊢G₃ A₃≡A₃ [F₃] [G₃] G₃-ext)
                   (Πᵣ ! .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₄ G₄ [[ ⊢A₄ , ⊢ΠF₄G₄ , D₄ ]] ⊢F₄ ⊢G₄ A₄≡A₄ [F₄] [G₄] G₄-ext))
                   (Π₌ F₄′ G₄′ D₄′ A₃≡A₄′ [F₃≡F₄′] [G₃≡G₄′]) =
    ∃₌ (Id (U ⁰) F₂ F₄) (E₂.IdGG₁ (step id) (var 0))
    E₂.D∃ ∃₁≡∃₂
    [IdFF₁≡IdFF₂]
    (λ {ρ} {Δ} {e} [ρ] ⊢Δ [e] → irrelevanceEq″ (PE.sym (E₁.wksubst-IdTel ρ e)) (PE.sym (E₂.wksubst-IdTel ρ e)) PE.refl PE.refl
      (E₁.[IdGG₁] [ρ] ⊢Δ [e]) (PE.subst (λ X → Δ ⊩⟨ ι ¹ ⟩ X ^ [ % , ι ¹ ]) (PE.sym (E₁.wksubst-IdTel ρ e)) (E₁.[IdGG₁] [ρ] ⊢Δ [e]))
      ([IdGG₁≡IdGG₂] [ρ] ⊢Δ [e]))
  where
    Π≡Π = whrDet* (D₂ , Whnf.Πₙ) (D₂′ , Whnf.Πₙ)
    F₂≡F₂′ = let x , _ , _ , _ , _ = Π-PE-injectivity Π≡Π in x
    G₂≡G₂′ = let _ , _ , _ , x , _ = Π-PE-injectivity Π≡Π in x
    Π≡Π′ = whrDet* (D₄ , Whnf.Πₙ) (D₄′ , Whnf.Πₙ)
    F₄≡F₄′ = let x , _ , _ , _ , _ = Π-PE-injectivity Π≡Π′ in x
    G₄≡G₄′ = let _ , _ , _ , x , _ = Π-PE-injectivity Π≡Π′ in x

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

    open IdTypeU-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
      ⊢A₃ ⊢ΠF₃G₃ D₃ ⊢F₃ ⊢G₃ A₃≡A₃ [F₃] [G₃] G₃-ext
      ⊢A₄ ⊢ΠF₄G₄ D₄ ⊢F₄ ⊢G₄ A₄≡A₄ [F₄] [G₄] G₄-ext
      A₁≡A₂ A₃≡A₄ [F₁≡F₂] [F₃≡F₄] [G₁≡G₂] [G₃≡G₄]
      (λ [ρ] ⊢Δ → [Id]U ⊢Δ ([F₁] [ρ] ⊢Δ) ([F₃] [ρ] ⊢Δ))
      (λ [ρ] ⊢Δ [x] [y] → [Id]U ⊢Δ ([G₁] [ρ] ⊢Δ [x]) ([G₃] [ρ] ⊢Δ [y]))
      (λ [ρ] ⊢Δ → [Id]U ⊢Δ ([F₂] [ρ] ⊢Δ) ([F₄] [ρ] ⊢Δ))
      (λ [ρ] ⊢Δ [x] [y] → [Id]U ⊢Δ ([G₂] [ρ] ⊢Δ [x]) ([G₄] [ρ] ⊢Δ [y]))
      (λ [ρ] ⊢Δ [x] [x′] [x≡x′] [y] [y′] [y≡y′] →
        [IdExt]U ⊢Δ ([G₁] [ρ] ⊢Δ [x]) ([G₁] [ρ] ⊢Δ [x′]) (G₁-ext [ρ] ⊢Δ [x] [x′] [x≡x′]) ([G₃] [ρ] ⊢Δ [y]) ([G₃] [ρ] ⊢Δ [y′]) (G₃-ext [ρ] ⊢Δ [y] [y′] [y≡y′]))
      (λ [ρ] ⊢Δ [x] [x′] [x≡x′] [y] [y′] [y≡y′] →
        [IdExt]U ⊢Δ ([G₂] [ρ] ⊢Δ [x]) ([G₂] [ρ] ⊢Δ [x′]) (G₂-ext [ρ] ⊢Δ [x] [x′] [x≡x′]) ([G₄] [ρ] ⊢Δ [y]) ([G₄] [ρ] ⊢Δ [y′]) (G₄-ext [ρ] ⊢Δ [y] [y′] [y≡y′]))
      (λ [ρ] ⊢Δ → [IdExt]U ⊢Δ ([F₁] [ρ] ⊢Δ) ([F₂] [ρ] ⊢Δ) ([F₁≡F₂] [ρ] ⊢Δ) ([F₃] [ρ] ⊢Δ) ([F₄] [ρ] ⊢Δ) ([F₃≡F₄] [ρ] ⊢Δ))
      (λ [ρ] ⊢Δ [x₁] [x₂] [G₁x₁≡G₂x₂] [x₃] [x₄] [G₃x₃≡G₄x₄] → [IdExt]U ⊢Δ ([G₁] [ρ] ⊢Δ [x₁]) ([G₂] [ρ] ⊢Δ [x₂]) [G₁x₁≡G₂x₂] ([G₃] [ρ] ⊢Δ [x₃]) ([G₄] [ρ] ⊢Δ [x₄]) [G₃x₃≡G₄x₄])

[IdExtShape]U {A₁} {A₂} {A₃} {A₄} {Γ}  ⊢Γ _ _
                   (Πᵥ (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₁ G₁ [[ ⊢A₁ , ⊢ΠF₁G₁ , D₁ ]] ⊢F₁ ⊢G₁ A₁≡A₁ [F₁] [G₁] G₁-ext)
                   (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₂ G₂ [[ ⊢A₂ , ⊢ΠF₂G₂ , D₂ ]] ⊢F₂ ⊢G₂ A₂≡A₂ [F₂] [G₂] G₂-ext))
                   (Π₌ F₂′ G₂′ D₂′ A₁≡A₂′ [F₁≡F₂′] [G₁≡G₂′])
               _ _ (Πᵥ (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₃ G₃ [[ ⊢A₃ , ⊢ΠF₃G₃ , D₃ ]] ⊢F₃ ⊢G₃ A₃≡A₃ [F₃] [G₃] G₃-ext)
                   (Πᵣ % .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F₄ G₄ [[ ⊢A₄ , ⊢ΠF₄G₄ , D₄ ]] ⊢F₄ ⊢G₄ A₄≡A₄ [F₄] [G₄] G₄-ext))
                   (Π₌ F₄′ G₄′ D₄′ A₃≡A₄′ [F₃≡F₄′] [G₃≡G₄′]) =
    ∃₌ (Id (SProp ⁰) F₂ F₄) (E₂.IdGG₁ (step id) (var 0))
    E₂.D∃ ∃₁≡∃₂
    [IdFF₁≡IdFF₂]
    (λ {ρ} {Δ} {e} [ρ] ⊢Δ [e] → irrelevanceEq″ (PE.sym (E₁.wksubst-IdTel ρ e)) (PE.sym (E₂.wksubst-IdTel ρ e)) PE.refl PE.refl
      (E₁.[IdGG₁] [ρ] ⊢Δ [e]) (PE.subst (λ X → Δ ⊩⟨ ι ¹ ⟩ X ^ [ % , ι ¹ ]) (PE.sym (E₁.wksubst-IdTel ρ e)) (E₁.[IdGG₁] [ρ] ⊢Δ [e]))
      ([IdGG₁≡IdGG₂] [ρ] ⊢Δ [e]))
  where
    Π≡Π = whrDet* (D₂ , Whnf.Πₙ) (D₂′ , Whnf.Πₙ)
    F₂≡F₂′ = let x , _ , _ , _ , _ = Π-PE-injectivity Π≡Π in x
    G₂≡G₂′ = let _ , _ , _ , x , _ = Π-PE-injectivity Π≡Π in x
    Π≡Π′ = whrDet* (D₄ , Whnf.Πₙ) (D₄′ , Whnf.Πₙ)
    F₄≡F₄′ = let x , _ , _ , _ , _ = Π-PE-injectivity Π≡Π′ in x
    G₄≡G₄′ = let _ , _ , _ , x , _ = Π-PE-injectivity Π≡Π′ in x

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

    open IdTypeU-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
      ⊢A₃ ⊢ΠF₃G₃ D₃ ⊢F₃ ⊢G₃ A₃≡A₃ [F₃] [G₃] G₃-ext
      ⊢A₄ ⊢ΠF₄G₄ D₄ ⊢F₄ ⊢G₄ A₄≡A₄ [F₄] [G₄] G₄-ext
      A₁≡A₂ A₃≡A₄ [F₁≡F₂] [F₃≡F₄] [G₁≡G₂] [G₃≡G₄]
      (λ [ρ] ⊢Δ → [Id]SProp ⊢Δ ([F₁] [ρ] ⊢Δ) ([F₃] [ρ] ⊢Δ))
      (λ [ρ] ⊢Δ [x] [y] → [Id]U ⊢Δ ([G₁] [ρ] ⊢Δ [x]) ([G₃] [ρ] ⊢Δ [y]))
      (λ [ρ] ⊢Δ → [Id]SProp ⊢Δ ([F₂] [ρ] ⊢Δ) ([F₄] [ρ] ⊢Δ))
      (λ [ρ] ⊢Δ [x] [y] → [Id]U ⊢Δ ([G₂] [ρ] ⊢Δ [x]) ([G₄] [ρ] ⊢Δ [y]))
      (λ [ρ] ⊢Δ [x] [x′] [x≡x′] [y] [y′] [y≡y′] →
        [IdExt]U ⊢Δ ([G₁] [ρ] ⊢Δ [x]) ([G₁] [ρ] ⊢Δ [x′]) (G₁-ext [ρ] ⊢Δ [x] [x′] [x≡x′]) ([G₃] [ρ] ⊢Δ [y]) ([G₃] [ρ] ⊢Δ [y′]) (G₃-ext [ρ] ⊢Δ [y] [y′] [y≡y′]))
      (λ [ρ] ⊢Δ [x] [x′] [x≡x′] [y] [y′] [y≡y′] →
        [IdExt]U ⊢Δ ([G₂] [ρ] ⊢Δ [x]) ([G₂] [ρ] ⊢Δ [x′]) (G₂-ext [ρ] ⊢Δ [x] [x′] [x≡x′]) ([G₄] [ρ] ⊢Δ [y]) ([G₄] [ρ] ⊢Δ [y′]) (G₄-ext [ρ] ⊢Δ [y] [y′] [y≡y′]))
      (λ [ρ] ⊢Δ → [IdExt]SProp ⊢Δ ([F₁] [ρ] ⊢Δ) ([F₂] [ρ] ⊢Δ) ([F₁≡F₂] [ρ] ⊢Δ) ([F₃] [ρ] ⊢Δ) ([F₄] [ρ] ⊢Δ) ([F₃≡F₄] [ρ] ⊢Δ))
      (λ [ρ] ⊢Δ [x₁] [x₂] [G₁x₁≡G₂x₂] [x₃] [x₄] [G₃x₃≡G₄x₄] → [IdExt]U ⊢Δ ([G₁] [ρ] ⊢Δ [x₁]) ([G₂] [ρ] ⊢Δ [x₂]) [G₁x₁≡G₂x₂] ([G₃] [ρ] ⊢Δ [x₃]) ([G₄] [ρ] ⊢Δ [x₄]) [G₃x₃≡G₄x₄])

[IdExt]U ⊢Γ [A] [A′] [A≡A′] [B] [B′] [B≡B′] = [IdExtShape]U ⊢Γ [A] [A′] (goodCases [A] [A′] [A≡A′]) [A≡A′] [B] [B′] (goodCases [B] [B′] [B≡B′]) [B≡B′]

Ugen' : ∀ {Γ rU l} → (⊢Γ : ⊢ Γ) →  ((next l) LogRel.⊩¹U logRelRec (next l) ^ Γ) (Univ rU l) (next l)
Ugen' {Γ} {rU} {⁰} ⊢Γ = Uᵣ rU ⁰ emb< PE.refl ((idRed:*: (Ugenⱼ ⊢Γ)))
Ugen' {Γ} {rU} {¹} ⊢Γ = Uᵣ rU ¹ ∞< PE.refl (idRed:*: (Uⱼ ⊢Γ))

[Id]UGen : ∀ {A t u Γ l}
         (⊢Γ : ⊢ Γ)
         ([A] : (l LogRel.⊩¹U logRelRec l ^ Γ) A (ι ¹))
         ([t] : Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , ι ¹ ] / Uᵣ [A])
         ([u] : Γ ⊩⟨ l ⟩ u ∷ A ^ [ ! , ι ¹ ] / Uᵣ [A])
       → Γ ⊩⟨ l ⟩ Id A t u ^ [ % , ι ¹ ]
[Id]UGen {A} {t} {u} {Γ} {ι .¹} ⊢Γ (Uᵣ ! ⁰ emb< PE.refl [[ ⊢A , ⊢B , D ]]) (Uₜ K d typeK K≡K [t]) (Uₜ M d₁ typeM M≡M [u]) =
  let
    [t0] : Γ ⊩⟨ ι ⁰ ⟩ t ^ [ ! , ι ⁰ ]
    [t0] = PE.subst (λ X → Γ ⊩⟨ ι ⁰ ⟩ X ^ [ ! , ι ⁰ ]) (wk-id t) ([t] Twk.id ⊢Γ)
    [u0] = PE.subst (λ X → Γ ⊩⟨ ι ⁰ ⟩ X ^ [ ! , ι ⁰ ]) (wk-id u) ([u] Twk.id ⊢Γ)
    ⊢tA = conv (un-univ (escape [t0])) (sym (subset* D))
    ⊢uA = conv (un-univ (escape [u0])) (sym (subset* D))
  in proj₁ (redSubst* (IdRed* ⊢tA ⊢uA D) ([Id]U ⊢Γ [t0] [u0]))

[Id]UGen {A} {t} {u} {Γ} {ι .¹} ⊢Γ (Uᵣ % ⁰ emb< PE.refl [[ ⊢A , ⊢B , D ]]) (Uₜ K d typeK K≡K [t]) (Uₜ M d₁ typeM M≡M [u]) =
  let
    [t0] : Γ ⊩⟨ ι ⁰ ⟩ t ^ [ % , ι ⁰ ]
    [t0] = PE.subst (λ X → Γ ⊩⟨ ι ⁰ ⟩ X ^ [ % , ι ⁰ ]) (wk-id t) ([t] Twk.id ⊢Γ)
    [u0] = PE.subst (λ X → Γ ⊩⟨ ι ⁰ ⟩ X ^ [ % , ι ⁰ ]) (wk-id u) ([u] Twk.id ⊢Γ)
    ⊢tA = conv (un-univ (escape [t0])) (sym (subset* D))
    ⊢uA = conv (un-univ (escape [u0])) (sym (subset* D))
  in proj₁ (redSubst* (IdRed* ⊢tA ⊢uA D) ([Id]SProp ⊢Γ [t0] [u0]))

[IdExt]UGen : ∀ {A B t v u w Γ l l'}
         (⊢Γ : ⊢ Γ)
         ([A] : (l LogRel.⊩¹U logRelRec l ^ Γ) A (ι ¹))
         ([B] : (l' LogRel.⊩¹U logRelRec l' ^ Γ) B (ι ¹))
         ([A≡B] : Γ ⊩⟨ l ⟩ A ≡ B ^ [ ! , ι ¹ ] / Uᵣ [A])
         ([t] : Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , ι ¹ ] / Uᵣ [A])
         ([v] : Γ ⊩⟨ l' ⟩ v ∷ B ^ [ ! , ι ¹ ] / Uᵣ [B])
         ([t≡v] : Γ ⊩⟨ l ⟩ t ≡ v ∷ A ^ [ ! , ι ¹ ] / Uᵣ [A])
         ([u] : Γ ⊩⟨ l ⟩ u ∷ A ^ [ ! , ι ¹ ] / Uᵣ [A])
         ([w] : Γ ⊩⟨ l' ⟩ w ∷ B ^ [ ! , ι ¹ ] / Uᵣ [B])
         ([u≡w] : Γ ⊩⟨ l ⟩ u ≡ w ∷ A ^ [ ! , ι ¹ ] / Uᵣ [A])
       → Γ ⊩⟨ l ⟩ Id A t u ≡ Id B v w ^ [ % , ι ¹ ] / [Id]UGen ⊢Γ [A] [t] [u]
[IdExt]UGen {A} {B} {t} {v} {u} {w} {Γ} {.(ι ¹)} {.(ι ¹)} ⊢Γ (Uᵣ ! ⁰ emb< PE.refl d) (Uᵣ r₁ ⁰ emb< PE.refl d₁) [A≡B] [t] [v] [t≡v] [u] [w] [u≡w] =
  let U≡U = whrDet* (red d₁ , Uₙ) ([A≡B] , Uₙ)
      r≡r , _ = Univ-PE-injectivity U≡U
      [UA] = Uᵣ ! ⁰ emb< PE.refl d
      [UB] = Uᵣ r₁ ⁰ emb< PE.refl d₁
      [U] = Ugen' ⊢Γ
      [U]' = Ugen' ⊢Γ
      [UA]' , [UAeq] = redSubst* (red d) (Uᵣ [U])
      [UB]' , [UBeq] = redSubst* (PE.subst (λ X → Γ ⊢ _ ⇒* Univ X _ ^ _) r≡r (red d₁)) (Uᵣ [U]')
      [t]′ = convTerm₁ {t = t} [UA]' (Uᵣ [U]) [UAeq] (irrelevanceTerm (Uᵣ [UA]) [UA]' [t])
      [t^] = univEq (Uᵣ [U]) [t]′
      [v]′ = convTerm₁ {t = v} [UB]' (Uᵣ [U]) [UBeq] (irrelevanceTerm (Uᵣ [UB]) [UB]' [v])
      [v^] = univEq (Uᵣ [U]) [v]′
      [t≡v]′ = convEqTerm₁ {t = t} {u = v} [UA]' (Uᵣ [U]) [UAeq] (irrelevanceEqTerm (Uᵣ [UA]) [UA]' [t≡v])
      [t≡v^] = univEqEq (Uᵣ [U]) [t^] [t≡v]′
      [u]′ = convTerm₁ {t = u} [UA]' (Uᵣ [U]) [UAeq] (irrelevanceTerm (Uᵣ [UA]) [UA]' [u])
      [u^] = univEq (Uᵣ [U]) [u]′
      [w]′ = convTerm₁ {t = w} [UB]' (Uᵣ [U]) [UBeq] (irrelevanceTerm (Uᵣ [UB]) [UB]'  [w])
      [w^] = univEq (Uᵣ [U]) [w]′
      [u≡w]′ = convEqTerm₁ {t = u} {u = w} [UA]' (Uᵣ [U]) [UAeq] (irrelevanceEqTerm (Uᵣ [UA]) [UA]' [u≡w])
      [u≡w^] = univEqEq (Uᵣ [U]) [u^] [u≡w]′
      X = irrelevanceEq {A = Id (U ⁰) t u} {B = Id (U ⁰) v w} ([Id]U ⊢Γ [t^] [u^]) ([Id]UGen ⊢Γ [U] [t]′ [u]′) ([IdExt]U ⊢Γ [t^] [v^] [t≡v^] [u^] [w^] [u≡w^])
      [IdA] , [IdA≡U] = redSubst* (IdRed* (escapeTerm (Uᵣ [UA]) [t]) (escapeTerm (Uᵣ [UA]) [u]) (red d)) ([Id]UGen ⊢Γ [U] [t]′ [u]′)
      [IdB] , [IdB≡U] = redSubst* (IdRed* (escapeTerm (Uᵣ [UB]) [v]) (escapeTerm (Uᵣ [UB]) [w]) (PE.subst (λ X → Γ ⊢ _ ⇒* Univ X _ ^ _) r≡r (red d₁))) ([Id]UGen ⊢Γ [U] [v]′ [w]′)
      [IdA≡U]′ = irrelevanceEq {A = Id A t u} {B = Id (U ⁰) t u} [IdA] ([Id]UGen ⊢Γ [UA] [t] [u]) [IdA≡U]
      [IdB≡U]′ = irrelevanceEq {A = Id B v w} {B = Id (U ⁰) v w} [IdB] ([Id]UGen ⊢Γ [UB] [v] [w]) [IdB≡U]
  in transEq {A = Id A t u} {B = Id (U _) t u} {C = Id B v w}  ([Id]UGen ⊢Γ [UA] [t] [u]) ([Id]UGen ⊢Γ [U] [t]′ [u]′) ([Id]UGen ⊢Γ [UB] [v] [w])
                  [IdA≡U]′
                  (transEq {A = Id (U _) t u} {B = Id (U _) v w} {C = Id B v w} ([Id]UGen ⊢Γ [U] [t]′ [u]′) ([Id]UGen ⊢Γ [U] [v]′ [w]′) ([Id]UGen ⊢Γ [UB] [v] [w])
                                   X (symEq {A = Id B v w} {B = Id (U _) v w} ([Id]UGen ⊢Γ [UB] [v] [w]) ([Id]UGen ⊢Γ [U] [v]′ [w]′) [IdB≡U]′))

[IdExt]UGen {A} {B} {t} {v} {u} {w} {Γ} {.(ι ¹)} {.(ι ¹)} ⊢Γ (Uᵣ % ⁰ emb< PE.refl d) (Uᵣ r₁ ⁰ emb< PE.refl d₁) [A≡B] [t] [v] [t≡v] [u] [w] [u≡w] =
  let U≡U = whrDet* (red d₁ , Uₙ) ([A≡B] , Uₙ)
      r≡r , _ = Univ-PE-injectivity U≡U
      [UA] = Uᵣ % ⁰ emb< PE.refl d
      [UB] = Uᵣ r₁ ⁰ emb< PE.refl d₁
      [U] = Ugen' ⊢Γ
      [U]' = Ugen' ⊢Γ
      [UA]' , [UAeq] = redSubst* (red d) (Uᵣ [U])
      [UB]' , [UBeq] = redSubst* (PE.subst (λ X → Γ ⊢ _ ⇒* Univ X _ ^ _) r≡r (red d₁)) (Uᵣ [U]')
      [t]′ = convTerm₁ {t = t} [UA]' (Uᵣ [U]) [UAeq] (irrelevanceTerm (Uᵣ [UA]) [UA]' [t])
      [t^] = univEq (Uᵣ [U]) [t]′
      [v]′ = convTerm₁ {t = v} [UB]' (Uᵣ [U]) [UBeq] (irrelevanceTerm (Uᵣ [UB]) [UB]' [v])
      [v^] = univEq (Uᵣ [U]) [v]′
      [t≡v]′ = convEqTerm₁ {t = t} {u = v} [UA]' (Uᵣ [U]) [UAeq] (irrelevanceEqTerm (Uᵣ [UA]) [UA]' [t≡v])
      [t≡v^] = univEqEq (Uᵣ [U]) [t^] [t≡v]′
      [u]′ = convTerm₁ {t = u} [UA]' (Uᵣ [U]) [UAeq] (irrelevanceTerm (Uᵣ [UA]) [UA]' [u])
      [u^] = univEq (Uᵣ [U]) [u]′
      [w]′ = convTerm₁ {t = w} [UB]' (Uᵣ [U]) [UBeq] (irrelevanceTerm (Uᵣ [UB]) [UB]'  [w])
      [w^] = univEq (Uᵣ [U]) [w]′
      [u≡w]′ = convEqTerm₁ {t = u} {u = w} [UA]' (Uᵣ [U]) [UAeq] (irrelevanceEqTerm (Uᵣ [UA]) [UA]' [u≡w])
      [u≡w^] = univEqEq (Uᵣ [U]) [u^] [u≡w]′
      X = irrelevanceEq {A = Id (SProp ⁰) t u} {B = Id (SProp ⁰) v w} ([Id]SProp ⊢Γ [t^] [u^]) ([Id]UGen ⊢Γ [U] [t]′ [u]′) ([IdExt]SProp ⊢Γ [t^] [v^] [t≡v^] [u^] [w^] [u≡w^])
      [IdA] , [IdA≡U] = redSubst* (IdRed* (escapeTerm (Uᵣ [UA]) [t]) (escapeTerm (Uᵣ [UA]) [u]) (red d)) ([Id]UGen ⊢Γ [U] [t]′ [u]′)
      [IdB] , [IdB≡U] = redSubst* (IdRed* (escapeTerm (Uᵣ [UB]) [v]) (escapeTerm (Uᵣ [UB]) [w]) (PE.subst (λ X → Γ ⊢ _ ⇒* Univ X _ ^ _) r≡r (red d₁))) ([Id]UGen ⊢Γ [U] [v]′ [w]′)
      [IdA≡U]′ = irrelevanceEq {A = Id A t u} {B = Id (SProp ⁰) t u} [IdA] ([Id]UGen ⊢Γ [UA] [t] [u]) [IdA≡U]
      [IdB≡U]′ = irrelevanceEq {A = Id B v w} {B = Id (SProp ⁰) v w} [IdB] ([Id]UGen ⊢Γ [UB] [v] [w]) [IdB≡U]
  in transEq {A = Id A t u} {B = Id (SProp _) t u} {C = Id B v w}  ([Id]UGen ⊢Γ [UA] [t] [u]) ([Id]UGen ⊢Γ [U] [t]′ [u]′) ([Id]UGen ⊢Γ [UB] [v] [w])
                  [IdA≡U]′
                  (transEq {A = Id (SProp _) t u} {B = Id (SProp _) v w} {C = Id B v w} ([Id]UGen ⊢Γ [U] [t]′ [u]′) ([Id]UGen ⊢Γ [U] [v]′ [w]′) ([Id]UGen ⊢Γ [UB] [v] [w])
                                   X (symEq {A = Id B v w} {B = Id (SProp _) v w} ([Id]UGen ⊢Γ [UB] [v] [w]) ([Id]UGen ⊢Γ [U] [v]′ [w]′) [IdB≡U]′))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

module Cardinality.Finite.Structure where

open import Prelude
open import Data.Fin
open import Data.Nat
open import Data.Nat.Properties

private
  variable
    n m : ℕ

liftˡ : ∀ n m → Fin m → Fin (n + m)
liftˡ zero    m x = x
liftˡ (suc n) m x = fs (liftˡ n m x)

liftʳ : ∀ n m → Fin n → Fin (n + m)
liftʳ (suc n) m f0     = f0
liftʳ (suc n) m (fs x) = fs (liftʳ n m x)

mapl : (A → B) → A ⊎ C → B ⊎ C
mapl f (inl x) = inl (f x)
mapl f (inr x) = inr x

fin-sum-to : ∀ n m → Fin n ⊎ Fin m → Fin (n + m)
fin-sum-to n m = either (liftʳ n m) (liftˡ n m)

fin-sum-from : ∀ n m → Fin (n + m) →  Fin n ⊎ Fin m
fin-sum-from zero    m x      = inr x
fin-sum-from (suc n) m f0     = inl f0
fin-sum-from (suc n) m (fs x) = mapl fs (fin-sum-from n m x)

mapl-distrib : ∀ {a b c d} {A : Type a} {B : Type b} {C : Type c} {D : Type d} (xs : A ⊎ B) (h : A → C) (f : C → D) (g : B → D) → either′ f g (mapl h xs) ≡ either′ (f ∘′ h) g xs
mapl-distrib (inl x) h f g = refl
mapl-distrib (inr x) h f g = refl

either-distrib : ∀ {d} {D : Type d} (f : A → C) (g : B → C) (h : C → D) (xs : A ⊎ B) → either′ (h ∘ f) (h ∘ g) xs ≡ h (either′ f g xs)
either-distrib f g h (inl x) = refl
either-distrib f g h (inr x) = refl

open import Path.Reasoning

fin-sum-to-from : ∀ n m x → fin-sum-to n m (fin-sum-from n m x) ≡ x
fin-sum-to-from zero    m x      = refl
fin-sum-to-from (suc n) m f0     = refl
fin-sum-to-from (suc n) m (fs x) =
  fin-sum-to (suc n) m (mapl fs (fin-sum-from n m x)) ≡⟨ mapl-distrib (fin-sum-from n m x) fs (liftʳ (suc n) m) (liftˡ (suc n) m) ⟩
  either (liftʳ (suc n) m ∘ fs) (liftˡ (suc n) m) (fin-sum-from n m x) ≡⟨⟩
  either (fs ∘ liftʳ n m) (fs ∘ liftˡ n m) (fin-sum-from n m x) ≡⟨ either-distrib (liftʳ n m) (liftˡ n m) fs (fin-sum-from n m x) ⟩
  fs (either (liftʳ n m) (liftˡ n m) (fin-sum-from n m x)) ≡⟨ cong fs (fin-sum-to-from n m x) ⟩
  fs x ∎

-- fin-sum-from-to : ∀ n m x → fin-sum-from n m (fin-sum-to n m x) ≡ x
-- fin-sum-from-to n m (inl x) = {!!}
-- fin-sum-from-to n m (inr x) = {!!}

-- fin-sum : ∀ n m → Fin n ⊎ Fin m ⇔ Fin (n + m)
-- fin-sum n m .fun = fin-sum-to n m
-- fin-sum n m .inv = fin-sum-from n m
-- fin-sum n m .rightInv = fin-sum-to-from n m
-- fin-sum n m .leftInv = fin-sum-from-to n m

ext: agda

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Data.Signed where

open import Data.Bit using
  (Bit
  ; b0
  ; b1
  ; Bits-num
  ; Bits-neg
  ; Overflowing
  ; _overflow:_
  ; result
  ; carry
  ; WithCarry
  ; _with-carry:_
  ; toBool
  ; tryToFinₙ
  ; !ₙ
  ; _⊕_
  ; _↔_
  ) renaming
  ( _+_ to bit+
  ; _-_ to bit-
  ; ! to bit!
  ; _&_ to bit&
  ; _~|_ to bit|
  ; _^_ to bit^
  ; _>>_ to bit>>
  ; _<<_ to bit<<
  )
open import Data.Unit using (⊤)
open import Data.Nat using (ℕ; suc; zero) renaming (_≤_ to ℕ≤)
open import Data.Vec using (Vec; _∷_; []; head; tail; replicate)
open import Data.Nat.Literal using (Number)
open import Data.Int.Literal using (Negative)
open import Data.Maybe using (just; nothing)
open import Data.Empty using (⊥)

infixl 8 _-_ _+_
infixl 7 _<<_ _>>_
infixl 6 _&_
infixl 5 _^_
infixl 4 _~|_

record Signed (n : ℕ) : Set where
  constructor mk-int
  field
    bits : Vec Bit n

open Signed public

instance
  Signed-num : {m : ℕ} → Number (Signed m)
  Signed-num {zero} .Number.Constraint = Number.Constraint (Bits-num {zero})
  Signed-num {suc m} .Number.Constraint = Number.Constraint (Bits-num {m})
  Signed-num {zero} .Number.fromNat zero ⦃ p ⦄ = mk-int [] where
  Signed-num {zero} .Number.fromNat (suc _) ⦃ ℕ≤.s≤s () ⦄
  Signed-num {suc m} .Number.fromNat n ⦃ p ⦄ = mk-int (mk-bits p) where
    mk-bits : Number.Constraint (Bits-num {m}) n → Vec Bit (suc m)
    mk-bits p = b0 ∷ Number.fromNat Bits-num n ⦃ p ⦄

instance
  Signed-neg : {m : ℕ} → Negative (Signed (suc m))
  Signed-neg {m} .Negative.Constraint = Negative.Constraint (Bits-neg {m})
  Signed-neg {m} .Negative.fromNeg n ⦃ p ⦄ = mk-int bitVec where
    bitVec : Vec Bit (suc m)
    bitVec = Negative.fromNeg (Bits-neg {m}) n ⦃ p ⦄

_+_ : {n : ℕ} → Signed n → Signed n → Overflowing (Signed n)
p + q = mk-int (result sum) overflow: toBool overflow where
  sum = bit+ (bits p) (bits q)
  last-carry : {n : ℕ} → Vec Bit n → Bit
  last-carry [] = b0
  last-carry (b ∷ _) = b
  overflow = head (carry sum) ⊕ last-carry (tail (carry sum))

_-_ : {n : ℕ} → Signed n → Signed n → Overflowing (Signed n)
p - q = mk-int (result sub) overflow: toBool overflow where
  sub = bit- (bits p) (bits q)
  last-carry : {n : ℕ} → Vec Bit n → Bit
  last-carry [] = b0
  last-carry (b ∷ _) = b
  overflow = head (carry sub) ↔ last-carry (tail (carry sub))

rotr : {n : ℕ} → Signed n → Signed n → WithCarry (Signed n) (Signed n)
rotr {n} (mk-int ps) (mk-int qs) = new-result with-carry: new-carry where
  shifted : WithCarry (Vec Bit n) (Vec Bit n)
  shifted with tryToFinₙ qs
  ...        | just i  = bit>> ps i
  ...        | nothing = replicate b0 with-carry: ps
  new-result : Signed n
  new-result = mk-int (result shifted)
  new-carry : Signed n
  new-carry = mk-int (carry shifted)

rotl : {n : ℕ} → Signed n → Signed n → WithCarry (Signed n) (Signed n)
rotl {n} (mk-int ps) (mk-int qs) = new-result with-carry: new-carry where
  shifted : WithCarry (Vec Bit n) (Vec Bit n)
  shifted with tryToFinₙ qs
  ...        | just i  = bit<< ps i
  ...        | nothing = replicate b0 with-carry: ps
  new-result : Signed n
  new-result = mk-int (result shifted)
  new-carry : Signed n
  new-carry = mk-int (carry shifted)

_>>_ : {n : ℕ} → Signed n → Signed n → Signed n
ps >> qs = result (rotr ps qs)

_<<_ : {n : ℕ} → Signed n → Signed n → Signed n
ps << qs = result (rotl ps qs)

arotr : {n : ℕ} → Signed n → Signed n → WithCarry (Signed n) (Signed n)
arotr {n} (mk-int []) _ = mk-int [] with-carry: mk-int []
arotr {suc n} (mk-int (p ∷ ps)) (mk-int qs) = new-result with-carry: new-carry
  where
    shifted : WithCarry (Vec Bit n) (Vec Bit n)
    shifted with tryToFinₙ qs
    ...        | just i  = bit>> ps i
    ...        | nothing = replicate b0 with-carry: ps
    new-result : Signed (suc n)
    new-result = mk-int (p ∷ result shifted)
    new-carry : Signed (suc n)
    new-carry = mk-int (b0 ∷ carry shifted)

arotl : {n : ℕ} → Signed n → Signed n → WithCarry (Signed n) (Signed n)
arotl {n} (mk-int []) _ = mk-int [] with-carry: mk-int []
arotl {suc n} (mk-int (p ∷ ps)) (mk-int qs) = new-result with-carry: new-carry
  where
    shifted : WithCarry (Vec Bit n) (Vec Bit n)
    shifted with tryToFinₙ qs
    ...        | just i  = bit<< ps i
    ...        | nothing = replicate b0 with-carry: ps
    new-result : Signed (suc n)
    new-result = mk-int (p ∷ result shifted)
    new-carry : Signed (suc n)
    new-carry = mk-int (b0 ∷ carry shifted)

_a>>_ : {n : ℕ} → Signed n → Signed n → Signed n
ps a>> qs = result (rotr ps qs)

_a<<_ : {n : ℕ} → Signed n → Signed n → Signed n
ps a<< qs = result (rotl ps qs)

! : {n : ℕ} → Signed n → Signed n
! (mk-int ps) = mk-int (!ₙ ps)

_&_ : {n : ℕ} → Signed n → Signed n → Signed n
(mk-int ps) & (mk-int qs) = mk-int (bit& ps qs)

_~|_ : {n : ℕ} → Signed n → Signed n → Signed n
(mk-int ps) ~| (mk-int qs) = mk-int (bit| ps qs)

_^_ : {n : ℕ} → Signed n → Signed n → Signed n
(mk-int ps) ^ (mk-int qs) = mk-int (bit^ ps qs)

max_stars_repo_name: brunoczim/Celeste

max_issues_repo_name: brunoczim/Celeste

max_forks_repo_name: brunoczim/Celeste


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Functions
open import Setoids.Setoids
open import Setoids.Subset
open import Graphs.Definition
open import Sets.FinSet.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Sets.EquivalenceRelations
open import Graphs.CompleteGraph
open import Graphs.Colouring

module Graphs.RamseyTriangle where

hasMonochromaticTriangle : {a : _} {n : ℕ} (G : Graph a (reflSetoid (FinSet n))) → Set (lsuc lzero)
hasMonochromaticTriangle {n = n} G = Sg (FinSet n → Set) λ pred → (subset (reflSetoid (FinSet n)) pred) && {!!}

ramseyForTriangle : (k : ℕ) → Sg ℕ (λ N → (n : ℕ) → (N <N n) → (c : Colouring k (Kn n)) → {!!})
ramseyForTriangle k = {!!}


text:
{-# OPTIONS --sized-types #-}

module SizedTypesRigidVarClash where

postulate
  Size : Set
  _^   : Size -> Size
  ∞    : Size

{-# BUILTIN SIZE Size  #-}
{-# BUILTIN SIZESUC _^ #-}
{-# BUILTIN SIZEINF ∞  #-}

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {size ^}
  suc  : {size : Size} -> Nat {size} -> Nat {size ^}

inc : {i j : Size} -> Nat {i} -> Nat {j ^}
inc x = suc x

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
-- Andreas, 2017-01-18, issue #2413
-- As-patterns of variable patterns

data Bool : Set where
  true false : Bool

test : Bool → Bool
test x@y = {!x!}  -- split on x

test1 : Bool → Bool
test1 x@_ = {!x!} -- split on x

test2 : Bool → Bool
test2 x@y = {!y!} -- split on y

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module reverse_string where

open import Data.String
open import Data.List

reverse_string : String → String
reverse_string s = fromList (reverse (toList s))

max_issues_repo_name: seanwallawalla-forks/RosettaCodeData

max_forks_repo_name: seanwallawalla-forks/RosettaCodeData


text:
{-# OPTIONS --safe --without-K #-}
open import Algebra.Bundles using (Monoid)

module Categories.Category.Construction.MonoidAsCategory o {c ℓ} (M : Monoid c ℓ) where

open import Data.Unit.Polymorphic
open import Level

open import Categories.Category.Core

open Monoid M

-- A monoid is a category with one object
MonoidAsCategory : Category o c ℓ
MonoidAsCategory = record
  { Obj = ⊤
  ; assoc = assoc _ _ _
  ; sym-assoc = sym (assoc _ _ _)
  ; identityˡ = identityˡ _
  ; identityʳ = identityʳ _
  ; identity² = identityˡ _
  ; equiv = isEquivalence
  ; ∘-resp-≈ = ∙-cong
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------------
-- Non-terminating GCD
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.GCD.GCD-NT where

open import Data.Nat
open import Relation.Nullary

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

{-# TERMINATING #-}
gcd : ℕ → ℕ → ℕ
gcd 0       0       = 0
gcd (suc m) 0       = suc m
gcd 0       (suc n) = suc n
gcd (suc m) (suc n) with suc m ≤? suc n
gcd (suc m) (suc n) | yes p = gcd (suc m) (suc n ∸ suc m)
gcd (suc m) (suc n) | no ¬p = gcd (suc m ∸ suc n) (suc n)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Structure.Signature where

open import Data.Tuple.Raise
open import Data.Tuple.Raiseᵣ.Functions
import      Lvl
open import Numeral.Natural
open import Structure.Function
open import Structure.Setoid
open import Structure.Relator
open import Type

private variable ℓ ℓᵢ ℓᵢ₁ ℓᵢ₂ ℓᵢ₃ ℓd ℓd₁ ℓd₂ ℓᵣ ℓᵣ₁ ℓᵣ₂ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable n : ℕ

-- A signature consists of a countable family of sets of function and relation symbols.
-- `functions(n)` and `relations(n)` should be interpreted as the indices for functions/relations of arity `n`.
record Signature : Type{Lvl.𝐒(ℓᵢ₁ Lvl.⊔ ℓᵢ₂)} where
  field
    functions : ℕ → Type{ℓᵢ₁}
    relations : ℕ → Type{ℓᵢ₂}

private variable s : Signature{ℓᵢ₁}{ℓᵢ₂}

import      Data.Tuple.Equiv as Tuple

-- A structure with a signature `s` consists of a domain and interpretations of the function/relation symbols in `s`.
record Structure (s : Signature{ℓᵢ₁}{ℓᵢ₂}) : Type{Lvl.𝐒(ℓₑ Lvl.⊔ ℓd Lvl.⊔ ℓᵣ) Lvl.⊔ ℓᵢ₁ Lvl.⊔ ℓᵢ₂} where
  open Signature(s)
  field
    domain : Type{ℓd}
    ⦃ equiv ⦄ : ∀{n} → Equiv{ℓₑ}(domain ^ n)
    ⦃ ext ⦄ : ∀{n} → Tuple.Extensionality(equiv{𝐒(𝐒 n)})
    function : functions(n) → ((domain ^ n) → domain)
    ⦃ function-func ⦄ : ∀{fi} → Function(function{n} fi)
    relation : relations(n) → ((domain ^ n) → Type{ℓᵣ})
    ⦃ relation-func ⦄ : ∀{ri} → UnaryRelator(relation{n} ri)

open Structure public using() renaming (domain to dom ; function to fn ; relation to rel)

open import Logic.Predicate

module _ {s : Signature{ℓᵢ₁}{ℓᵢ₂}} where
  private variable A B C S : Structure{ℓd = ℓd}{ℓᵣ = ℓᵣ}(s)
  private variable fi : Signature.functions s n
  private variable ri : Signature.relations s n
  private variable xs : dom(S) ^ n

  record Homomorphism
    (A : Structure{ℓₑ = ℓₑ₁}{ℓd = ℓd₁}{ℓᵣ = ℓᵣ₁}(s))
    (B : Structure{ℓₑ = ℓₑ₂}{ℓd = ℓd₂}{ℓᵣ = ℓᵣ₂}(s))
    (f : dom(A) → dom(B))
    : Type{ℓₑ₁ Lvl.⊔ ℓₑ₂ Lvl.⊔ ℓd₁ Lvl.⊔ ℓd₂ Lvl.⊔ ℓᵣ₁ Lvl.⊔ ℓᵣ₂ Lvl.⊔ Lvl.ofType(Type.of s)}
    where

    field
      ⦃ function ⦄ : Function(f)
      preserve-functions : ∀{xs : dom(A) ^ n} → (f(fn(A) fi xs) ≡ fn(B) fi (map f xs))
      preserve-relations : ∀{xs : dom(A) ^ n} → (rel(A) ri xs) → (rel(B) ri (map f xs))

  _→ₛₜᵣᵤ_ : Structure{ℓₑ = ℓₑ₁}{ℓd = ℓd₁}{ℓᵣ = ℓᵣ₁}(s) → Structure{ℓₑ = ℓₑ₂}{ℓd = ℓd₂}{ℓᵣ = ℓᵣ₂}(s) → Type
  A →ₛₜᵣᵤ B = ∃(Homomorphism A B)

  open import Data
  open import Data.Tuple as Tuple using (_,_)
  open import Data.Tuple.Raiseᵣ.Proofs
  open import Functional
  open import Function.Proofs
  open import Lang.Instance
  open import Structure.Operator
  open import Structure.Relator.Properties
  open import Syntax.Transitivity

  idₛₜᵣᵤ : A →ₛₜᵣᵤ A
  ∃.witness idₛₜᵣᵤ = id
  Homomorphism.preserve-functions (∃.proof (idₛₜᵣᵤ {A = A})) {n} {fi} {xs} = congruence₁(fn A fi) (symmetry(Equiv._≡_ (Structure.equiv A)) ⦃ Equiv.symmetry infer ⦄ map-id)
  Homomorphism.preserve-relations (∃.proof (idₛₜᵣᵤ {A = A})) {n} {ri} {xs} = substitute₁ₗ(rel A ri) map-id

  _∘ₛₜᵣᵤ_ : let _ = A , B , C in (B →ₛₜᵣᵤ C) → (A →ₛₜᵣᵤ B) → (A →ₛₜᵣᵤ C)
  ∃.witness (([∃]-intro f) ∘ₛₜᵣᵤ ([∃]-intro g)) = f ∘ g
  Homomorphism.function (∃.proof ([∃]-intro f ∘ₛₜᵣᵤ [∃]-intro g)) = [∘]-function {f = f}{g = g}
  Homomorphism.preserve-functions (∃.proof (_∘ₛₜᵣᵤ_ {A = A} {B = B} {C = C} ([∃]-intro f ⦃ hom-f ⦄) ([∃]-intro g ⦃ hom-g ⦄))) {fi = fi} = transitivity(_≡_) ⦃ Equiv.transitivity infer ⦄ (transitivity(_≡_) ⦃ Equiv.transitivity infer ⦄ (congruence₁(f) (Homomorphism.preserve-functions hom-g)) (Homomorphism.preserve-functions hom-f)) (congruence₁(fn C fi) (symmetry(Equiv._≡_ (Structure.equiv C)) ⦃ Equiv.symmetry infer ⦄ (map-[∘] {f = f}{g = g})))
  Homomorphism.preserve-relations (∃.proof (_∘ₛₜᵣᵤ_ {A = A} {B = B} {C = C} ([∃]-intro f ⦃ hom-f ⦄) ([∃]-intro g ⦃ hom-g ⦄))) {ri = ri} = substitute₁ₗ (rel C ri) map-[∘] ∘ Homomorphism.preserve-relations hom-f ∘ Homomorphism.preserve-relations hom-g

  open import Function.Equals
  open import Function.Equals.Proofs
  open import Logic.Predicate.Equiv
  open import Structure.Category
  open import Structure.Categorical.Properties

  Structure-Homomorphism-category : Category(_→ₛₜᵣᵤ_ {ℓₑ}{ℓd}{ℓᵣ})
  Category._∘_ Structure-Homomorphism-category = _∘ₛₜᵣᵤ_
  Category.id  Structure-Homomorphism-category = idₛₜᵣᵤ
  BinaryOperator.congruence (Category.binaryOperator Structure-Homomorphism-category) = [⊜][∘]-binaryOperator-raw
  _⊜_.proof (Morphism.Associativity.proof (Category.associativity Structure-Homomorphism-category) {_} {_} {_} {_} {[∃]-intro f} {[∃]-intro g} {[∃]-intro h}) {x} = reflexivity(_≡_) ⦃ Equiv.reflexivity infer ⦄ {f(g(h(x)))}
  _⊜_.proof (Morphism.Identityₗ.proof (Tuple.left (Category.identity Structure-Homomorphism-category)) {f = [∃]-intro f}) {x} = reflexivity(_≡_) ⦃ Equiv.reflexivity infer ⦄ {f(x)}
  _⊜_.proof (Morphism.Identityᵣ.proof (Tuple.right (Category.identity Structure-Homomorphism-category)) {f = [∃]-intro f}) {x} = reflexivity(_≡_) ⦃ Equiv.reflexivity infer ⦄ {f(x)}

module _ (s : Signature{ℓᵢ₁}{ℓᵢ₂}) where
  data Term : Type{ℓᵢ₁} where
    var  : ℕ → Term
    func : (Signature.functions s n) → (Term ^ n) → Term

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:
module Issue292-19 where

postulate
  I     : Set
  i₁ i₂ : I
  J     : Set
  j     : I → J

data D : I → Set where
  d₁ : D i₁
  d₂ : D i₂

data P : ∀ i → D i → Set where
  p₁ : P i₁ d₁
  p₂ : P i₂ d₂

data P′ : ∀ i → D i → Set where
  p₁ : P′ i₁ d₁

data E : J → Set where
  e₁ : E (j i₁)
  e₂ : E (j i₂)

data Q : ∀ i → E i → Set where
  q₁ : Q (j i₁) e₁
  q₂ : Q (j i₂) e₂

Ok : Q (j i₁) e₁ → Set₁
Ok q₁ = Set

AlsoOk : P i₁ d₁ → Set₁
AlsoOk p₁ = Set

Foo : ∀ {i} (d : D i) → P′ i d → Set₁
Foo d₁ _  = Set
Foo d₂ ()


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Data.List.Any.Membership instantiated with propositional equality,
-- along with some additional definitions.
------------------------------------------------------------------------

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

module Data.List.Membership.Propositional {a} {A : Set a} where

open import Data.List.Relation.Unary.Any using (Any)
open import Relation.Binary.PropositionalEquality using (setoid; subst)

import Data.List.Membership.Setoid as SetoidMembership

------------------------------------------------------------------------
-- Re-export contents of setoid membership

open SetoidMembership (setoid A) public hiding (lose)

------------------------------------------------------------------------
-- Other operations

lose : ∀ {p} {P : A → Set p} {x xs} → x ∈ xs → P x → Any P xs
lose = SetoidMembership.lose (setoid A) (subst _)


text:
module TelescopingLet2 where

f : (let ★ = Set) (A : ★) → A → Set₁
f A x = ★
-- should fail, since ★ is not in scope in the definition


text:
module Ag05 where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Bool

{-
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x
-}
data Refine : (A : Set) → (A → Set) → Set where
  MkRefine : ∀ {A : Set} {f : A → Set} → (a : A) → (f a) → Refine A f

data _∧_ : Set → Set → Set where
  and : ∀ (A B : Set) → A ∧ B

-- hl-suc : ∀ {a : Nat} → Refine Nat (λ )

silly : Set
silly = Refine Nat (_≡_ 0)

sillySon : silly
sillySon = MkRefine zero refl

data _≤_ : Nat → Nat → Set where
  z≤s : ∀ {b   : Nat} → 0 ≤ b
  s≤s : ∀ {m n : Nat} → m ≤ n → suc m ≤ suc n

data le-Total (x y : Nat) : Set where
  le-left  : x ≤ y → le-Total x y
  le-right : y ≤ x → le-Total x y

le : Nat → Nat → Bool
le zero    zero    = true
le zero    (suc n) = true
le (suc m) zero    = false
le (suc m) (suc n) = le m n

le-wtf : ∀ (x y : Nat) → le-Total x y
le-wtf zero    zero    = le-left z≤s
le-wtf zero    (suc y) = le-left z≤s
le-wtf (suc x) zero    = le-right z≤s
le-wtf (suc x) (suc y) with le-wtf x y
...                    | le-left  P = le-left  (s≤s P)
...                    | le-right Q = le-right (s≤s Q)
{- with le x y -- x ≤ y
...        | true  = {!!}
...        | false = {!!}
-}
_⟨_⟩ : (A : Set) → (A → Set) → Set
_⟨_⟩ = Refine

and-refine : ∀ {A : Set} (f g : A → Set)
           → (a : A) → f a → g a
           → Refine A (λ x → (f x) ∧ (g x))
and-refine f g x Pa Pb = MkRefine x (and (f x) (g x))

hSuc : ∀ {m : Nat} → ( Nat ⟨ (λ x → x ≤ m     ) ⟩ )
                   → ( Nat ⟨ (λ x → x ≤ suc m ) ⟩ )
hSuc (MkRefine a P) = MkRefine (suc a) (s≤s P)

postulate
  ≤-trans : ∀ {x y z : Nat} → x ≤ y → y ≤ z → x ≤ z

min : ∀ {m n : Nat} → ( Nat ⟨ (λ x → x ≤ m)             ⟩ )
                    → ( Nat ⟨ (λ x → x ≤ n)             ⟩ )
                    → ( Nat ⟨ (λ x → (x ≤ m) ∧ (x ≤ n)) ⟩ )
min (MkRefine a Pa) (MkRefine b Pb) with le-wtf a b
...                    {- a ≤ b -}  | le-left  P = {!and-refine ? ? Pa ? !}
...                    {- b ≤ a -}  | le-right Q = {!and-refine _ _ ? Pb !}
{-
with le-Total a b
...                                 | le-left  a = {!!}
...                                 | le-right b = ? -}
{-
min {m} {n} (MkRefine a P₀) (MkRefine b P₁) with (le a b)
...                                 | true  = {!!}
...                                 | false = {!!}
-}
{-
min {m} {n} (MkRefine zero x)    (MkRefine b y)    = MkRefine 0 (and (zero ≤ m) (zero ≤ n))
min {m} {n} (MkRefine (suc a) x) (MkRefine zero y) = MkRefine 0 (and (zero ≤ m) (zero ≤ n))
min {suc m} {suc n} (MkRefine (suc a) x) (MkRefine (suc b) y) = {!hSuc (min (MkRefine a ?) (MkRefine b ?))!}
-}

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


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

-- the usual notion of mate is defined by two isomorphisms between hom set(oid)s are natural,
-- but due to explicit universe level, a different definition is used.
module Categories.Adjoint.Mate where

open import Level
open import Data.Product using (Σ; _,_)
open import Function.Equality using (Π; _⟶_; _⇨_) renaming (_∘_ to _∙_)
open import Relation.Binary using (Setoid; IsEquivalence)

open import Categories.Category
open import Categories.Category.Instance.Setoids
open import Categories.Functor
open import Categories.Functor.Hom
open import Categories.NaturalTransformation renaming (id to idN)
open import Categories.NaturalTransformation.Equivalence using (_≃_)
open import Categories.Adjoint
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D : Category o ℓ e
    L L′ R R′ : Functor C D

-- this notion of mate can be seen in MacLane in which this notion is shown equivalent to the
-- definition via naturally isomorphic hom setoids.
record Mate {L : Functor C D}
            (L⊣R : L ⊣ R) (L′⊣R′ : L′ ⊣ R′)
            (α : NaturalTransformation L L′)
            (β : NaturalTransformation R′ R) : Set (levelOfTerm L⊣R ⊔ levelOfTerm L′⊣R′) where
  private
    module L⊣R   = Adjoint L⊣R
    module L′⊣R′ = Adjoint L′⊣R′
    module C = Category C
    module D = Category D

  field
    commute₁ : (R ∘ˡ α) ∘ᵥ L⊣R.unit ≃ (β ∘ʳ L′) ∘ᵥ L′⊣R′.unit
    commute₂ : L⊣R.counit ∘ᵥ L ∘ˡ β ≃ L′⊣R′.counit ∘ᵥ (α ∘ʳ R′)

  -- there are two equivalent commutative diagram
  open NaturalTransformation renaming (commute to η-commute)
  open Functor
  module _ where
    open D
    open HomReasoning
    open MR D

    commute₃ : ∀ {X} → L⊣R.counit.η (F₀ L′ X) ∘ F₁ L (η β (F₀ L′ X)) ∘ F₁ L (L′⊣R′.unit.η X) ≈ η α X
    commute₃ {X} = begin
      L⊣R.counit.η (F₀ L′ X) ∘ F₁ L (η β (F₀ L′ X)) ∘ F₁ L (L′⊣R′.unit.η X)
        ≈˘⟨ refl⟩∘⟨ homomorphism L ⟩
      L⊣R.counit.η (F₀ L′ X) ∘ F₁ L (η β (F₀ L′ X) C.∘ L′⊣R′.unit.η X)
        ≈˘⟨ refl⟩∘⟨ F-resp-≈ L commute₁ ⟩
      L⊣R.counit.η (F₀ L′ X) ∘ F₁ L (F₁ R (η α X) C.∘ L⊣R.unit.η X)
        ≈⟨ L⊣R.RLadjunct≈id ⟩
      η α X
        ∎

  module _ where
    open C
    open HomReasoning
    open MR C

    commute₄ : ∀ {X} → F₁ R (L′⊣R′.counit.η X) ∘ F₁ R (η α (F₀ R′ X)) ∘ L⊣R.unit.η (F₀ R′ X) ≈ η β X
    commute₄ {X} = begin
      F₁ R (L′⊣R′.counit.η X) ∘ F₁ R (η α (F₀ R′ X)) ∘ L⊣R.unit.η (F₀ R′ X)
        ≈˘⟨ pushˡ (homomorphism R) ⟩
      F₁ R (L′⊣R′.counit.η X D.∘ η α (F₀ R′ X)) ∘ L⊣R.unit.η (F₀ R′ X)
        ≈˘⟨ F-resp-≈ R commute₂ ⟩∘⟨refl ⟩
      F₁ R (L⊣R.counit.η X D.∘ F₁ L (η β X)) ∘ L⊣R.unit.η (F₀ R′ X)
        ≈⟨ L⊣R.LRadjunct≈id ⟩
      η β X
         ∎

record HaveMate {L L′ : Functor C D} {R R′ : Functor D C}
                (L⊣R : L ⊣ R) (L′⊣R′ : L′ ⊣ R′) : Set (levelOfTerm L⊣R ⊔ levelOfTerm L′⊣R′) where
  field
    α    : NaturalTransformation L L′
    β    : NaturalTransformation R′ R
    mate : Mate L⊣R L′⊣R′ α β

  module α = NaturalTransformation α
  module β = NaturalTransformation β
  open Mate mate public

-- show that the commutative diagram implies natural isomorphism between homsetoids.
-- the problem is that two homsetoids live in two universe level, in a situation similar to the definition
-- of adjoint via naturally isomorphic homsetoids.
module _ {L L′ : Functor C D} {R R′ : Functor D C}
         {L⊣R : L ⊣ R} {L′⊣R′ : L′ ⊣ R′}
         {α : NaturalTransformation L L′}
         {β : NaturalTransformation R′ R}
         (mate : Mate L⊣R L′⊣R′ α β) where
  private
    open Mate mate
    open Functor
    module C     = Category C
    module D     = Category D
    module α     = NaturalTransformation α
    module β     = NaturalTransformation β
    module L⊣R   = Adjoint L⊣R
    module L′⊣R′ = Adjoint L′⊣R′

  -- there are two squares to show
  module _ {X : C.Obj} {Y : D.Obj} where
    open Setoid (L′⊣R′.Hom[L-,-].F₀ (X , Y) ⇨ L⊣R.Hom[-,R-].F₀ (X , Y))
    open C hiding (_≈_)
    open MR C
    open C.HomReasoning
    module DH = D.HomReasoning

    mate-commute₁ : F₁ Hom[ C ][-,-] (C.id , β.η Y) ∙ L′⊣R′.Hom-inverse.to {X} {Y}
                  ≈ L⊣R.Hom-inverse.to {X} {Y} ∙ F₁ Hom[ D ][-,-] (α.η X , D.id)
    mate-commute₁ {f} {g} f≈g = begin
      β.η Y ∘ (F₁ R′ f ∘ L′⊣R′.unit.η X) ∘ C.id  ≈⟨ refl⟩∘⟨ identityʳ ⟩
      β.η Y ∘ F₁ R′ f ∘ L′⊣R′.unit.η X           ≈⟨ pullˡ (β.commute f) ⟩
      (F₁ R f ∘ β.η (F₀ L′ X)) ∘ L′⊣R′.unit.η X  ≈˘⟨ pushʳ commute₁ ⟩
      F₁ R f ∘ F₁ R (α.η X) ∘ L⊣R.unit.η X       ≈˘⟨ pushˡ (homomorphism R) ⟩
      F₁ R (f D.∘ α.η X) ∘ L⊣R.unit.η X          ≈⟨ F-resp-≈ R (D.∘-resp-≈ˡ f≈g DH.○ DH.⟺ D.identityˡ) ⟩∘⟨refl ⟩
      F₁ R (D.id D.∘ g D.∘ α.η X) ∘ L⊣R.unit.η X ∎

  module _ {X : C.Obj} {Y : D.Obj} where
    open Setoid (L′⊣R′.Hom[-,R-].F₀ (X , Y) ⇨ L⊣R.Hom[L-,-].F₀ (X , Y))
    open D hiding (_≈_)
    open MR D
    open D.HomReasoning
    module CH = C.HomReasoning

    mate-commute₂ : F₁ Hom[ D ][-,-] (α.η X , D.id) ∙ L′⊣R′.Hom-inverse.from {X} {Y}
                  ≈ L⊣R.Hom-inverse.from {X} {Y} ∙ F₁ Hom[ C ][-,-] (C.id , β.η Y)
    mate-commute₂ {f} {g} f≈g = begin
      D.id ∘ (L′⊣R′.counit.η Y ∘ F₁ L′ f) ∘ α.η X  ≈⟨ identityˡ ⟩
      (L′⊣R′.counit.η Y ∘ F₁ L′ f) ∘ α.η X         ≈˘⟨ pushʳ (α.commute f) ⟩
      L′⊣R′.counit.η Y ∘ α.η (F₀ R′ Y) ∘ F₁ L f    ≈˘⟨ pushˡ commute₂ ⟩
      (L⊣R.counit.η Y ∘ F₁ L (β.η Y)) ∘ F₁ L f     ≈˘⟨ pushʳ (homomorphism L) ⟩
      L⊣R.counit.η Y ∘ F₁ L (β.η Y C.∘ f)          ≈⟨ refl⟩∘⟨ F-resp-≈ L (C.∘-resp-≈ʳ (f≈g CH.○ CH.⟺ C.identityʳ)) ⟩
      L⊣R.counit.η Y ∘ F₁ L (β.η Y C.∘ g C.∘ C.id) ∎

-- alternatively, if commute₃ and commute₄ are shown, then a Mate can be constructed.

module _ {L L′ : Functor C D} {R R′ : Functor D C}
         {L⊣R : L ⊣ R} {L′⊣R′ : L′ ⊣ R′}
         {α : NaturalTransformation L L′}
         {β : NaturalTransformation R′ R} where
  private
    open Functor
    module C     = Category C
    module D     = Category D
    module α     = NaturalTransformation α
    module β     = NaturalTransformation β
    module L⊣R   = Adjoint L⊣R
    module L′⊣R′ = Adjoint L′⊣R′

  module _ (commute₃ : ∀ {X} → L⊣R.counit.η (F₀ L′ X) D.∘ F₁ L (β.η (F₀ L′ X)) D.∘ F₁ L (L′⊣R′.unit.η X) D.≈ α.η X) where
    open C
    open HomReasoning

    commute₁ : ∀ {X} → F₁ R (α.η X) ∘ L⊣R.unit.η X ≈ β.η (F₀ L′ X) ∘ L′⊣R′.unit.η X
    commute₁ {X} = begin
      F₁ R (α.η X) ∘ L⊣R.unit.η X
        ≈˘⟨ F-resp-≈ R commute₃ ⟩∘⟨refl ⟩
      F₁ R (L⊣R.counit.η (F₀ L′ X) D.∘ F₁ L (β.η (F₀ L′ X)) D.∘ F₁ L (L′⊣R′.unit.η X)) ∘ L⊣R.unit.η X
        ≈˘⟨ F-resp-≈ R (D.∘-resp-≈ʳ (homomorphism L)) ⟩∘⟨refl ⟩
      F₁ R (L⊣R.counit.η (F₀ L′ X) D.∘ F₁ L (β.η (F₀ L′ X) ∘ L′⊣R′.unit.η X)) ∘ L⊣R.unit.η X
        ≈⟨ L⊣R.LRadjunct≈id ⟩
      β.η (F₀ L′ X) ∘ L′⊣R′.unit.η X
        ∎

  module _ (commute₄ : ∀ {X} → F₁ R (L′⊣R′.counit.η X) C.∘ F₁ R (α.η (F₀ R′ X)) C.∘ L⊣R.unit.η (F₀ R′ X) C.≈ β.η X) where
    open D
    open HomReasoning
    open MR C

    commute₂ : ∀ {X} → L⊣R.counit.η X ∘ F₁ L (β.η X) ≈ L′⊣R′.counit.η X ∘ α.η (F₀ R′ X)
    commute₂ {X} = begin
      L⊣R.counit.η X ∘ F₁ L (β.η X)
        ≈˘⟨ refl⟩∘⟨ F-resp-≈ L commute₄ ⟩
      L⊣R.counit.η X ∘ F₁ L (F₁ R (L′⊣R′.counit.η X) C.∘ F₁ R (α.η (F₀ R′ X)) C.∘ L⊣R.unit.η (F₀ R′ X))
        ≈˘⟨ refl⟩∘⟨ F-resp-≈ L (pushˡ (homomorphism R)) ⟩
      L⊣R.counit.η X ∘ F₁ L (F₁ R (L′⊣R′.counit.η X ∘ α.η (F₀ R′ X)) C.∘ L⊣R.unit.η (F₀ R′ X))
        ≈⟨ L⊣R.RLadjunct≈id ⟩
      L′⊣R′.counit.η X ∘ α.η (F₀ R′ X)
        ∎

  mate′ : (∀ {X} → L⊣R.counit.η (F₀ L′ X) D.∘ F₁ L (β.η (F₀ L′ X)) D.∘ F₁ L (L′⊣R′.unit.η X) D.≈ α.η X) →
          (∀ {X} → F₁ R (L′⊣R′.counit.η X) C.∘ F₁ R (α.η (F₀ R′ X)) C.∘ L⊣R.unit.η (F₀ R′ X) C.≈ β.η X) →
          Mate L⊣R L′⊣R′ α β
  mate′ commute₃ commute₄ = record
    { commute₁ = commute₁ commute₃
    ; commute₂ = commute₂ commute₄
    }


text:
open import Agda.Builtin.List

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

foldr : ∀ {a b} {A : Set a} {B : Set b} → (A → B → B) → B → List A → B
foldr c n []       = n
foldr c n (x ∷ xs) = c x (foldr c n xs)

data Rose (A : Set) : Set where
  leaf : (a : A) → Rose A
  node : (rs : List (Rose A)) → Rose A

record IsSeq (A S : Set) : Set where
  field
    nil : S
    sg  : (a : A) → S
    _∙_ : (s t : S) → S

  concat : (ss : List S) → S
  concat = foldr _∙_ nil

open IsSeq {{...}}

{-# TERMINATING #-}
flatten : ∀{A S} {{_ : IsSeq A S}} → Rose A → S
flatten (leaf a) = sg a
flatten (node rs) = concat (map flatten rs)


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
{-
This file contains:
1. The long exact sequence of loop spaces Ωⁿ (fib f) → Ωⁿ A → Ωⁿ B
2. The long exact sequence of homotopy groups πₙ(fib f) → πₙ A → πₙ B
3. Some lemmas relating the map in the sequence to maps using the
   other definition of πₙ (maps from Sⁿ)
-}
module Cubical.Homotopy.Group.LES where

open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Group.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc)
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism
open Iso
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function

open import Cubical.HITs.SetTruncation
  renaming (rec to sRec
          ; elim to sElim ; elim2 to sElim2
          ; map to sMap)
open import Cubical.HITs.PropositionalTruncation
  renaming (rec to pRec)

open import Cubical.Data.Sigma
open import Cubical.Data.Nat

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.GroupPath

-- We will need an explicitly defined equivalence
-- (PathP (λ i → p i ≡ y) q q) ≃ (sym q ∙∙ p ∙∙ q ≡ refl)
-- This is given by →∙∙lCancel below
module _ {ℓ : Level} {A : Type ℓ} {x y : A} (p : x ≡ x) (q : x ≡ y) where
  →∙∙lCancel-fill : PathP (λ i → p i ≡ y) q q → I → I → I → A
  →∙∙lCancel-fill PP k i j =
    hfill (λ k → λ {(i = i0) → doubleCompPath-filler (sym q) p q k j
                 ; (i = i1) → y
                 ; (j = i0) → q (i ∨ k)
                 ; (j = i1) → q (i ∨ k)})
        (inS (PP j i))
        k

  ←∙∙lCancel-fill : sym q ∙∙ p ∙∙ q ≡ refl → I → I → I → A
  ←∙∙lCancel-fill PP k i j =
    hfill (λ k → λ {(i = i0) → q (j ∨ ~ k)
                   ; (i = i1) → q (j ∨ ~ k)
                   ; (j = i0) → doubleCompPath-filler (sym q) p q (~ k) i
                   ; (j = i1) → y})
          (inS (PP j i))
          k

  →∙∙lCancel : PathP (λ i → p i ≡ y) q q → sym q ∙∙ p ∙∙ q ≡ refl
  →∙∙lCancel PP i j = →∙∙lCancel-fill PP i1 i j

  ←∙∙lCancel : sym q ∙∙ p ∙∙ q ≡ refl → PathP (λ i → p i ≡ y) q q
  ←∙∙lCancel PP i j = ←∙∙lCancel-fill PP i1 i j

  ←∙∙lCancel→∙∙lCancel : (PP : PathP (λ i → p i ≡ y) q q)
    → ←∙∙lCancel (→∙∙lCancel PP) ≡ PP
  ←∙∙lCancel→∙∙lCancel PP r i j =
    hcomp (λ k → λ {(r = i0) → ←∙∙lCancel-fill (→∙∙lCancel PP) k i j
                   ; (r = i1) → PP i j
                   ; (j = i0) → doubleCompPath-filler (sym q) p q (~ k ∧ ~ r) i
                   ; (j = i1) → y
                   ; (i = i0) → q (j ∨ ~ k ∧ ~ r)
                   ; (i = i1) → q (j ∨ ~ k ∧ ~ r)})
     (hcomp (λ k → λ {(r = i0) → →∙∙lCancel-fill PP k j i
                   ; (r = i1) → PP i j
                   ; (j = i0) → doubleCompPath-filler (sym q) p q (k ∧ ~ r) i
                   ; (j = i1) → y
                   ; (i = i0) → q (j ∨ k ∧ ~ r)
                   ; (i = i1) → q (j ∨ k ∧ ~ r)})
            (PP i j))

  →∙∙lCancel←∙∙lCancel : (PP : sym q ∙∙ p ∙∙ q ≡ refl)
    → →∙∙lCancel (←∙∙lCancel PP) ≡ PP
  →∙∙lCancel←∙∙lCancel PP r i j =
    hcomp (λ k → λ {(r = i0) → →∙∙lCancel-fill (←∙∙lCancel PP) k i j
                   ; (r = i1) → PP i j
                   ; (j = i0) → q (i ∨ k ∨ r)
                   ; (j = i1) → q (i ∨ k ∨ r)
                   ; (i = i0) → doubleCompPath-filler (sym q) p q (r ∨ k) j
                   ; (i = i1) → y})
     (hcomp (λ k → λ {(r = i0) → ←∙∙lCancel-fill PP k j i
                   ; (r = i1) → PP i j
                   ; (j = i0) → q (i ∨ r ∨ ~ k)
                   ; (j = i1) → q (i ∨ r ∨ ~ k)
                   ; (i = i0) → doubleCompPath-filler (sym q) p q (r ∨ ~ k) j
                   ; (i = i1) → y})
            (PP i j))

←∙∙lCancel-refl-refl :
  {ℓ : Level} {A : Type ℓ} {x : A} (p : refl {x = x} ≡ refl)
  → ←∙∙lCancel {x = x} {y = x} refl refl (sym (rUnit refl) ∙ p)
  ≡ flipSquare p
←∙∙lCancel-refl-refl p k i j =
  hcomp (λ r → λ { (i = i0) → p i0 i0
             ; (i = i1) → p i0 i0
             ; (j = i0) → rUnit (λ _ → p i0 i0) (~ r) i
             ; (j = i1) → p i0 i0
             ; (k = i0) → ←∙∙lCancel-fill refl refl (sym (rUnit refl) ∙ p) r i j
             ; (k = i1) → compPath-filler' (sym (rUnit refl)) p (~ r) j i})
         ((sym (rUnit refl) ∙ p) j i)

{- We need an iso Ω(fib f) ≅ fib(Ω f) -}
ΩFibreIso : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B)
            → Iso (typ (Ω (fiber (fst f) (pt B) , (pt A) , snd f)))
                   (fiber (Ω→ f .fst) refl)
fun (ΩFibreIso f) p = (cong fst p) ,
                   →∙∙lCancel (cong (fst f) (cong fst p)) (snd f)
                      (cong snd p)
fst (inv (ΩFibreIso f) (p , q) i) = p i
snd (inv (ΩFibreIso f) (p , q) i) = ←∙∙lCancel (cong (fst f) p) (snd f) q i
rightInv (ΩFibreIso f) (p , q) = ΣPathP (refl , →∙∙lCancel←∙∙lCancel _ _ q)
fst (leftInv (ΩFibreIso f) p i j) = fst (p j)
snd (leftInv (ΩFibreIso f) p i j) k =
  ←∙∙lCancel→∙∙lCancel _ _ (cong snd p) i j k

{- Some homomorphism properties of the above iso -}
ΩFibreIsopres∙fst : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B)
                    → (p q : (typ (Ω (fiber (fst f) (pt B) , (pt A) , snd f))))
                    → fst (fun (ΩFibreIso f) (p ∙ q))
                    ≡ fst (fun (ΩFibreIso f) p) ∙ fst (fun (ΩFibreIso f) q)
ΩFibreIsopres∙fst f p q = cong-∙ fst p q

ΩFibreIso⁻pres∙snd : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'}
                    (f : A →∙ B) (p q : typ (Ω (Ω B)))
                    → inv (ΩFibreIso f) (refl , (Ω→ f .snd ∙ p ∙ q))
                    ≡ inv (ΩFibreIso f) (refl , Ω→ f .snd ∙ p)
                    ∙ inv (ΩFibreIso f) (refl , Ω→ f .snd ∙ q)
ΩFibreIso⁻pres∙snd {A = A} {B = B}=
  →∙J (λ b₀ f → (p q : typ (Ω (Ω (fst B , b₀))))
               → inv (ΩFibreIso f) (refl , (Ω→ f .snd ∙ p ∙ q))
                 ≡ inv (ΩFibreIso f) (refl , Ω→ f .snd ∙ p)
                 ∙ inv (ΩFibreIso f) (refl , Ω→ f .snd ∙ q))
       ind
  where
  ind : (f : typ A → typ B) (p q : typ (Ω (Ω (fst B , f (pt A)))))
      → inv (ΩFibreIso (f , refl)) (refl , (sym (rUnit refl) ∙ p ∙ q))
       ≡ inv (ΩFibreIso (f , refl)) (refl , sym (rUnit refl) ∙ p)
       ∙ inv (ΩFibreIso (f , refl)) (refl , sym (rUnit refl) ∙ q)
  fst (ind f p q i j) =
    (rUnit refl
     ∙ sym (cong-∙ fst
      (inv (ΩFibreIso (f , refl)) (refl , sym (rUnit refl) ∙ p))
      (inv (ΩFibreIso (f , refl)) (refl , sym (rUnit refl) ∙ q)))) i j
  snd (ind f p q i j) k =
    hcomp (λ r
      → λ {(i = i0) → ←∙∙lCancel-refl-refl (p ∙ q) (~ r) j k --
          ; (i = i1) →
            snd (compPath-filler
                (inv (ΩFibreIso (f , refl))
                     (refl , sym (rUnit refl) ∙ p))
                (inv (ΩFibreIso (f , refl))
                     (refl , sym (rUnit refl) ∙ q)) r j) k
          ; (j = i0) → f (snd A)
          ; (j = i1) → snd (inv (ΩFibreIso (f , refl))
                            (refl , sym (rUnit refl) ∙ q) (r ∨ ~ i)) k
          ; (k = i0) → main r i j
          ; (k = i1) → f (snd A)})
       (hcomp (λ r → λ {(i = i0) → (p ∙ q) k j
                   ; (i = i1) → ←∙∙lCancel-refl-refl p (~ r) j k
                   ; (j = i0) → f (snd A)
                   ; (j = i1) → ←∙∙lCancel-refl-refl q (~ r) (~ i) k
                   ; (k = i0) → f (pt A)
                   ; (k = i1) → f (snd A)})
              (hcomp (λ r → λ {(i = i0) → (compPath-filler' p q r) k j
                   ; (i = i1) → p (k ∨ ~ r) j
                   ; (j = i0) → f (snd A)
                   ; (j = i1) → q k (~ i)
                   ; (k = i0) → p (k ∨ ~ r) j
                   ; (k = i1) → f (snd A)})
               (q k (~ i ∧ j))))
    where
    P = (inv (ΩFibreIso (f , refl)) (refl , sym (rUnit refl) ∙ p))
    Q = (inv (ΩFibreIso (f , refl)) (refl , sym (rUnit refl) ∙ q))

    main : I → I → I → fst B
    main r i j =
      hcomp (λ k → λ {(i = i0) → f (snd A)
                     ; (i = i1) → f (fst (compPath-filler P Q (r ∨ ~ k) j))
                     ; (j = i0) → f (snd A)
                     ; (j = i1) → f (snd A)
                     ; (r = i0) → f (fst (compPath-filler P Q (i ∧ ~ k) j))
                     ; (r = i1) → f ((rUnit refl ∙ sym (cong-∙ fst P Q)) i j)})
            (hcomp (λ k → λ {(i = i0) → f (rUnit (λ _ → pt A) (~ k ∧ r) j)
                     ; (i = i1) → f (fst ((P ∙ Q) j))
                     ; (j = i0) → f (snd A)
                     ; (j = i1) → f (snd A)
                     ; (r = i0) → f (fst (compPath-filler P Q i j))
                     ; (r = i1) → f ((compPath-filler' (rUnit refl)
                                     (sym (cong-∙ fst P Q)) k) i j)})
             (hcomp (λ k → λ {(i = i0) → f (rUnit (λ _ → pt A) (k ∧ r) j)
                     ; (i = i1) → f (fst (compPath-filler P Q k j))
                     ; (j = i0) → f (snd A)
                     ; (j = i1) → f (snd A)
                     ; (r = i0) → f (fst (compPath-filler P Q (i ∧ k) j))
                     ; (r = i1) → f ((cong-∙∙-filler fst refl P Q) k (~ i) j)})
                    (f (snd A))))

ΩFibreIso∙ : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B)
            → Iso.fun (ΩFibreIso f) refl ≡ (refl , (∙∙lCancel (snd f)))
ΩFibreIso∙ {A = A} {B = B} =
  →∙J (λ b f → Iso.fun (ΩFibreIso f) refl ≡ (refl , (∙∙lCancel (snd f))))
    λ f → ΣPathP (refl , help f)
  where
  help : (f : fst A → fst B) →
       →∙∙lCancel (λ i → f (snd A)) refl (λ i → refl)
       ≡ ∙∙lCancel refl
  help f i j r =
    hcomp (λ k → λ {(i = i0) →
                    →∙∙lCancel-fill (λ _ → f (snd A)) refl refl k j r
                   ; (i = i1) → ∙∙lCancel-fill (λ _ → f (snd A))  j r k
                   ; (j = i0) → rUnit (λ _ → f (snd A)) k r
                   ; (j = i1) → f (snd A)
                   ; (r = i1) → f (snd A)
                   ; (r = i0) → f (snd A)})
          (f (snd A))

ΩFibreIso⁻∙ : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B)
           → Iso.inv (ΩFibreIso f) (refl , (∙∙lCancel (snd f))) ≡ refl
ΩFibreIso⁻∙ f =
  cong (Iso.inv (ΩFibreIso f)) (sym (ΩFibreIso∙ f)) ∙ leftInv (ΩFibreIso f) refl

{- Ωⁿ (fib f) ≃∙ fib (Ωⁿ f) -}
Ω^Fibre≃∙ : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} (n : ℕ) (f : A →∙ B)
             → ((Ω^ n) (fiber (fst f) (pt B) , (pt A) , snd f))
              ≃∙ ((fiber (Ω^→ n f .fst) (snd ((Ω^ n) B)))
                , (snd ((Ω^ n) A)) , (Ω^→ n f .snd))
Ω^Fibre≃∙ zero f =  (idEquiv _) , refl
Ω^Fibre≃∙ (suc n) f =
  compEquiv∙
    (Ω≃∙ (Ω^Fibre≃∙ n f))
    ((isoToEquiv (ΩFibreIso (Ω^→ n f))) , ΩFibreIso∙ (Ω^→ n f))

{- Its inverse iso directly defined -}
Ω^Fibre≃∙⁻ : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'}
     (n : ℕ) (f : A →∙ B)
  → ((fiber (Ω^→ n f .fst) (snd ((Ω^ n) B)))
     , (snd ((Ω^ n) A)) , (Ω^→ n f .snd))
  ≃∙ ((Ω^ n) (fiber (fst f) (pt B) , (pt A) , snd f))
Ω^Fibre≃∙⁻ zero f = (idEquiv _) , refl
Ω^Fibre≃∙⁻ (suc n) f =
  compEquiv∙
    ((isoToEquiv (invIso (ΩFibreIso (Ω^→ n f))))
    , (ΩFibreIso⁻∙ (Ω^→ n f)))
    (Ω≃∙ (Ω^Fibre≃∙⁻ n f))

isHomogeneousΩ^→fib : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'}
    (n : ℕ) (f : A →∙ B)
  → isHomogeneous
    ((fiber (Ω^→ (suc n) f .fst) (snd ((Ω^ (suc n)) B)))
      , (snd ((Ω^ (suc n)) A)) , (Ω^→ (suc n) f .snd))
isHomogeneousΩ^→fib n f =
  subst isHomogeneous (ua∙ ((fst (Ω^Fibre≃∙ (suc n) f)))
                           (snd (Ω^Fibre≃∙ (suc n) f)))
                      (isHomogeneousPath _ _)

Ω^Fibre≃∙sect : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'}
     (n : ℕ) (f : A →∙ B)
  → (≃∙map (Ω^Fibre≃∙⁻ n f) ∘∙ ≃∙map (Ω^Fibre≃∙ n f))
    ≡ idfun∙ _
Ω^Fibre≃∙sect zero f = ΣPathP (refl , (sym (rUnit refl)))
Ω^Fibre≃∙sect (suc n) f =
  →∙Homogeneous≡ (isHomogeneousPath _ _)
    (funExt
      λ p → cong (fst (fst (Ω≃∙ (Ω^Fibre≃∙⁻ n f))))
                   (leftInv (ΩFibreIso (Ω^→ n f))
                     ((fst (fst (Ω≃∙ (Ω^Fibre≃∙ n f))) p)))
          ∙ sym (Ω→∘ (≃∙map (Ω^Fibre≃∙⁻ n f))
                      (≃∙map (Ω^Fibre≃∙ n f)) p)
          ∙ (λ i → (Ω→ (Ω^Fibre≃∙sect n f i)) .fst p)
          ∙ sym (rUnit p))

Ω^Fibre≃∙retr : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'}
     (n : ℕ) (f : A →∙ B)
  → (≃∙map (Ω^Fibre≃∙ n f) ∘∙ ≃∙map (Ω^Fibre≃∙⁻ n f))
    ≡ idfun∙ _
Ω^Fibre≃∙retr zero f = ΣPathP (refl , (sym (rUnit refl)))
Ω^Fibre≃∙retr (suc n) f =
    →∙Homogeneous≡ (isHomogeneousΩ^→fib n f)
      (funExt (λ p →
        cong (fun (ΩFibreIso (Ω^→ n f)))
          ((sym (Ω→∘ (≃∙map (Ω^Fibre≃∙ n f))
                     (≃∙map (Ω^Fibre≃∙⁻ n f))
               (inv (ΩFibreIso (Ω^→ n f)) p)))
         ∙ (λ i → Ω→ (Ω^Fibre≃∙retr n f i) .fst (inv (ΩFibreIso (Ω^→ n f)) p))
         ∙ sym (rUnit (inv (ΩFibreIso (Ω^→ n f)) p)))
        ∙ rightInv (ΩFibreIso (Ω^→ n f)) p))

Ω^Fibre≃∙' : {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'}
     (n : ℕ) (f : A →∙ B)
  → ((Ω^ n) (fiber (fst f) (pt B) , (pt A) , snd f))
   ≃∙ ((fiber (Ω^→ n f .fst) (snd ((Ω^ n) B)))
     , (snd ((Ω^ n) A)) , (Ω^→ n f .snd))
Ω^Fibre≃∙' zero f = idEquiv _ , refl
Ω^Fibre≃∙' (suc zero) f =
  (isoToEquiv (ΩFibreIso (Ω^→ zero f))) , ΩFibreIso∙ (Ω^→ zero f)
Ω^Fibre≃∙' (suc (suc n)) f =
  compEquiv∙
    (Ω≃∙ (Ω^Fibre≃∙ (suc n) f))
    ((isoToEquiv (ΩFibreIso (Ω^→ (suc n) f))) , ΩFibreIso∙ (Ω^→ (suc n) f))

-- The long exact sequence of loop spaces.
module ΩLES {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) where
  {- Fibre of f -}
  fibf : Pointed _
  fibf = fiber (fst f) (pt B) , (pt A , snd f)

  {- Fibre of Ωⁿ f -}
  fibΩ^f : (n : ℕ) → Pointed _
  fst (fibΩ^f n) = fiber (Ω^→ n f .fst) (snd ((Ω^ n) B))
  snd (fibΩ^f n) = (snd ((Ω^ n) A)) , (Ω^→ n f .snd)

  Ω^fibf : (n : ℕ) → Pointed _
  Ω^fibf n = (Ω^ n) fibf

  {- Helper function fib (Ωⁿ f) → Ωⁿ A -}
  fibΩ^f→A : (n : ℕ) → fibΩ^f n →∙ (Ω^ n) A
  fst (fibΩ^f→A n) = fst
  snd (fibΩ^f→A n) = refl

  {- The main function Ωⁿ(fib f) → Ωⁿ A, which is just the composition
  Ωⁿ(fib f) ≃ fib (Ωⁿ f) → Ωⁿ A, where the last function is
  fibΩ^f→A. Hence most proofs will concern fibΩ^f→A, since it is easier to
  work with. -}
  Ω^fibf→A : (n : ℕ) → Ω^fibf n →∙ (Ω^ n) A
  Ω^fibf→A n = fibΩ^f→A n ∘∙ ≃∙map (Ω^Fibre≃∙ n f)

  {- The function preserves path composition -}
  Ω^fibf→A-pres∙ : (n : ℕ) → (p q : Ω^fibf (suc n) .fst)
    → Ω^fibf→A (suc n) .fst (p ∙ q)
     ≡ Ω^fibf→A (suc n) .fst p
     ∙ Ω^fibf→A (suc n) .fst q
  Ω^fibf→A-pres∙ n p q =
    cong (fst (fibΩ^f→A (suc n)))
      (cong (fun (ΩFibreIso (Ω^→ n f)))
        (Ω→pres∙ (≃∙map (Ω^Fibre≃∙ n f)) p q))
    ∙ ΩFibreIsopres∙fst (Ω^→ n f)
        (fst (Ω→ (≃∙map (Ω^Fibre≃∙ n f))) p)
        (fst (Ω→ (≃∙map (Ω^Fibre≃∙ n f))) q)

  {- The function Ωⁿ A → Ωⁿ B -}
  A→B : (n : ℕ) → (Ω^ n) A →∙ (Ω^ n) B
  A→B n = Ω^→ n f

  {- It preserves path composition -}
  A→B-pres∙ : (n : ℕ) → (p q : typ ((Ω^ (suc n)) A))
            → fst (A→B (suc n)) (p ∙ q)
            ≡ fst (A→B (suc n)) p ∙ fst (A→B (suc n)) q
  A→B-pres∙ n p q = Ω^→pres∙ f n p q

  {- Helper function Ωⁿ⁺¹ B → fib (Ωⁿ f) -}
  ΩB→fibΩ^f : (n : ℕ) → ((Ω^ (suc n)) B) →∙ fibΩ^f n
  fst (ΩB→fibΩ^f n) x = (snd ((Ω^ n) A)) , (Ω^→ n f .snd ∙ x)
  snd (ΩB→fibΩ^f n) = ΣPathP (refl , (sym (rUnit _)))

  {- The main function Ωⁿ⁺¹ B → Ωⁿ (fib f),
     factoring through the above function -}
  ΩB→Ω^fibf : (n : ℕ) → (Ω^ (suc n)) B →∙ Ω^fibf n
  ΩB→Ω^fibf n =
       (≃∙map (Ω^Fibre≃∙⁻ n f))
    ∘∙ ΩB→fibΩ^f n

  {- It preserves path composition -}
  ΩB→Ω^fibf-pres∙ : (n : ℕ) → (p q : typ ((Ω^ (2 + n)) B))
    → fst (ΩB→Ω^fibf (suc n)) (p ∙ q)
     ≡ fst (ΩB→Ω^fibf (suc n)) p ∙ fst (ΩB→Ω^fibf (suc n)) q
  ΩB→Ω^fibf-pres∙ n p q =
      cong (fst (fst (Ω^Fibre≃∙⁻ (suc n) f)))
        refl
    ∙ cong (fst (fst (Ω≃∙ (Ω^Fibre≃∙⁻ n f))))
        (cong (fun (invIso (ΩFibreIso (Ω^→ n f))))
          (λ _ → snd ((Ω^ suc n) A) , Ω^→ (suc n) f .snd ∙ p ∙ q))
    ∙ cong (fst (fst (Ω≃∙ (Ω^Fibre≃∙⁻ n f))))
           (ΩFibreIso⁻pres∙snd (Ω^→ n f) p q)
    ∙ Ω≃∙pres∙ (Ω^Fibre≃∙⁻ n f)
        (inv (ΩFibreIso (Ω^→ n f)) (refl , Ω→ (Ω^→ n f) .snd ∙ p))
        (inv (ΩFibreIso (Ω^→ n f)) (refl , Ω→ (Ω^→ n f) .snd ∙ q))

  {- Hence we have our sequence
     ... → Ωⁿ⁺¹B → Ωⁿ(fib f) → Ωⁿ A → Ωⁿ B → ...  (*)
     We first prove the exactness properties for the helper functions
     ΩB→fibΩ^f and fibΩ^f→A, and then deduce exactness of the whole sequence
     by noting that the functions in (*) are just ΩB→fibΩ^f, fibΩ^f→A but
     composed with equivalences
  -}
  private
    Im-fibΩ^f→A⊂Ker-A→B : (n : ℕ) (x : _)
                       → isInIm∙ (fibΩ^f→A n) x
                       → isInKer∙ (A→B n) x
    Im-fibΩ^f→A⊂Ker-A→B n x =
      uncurry λ p → J (λ x _ → isInKer∙ (A→B n) x)
        (snd p)

    Ker-fibΩ^f→A⊂Im-ΩB→fibΩ^f : (n : ℕ) (x : _)
                       → isInKer∙ (fibΩ^f→A n) x
                       → isInIm∙ (ΩB→fibΩ^f n) x
    Ker-fibΩ^f→A⊂Im-ΩB→fibΩ^f n x ker =
        (sym (Ω^→ n f .snd)
      ∙ cong (Ω^→ n f .fst) (sym ker) ∙ snd x) , ΣPathP ((sym ker) ,
      ((∙assoc (Ω^→ n f .snd)
        (sym (Ω^→ n f .snd))
        (sym (cong (Ω^→ n f .fst) ker) ∙ snd x)
      ∙∙ cong (_∙ (sym (cong (Ω^→ n f .fst) ker) ∙ snd x))
              (rCancel (Ω^→ n f .snd))
      ∙∙ sym (lUnit (sym (cong (Ω^→ n f .fst) ker) ∙ snd x)))
      ◁ (λ i j → compPath-filler'
                  (cong (Ω^→ n f .fst) (sym ker)) (snd x) (~ i) j)))

    Im-A→B⊂Ker-ΩB→fibΩ^f : (n : ℕ) (x : fst (((Ω^ (suc n)) B)))
                       → isInIm∙ (A→B (suc n)) x
                       → isInKer∙ (ΩB→fibΩ^f n) x
    Im-A→B⊂Ker-ΩB→fibΩ^f n x =
      uncurry λ p
       → J (λ x _ → isInKer∙ (ΩB→fibΩ^f n) x)
         (ΣPathP (p , (((λ i → (λ j → Ω^→ n f .snd (j ∧ ~ i))
                             ∙ ((λ j → Ω^→ n f .snd (~ j ∧ ~ i))
                             ∙∙ cong (Ω^→ n f .fst) p
                             ∙∙ Ω^→ n f .snd))
                      ∙ sym (lUnit (cong (Ω^→ n f .fst) p ∙ Ω^→ n f .snd)))
                    ◁ λ i j → compPath-filler'
                       (cong (Ω^→ n f .fst) p) (Ω^→ n f .snd) (~ i) j)))

    Ker-ΩB→fibΩ^f⊂Im-A→B : (n : ℕ) (x : fst (((Ω^ (suc n)) B)))
                       → isInKer∙ (ΩB→fibΩ^f n) x
                       → isInIm∙ (A→B (suc n)) x
    fst (Ker-ΩB→fibΩ^f⊂Im-A→B n x inker) = cong fst inker
    snd (Ker-ΩB→fibΩ^f⊂Im-A→B n x inker) = lem
      where
      lem : fst (A→B (suc n)) (λ i → fst (inker i)) ≡ x
      lem i j =
        hcomp (λ k → λ { (i = i0) → doubleCompPath-filler
                                       (sym (snd (Ω^→ n f)))
                                       ((λ i → Ω^→ n f .fst (fst (inker i))))
                                       (snd (Ω^→ n f)) k j
                        ; (i = i1) → compPath-filler' (Ω^→ n f .snd) x (~ k) j
                        ; (j = i0) → snd (Ω^→ n f) k
                        ; (j = i1) → snd (Ω^→ n f) (k ∨ i)})
              (hcomp (λ k → λ { (i = i0) → (snd (inker j)) (~ k)
                               ; (i = i1) → ((Ω^→ n f .snd) ∙ x) (j ∨ ~ k)
                               ; (j = i0) → ((Ω^→ n f .snd) ∙ x) (~ k)
                               ; (j = i1) → snd (Ω^→ n f) (i ∨ ~ k)})
                      (snd ((Ω^ n) B)))

  {- Finally, we get exactness of the sequence
     we are interested in -}
  Im-Ω^fibf→A⊂Ker-A→B : (n : ℕ) (x : _)
                     → isInIm∙ (Ω^fibf→A n) x
                     → isInKer∙ (A→B n) x
  Im-Ω^fibf→A⊂Ker-A→B n x x₁ =
    Im-fibΩ^f→A⊂Ker-A→B n x
      (((fst (fst (Ω^Fibre≃∙ n f))) (fst x₁))
        , snd x₁)

  Ker-A→B⊂Im-Ω^fibf→A : (n : ℕ) (x : _)
                   → isInKer∙ (A→B n) x
                   → isInIm∙ (Ω^fibf→A n) x
  Ker-A→B⊂Im-Ω^fibf→A n x ker =
      invEq (fst (Ω^Fibre≃∙ n f)) (x , ker)
    , (cong fst (secEq (fst (Ω^Fibre≃∙ n f)) (x , ker)))

  Ker-Ω^fibf→A⊂Im-ΩB→Ω^fibf : (n : ℕ) (x : _)
                     → isInKer∙ (Ω^fibf→A n) x
                     → isInIm∙ (ΩB→Ω^fibf n) x
  Ker-Ω^fibf→A⊂Im-ΩB→Ω^fibf n x p =
      fst r
    , cong (fst ((fst (Ω^Fibre≃∙⁻ n f)))) (snd r)
    ∙ funExt⁻ (cong fst (Ω^Fibre≃∙sect n f)) x
    where
    r : isInIm∙ (ΩB→fibΩ^f n) (fst (fst (Ω^Fibre≃∙ n f)) x)
    r = Ker-fibΩ^f→A⊂Im-ΩB→fibΩ^f n (fst (fst (Ω^Fibre≃∙ n f)) x) p

  Im-ΩB→Ω^fibf⊂Ker-Ω^fibf→A : (n : ℕ) (x : _)
                     → isInIm∙ (ΩB→Ω^fibf n) x
                     → isInKer∙ (Ω^fibf→A n) x
  Im-ΩB→Ω^fibf⊂Ker-Ω^fibf→A n x =
    uncurry λ p →
      J (λ x _ → isInKer∙ (Ω^fibf→A n) x)
        (cong (fst (fibΩ^f→A n))
          (funExt⁻ (cong fst (Ω^Fibre≃∙retr n f)) _))

  Im-A→B⊂Ker-ΩB→Ω^fibf : (n : ℕ) (x : fst (((Ω^ (suc n)) B)))
                     → isInIm∙ (A→B (suc n)) x
                     → isInKer∙ (ΩB→Ω^fibf n) x
  Im-A→B⊂Ker-ΩB→Ω^fibf n x p =
      cong (fst ((fst (Ω^Fibre≃∙⁻ n f))))
           (Im-A→B⊂Ker-ΩB→fibΩ^f n x p)
    ∙ snd (Ω^Fibre≃∙⁻ n f)

  Ker-ΩB→Ω^fibf⊂Im-A→B : (n : ℕ) (x : fst (((Ω^ (suc n)) B)))
                     → isInKer∙ (ΩB→Ω^fibf n) x
                     → isInIm∙ (A→B (suc n)) x
  Ker-ΩB→Ω^fibf⊂Im-A→B n x p =
    Ker-ΩB→fibΩ^f⊂Im-A→B n x
         (funExt⁻ (cong fst (sym (Ω^Fibre≃∙retr n f))) (ΩB→fibΩ^f n .fst x)
        ∙ cong (fst (fst (Ω^Fibre≃∙ n f))) p
        ∙ snd (Ω^Fibre≃∙ n f))

{- Some useful lemmas for converting the above sequence a
a sequence of homotopy groups -}
module setTruncLemmas {ℓ ℓ' ℓ'' : Level}
  {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
  (n m l : ℕ)
  (f : (Ω ((Ω^ n) A)) →∙ (Ω ((Ω^ m) B)))
  (g : (Ω ((Ω^ m) B)) →∙ (Ω ((Ω^ l) C)))
  (e₁ : IsGroupHom (snd (πGr n A)) (sMap (fst f)) (snd (πGr m B)))
  (e₂ : IsGroupHom (snd (πGr m B)) (sMap (fst g)) (snd (πGr l C))) where

  ker⊂im : ((x : typ (Ω ((Ω^ m) B))) → isInKer∙ g x → isInIm∙ f x)
         → (x : π (suc m) B) → isInKer (_ , e₂) x → isInIm (_  , e₁) x
  ker⊂im ind =
    sElim (λ _ → isSetΠ λ _ → isProp→isSet squash₁)
      λ p ker →
        pRec squash₁
        (λ ker∙ → ∣ ∣ ind p ker∙ .fst ∣₂ , cong ∣_∣₂ (ind p ker∙ .snd) ∣₁ )
        (fun PathIdTrunc₀Iso ker)

  im⊂ker : ((x : typ (Ω ((Ω^ m) B))) → isInIm∙ f x → isInKer∙ g x)
        → (x : π (suc m) B) → isInIm (_  , e₁) x → isInKer (_ , e₂) x
  im⊂ker ind =
    sElim (λ _ → isSetΠ λ _ → isSetPathImplicit)
      λ p →
       pRec (squash₂ _ _)
       (uncurry (sElim (λ _ → isSetΠ λ _ → isSetPathImplicit)
         λ a q → pRec (squash₂ _ _)
                       (λ q → cong ∣_∣₂ (ind p (a , q)))
                       (fun PathIdTrunc₀Iso q)))

{- The long exact sequence of homotopy groups -}
module πLES {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) where
  module Ωs = ΩLES f
  open Ωs renaming (A→B to A→B')

  fib = fibf

  fib→A : (n : ℕ) → GroupHom (πGr n fib) (πGr n A)
  fst (fib→A n) = sMap (fst (Ω^fibf→A (suc n)))
  snd (fib→A n) =
    makeIsGroupHom
      (sElim2 (λ _  _ → isSetPathImplicit)
        λ p q → cong ∣_∣₂ (Ω^fibf→A-pres∙ n p q))

  A→B : (n : ℕ) → GroupHom (πGr n A) (πGr n B)
  fst (A→B n) = sMap (fst (A→B' (suc n)))
  snd (A→B n) =
    makeIsGroupHom
      (sElim2 (λ _  _ → isSetPathImplicit)
        λ g h → cong ∣_∣₂ (Ω^→pres∙ f n g h))

  B→fib : (n : ℕ) → GroupHom (πGr (suc n) B) (πGr n fib)
  fst (B→fib n) = sMap (fst (ΩB→Ω^fibf (suc n)))
  snd (B→fib n) =
    makeIsGroupHom
      (sElim2
        (λ _  _ → isSetPathImplicit)
        λ p q → cong ∣_∣₂ (ΩB→Ω^fibf-pres∙ n p q))

  Ker-A→B⊂Im-fib→A : (n : ℕ) (x : π (suc n) A)
    → isInKer (A→B n) x
    → isInIm (fib→A n) x
  Ker-A→B⊂Im-fib→A n =
    setTruncLemmas.ker⊂im n n n
      (Ω^fibf→A (suc n)) (A→B' (suc n))
      (snd (fib→A n)) (snd (A→B n))
      (Ker-A→B⊂Im-Ω^fibf→A (suc n))

  Im-fib→A⊂Ker-A→B : (n : ℕ) (x : π (suc n) A)
    → isInIm (fib→A n) x
    → isInKer (A→B n) x
  Im-fib→A⊂Ker-A→B n =
    setTruncLemmas.im⊂ker n n n
      (Ω^fibf→A (suc n)) (A→B' (suc n))
      (snd (fib→A n)) (snd (A→B n))
      (Im-Ω^fibf→A⊂Ker-A→B (suc n))

  Ker-fib→A⊂Im-B→fib : (n : ℕ) (x : π (suc n) fib)
    → isInKer (fib→A n) x
    → isInIm (B→fib n) x
  Ker-fib→A⊂Im-B→fib n =
    setTruncLemmas.ker⊂im (suc n) n n
      (ΩB→Ω^fibf (suc n)) (Ω^fibf→A (suc n))
      (snd (B→fib n)) (snd (fib→A n))
      (Ker-Ω^fibf→A⊂Im-ΩB→Ω^fibf (suc n))

  Im-B→fib⊂Ker-fib→A : (n : ℕ) (x : π (suc n) fib)
    → isInIm (B→fib n) x
    → isInKer (fib→A n) x
  Im-B→fib⊂Ker-fib→A n =
    setTruncLemmas.im⊂ker (suc n) n n
      (ΩB→Ω^fibf (suc n)) (Ω^fibf→A (suc n))
      (snd (B→fib n)) (snd (fib→A n))
      (Im-ΩB→Ω^fibf⊂Ker-Ω^fibf→A (suc n))

  Im-A→B⊂Ker-B→fib : (n : ℕ) (x : π (suc (suc n)) B)
    → isInIm (A→B (suc n)) x
    → isInKer (B→fib n) x
  Im-A→B⊂Ker-B→fib n =
    setTruncLemmas.im⊂ker (suc n) (suc n) n
      (A→B' (suc (suc n))) (ΩB→Ω^fibf (suc n))
      (snd (A→B (suc n))) (snd (B→fib n))
      (Im-A→B⊂Ker-ΩB→Ω^fibf (suc n))

  Ker-B→fib⊂Im-A→B : (n : ℕ) (x : π (suc (suc n)) B)
    → isInKer (B→fib n) x
    → isInIm (A→B (suc n)) x
  Ker-B→fib⊂Im-A→B n =
    setTruncLemmas.ker⊂im (suc n) (suc n) n
      (A→B' (suc (suc n))) (ΩB→Ω^fibf (suc n))
      (snd (A→B (suc n))) (snd (B→fib n))
      (Ker-ΩB→Ω^fibf⊂Im-A→B (suc n))

{- We prove that the map Ωⁿ(fib f) → Ωⁿ A indeed is just the map
Ωⁿ fst -}
private
  Ω^fibf→A-ind : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (n : ℕ) (f : A →∙ B)
        → ΩLES.Ω^fibf→A f (suc n) ≡ Ω→ (ΩLES.Ω^fibf→A f n)
  Ω^fibf→A-ind {A = A} {B = B} n f =
      (λ _ → πLES.Ωs.fibΩ^f→A f (suc n)
     ∘∙ ≃∙map (Ω^Fibre≃∙ (suc n) f))
    ∙ →∙Homogeneous≡ (isHomogeneousPath _ _)
      (funExt λ p →
        (λ j → cong fst (Ω→ (≃∙map (Ω^Fibre≃∙ n f)) .fst p))
       ∙ rUnit ((λ i → fst
           (Ω→ (≃∙map (Ω^Fibre≃∙ n f)) .fst p i)))
      ∙ sym (Ω→∘ (πLES.Ωs.fibΩ^f→A f n) (≃∙map (Ω^Fibre≃∙ n f)) p))

Ω^fibf→A≡ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (n : ℕ) (f : A →∙ B)
      → ΩLES.Ω^fibf→A f n ≡ Ω^→ n (fst , refl)
Ω^fibf→A≡ zero f = ΣPathP (refl , (sym (lUnit refl)))
Ω^fibf→A≡ (suc n) f = Ω^fibf→A-ind n f ∙ cong Ω→ (Ω^fibf→A≡ n f)

{- We now get a nice characterisation of the functions in the induced LES
of homotopy groups defined using (Sⁿ →∙ A) -}

π∘∙A→B-PathP : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (n : ℕ) (f : A →∙ B)
  → PathP (λ i → GroupHomπ≅π'PathP A B n i)
           (πLES.A→B f n)
           (π'∘∙Hom n f)
π∘∙A→B-PathP n f =
  toPathP (Σ≡Prop (λ _ → isPropIsGroupHom _ _) (π'∘∙Hom'≡π'∘∙fun n f))

π∘∙fib→A-PathP : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (n : ℕ) (f : A →∙ B)
  → PathP (λ i → GroupHomπ≅π'PathP (ΩLES.fibf f) A n i)
           (πLES.fib→A f n)
           (π'∘∙Hom n (fst , refl))
π∘∙fib→A-PathP {A = A} {B = B} n f =
  toPathP (Σ≡Prop (λ _ → isPropIsGroupHom _ _)
    (cong (transport
      (λ i → (fst (GroupPath _ _)
               (GroupIso→GroupEquiv (π'Gr≅πGr n (ΩLES.fibf f))) (~ i)) .fst
           → (fst (GroupPath _ _)
               (GroupIso→GroupEquiv (π'Gr≅πGr n A)) (~ i)) .fst))
          lem
   ∙ π'∘∙Hom'≡π'∘∙fun n (fst , refl)))
  where
  lem : πLES.fib→A f n .fst ≡ sMap (Ω^→ (suc n) (fst , refl) .fst)
  lem = cong sMap (cong fst (Ω^fibf→A≡ (suc n) f))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --cubical --safe #-}
module CubicalAbsurd where

open import Cubical.Core.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Empty

theWrongThing : 1 + 1 ≡ 3 → ⊥
theWrongThing thatMoney = znots (injSuc (injSuc thatMoney))