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

open import Categories.Category

module Categories.Diagram.Pullback.Properties {o ℓ e} (C : Category o ℓ e) where

open import Function using (_$_)

open import Categories.Category.Cartesian C
open import Categories.Diagram.Pullback C
open import Categories.Diagram.Equalizer C
open import Categories.Object.Product C
open import Categories.Object.Terminal C
open import Categories.Morphism.Reasoning C

private
  open Category C
  variable
    X Y Z : Obj
    f g h i : X ⇒ Y
open HomReasoning

-- pullback from a terminal object is the same as a product
module _ (t : Terminal) where
  open Terminal t

  pullback-⊤⇒product : Pullback (! {X}) (! {Y}) → Product X Y
  pullback-⊤⇒product p = record
    { A×B      = P
    ; π₁       = p₁
    ; π₂       = p₂
    ; ⟨_,_⟩    = λ f g → universal (!-unique₂ {f = ! ∘ f} {g = ! ∘ g})
    ; project₁ = p₁∘universal≈h₁
    ; project₂ = p₂∘universal≈h₂
    ; unique   = λ eq eq′ → ⟺ (unique eq eq′)
    }
    where open Pullback p

  product⇒pullback-⊤ : Product X Y → Pullback (! {X}) (! {Y})
  product⇒pullback-⊤ p = record
    { p₁              = π₁
    ; p₂              = π₂
    ; isPullback = record
      { commute         = !-unique₂
      ; universal       = λ {_ f g} _ → ⟨ f , g ⟩
      ; unique          = λ eq eq′ → ⟺ (unique eq eq′)
      ; p₁∘universal≈h₁ = project₁
      ; p₂∘universal≈h₂ = project₂
      }
    }
    where open Product p

-- pullbacks respect _≈_
module _ (p : Pullback f g) where
  open Pullback p

  pullback-resp-≈ : f ≈ h → g ≈ i → Pullback h i
  pullback-resp-≈ eq eq′ = record
    { p₁              = p₁
    ; p₂              = p₂
    ; isPullback = record
      { commute         = ∘-resp-≈ˡ (⟺ eq) ○ commute ○ ∘-resp-≈ˡ eq′
      ; universal       = λ eq″ → universal (∘-resp-≈ˡ eq ○ eq″ ○ ∘-resp-≈ˡ (⟺ eq′))
      ; unique          = unique
      ; p₁∘universal≈h₁ = p₁∘universal≈h₁
      ; p₂∘universal≈h₂ = p₂∘universal≈h₂
      }
    }

-- Some facts about pulling back along identity
module _ (p : Pullback id f) where
  open Pullback p

  -- This is a more subtle way of saying that 'p₂ ≈ id', without involving heterogenous equality.
  pullback-identity : universal id-comm-sym ∘ p₂ ≈ id
  pullback-identity = begin
    universal Basic.id-comm-sym ∘ p₂ ≈⟨ unique ( pullˡ p₁∘universal≈h₁ ) (pullˡ p₂∘universal≈h₂)  ⟩
    universal eq                     ≈⟨ universal-resp-≈ (⟺ commute ○ identityˡ) identityˡ ⟩
    universal commute                ≈˘⟨ Pullback.id-unique p ⟩
    id ∎
    where
      eq : id ∘ f ∘ p₂ ≈ f ∘ id ∘ p₂
      eq = begin
        (id ∘ f ∘ p₂) ≈⟨ elimˡ Equiv.refl ⟩
        (f ∘ p₂)      ≈˘⟨ refl⟩∘⟨ identityˡ ⟩
        (f ∘ id ∘ p₂) ∎

module _ (pullbacks : ∀ {X Y Z} (f : X ⇒ Z) (g : Y ⇒ Z) → Pullback f g)
         (cartesian : Cartesian) where
  open Cartesian cartesian

  pullback×cartesian⇒equalizer : Equalizer f g
  pullback×cartesian⇒equalizer {f = f} {g = g} = record
    { arr       = p.p₁
    ; equality  = equality
    ; equalize  = λ {_ h} eq → p.universal $ begin
      ⟨ f , g ⟩ ∘ h               ≈⟨ ⟨⟩∘ ⟩
      ⟨ f ∘ h , g ∘ h ⟩           ≈˘⟨ ⟨⟩-cong₂ identityˡ (identityˡ ○ eq) ⟩
      ⟨ id ∘ f ∘ h , id ∘ f ∘ h ⟩ ≈˘⟨ ⟨⟩∘ ⟩
      ⟨ id , id ⟩ ∘ f ∘ h         ∎
    ; universal = ⟺ p.p₁∘universal≈h₁
    ; unique    = λ eq → p.unique (⟺ eq)
                                  (⟺ (pullˡ eq′) ○ ⟺ (∘-resp-≈ʳ eq))
    }
    where p : Pullback ⟨ f , g ⟩ ⟨ id , id ⟩
          p = pullbacks _ _
          module p = Pullback p
          eq : ⟨ f ∘ p.p₁ , g ∘ p.p₁ ⟩ ≈ ⟨ p.p₂ , p.p₂ ⟩
          eq = begin
            ⟨ f ∘ p.p₁ , g ∘ p.p₁ ⟩      ≈˘⟨ ⟨⟩∘ ⟩
            ⟨ f , g ⟩ ∘ p.p₁             ≈⟨ p.commute ⟩
            ⟨ id , id ⟩ ∘ p.p₂           ≈⟨ ⟨⟩∘ ⟩
            ⟨ id ∘ p.p₂ , id ∘ p.p₂ ⟩    ≈⟨ ⟨⟩-cong₂ identityˡ identityˡ ⟩
            ⟨ p.p₂ , p.p₂ ⟩              ∎
          eq′ : f ∘ p.p₁ ≈  p.p₂
          eq′ = begin
            f ∘ p.p₁                     ≈˘⟨ project₁ ⟩
            π₁ ∘ ⟨ f ∘ p.p₁ , g ∘ p.p₁ ⟩ ≈⟨ refl⟩∘⟨ eq ⟩
            π₁ ∘ ⟨ p.p₂ , p.p₂ ⟩         ≈⟨ project₁ ⟩
            p.p₂                         ∎
          equality : f ∘ p.p₁ ≈ g ∘ p.p₁
          equality = begin
            f ∘ p.p₁                     ≈⟨ eq′ ⟩
            p.p₂                         ≈˘⟨ project₂ ⟩
            π₂ ∘ ⟨ p.p₂ , p.p₂ ⟩         ≈˘⟨ refl⟩∘⟨ eq ⟩
            π₂ ∘ ⟨ f ∘ p.p₁ , g ∘ p.p₁ ⟩ ≈⟨ project₂ ⟩
            g ∘ p.p₁                     ∎


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)

open import Relation.Binary

import MultiSorted.Context as MSC
import MultiSorted.AlgebraicTheory as MST
import SingleSorted.AlgebraicTheory

module MultiSorted.FromSingleSorted
  (Σ : SingleSorted.AlgebraicTheory.Signature)
  (𝒯 : SingleSorted.AlgebraicTheory.Theory lzero Σ)
  where

module SS where
  open SingleSorted.AlgebraicTheory public
  open SingleSorted.AlgebraicTheory.Signature Σ public

data 𝒜 : Set where
  A : 𝒜

single-sort : ∀ (X : 𝒜) → X ≡ A
single-sort A = refl

-- We have to transform the following constructions from the single sorted to the multi sorted setting
-- contexts, variables, operations, terms, equations, theory

singleSortedToMultiSortedContext : ∀ {𝓈} {Sort : Set 𝓈} (X : Sort) → SS.Context → MSC.Context Sort
singleSortedToMultiSortedContext _ SS.ctx-empty = MSC.Context.ctx-empty
singleSortedToMultiSortedContext X SS.ctx-slot = MSC.Context.ctx-slot X
singleSortedToMultiSortedContext X (SS.ctx-concat Γ Δ) =
  MSC.Context.ctx-concat (singleSortedToMultiSortedContext X Γ) (singleSortedToMultiSortedContext X Δ)

multiSortedToSingleSortedContext : ∀ {𝓈} {Sort : Set 𝓈} (X : Sort) → MSC.Context Sort → SS.Context
multiSortedToSingleSortedContext X MSC.ctx-empty = SS.ctx-empty
multiSortedToSingleSortedContext X (MSC.ctx-slot x) = SS.ctx-slot
multiSortedToSingleSortedContext X (MSC.ctx-concat Γ Δ) =
  SS.ctx-concat (multiSortedToSingleSortedContext X Γ) (multiSortedToSingleSortedContext X Δ)

S : MST.Signature
S = record { sort = 𝒜
           ; oper = SS.Signature.oper Σ
           ; oper-arity = λ{ f → singleSortedToMultiSortedContext A (SS.Signature.oper-arity Σ f) }
           ; oper-sort = λ{ f → A }
           }

module MS where
  open MST.Signature S public

singleSortedToMultiSortedVar : ∀ {Γ : SS.Context}
  → SS.var Γ  → MS.var (singleSortedToMultiSortedContext A Γ)
singleSortedToMultiSortedVar SS.var-var = MS.var-var
singleSortedToMultiSortedVar (SS.var-inl x) = MS.var-inl (singleSortedToMultiSortedVar x)
singleSortedToMultiSortedVar (SS.var-inr x) = MS.var-inr (singleSortedToMultiSortedVar x)

coerce : ∀ {Γ : MS.Context} {X} {Y} → MS.Term Γ X → MS.Term Γ Y
coerce {Γ} {A} {A} t = subst (MS.Term Γ) refl t

argToArg : ∀ {Δ : SS.Context} → MS.arg (singleSortedToMultiSortedContext A Δ) → SS.arg Δ
argToArg {SS.ctx-slot} i = SS.var-var
argToArg {SS.ctx-concat Δ Γ} (MSC.var-inl i) = SS.var-inl (argToArg i)
argToArg {SS.ctx-concat Δ Γ} (MSC.var-inr i) = SS.var-inr (argToArg i)

singleSortedToMultiSortedTerm : ∀ {Γ : SS.Context}
  → SS.Term Γ
  → MS.Term (singleSortedToMultiSortedContext A Γ) A
singleSortedToMultiSortedTerm {Γ} (SS.tm-var x) = coerce (MS.tm-var (singleSortedToMultiSortedVar x))
singleSortedToMultiSortedTerm (SS.tm-oper f ts) = MS.tm-oper f
  (λ i → coerce (singleSortedToMultiSortedTerm (ts (argToArg i))))

singleSortedToMultiSortedEquation : SS.Equation → MST.Equation S
singleSortedToMultiSortedEquation eq =
  MST.make-eq
    (singleSortedToMultiSortedContext A (SS.Equation.eq-ctx eq))
    A
    (singleSortedToMultiSortedTerm (SS.Equation.eq-lhs eq))
    (singleSortedToMultiSortedTerm (SS.Equation.eq-rhs eq))

𝓣 : MST.Theory lzero S
𝓣 = record { ax = SS.Theory.ax 𝒯
            ; ax-eq = λ{ a → singleSortedToMultiSortedEquation (SS.Theory.ax-eq 𝒯 a)}
            }

ext: agda

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
------------------------------------------------------------------------
-- Polymorphic and iso-recursive types
------------------------------------------------------------------------

module SystemF.Type where

open import Data.Fin using (Fin; zero; suc)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Nat using (ℕ; _+_)
open import Data.Star using (Star; ε; _◅_)
open import Data.Vec using (Vec; []; _∷_; lookup; map)
open import Relation.Binary.PropositionalEquality as PropEq
  using (refl; _≡_; cong; cong₂; sym)
open PropEq.≡-Reasoning

------------------------------------------------------------------------
-- Polymorphic and iso-recursive types

infixr 7 _→'_

-- Types with up to n free type variables
data Type (n : ℕ) : Set where
  var  : Fin n           → Type n   -- type variable
  _→'_ : Type n → Type n → Type n   -- arrow/function type
  ∀'   : Type (1 + n)    → Type n   -- universal type
  μ    : Type (1 + n)    → Type n   -- recursive type

------------------------------------------------------------------------
-- Substitutions in types

module TypeSubst where
  module TypeApp {T : ℕ → Set} (l : Lift T Type) where
    open Lift l hiding (var)

    infixl 8 _/_

    -- Apply a substitution to a type
    _/_ : ∀ {m n} → Type m → Sub T m n → Type n
    var x    / σ = lift (lookup σ x)
    (a →' b) / σ = (a / σ) →' (b / σ)
    ∀' a     / σ = ∀' (a / σ ↑)
    μ a      / σ = μ (a / σ ↑)

    open Application (record { _/_ = _/_ }) using (_/✶_)

    -- Helper lemmas relating application of simple substitutions (_/_)
    -- to application of sequences of substititions (_/✶_).  These are
    -- used to derive other (more general) lemmas below.

    →'-/✶-↑✶ : ∀ k {m n a b} (ρs : Subs T m n) →
               (a →' b) /✶ ρs ↑✶ k ≡ (a /✶ ρs ↑✶ k) →' (b /✶ ρs ↑✶ k)
    →'-/✶-↑✶ k ε        = refl
    →'-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (→'-/✶-↑✶ k ρs) refl

    ∀'-/✶-↑✶ : ∀ k {m n a} (ρs : Subs T m n) →
               (∀' a) /✶ ρs ↑✶ k ≡ ∀' (a /✶ ρs ↑✶ (1 + k))
    ∀'-/✶-↑✶ k ε        = refl
    ∀'-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (∀'-/✶-↑✶ k ρs) refl

    μT-/✶-↑✶ : ∀ k {m n a} (ρs : Subs T m n) →
               (μ a) /✶ ρs ↑✶ k ≡ μ (a /✶ ρs ↑✶ (1 + k))
    μT-/✶-↑✶ k ε        = refl
    μT-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (μT-/✶-↑✶ k ρs) refl

  -- Defining the abstract members var and _/_ in
  -- Data.Fin.Substitution.TermSubst for T = Type gives us access to a
  -- number of (generic) substitution functions out-of-the-box.
  typeSubst : TermSubst Type
  typeSubst = record { var = var; app = TypeApp._/_ }

  open TermSubst typeSubst public hiding (var)

  weaken↑ : ∀ {n} → Type (1 + n) → Type (2 + n)
  weaken↑ a = a / wk ↑

  infix 8 _[/_]

  -- Shorthand for single-variable type substitutions
  _[/_] : ∀ {n} → Type (1 + n) → Type n → Type n
  a [/ b ] = a / sub b

-- Substitution lemmas.
module TypeLemmas where

  -- FIXME: The following lemmas are generic and should go somewhere
  -- else.
  module AdditionalLemmas {T} (lemmas : TermLemmas T) where
    open TermLemmas lemmas

    -- Weakening commutes with single-variable substitution
    weaken-sub : ∀ {n} (a : T (1 + n)) (b : T n) →
                 weaken (a / sub b) ≡ a / wk ↑ / sub (weaken b)
    weaken-sub a b = begin
      weaken (a / sub b)        ≡⟨ sym (/-wk′ (a / sub b)) ⟩
      a / sub b / wk            ≡⟨ sub-commutes a ⟩
      a / wk ↑ / sub (b / wk)   ≡⟨ cong (λ c → a / wk ↑ / sub c) (/-wk′ b) ⟩
      a / wk ↑ / sub (weaken b) ∎
      where /-wk′ : ∀ {n} (a : T n) → a / wk ≡ weaken a
            /-wk′ a = /-wk {t = a}

    -- Weakening commutes with reverse composition of substitutions.
    map-weaken-⊙ : ∀ {m n k} (σ₁ : Sub T m n) (σ₂ : Sub T n k) →
                   map weaken (σ₁ ⊙ σ₂) ≡ (map weaken σ₁) ⊙ (σ₂ ↑)
    map-weaken-⊙ σ₁ σ₂ = begin
      map weaken (σ₁ ⊙ σ₂)     ≡⟨ map-weaken ⟩
      (σ₁ ⊙ σ₂) ⊙ wk           ≡⟨ sym ⊙-assoc ⟩
      σ₁ ⊙ (σ₂ ⊙ wk)           ≡⟨ cong (λ σ₂ → σ₁ ⊙ σ₂) ⊙-wk ⟩
      σ₁ ⊙ (wk ⊙ (σ₂ ↑))       ≡⟨ ⊙-assoc ⟩
      (σ₁ ⊙ wk) ⊙ (σ₂ ↑)       ≡⟨ cong (λ σ₁ → σ₁ ⊙ (σ₂ ↑)) (sym map-weaken) ⟩
      (map weaken σ₁) ⊙ (σ₂ ↑) ∎

  -- Giving concrete definitions (i.e. proofs) for the abstract members
  -- (i.e. lemmas) in Data.Fin.Substitution.Lemmas.TermLemmas for T =
  -- Type gives us access to a number of (generic) substitutions lemmas
  -- out-of-the-box.
  typeLemmas : TermLemmas Type
  typeLemmas = record
    { termSubst = TypeSubst.typeSubst
    ; app-var   = refl
    ; /✶-↑✶     = Lemma./✶-↑✶
    }
    where
    module Lemma {T₁ T₂} {lift₁ : Lift T₁ Type} {lift₂ : Lift T₂ Type} where

      open TypeSubst
      open Lifted lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
      open Lifted lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)

      /✶-↑✶ : ∀ {m n} (ρs₁ : Subs T₁ m n) (ρs₂ : Subs T₂ m n) →
              (∀ k x → var x /✶₁ ρs₁ ↑✶₁ k ≡ var x /✶₂ ρs₂ ↑✶₂ k) →
               ∀ k t → t     /✶₁ ρs₁ ↑✶₁ k ≡ t     /✶₂ ρs₂ ↑✶₂ k
      /✶-↑✶ ρs₁ ρs₂ hyp k (var x) = hyp k x
      /✶-↑✶ ρs₁ ρs₂ hyp k (a →' b) = begin
          (a →' b) /✶₁ ρs₁ ↑✶₁ k
        ≡⟨ TypeApp.→'-/✶-↑✶ _ k ρs₁ ⟩
          (a /✶₁ ρs₁ ↑✶₁ k) →' (b /✶₁ ρs₁ ↑✶₁ k)
        ≡⟨ cong₂ _→'_ (/✶-↑✶ ρs₁ ρs₂ hyp k a) (/✶-↑✶ ρs₁ ρs₂ hyp k b) ⟩
          (a /✶₂ ρs₂ ↑✶₂ k) →' (b /✶₂ ρs₂ ↑✶₂ k)
        ≡⟨ sym (TypeApp.→'-/✶-↑✶ _ k ρs₂) ⟩
          (a →' b) /✶₂ ρs₂ ↑✶₂ k
        ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (∀' a) = begin
        (∀' a) /✶₁ ρs₁ ↑✶₁ k        ≡⟨ TypeApp.∀'-/✶-↑✶ _ k ρs₁ ⟩
        ∀' (a /✶₁ ρs₁ ↑✶₁ (1 + k))  ≡⟨ cong ∀' (/✶-↑✶ ρs₁ ρs₂ hyp (1 + k) a) ⟩
        ∀' (a /✶₂ ρs₂ ↑✶₂ (1 + k))  ≡⟨ sym (TypeApp.∀'-/✶-↑✶ _ k ρs₂) ⟩
        (∀' a) /✶₂ ρs₂ ↑✶₂ k        ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (μ a) = begin
        (μ a) /✶₁ ρs₁ ↑✶₁ k         ≡⟨ TypeApp.μT-/✶-↑✶ _ k ρs₁ ⟩
        μ (a /✶₁ ρs₁ ↑✶₁ (1 + k))   ≡⟨ cong μ (/✶-↑✶ ρs₁ ρs₂ hyp (1 + k) a) ⟩
        μ (a /✶₂ ρs₂ ↑✶₂ (1 + k))   ≡⟨ sym (TypeApp.μT-/✶-↑✶ _ k ρs₂) ⟩
        (μ a) /✶₂ ρs₂ ↑✶₂ k         ∎

  open TermLemmas typeLemmas public hiding (var)
  open TypeSubst public using (_[/_]; _/Var_; weaken↑; module Lifted)

  -- The above lemma /✶-↑✶ specialized to single substitutions
  /-↑⋆ : ∀ {T₁ T₂} {lift₁ : Lift T₁ Type} {lift₂ : Lift T₂ Type} →
         let open Lifted lift₁ using () renaming (_↑⋆_ to _↑⋆₁_; _/_ to _/₁_)
             open Lifted lift₂ using () renaming (_↑⋆_ to _↑⋆₂_; _/_ to _/₂_)
         in
         ∀ {n k} (ρ₁ : Sub T₁ n k) (ρ₂ : Sub T₂ n k) →
         (∀ i x → var x /₁ ρ₁ ↑⋆₁ i ≡ var x /₂ ρ₂ ↑⋆₂ i) →
          ∀ i a → a /₁ ρ₁ ↑⋆₁ i ≡ a /₂ ρ₂ ↑⋆₂ i
  /-↑⋆ ρ₁ ρ₂ hyp i a = /✶-↑✶ (ρ₁ ◅ ε) (ρ₂ ◅ ε) hyp i a

  open AdditionalLemmas typeLemmas public

------------------------------------------------------------------------
-- Encoding/translation of additional type operators

module TypeOperators where
  open TypeLemmas hiding (id)

  -- Type of the polymorphic identity
  id : ∀ {n} → Type n
  id = ∀' ((var zero) →' (var zero))

  -- Bottom/initial/zero type
  ⊥ : ∀ {n} → Type n
  ⊥ = ∀' (var zero)

  -- Top/terminal/unit type
  ⊤ : ∀ {n} → Type n
  ⊤ = id

  -- Existential type
  ∃ : ∀ {n} → Type (1 + n) → Type n
  ∃ a = ∀' (∀' (weaken↑ a →' var (suc zero)) →' var zero)

  infixr 7 _→ⁿ_

  -- n-ary function type
  _→ⁿ_ : ∀ {n k} → Vec (Type n) k → Type n → Type n
  []       →ⁿ z = z
  (a ∷ as) →ⁿ z = as →ⁿ a →' z

  -- Record/finite tuple
  rec : ∀ {n k} → Vec (Type n) k → Type n
  rec []       = ⊤
  rec (a ∷ as) = ∀' ((map weaken (a ∷ as) →ⁿ var zero) →' var zero)

------------------------------------------------------------------------
-- Lemmas about encoded type operators

module TypeOperatorLemmas where
  open TypeOperators
  open TypeLemmas hiding (_/_; id)

  module TypeOperatorAppLemmas {T} (l : Lift T Type) where
    open TypeSubst.TypeApp l

    -- Type substitution commutes with the translation of of n-ary
    -- function types
    /-→ⁿ : ∀ {m n k} (as : Vec (Type m) k) (b : Type m) (σ : Sub T m n) →
           (as →ⁿ b) / σ ≡ map (λ a → a / σ) as →ⁿ b / σ
    /-→ⁿ []       _ _ = refl
    /-→ⁿ (a ∷ as) b σ = /-→ⁿ as (a →' b) σ

    -- FIXME: Write similar lemmas for the remaining type operators

  private
    module WeakeningLemmas where
      open TypeOperatorAppLemmas TypeSubst.varLift

      -- Weakening commutes with the translation of of n-ary function
      -- types
      weaken-→ⁿ : ∀ {n k} (as : Vec (Type n) k) (b : Type n) →
                  weaken (as →ⁿ b) ≡ map weaken as →ⁿ weaken b
      weaken-→ⁿ as b = /-→ⁿ as b VarSubst.wk

      -- FIXME: Write similar lemmas for the remaining type operators

  open TypeOperatorAppLemmas TypeSubst.termLift public
  open WeakeningLemmas public

max_stars_repo_name: sstucki/system-f-agda

max_issues_repo_name: sstucki/system-f-agda

max_forks_repo_name: sstucki/system-f-agda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Universe {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Weakening as Lwk
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance as Irr
open import Definition.Typed.Properties
open import Definition.LogicalRelation.Properties.MaybeEmb
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Properties.Reduction
open import Definition.LogicalRelation.Properties.Conversion
open import Tools.Product
import Tools.PropositionalEquality as PE
open import Tools.Empty using (⊥; ⊥-elim)

import Data.Fin as Fin
import Data.Nat as Nat

Ugen : ∀ {Γ rU l} → (⊢Γ : ⊢ Γ) →  Γ ⊩⟨ next l ⟩ Univ rU l ^ [ ! , next l ]
Ugen {Γ} {rU} {⁰} ⊢Γ = Uᵣ′ (Univ rU ⁰) (ι ¹) rU ⁰ emb< PE.refl ((idRed:*: (Ugenⱼ ⊢Γ)))
Ugen {Γ} {rU} {¹} ⊢Γ = Uᵣ′ (Univ rU ¹) ∞ rU ¹ ∞< PE.refl (idRed:*: (Uⱼ ⊢Γ))

U-Relevance-Level : ∀ {l ll Γ A} ([U] : Γ ⊩⟨ l ⟩U A ^ ll) → Relevance × Level
U-Relevance-Level (noemb (Uᵣ r l′ l< eq d)) =  r , l′
U-Relevance-Level (emb x X) = U-Relevance-Level X

univRedTerm : ∀ {Γ r l u t ti}
        → Γ ⊢ Univ r l ⇒ u ∷ t ^ ti
        → ⊥
univRedTerm (conv d′ A≡t) = univRedTerm d′

univRed* : ∀ {Γ r l r′ l′ ti}
         → Γ ⊢ Univ r l ⇒* Univ r′ l′ ^ ti
         → (r PE.≡ r′) × (l PE.≡ l′)
univRed* (id x) = PE.refl , PE.refl
univRed* (univ x ⇨ D) = ⊥-elim (univRedTerm x)

-- Reducible terms of type U are reducible types.
univEq : ∀ {l Γ A r l′ ll′}
       → ([U] : Γ ⊩⟨ l ⟩ Univ r l′ ^ [ ! , ll′ ] )
       → Γ ⊩⟨ l ⟩ A ∷ Univ r l′ ^ [ ! , ll′ ] / [U]
       → Γ ⊩⟨ ι l′ ⟩ A ^ [ r , ι l′ ]
univEq {ι ⁰} {Γ} {A} {r} {l′} (Uᵣ (Uᵣ r₁ l′₁ () eq [[ ⊢A , ⊢B , D ]])) (Uₜ K d₁ typeK K≡K [t])
univEq {ι ¹} {Γ} {A} {r} {l′} (Uᵣ (Uᵣ r₁ ⁰ emb< eq [[ ⊢A , ⊢B , D ]])) (Uₜ K d₁ typeK K≡K [t]) =
  let
    ⊢Γ = wf ⊢A
    r≡r₁ , l′≡l′₁ = univRed* D
    [t]′ : Γ ⊩⟨ ι ⁰ ⟩ A ^ [ r₁ , ι ⁰ ]
    [t]′ = PE.subst (λ X → Γ ⊩⟨ _ ⟩ X ^ [ _ , _ ])
      (Definition.Untyped.Properties.wk-id A) ([t] Definition.Typed.Weakening.id ⊢Γ)
  in
  PE.subst₂ (λ X Y → Γ ⊩⟨ ι Y ⟩ A ^ [ X , ι Y ]) (PE.sym r≡r₁) (PE.sym l′≡l′₁) [t]′
univEq {∞} {Γ} {A} {r} {l′} (Uᵣ (Uᵣ r₁ ¹ _ eq [[ ⊢A , ⊢B , D ]])) (Uₜ K d₁ typeK K≡K [t]) =
  let
    ⊢Γ = wf ⊢A
    r≡r₁ , l′≡l′₁ = univRed* D
    [t]′ : Γ ⊩⟨ ι ¹ ⟩ A ^ [ r₁ , ι ¹ ]
    [t]′ = PE.subst (λ X → Γ ⊩⟨ _ ⟩ X ^ [ _ , _ ])
      (Definition.Untyped.Properties.wk-id A) ([t] Definition.Typed.Weakening.id ⊢Γ)
  in
  PE.subst₂ (λ X Y → Γ ⊩⟨ ι Y ⟩ A ^ [ X , ι Y ]) (PE.sym r≡r₁) (PE.sym l′≡l′₁) [t]′
univEq (ℕᵣ [[ ⊢A , ⊢B , univ x ⇨ D ]]) [A] = ⊥-elim (univRedTerm x)
univEq (ne′ K [[ ⊢A , ⊢B , univ x ⇨ D ]] neK K≡K) [A] = ⊥-elim (univRedTerm x)
univEq (Πᵣ′ rF lF lG _ _ F G [[ ⊢A , ⊢B , univ x ⇨ D ]] ⊢F ⊢G A≡A [F] [G] G-ext) [A] =
  ⊥-elim (univRedTerm x)
univEq {ι ¹} (emb _ [U]′) [A] = univEq [U]′ [A]
univEq {∞} (emb _ [U]′) [A] = univEq [U]′ [A]

univEqGen : ∀ {Γ UA A l′}
       → ([U] : ((next l′) LogRel.⊩¹U logRelRec (next l′) ^ Γ) UA (next l′))
       → Γ ⊩⟨ next l′ ⟩ A ∷ UA ^ [ ! , next l′ ] / Uᵣ [U]
       → Γ ⊩⟨ ι l′ ⟩ A ^ [ LogRel._⊩¹U_^_.r [U] , ι l′ ]
univEqGen {Γ} {UA} {A} {l′} [UA] [A] =
  let (Uᵣ r l′₁ l< e [[ ⊢A , ⊢B , D ]]) = [UA]
      [U] = Ugen {l = l′} (wf ⊢A)
      [UA]' , [UAeq] = redSubst* (PE.subst (λ X →  Γ ⊢ UA ⇒* Univ r X ^ [ ! , next X ]) (next-inj e) D) [U]
  in univEq [U] (convTerm₁ {t = A} [UA]' [U] [UAeq] (irrelevanceTerm (Uᵣ [UA]) [UA]' [A]))

univ⊩ : ∀ {A Γ rU lU lU' l}
        ([U] : Γ ⊩⟨ l ⟩ Univ rU lU ^ [ ! , lU' ])
      → Γ ⊩⟨ l ⟩ A ∷ Univ rU lU ^ [ ! , lU' ] / [U]
      → Γ ⊩⟨ ι lU ⟩ A ^ [ rU , ι lU ]
univ⊩ {lU = lU} {l = l} [U] [A] = irrelevance-≤ (≡is≤ PE.refl) (univEq [U] [A])

univEqTerm : ∀ {Γ A t r l′ ll′}
       → ([U] : Γ ⊩⟨ ∞ ⟩ Univ r l′ ^ [ ! , ll′ ] )
       → ([A] : Γ ⊩⟨ ∞ ⟩ A ∷ Univ r l′ ^ [ ! , ll′ ] / [U])
       → Γ ⊩⟨ ∞ ⟩ t ∷ A ^ [ r , ι l′ ] / maybeEmb (univ⊩ [U] [A])
       → Γ ⊩⟨ ι l′ ⟩ t ∷ A ^ [ r , ι l′ ] / univEq [U] [A]
univEqTerm {Γ} {A} {t} {r} {⁰} [U] [A] [t] = [t]
univEqTerm {Γ} {A} {t} {r} {¹} [U] [A] [t] = [t]

-- Helper function for reducible term equality of type U for specific type derivations.
univEqEq′ : ∀ {l ll l′ Γ X A B} ([U] : Γ ⊩⟨ l ⟩U X ^ ll) →
            let r = toTypeInfo (U-Relevance-Level [U])
            in
              ([A] : Γ ⊩⟨ l′ ⟩ A ^ r)
              → Γ ⊩⟨ l ⟩ A ≡ B ∷ X ^ [ ! , ll ] / U-intr [U]
              → Γ ⊩⟨ l′ ⟩ A ≡ B  ^ r / [A]
univEqEq′ {l} {ll} {l″} {Γ} {X} {A} {B} (noemb (Uᵣ r l′ l< eq [[ ⊢A , ⊢B , D ]])) [A]
          (Uₜ₌ (Uₜ K d typeK K≡K [t]) [u] A≡B [t≡u]) =
  let ⊢Γ = wf ⊢A in
  irrelevanceEq″ (Definition.Untyped.Properties.wk-id A) (Definition.Untyped.Properties.wk-id B) PE.refl PE.refl
    (emb l< ([t] Definition.Typed.Weakening.id ⊢Γ)) [A]
    ([t≡u] Definition.Typed.Weakening.id ⊢Γ)
univEqEq′ (emb emb< X) [A] [A≡B] = univEqEq′ X [A] [A≡B]
univEqEq′ (emb ∞< X) [A] [A≡B] = univEqEq′ X [A] [A≡B]

UnivNotℕ : ∀ {Γ r ll} →  Γ ⊩ℕ Univ r ll → ⊥
UnivNotℕ {ll = ⁰} [[ ⊢A , ⊢B , D ]] = U≢ℕ (whrDet* (id (univ (univ 0<1 (wf ⊢A))) , Uₙ) (D , ℕₙ))
UnivNotℕ {ll = ¹} [[ ⊢A , ⊢B , D ]] = U≢ℕ (whrDet* (id (Uⱼ (wf ⊢A)) , Uₙ) (D , ℕₙ))

UnivNotΠ : ∀ {Γ r r' lΠ l ll} → (l LogRel.⊩¹Π logRelRec l ^[ Γ , Univ r ll ]) r' lΠ → ⊥
UnivNotΠ {ll = ⁰} (Πᵣ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) = U≢Π (whrDet* (id (univ (univ 0<1 (wf ⊢F))) , Uₙ) (red D , Πₙ))
UnivNotΠ {ll = ¹} (Πᵣ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) = U≢Π (whrDet* (id (Uⱼ (wf ⊢F)) , Uₙ) (red D , Πₙ))

U-Relevance-Level-eq : ∀ {l Γ r ll ll'} ([U] : Γ ⊩⟨ l ⟩ Univ r ll ^ [ ! , ll' ]) → U-Relevance-Level (U-elim [U]) PE.≡ (r , ll)
U-Relevance-Level-eq {ll = ⁰} (Uᵣ (Uᵣ r ⁰ l< eq d)) = ×-eq (Univ-PE-injectivity (whrDet* (red d , Uₙ) (id (univ (univ 0<1 (wf (_⊢_:⇒*:_^_.⊢A d)))) , Uₙ)))
U-Relevance-Level-eq {ll = ¹} (Uᵣ (Uᵣ r ⁰ l< eq d)) = let _ , X = (Univ-PE-injectivity (whrDet* (red d , Uₙ) (id (Uⱼ (wf (_⊢_:⇒*:_^_.⊢A d))) , Uₙ))) in ⊥-elim (⁰≢¹ X)
U-Relevance-Level-eq {ll = ¹} (Uᵣ (Uᵣ r ¹ l< eq d)) = ×-eq (Univ-PE-injectivity (whrDet* (red d , Uₙ) (id (Uⱼ (wf (_⊢_:⇒*:_^_.⊢A d))) , Uₙ)))
U-Relevance-Level-eq (ℕᵣ X) = ⊥-elim (UnivNotℕ X)
U-Relevance-Level-eq (ne′ K D neK K≡K) = ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
U-Relevance-Level-eq (Πᵣ X) = ⊥-elim (UnivNotΠ X)
U-Relevance-Level-eq {ι ¹} (emb l< (ℕᵣ X)) = ⊥-elim (UnivNotℕ X)
U-Relevance-Level-eq {ι ¹} (emb l< (ne′ K D neK K≡K)) = ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
U-Relevance-Level-eq {ι ¹} (emb l< (Πᵣ X)) = ⊥-elim (UnivNotΠ X)
U-Relevance-Level-eq {∞} {ll = ⁰} (emb ∞< (Uᵣ (Uᵣ r ⁰ l<₁ eq d))) = ×-eq (Univ-PE-injectivity (whrDet* (red d , Uₙ) (id (univ (univ 0<1 (wf (_⊢_:⇒*:_^_.⊢A d)))) , Uₙ)))
U-Relevance-Level-eq {∞} {ll = ¹} (emb ∞< (Uᵣ (Uᵣ r ⁰ l<₁ eq d))) = let _ , X = (Univ-PE-injectivity (whrDet* (red d , Uₙ) (id (Uⱼ (wf (_⊢_:⇒*:_^_.⊢A d))) , Uₙ))) in ⊥-elim (⁰≢¹ X)
U-Relevance-Level-eq {∞} {ll = ¹} (emb ∞< (Uᵣ (Uᵣ r ¹ l<₁ eq d))) = ×-eq (Univ-PE-injectivity (whrDet* (red d , Uₙ) (id (Uⱼ (wf (_⊢_:⇒*:_^_.⊢A d))) , Uₙ)))
U-Relevance-Level-eq {∞} (emb {l′ = ι ¹} l< (ℕᵣ X)) = ⊥-elim (UnivNotℕ X)
U-Relevance-Level-eq {∞} (emb {l′ = ι ¹} l< (ne′ K D neK K≡K)) = ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
U-Relevance-Level-eq {∞} (emb {l′ = ι ¹} l< (Πᵣ x)) = ⊥-elim (UnivNotΠ x)
U-Relevance-Level-eq {∞} (emb {l′ = ι ¹} l< (emb {l′ = ι ⁰} emb< (ℕᵣ x))) = ⊥-elim (UnivNotℕ x)
U-Relevance-Level-eq {∞} (emb {l′ = ι ¹} l< (emb {l′ = ι ⁰} emb< (ne′ K D neK K≡K))) = ⊥-elim (U≢ne neK (whnfRed* (red D) Uₙ))
U-Relevance-Level-eq {∞} (emb {l′ = ι ¹} l< (emb {l′ = ι ⁰} emb< (Πᵣ x))) = ⊥-elim (UnivNotΠ x)

helper-eq : ∀ {l Γ A B r r'} {[A] : Γ ⊩⟨ l ⟩ A ^ r} (e : r PE.≡ r' ) → Γ ⊩⟨ l ⟩ A ≡ B ^ r' / (PE.subst _ e [A]) → Γ ⊩⟨ l ⟩ A ≡ B ^ r / [A]
helper-eq PE.refl X = X

-- Reducible term equality of type U is reducible type equality.
univEqEq : ∀ {l l′ Γ A B r ll} ([U] : Γ ⊩⟨ l ⟩ Univ r ll ^ [ ! , next ll ]) ([A] : Γ ⊩⟨ l′ ⟩ A ^ [ r , ι ll ])
         → Γ ⊩⟨ l ⟩ A ≡ B ∷ Univ r ll ^ [ ! , next ll ] / [U]
         → Γ ⊩⟨ l′ ⟩ A ≡ B ^ [ r , ι ll ] / [A]
univEqEq {l} {l′} {Γ} {A} {B} {r} {ll} [U] [A] [A≡B] =
  let [A≡B]′ = irrelevanceEqTerm [U] (U-intr (U-elim [U])) [A≡B]
      X = univEqEq′ (U-elim [U]) (PE.subst (λ r → Γ ⊩⟨ l′ ⟩ A ^ r) (PE.sym (PE.cong toTypeInfo (U-Relevance-Level-eq [U]))) [A]) [A≡B]′
  in helper-eq (PE.sym (PE.cong toTypeInfo (U-Relevance-Level-eq [U]))) X

univEqEqTerm : ∀ {Γ A t u r l′ ll}
             → ([U] : Γ ⊩⟨ ∞ ⟩ Univ r l′ ^ [ ! , ll ] )
             → ([A] : Γ ⊩⟨ ∞ ⟩ A ∷ Univ r l′ ^ [ ! , ll ] / [U])
             → Γ ⊩⟨ ∞ ⟩ t ∷ A ^ [ r , ι l′ ] / maybeEmb (univ⊩ [U] [A])
             → Γ ⊩⟨ ∞ ⟩ t ≡ u ∷ A ^ [ r , ι l′ ] / maybeEmb (univ⊩ [U] [A])
             → Γ ⊩⟨ ι l′ ⟩ t ≡ u ∷ A ^ [ r , ι l′ ] / univEq [U] [A]
univEqEqTerm {Γ} {A} {t} {u} {r} {⁰} [U] [A] [t] [t≡u] = [t≡u]
univEqEqTerm {Γ} {A} {t} {u} {r} {¹} [U] [A] [t] [t≡u] = [t≡u]

un-univEq : ∀ {l Γ A r }
          → ([A] : Γ ⊩⟨ ι l ⟩ A ^ [ r , ι l ])
          → let [U] : Γ ⊩⟨ next l ⟩ Univ r l ^ [ ! , next l ]
                [U] = Ugen (wf (escape [A]))
            in Γ ⊩⟨ next l ⟩ A ∷ Univ r l ^ [ ! , next l ] / [U]
un-univEq {⁰} {Γ} {A} {.!} (ℕᵣ [[ ⊢A , ⊢ℕ , D ]] ) = Uₜ ℕ (un-univ:⇒*: [[ ⊢A , ⊢ℕ , D ]]) ℕₙ (≅ₜ-ℕrefl (wf ⊢A)) (λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (ℕᵣ [[ ⊢A , ⊢ℕ , D ]] ))
un-univEq {⁰} {Γ} {A} {.%} (Emptyᵣ [[ ⊢A , ⊢Empty , D ]]) = Uₜ (Empty ⁰) (un-univ:⇒*: [[ ⊢A , ⊢Empty , D ]]) Emptyₙ (≅ₜ-Emptyrefl (wf ⊢A))
                                                                                (λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (Emptyᵣ [[ ⊢A , ⊢Empty , D ]] ))
un-univEq {⁰} {Γ} {A} {r} (ne′ K D neK K≡K) = Uₜ K (un-univ:⇒*: D) (ne neK) (~-to-≅ₜ K≡K) (λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (ne′ K D neK K≡K))
un-univEq {⁰} {Γ} {A} {r} (Πᵣ′ rF .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F G D ⊢F ⊢G A≡A [F] [G] G-ext) =
  Uₜ (Π F ^ rF ° ⁰ ▹ G ° ⁰ ° ⁰) (un-univ:⇒*: D) Πₙ (≅-un-univ A≡A) λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (Πᵣ′ rF ⁰ ⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F G D ⊢F ⊢G A≡A [F] [G] G-ext)
un-univEq {⁰}  {Γ} {A} {.%} (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) =
  Uₜ (∃ F ▹ G) (un-univ:⇒*: D) ∃ₙ (≅-un-univ A≡A) λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
un-univEq {¹} {Γ} {A} {.!} (Uᵣ (Uᵣ r .⁰ emb< eq [[ ⊢A , ⊢B , D ]])) = Uₜ (Univ r ⁰) (un-univ:⇒*: [[ ⊢A , ⊢B , D ]]) Uₙ (≅-U⁰refl (wf ⊢A))
                                                                              (λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (Uᵣ (Uᵣ r ⁰ emb< eq [[ ⊢A , ⊢B , D ]] )))
un-univEq {¹} {Γ} {A} {.%} (Emptyᵣ [[ ⊢A , ⊢Empty , D ]]) = Uₜ (Empty ¹) (un-univ:⇒*: [[ ⊢A , ⊢Empty , D ]]) Emptyₙ (≅ₜ-Emptyrefl (wf ⊢A))
                                                                                (λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (Emptyᵣ [[ ⊢A , ⊢Empty , D ]] ))
un-univEq {¹} {Γ} {A} {r} (ne′ K D neK K≡K) = Uₜ K (un-univ:⇒*: D) (ne neK) (~-to-≅ₜ K≡K) (λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (ne′ K D neK K≡K))
un-univEq {¹} {Γ} {A} {r} (Πᵣ′ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext) =
  Uₜ (Π F ^ rF ° lF ▹ G ° lG ° ¹ ) (un-univ:⇒*: D) Πₙ (≅-un-univ A≡A) λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (Πᵣ′ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext)
un-univEq {¹} {Γ} {A} {.%} (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) =
  Uₜ (∃ F ▹ G) (un-univ:⇒*: D) ∃ₙ (≅-un-univ A≡A) λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
un-univEq {¹} {Γ} {A} {.%} (emb emb< (Emptyᵣ [[ ⊢A , ⊢Empty , D ]])) = Uₜ (Empty ¹) (un-univ:⇒*: [[ ⊢A , ⊢Empty , D ]]) Emptyₙ (≅ₜ-Emptyrefl (wf ⊢A))
                                                                                (λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (Emptyᵣ [[ ⊢A , ⊢Empty , D ]] ))
un-univEq {¹} {Γ} {A} {r} (emb emb< (ne′ K D neK K≡K)) = Uₜ K (un-univ:⇒*: D) (ne neK) (~-to-≅ₜ K≡K) (λ [ρ] ⊢Δ → Lwk.wk [ρ] ⊢Δ (ne′ K D neK K≡K))
un-univEq {¹} {Γ} {A} {r} (emb emb< (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) =
  Uₜ (Π F ^ rF ° lF ▹ G ° lG ° ¹) (un-univ:⇒*: D) Πₙ (≅-un-univ A≡A) λ [ρ] ⊢Δ → let X = Lwk.wk [ρ] ⊢Δ (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) in maybeEmb′ (<is≤ 0<1) X
un-univEq {¹} {Γ} {A} {.%} (emb emb< (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) =
  Uₜ (∃ F ▹ G) (un-univ:⇒*: D) ∃ₙ (≅-un-univ A≡A) λ [ρ] ⊢Δ → let X = Lwk.wk [ρ] ⊢Δ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) in maybeEmb′ (<is≤ 0<1) X

un-univEqEq-Shape : ∀ {l Γ A B r }
          ([A] : Γ ⊩⟨ ι l ⟩ A ^ [ r , ι l ]) ([B] : Γ ⊩⟨ ι l ⟩ B ^ [ r , ι l ])
          (ShapeA : ShapeView Γ (ι l) (ι l) A B [ r , ι l ] [ r , ι l ] [A] [B])
          ([A≡B] : Γ ⊩⟨ ι l ⟩ A ≡ B ^ [ r , ι l ] / [A])
          → let [U] : Γ ⊩⟨ next l ⟩ Univ r l ^ [ ! , next l ]
                [U] = Ugen (wf (escape [A]))
            in Γ ⊩⟨ next l ⟩ A ≡ B ∷ Univ r l ^ [ ! , next l ] / [U]
un-univEqEq-Shape {⁰} {Γ} {A} {B} {.!} _ _ (ℕᵥ [[ ⊢A , ⊢ℕ , D ]] ℕB) [A≡B] =
  let [A] = ℕᵣ [[ ⊢A , ⊢ℕ , D ]]
      [B] = ℕᵣ [[ redFirst* [A≡B] , ⊢ℕ , [A≡B] ]]
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ⁰} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅ₜ-ℕrefl (wf ⊢A)) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {⁰} {Γ} {A} {B} {.%} _ _ (Emptyᵥ [[ ⊢A , ⊢Empty , D ]] EmptyB) [A≡B] =
  let [A] = Emptyᵣ [[ ⊢A , ⊢Empty , D ]]
      [B] = Emptyᵣ [[ redFirst* [A≡B] , ⊢Empty , [A≡B] ]]
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ⁰} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅ₜ-Emptyrefl (wf ⊢A)) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {⁰} {Γ} {A} {B} {r} _ _  (ne (ne K D neK K≡K) neB) (ne₌ M D′ neM K≡M) =
  let [A] = ne′ K D neK K≡K
      [B] = ne′ M D′ neM (~-trans (~-sym K≡M) K≡M)
      [A≡B] = ne₌ M D′ neM K≡M
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ⁰} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (~-to-≅ₜ K≡M) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {⁰} {Γ} {A} {B} {r} _ _ (Πᵥ (Πᵣ rF .⁰ .⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F G D ⊢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′]) =
  let [A] = Πᵣ′ rF ⁰ ⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = Πᵣ′ rF' ⁰ ⁰ (≡is≤ PE.refl) (≡is≤ PE.refl) F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , rF≡rF , _ , G≡G , _ = Π-PE-injectivity (whrDet* (D′ , Whnf.Πₙ) (red D' , Whnf.Πₙ))
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ⁰} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ Π F ^ rF ° ⁰ ▹ G ° ⁰ ° _ ≅  Π F' ^ rF' ° ⁰ ▹ X ° ⁰ ° _ ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ Π F ^ rF ° ⁰ ▹ G ° ⁰ ° _ ≅  Π X ^ rF' ° ⁰ ▹ G′ ° ⁰ ° _ ^ _ ) F≡F
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° ⁰ ▹ G ° ⁰ ° _ ≅  Π F′ ^ X ° ⁰ ▹ G′ ° ⁰ ° _ ^ _ ) rF≡rF A≡B)))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]

un-univEqEq-Shape {⁰} {Γ} {A} {B} {.%} _ _ (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                        (∃ᵣ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'))
                                    (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let [A] = ∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = ∃ᵣ′ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = ∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , G≡G  = ∃-PE-injectivity (whrDet* (D′ , Whnf.∃ₙ) (red D' , Whnf.∃ₙ))
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ⁰} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ F' ▹ X ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ X ▹ G′ ^ _ ) F≡F A≡B))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {.!} _ _ (Uᵥ (Uᵣ r .⁰ emb< eq d) (Uᵣ r₁ .⁰ emb< eq₁ d₁)) [A≡B] =
  let [A] = Uᵣ (Uᵣ r ⁰ emb< eq d)
      [B] = Uᵣ (Uᵣ r₁ ⁰ emb< eq₁ d₁)
      [[ ⊢A , _ , _ ]] = d
      r≡r , _ = Univ-PE-injectivity (whrDet* (red d₁ , Whnf.Uₙ) ([A≡B] , Whnf.Uₙ))
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (PE.subst (λ X → _ ⊢  Univ r ⁰ ≅ Univ X ⁰ ∷ U _ ^ _ ) (PE.sym r≡r) (≅-U⁰refl (wf ⊢A))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {.%} _ _ (Emptyᵥ [[ ⊢A , ⊢Empty , D ]] EmptyB) [A≡B] =
  let [A] = Emptyᵣ [[ ⊢A , ⊢Empty , D ]]
      [B] = Emptyᵣ [[ redFirst* [A≡B] , ⊢Empty , [A≡B] ]]
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅ₜ-Emptyrefl (wf ⊢A)) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {r} _ _  (ne (ne K D neK K≡K) neB) (ne₌ M D′ neM K≡M) =
  let [A] = ne′ K D neK K≡K
      [B] = ne′ M D′ neM (~-trans (~-sym K≡M) K≡M)
      [A≡B] = ne₌ M D′ neM K≡M
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (~-to-≅ₜ K≡M) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {r} _ _ (Πᵥ (Πᵣ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                        (Πᵣ rF' lF' lG' lF<' lG<' F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'))
                                    (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let [A] = Πᵣ′ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = Πᵣ′ rF' lF' lG' lF<' lG<' F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , rF≡rF , lF≡lF , G≡G , lG≡lG , _ = Π-PE-injectivity (whrDet* (D′ , Whnf.Πₙ) (red D' , Whnf.Πₙ))
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F' ^ rF' ° lF' ▹ X ° lG' ° _ ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π X ^ rF' ° lF' ▹ G′ ° lG' ° _ ^ _ ) F≡F
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ rF' ° lF' ▹ G′ ° X ° _ ^ _ ) lG≡lG
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ rF' ° X ▹ G′ ° lG ° _ ^ _ ) lF≡lF
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ X ° lF ▹ G′ ° lG ° _ ^ _ ) rF≡rF A≡B)))))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {.%} _ _ (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                        (∃ᵣ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'))
                                    (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let [A] = ∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = ∃ᵣ′ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = ∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , G≡G  = ∃-PE-injectivity (whrDet* (D′ , Whnf.∃ₙ) (red D' , Whnf.∃ₙ))
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ F' ▹ X ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ X ▹ G′ ^ _ ) F≡F A≡B))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {.%} _ _ (emb⁰¹ (Emptyᵥ [[ ⊢A , ⊢Empty , D ]] EmptyB)) [A≡B] =
  let [A] = Emptyᵣ [[ ⊢A , ⊢Empty , D ]]
      [B] = Emptyᵣ [[ redFirst* [A≡B] , ⊢Empty , [A≡B] ]]
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅ₜ-Emptyrefl (wf ⊢A)) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {r} _ _ (emb⁰¹ (ne (ne K D neK K≡K) neB)) (ne₌ M D′ neM K≡M) =
  let [A] = ne′ K D neK K≡K
      [B] = ne′ M D′ neM (~-trans (~-sym K≡M) K≡M)
      [A≡B] = ne₌ M D′ neM K≡M
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (~-to-≅ₜ K≡M) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {r} _ _ (emb⁰¹ (Πᵥ (Πᵣ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                        (Πᵣ rF' lF' lG' lF<' lG<' F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext')))
                                    (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let [A] = Πᵣ′ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = Πᵣ′ rF' lF' lG' lF<' lG<' F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , rF≡rF , lF≡lF , G≡G , lG≡lG , _ = Π-PE-injectivity (whrDet* (D′ , Whnf.Πₙ) (red D' , Whnf.Πₙ))
  in Uₜ₌ (un-univEq (maybeEmb′ (<is≤ 0<1) [A])) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F' ^ rF' ° lF' ▹ X ° lG' ° _ ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π X ^ rF' ° lF' ▹ G′ ° lG' ° _ ^ _ ) F≡F
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ rF' ° lF' ▹ G′ ° X ° _ ^ _ ) lG≡lG
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ rF' ° X ▹ G′ ° lG ° _ ^ _ ) lF≡lF
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ X ° lF ▹ G′ ° lG ° _ ^ _ ) rF≡rF A≡B)))))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {.%} _ _ (emb⁰¹ (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                        (∃ᵣ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext')))
                                    (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let [A] = ∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = ∃ᵣ′ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = ∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , G≡G  = ∃-PE-injectivity (whrDet* (D′ , Whnf.∃ₙ) (red D' , Whnf.∃ₙ))
  in Uₜ₌ (un-univEq (maybeEmb′ (<is≤ 0<1) [A])) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ F' ▹ X ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ X ▹ G′ ^ _ ) F≡F A≡B))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {.%} _ _ (emb⁰¹ (emb¹⁰ (Emptyᵥ [[ ⊢A , ⊢Empty , D ]] EmptyB))) [A≡B] =
  let [A] = Emptyᵣ [[ ⊢A , ⊢Empty , D ]]
      [B] = Emptyᵣ [[ redFirst* [A≡B] , ⊢Empty , [A≡B] ]]
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅ₜ-Emptyrefl (wf ⊢A)) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {r} _ _ (emb⁰¹ (emb¹⁰ (ne (ne K D neK K≡K) neB))) (ne₌ M D′ neM K≡M) =
  let [A] = ne′ K D neK K≡K
      [B] = ne′ M D′ neM (~-trans (~-sym K≡M) K≡M)
      [A≡B] = ne₌ M D′ neM K≡M
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (~-to-≅ₜ K≡M) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {r} _ _ (emb⁰¹ (emb¹⁰ (Πᵥ (Πᵣ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                        (Πᵣ rF' lF' lG' lF<' lG<' F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'))))
                                    (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let [A] = Πᵣ′ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = Πᵣ′ rF' lF' lG' lF<' lG<' F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , rF≡rF , lF≡lF , G≡G , lG≡lG , _ = Π-PE-injectivity (whrDet* (D′ , Whnf.Πₙ) (red D' , Whnf.Πₙ))
  in Uₜ₌ (un-univEq (maybeEmb′ (<is≤ 0<1) [A])) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq (maybeEmb′ (<is≤ 0<1) [B])))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F' ^ rF' ° lF' ▹ X ° lG' ° _ ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π X ^ rF' ° lF' ▹ G′ ° lG' ° _ ^ _ ) F≡F
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ rF' ° lF' ▹ G′ ° X ° _ ^ _ ) lG≡lG
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ rF' ° X ▹ G′ ° lG ° _ ^ _ ) lF≡lF
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ X ° lF ▹ G′ ° lG ° _ ^ _ ) rF≡rF A≡B)))))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {.%} _ _ (emb⁰¹ (emb¹⁰ (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                        (∃ᵣ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'))))
                                    (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let [A] = ∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = ∃ᵣ′ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = ∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , G≡G  = ∃-PE-injectivity (whrDet* (D′ , Whnf.∃ₙ) (red D' , Whnf.∃ₙ))
  in Uₜ₌ (un-univEq (maybeEmb′ (<is≤ 0<1) [A])) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq (maybeEmb′ (<is≤ 0<1) [B])))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ F' ▹ X ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ X ▹ G′ ^ _ ) F≡F A≡B))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {.%} _ _ (emb¹⁰ (Emptyᵥ [[ ⊢A , ⊢Empty , D ]] EmptyB)) [A≡B] =
  let [A] = Emptyᵣ [[ ⊢A , ⊢Empty , D ]]
      [B] = Emptyᵣ [[ redFirst* [A≡B] , ⊢Empty , [A≡B] ]]
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅ₜ-Emptyrefl (wf ⊢A)) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {r} _ _ (emb¹⁰ (ne (ne K D neK K≡K) neB)) (ne₌ M D′ neM K≡M) =
  let [A] = ne′ K D neK K≡K
      [B] = ne′ M D′ neM (~-trans (~-sym K≡M) K≡M)
      [A≡B] = ne₌ M D′ neM K≡M
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (~-to-≅ₜ K≡M) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {r} _ _ (emb¹⁰ (Πᵥ (Πᵣ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                        (Πᵣ rF' lF' lG' lF<' lG<' F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext')))
                                    (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let [A] = Πᵣ′ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = Πᵣ′ rF' lF' lG' lF<' lG<' F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , rF≡rF , lF≡lF , G≡G , lG≡lG , _ = Π-PE-injectivity (whrDet* (D′ , Whnf.Πₙ) (red D' , Whnf.Πₙ))
  in Uₜ₌ (un-univEq [A] ) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq (maybeEmb′ (<is≤ 0<1) [B])))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F' ^ rF' ° lF' ▹ X ° lG' ° _ ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π X ^ rF' ° lF' ▹ G′ ° lG' ° _ ^ _ ) F≡F
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ rF' ° lF' ▹ G′ ° X ° _ ^ _ ) lG≡lG
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ rF' ° X ▹ G′ ° lG ° _ ^ _ ) lF≡lF
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ X ° lF ▹ G′ ° lG ° _ ^ _ ) rF≡rF A≡B)))))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {.%} _ _ (emb¹⁰ (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                         (∃ᵣ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext')))
                                    (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let [A] = ∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = ∃ᵣ′ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = ∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , G≡G  = ∃-PE-injectivity (whrDet* (D′ , Whnf.∃ₙ) (red D' , Whnf.∃ₙ))
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq (maybeEmb′ (<is≤ 0<1) [B])))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ F' ▹ X ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ X ▹ G′ ^ _ ) F≡F A≡B))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {.%} _ _ (emb¹⁰ (emb⁰¹ (Emptyᵥ [[ ⊢A , ⊢Empty , D ]] EmptyB))) [A≡B] =
  let [A] = Emptyᵣ [[ ⊢A , ⊢Empty , D ]]
      [B] = Emptyᵣ [[ redFirst* [A≡B] , ⊢Empty , [A≡B] ]]
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (≅ₜ-Emptyrefl (wf ⊢A)) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {r} _ _ (emb¹⁰ (emb⁰¹ (ne (ne K D neK K≡K) neB))) (ne₌ M D′ neM K≡M) =
  let [A] = ne′ K D neK K≡K
      [B] = ne′ M D′ neM (~-trans (~-sym K≡M) K≡M)
      [A≡B] = ne₌ M D′ neM K≡M
  in Uₜ₌ (un-univEq [A]) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq [B]))
         (~-to-≅ₜ K≡M) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {r} _ _ (emb¹⁰ (emb⁰¹ (Πᵥ (Πᵣ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                        (Πᵣ rF' lF' lG' lF<' lG<' F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'))))
                                    (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let [A] = Πᵣ′ rF lF lG lF< lG< F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = Πᵣ′ rF' lF' lG' lF<' lG<' F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , rF≡rF , lF≡lF , G≡G , lG≡lG , _ = Π-PE-injectivity (whrDet* (D′ , Whnf.Πₙ) (red D' , Whnf.Πₙ))
  in Uₜ₌ (un-univEq (maybeEmb′ (<is≤ 0<1) [A])) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq (maybeEmb′ (<is≤ 0<1) [B])))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG  ° _ ≅  Π F' ^ rF' ° lF' ▹ X ° lG' ° _ ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π X ^ rF' ° lF' ▹ G′ ° lG' ° _ ^ _ ) F≡F
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ rF' ° lF' ▹ G′ ° X ° _ ^ _ ) lG≡lG
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ rF' ° X ▹ G′ ° lG ° _ ^ _ ) lF≡lF
             (PE.subst (λ X → _ ⊢ Π F ^ rF ° lF ▹ G ° lG ° _ ≅  Π F′ ^ X ° lF ▹ G′ ° lG ° _  ^ _ ) rF≡rF A≡B)))))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]
un-univEqEq-Shape {¹} {Γ} {A} {B} {.%} _ _ (emb¹⁰ (emb⁰¹ (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                        (∃ᵣ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'))))
                                    (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let [A] = ∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
      [B] = ∃ᵣ′ F' G' D' ⊢F' ⊢G' A≡A' [F'] [G'] G-ext'
      [A≡B] = ∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
      F≡F , G≡G  = ∃-PE-injectivity (whrDet* (D′ , Whnf.∃ₙ) (red D' , Whnf.∃ₙ))
  in Uₜ₌ (un-univEq (maybeEmb′ (<is≤ 0<1) [A])) (irrelevanceTerm {l = next ¹} (Ugen (wf (escape [B]))) (Ugen (wf (escape [A]))) (un-univEq (maybeEmb′ (<is≤ 0<1) [B])))
         (≅-un-univ (
           PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ F' ▹ X ^ _ ) G≡G
           (PE.subst (λ X → _ ⊢ ∃ F ▹ G ≅  ∃ X ▹ G′ ^ _ ) F≡F A≡B))) λ [ρ] ⊢Δ → Lwk.wkEq [ρ] ⊢Δ [A] [A≡B]

un-univEqEq : ∀ {l Γ A B r }
          ([A] : Γ ⊩⟨ ι l ⟩ A ^ [ r , ι l ]) ([B] : Γ ⊩⟨ ι l ⟩ B ^ [ r , ι l ])
          ([A≡B] : Γ ⊩⟨ ι l ⟩ A ≡ B ^ [ r , ι l ] / [A])
          → let [U] : Γ ⊩⟨ next l ⟩ Univ r l ^ [ ! , next l ]
                [U] = Ugen (wf (escape [A]))
            in Γ ⊩⟨ next l ⟩ A ≡ B ∷ Univ r l ^ [ ! , next l ] / [U]
un-univEqEq [A] [B] [A≡B] = un-univEqEq-Shape [A] [B] (goodCases [A] [B] [A≡B]) [A≡B]

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
-- Products and Cartesian categories
module CategoryTheory.BCCCs.Cartesian where

open import CategoryTheory.Categories

open import Relation.Binary using (IsEquivalence)

module _ {n} (ℂ : Category n) where

    open Category ℂ

    -- Terminal object in a category
    record TerminalObj : Set (lsuc n) where
        field
            -- | Data
            -- The terminal object
            ⊤ : obj
            -- Canonical morphism
            ! : {A : obj} -> (A ~> ⊤)

            -- | Laws
            -- Need to show that the canonical morphism ! is unique
            !-unique : {A : obj} -> (m : A ~> ⊤)
                  -> m ≈ !

    -- Product of two objects
    -- Based on github.com/copumpkin/categories
    record Product (A B : obj) : Set (lsuc n) where
        infix 10 ⟨_,_⟩
        field
            -- | Data
            -- Product of A and B
            A⊗B : obj
            -- First projection
            π₁ : A⊗B ~> A
            -- Second projection
            π₂ : A⊗B ~> B
            -- Canonical mediator
            ⟨_,_⟩ : ∀{P} -> (P ~> A) -> (P ~> B) -> (P ~> A⊗B)

            -- | Laws
            -- ⟨_,_⟩ expresses that given another candidate product C
            -- and candidate projections to A and B there is a morphism
            -- from P to A⊗B. We need to check that this mediator makes
            -- the product diagram commute and is unique.

            π₁-comm : ∀{P} -> {p₁ : P ~> A} {p₂ : P ~> B}
                   -> π₁ ∘ ⟨ p₁ , p₂ ⟩ ≈ p₁
            π₂-comm : ∀{P} -> {p₁ : P ~> A} {p₂ : P ~> B}
                   -> π₂ ∘ ⟨ p₁ , p₂ ⟩ ≈ p₂
            ⊗-unique  : ∀{P} -> {p₁ : P ~> A} {p₂ : P ~> B} {m : P ~> A⊗B}
                   -> π₁ ∘ m ≈ p₁ -> π₂ ∘ m ≈ p₂ -> ⟨ p₁ , p₂ ⟩ ≈ m

        -- η-expansion of function pairs (via morphisms)
        ⊗-η-exp : ∀{P} -> {m : P ~> A⊗B}
               -> ⟨ π₁ ∘ m , π₂ ∘ m ⟩ ≈ m
        ⊗-η-exp = ⊗-unique r≈ r≈

        -- Pairing of projection functions is the identity
        ⊗-η-id : ⟨ π₁ , π₂ ⟩ ≈ id
        ⊗-η-id = ⊗-unique id-right id-right

        -- Congruence over function pairing
        ⟨,⟩-cong : ∀{P} -> {p₁ q₁ : P ~> A} {p₂ q₂ : P ~> B}
               -> p₁ ≈ q₁ -> p₂ ≈ q₂
               -> ⟨ p₁ , p₂ ⟩ ≈ ⟨ q₁ , q₂ ⟩
        ⟨,⟩-cong pr1 pr2 = ⊗-unique (π₁-comm ≈> pr1 [sym]) (π₂-comm ≈> pr2 [sym])

        ⟨,⟩-distrib : ∀{P Q} -> {h : P ~> Q} {f : Q ~> A} {g : Q ~> B}
                  -> ⟨ f , g ⟩ ∘ h ≈ ⟨ f ∘ h , g ∘ h ⟩
        ⟨,⟩-distrib = ⊗-unique (∘-assoc [sym] ≈> ≈-cong-left π₁-comm)
                            (∘-assoc [sym] ≈> ≈-cong-left π₂-comm) [sym]

-- Type class for Cartesian categories
record Cartesian {n} (ℂ : Category n) : Set (lsuc n) where
    open Category ℂ
    field
        -- | Data
        -- Terminal object
        term : TerminalObj ℂ
        -- Binary products for all pairs of objects
        prod : ∀(A B : obj) -> Product ℂ A B

    open TerminalObj term public
    open module P {A} {B} = Product (prod A B) public

    -- Shorthand for sum object
    infixl 25 _⊗_
    _⊗_ : (A B : obj) -> obj
    A ⊗ B = A⊗B {A} {B}

    -- Parallel product of morphisms
    infixl 65 _*_
    _*_ : {A B P Q : obj} -> (A ~> P) -> (B ~> Q)
       -> (A ⊗ B ~> P ⊗ Q)
    _*_ {A} {B} {P} {Q} f g = ⟨ f ∘ π₁ , g ∘ π₂ ⟩

    -- Parallel product with an idempotent morphism distributes over ∘
    *-idemp-dist-∘ : {A B C D : obj}{g : B ~> C}{f : A ~> B}{h : D ~> D}
            -> h ∘ h ≈ h
            -> g * h ∘ f * h ≈ (g ∘ f) * h
    *-idemp-dist-∘ {g = g}{f}{h} idemp = ⊗-unique u₁ u₂ [sym]
        where
        u₁ : π₁ ∘ (g * h ∘ f * h) ≈ (g ∘ f) ∘ π₁
        u₁ = ∘-assoc [sym] ≈> ≈-cong-left π₁-comm
          ≈> ∘-assoc ≈> ≈-cong-right π₁-comm ≈> ∘-assoc [sym]
        u₂ : π₂ ∘ (g * h ∘ f * h) ≈ h ∘ π₂
        u₂ = ∘-assoc [sym] ≈> ≈-cong-left π₂-comm
          ≈> ∘-assoc ≈> ≈-cong-right π₂-comm
          ≈> ∘-assoc [sym] ≈> ≈-cong-left idemp

    -- Parallel product with an idempotent morphism distributes over ∘
    *-id-dist-∘ : {A B C : obj}{g : B ~> C}{f : A ~> B}
            -> (_*_ {B = B} g id) ∘ f * id ≈ (g ∘ f) * id
    *-id-dist-∘ = *-idemp-dist-∘ id-right

    -- Commutativity of product
    comm : {A B : obj} -> A ⊗ B ~> B ⊗ A
    comm {A}{B} = ⟨ π₂ , π₁ ⟩

    -- Associativity of product
    assoc-left : {A B C : obj} -> A ⊗ (B ⊗ C) ~> (A ⊗ B) ⊗ C
    assoc-left = ⟨ ⟨ π₁ , (π₁ ∘ π₂) ⟩ , π₂ ∘ π₂ ⟩

    assoc-right : {A B C : obj} -> (A ⊗ B) ⊗ C ~> A ⊗ (B ⊗ C)
    assoc-right = ⟨ π₁ ∘ π₁ , ⟨ (π₂ ∘ π₁) , π₂ ⟩ ⟩

    -- Left and right unit for product
    unit-left : {A : obj} -> ⊤ ⊗ A ~> A
    unit-left = π₂

    unit-right : {A : obj} -> A ⊗ ⊤ ~> A
    unit-right = π₁

    -- The terminal object is the unit for product
    ⊤-left-cancel : ∀{A} -> ⊤ ⊗ A <~> A
    ⊤-left-cancel {A} = record
        { iso~> = π₂
        ; iso<~ = ⟨ ! , id ⟩
        ; iso-id₁ = iso-id₁-⊤
        ; iso-id₂ = π₂-comm
        }
        where
        iso-id₁-⊤ : ⟨ ! , id ⟩ ∘ π₂ ≈ id
        iso-id₁-⊤ =
            begin
                ⟨ ! , id ⟩ ∘ π₂
            ≈⟨ ⟨,⟩-distrib ⟩
                ⟨ ! ∘ π₂ , id ∘ π₂ ⟩
            ≈⟨ ⟨,⟩-cong r≈ id-left ⟩
                ⟨ ! ∘ π₂ , π₂ ⟩
            ≈⟨ ⟨,⟩-cong (!-unique (! ∘ π₂)) r≈ ⟩
                ⟨ ! , π₂ ⟩
            ≈⟨ ⟨,⟩-cong ((!-unique π₁) [sym]) r≈ ⟩
                ⟨ π₁ , π₂ ⟩
            ≈⟨ ⊗-η-id ⟩
                id
            ∎

    ⊤-right-cancel : ∀{A} -> A ⊗ ⊤ <~> A
    ⊤-right-cancel {A} = record
        { iso~> = π₁
        ; iso<~ = ⟨ id , ! ⟩
        ; iso-id₁ = iso-id₁-⊤
        ; iso-id₂ = π₁-comm
        }
        where
        iso-id₁-⊤ : ⟨ id , ! ⟩ ∘ π₁ ≈ id
        iso-id₁-⊤ =
            begin
                ⟨ id , ! ⟩ ∘ π₁
            ≈⟨ ⟨,⟩-distrib ⟩
                ⟨ id ∘ π₁ , ! ∘ π₁ ⟩
            ≈⟨ ⟨,⟩-cong id-left r≈ ⟩
                ⟨ π₁ , ! ∘ π₁ ⟩
            ≈⟨ ⟨,⟩-cong r≈ (!-unique (! ∘ π₁)) ⟩
                ⟨ π₁ , ! ⟩
            ≈⟨ ⟨,⟩-cong r≈ ((!-unique π₂) [sym]) ⟩
                ⟨ π₁ , π₂ ⟩
            ≈⟨ ⊗-η-id ⟩
                id
            ∎

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module Issue309b where

data D : Set where
  d : D → D

syntax d x = f

g : D → D
g (d x) = f

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module TerminationListInsertionNaive where

data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

infixr 50 _::_

-- non-deterministic choice
postulate
  _⊕_ : {A : Set} -> A -> A -> A
infixl 10 _⊕_

-- a funny formulation of insert
-- insert (a :: l)  inserts a into l
--
-- this example cannot be handled with subpatterns
-- it is done with structured orders
-- could also be done with sized types

insert : {A : Set} -> List A -> List A
insert [] = []
insert (a :: []) = a :: []
insert (a :: b :: bs) = a :: b :: bs ⊕        -- case a <= b
                        b :: insert (a :: bs) -- case a > b

-- list flattening
-- termination using structured orders
flat : {A : Set} -> List (List A) -> List A
flat [] = []
flat ([] :: ll) = flat ll
flat ((x :: l) :: ll) = x :: flat (l :: ll)

{- generates two recursive calls with the following call matrices

      [] :: ll         (x :: l)   ll

  ll  <            l   <          .
                   ll  .          =

during composition, the second is collapsed to =, so the call graph is
already complete.  Both matrices are idempotent and contain a strictly
decreasing argument.

It could also be done with sized types; lexicographic in (i,j)
with type

  flat : {A : Set} -> (1 + Listʲ A × List^i (List^∞ A)) -> List^∞ A

-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Unit.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Nat
open import Cubical.Data.Unit.Base
open import Cubical.Data.Prod.Base

open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

open import Cubical.Reflection.StrictEquiv

isContrUnit : isContr Unit
isContrUnit = tt , λ {tt → refl}

isPropUnit : isProp Unit
isPropUnit _ _ i = tt -- definitionally equal to: isContr→isProp isContrUnit

isSetUnit : isSet Unit
isSetUnit = isProp→isSet isPropUnit

isOfHLevelUnit : (n : HLevel) → isOfHLevel n Unit
isOfHLevelUnit n = isContr→isOfHLevel n isContrUnit

module _ {ℓ} (A : Type ℓ) where
  UnitToType≃ : (Unit → A) ≃ A
  unquoteDef UnitToType≃ = defStrictEquiv UnitToType≃ (λ f → f _) const

UnitToTypePath : ∀ {ℓ} (A : Type ℓ) → (Unit → A) ≡ A
UnitToTypePath A = ua (UnitToType≃ A)

isContr→Iso2 : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → isContr A → Iso (A → B) B
Iso.fun (isContr→Iso2 iscontr) f = f (fst iscontr)
Iso.inv (isContr→Iso2 iscontr) b _ = b
Iso.rightInv (isContr→Iso2 iscontr) _ = refl
Iso.leftInv (isContr→Iso2 iscontr) f = funExt λ x → cong f (snd iscontr x)

diagonal-unit : Unit ≡ Unit × Unit
diagonal-unit = isoToPath (iso (λ x → tt , tt) (λ x → tt) (λ {(tt , tt) i → tt , tt}) λ {tt i → tt})

fibId : ∀ {ℓ} (A : Type ℓ) → (fiber (λ (x : A) → tt) tt) ≡ A
fibId A = ua e
  where
  unquoteDecl e = declStrictEquiv e fst (λ a → a , refl)

isContr→≃Unit : ∀ {ℓ} {A : Type ℓ} → isContr A → A ≃ Unit
isContr→≃Unit contr = isoToEquiv (iso (λ _ → tt) (λ _ → fst contr) (λ _ → refl) λ _ → snd contr _)

isContr→≡Unit : {A : Type₀} → isContr A → A ≡ Unit
isContr→≡Unit contr = ua (isContr→≃Unit contr)

isContrUnit* : ∀ {ℓ} → isContr (Unit* {ℓ})
isContrUnit* = tt* , λ _ → refl

isPropUnit* : ∀ {ℓ} → isProp (Unit* {ℓ})
isPropUnit* _ _ = refl

isOfHLevelUnit* : ∀ {ℓ} (n : HLevel) → isOfHLevel n (Unit* {ℓ})
isOfHLevelUnit* zero = tt* , λ _ → refl
isOfHLevelUnit* (suc zero) _ _ = refl
isOfHLevelUnit* (suc (suc zero)) _ _ _ _ _ _ = tt*
isOfHLevelUnit* (suc (suc (suc n))) = isOfHLevelPlus 3 (isOfHLevelUnit* n)

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
open import Common.Prelude

_test_ : Nat → Nat → Nat
_test n = _+ n

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module ChainRule where

  import Sets
  import Functor
  import Logic.ChainReasoning.Poly as CR
  import Isomorphism
  import Derivative

  open Derivative
  open Sets
  open Functor
  open Semantics
  open Isomorphism
  module Chain = CR _==_ (\x -> refl{x = x}) (\x y z -> trans{x = x}{y}{z})
  open Chain

  chain-rule : (F G : U)(X : Set) -> ⟦ ∂ (F [ G ]) ⟧ X ≅ ⟦ ∂ F [ G ] × ∂ G ⟧ X
  chain-rule F G X = iso (i F) (j F) (ji F) (ij F)
    where
      i : (F : U) -> ⟦ ∂ (F [ G ]) ⟧ X -> ⟦ ∂ F [ G ] × ∂ G ⟧ X
      i (K A)	  ()
      i Id	  x		    = < <> , x >
      i (F₁ + F₂) (inl c)	    = (inl <×> id) (i F₁ c)
      i (F₁ + F₂) (inr c)	    = (inr <×> id) (i F₂ c)
      i (F₁ × F₂) (inl < c  , f₂ >) = (inl ∘ <∙, f₂ > <×> id) (i F₁ c)
      i (F₁ × F₂) (inr < f₁ , c  >) = (inr ∘ < f₁ ,∙> <×> id) (i F₂ c)

      j : (F : U) -> ⟦ ∂ F [ G ] × ∂ G ⟧ X -> ⟦ ∂ (F [ G ]) ⟧ X
      j (K A)	  < () , _ >
      j Id	  < <> , x > = x
      j (F₁ + F₂) < inl x , y > = inl (j F₁ < x , y >)
      j (F₁ + F₂) < inr x , y > = inr (j F₂ < x , y >)
      j (F₁ × F₂) < inl < x , y > , z > = inl < j F₁ < x , z > , y >
      j (F₁ × F₂) < inr < x , y > , z > = inr < x , j F₂ < y , z > >

      ij : (F : U)(x : _) -> i F (j F x) == x
      ij (K A)	   < () , _ >
      ij Id	   < <> , x > = refl
      ij (F₁ + F₂) < lx@(inl x) , y > =
	subst (\ ∙ -> (inl <×> id) ∙ == < lx , y >)
	      (ij F₁ < x , y >) refl
      ij (F₁ + F₂) < rx@(inr x) , y > =
	subst (\ ∙ -> (inr <×> id) ∙ == < rx , y >)
	      (ij F₂ < x , y >) refl
      ij (F₁ × F₂) < xy@(inl < x , y >) , z > =
	subst (\ ∙ -> (inl ∘ <∙, y > <×> id) ∙ == < xy , z >)
	      (ij F₁ < x , z >) refl
      ij (F₁ × F₂) < xy@(inr < x , y >) , z > =
	subst (\ ∙ -> (inr ∘ < x ,∙> <×> id) ∙ == < xy , z >)
	      (ij F₂ < y , z >) refl

      ji : (F : U)(y : _) -> j F (i F y) == y
      ji (K A) ()
      ji Id x = refl
      ji (F₁ + F₂) (inl c) =
	chain> j (F₁ + F₂) ((inl <×> id) (i F₁ c))
	   === inl (j F₁ _)	    by cong (j (F₁ + F₂) ∘ (inl <×> id)) (η-[×] (i F₁ c))
	   === inl (j F₁ (i F₁ c))  by cong (inl ∘ j F₁) (sym $ η-[×] (i F₁ c))
	   === inl c		    by cong inl (ji F₁ c)
      ji (F₁ + F₂) rc @ (inr c) =
	subst (\ ∙ -> j (F₁ + F₂) ((inr <×> id) ∙) == rc) (η-[×] (i F₂ c))
	$ subst (\ ∙ -> inr (j F₂ ∙) == rc) (sym $ η-[×] (i F₂ c))
	$ subst (\ ∙ -> inr ∙ == rc) (ji F₂ c) refl
      ji (F₁ × F₂) l @ (inl < c , f₂ >) =
	subst (\ ∙ -> j (F₁ × F₂) ((inl ∘ <∙, f₂ > <×> id) ∙) == l) (η-[×] (i F₁ c))
	$ subst (\ ∙ -> inl < j F₁ ∙ , f₂ > == l) (sym $ η-[×] (i F₁ c))
	$ subst (\ ∙ -> inl < ∙ , f₂ > == l) (ji F₁ c) refl
      ji (F₁ × F₂) r @ (inr < f₁ , c >) =
	subst (\ ∙ -> j (F₁ × F₂) ((inr ∘ < f₁ ,∙> <×> id) ∙) == r) (η-[×] (i F₂ c))
	$ subst (\ ∙ -> inr < f₁ , j F₂ ∙ > == r) (sym $ η-[×] (i F₂ c))
	$ subst (\ ∙ -> inr < f₁ , ∙ > == r) (ji F₂ c) refl


text:
module Data.List.Relation where

import      Lvl
import      Data
open import Data.List
open import Logic
open import Logic.Propositional
open import Structure.Setoid
open import Type

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable T : Type{ℓ}

data Empty {ℓ}{T : Type{ℓ}} : List(T) → Stmt{Lvl.𝐒(ℓ)} where
  intro : Empty(∅)

-- Statement of whether a list is contained in the beginning of another list
_isPrefixOf_ : ⦃ equiv : Equiv{ℓₑ}(T) ⦄ → List(T) → List(T) → Stmt{Lvl.of(T) Lvl.⊔ ℓₑ}
∅            isPrefixOf _       = Data.Unit
(p ⊰ prefix) isPrefixOf ∅       = Data.Empty
(p ⊰ prefix) isPrefixOf (x ⊰ l) = (p ≡ x) ∧ (prefix isPrefixOf l)
-- _isPrefixOf_ prefix l = (∃ \rest → l ≡ (prefix ++ rest))

-- Statement of whether a list is contained in the end of another list
_isSuffixOf_ : ⦃ equiv : Equiv{ℓₑ₁}(T) ⦄ → ⦃ equiv-list : Equiv{ℓₑ₂}(List(T)) ⦄ → List(T) → List(T) → Stmt{Lvl.of(T) Lvl.⊔ ℓₑ₁ Lvl.⊔ ℓₑ₂}
∅            isSuffixOf _       = Data.Unit
(p ⊰ prefix) isSuffixOf ∅       = Data.Empty
(p ⊰ prefix) isSuffixOf (x ⊰ l) = ((p ⊰ prefix) isSuffixOf l) ∨ ((p ⊰ prefix) ≡ (x ⊰ l))
-- _isSuffixOf_ suffix l = (∃ \rest → l ≡ (rest ++ suffix))

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:
-- An example of something where normalization is surprisingly slow
{-# OPTIONS --cubical --safe #-}
module Cubical.Experiments.Problem where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

open import Cubical.Data.Int

open import Cubical.HITs.S1
open import Cubical.HITs.S2
open import Cubical.HITs.S3
open import Cubical.HITs.Join
open import Cubical.HITs.Hopf

ptType : Type _
ptType = Σ Type₀ \ A → A

pt : (A : ptType) → A .fst
pt A = A .snd

S¹pt : ptType
S¹pt = (S¹ , base)
S²pt : ptType
S²pt = (S² , base)
S³pt : ptType
S³pt = (S³ , base)
joinpt : ptType
joinpt = (join S¹ S¹ , inl base)

Ω : (A : ptType) → ptType
Ω A = Path _ (pt A) (pt A) , refl
Ω² : (A : ptType) → ptType
Ω² A = Ω (Ω A)
Ω³ : (A : ptType) → ptType
Ω³ A = Ω² (Ω A)

α : join S¹ S¹ → S²
α (inl _) = base
α (inr _) = base
α (push x y i) = (merid y ∙ merid x) i
  where
  merid : S¹ → Path S² base base
  merid base = refl
  merid (loop i) = λ j → surf i j

-- The tests

test0To2 : Ω³ S³pt .fst
test0To2 i j k = surf i j k

f3 : Ω³ S³pt .fst → Ω³ joinpt .fst
f3 p i j k = S³→joinS¹S¹ (p i j k)

test0To3 : Ω³ joinpt .fst
test0To3 = f3 test0To2

f4 : Ω³ joinpt .fst → Ω³ S²pt .fst
f4 p i j k = α (p i j k)

test0To4 : Ω³ S²pt .fst
test0To4 = f4 test0To3

innerpath : ∀ i j → HopfS² (test0To4 i j i1)
innerpath i j = transp (λ k → HopfS² (test0To4 i j k)) i0 base

-- C-c C-n problem uses a lot of memory
problem : pos 0 ≡ pos 0
problem i = transp (λ j → helix (innerpath i j)) i0 (pos 0)

-- Lots of tests: (thanks Evan!)

winding2 : Path (Path S² base base) refl refl → Int
winding2 p = winding (λ j → transp (λ i → HopfS² (p i j)) i0 base)

test0 : Int
test0 = winding2 (λ i j → surf i j)

test1 : Int
test1 = winding2 (λ i j → surf j i)

test2 : Int
test2 = winding2 (λ i j → hcomp (λ _ → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) (surf i j))

test3 : Int
test3 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) base)

test4 : Int
test4 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) base)

test5 : Int
test5 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → surf k i ; (j = i1) → base}) base)

test6 : Int
test6 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → surf k i}) base)

test7 : Int
test7 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → surf j k ; (j = i0) → base ; (j = i1) → base}) (surf i j))

test8 : Int
test8 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → surf k i ; (j = i1) → base}) (surf i j))

test9 : Int
test9 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → surf k i}) (surf i j))

test10 : Int
test10 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) (surf i j))

-- Tests using HopfS²'

winding2' : Path (Path S² base base) refl refl → Int
winding2' p = winding (λ j → transp (λ i → HopfS²' (p i j)) i0 base)

test0' : Int
test0' = winding2' (λ i j → surf i j)

test1' : Int
test1' = winding2' (λ i j → surf j i)

test2' : Int
test2' = winding2' (λ i j → hcomp (λ _ → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) (surf i j))

test3' : Int
test3' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) base)

test4' : Int
test4' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) base)

test5' : Int
test5' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → surf k i ; (j = i1) → base}) base)

test6' : Int
test6' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → surf k i}) base)

test7' : Int
test7' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → surf j k ; (j = i0) → base ; (j = i1) → base}) (surf i j))

test8' : Int
test8' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → surf k i ; (j = i1) → base}) (surf i j))

test9' : Int
test9' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → surf k i}) (surf i j))

test10' : Int
test10' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) (surf i j))

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence

module HoTT.Equivalence.Coproduct where

open variables
private variable A' B' : 𝒰 i

+-empty₁ : 𝟎 {i} + B ≃ B
+-empty₁ = let open Iso in iso→eqv λ where
  .f (inl ())
  .f (inr b) → b
  .g         → inr
  .η (inl ())
  .η (inr b) → refl
  .ε _       → refl

+-empty₂ : A + 𝟎 {j} ≃ A
+-empty₂ = let open Iso in iso→eqv λ where
  .f (inl a) → a
  .f (inr ())
  .g         → inl
  .η (inl b) → refl
  .η (inr ())
  .ε _       → refl

+-comm : A + B ≃ B + A
+-comm = let open Iso in iso→eqv λ where
  .f (inl a) → inr a
  .f (inr b) → inl b
  .g (inl b) → inr b
  .g (inr a) → inl a
  .η (inl a) → refl
  .η (inr b) → refl
  .ε (inl b) → refl
  .ε (inr a) → refl

+-equiv : A ≃ A' → B ≃ B' → A + B ≃ A' + B'
+-equiv e₁ e₂ =
  iso→eqv λ where
    .f (inl a)  → inl (f₁ a)
    .f (inr b)  → inr (f₂ b)
    .g (inl a') → inl (g₁ a')
    .g (inr b') → inr (g₂ b')
    .η (inl a)  → ap inl (η₁ a)
    .η (inr b)  → ap inr (η₂ b)
    .ε (inl a') → ap inl (ε₁ a')
    .ε (inr b') → ap inr (ε₂ b')
  where
  open Iso
  open Iso (eqv→iso e₁) renaming (f to f₁ ; g to g₁ ; η to η₁ ; ε to ε₁)
  open Iso (eqv→iso e₂) renaming (f to f₂ ; g to g₂ ; η to η₂ ; ε to ε₂)

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
module Datoid where

  import Equiv
  import Prelude

  open Equiv
  open Prelude

  data Datoid : Set1 where
    datoid : (a : Set) -> DecidableEquiv a -> Datoid

  El : Datoid -> Set
  El (datoid a _) = a

  datoidEq : (a : Datoid) -> DecidableEquiv (El a)
  datoidEq (datoid _ eq) = eq

  datoidRel : (a : Datoid) -> El a -> El a -> Set
  datoidRel d = rel' (datoidEq d)

  datoidDecRel :  (a : Datoid) -> (x y : El a)
               -> Either (datoidRel a x y) (Not (datoidRel a x y))
  datoidDecRel d = decRel (datoidEq d)

  dRefl : (a : Datoid) -> {x : El a} -> datoidRel a x x
  dRefl a = refl (datoidEq a)

  dSym : (a : Datoid) -> {x y : El a}
      -> datoidRel a x y -> datoidRel a y x
  dSym a = sym (datoidEq a)

  dTrans : (a : Datoid) -> {x y z : El a}
      -> datoidRel a x y -> datoidRel a y z -> datoidRel a x z
  dTrans a = trans (datoidEq a)

  data Respects (a : Datoid) (P : El a -> Set) : Set where
    respects : ((x y : El a) -> datoidRel a x y -> P x -> P y) -> Respects a P

  subst :  {a : Datoid} -> {P : El a -> Set} -> Respects a P
        -> (x y : El a) -> datoidRel a x y -> P x -> P y
  subst (respects f) = f

  pairDatoid : (a b : Datoid) -> Datoid
  pairDatoid a b = datoid (Pair (El a) (El b))
                          (pairEquiv (datoidEq a) (datoidEq b))


text:
open import MLib.Prelude.FromStdlib
open import Relation.Binary using (Decidable; IsStrictTotalOrder)

module MLib.Prelude.DFS
  {v p e} {V : Set v} (_⇒_ : V → V → Set e)
  {_<_ : V → V → Set p} (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
  where

open import MLib.Prelude.Path
open Bool using (T)
open import Function.Equivalence using (Equivalence)

import Data.AVL isStrictTotalOrder as Tree
open Tree using (Tree)

-- A (directed) graph is a map from vertices to the list of edges out of that
-- vertex.
Graph = Tree (λ x → List (∃ λ y → x ⇒ y))

private
  module Seen where
    -- Represents a set of vertices that have been seen. At most 'n' vertices
    -- have /not/ been seen.
    record SeenSet (n : ℕ) : Set (v ⊔ˡ e ⊔ˡ p) where
      constructor mkSeen
      field
        getSeen : Tree (λ _ → ⊤)

    isSeen : ∀ {n} → V → SeenSet n → Bool
    isSeen x (mkSeen t) = x Tree.∈? t

    -- Mark a vertex as seen, thus reducing the number of /unseen/ vertices.
    mark : ∀ {n} → V → SeenSet (Nat.suc n) → Maybe (SeenSet n)
    mark x u@(mkSeen t) = if Bool.not (isSeen x u) then just (mkSeen (Tree.insert x tt t)) else nothing

    -- Make a seen set for a particular graph. The number of unseen vertices in
    -- the result is bounded above by the number of vertices in the graph.
    forGraph : Graph → ∃ SeenSet
    forGraph gr = (countVertices gr , mkSeen Tree.empty)
      where
      -- this overcounts but that doesn't matter because the index is only there
      -- to ensure termination of the DFS
      countVertices : Graph → ℕ
      countVertices = List.foldr (λ { (_ , es) n → List.foldr (λ _ → Nat.suc) n es }) 0 ∘ Tree.toList

    inj : ∀ {n} → SeenSet n → SeenSet (Nat.suc n)
    inj (mkSeen t) = mkSeen t

open Seen using (SeenSet)

private
  infixl 1 _>>=ₛ_

  MonadDfs : ∀ {a} → ℕ → Set a → Set (v ⊔ˡ (p ⊔ˡ (e ⊔ˡ a)))
  MonadDfs n A = SeenSet n → A × SeenSet n

  runMonadDfs : ∀ {n a} {A : Set a} → MonadDfs n A → SeenSet n → A
  runMonadDfs f = proj₁ ∘ f

  _>>=ₛ_ : ∀ {n a b} {A : Set a} {B : Set b} → MonadDfs n A → (A → MonadDfs n B) → MonadDfs n B
  (f >>=ₛ g) s =
    let x , s′ = f s
    in g x s′

  returnₛ : ∀ {n a} {A : Set a} → A → MonadDfs n A
  returnₛ x s = x , s

  withMarked : ∀ {n a} {A : Set a} V → MonadDfs n A → MonadDfs (Nat.suc n) (Maybe A)
  withMarked v f s =
    case Seen.mark v s of λ
    { (just s′) →
      let x , s′′ = f s′
      in just x , Seen.inj s′′
    ; nothing → nothing , s
    }

module _ (graph : Graph) where

  private
    PathsFrom = List ∘ ∃ ∘ Path _⇒_

    -- Calculates paths from the given source to every reachable target not in
    -- the seen set. Returns the new seen set, the list of paths found, and
    -- a boolean indicating whether this source was previously in the seen
    -- set.
    pathsFromSource : ∀ {n} (source : V) → MonadDfs n (Maybe (PathsFrom source))

    -- Calculates paths from the given source to every reachable target not in
    -- the seen set, whose first edge is among the list given.
    pathsViaEdges : ∀ {n} {source : V} → List (∃ (λ dest → source ⇒ dest)) → MonadDfs n (PathsFrom source)

    -- Calculates paths via the edge given to every reachable target not in the
    -- seen set.
    pathsViaEdge : ∀ {n} {source dest : V} → source ⇒ dest → MonadDfs n (PathsFrom source)

    -- The base case of induction on the size of the seen set. This is only here
    -- to satisfy the termination checker.
    pathsFromSource {Nat.zero} source = returnₛ nothing
    pathsFromSource {Nat.suc _} source = withMarked source (
      case Tree.lookup source graph of λ
      -- We have a list of edges from this source to some other vertex. For
      -- each of these, a recursive call will only return paths from that
      -- vertex if it is yet unseen. Note the recursive call is on a seen set
      -- with an index one lower, satisfying Agda's termination checker.
      { (just es) → pathsViaEdges es >>=ₛ returnₛ ∘ just
      -- there are no edges from this source so nothing is reachable from it
      ; nothing → returnₛ (just [])
      }) >>=ₛ maybe returnₛ (returnₛ nothing)

    pathsViaEdges [] = returnₛ []
    pathsViaEdges ((d , e) ∷ es) =
      pathsViaEdge e >>=ₛ λ pathsVia-d →
      pathsViaEdges es >>=ₛ λ restPaths →
      returnₛ (pathsVia-d List.++ restPaths)

    pathsViaEdge {dest = d} e =
      pathsFromSource d >>=ₛ λ
      { (just pathsFrom-d) →
        let pathsVia-d = List.map (λ {(d′ , p) → d′ , connect (edge e) p}) pathsFrom-d
        in returnₛ ((_ , edge e) ∷ pathsVia-d)
      ; nothing → returnₛ []
      }

  -- Given a source vertex S, finds all vertices T such that there is a path
  -- from S to T, and returns the path. No target vertex is returned more than
  -- once.
  allTargetsFrom : (source : V) → List (∃ (Path _⇒_ source))
  allTargetsFrom source =
    let _ , seen = Seen.forGraph graph
    in maybe id [] (runMonadDfs (pathsFromSource source) seen)

module _ (graph : Graph) (matches : V → Bool) where

  private
    findMatchingFrom : ∀ {n} (source : V) → MonadDfs n (Maybe (∃ λ dest → Path _⇒_ source dest × T (matches dest)))
    findMatchingViaEdges : ∀ {n} {source : V} → List (∃ (λ inter → source ⇒ inter)) → MonadDfs n (Maybe (∃ λ dest → Path _⇒_ source dest × T (matches dest)))
    findMatchingViaEdge : ∀ {n} {source inter : V} → source ⇒ inter → MonadDfs n (Maybe (∃ λ dest → Path _⇒_ source dest × T (matches dest)))

    -- The base case of induction on the size of the seen set. This is only here
    -- to satisfy the termination checker.
    findMatchingFrom {Nat.zero} source = returnₛ nothing
    findMatchingFrom {Nat.suc _} source = withMarked source (
      case Tree.lookup source graph of λ
      -- We have a list of edges from this source to some other vertex. For
      -- each of these, a recursive call will only return paths from that
      -- vertex if it is yet unseen. Note the recursive call is on a seen set
      -- with an index one lower, satisfying Agda's termination checker.
      { (just es) → findMatchingViaEdges es
      -- there are no edges from this source so nothing is reachable from it
      ; nothing → returnₛ nothing
      }) >>=ₛ maybe returnₛ (returnₛ nothing)

    findMatchingViaEdges [] = returnₛ nothing
    findMatchingViaEdges ((d , e) ∷ es) =
      findMatchingViaEdge e >>=ₛ λ
      { (just r) → returnₛ (just r)
      ; nothing → findMatchingViaEdges es
      }

    findMatchingViaEdge {inter = d} e with matches d | ≡.inspect matches d
    findMatchingViaEdge {inter = _} e | true | ≡.[ eq ] = returnₛ (just (_ , edge e , Equivalence.from Bool.T-≡ ⟨$⟩ eq))
    findMatchingViaEdge {inter = d} e | false | _ =
      findMatchingFrom d >>=ₛ λ
      { (just (_ , p , q)) → returnₛ (just (_ , connect (edge e) p , q))
      ; nothing → returnₛ nothing
      }

  -- Given a source vertex S, finds all vertices T such that there is a path
  -- from S to T, and returns the path. No target vertex is returned more than
  -- once.
  findMatching : (source : V) → Maybe (∃ λ dest → Path _⇒_ source dest × T (matches dest))
  findMatching source =
    let _ , seen = Seen.forGraph graph
    in runMonadDfs (findMatchingFrom source) seen

module _ (graph : Graph) {dest} (isDest : ∀ v → Dec (v ≡ dest)) where
  -- Given a source vertex S, finds all vertices T such that there is a path
  -- from S to T, and returns the path. No target vertex is returned more than
  -- once.
  findDest : (source : V) → Maybe (Path _⇒_ source dest)
  findDest source with findMatching graph (⌊_⌋ ∘ isDest) source
  ... | just (dest′ , p , q) with isDest dest′
  ... | yes ≡.refl = just p
  findDest source | just (_ , _ , ()) | no _
  findDest source | nothing = nothing


text:
open import Oscar.Prelude
open import Oscar.Class.[ExtensibleType]
open import Oscar.Data.Proposequality

module Oscar.Class.[ExtensibleType].Proposequality where

instance

  [ExtensibleType]Proposequality : ∀ {a} {b} {A : Set a} {B : A → Set b} → [ExtensibleType] (λ {w} → Proposequality⟦ B w ⟧)
  [ExtensibleType]Proposequality = ∁


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

module TreeFold where

open import Prelude
open import Data.List
open import Algebra using (Associative)
open import Data.List.Properties using (foldr-fusion; foldl-fusion; foldl′-foldl)

infixr 5 _^_&_
data Spine (A : Type a) : Type a where
  &0 : Spine A
  _^_&_ : A → ℕ → Spine A → Spine A

private variable n : ℕ

module Cons (f : A → A → A) where
  infixr 5 _^_∹_
  _^_∹_ : A → ℕ → Spine A → Spine A
  x ^ n ∹ &0 = x ^ n & &0
  x ^ n ∹ y ^ zero  & xs = f x y ^ suc n ∹ xs
  x ^ n ∹ y ^ suc m & xs = x ^ n & y ^ m & xs

  _∹_ : A → Spine A → Spine A
  _∹_ = _^ zero ∹_

module TreeFoldR (f : A → A → A) (z : A) where
  open Cons f public

  fold : Spine A → A
  fold &0 = z
  fold (x ^ n & xs) = f x (fold xs)

  spine : List A → Spine A
  spine = foldr _∹_ &0

  treeFold : List A → A
  treeFold = fold ∘ spine

  ∹-hom : Associative f → ∀ x xs → fold (x ^ n ∹ xs) ≡ f x (fold xs)
  ∹-hom p x &0 = refl
  ∹-hom p x (y ^ zero  & xs) = ∹-hom p (f x y) xs ; p x y (fold xs)
  ∹-hom p x (y ^ suc n & xs) = refl

  treeFoldHom : Associative f → ∀ xs → treeFold xs ≡ foldr f z xs
  treeFoldHom f-assoc = foldr-fusion fold &0 (∹-hom f-assoc)

module TreeFold1 (f : A → A → A) where
  open import Data.Maybe
  open import Data.Maybe.Properties
  open import Data.List.Properties

  f? : Maybe A → Maybe A → Maybe A
  f? nothing  = id
  f? (just x) = just ∘ maybe x (f x)

  open TreeFoldR f? nothing

  treeFoldMay : List A → Maybe A
  treeFoldMay = treeFold ∘ map just

  treeFoldMayHom : Associative f → ∀ xs → treeFoldMay xs ≡ foldrMay f xs
  treeFoldMayHom f-assoc xs = treeFoldHom f?-assoc (map just xs) ; map-fusion f? nothing just xs
    where
    f?-assoc : Associative f?
    f?-assoc nothing y z = refl
    f?-assoc (just x) nothing z = refl
    f?-assoc (just x) (just y) nothing = refl
    f?-assoc (just x) (just y) (just z) = cong just (f-assoc x y z)

  isJustSpine? : Spine (Maybe A) → Bool
  isJustSpine? &0 = false
  isJustSpine? (x ^ y & xs) = is-just x

  IsJustSpine : Spine (Maybe A) → Type
  IsJustSpine = T ∘ isJustSpine?

  isJust-cons : ∀ x n xs → IsJustSpine (just x ^ n ∹ xs)
  isJust-cons x n &0 = tt
  isJust-cons x n (y ^ zero  & xs) = isJust-cons (maybe x (f x) y) (suc n) xs
  isJust-cons x n (y ^ suc m & xs) = tt

  isJust-spine : ∀ xs → NonEmpty xs → IsJustSpine (spine (map just xs))
  isJust-spine (x ∷ xs) p = isJust-cons x 0 (spine (map just xs))

  isJust-fold : ∀ xs → IsJustSpine xs → IsJust (fold xs)
  isJust-fold (just _ ^ _ & _) _ = tt

  isJust-treeFoldMay : ∀ xs → NonEmpty xs → IsJust (treeFoldMay xs)
  isJust-treeFoldMay xs xsne = isJust-fold (spine (map just xs)) (isJust-spine xs xsne)

  treeFold1 : (xs : List A) → ⦃ NonEmpty xs ⦄ → A
  treeFold1 xs ⦃ xsne ⦄ = fromJust (treeFoldMay xs)
    where instance _ = isJust-treeFoldMay xs xsne

  -- treeFold1-hom : Associative f → ∀ xs → ⦃ xsne : NonEmpty xs ⦄ → treeFold1 xs ≡ foldr1 f xs
  -- treeFold1-hom f-assoc xs ⦃ xsne ⦄ = {!!}
open TreeFold1 using (treeFoldMay; treeFoldMayHom; treeFold1) public

open TreeFoldR using (treeFold; treeFoldHom) public

module TreeFoldL (f : A → A → A) (z : A) where
  open TreeFoldR (flip f) z using (_∹_; fold; ∹-hom) public

  spine : List A → Spine A
  spine = foldl (flip _∹_) &0

  treeFoldL : List A → A
  treeFoldL = fold ∘ spine

  treeFoldLHom : Associative f → ∀ xs → treeFoldL xs ≡ foldl f z xs
  treeFoldLHom p = foldl-fusion fold &0 (flip (∹-hom λ x y z → sym (p z y x)))

open TreeFoldL using (treeFoldL; treeFoldLHom) public

module StrictCons (f : A → A → A) where
  infixr 5 _^_∹_
  _^_∹_ : A → ℕ → Spine A → Spine A
  x ^ n ∹ &0 = x ^ n & &0
  x ^ n ∹ y ^ zero  & xs = (_^ suc n ∹ xs) $! (f x y)
  x ^ n ∹ y ^ suc m & xs = x ^ n & y ^ m & xs

  _∹_ : A → Spine A → Spine A
  _∹_ = _^ zero ∹_

  private module Lazy = Cons f

  strict-lazy-cons : ∀ x n xs → x ^ n ∹ xs ≡ x Lazy.^ n ∹ xs
  strict-lazy-cons x n &0 = refl
  strict-lazy-cons x n (y ^ zero  & xs) = $!-≡ (_^ suc n ∹ xs) (f x y) ; strict-lazy-cons (f x y) (suc n) xs
  strict-lazy-cons x n (y ^ suc m & xs) = refl

module TreeFoldL′ (f : A → A → A) (z : A) where
  open StrictCons (flip f)

  spine : List A → Spine A
  spine = foldl′ (flip _∹_) &0

  private module Lazy = TreeFoldL f z

  open Lazy using (fold)

  treeFoldL′ : List A → A
  treeFoldL′ = fold ∘ spine

  treeFoldL′Hom : Associative f → ∀ xs → treeFoldL′ xs ≡ foldl f z xs
  treeFoldL′Hom p xs =
    cong fold (foldl′-foldl (flip _∹_) &0 xs ; cong (λ c → foldl c &0 xs) (funExt λ ys → funExt λ y → strict-lazy-cons y 0 ys)) ;
    Lazy.treeFoldLHom p xs

open TreeFoldL′ using (treeFoldL′; treeFoldL′Hom) public

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------------
-- Testing the translation of definitions
------------------------------------------------------------------------------

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

module Definition05 where

postulate
  D   : Set
  _≡_ : D → D → Set
  op  : D → D
  a   : D

b : D
b = a
{-# ATP definition b #-}

c : D
c = op b
{-# ATP definition c #-}

-- We test the use of an ATP definition inside other ATP definition.
postulate foo : c ≡ op a
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Bound.Lower (A : Set) where

data Bound : Set where
  bot : Bound
  val : A → Bound

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- 2014-05-16 Andreas: Question mark not recognized by emacs

module _ where

data Nat : Set where
  suc : Nat → Nat

data Fin : Nat → Set where
  zero : ∀ n → Fin (suc n)

test : ∀ n → Fin n → Set
test .? (zero n) = Nat

-- The questionmark in the dot pattern is not recognized by emacs-mode.

-- This cannot be tested by test/interaction, but I still put the test case here.


text:
module BHeap.Order {A : Set}(_≤_ : A → A → Set) where

open import BHeap _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.Nat

_≺_ : {b b' : Bound} → BHeap b → BHeap b' → Set
h ≺ h' = # h <′ # h'

data Acc {b' : Bound}(h' : BHeap b') : Set where
  acc : (∀ {b} h → (_≺_ {b} {b'} h h') → Acc h) → Acc h'


text:
open import Data.Boolean
open import Type

module Data.BinaryTree.Heap {ℓ} {T : Type{ℓ}} (_≤?_ : T → T → Bool) where

import      Lvl
open import Data hiding (empty)
open import Data.BinaryTree

BinaryHeap = BinaryTree (Unit{Lvl.𝟎}) (T)

private variable ℓᵣ : Lvl.Level
private variable R : Type{ℓᵣ}

open import Data.Option
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional as Fn using (_∘_ ; _∘₂_ ; _$_)

merge : BinaryHeap → BinaryHeap → BinaryHeap
merge (Leaf <>)         (Leaf <>)      = Leaf <>
merge x@(Node _ _ _)    (Leaf <>)      = x
merge (Leaf <>)         y@(Node _ _ _) = y
merge x@(Node xa xl xr) y@(Node ya yl yr) with (xa ≤? ya) | (\_ → merge y xr) | (\_ → merge x yr)
... | 𝑇 | 𝑇-branch | _ = Node xa (𝑇-branch(<>{Lvl.𝟎})) xl
... | 𝐹 | _ | 𝐹-branch = Node ya (𝐹-branch(<>{Lvl.𝟎})) yl

insert : T → BinaryHeap → BinaryHeap
insert a = merge(singleton a)

pop : BinaryHeap → Option(T ⨯ BinaryHeap)
pop (Leaf <>)    = None
pop (Node a l r) = Some(a , merge l r)

{-# TERMINATING #-}
foldOrdered : (T → R → R) → R → BinaryHeap → R
foldOrdered(_▫_) id (Leaf <>)    = id
foldOrdered(_▫_) id (Node a l r) = a ▫ foldOrdered(_▫_) id (merge l r)

filterFold : (T → R → Option(R)) → R → BinaryHeap → (R ⨯ BinaryHeap)
filterFold (_▫_) r₀ (Leaf <>)    = (r₀ , Leaf <>)
filterFold (_▫_) r₀ (Node a l r)
  with (r₁ , il) ← filterFold (_▫_) r₀ l
  with (r₂ , ir) ← filterFold (_▫_) r₁ r
  with (a ▫ r₂)
... | Some r₃ = (r₃ , merge il ir)
... | None    = (r₂ , Node a il ir)

filter : (T → Bool) → BinaryHeap → BinaryHeap
filter f = Tuple.right ∘ filterFold (\{a <> → (\{𝐹 → None ; 𝑇 → Some <>}) $ f(a)}) (<>{Lvl.𝟎})

open import Data.List
import      Data.List.Functions as List

separate : (T → Bool) → BinaryHeap → (List(T) ⨯ BinaryHeap)
separate f = filterFold (\a l → (\{𝐹 → None ; 𝑇 → Some(a ⊰ l)}) $ f(a)) ∅

update : (T → Bool) → (T → T) → BinaryHeap → BinaryHeap
update p f a with (as , b) ← separate p a = List.foldᵣ insert b (List.map f as)


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

-- Thm: (∃x)A(x), (∀x)(A(x) ⇒ B(x)) ⊢ (∃x)B(x)

-- From: Elliott Mendelson. Introduction to mathematical logic. Chapman &
-- Hall, 4th edition, 1997, p. 155.

-- Rule A4: (∀x)A(x) ⇒ A(t) (with some conditions)
-- Rule E4: A(t) ⇒ (∃x)A(x) (with some conditions)
-- Rule C: From (∃x)A(x) to A(t) (with some conditions)

-- 1. (∃x)A(x)          Hyp
-- 2. (∀x)(A(x) ⇒ B(x)) Hyp
-- 3. A(b)              1, rule C
-- 4. A(b) ⇒ B(b)       2, rule A4
-- 5. B(b)              4,3 MP
-- 6. (∃x)B(x)          5, rule E4

module FOT.Common.FOL.Existential.Witness where

postulate
  D   : Set
  A B : D → Set

module Witness where

  infixr 7 _,_

  data ∃ (A : D → Set) : Set where
    _,_ : ∀ x → A x → ∃ A

  ∃-elim : {A : D → Set}{B : Set} → ∃ A → (∀ x → A x → B) → B
  ∃-elim (x , Ax) h = h x Ax

  -- A proof using the existential elimination.
  prf₁ : ∃ A → (∀ {x} → A x → B x) → ∃ B
  prf₁ h₁ h₂ = ∃-elim h₁ (λ x Ax → x , (h₂ Ax))

  -- A proof using pattern matching.
  prf₂ : ∃ A → (∀ {x} → A x → B x) → ∃ B
  prf₂ (x , Ax) h = x , h Ax

module NonWitness₁ where

  data ∃ (A : D → Set) : Set where
    ∃-intro : ∀ {x} → A x → ∃ A

  ∃-elim : {A : D → Set}{B : Set} → ∃ A → (∀ {x} → A x → B) → B
  ∃-elim (∃-intro Ax) h = h Ax

  -- A proof using the existential elimination.
  prf₁ : ∃ A → (∀ {x} → A x → B x) → ∃ B
  prf₁ h₁ h₂ = ∃-elim h₁ (λ Ax → ∃-intro (h₂ Ax))

  -- A proof using pattern matching.
  prf₂ : ∃ A → (∀ {x} → A x → B x) → ∃ B
  prf₂ (∃-intro Ax) h = ∃-intro (h Ax)

module NonWitness₂ where

  -- We add 3 to the fixities of the Agda standard library 0.8.1 (see
  -- Relation/Nullary/Core.agda).
  infix 6 ¬_

  -- The empty type.
  data ⊥ : Set where

  ⊥-elim : {A : Set} → ⊥ → A
  ⊥-elim ()

  ¬_ : Set → Set
  ¬ A = A → ⊥

  ∃ : (D → Set) → Set
  ∃ A = ¬ (∀ x → ¬ (A x))

  prf : ∃ A → (∀ x → A x → B x) → ∃ B
  prf h₁ h₂ h₃ = h₁ (λ x Ax → h₃ x (h₂ x Ax))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc