text:
------------------------------------------------------------------------
-- Context extensions with the leftmost element in the outermost
-- position
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Context.Extension.Left
  {i u e} (Uni : IndexedUniverse i u e) where

import deBruijn.Context.Basics          as Basics
import deBruijn.Context.Extension.Right as Right
open import Function
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open Basics Uni
open Right  Uni
open P.≡-Reasoning

------------------------------------------------------------------------
-- Context extensions along with various operations making use of them

-- Context extensions.

infixr 5 _◅_

data Ctxt₊ (Γ : Ctxt) : Set (i ⊔ u ⊔ e) where
  ε   : Ctxt₊ Γ
  _◅_ : (σ : Type Γ) (Γ₊ : Ctxt₊ (Γ ▻ σ)) → Ctxt₊ Γ

-- A synonym.

ε₊[_] : (Γ : Ctxt) → Ctxt₊ Γ
ε₊[ _ ] = ε

-- Appends a context extension to a context.

infixl 5 _++₊_

_++₊_ : (Γ : Ctxt) → Ctxt₊ Γ → Ctxt
Γ ++₊ ε        = Γ
Γ ++₊ (σ ◅ Γ₊) = Γ ▻ σ ++₊ Γ₊

-- The following operations append a context extension to a context
-- extension.

infixl 5 _₊++₊_ _⁺++₊_

_₊++₊_ : ∀ {Γ} Γ₊ → Ctxt₊ (Γ ++₊ Γ₊) → Ctxt₊ Γ
ε        ₊++₊ Γ₊₊ = Γ₊₊
(σ ◅ Γ₊) ₊++₊ Γ₊₊ = σ ◅ (Γ₊ ₊++₊ Γ₊₊)

_⁺++₊_ : ∀ {Γ} Γ⁺ → Ctxt₊ (Γ ++⁺ Γ⁺) → Ctxt₊ Γ
ε      ⁺++₊ Γ₊ = Γ₊
Γ⁺ ▻ σ ⁺++₊ Γ₊ = Γ⁺ ⁺++₊ (σ ◅ Γ₊)

-- Application of context morphisms to context extensions.

infixl 8 _/̂₊_

_/̂₊_ : ∀ {Γ Δ} → Ctxt₊ Γ → Γ ⇨̂ Δ → Ctxt₊ Δ
ε        /̂₊ ρ̂ = ε
(σ ◅ Γ₊) /̂₊ ρ̂ = σ /̂ ρ̂ ◅ Γ₊ /̂₊ ρ̂ ↑̂

-- N-ary lifting of context morphisms.

infixl 10 _↑̂₊_

_↑̂₊_ : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) Γ₊ → Γ ++₊ Γ₊ ⇨̂ Δ ++₊ Γ₊ /̂₊ ρ̂
ρ̂ ↑̂₊ ε        = ρ̂
ρ̂ ↑̂₊ (σ ◅ Γ₊) = ρ̂ ↑̂ ↑̂₊ Γ₊

-- N-ary weakening.

ŵk₊ : ∀ {Γ} Γ₊ → Γ ⇨̂ Γ ++₊ Γ₊
ŵk₊ ε        = îd
ŵk₊ (σ ◅ Γ₊) = ŵk[ σ ] ∘̂ ŵk₊ Γ₊

------------------------------------------------------------------------
-- Equality

-- Equality of context extensions.

record [Ctxt₊] : Set (i ⊔ u ⊔ e) where
  constructor [_]
  field
    {Γ} : Ctxt
    Γ₊  : Ctxt₊ Γ

infix 4 _≅-Ctxt₊_

_≅-Ctxt₊_ : ∀ {Γ₁} (Γ₊₁ : Ctxt₊ Γ₁)
              {Γ₂} (Γ₊₂ : Ctxt₊ Γ₂) → Set _
Γ₊₁ ≅-Ctxt₊ Γ₊₂ = _≡_ {A = [Ctxt₊]} [ Γ₊₁ ] [ Γ₊₂ ]

≅-Ctxt₊-⇒-≡ : ∀ {Γ} {Γ₊₁ Γ₊₂ : Ctxt₊ Γ} →
              Γ₊₁ ≅-Ctxt₊ Γ₊₂ → Γ₊₁ ≡ Γ₊₂
≅-Ctxt₊-⇒-≡ P.refl = P.refl

-- Certain uses of substitutivity can be removed.

drop-subst-Ctxt₊ : ∀ {a} {A : Set a} {x₁ x₂}
                   (f : A → Ctxt) {Γ₊} (x₁≡x₂ : x₁ ≡ x₂) →
                   P.subst (λ x → Ctxt₊ (f x)) x₁≡x₂ Γ₊ ≅-Ctxt₊ Γ₊
drop-subst-Ctxt₊ f P.refl = P.refl

------------------------------------------------------------------------
-- Some congruences

ε₊-cong : ∀ {Γ₁ Γ₂} → Γ₁ ≅-Ctxt Γ₂ → ε₊[ Γ₁ ] ≅-Ctxt₊ ε₊[ Γ₂ ]
ε₊-cong P.refl = P.refl

◅-cong : ∀ {Γ₁ σ₁} {Γ₊₁ : Ctxt₊ (Γ₁ ▻ σ₁)}
           {Γ₂ σ₂} {Γ₊₂ : Ctxt₊ (Γ₂ ▻ σ₂)} →
         Γ₊₁ ≅-Ctxt₊ Γ₊₂ → σ₁ ◅ Γ₊₁ ≅-Ctxt₊ σ₂ ◅ Γ₊₂
◅-cong P.refl = P.refl

++₊-cong : ∀ {Γ₁} {Γ₊₁ : Ctxt₊ Γ₁} {Γ₂} {Γ₊₂ : Ctxt₊ Γ₂} →
           Γ₊₁ ≅-Ctxt₊ Γ₊₂ → Γ₁ ++₊ Γ₊₁ ≅-Ctxt Γ₂ ++₊ Γ₊₂
++₊-cong P.refl = P.refl

₊++₊-cong : ∀ {Γ₁ Γ₊₁} {Γ₊₊₁ : Ctxt₊ (Γ₁ ++₊ Γ₊₁)}
              {Γ₂ Γ₊₂} {Γ₊₊₂ : Ctxt₊ (Γ₂ ++₊ Γ₊₂)} →
            Γ₊₁ ≅-Ctxt₊ Γ₊₂ → Γ₊₊₁ ≅-Ctxt₊ Γ₊₊₂ →
            Γ₊₁ ₊++₊ Γ₊₊₁ ≅-Ctxt₊ Γ₊₂ ₊++₊ Γ₊₊₂
₊++₊-cong P.refl P.refl = P.refl

⁺++₊-cong : ∀ {Γ₁ Γ⁺₁} {Γ₊₁ : Ctxt₊ (Γ₁ ++⁺ Γ⁺₁)}
              {Γ₂ Γ⁺₂} {Γ₊₂ : Ctxt₊ (Γ₂ ++⁺ Γ⁺₂)} →
            Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → Γ₊₁ ≅-Ctxt₊ Γ₊₂ →
            Γ⁺₁ ⁺++₊ Γ₊₁ ≅-Ctxt₊ Γ⁺₂ ⁺++₊ Γ₊₂
⁺++₊-cong P.refl P.refl = P.refl

/̂₊-cong : ∀ {Γ₁ Δ₁} {Γ₊₁ : Ctxt₊ Γ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁}
            {Γ₂ Δ₂} {Γ₊₂ : Ctxt₊ Γ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} →
          Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ̂₁ ≅-⇨̂ ρ̂₂ → Γ₊₁ /̂₊ ρ̂₁ ≅-Ctxt₊ Γ₊₂ /̂₊ ρ̂₂
/̂₊-cong P.refl P.refl = P.refl

↑̂₊-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {Γ₊₁ : Ctxt₊ Γ₁}
            {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {Γ₊₂ : Ctxt₊ Γ₂} →
          ρ̂₁ ≅-⇨̂ ρ̂₂ → Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ̂₁ ↑̂₊ Γ₊₁ ≅-⇨̂ ρ̂₂ ↑̂₊ Γ₊₂
↑̂₊-cong P.refl P.refl = P.refl

ŵk₊-cong : ∀ {Γ₁} {Γ₊₁ : Ctxt₊ Γ₁} {Γ₂} {Γ₊₂ : Ctxt₊ Γ₂} →
           Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ŵk₊ Γ₊₁ ≅-⇨̂ ŵk₊ Γ₊₂
ŵk₊-cong P.refl = P.refl

------------------------------------------------------------------------
-- Some properties

abstract

  -- Γ ++₊_ has at most one right identity.

  private

    ++₊-right-identity-unique′ :
      ∀ {Γ} Γ⁺ Γ₊ → Γ ≅-Ctxt Γ ++⁺ Γ⁺ ++₊ Γ₊ → Γ₊ ≅-Ctxt₊ ε₊[ Γ ++⁺ Γ⁺ ]
    ++₊-right-identity-unique′ Γ⁺ ε        _  = P.refl
    ++₊-right-identity-unique′ Γ⁺ (σ ◅ Γ₊) eq
      with ++₊-right-identity-unique′ (Γ⁺ ▻ σ) Γ₊ eq
    ++₊-right-identity-unique′ Γ⁺ (σ ◅ .ε) eq | P.refl
      with ++⁺-right-identity-unique (Γ⁺ ▻ σ) eq
    ... | ()

  ++₊-right-identity-unique :
    ∀ {Γ} Γ₊ → Γ ≅-Ctxt Γ ++₊ Γ₊ → Γ₊ ≅-Ctxt₊ ε₊[ Γ ]
  ++₊-right-identity-unique Γ₊ = ++₊-right-identity-unique′ ε Γ₊

  -- Γ ++₊_ is left cancellative.

  private

    cancel-++₊-left′ : ∀ {Γ} Γ⁺₁ Γ₊₁ Γ⁺₂ Γ₊₂ →
                       Γ ++⁺ Γ⁺₁ ++₊ Γ₊₁ ≅-Ctxt Γ ++⁺ Γ⁺₂ ++₊ Γ₊₂ →
                       Γ⁺₁ ⁺++₊ Γ₊₁ ≅-Ctxt₊ Γ⁺₂ ⁺++₊ Γ₊₂
    cancel-++₊-left′ Γ⁺₁ ε          Γ⁺₂ ε          eq = ⁺++₊-cong (cancel-++⁺-left Γ⁺₁ Γ⁺₂ eq) (ε₊-cong eq)
    cancel-++₊-left′ Γ⁺₁ (σ₁ ◅ Γ₊₁) Γ⁺₂ (σ₂ ◅ Γ₊₂) eq = cancel-++₊-left′ (Γ⁺₁ ▻ σ₁) Γ₊₁ (Γ⁺₂ ▻ σ₂) Γ₊₂ eq
    cancel-++₊-left′ Γ⁺₁ ε          Γ⁺₂ (σ₂ ◅ Γ₊₂) eq = cancel-++₊-left′  Γ⁺₁       ε   (Γ⁺₂ ▻ σ₂) Γ₊₂ eq
    cancel-++₊-left′ Γ⁺₁ (σ₁ ◅ Γ₊₁) Γ⁺₂ ε          eq = cancel-++₊-left′ (Γ⁺₁ ▻ σ₁) Γ₊₁  Γ⁺₂       ε   eq

  cancel-++₊-left : ∀ {Γ} (Γ₊₁ Γ₊₂ : Ctxt₊ Γ) →
                    Γ ++₊ Γ₊₁ ≅-Ctxt Γ ++₊ Γ₊₂ → Γ₊₁ ≅-Ctxt₊ Γ₊₂
  cancel-++₊-left Γ₊₁ Γ₊₂ = cancel-++₊-left′ ε Γ₊₁ ε Γ₊₂

  -- _++₊_/_₊++₊_ are associative.

  ++₊-++₊ : ∀ {Γ} Γ₊ Γ₊₊ → Γ ++₊ Γ₊ ++₊ Γ₊₊ ≅-Ctxt Γ ++₊ (Γ₊ ₊++₊ Γ₊₊)
  ++₊-++₊ ε        Γ₊₊ = P.refl
  ++₊-++₊ (σ ◅ Γ₊) Γ₊₊ = ++₊-++₊ Γ₊ Γ₊₊

  -- The identity substitution has no effect.

  /̂₊-îd : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → Γ₊ /̂₊ îd ≅-Ctxt₊ Γ₊
  /̂₊-îd ε        = P.refl
  /̂₊-îd (σ ◅ Γ₊) = ◅-cong (/̂₊-îd Γ₊)

  -- The n-ary lifting of the identity substitution is the identity
  -- substitution.

  îd-↑̂₊ : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → îd ↑̂₊ Γ₊ ≅-⇨̂ îd[ Γ ++₊ Γ₊ ]
  îd-↑̂₊ ε        = P.refl
  îd-↑̂₊ (σ ◅ Γ₊) = begin
    [ îd ↑̂ ↑̂₊ Γ₊ ]  ≡⟨ P.refl ⟩
    [ îd ↑̂₊ Γ₊   ]  ≡⟨ îd-↑̂₊ Γ₊ ⟩
    [ îd         ]  ∎

  -- The identity substitution has no effect even if lifted.

  /̂-îd-↑̂₊ : ∀ {Γ} Γ₊ (σ : Type (Γ ++₊ Γ₊)) → σ /̂ îd ↑̂₊ Γ₊ ≅-Type σ
  /̂-îd-↑̂₊ Γ₊ σ = begin
    [ σ /̂ îd ↑̂₊ Γ₊ ]  ≡⟨ /̂-cong (P.refl {x = [ σ ]}) (îd-↑̂₊ Γ₊) ⟩
    [ σ /̂ îd       ]  ≡⟨ P.refl ⟩
    [ σ            ]  ∎

  -- Applying two substitutions is equivalent to applying their
  -- composition.

  /̂₊-∘̂ : ∀ {Γ Δ Ε} Γ₊ (ρ̂₁ : Γ ⇨̂ Δ) (ρ̂₂ : Δ ⇨̂ Ε) →
         Γ₊ /̂₊ ρ̂₁ ∘̂ ρ̂₂ ≅-Ctxt₊ Γ₊ /̂₊ ρ̂₁ /̂₊ ρ̂₂
  /̂₊-∘̂ ε        ρ̂₁ ρ̂₂ = P.refl
  /̂₊-∘̂ (σ ◅ Γ₊) ρ̂₁ ρ̂₂ = ◅-cong (/̂₊-∘̂ Γ₊ (ρ̂₁ ↑̂) (ρ̂₂ ↑̂))

  -- _↑̂₊_ distributes over _∘̂_.

  ∘̂-↑̂₊ : ∀ {Γ Δ Ε} (ρ̂₁ : Γ ⇨̂ Δ) (ρ̂₂ : Δ ⇨̂ Ε) Γ₊ →
         (ρ̂₁ ∘̂ ρ̂₂) ↑̂₊ Γ₊ ≅-⇨̂ ρ̂₁ ↑̂₊ Γ₊ ∘̂ ρ̂₂ ↑̂₊ (Γ₊ /̂₊ ρ̂₁)
  ∘̂-↑̂₊ ρ̂₁ ρ̂₂ ε        = P.refl
  ∘̂-↑̂₊ ρ̂₁ ρ̂₂ (σ ◅ Γ₊) = begin
    [ (ρ̂₁ ∘̂ ρ̂₂) ↑̂ ↑̂₊ Γ₊                     ]  ≡⟨ P.refl ⟩
    [ (ρ̂₁ ↑̂ ∘̂ ρ̂₂ ↑̂) ↑̂₊ Γ₊                   ]  ≡⟨ ∘̂-↑̂₊ (ρ̂₁ ↑̂) (ρ̂₂ ↑̂) Γ₊ ⟩
    [ (ρ̂₁ ↑̂ ↑̂₊ Γ₊) ∘̂ (ρ̂₂ ↑̂ ↑̂₊ (Γ₊ /̂₊ ρ̂₁ ↑̂)) ]  ∎

  -- A corollary.

  /̂-↑̂₊-/̂-ŵk-↑̂₊ : ∀ {Γ Δ} σ (ρ̂ : Γ ⇨̂ Δ) (Γ₊ : Ctxt₊ Γ) τ →
                 τ /̂ ρ̂ ↑̂₊ Γ₊ /̂ ŵk[ σ /̂ ρ̂ ] ↑̂₊ (Γ₊ /̂₊ ρ̂) ≅-Type
                 τ /̂ ŵk[ σ ] ↑̂₊ Γ₊ /̂ ρ̂ ↑̂ ↑̂₊ (Γ₊ /̂₊ ŵk)
  /̂-↑̂₊-/̂-ŵk-↑̂₊ σ ρ̂ Γ₊ τ = /̂-cong (P.refl {x = [ τ ]}) (begin
    [ ρ̂ ↑̂₊ Γ₊ ∘̂ ŵk ↑̂₊ (Γ₊ /̂₊ ρ̂)         ]  ≡⟨ P.sym $ ∘̂-↑̂₊ ρ̂ ŵk Γ₊ ⟩
    [ (ρ̂ ∘̂ ŵk) ↑̂₊ Γ₊                    ]  ≡⟨ P.refl ⟩
    [ (ŵk[ σ ] ∘̂ ρ̂ ↑̂) ↑̂₊ Γ₊             ]  ≡⟨ ∘̂-↑̂₊ ŵk[ σ ] (ρ̂ ↑̂) Γ₊ ⟩
    [ ŵk[ σ ] ↑̂₊ Γ₊ ∘̂ ρ̂ ↑̂ ↑̂₊ (Γ₊ /̂₊ ŵk) ]  ∎)

  -- ŵk₊ commutes (modulo lifting) with arbitrary context morphisms.

  ∘̂-ŵk₊ : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) Γ₊ →
          ρ̂ ∘̂ ŵk₊ (Γ₊ /̂₊ ρ̂) ≅-⇨̂ ŵk₊ Γ₊ ∘̂ ρ̂ ↑̂₊ Γ₊
  ∘̂-ŵk₊ ρ̂ ε        = P.refl
  ∘̂-ŵk₊ ρ̂ (σ ◅ Γ₊) = begin
    [ ρ̂ ∘̂ ŵk ∘̂ ŵk₊ (Γ₊ /̂₊ ρ̂ ↑̂)         ]  ≡⟨ P.refl ⟩
    [ ŵk[ σ ] ∘̂ ρ̂ ↑̂ ∘̂ ŵk₊ (Γ₊ /̂₊ ρ̂ ↑̂)  ]  ≡⟨ ∘̂-cong (P.refl {x = [ ŵk ]}) (∘̂-ŵk₊ (ρ̂ ↑̂) Γ₊) ⟩
    [ ŵk ∘̂ ŵk₊ Γ₊ ∘̂ ρ̂ ↑̂ ↑̂₊ Γ₊          ]  ∎

  -- ŵk₊ is homomorphic with respect to _₊++₊_/_∘̂_.

  ŵk₊-₊++₊ : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) (Γ₊₊ : Ctxt₊ (Γ ++₊ Γ₊)) →
             ŵk₊ (Γ₊ ₊++₊ Γ₊₊) ≅-⇨̂ ŵk₊ Γ₊ ∘̂ ŵk₊ Γ₊₊
  ŵk₊-₊++₊ ε        Γ₊₊ = P.refl
  ŵk₊-₊++₊ (σ ◅ Γ₊) Γ₊₊ = ∘̂-cong (P.refl {x = [ ŵk ]}) (ŵk₊-₊++₊ Γ₊ Γ₊₊)

  -- Two n-ary liftings can be merged into one.

  ↑̂₊-₊++₊ : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) Γ₊ Γ₊₊ →
            ρ̂ ↑̂₊ (Γ₊ ₊++₊ Γ₊₊) ≅-⇨̂ ρ̂ ↑̂₊ Γ₊ ↑̂₊ Γ₊₊
  ↑̂₊-₊++₊ ρ̂ ε        Γ₊₊ = P.refl
  ↑̂₊-₊++₊ ρ̂ (σ ◅ Γ₊) Γ₊₊ = ↑̂₊-₊++₊ (ρ̂ ↑̂) Γ₊ Γ₊₊

  -- _/̂₊_ distributes over _₊++₊_ (sort of).

  ++₊-₊++₊-/̂₊ :
    ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) Γ₊ Γ₊₊ →
    Δ ++₊ (Γ₊ ₊++₊ Γ₊₊) /̂₊ ρ̂ ≅-Ctxt Δ ++₊ Γ₊ /̂₊ ρ̂ ++₊ Γ₊₊ /̂₊ ρ̂ ↑̂₊ Γ₊
  ++₊-₊++₊-/̂₊         ρ̂ ε        Γ₊₊ = P.refl
  ++₊-₊++₊-/̂₊ {Δ = Δ} ρ̂ (σ ◅ Γ₊) Γ₊₊ = ++₊-₊++₊-/̂₊ (ρ̂ ↑̂) Γ₊ Γ₊₊

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
{-

Macros (autoDesc, AutoStructure, AutoEquivStr, autoUnivalentStr) for automatically generating structure definitions.

For example:

  autoDesc (λ (X : Type₀) → X → X × ℕ)   ↦   recvar (var , constant ℕ)

We prefer to use the constant structure whenever possible, e.g., [autoDesc (λ (X : Type₀) → ℕ → ℕ)]
is [constant (ℕ → ℕ)] rather than [param ℕ (constant ℕ)].

Writing [auto* (λ X → ⋯)] doesn't seem to work, but [auto* (λ (X : Type ℓ) → ⋯)] does.

-}
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Structures.Auto where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.List
open import Cubical.Data.Bool
open import Cubical.Data.Maybe

open import Cubical.Structures.Macro as Macro

import Agda.Builtin.Reflection as R

-- Magic number
private
  FUEL = 10000

-- Mark part of a structure definition as functorial
abstract
  Funct[_] : ∀ {ℓ} → Type ℓ → Type ℓ
  Funct[ A ] = A

-- Some reflection utilities
private
  _>>=_ = R.bindTC
  _<|>_ = R.catchTC

  _>>_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → R.TC A → R.TC B → R.TC B
  f >> g = f >>= λ _ → g

  infixl 4 _>>=_ _>>_ _<|>_

  varg : ∀ {ℓ} {A : Type ℓ} → A → R.Arg A
  varg = R.arg (R.arg-info R.visible R.relevant)

  tLevel = R.def (quote Level) []

  tType : R.Term → R.Term
  tType ℓ = R.def (quote Type) [ varg ℓ ]

  tFuncDesc : R.Term → R.Term
  tFuncDesc ℓ = R.def (quote FuncDesc) [ varg ℓ ]

  tDesc : R.Term → R.Term
  tDesc ℓ = R.def (quote Desc) [ varg ℓ ]

  func : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
  func ℓ ℓ' = Type ℓ → Type ℓ'

  tStruct : R.Term → R.Term → R.Term
  tStruct ℓ ℓ' = R.def (quote func) (varg ℓ ∷ varg ℓ' ∷ [])

  newMeta = R.checkType R.unknown

-- We try to build a descriptor by unifying the provided structure with combinators we're aware of. We
-- redefine the structure combinators as the *Shape terms below so that we don't depend on the specific way
-- these are defined in other files (order of implicit arguments and so on); the syntactic analysis that goes
-- on here means that we would get mysterious errors if those changed.
private
  constantShape : ∀ {ℓ'} (ℓ : Level) (A : Type ℓ') → (Type ℓ → Type ℓ')
  constantShape _ A _ = A

  pointedShape : (ℓ : Level) → Type ℓ → Type ℓ
  pointedShape _ X = X

  joinShape : ∀ {ℓ₀ ℓ₁} (ℓ : Level)
    → (Type ℓ → Type ℓ₀) → (Type ℓ → Type ℓ₁) → Type ℓ → Type (ℓ-max ℓ₀ ℓ₁)
  joinShape _ A₀ A₁ X = A₀ X × A₁ X

  paramShape : ∀ {ℓ₀ ℓ'} (ℓ : Level)
    → Type ℓ' → (Type ℓ → Type ℓ₀) → Type ℓ → Type (ℓ-max ℓ' ℓ₀)
  paramShape _ A A₀ X = A → A₀ X

  recvarShape : ∀ {ℓ₀} (ℓ : Level)
    → (Type ℓ → Type ℓ₀) → Type ℓ → Type (ℓ-max ℓ ℓ₀)
  recvarShape _ A₀ X = X → A₀ X

  maybeShape : ∀ {ℓ₀} (ℓ : Level)
    → (Type ℓ → Type ℓ₀) → Type ℓ → Type ℓ₀
  maybeShape _ A₀ X = Maybe (A₀ X)

  functorialShape : ∀ {ℓ₀} (ℓ : Level)
    → (Type ℓ → Type ℓ₀) → Type ℓ → Type ℓ₀
  functorialShape _ A₀ X = Funct[ A₀ X ]

private
  -- Build functorial structure descriptor from a function [t : Type ℓ → Type ℓ']
  buildFuncDesc : ℕ → R.Term → R.Term → R.Term → R.TC R.Term
  buildFuncDesc zero ℓ ℓ' t = R.typeError (R.strErr "Ran out of fuel! at \n" ∷ R.termErr t ∷ [])
  buildFuncDesc (suc fuel) ℓ ℓ' t =
    tryConstant t <|> tryPointed t <|> tryJoin t <|> tryParam t <|> tryMaybe t <|>
    R.typeError (R.strErr "Can't automatically generate a functorial structure for\n" ∷ R.termErr t ∷ [])
    where
    tryConstant : R.Term → R.TC R.Term
    tryConstant t =
      newMeta (tType ℓ') >>= λ A →
      R.unify t (R.def (quote constantShape) (varg ℓ ∷ varg A ∷ [])) >>
      R.returnTC (R.con (quote FuncDesc.constant) (varg A ∷ []))

    tryPointed : R.Term → R.TC R.Term
    tryPointed t =
      R.unify t (R.def (quote pointedShape) (varg ℓ ∷ [])) >>
      R.returnTC (R.con (quote FuncDesc.var) [])

    tryParam : R.Term → R.TC R.Term
    tryParam t =
      newMeta (tType R.unknown) >>= λ A →
      newMeta tLevel >>= λ ℓ₀ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      R.unify t (R.def (quote paramShape) (varg ℓ ∷ varg A ∷ varg A₀ ∷ [])) >>
      buildFuncDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      R.returnTC (R.con (quote FuncDesc.param) (varg A ∷ varg d₀ ∷ []))

    tryJoin : R.Term → R.TC R.Term
    tryJoin t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta tLevel >>= λ ℓ₁ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      newMeta (tStruct ℓ ℓ₁) >>= λ A₁ →
      R.unify t (R.def (quote joinShape) (varg ℓ ∷ varg A₀ ∷ varg A₁ ∷ [])) >>
      buildFuncDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      buildFuncDesc fuel ℓ ℓ₁ A₁ >>= λ d₁ →
      R.returnTC (R.con (quote FuncDesc._,_) (varg d₀ ∷ varg d₁ ∷ []))

    tryMaybe : R.Term → R.TC R.Term
    tryMaybe t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      R.unify t (R.def (quote maybeShape) (varg ℓ ∷ varg A₀ ∷ [])) >>
      buildFuncDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      R.returnTC (R.con (quote FuncDesc.maybe) (varg d₀ ∷ []))

  autoFuncDesc' : R.Term → R.Term → R.TC Unit
  autoFuncDesc' t hole =
    R.inferType hole >>= λ H →
    newMeta tLevel >>= λ ℓ →
    newMeta tLevel >>= λ ℓ' →
    R.unify (tFuncDesc ℓ) H >>
    R.checkType t (tStruct ℓ ℓ') >>
    buildFuncDesc FUEL ℓ ℓ' t >>= R.unify hole

  -- Build structure descriptor from a function [t : Type ℓ → Type ℓ']
  buildDesc : ℕ → R.Term → R.Term → R.Term → R.TC R.Term
  buildDesc zero ℓ ℓ' t = R.typeError (R.strErr "Ran out of fuel! at \n" ∷ R.termErr t ∷ [])
  buildDesc (suc fuel) ℓ ℓ' t =
    tryConstant t <|> tryPointed t <|> tryJoin t <|> tryParam t <|> tryRecvar t <|> tryMaybe t <|>
    tryFunct t <|>
    R.typeError (R.strErr "Can't automatically generate a structure for\n" ∷ R.termErr t ∷ [])
    where
    tryConstant : R.Term → R.TC R.Term
    tryConstant t =
      newMeta (tType ℓ') >>= λ A →
      R.unify t (R.def (quote constantShape) (varg ℓ ∷ varg A ∷ [])) >>
      R.returnTC (R.con (quote Desc.constant) (varg A ∷ []))

    tryPointed : R.Term → R.TC R.Term
    tryPointed t =
      R.unify t (R.def (quote pointedShape) (varg ℓ ∷ [])) >>
      R.returnTC (R.con (quote Desc.var) [])

    tryJoin : R.Term → R.TC R.Term
    tryJoin t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta tLevel >>= λ ℓ₁ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      newMeta (tStruct ℓ ℓ₁) >>= λ A₁ →
      R.unify t (R.def (quote joinShape) (varg ℓ ∷ varg A₀ ∷ varg A₁ ∷ [])) >>
      buildDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      buildDesc fuel ℓ ℓ₁ A₁ >>= λ d₁ →
      R.returnTC (R.con (quote Desc._,_) (varg d₀ ∷ varg d₁ ∷ []))

    tryParam : R.Term → R.TC R.Term
    tryParam t =
      newMeta (tType R.unknown) >>= λ A →
      newMeta tLevel >>= λ ℓ₀ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      R.unify t (R.def (quote paramShape) (varg ℓ ∷ varg A ∷ varg A₀ ∷ [])) >>
      buildDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      R.returnTC (R.con (quote Desc.param) (varg A ∷ varg d₀ ∷ []))

    tryRecvar : R.Term → R.TC R.Term
    tryRecvar t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      R.unify t (R.def (quote recvarShape) (varg ℓ ∷ varg A₀ ∷ [])) >>
      buildDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      R.returnTC (R.con (quote Desc.recvar) (varg d₀ ∷ []))

    tryMaybe : R.Term → R.TC R.Term
    tryMaybe t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      R.unify t (R.def (quote maybeShape) (varg ℓ ∷ varg A₀ ∷ [])) >>
      buildDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      R.returnTC (R.con (quote Desc.maybe) (varg d₀ ∷ []))

    tryFunct : R.Term → R.TC R.Term
    tryFunct t =
      newMeta (tStruct ℓ ℓ') >>= λ A₀ →
      R.unify t (R.def (quote functorialShape) (varg ℓ ∷ varg A₀ ∷ [])) >>
      buildFuncDesc fuel ℓ ℓ' A₀ >>= λ d₀ →
      R.returnTC (R.con (quote Desc.functorial) (varg d₀ ∷ []))

  autoDesc' : R.Term → R.Term → R.TC Unit
  autoDesc' t hole =
    R.inferType hole >>= λ H →
    newMeta tLevel >>= λ ℓ →
    newMeta tLevel >>= λ ℓ' →
    R.unify (tDesc ℓ) H >>
    R.checkType t (tStruct ℓ ℓ') >>
    buildDesc FUEL ℓ ℓ' t >>= R.unify hole

macro
  -- (Type ℓ → Type ℓ₁) → FuncDesc ℓ
  autoFuncDesc : R.Term → R.Term → R.TC Unit
  autoFuncDesc = autoFuncDesc'

  -- (S : Type ℓ → Type ℓ₁) → ∀ {X Y} → (X → Y) → (S X → S Y)
  autoFuncAction : R.Term → R.Term → R.TC Unit
  autoFuncAction t hole =
    newMeta (tFuncDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote funcMacroAction) [ varg d ]) >>
    autoFuncDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → ∀ {X} s → autoFuncAction S (idfun X) s ≡ s
  autoFuncId : R.Term → R.Term → R.TC Unit
  autoFuncId t hole =
    newMeta (tFuncDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote funcMacroId) [ varg d ]) >>
    autoFuncDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → Desc ℓ
  autoDesc : R.Term → R.Term → R.TC Unit
  autoDesc = autoDesc'

  -- (S : Type ℓ → Type ℓ₁) → (Type ℓ → Type ℓ₁)
  -- Removes Funct[_] annotations
  AutoStructure : R.Term → R.Term → R.TC Unit
  AutoStructure t hole =
    newMeta (tDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote MacroStructure) [ varg d ]) >>
    autoDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → StrIso (AutoStructure S) _
  AutoEquivStr : R.Term → R.Term → R.TC Unit
  AutoEquivStr t hole =
    newMeta (tDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote MacroEquivStr) [ varg d ]) >>
    autoDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → SNS (AutoStructure S) (AutoEquivStr S)
  autoUnivalentStr : R.Term → R.Term → R.TC Unit
  autoUnivalentStr t hole =
    newMeta (tDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote MacroUnivalentStr) [ varg d ]) >>
    autoDesc' t d

ext: agda

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
module Preliminaries where

  open import Agda.Primitive using (Level) renaming (lzero to lZ; lsuc to lS; _⊔_ to lmax)

  -- ----------------------------------------------------------------------
  -- functions

  _o_ : {A B C : Set} → (B → C) → (A → B) → A → C
  g o f = \ x → g (f x)
  infixr 10 _o_

  -- ----------------------------------------------------------------------
  -- identity type

  data _==_ {l : Level} {A : Set l} (M : A) : A → Set l where
    Refl : M == M

  Id : {l : Level} {A : Set l} (M : A) → A → Set l
  Id M N = M == N

  {-# BUILTIN EQUALITY _==_ #-}
  {-# BUILTIN REFL Refl #-}

  transport : {l1 : Level} {l2 : Level} {A : Set l1} (B : A → Set l2)
              {a1 a2 : A} → a1 == a2 → (B a1 → B a2)
  transport B Refl = λ x → x

  ! : {l : Level} {A : Set l} {M N : A} → M == N → N == M
  ! Refl = Refl

  _∘_  : {l : Level} {A : Set l} {M N P : A}
      → N == P → M == N → M == P
  β ∘ Refl = β

  ap :  {l1 l2 : Level} {A : Set l1} {B : Set l2} {M N : A}
       (f : A → B) → M == N → (f M) == (f N)
  ap f Refl = Refl

  ap2 : {l1 l2 l3 : Level} {A : Set l1} {B : Set l2} {C : Set l3} {M N : A} {M' N' : B} (f : A -> B -> C) -> M == N -> M' == N' -> (f M M') == (f N N')
  ap2 f Refl Refl = Refl

  ap3 : {l1 l2 l3 l4 : Level} {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4} {M N : A} {M' N' : B} {M'' N'' : C}
      (f : A → B → C → D) → M == N → M' == N' → M'' == N'' → (f M M' M'') == (f N N' N'')
  ap3 f Refl Refl Refl = Refl

  postulate
    -- function extensionality
    λ=  : {l1 l2 : Level} {A : Set l1} {B : A -> Set l2} {f g : (x : A) -> B x} -> ((x : A) -> (f x) == (g x)) -> f == g
    -- function extensionality for implicit functions
    λ=i  : {l1 l2 : Level} {A : Set l1} {B : A -> Set l2} {f g : {x : A} -> B x} -> ((x : A) -> (f {x}) == (g {x})) -> _==_ {_}{ {x : A} → B x } f g

  private primitive primTrustMe : {l : Level} {A : Set l} {x y : A} -> x == y

  infixr 9 _==_

  infix  2 _∎
  infixr 2 _=⟨_⟩_

  _=⟨_⟩_ : {l : Level} {A : Set l} (x : A) {y z : A} → x == y → y == z → x == z
  _ =⟨ p1 ⟩ p2 = (p2 ∘ p1)

  _∎ : {l : Level} {A : Set l} (x : A) → x == x
  _∎ _ = Refl

  -- ----------------------------------------------------------------------
  -- product types

  record Unit : Set where
    constructor <>

  record Σ {l1 l2 : Level} {A : Set l1} (B : A -> Set l2) : Set (lmax l1 l2) where
    constructor _,_
    field
      fst : A
      snd : B fst
  open Σ public

  infixr 0 _,_

  _×_ : {l1 l2 : Level} → Set l1 -> Set l2 -> Set (lmax l1 l2)
  A × B = Σ (\ (_ : A) -> B)

  infixr 10 _×_

  -- ----------------------------------------------------------------------
  -- booleans

  data Bool : Set where
     True : Bool
     False : Bool
  {-# COMPILED_DATA Bool Bool True False #-}
  {-# BUILTIN BOOL  Bool  #-}
  {-# BUILTIN TRUE  True  #-}
  {-# BUILTIN FALSE False #-}

  -- ----------------------------------------------------------------------
  -- order

  data Order : Set where
    Less : Order
    Equal : Order
    Greater : Order

  -- ----------------------------------------------------------------------
  -- sums

  data Void : Set where

  abort : {A : Set} → Void → A
  abort ()

  data Either (A B : Set) : Set where
    Inl : A → Either A B
    Inr : B → Either A B

  DecEq : Set → Set
  DecEq A = (x y : A) → Either (x == y) (x == y → Void)

  -- ----------------------------------------------------------------------
  -- natural numbers

  module Nat where
    data Nat : Set where
      Z : Nat
      S : Nat -> Nat

    -- let's you use numerals for Nat
    {-# BUILTIN NATURAL Nat #-}

    _+_ : Nat → Nat → Nat
    Z + n = n
    (S m) + n = S (m + n)

    max : Nat → Nat → Nat
    max Z n = n
    max m Z = m
    max (S m) (S n) = S (max m n)

    equal : Nat → Nat → Bool
    equal Z Z = True
    equal Z (S _) = False
    equal (S _) Z = False
    equal (S m) (S n) = equal m n

    compare : Nat → Nat → Order
    compare Z Z = Equal
    compare Z (S m) = Less
    compare (S n) Z = Greater
    compare (S n) (S m) = compare n m

  open Nat public using (Nat ; Z ; S)

  -- ----------------------------------------------------------------------
  -- monad

  module Monad where

    record Monad : Set1 where
      field
        T : Set → Set
        return : ∀ {A} → A → T A
        _>>=_  : ∀ {A B} → T A → (A → T B) -> T B

  -- ----------------------------------------------------------------------
  -- options

  module Maybe where

    data Maybe {l : Level} (A : Set l) : Set l where
      Some : A → Maybe A
      None : Maybe A

    Monad : Monad.Monad
    Monad = record { T = Maybe; return = Some; _>>=_ = (λ {None _ → None; (Some v) f → f v}) }

  open Maybe public using (Maybe;Some;None)

  -- ----------------------------------------------------------------------
  -- lists

  module List where
    data List {l : Level} (A : Set l) : Set l where
      []  : List A
      _::_ : A -> List A -> List A

    {-# COMPILED_DATA List [] [] (:) #-}
    {-# BUILTIN LIST List #-}
    {-# BUILTIN NIL [] #-}
    {-# BUILTIN CONS _::_ #-}

    infixr 99 _::_

    _++_ : {A : Set} → List A → List A → List A
    [] ++ ys = ys
    (x :: xs) ++ ys = x :: (xs ++ ys)

    infixr 10 _++_

    map : {l1 l2 : Level} {A : Set l1} {B : Set l2} → (A → B) → List A → List B
    map f [] = []
    map f (x :: xs) = f x :: map f xs

    map-id : {l : Level} {A : Set l} (l : List A) → map (\ (x : A) → x) l == l
    map-id [] = Refl
    map-id (x :: l) with map (\ x -> x) l | map-id l
    ... | ._ | Refl = Refl

    ++-assoc : ∀ {A} (l1 l2 l3 : List A) → (l1 ++ l2) ++ l3 == l1 ++ (l2 ++ l3)
    ++-assoc [] l2 l3 = Refl
    ++-assoc (x :: xs) l2 l3 = ap (_::_ x) (++-assoc xs l2 l3)

  open List public using (List ; [] ; _::_)

  -- ----------------------------------------------------------------------
  -- characters

  module Char where

    postulate {- Agda Primitive -}
      Char : Set

    {-# BUILTIN CHAR Char #-}
    {-# COMPILED_TYPE Char Char #-}

    private
     primitive
      primCharToNat    : Char → Nat
      primCharEquality : Char → Char → Bool

    toNat : Char → Nat
    toNat = primCharToNat

    equalb : Char -> Char -> Bool
    equalb = primCharEquality

    -- need to go outside the real language a little to give the primitives good types,
    -- but from the outside this should be safe
    equal : DecEq Char
    equal x y with equalb x y
    ... | True = Inl primTrustMe
    ... | False = Inr canthappen where
      postulate canthappen : _

  open Char public using (Char)

  -- ----------------------------------------------------------------------
  -- vectors

  module Vector where

    data Vec (A : Set) : Nat → Set where
      []   : Vec A 0
      _::_ : ∀ {n} → A → Vec A n → Vec A (S n)

    infixr 99 _::_

    Vec-elim : {A : Set} (P : {n : Nat} → Vec A n → Set)
               → (P [])
               → ({n : Nat} (x : A) (xs : Vec A n) → P xs → P (x :: xs))
               → {n : Nat} (v : Vec A n) → P v
    Vec-elim P n c [] = n
    Vec-elim P n c (y :: ys) = c y ys (Vec-elim P n c ys)

    fromList : {A : Set} → List A → Σ \n → Vec A n
    fromList [] = _ , []
    fromList (x :: xs) = _ , x :: snd (fromList xs)

    toList : {A : Set} {n : Nat} → Vec A n → List A
    toList [] = []
    toList (x :: xs) = x :: (toList xs)

    toList' : {A : Set} → (Σ \ n → Vec A n) → List A
    toList' (._ , []) = []
    toList' (._ , (x :: xs)) = x :: (toList' (_ , xs))

  -- ----------------------------------------------------------------------
  -- strings

  module String where

    postulate {- Agda Primitive -}
      String : Set
    {-# BUILTIN STRING  String #-}
    {-# COMPILED_TYPE String String #-}

    private
      primitive
         primStringToList   : String -> List Char
         primStringFromList : List Char -> String
         primStringAppend   : String -> String -> String
         primStringEquality : String -> String -> Bool

    equal : String -> String -> Bool
    equal = primStringEquality

    toList = primStringToList
    fromList = primStringFromList

    append = primStringAppend

    toVec : String -> Σ \ m → Vector.Vec Char m
    toVec = Vector.fromList o toList

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
------------------------------------------------------------------------
-- Operators
------------------------------------------------------------------------

module Mixfix.Operator where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Vec  using (Vec)
open import Data.Product using (∃; ∃₂; _,_)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.String using (String)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Mixfix.Fixity

-- Name parts.

NamePart : Set
NamePart = String

-- Operators. The parameter arity is the internal arity of the
-- operator, i.e. the number of arguments taken between the first and
-- last name parts.

record Operator (fix : Fixity) (arity : ℕ) : Set where
  field nameParts : Vec NamePart (1 + arity)

open Operator public

-- Predicate filtering out operators of the given fixity and
-- associativity.

hasFixity : ∀ fix → ∃₂ Operator → Maybe (∃ (Operator fix))
hasFixity fix (fix' , op) with fix ≟ fix'
hasFixity fix (.fix , op) | yes refl = just op
hasFixity fix (fix' , op) | _        = nothing

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decision procedures for finite sets and subsets of finite sets
------------------------------------------------------------------------

module Data.Fin.Dec where

open import Function
import Data.Bool as Bool
open import Data.Nat hiding (_<_)
open import Data.Vec hiding (_∈_)
open import Data.Vec.Equality as VecEq
  using () renaming (module PropositionalEquality to PropVecEq)
open import Data.Fin
open import Data.Fin.Subset
open import Data.Fin.Subset.Properties
open import Data.Product as Prod
open import Data.Empty
open import Function
import Function.Equivalence as Eq
open import Relation.Binary as B
import Relation.Binary.HeterogeneousEquality as H
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Unary as U using (Pred)

infix 4 _∈?_

_∈?_ : ∀ {n} x (p : Subset n) → Dec (x ∈ p)
zero  ∈? inside  ∷ p = yes here
zero  ∈? outside ∷ p = no  λ()
suc n ∈? s ∷ p       with n ∈? p
...                  | yes n∈p = yes (there n∈p)
...                  | no  n∉p = no  (n∉p ∘ drop-there)

private

  restrictP : ∀ {p n} → (Fin (suc n) → Set p) → (Fin n → Set p)
  restrictP P f = P (suc f)

  restrict : ∀ {p n} {P : Fin (suc n) → Set p} →
             U.Decidable P → U.Decidable (restrictP P)
  restrict dec f = dec (suc f)

any? : ∀ {n} {P : Fin n → Set} →
       U.Decidable P → Dec (∃ P)
any? {zero}      dec = no λ { (() , _) }
any? {suc n} {P} dec with dec zero | any? (restrict dec)
...                  | yes p | _            = yes (_ , p)
...                  | _     | yes (_ , p') = yes (_ , p')
...                  | no ¬p | no ¬p'       = no helper
  where
  helper : ∄ P
  helper (zero  , p)  = ¬p p
  helper (suc f , p') = ¬p' (_ , p')

nonempty? : ∀ {n} (p : Subset n) → Dec (Nonempty p)
nonempty? p = any? (λ x → x ∈? p)

private

  restrict∈ : ∀ {p q n}
              (P : Fin (suc n) → Set p) {Q : Fin (suc n) → Set q} →
              (∀ {f} → Q f → Dec (P f)) →
              (∀ {f} → restrictP Q f → Dec (restrictP P f))
  restrict∈ _ dec {f} Qf = dec {suc f} Qf

decFinSubset : ∀ {p q n} {P : Fin n → Set p} {Q : Fin n → Set q} →
               U.Decidable Q →
               (∀ {f} → Q f → Dec (P f)) →
               Dec (∀ {f} → Q f → P f)
decFinSubset {n = zero}          _    _    = yes λ{}
decFinSubset {n = suc n} {P} {Q} decQ decP = helper
  where
  helper : Dec (∀ {f} → Q f → P f)
  helper with decFinSubset (restrict decQ) (restrict∈ P decP)
  helper | no ¬q⟶p = no (λ q⟶p → ¬q⟶p (λ {f} q → q⟶p {suc f} q))
  helper | yes q⟶p with decQ zero
  helper | yes q⟶p | yes q₀ with decP q₀
  helper | yes q⟶p | yes q₀ | no ¬p₀ = no (λ q⟶p → ¬p₀ (q⟶p {zero} q₀))
  helper | yes q⟶p | yes q₀ | yes p₀ = yes (λ {_} → hlpr _)
    where
    hlpr : ∀ f → Q f → P f
    hlpr zero    _  = p₀
    hlpr (suc f) qf = q⟶p qf
  helper | yes q⟶p | no ¬q₀ = yes (λ {_} → hlpr _)
    where
    hlpr : ∀ f → Q f → P f
    hlpr zero    q₀ = ⊥-elim (¬q₀ q₀)
    hlpr (suc f) qf = q⟶p qf

all∈? : ∀ {n p} {P : Fin n → Set p} {q} →
        (∀ {f} → f ∈ q → Dec (P f)) →
        Dec (∀ {f} → f ∈ q → P f)
all∈? {q = q} dec = decFinSubset (λ f → f ∈? q) dec

all? : ∀ {n p} {P : Fin n → Set p} →
       U.Decidable P → Dec (∀ f → P f)
all? dec with all∈? {q = ⊤} (λ {f} _ → dec f)
...      | yes ∀p = yes (λ f → ∀p ∈⊤)
...      | no ¬∀p = no  (λ ∀p → ¬∀p (λ {f} _ → ∀p f))

decLift : ∀ {n} {P : Fin n → Set} →
          U.Decidable P → U.Decidable (Lift P)
decLift dec p = all∈? (λ {x} _ → dec x)

private

  restrictSP : ∀ {n} → Side → (Subset (suc n) → Set) → (Subset n → Set)
  restrictSP s P p = P (s ∷ p)

  restrictS : ∀ {n} {P : Subset (suc n) → Set} →
              (s : Side) → U.Decidable P → U.Decidable (restrictSP s P)
  restrictS s dec p = dec (s ∷ p)

anySubset? : ∀ {n} {P : Subset n → Set} →
             U.Decidable P → Dec (∃ P)
anySubset? {zero} {P} dec with dec []
... | yes P[] = yes (_ , P[])
... | no ¬P[] = no helper
  where
  helper : ∄ P
  helper ([] , P[]) = ¬P[] P[]
anySubset? {suc n} {P} dec with anySubset? (restrictS inside  dec)
                              | anySubset? (restrictS outside dec)
... | yes (_ , Pp) | _            = yes (_ , Pp)
... | _            | yes (_ , Pp) = yes (_ , Pp)
... | no ¬Pp       | no ¬Pp'      = no helper
    where
    helper : ∄ P
    helper (inside  ∷ p , Pp)  = ¬Pp  (_ , Pp)
    helper (outside ∷ p , Pp') = ¬Pp' (_ , Pp')

-- If a decidable predicate P over a finite set is sometimes false,
-- then we can find the smallest value for which this is the case.

¬∀⟶∃¬-smallest :
  ∀ n {p} (P : Fin n → Set p) → U.Decidable P →
  ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
¬∀⟶∃¬-smallest zero    P dec ¬∀iPi = ⊥-elim (¬∀iPi (λ()))
¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi with dec zero
¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi | no ¬P0 = (zero , ¬P0 , λ ())
¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi | yes P0 =
  Prod.map suc (Prod.map id extend′) $
    ¬∀⟶∃¬-smallest n (λ n → P (suc n)) (dec ∘ suc) (¬∀iPi ∘ extend)
  where
  extend : (∀ i → P (suc i)) → (∀ i → P i)
  extend ∀iP[1+i] zero    = P0
  extend ∀iP[1+i] (suc i) = ∀iP[1+i] i

  extend′ : ∀ {i : Fin n} →
            ((j : Fin′ i) → P (suc (inject j))) →
            ((j : Fin′ (suc i)) → P (inject j))
  extend′ g zero    = P0
  extend′ g (suc j) = g j

-- Decision procedure for _⊆_ (obtained via the natural lattice
-- order).

infix 4 _⊆?_

_⊆?_ : ∀ {n} → B.Decidable (_⊆_ {n = n})
p₁ ⊆? p₂ =
  Dec.map (Eq.sym NaturalPoset.orders-equivalent) $
  Dec.map′ PropVecEq.to-≡ PropVecEq.from-≡ $
  VecEq.DecidableEquality._≟_ Bool.decSetoid p₁ (p₁ ∩ p₂)


text:
open import Silica
open import HeapProperties

open import Data.List.Membership.DecSetoid ≡-decSetoid
open import Data.List.Relation.Unary.Any

open TypeEnvContext

------------ Lemmas --------------
-- If an expression is well-typed in Δ, then all locations in the expression are in Δ.
locationsInExprAreInContext : ∀ {Δ Δ' e T fl}
                              → ∀ {l : IndirectRef}
                              → Δ ⊢ e ⦂ T ⊣ Δ'
                              → FreeLocations e fl
                              → l ∈ fl
                              ----------------
                              → ∃[ T' ] ((StaticEnv.locEnv Δ) ∋ l ⦂ T')

-- fl is empty, so l is in fl leads to a contradiction.
locationsInExprAreInContext (varTy x spl) varFL ()
-- l is related to e, so therefore we can point to where l is in Δ.
locationsInExprAreInContext (locTy {Δ = Δ''} {T₁ = T₁} l spl) (locFL l) (here refl) =  ⟨ T₁ , Z ⟩
locationsInExprAreInContext (locTy {Δ = Δ''} {T₁} l spl) (locFL l) (there ())
locationsInExprAreInContext (objTy o spl) objValFL ()
locationsInExprAreInContext (boolTy b) boolFL ()
locationsInExprAreInContext ty voidFL ()

-- TODO: relax progress a little per statement of Theorem 5.1.
data Progress : Expr → Set where
  step : ∀ (Σ Σ' : RuntimeEnv)
         → ∀ (e e' : Expr)
         → (Σ , e ⟶ Σ' , e')
         -------------
         → Progress e

  done : ∀ {e : Value}
         ---------
         → Progress (valExpr e)

progress : ∀ {e T Δ Δ'}
           → ∀ (Σ : RuntimeEnv)
           → Closed e
           → Σ & Δ ok
           → Δ ⊢ e ⦂ T ⊣ Δ'
           ---------------
           → Progress e

progress Σ (closed (simpleExpr (var x)) ()) consis (varTy x split) -- Contradiction: var x has free variables, but we assumed e was closed.
-- TODO: Refactor these cases to avoid duplication!
progress Σ cl consis@(ok {Σ} _ _ _ _ _) ty@(locTy l voidSplit) =
  let
    locationExistsInContext = locationsInExprAreInContext ty (locFL l) (here refl)
    lInDelta = proj₂ locationExistsInContext
    heapLookupResult = voidLookup consis lInDelta
  in
    step Σ Σ (simpleExpr (loc l)) (valExpr voidVal) (SElookup ty heapLookupResult)
progress Σ cl consis@(ok {Σ} _ _ _ _ _) ty@(locTy l booleanSplit) =
  let
    locationExistsInContext = locationsInExprAreInContext ty (locFL l) (here refl)
    lInDelta = proj₂ locationExistsInContext
    heapLookupResult = boolLookup consis lInDelta
  in
    step Σ Σ (simpleExpr (loc l)) (valExpr (boolVal (proj₁ heapLookupResult))) (SElookup ty (proj₂ heapLookupResult))
progress Σ cl consis@(ok {Σ} _ _ _ _ _) ty@(locTy l (unownedSplit _ _ _ _)) =
  let
    locationExistsInContext = locationsInExprAreInContext ty (locFL l) (here refl)
    lInDelta = proj₂ locationExistsInContext
    heapLookupResult = locLookup consis lInDelta
    heapLookupFound = proj₁ (proj₂ heapLookupResult)
    o = proj₁ heapLookupResult
  in
    step Σ Σ (simpleExpr (loc l)) (valExpr (objVal o)) (SElookup ty heapLookupFound)
progress Σ cl consis@(ok {Σ} _ _ _ _ _) ty@(locTy l (shared-shared-shared _)) =
  let
    locationExistsInContext = locationsInExprAreInContext ty (locFL l) (here refl)
    lInDelta = proj₂ locationExistsInContext
    heapLookupResult = locLookup consis lInDelta
    heapLookupFound = proj₁ (proj₂ heapLookupResult)
    o = proj₁ heapLookupResult
  in
    step Σ Σ (simpleExpr (loc l)) (valExpr (objVal o)) (SElookup ty heapLookupFound)
progress Σ cl consis@(ok {Σ} _ _ _ _ _) ty@(locTy l (owned-shared _)) =
  let
    locationExistsInContext = locationsInExprAreInContext ty (locFL l) (here refl)
    lInDelta = proj₂ locationExistsInContext
    heapLookupResult = locLookup consis lInDelta
    heapLookupFound = proj₁ (proj₂ heapLookupResult)
    o = proj₁ heapLookupResult
  in
    step Σ Σ (simpleExpr (loc l)) (valExpr (objVal o)) (SElookup ty heapLookupFound)
progress Σ cl consis@(ok {Σ} _ _ _ _ _) ty@(locTy l (states-shared _)) =
  let
    locationExistsInContext = locationsInExprAreInContext ty (locFL l) (here refl)
    lInDelta = proj₂ locationExistsInContext
    heapLookupResult = locLookup consis lInDelta
    heapLookupFound = proj₁ (proj₂ heapLookupResult)
    o = proj₁ heapLookupResult
  in
    step Σ Σ (simpleExpr (loc l)) (valExpr (objVal o)) (SElookup ty heapLookupFound)

progress Σ cl consis (objTy o split) =  done
progress Σ cl consis (boolTy b) = done
progress Σ cl consis (voidTy) = done
progress Σ cl consis (assertTyₗ {s₁ = s} {l = l} tcEq subset) = step Σ Σ (assertₗ l s) (valExpr voidVal) (SEassertₗ {Σ} l s)
progress Σ cl consis (assertTyₓ {s₁ = s} {x = x} tcEq subset) = step Σ Σ (assertₓ x s) (valExpr voidVal) (SEassertₓ {Σ} x s)

progress Σ cl consis (newTy {Γ} {Δ} {Δ'} {Δ''} {states} {C} {st} {x₁} {x₂} stOK x₁Ty x₂Ty CInΓ refl) =
  let
    oFresh = ObjectRefContext.fresh (RuntimeEnv.μ Σ)
    o = proj₁ oFresh
    μ' =  (RuntimeEnv.μ Σ) ObjectRefContext., o ⦂ record { contractName = C ; stateName = st ; x₁ = x₁ ; x₂ = x₂ }
    Σ' = record Σ {μ = μ'}

  in
    step Σ Σ' (new C st x₁ x₂)  (valExpr (objVal o)) (SEnew (proj₁ (proj₂ oFresh)) refl refl)

max_stars_repo_name: ivoysey/Obsidian

max_issues_repo_name: ivoysey/Obsidian

max_forks_repo_name: ivoysey/Obsidian


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------

-- This file contains some core definitions which are reexported by
-- Relation.Binary.Indexed.

module Relation.Binary.Indexed.Core where

open import Function
open import Level
import Relation.Binary.Core as B
import Relation.Binary.Core as P

------------------------------------------------------------------------
-- Indexed binary relations

-- Heterogeneous.

REL : ∀ {i₁ i₂ a₁ a₂} {I₁ : Set i₁} {I₂ : Set i₂} →
      (I₁ → Set a₁) → (I₂ → Set a₂) → (ℓ : Level) → Set _
REL A₁ A₂ ℓ = ∀ {i₁ i₂} → A₁ i₁ → A₂ i₂ → Set ℓ

-- Homogeneous.

Rel : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
Rel A ℓ = REL A A ℓ

------------------------------------------------------------------------
-- Simple properties of indexed binary relations

-- Reflexivity.

Reflexive : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → Rel A ℓ → Set _
Reflexive _ _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})

-- Symmetry.

Symmetric : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → Rel A ℓ → Set _
Symmetric _ _∼_ = ∀ {i j} → B.Sym (_∼_ {i} {j}) _∼_

-- Transitivity.

Transitive : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → Rel A ℓ → Set _
Transitive _ _∼_ = ∀ {i j k} → B.Trans _∼_ (_∼_ {j}) (_∼_ {i} {k})

------------------------------------------------------------------------
-- Setoids

record IsEquivalence {i a ℓ} {I : Set i} (A : I → Set a)
                     (_≈_ : Rel A ℓ) : Set (i ⊔ a ⊔ ℓ) where
  field
    refl  : Reflexive A _≈_
    sym   : Symmetric A _≈_
    trans : Transitive A _≈_

  reflexive : ∀ {i} → P._≡_ ⟨ B._⇒_ ⟩ _≈_ {i}
  reflexive P.refl = refl

record Setoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : I → Set c
    _≈_           : Rel Carrier ℓ
    isEquivalence : IsEquivalence Carrier _≈_

  open IsEquivalence isEquivalence public


text:
{-

Product of structures S and T: X ↦ S X × T X

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Relational.Product where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Univalence
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation as Trunc
open import Cubical.HITs.SetQuotients

open import Cubical.Structures.Product

private
  variable
    ℓ ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓ₂' ℓ₂'' : Level

-- Structured relations

ProductRelStr :
  {S₁ : Type ℓ → Type ℓ₁} (ρ₁ : StrRel S₁ ℓ₁')
  {S₂ : Type ℓ → Type ℓ₂} (ρ₂ : StrRel S₂ ℓ₂')
  → StrRel (ProductStructure S₁ S₂) (ℓ-max ℓ₁' ℓ₂')
ProductRelStr ρ₁ ρ₂ R (s₁ , s₂) (t₁ , t₂) =
  ρ₁ R s₁ t₁ × ρ₂ R s₂ t₂

productSuitableRel :
  {S₁ : Type ℓ → Type ℓ₁} {ρ₁ : StrRel S₁ ℓ₁'}
  {S₂ : Type ℓ → Type ℓ₂} {ρ₂ : StrRel S₂ ℓ₂'}
  → SuitableStrRel S₁ ρ₁ → SuitableStrRel S₂ ρ₂
  → SuitableStrRel (ProductStructure S₁ S₂) (ProductRelStr ρ₁ ρ₂)
productSuitableRel θ₁ θ₂ .quo (X , s₁ , s₂) R (r₁ , r₂) .fst .fst =
  θ₁ .quo (X , s₁) R r₁ .fst .fst , θ₂ .quo (X , s₂) R r₂ .fst .fst
productSuitableRel θ₁ θ₂ .quo (X , s₁ , s₂) R (r₁ , r₂) .fst .snd =
  θ₁ .quo (X , s₁) R r₁ .fst .snd , θ₂ .quo (X , s₂) R r₂ .fst .snd
productSuitableRel θ₁ θ₂ .quo (X , s₁ , s₂) R (r₁ , r₂) .snd ((q₁ , q₂) , (c₁ , c₂)) i .fst =
  θ₁ .quo (X , s₁) R r₁ .snd (q₁ , c₁) i .fst , θ₂ .quo (X , s₂) R r₂ .snd (q₂ , c₂) i .fst
productSuitableRel θ₁ θ₂ .quo (X , s₁ , s₂) R (r₁ , r₂) .snd ((q₁ , q₂) , (c₁ , c₂)) i .snd =
  θ₁ .quo (X , s₁) R r₁ .snd (q₁ , c₁) i .snd , θ₂ .quo (X , s₂) R r₂ .snd (q₂ , c₂) i .snd
productSuitableRel θ₁ θ₂ .symmetric R (r₁ , r₂) =
  θ₁ .symmetric R r₁ , θ₂ .symmetric R r₂
productSuitableRel θ₁ θ₂ .transitive R R' (r₁ , r₂) (r₁' , r₂') =
  θ₁ .transitive R R' r₁ r₁' , θ₂ .transitive R R' r₂ r₂'
productSuitableRel θ₁ θ₂ .set setX =
  isSet× (θ₁ .set setX) (θ₂ .set setX)
productSuitableRel θ₁ θ₂ .prop propR (s₁ , s₂) (t₁ , t₂) =
  isProp× (θ₁ .prop propR s₁ t₁) (θ₂ .prop propR s₂ t₂)

productRelMatchesEquiv :
  {S₁ : Type ℓ → Type ℓ₁} (ρ₁ : StrRel S₁ ℓ₁') {ι₁ : StrEquiv S₁ ℓ₁''}
  {S₂ : Type ℓ → Type ℓ₂} (ρ₂ : StrRel S₂ ℓ₂') {ι₂ : StrEquiv S₂ ℓ₂''}
  → StrRelMatchesEquiv ρ₁ ι₁ → StrRelMatchesEquiv ρ₂ ι₂
  → StrRelMatchesEquiv (ProductRelStr ρ₁ ρ₂) (ProductEquivStr ι₁ ι₂)
productRelMatchesEquiv ρ₁ ρ₂ μ₁ μ₂ A B e =
  Σ-cong-equiv (μ₁ _ _ e) (λ _ → μ₂ _ _ e)

productRelAction :
  {S₁ : Type ℓ → Type ℓ₁} {ρ₁ : StrRel S₁ ℓ₁'} (α₁ : StrRelAction ρ₁)
  {S₂ : Type ℓ → Type ℓ₂} {ρ₂ : StrRel S₂ ℓ₂'} (α₂ : StrRelAction ρ₂)
  → StrRelAction (ProductRelStr ρ₁ ρ₂)
productRelAction α₁ α₂ .actStr f (s₁ , s₂) = α₁ .actStr f s₁ , α₂ .actStr f s₂
productRelAction α₁ α₂ .actStrId (s₁ , s₂) = ΣPathP (α₁ .actStrId s₁ , α₂ .actStrId s₂)
productRelAction α₁ α₂ .actRel h _ _ (r₁ , r₂) = α₁ .actRel h _ _ r₁ , α₂ .actRel h _ _ r₂

productPositiveRel :
  {S₁ : Type ℓ → Type ℓ₁} {ρ₁ : StrRel S₁ ℓ₁'} {θ₁ : SuitableStrRel S₁ ρ₁}
  {S₂ : Type ℓ → Type ℓ₂} {ρ₂ : StrRel S₂ ℓ₂'} {θ₂ : SuitableStrRel S₂ ρ₂}
  → PositiveStrRel θ₁
  → PositiveStrRel θ₂
  → PositiveStrRel (productSuitableRel θ₁ θ₂)
productPositiveRel σ₁ σ₂ .act = productRelAction (σ₁ .act) (σ₂ .act)
productPositiveRel σ₁ σ₂ .reflexive (s₁ , s₂) = σ₁ .reflexive s₁ , σ₂ .reflexive s₂
productPositiveRel σ₁ σ₂ .detransitive R R' (rr'₁ , rr'₂) =
  Trunc.rec squash
    (λ {(s₁ , r₁ , r₁') →
      Trunc.rec squash
        (λ {(s₂ , r₂ , r₂') → ∣ (s₁ , s₂) , (r₁ , r₂) , (r₁' , r₂') ∣})
        (σ₂ .detransitive R R' rr'₂)})
    (σ₁ .detransitive R R' rr'₁)
productPositiveRel {S₁ = S₁} {ρ₁} {θ₁} {S₂} {ρ₂} {θ₂} σ₁ σ₂ .quo {X} R =
  subst isEquiv
    (funExt (elimProp (λ _ → productSuitableRel θ₁ θ₂ .set squash/ _ _) (λ _ → refl)))
    (compEquiv
      (isoToEquiv isom)
      (Σ-cong-equiv (_ , σ₁ .quo R) (λ _ → _ , σ₂ .quo R)) .snd)
  where
  fwd :
    ProductStructure S₁ S₂ X / ProductRelStr ρ₁ ρ₂ (R .fst .fst)
    → (S₁ X / ρ₁ (R .fst .fst)) × (S₂ X / ρ₂ (R .fst .fst))
  fwd [ s₁ , s₂ ] = [ s₁ ] , [ s₂ ]
  fwd (eq/ (s₁ , s₂) (t₁ , t₂) (r₁ , r₂) i) = eq/ s₁ t₁ r₁ i , eq/ s₂ t₂ r₂ i
  fwd (squash/ _ _ p q i j) =
    isSet× squash/ squash/ _ _ (cong fwd p) (cong fwd q) i j

  bwd[] : S₁ X → S₂ X / ρ₂ (R .fst .fst)
    → ProductStructure S₁ S₂ X / ProductRelStr ρ₁ ρ₂ (R .fst .fst)
  bwd[] s₁ [ s₂ ] = [ s₁ , s₂ ]
  bwd[] s₁ (eq/ s₂ t₂ r₂ i) =
    eq/ (s₁ , s₂) (s₁ , t₂) (posRelReflexive σ₁ R s₁ , r₂) i
  bwd[] s₁ (squash/ _ _ p q i j) =
    squash/ _ _ (λ j → bwd[] s₁ (p j)) (λ j → bwd[] s₁ (q j)) i j

  bwd : S₁ X / ρ₁ (R .fst .fst) → S₂ X / ρ₂ (R .fst .fst)
    → ProductStructure S₁ S₂ X / ProductRelStr ρ₁ ρ₂ (R .fst .fst)
  bwd [ s₁ ] u = bwd[] s₁ u
  bwd (eq/ s₁ t₁ r₁ i) u = path u i
    where
    path : ∀ u → bwd [ s₁ ] u ≡ bwd [ t₁ ] u
    path = elimProp (λ _ → squash/ _ _) (λ s₂ → eq/ (s₁ , s₂) (t₁ , s₂) (r₁ , posRelReflexive σ₂ R s₂))
  bwd (squash/ _ _ p q i j) =
    isSetΠ (λ _ → squash/) _ _ (cong bwd p) (cong bwd q) i j

  open Iso
  isom : Iso _ _
  isom .fun = fwd
  isom .inv = uncurry bwd
  isom .rightInv =
    uncurry
      (elimProp (λ _ → isPropΠ λ _ → isSet× squash/ squash/ _ _)
        (λ _ → elimProp (λ _ → isSet× squash/ squash/ _ _) (λ _ → refl)))
  isom .leftInv = elimProp (λ _ → squash/ _ _) (λ _ → refl)

productRelMatchesTransp :
  {S₁ : Type ℓ → Type ℓ₁} (ρ₁ : StrRel S₁ ℓ₁') (α₁ : EquivAction S₁)
  {S₂ : Type ℓ → Type ℓ₂} (ρ₂ : StrRel S₂ ℓ₂') (α₂ : EquivAction S₂)
  → StrRelMatchesEquiv ρ₁ (EquivAction→StrEquiv α₁)
  → StrRelMatchesEquiv ρ₂ (EquivAction→StrEquiv α₂)
  → StrRelMatchesEquiv (ProductRelStr ρ₁ ρ₂) (EquivAction→StrEquiv (productEquivAction α₁ α₂))
productRelMatchesTransp _ _ _ _ μ₁ μ₂ _ _ e =
  compEquiv (Σ-cong-equiv (μ₁ _ _ e) (λ _ → μ₂ _ _ e)) ΣPath≃PathΣ

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module List.Permutation.Pair (A : Set) where

open import Data.List
open import Data.Product

data _≈_ : List A → List A × List A → Set where
  ≈[]r : (xs : List A)
                   → xs ≈ (xs , [])
  ≈[]l : (xs : List A)
                   → xs ≈ ([] , xs)
  ≈xr : {x : A}{xs ys zs : List A}
                   → xs ≈ (ys , zs)
                   → (x ∷ xs) ≈ (ys , x ∷ zs)
  ≈xl : {x : A}{xs ys zs : List A}
                   → xs ≈ (ys , zs)
                   → (x ∷ xs) ≈ (x ∷ ys , zs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Semantics where

open import Data.Nat hiding (_⊔_; _⊓_)
open import Data.Product
open import Data.Sum
open import Data.String using (String)
open import Data.Unit hiding (_≟_)
open import Data.Empty

open import Relation.Nullary
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_;_≢_; refl)
open Eq.≡-Reasoning
open import Level hiding (_⊔_) renaming (zero to lzero; suc to lsuc)

{- TODO:
* subtyping of refinement types
* union types
* intersection types
-}

Id = String

variable
  x y : Id
  ℓ : Level

data Expr : Set where
  Nat : ℕ → Expr
  Var : Id → Expr
  Lam : Id → Expr → Expr
  App : Expr → Expr → Expr
  Pair : Expr → Expr → Expr
  Fst Snd : Expr → Expr
  Inl Inr : Expr → Expr
  Case : Expr → Id → Expr → Id → Expr → Expr

data RawType : Set where
  Nat : RawType
  _⇒_ _⋆_ _⊹_ : RawType → RawType → RawType

ss⇒tt : ∀ {S S₁ T T₁ : RawType} → (S ⇒ S₁) ≡ (T ⇒ T₁) → (S ≡ T × S₁ ≡ T₁)
ss⇒tt refl = refl , refl

ss⋆tt : ∀ {S S₁ T T₁ : RawType} → (S ⋆ S₁) ≡ (T ⋆ T₁) → (S ≡ T × S₁ ≡ T₁)
ss⋆tt refl = refl , refl

ss⊹tt : ∀ {S S₁ T T₁ : RawType} → (S ⊹ S₁) ≡ (T ⊹ T₁) → (S ≡ T × S₁ ≡ T₁)
ss⊹tt refl = refl , refl

data Type : Set₁ where
  Base : (P : ℕ → Set) → Type -- refinement
  Nat : Type
  _⇒_ : Type → Type → Type
  _⋆_ : Type → Type → Type
  _⊹_ : Type → Type → Type

T-Nat = Base (λ n → ⊤) -- all natural numbers

data ne : Type → Set where
  ne-base : ∀ {P} → (∃P : Σ ℕ P) → ne (Base P)
  ne-nat : ne Nat
  ne-⇒ : ∀ {S T} → ne S → ne T → ne (S ⇒ T)
  ne-⋆ : ∀ {S T} → ne S → ne T → ne (S ⋆ T)
  ne-⊹L : ∀ {S T} → ne S → ne (S ⊹ T)
  ne-⊹R : ∀ {S T} → ne T → ne (S ⊹ T)

data Env (A : Set ℓ) : Set ℓ where
  · : Env A
  _,_⦂_ : Env A → (x : Id) → (a : A) → Env A

∥_∥ : Type → RawType
∥ Base P ∥ = Nat
∥ Nat ∥ = Nat
∥ S ⇒ S₁ ∥ = ∥ S ∥ ⇒ ∥ S₁ ∥
∥ S ⋆ S₁ ∥ = ∥ S ∥ ⋆ ∥ S₁ ∥
∥ S ⊹ S₁ ∥ = ∥ S ∥ ⊹ ∥ S₁ ∥

_∨_ : (P Q : ℕ → Set) → ℕ → Set
P ∨ Q = λ n → P n ⊎ Q n

_∧_ : (P Q : ℕ → Set) → ℕ → Set
P ∧ Q = λ n → P n × Q n

implies : ∀ {P Q : ℕ → Set} → (n : ℕ) → P n → (P n ⊎ Q n)
implies n Pn = inj₁ Pn

p*q->p : ∀ {P Q : ℕ → Set} → (n : ℕ) → (P n × Q n) → P n
p*q->p n (Pn , Qn) = Pn

_⊔_ _⊓_  : (S T : Type) {r : ∥ S ∥ ≡ ∥ T ∥} → Type

(Base P ⊔ Base P₁) {refl} = Base (P ∨ P₁)
(Base P ⊔ Nat) = Nat
(Nat ⊔ Base P) = Nat
(Nat ⊔ Nat) = Nat
((S ⇒ S₁) ⊔ (T ⇒ T₁)) {r} with ss⇒tt r
... | sss , ttt = (S ⊓ T){sss} ⇒ (S₁ ⊔ T₁){ttt}
((S ⋆ S₁) ⊔ (T ⋆ T₁)) {r} with ss⋆tt r
... | sss , ttt = (S ⊔ T){sss} ⋆ (S₁ ⊔ T₁){ttt}
((S ⊹ S₁) ⊔ (T ⊹ T₁)) {r} with ss⊹tt r
... | sss , ttt = (S ⊔ T){sss} ⊹ (S₁ ⊔ T₁){ttt}

Base P ⊓ Base P₁ = Base (P ∧ P₁)
Base P ⊓ Nat = Base P
Nat ⊓ Base P = Base P
Nat ⊓ Nat = Nat
((S ⇒ S₁) ⊓ (T ⇒ T₁)){r} with ss⇒tt r
... | sss , ttt = (S ⊔ T){sss} ⇒ (S₁ ⊓ T₁){ttt}
((S ⋆ S₁) ⊓ (T ⋆ T₁)){r} with ss⋆tt r
... | sss , ttt = (S ⊓ T){sss} ⋆ (S₁ ⊓ T₁){ttt}
((S ⊹ S₁) ⊓ (T ⊹ T₁)){r} with ss⊹tt r
... | sss , ttt = (S ⊓ T){sss} ⊹ (S₁ ⊓ T₁){ttt}

variable
  S T U S′ T′ U′ U″ : Type
  Γ Γ₁ Γ₂ : Env Type
  L M N : Expr
  n : ℕ
  P : ℕ → Set

data Split {A : Set ℓ} : Env A → Env A → Env A → Set ℓ where
  nil : Split · · ·
  lft : ∀ {a : A}{Γ Γ₁ Γ₂ : Env A} → Split Γ Γ₁ Γ₂ → Split (Γ , x ⦂ a) (Γ₁ , x ⦂ a) Γ₂
  rgt : ∀ {a : A}{Γ Γ₁ Γ₂ : Env A} → Split Γ Γ₁ Γ₂ → Split (Γ , x ⦂ a) Γ₁ (Γ₂ , x ⦂ a)

data _⦂_∈_ {A : Set ℓ} : Id → A → Env A → Set ℓ where

  found : ∀ {a : A}{E : Env A} →
    x ⦂ a ∈ (E , x ⦂ a)

  there : ∀ {a a' : A}{E : Env A} →
    x ⦂ a ∈ E →
      -- x ≢ y →
    x ⦂ a ∈ (E , y ⦂ a')

data _<:_ : Type → Type → Set where

  <:-refl :
    T <: T

  <:-base :
    (P Q : ℕ → Set) →
    (p→q : ∀ n → P n → Q n) →
    Base P <: Base Q

  <:-base-nat :
    Base P <: Nat

  <:-⇒ :
    S′ <: S →
    T <: T′ →
    (S ⇒ T) <: (S′ ⇒ T′)

  <:-⋆ :
    S <: S′ →
    T <: T′ →
    (S ⋆ T) <: (S′ ⋆ T′)

  <:-⊹ :
    S <: S′ →
    T <: T′ →
    (S ⊹ T) <: (S′ ⊹ T′)

-- subtyping is compatible with raw types

<:-raw : S <: T → ∥ S ∥ ≡ ∥ T ∥
<:-raw <:-refl = refl
<:-raw (<:-base P Q p→q) = refl
<:-raw <:-base-nat = refl
<:-raw (<:-⇒ s<:t s<:t₁) = Eq.cong₂ _⇒_ (Eq.sym (<:-raw s<:t)) (<:-raw s<:t₁)
<:-raw (<:-⋆ s<:t s<:t₁) = Eq.cong₂ _⋆_ (<:-raw s<:t) (<:-raw s<:t₁)
<:-raw (<:-⊹ s<:t s<:t₁) = Eq.cong₂ _⊹_ (<:-raw s<:t) (<:-raw s<:t₁)

<:-⊔ : ∀ S T → {c : ∥ S ∥ ≡ ∥ T ∥} → S <: (S ⊔ T){c}
<:-⊓ : ∀ S T → {c : ∥ S ∥ ≡ ∥ T ∥} → (S ⊓ T){c} <: S

<:-⊔ (Base P) (Base P₁) {refl} = <:-base P (P ∨ P₁) implies
<:-⊔ (Base P) Nat = <:-base-nat
<:-⊔ Nat (Base P) = <:-refl
<:-⊔ Nat Nat = <:-refl
<:-⊔ (S ⇒ S₁) (T ⇒ T₁) {c} with ss⇒tt c
... | c1 , c2 = <:-⇒ (<:-⊓ S T) (<:-⊔ S₁ T₁)
<:-⊔ (S ⋆ S₁) (T ⋆ T₁) {c} with ss⋆tt c
... | c1 , c2 = <:-⋆ (<:-⊔ S T) (<:-⊔ S₁ T₁)
<:-⊔ (S ⊹ S₁) (T ⊹ T₁) {c} with ss⊹tt c
... | c1 , c2 = <:-⊹ (<:-⊔ S T) (<:-⊔ S₁ T₁)

<:-⊓ (Base P) (Base P₁) {refl} = <:-base (P ∧ P₁) P p*q->p
<:-⊓ (Base P) Nat = <:-refl
<:-⊓ Nat (Base P) = <:-base-nat
<:-⊓ Nat Nat = <:-refl
<:-⊓ (S ⇒ S₁) (T ⇒ T₁) {c} with ss⇒tt c
... | c1 , c2 = <:-⇒ (<:-⊔ S T) (<:-⊓ S₁ T₁)
<:-⊓ (S ⋆ S₁) (T ⋆ T₁) {c} with ss⋆tt c
... | c1 , c2 = <:-⋆ (<:-⊓ S T) (<:-⊓ S₁ T₁)
<:-⊓ (S ⊹ S₁) (T ⊹ T₁) {c} with ss⊹tt c
... | c1 , c2 = <:-⊹ (<:-⊓ S T) (<:-⊓ S₁ T₁)

-- should be in terms of RawType for evaluation

data _⊢_⦂_ : Env Type → Expr → Type → Set₁ where

  nat' :
    Γ ⊢ Nat n ⦂ Base (_≡_ n)

  var :
    (x∈ : x ⦂ T ∈ Γ) →
    --------------------
    Γ ⊢ Var x ⦂ T

  lam :
    (Γ , x ⦂ S) ⊢ M ⦂ T →
    --------------------
    Γ ⊢ Lam x M ⦂ (S ⇒ T)

  app :
    Γ ⊢ M ⦂ (S ⇒ T) →
    Γ ⊢ N ⦂ S →
    --------------------
    Γ ⊢ App M N ⦂ T

  pair :
    Γ ⊢ M ⦂ S →
    Γ ⊢ N ⦂ T →
    --------------------
    Γ ⊢ Pair M N ⦂ (S ⋆ T)

  pair-E1 :
    Γ ⊢ M ⦂ (S ⋆ T) →
    --------------------
    Γ ⊢ Fst M ⦂ S

  pair-E2 :
    Γ ⊢ M ⦂ (S ⋆ T) →
    --------------------
    Γ ⊢ Snd M ⦂ T

  sum-I1 :
    Γ ⊢ M ⦂ S →
    --------------------
    Γ ⊢ Inl M ⦂ (S ⊹ T)

  sum-I2 :
    Γ ⊢ N ⦂ T →
    --------------------
    Γ ⊢ Inl N ⦂ (S ⊹ T)

  sum-E :
    Γ ⊢ L ⦂ (S ⊹ T) →
    (Γ , x ⦂ S) ⊢ M ⦂ U →
    (Γ , y ⦂ T) ⊢ N ⦂ U →
    --------------------
    Γ ⊢ Case L x M y N ⦂ U

split-sym : Split Γ Γ₁ Γ₂ → Split Γ Γ₂ Γ₁
split-sym nil = nil
split-sym (lft sp) = rgt (split-sym sp)
split-sym (rgt sp) = lft (split-sym sp)

weaken-∈ : Split Γ Γ₁ Γ₂ → x ⦂ T ∈ Γ₁ → x ⦂ T ∈ Γ
weaken-∈ (lft sp) found = found
weaken-∈ (rgt sp) found = there (weaken-∈ sp found)
weaken-∈ (lft sp) (there x∈) = there (weaken-∈ sp x∈)
weaken-∈ (rgt sp) (there x∈) = there (weaken-∈ sp (there x∈))

weaken : Split Γ Γ₁ Γ₂ → Γ₁ ⊢ M ⦂ T → Γ ⊢ M ⦂ T
weaken sp (nat') = nat'
weaken sp (var x∈) = var (weaken-∈ sp x∈)
weaken sp (lam ⊢M) = lam (weaken (lft sp) ⊢M)
weaken sp (app ⊢M ⊢N) = app (weaken sp ⊢M) (weaken sp ⊢N)
weaken sp (pair ⊢M ⊢N) = pair (weaken sp ⊢M) (weaken sp ⊢N)
weaken sp (pair-E1 ⊢M) = pair-E1 (weaken sp ⊢M)
weaken sp (pair-E2 ⊢M) = pair-E2 (weaken sp ⊢M)
weaken sp (sum-I1 ⊢M) = sum-I1 (weaken sp ⊢M)
weaken sp (sum-I2 ⊢N) = sum-I2 (weaken sp ⊢N)
weaken sp (sum-E ⊢L ⊢M ⊢N) = sum-E (weaken sp ⊢L) (weaken (lft sp) ⊢M) (weaken (lft sp) ⊢N)

-- incorrectness typing

P=n : ℕ → ℕ → Set
P=n = λ n x → n ≡ x

data _⊢_÷_ : Env Type → Expr → Type → Set₁ where

  nat' :
    --------------------
    · ⊢ Nat n ÷ Base (_≡_ n)

  var1 :
    ( · , x ⦂ T) ⊢ Var x ÷ T

{-
  var :
    x ⦂ T ∈ Γ →
    --------------------
    Γ ⊢ Var x ÷ T
-}

  lam :
    (· , x ⦂ S) ⊢ M ÷ T →
    --------------------
    · ⊢ Lam x M ÷ (S ⇒ T)

  pair :
    Split Γ Γ₁ Γ₂ →
    Γ₁ ⊢ M ÷ S →
    Γ₂ ⊢ N ÷ T →
    --------------------
    Γ ⊢ Pair M N ÷ (S ⋆ T)

  pair-E1 :
    Γ ⊢ M ÷ (S ⋆ T) →
    --------------------
    Γ ⊢ Fst M ÷ S

  pair-E2 :
    Γ ⊢ M ÷ (S ⋆ T) →
    --------------------
    Γ ⊢ Snd M ÷ T

  sum-E :
    Split Γ Γ₁ Γ₂ →
    Γ₁ ⊢ L ÷ (S ⊹ T) →
    (Γ₂ , x ⦂ S) ⊢ M ÷ U →
    (Γ₂ , y ⦂ T) ⊢ N ÷ U →
    --------------------
    Γ ⊢ Case L x M y N ÷ U

  sum-E′ : ∀ {ru′=ru″} →
    Split Γ Γ₁ Γ₂ →
    Γ₁ ⊢ L ÷ (S ⊹ T) →
    (Γ₂ , x ⦂ S) ⊢ M ÷ U′ →
    (Γ₂ , y ⦂ T) ⊢ N ÷ U″ →
    U ≡ (U′ ⊔ U″){ru′=ru″} →
    --------------------
    Γ ⊢ Case L x M y N ÷ U

{-
  `sub` :
    Γ ⊢ M ÷ S →
    T <: S →
    --------------------
    Γ ⊢ M ÷ T
-}

record _←_ (A B : Set) : Set where
  field
    func : A → B
    back : ∀ (b : B) → ∃ λ (a : A) → func a ≡ b

open _←_

T⟦_⟧ : Type → Set
T⟦ Base P ⟧ = Σ ℕ P
T⟦ Nat ⟧ = ℕ
T⟦ S ⇒ T ⟧ = T⟦ S ⟧ → T⟦ T ⟧
T⟦ S ⋆ T ⟧ = T⟦ S ⟧ × T⟦ T ⟧
T⟦ S ⊹ T ⟧ = T⟦ S ⟧ ⊎ T⟦ T ⟧

T'⟦_⟧ : Type → Set
T'⟦ Base P ⟧ = Σ ℕ P
T'⟦ Nat ⟧ = ℕ
T'⟦ S ⇒ T ⟧ = T'⟦ S ⟧ ← T'⟦ T ⟧
T'⟦ S ⋆ T ⟧ = T'⟦ S ⟧ × T'⟦ T ⟧
T'⟦ S ⊹ T ⟧ = T'⟦ S ⟧ ⊎ T'⟦ T ⟧

E⟦_⟧ : Env Type → Env Set
E⟦ · ⟧ = ·
E⟦ Γ , x ⦂ T ⟧ = E⟦ Γ ⟧ , x ⦂ T⟦ T ⟧

data iEnv : Env Set → Set where
  · : iEnv ·
  _,_⦂_ : ∀ {E}{A} → iEnv E → (x : Id) → (a : A) → iEnv (E , x ⦂ A)

lookup : (x ⦂ T ∈ Γ) → iEnv E⟦ Γ ⟧ → T⟦ T ⟧
lookup found (γ , _ ⦂ a) = a
lookup (there x∈) (γ , _ ⦂ a) = lookup x∈ γ

eval : Γ ⊢ M ⦂ T → iEnv E⟦ Γ ⟧ → T⟦ T ⟧
eval (nat'{n = n}) γ = n , refl
eval (var x∈) γ = lookup x∈ γ
eval (lam ⊢M) γ = λ s → eval ⊢M (γ , _ ⦂ s)
eval (app ⊢M ⊢N) γ = eval ⊢M γ (eval ⊢N γ)
eval (pair ⊢M ⊢N) γ = (eval ⊢M γ) , (eval ⊢N γ)
eval (pair-E1 ⊢M) γ = proj₁ (eval ⊢M γ)
eval (pair-E2 ⊢M) γ = proj₂ (eval ⊢M γ)
eval (sum-I1 ⊢M) γ = inj₁ (eval ⊢M γ)
eval (sum-I2 ⊢N) γ = inj₂ (eval ⊢N γ)
eval (sum-E{S = S}{T = T}{U = U} ⊢L ⊢M ⊢N) γ =
  [ (λ s → eval ⊢M (γ , _ ⦂ s)) , (λ t → eval ⊢N (γ , _ ⦂ t)) ] (eval ⊢L γ)

corr : Γ ⊢ M ÷ T → Γ ⊢ M ⦂ T
corr (nat') = nat'
corr var1 = var found
-- corr (var x) = var x
corr (lam ⊢M) = lam (corr ⊢M)
corr (pair-E1 ÷M) = pair-E1 (corr ÷M)
corr (pair-E2 ÷M) = pair-E2 (corr ÷M)
corr (pair sp ÷M ÷N) = pair (weaken sp (corr ÷M)) (weaken (split-sym sp) (corr ÷N))
corr (sum-E sp ÷L ÷M ÷N) = sum-E (weaken sp (corr  ÷L)) (weaken (lft (split-sym sp)) (corr ÷M)) (weaken (lft (split-sym sp)) (corr ÷N))
corr (sum-E′ sp ÷L ÷M ÷N U≡U′⊔U″) =
  sum-E (weaken sp (corr  ÷L)) (weaken (lft (split-sym sp)) (corr {!!})) (weaken (lft (split-sym sp)) (corr {!!}))
{-
corr (`sub` ÷M T<S) = {!÷M!}
-}

-- pick one element of a type to demonstrate non-emptiness
one : ∀ (T : Type) {net : ne T} → T⟦ T ⟧
one (Base P) {ne-base ∃P} = ∃P
one Nat = zero
one (T ⇒ T₁) {ne-⇒ ne-T ne-T₁} = λ x → one T₁ {ne-T₁}
one (T ⋆ T₁) {ne-⋆ ne-T ne-T₁} = (one T {ne-T}) , (one T₁ {ne-T₁})
one (T ⊹ T₁) {ne-⊹L ne-T} = inj₁ (one T {ne-T})
one (T ⊹ T₁) {ne-⊹R ne-T₁} = inj₂ (one T₁ {ne-T₁})

{- not needed
many : iEnv E⟦ Γ ⟧
many {·} = ·
many {Γ , x ⦂ T} = many , x ⦂ one T

gen : (x∈ : x ⦂ T ∈ Γ) (t  : T⟦ T ⟧) → iEnv E⟦ Γ ⟧
gen found t = many , _ ⦂ t
gen (there x∈) t = (gen x∈ t) , _ ⦂ one {!!}

lookup-gen : (x∈ : x ⦂ T ∈ Γ) (t  : T⟦ T ⟧) → lookup x∈ (gen x∈ t) ≡ t
lookup-gen found t = refl
lookup-gen (there x∈) t = lookup-gen x∈ t
-}

open Eq.≡-Reasoning

postulate
  ext : ∀ {A B : Set}{f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

unsplit-env : Split Γ Γ₁ Γ₂ → iEnv E⟦ Γ₁ ⟧ → iEnv E⟦ Γ₂ ⟧ → iEnv E⟦ Γ ⟧
unsplit-env nil γ₁ γ₂ = ·
unsplit-env (lft sp) (γ₁ , _ ⦂ a) γ₂ = (unsplit-env sp γ₁ γ₂) , _ ⦂ a
unsplit-env (rgt sp) γ₁ (γ₂ , _ ⦂ a) = (unsplit-env sp γ₁ γ₂) , _ ⦂ a

unsplit-split : (sp : Split Γ Γ₁ Γ₂) (γ₁ : iEnv E⟦ Γ₁ ⟧) (γ₂ : iEnv E⟦ Γ₂ ⟧) →
  unsplit-env sp γ₁ γ₂ ≡ unsplit-env (split-sym sp) γ₂ γ₁
unsplit-split nil γ₁ γ₂ = refl
unsplit-split (lft sp) (γ₁ , _ ⦂ a) γ₂ rewrite unsplit-split sp γ₁ γ₂ = refl
unsplit-split (rgt sp) γ₁ (γ₂ , _ ⦂ a) rewrite unsplit-split sp γ₁ γ₂ = refl

lookup-unsplit : (sp : Split Γ Γ₁ Γ₂) (γ₁ : iEnv E⟦ Γ₁ ⟧) (γ₂ : iEnv E⟦ Γ₂ ⟧) →
  (x∈ : x ⦂ T ∈ Γ₁) →
  lookup (weaken-∈ sp x∈) (unsplit-env sp γ₁ γ₂) ≡ lookup x∈ γ₁
lookup-unsplit (lft sp) (γ₁ , _ ⦂ a) γ₂ found = refl
lookup-unsplit (rgt sp) γ₁ (γ₂ , _ ⦂ a) found = lookup-unsplit sp γ₁ γ₂ found
lookup-unsplit (lft sp) (γ₁ , _ ⦂ a) γ₂ (there x∈) = lookup-unsplit sp γ₁ γ₂ x∈
lookup-unsplit (rgt sp) γ₁ (γ₂ , _ ⦂ a) (there x∈) = lookup-unsplit sp γ₁ γ₂ (there x∈)

eval-unsplit : (sp : Split Γ Γ₁ Γ₂) (γ₁ : iEnv E⟦ Γ₁ ⟧) (γ₂ : iEnv E⟦ Γ₂ ⟧) →
  (⊢M : Γ₁ ⊢ M ⦂ T) →
  eval (weaken sp ⊢M) (unsplit-env sp γ₁ γ₂) ≡ eval ⊢M γ₁
eval-unsplit sp γ₁ γ₂ (nat')= refl
eval-unsplit sp γ₁ γ₂ (var x∈) = lookup-unsplit sp γ₁ γ₂ x∈
eval-unsplit sp γ₁ γ₂ (lam ⊢M) = ext (λ s → eval-unsplit (lft sp) (γ₁ , _ ⦂ s) γ₂ ⊢M)
eval-unsplit sp γ₁ γ₂ (app ⊢M ⊢M₁)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢M | eval-unsplit sp γ₁ γ₂ ⊢M₁ = refl
eval-unsplit sp γ₁ γ₂ (pair ⊢M ⊢M₁)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢M | eval-unsplit sp γ₁ γ₂ ⊢M₁ = refl
eval-unsplit sp γ₁ γ₂ (pair-E1 ⊢M)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢M = refl
eval-unsplit sp γ₁ γ₂ (pair-E2 ⊢M)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢M = refl
eval-unsplit sp γ₁ γ₂ (sum-I1 ⊢M)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢M = refl
eval-unsplit sp γ₁ γ₂ (sum-I2 ⊢N)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢N = refl
eval-unsplit sp γ₁ γ₂ (sum-E ⊢L ⊢M ⊢N)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢L
        | ext (λ s → eval-unsplit (lft sp) (γ₁ , _ ⦂ s) γ₂ ⊢M)
        | ext (λ t → eval-unsplit (lft sp) (γ₁ , _ ⦂ t) γ₂ ⊢N)
  = refl

-- soundness of the incorrectness rules
lave :
  (÷M : Γ ⊢ M ÷ T) →
  ∀ (t : T⟦ T ⟧) →
  ∃ λ (γ : iEnv E⟦ Γ ⟧) →
  eval (corr ÷M) γ ≡ t

lave nat' (n , refl) = · , refl

lave var1 t = (· , _ ⦂ t) , refl
-- lave (var x∈) t =  (gen x∈ t) , lookup-gen x∈ t
lave (lam{x = x}{S = S} ÷M) t = · , ext aux
  where
    aux : (s : T⟦ S ⟧) → eval (corr ÷M) (· , x ⦂ s) ≡ t s
    aux s with lave ÷M (t s)
    ... | (· , .x ⦂ a) , snd = {!!} -- impossible to complete!

lave (pair-E1 ÷M) t with lave ÷M (t , one {!!})
... | γ , ih = γ , Eq.cong proj₁ ih
lave (pair-E2 ÷M) t with lave ÷M (one {!!} , t)
... | γ , ih = γ , Eq.cong proj₂ ih

lave (pair sp ÷M ÷N) (s , t) with lave ÷M s | lave ÷N t
... | γ₁ , ih-M | γ₂ , ih-N =
  unsplit-env sp γ₁ γ₂ ,
  Eq.cong₂ _,_ (Eq.trans (eval-unsplit sp γ₁ γ₂ (corr ÷M)) ih-M)
               (begin eval (weaken (split-sym sp) (corr ÷N)) (unsplit-env sp γ₁ γ₂)
               ≡⟨ Eq.cong (eval (weaken (split-sym sp) (corr ÷N))) (unsplit-split sp γ₁ γ₂) ⟩
               eval (weaken (split-sym sp) (corr ÷N)) (unsplit-env (split-sym sp) γ₂ γ₁)
               ≡⟨ eval-unsplit (split-sym sp) γ₂ γ₁ (corr ÷N) ⟩
               ih-N)

-- works, but unsatisfactory!
-- this proof uses only one branch of the case
-- this choice is possible because both branches ÷M and ÷N have the same type
-- in general, U could be the union of the types of ÷M and ÷N
lave (sum-E{S = S}{T = T}{U = U} sp ÷L ÷M ÷N) u
  with lave ÷M u | lave ÷N u
... | (γ₁ , x ⦂ s) , ih-M | (γ₂ , y ⦂ t) , ih-N
  with lave ÷L (inj₁ s)
... | γ₀ , ih-L
  =
  unsplit-env sp γ₀ γ₁ ,
  (begin [
      (λ s₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷M))
         (unsplit-env sp γ₀ γ₁ , x ⦂ s₁))
      ,
      (λ t₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷N))
         (unsplit-env sp γ₀ γ₁ , y ⦂ t₁))
      ]
      (eval (weaken sp (corr ÷L)) (unsplit-env sp γ₀ γ₁))
  ≡⟨ Eq.cong [
      (λ s₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷M))
         (unsplit-env sp γ₀ γ₁ , x ⦂ s₁))
      ,
      (λ t₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷N))
         (unsplit-env sp γ₀ γ₁ , y ⦂ t₁))
      ] (eval-unsplit sp γ₀ γ₁ (corr ÷L)) ⟩
    [
      (λ s₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷M))
         (unsplit-env sp γ₀ γ₁ , x ⦂ s₁))
      ,
      (λ t₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷N))
         (unsplit-env sp γ₀ γ₁ , y ⦂ t₁))
      ]
      (eval (corr ÷L) γ₀)
  ≡⟨ Eq.cong
       [
       (λ s₁ →
          eval (weaken (lft (split-sym sp)) (corr ÷M))
          (unsplit-env sp γ₀ γ₁ , x ⦂ s₁))
       ,
       (λ t₁ →
          eval (weaken (lft (split-sym sp)) (corr ÷N))
          (unsplit-env sp γ₀ γ₁ , y ⦂ t₁))
       ]
       ih-L ⟩
    eval (weaken (lft (split-sym sp)) (corr ÷M)) (unsplit-env sp γ₀ γ₁ , x ⦂ s)
  ≡⟨  Eq.cong (λ γ → eval (weaken (lft (split-sym sp)) (corr ÷M)) (γ , x ⦂ s)) (unsplit-split sp γ₀ γ₁) ⟩
    eval (weaken (lft (split-sym sp)) (corr ÷M)) (unsplit-env (split-sym sp) γ₁ γ₀ , x ⦂ s)
  ≡⟨⟩
    eval (weaken (lft (split-sym sp)) (corr ÷M)) (unsplit-env (lft (split-sym sp)) (γ₁ , x ⦂ s) γ₀)
  ≡⟨ eval-unsplit (lft (split-sym sp)) (γ₁ , x ⦂ s) γ₀ (corr ÷M) ⟩
    ih-M)

lave (sum-E′{S = S}{T = T}{U = U} sp ÷L ÷M ÷N uuu) u = {!!}

max_stars_repo_name: proglang/incorrectness

max_issues_repo_name: proglang/incorrectness

max_forks_repo_name: proglang/incorrectness


text:
module Oscar.Class.Associativity where

open import Oscar.Class.Preservativity
open import Oscar.Function
open import Oscar.Level
open import Oscar.Relation

record Associativity
  {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
    (_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n)
  {ℓ}
    (_≤_ : ∀ {m n} → m ► n → m ► n → Set ℓ)
  : Set (𝔞 ⊔ 𝔰 ⊔ ℓ) where
  field
    associativity : ∀ {k l} (f : k ► l) {m} (g : l ► m) {n} (h : m ► n) → (h ◅ (g ◅ f)) ≤ ((h ◅ g) ◅ f)

  instance `preservativity : ∀ {l} {m} {n} {w : m ► n} → Preservativity (λ ⋆ → _◅_ ⋆) (λ ⋆ → _◅_ ⋆) _≤_ (m ⟨ l ►_ ⟩→ n ∋ w ◅_) id (m ⟨ l ►_ ⟩→ n ∋ w ◅_)
  Preservativity.preservativity `preservativity g f = associativity f g _
--    ⦃ `preservativity ⦄ : ∀ {l} {m} {n} {w : m ► n} → Preservativity (λ ⋆ → _◅_ ⋆) (λ ⋆ → _◅_ ⋆) _≤_ (m ⟨ l ►_ ⟩→ n ∋ w ◅_) id (m ⟨ l ►_ ⟩→ n ∋ w ◅_)

open Associativity ⦃ … ⦄ public

module _ where

  private

    postulate
      A : Set
      _⇒_ : A → A → Set
      _∙_ : ∀ {m n} → m ⇒ n → ∀ {l} → m ⟨ l ⇒_ ⟩→ n
      _≋_ : ∀ {m n} → m ⇒ n → m ⇒ n → Set
      instance _ : Associativity _∙_ _≋_

    test-associativity₁ : ∀ {k l} (f : k ⇒ l) {m} (g : l ⇒ m) {n} (h : m ⇒ n) → (h ∙ (g ∙ f)) ≋ ((h ∙ g) ∙ f)
    test-associativity₁ = associativity {_◅_ = _∙_}

    test-associativity₂ : ∀ {k l} (f : k ⇒ l) {m} (g : l ⇒ m) {n} (h : m ⇒ n) → (h ∙ (g ∙ f)) ≋ ((h ∙ g) ∙ f)
    test-associativity₂ = associativity {_≤_ = _≋_}

-- Associativity : ∀
--   {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
--     (_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n)
--   {ℓ}
--     (_≤_ : ∀ {m n} → m ► n → m ► n → Set ℓ)
--   → Set (𝔞 ⊔ 𝔰 ⊔ ℓ)
-- Associativity {_►_ = _►_} _◅_ _≤_ =
--   ∀ {l} {m} {n} {w : m ► n} → Preservativity (λ ⋆ → _◅_ ⋆) (λ ⋆ → _◅_ ⋆) _≤_ (m ⟨ l ►_ ⟩→ n ∋ w ◅_) id (m ⟨ l ►_ ⟩→ n ∋ w ◅_)

-- -- record Associativity
-- --   {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
-- --     (_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n)
-- --   {𝔱} {▸ : 𝔄 → Set 𝔱}
-- --     (_◃_ : ∀ {m n} → m ► n → m ⟨ ▸ ⟩→ n)
-- --   {ℓ}
-- --     (_≤_ : ∀ {n} → ▸ n → ▸ n → Set ℓ)
-- --   : Set (𝔞 ⊔ 𝔰 ⊔ 𝔱 ⊔ ℓ) where
-- --   field
-- --     associativity : ∀ {l} (f : ▸ l) {m} (g : l ► m) {n} (h : m ► n) → (h ◃ (g ◃ f)) ≤ ((h ◅ g) ◃ f)

-- -- open Associativity ⦃ … ⦄ public

-- -- -- record Associativity
-- -- --   {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
-- -- --     (_▻_ : ∀ {l m n} → l ► m → m ⟨ _► n ⟩→ l)
-- -- --   {ℓ}
-- -- --     (_≤_ : ∀ {m n} → m ► n → m ► n → Set ℓ)
-- -- --   : Set (𝔞 ⊔ 𝔰 ⊔ ℓ) where
-- -- --   field
-- -- --     ⦃ `preservativity ⦄ : ∀ l m n w → Preservativity (_▻_ {l = l} {m = m} {n = n}) (_▻_ {l = l}) _≤_ (w ▻_) id (w ▻_)
-- -- -- --    ⦃ `preservativity ⦄ : ∀ n l w → Preservativity (λ ⋆ → _◅_ {n = n} ⋆) (λ ⋆ → _◅_ {l = l} ⋆) _≤_ (_◅ w) id (w ◅_)

-- -- -- -- record Associativity
-- -- -- --   {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
-- -- -- --     (_◅_ : ∀ {l m n} → m ► n → m ⟨ l ►_ ⟩→ n)
-- -- -- --   {ℓ}
-- -- -- --     (_≤_ : ∀ {m n} → m ► n → m ► n → Set ℓ)
-- -- -- --   : Set (𝔞 ⊔ 𝔰 ⊔ ℓ) where
-- -- -- --   field
-- -- -- --     ⦃ `preservativity ⦄ : ∀ l n w → Preservativity (flip (_◅_ {l = l} {n = n})) (flip _◅_) _≤_ (w ◅_) id (_◅ w)
-- -- -- -- --    ⦃ `preservativity ⦄ : ∀ n l w → Preservativity (λ ⋆ → _◅_ {n = n} ⋆) (λ ⋆ → _◅_ {l = l} ⋆) _≤_ (_◅ w) id (w ◅_)

-- -- -- -- -- record Associativity
-- -- -- -- --   {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
-- -- -- -- --     (_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n)
-- -- -- -- --   {ℓ}
-- -- -- -- --     (_≤_ : ∀ {m n} → m ► n → m ► n → Set ℓ)
-- -- -- -- --   : Set (𝔞 ⊔ 𝔰 ⊔ ℓ) where
-- -- -- -- --   field
-- -- -- -- --     ⦃ `preservativity ⦄ : ∀ n l w → Preservativity (λ ⋆ → _◅_ {n = n} ⋆) (λ ⋆ → _◅_ ⋆ {l = l}) _≤_ (_◅ w) id (w ◅_)

-- -- -- -- -- --    associativity : ∀ {k l} (f : k ► l) {m} (g : l ► m) {n} (h : m ► n) → (h ◅ (g ◅ f)) ≤ ((h ◅ g) ◅ f)

-- -- -- -- -- -- record Associativity
-- -- -- -- -- --   {a} {A : Set a} {b} {B : A → Set b} {c} {C : (x : A) → B x → Set c}
-- -- -- -- -- --     (_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n)
-- -- -- -- -- --   {ℓ}
-- -- -- -- -- --     (_≤_ : ∀ {m n} → m ► n → m ► n → Set ℓ)
-- -- -- -- -- --   : Set (𝔞 ⊔ 𝔰 ⊔ ℓ) where
-- -- -- -- -- --   field
-- -- -- -- -- --     ⦃ `preservativity ⦄ : Preservativity
-- -- -- -- -- --     associativity : ∀ {k l} (f : k ► l) {m} (g : l ► m) {n} (h : m ► n) → (h ◅ (g ◅ f)) ≤ ((h ◅ g) ◅ f)

-- -- -- -- -- -- open Associativity ⦃ … ⦄ public

-- -- -- -- -- -- -- record Associativity
-- -- -- -- -- -- --   {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
-- -- -- -- -- -- --     (_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n)
-- -- -- -- -- -- --   {ℓ}
-- -- -- -- -- -- --     (_≤_ : ∀ {m n} → m ► n → m ► n → Set ℓ)
-- -- -- -- -- -- --   : Set (𝔞 ⊔ 𝔰 ⊔ ℓ) where
-- -- -- -- -- -- --   field
-- -- -- -- -- -- --     associativity : ∀ {k l} (f : k ► l) {m} (g : l ► m) {n} (h : m ► n) → (h ◅ (g ◅ f)) ≤ ((h ◅ g) ◅ f)

-- -- -- -- -- -- -- open Associativity ⦃ … ⦄ public

-- -- -- -- -- -- -- -- record Associativity
-- -- -- -- -- -- -- --   {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
-- -- -- -- -- -- -- --     (_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n)
-- -- -- -- -- -- -- --   {𝔱} {▸ : 𝔄 → Set 𝔱}
-- -- -- -- -- -- -- --     (_◃_ : ∀ {m n} → m ► n → m ⟨ ▸ ⟩→ n)
-- -- -- -- -- -- -- --   {ℓ}
-- -- -- -- -- -- -- --     (_≤_ : ∀ {n} → ▸ n → ▸ n → Set ℓ)
-- -- -- -- -- -- -- --   : Set (𝔞 ⊔ 𝔰 ⊔ 𝔱 ⊔ ℓ) where
-- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- --     associativity : ∀ {l} (f : ▸ l) {m} (g : l ► m) {n} (h : m ► n) → (h ◃ (g ◃ f)) ≤ ((h ◅ g) ◃ f)

-- -- -- -- -- -- -- -- open Associativity ⦃ … ⦄ public

-- -- -- -- -- -- -- -- association : ∀
-- -- -- -- -- -- -- --   {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
-- -- -- -- -- -- -- --     (_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n)
-- -- -- -- -- -- -- --   {𝔱} {▸ : 𝔄 → Set 𝔱}
-- -- -- -- -- -- -- --     {_◃_ : ∀ {m n} → m ► n → m ⟨ ▸ ⟩→ n}
-- -- -- -- -- -- -- --   {ℓ}
-- -- -- -- -- -- -- --     (_≤_ : ∀ {n} → ▸ n → ▸ n → Set ℓ)
-- -- -- -- -- -- -- --   ⦃ _ : Associativity _◅_ _◃_ _≤_ ⦄
-- -- -- -- -- -- -- --   → ∀ {l} (f : ▸ l) {m} (g : l ► m) {n} (h : m ► n) → (h ◃ (g ◃ f)) ≤ ((h ◅ g) ◃ f)
-- -- -- -- -- -- -- -- association _◅_ _≤_ = associativity {_◅_ = _◅_} {_≤_ = _≤_}


text:
{-# OPTIONS --safe #-}
module Cubical.ZCohomology.Groups.Connected where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat
open import Cubical.Data.Int renaming (_+_ to _+ℤ_; +Comm to +ℤ-comm ; +Assoc to +ℤ-assoc)
open import Cubical.Data.Sigma hiding (_×_)

open import Cubical.HITs.SetTruncation as ST
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.Truncation as T
open import Cubical.HITs.Nullification

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties

open import Cubical.Homotopy.Connected

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Groups.Unit

private
  H⁰-connected-type : ∀ {ℓ} {A : Type ℓ} (a : A) → isConnected 2 A → Iso (coHom 0 A) ℤ
  Iso.fun (H⁰-connected-type a con) = ST.rec isSetℤ λ f → f a
  Iso.inv (H⁰-connected-type a con) b = ∣ (λ x → b) ∣₂
  Iso.rightInv (H⁰-connected-type a con) b = refl
  Iso.leftInv (H⁰-connected-type a con) =
    ST.elim (λ _ → isOfHLevelPath 2 isSetSetTrunc _ _)
           λ f → cong ∣_∣₂ (funExt λ x → T.rec₊ (isSetℤ _ _) (cong f) (isConnectedPath 1 con a x .fst))

open IsGroupHom
open Iso

H⁰-connected : ∀ {ℓ} {A : Type ℓ} (a : A) → ((x : A) → ∥ a ≡ x ∥₁) → GroupIso (coHomGr 0 A) ℤGroup
fun (fst (H⁰-connected a con)) = ST.rec isSetℤ (λ f → f a)
inv (fst (H⁰-connected a con)) b = ∣ (λ _ → b) ∣₂
rightInv (fst (H⁰-connected a con)) _ = refl
leftInv (fst (H⁰-connected a con)) =
  ST.elim (λ _ → isProp→isSet (isSetSetTrunc _ _))
        (λ f → cong ∣_∣₂ (funExt λ x → PT.rec (isSetℤ _ _) (cong f) (con x)))
snd (H⁰-connected a con) = makeIsGroupHom (ST.elim2 (λ _ _ → isProp→isSet (isSetℤ _ _)) λ x y → refl)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text: module Primitive where

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2011-10-02
{-# OPTIONS --show-implicit #-}
module Issue483a where

data _≡_ {A : Set}(a : A) : A → Set where
  refl : a ≡ a

data Empty : Set where

postulate A : Set

abort : .Empty → A
abort ()

test : let X : .Set1 → A
           X = _
       in  (x : Empty) → X Set ≡ abort x
test x = refl

-- this should fail with message like
--
--  Cannot instantiate the metavariable _16 to abort x since it
--  contains the variable x which is not in scope of the metavariable
--  when checking that the expression refl has type _16 _ ≡ abort x
--
-- a solution like X = λ _ → abort x : Set1 → A
-- would be invalid even though x is irrelevant, because there is no
-- term of type Set1 → A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
postulate
  A : Set
  F : { x : A } → Set
  G : ⦃ x : A ⦄ → Set


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.SIP

open import Cubical.Functions.FunExtEquiv

open import Cubical.Data.Nat
open import Cubical.Data.Vec

module _ {ℓ₁ ℓ₂ : Level} where

  NAryFunStructure : (n : ℕ) (S : Type ℓ₁ → Type ℓ₂)
    → Type ℓ₁ → Type (nAryLevel ℓ₁ ℓ₂ n)
  NAryFunStructure n S X = nAryOp n X (S X)

  -- iso for n-ary functions
  NAryFunEquivStr : (n : ℕ) {S : Type ℓ₁ → Type ℓ₂} {ℓ₃ : Level} (ι : StrEquiv S ℓ₃)
    → StrEquiv (NAryFunStructure n S) (ℓ-max ℓ₁ ℓ₃)
  NAryFunEquivStr n ι (X , fX) (Y , fY) e =
    (xs : Vec X n) → ι (X , fX $ⁿ xs) (Y , fY $ⁿ map (equivFun e) xs) e

  nAryFunUnivalentStr : {S : Type ℓ₁ → Type ℓ₂} (n : ℕ) {ℓ₃ : Level}
    (ι : StrEquiv S ℓ₃) (θ : UnivalentStr S ι)
    → UnivalentStr (NAryFunStructure n S) (NAryFunEquivStr n ι)
  nAryFunUnivalentStr n ι θ =
    SNS→UnivalentStr (NAryFunEquivStr n ι) λ fX fY →
    compEquiv
      (equivPi λ xs → UnivalentStr→SNS _ ι θ _ _)
      (nAryFunExtEquiv n fX fY)

module _ {ℓ₁ ℓ₂ : Level} where
  -- unary
  UnaryFunEquivStr : {S : Type ℓ₁ → Type ℓ₂} {ℓ₃ : Level} (ι : StrEquiv S ℓ₃)
    → StrEquiv (NAryFunStructure 1 S) (ℓ-max ℓ₁ ℓ₃)
  UnaryFunEquivStr ι (A , f) (B , g) e =
    (x : A) → ι (A , f x) (B , g (equivFun e x)) e

  unaryFunUnivalentStr : {S : Type ℓ₁ → Type ℓ₂} {ℓ₃ : Level}
    (ι : StrEquiv S ℓ₃) (θ : UnivalentStr S ι)
    → UnivalentStr (NAryFunStructure 1 S) (UnaryFunEquivStr ι)
  unaryFunUnivalentStr ι θ =
    SNS→UnivalentStr (UnaryFunEquivStr ι) λ fX fY →
    compEquiv (equivPi λ _ → UnivalentStr→SNS _ ι θ _ _) funExtEquiv

  -- binary
  BinaryFunEquivStr : {S : Type ℓ₁ → Type ℓ₂} {ℓ₃ : Level} (ι : StrEquiv S ℓ₃)
    → StrEquiv (NAryFunStructure 2 S) (ℓ-max ℓ₁ ℓ₃)
  BinaryFunEquivStr ι (A , f) (B , g) e =
    (x y : A) → ι (A , f x y) (B , g (equivFun e x) (equivFun e y)) e

  binaryFunUnivalentStr : {S : Type ℓ₁ → Type ℓ₂} {ℓ₃ : Level}
    (ι : StrEquiv S ℓ₃) (θ : UnivalentStr S ι)
    → UnivalentStr (NAryFunStructure 2 S) (BinaryFunEquivStr ι)
  binaryFunUnivalentStr ι θ =
    SNS→UnivalentStr (BinaryFunEquivStr ι) λ fX fY →
    compEquiv (equivPi λ _ → equivPi λ _ → UnivalentStr→SNS _ ι θ _ _) funExt₂Equiv


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.ShapeView {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Properties.Reflexivity

open import Tools.Product
open import Tools.Empty using (⊥; ⊥-elim)
import Tools.PropositionalEquality as PE

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

-- Type for maybe embeddings of reducible types
data MaybeEmb (l : TypeLevel) (⊩⟨_⟩ : TypeLevel → Set) : Set where
  noemb : ⊩⟨ l ⟩ → MaybeEmb l ⊩⟨_⟩
  emb   : ∀ {l′} → l′ <∞ l → MaybeEmb l′ ⊩⟨_⟩ → MaybeEmb l ⊩⟨_⟩

-- Specific reducible types with possible embedding

_⊩⟨_⟩U_^_ : (Γ : Con Term) (l : TypeLevel) (A : Term) (ll : TypeLevel) → Set
Γ ⊩⟨ l ⟩U A ^ ll = MaybeEmb l (λ l′ → Γ ⊩′⟨ l′ ⟩U A ^ ll)

_⊩⟨_⟩ℕ_ : (Γ : Con Term) (l : TypeLevel) (A : Term) → Set
Γ ⊩⟨ l ⟩ℕ A = MaybeEmb l (λ l′ → Γ ⊩ℕ A)

_⊩⟨_⟩Empty_^_ : (Γ : Con Term) (l : TypeLevel) (A : Term) (ll : Level) → Set
Γ ⊩⟨ l ⟩Empty A ^ ll = MaybeEmb l (λ l′ → Γ ⊩Empty A ^ ll)

_⊩⟨_⟩ne_^[_,_] : (Γ : Con Term) (l : TypeLevel) (A : Term) (r : Relevance) (ll : Level) → Set
Γ ⊩⟨ l ⟩ne A ^[ r , ll ] = MaybeEmb l (λ l′ → Γ ⊩ne A ^[ r , ll ])

_⊩⟨_⟩Π_^[_,_] : (Γ : Con Term) (l : TypeLevel) (A : Term) → Relevance → Level → Set
Γ ⊩⟨ l ⟩Π A ^[ r , lΠ ] = MaybeEmb l (λ l′ → Γ ⊩′⟨ l′ ⟩Π A ^[ r , lΠ ])

_⊩⟨_⟩∃_^_ : (Γ : Con Term) (l : TypeLevel) (A : Term) (ll : Level) → Set
Γ ⊩⟨ l ⟩∃ A ^ ll = MaybeEmb l (λ l′ → Γ ⊩′⟨ l′ ⟩∃ A ^ ll)

-- Construct a general reducible type from a specific

U-intr : ∀ {l Γ A ll } → (UA : Γ ⊩⟨ l ⟩U A ^ ll) → Γ ⊩⟨ l ⟩ A ^ [ ! , ll ]
U-intr (noemb UA) = Uᵣ UA
U-intr {l = ι ¹} (emb emb< x) = emb emb< (U-intr x)
U-intr {l = ∞}  (emb ∞< x) = emb ∞< (U-intr x)

ℕ-intr : ∀ {l A Γ} → Γ ⊩⟨ l ⟩ℕ A → Γ ⊩⟨ l ⟩ A ^ [ ! , ι ⁰ ]
ℕ-intr (noemb x) = ℕᵣ x
ℕ-intr {l = ι ¹} (emb emb< x) = emb emb< (ℕ-intr x)
ℕ-intr {l = ∞}  (emb ∞< x) = emb ∞< (ℕ-intr x)

Empty-intr : ∀ {l A Γ ll} → Γ ⊩⟨ l ⟩Empty A ^ ll → Γ ⊩⟨ l ⟩ A ^ [ % , ι ll ]
Empty-intr (noemb x) = Emptyᵣ x
Empty-intr {l = ι ¹} (emb emb< x) = emb emb< (Empty-intr x)
Empty-intr {l = ∞}  (emb ∞< x) = emb ∞< (Empty-intr x)

ne-intr : ∀ {l A Γ r ll} → Γ ⊩⟨ l ⟩ne A ^[ r , ll ] → Γ ⊩⟨ l ⟩ A ^ [ r , ι ll ]
ne-intr (noemb x) = ne x
ne-intr {l = ι ¹} (emb emb< x) = emb emb< (ne-intr x)
ne-intr {l = ∞}  (emb ∞< x) = emb ∞< (ne-intr x)

Π-intr : ∀ {l A Γ r ll} → Γ ⊩⟨ l ⟩Π A ^[ r , ll ]  → Γ ⊩⟨ l ⟩ A ^ [ r , ι ll ]
Π-intr (noemb x) = Πᵣ x
Π-intr {l = ι ¹} (emb emb< x) = emb emb< (Π-intr x)
Π-intr {l = ∞}  (emb ∞< x) = emb ∞< (Π-intr x)

∃-intr : ∀ {l A Γ ll} → Γ ⊩⟨ l ⟩∃ A ^ ll → Γ ⊩⟨ l ⟩ A ^ [ % , ι ll ]
∃-intr (noemb x) = ∃ᵣ x
∃-intr {l = ι ¹} (emb emb< x) = emb emb< (∃-intr x)
∃-intr {l = ∞}  (emb ∞< x) = emb ∞< (∃-intr x)

-- Construct a specific reducible type from a general with some criterion

U-elim′ : ∀ {l Γ A r l′ ll} → Γ ⊢ A ⇒* Univ r l′ ^ [ ! , ll ] → Γ ⊩⟨ l ⟩ A ^ [ ! , ll ] → Γ ⊩⟨ l ⟩U A ^ ll
U-elim′ D (Uᵣ′ A ll r l l< e D') = noemb (Uᵣ r l l< e D')
U-elim′ D (ℕᵣ D') =  ⊥-elim (U≢ℕ (whrDet* (D ,  Uₙ) (red D' , ℕₙ)))
U-elim′ D (ne′ K D' neK K≡K) =  ⊥-elim (U≢ne neK (whrDet* (D ,  Uₙ) (red D' , ne neK)))
U-elim′ D (Πᵣ′ rF lF lG _ _ F G D' ⊢F ⊢G A≡A [F] [G] G-ext) = ⊥-elim (U≢Π (whrDet* (D , Uₙ) (red D' , Πₙ)))
U-elim′ {ι ¹} D (emb emb< x) with U-elim′ D x
U-elim′ {ι ¹} D (emb emb< x) | noemb x₁ = emb emb< (noemb x₁)
U-elim′ {ι ¹} D (emb emb< x) | emb () x₁
U-elim′ {∞} D (emb ∞< x) with U-elim′ D x
U-elim′ {∞} D (emb ∞< x) | noemb x₁ = emb ∞< (noemb x₁)
U-elim′ {∞} D (emb ∞< x) | emb <l x₁ = emb {l′ = ι ¹} ∞< (emb <l x₁)

U-elim : ∀ {l Γ r l′ ll′} → Γ ⊩⟨ l ⟩ Univ r l′ ^ [ ! , ll′ ] → Γ ⊩⟨ l ⟩U Univ r l′ ^ ll′
U-elim [U] = U-elim′ (id (escape [U])) [U]

ℕ-elim′ : ∀ {l A Γ ll} → Γ ⊢ A ⇒* ℕ ^ [ ! , ll ]  → Γ ⊩⟨ l ⟩ A ^ [ ! , ll ] → Γ ⊩⟨ l ⟩ℕ A
ℕ-elim′ D (Uᵣ′ _ _ _ _ l< PE.refl [[ _ , _ , d ]]) = ⊥-elim (U≢ℕ (whrDet* (d , Uₙ) (D , ℕₙ)))
ℕ-elim′ D (ℕᵣ D′) = noemb D′
ℕ-elim′ D (ne′ K D′ neK K≡K) =
  ⊥-elim (ℕ≢ne neK (whrDet* (D , ℕₙ) (red D′ , ne neK)))
ℕ-elim′ D (Πᵣ′ rF lF lG _ _ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (ℕ≢Π (whrDet* (D , ℕₙ) (red D′ , Πₙ)))
ℕ-elim′ {ι ¹} D (emb emb< x) with ℕ-elim′ D x
ℕ-elim′ {ι ¹} D (emb emb< x) | noemb x₁ = emb emb< (noemb x₁)
ℕ-elim′ {ι ¹} D (emb emb< x) | emb () x₁
ℕ-elim′ {∞} D (emb ∞< x) with ℕ-elim′ D x
ℕ-elim′ {∞} D (emb ∞< x) | noemb x₁ = emb ∞< (noemb x₁)
ℕ-elim′ {∞} D (emb ∞< x) | emb <l x₁ = emb {l′ = ι ¹} ∞< (emb <l x₁)

ℕ-elim : ∀ {Γ l ll } → Γ ⊩⟨ l ⟩ ℕ ^ [ ! , ll ] → Γ ⊩⟨ l ⟩ℕ ℕ
ℕ-elim [ℕ] = ℕ-elim′ (id (escape [ℕ])) [ℕ]

Empty-elim′ : ∀ {l A ll Γ} → Γ ⊢ A ⇒* Empty ll ^ [ % , ι ll ] → Γ ⊩⟨ l ⟩ A ^ [ % , ι ll ] → Γ ⊩⟨ l ⟩Empty A ^ ll
Empty-elim′ D (Emptyᵣ D′) = noemb D′
Empty-elim′ D (ne′ K D′ neK K≡K) =
  ⊥-elim (Empty≢ne neK (whrDet* (D , Emptyₙ) (red D′ , ne neK)))
Empty-elim′ D (Πᵣ′ rF lF lG _ _ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (Empty≢Π (whrDet* (D , Emptyₙ) (red D′ , Πₙ)))
Empty-elim′ D (∃ᵣ′  F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (Empty≢∃ (whrDet* (D , Emptyₙ) (red D′ , ∃ₙ)))
Empty-elim′ {ι ¹} D (emb emb< x) with Empty-elim′ D x
Empty-elim′ {ι ¹} D (emb emb< x) | noemb x₁ = emb emb< (noemb x₁)
Empty-elim′ {ι ¹} D (emb emb< x) | emb () x₁
Empty-elim′ {∞} D (emb ∞< x) with Empty-elim′ D x
Empty-elim′ {∞} D (emb ∞< x) | noemb x₁ = emb ∞< (noemb x₁)
Empty-elim′ {∞} D (emb ∞< x) | emb <l x₁ = emb {l′ = ι ¹} ∞< (emb <l x₁)

Empty-elim : ∀ {Γ l ll } → Γ ⊩⟨ l ⟩ Empty ll ^ [ % , ι ll ] → Γ ⊩⟨ l ⟩Empty Empty ll ^ ll
Empty-elim [Empty] = Empty-elim′ (id (escape [Empty])) [Empty]

ne-elim′ : ∀ {l A Γ K r ll ll'} → Γ ⊢ A ⇒* K ^ [ r , ι ll ] → Neutral K → Γ ⊩⟨ l ⟩ A ^ [ r , ll' ] → ι ll PE.≡  ll' → Γ ⊩⟨ l ⟩ne A ^[ r , ll ]
ne-elim′ D neK (Uᵣ′ _ _ _ _ l< PE.refl [[ _ , _ , d ]]) e = ⊥-elim (U≢ne neK (whrDet* (d , Uₙ) (D , ne neK)))
ne-elim′ D neK (ℕᵣ D′) e = ⊥-elim (ℕ≢ne neK (whrDet* (red D′ , ℕₙ) (D , ne neK)))
ne-elim′ D neK (ne (ne K D′ neK′ K≡K)) PE.refl = noemb (ne K D′ neK′ K≡K)
ne-elim′ D neK (Πᵣ′ rF lF lG _ _ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) e =
  ⊥-elim (Π≢ne neK (whrDet* (red D′ , Πₙ) (D , ne neK)))
ne-elim′ D neK (∃ᵣ′ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) e =
  ⊥-elim (∃≢ne neK (whrDet* (red D′ , ∃ₙ) (D , ne neK)))
ne-elim′ D neK (Emptyᵣ D′) e = ⊥-elim (Empty≢ne neK (whrDet* (red D′ , Emptyₙ) (D , ne neK)))
ne-elim′ {ι ¹} D neK (emb emb< x) e with ne-elim′ D neK x e
ne-elim′ {ι ¹} D neK (emb emb< x) e | noemb x₁ = emb emb< (noemb x₁)
ne-elim′ {ι ¹} D neK (emb emb< x) e | emb () x₁
ne-elim′ {∞} D neK (emb ∞< x) e with ne-elim′ D neK x e
ne-elim′ {∞} D _ (emb ∞< x) e | noemb x₁ = emb ∞< (noemb x₁)
ne-elim′ {∞} D _ (emb ∞< x) e | emb <l x₁ = emb {l′ = ι ¹} ∞< (emb <l x₁)

ne-elim : ∀ {Γ l K r ll} → Neutral K  → Γ ⊩⟨ l ⟩ K ^ [ r , ι ll ] → Γ ⊩⟨ l ⟩ne K ^[ r , ll ]
ne-elim neK [K] = ne-elim′ (id (escape [K])) neK [K] PE.refl

Π-elim′ : ∀ {l A Γ F G rF lF lG r lΠ} → Γ ⊢ A ⇒* Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ r , ι lΠ ] → Γ ⊩⟨ l ⟩ A ^ [ r , ι lΠ ]  → Γ ⊩⟨ l ⟩Π A ^[ r , lΠ ]
Π-elim′ D (Uᵣ′ _ _ _ _ l< X [[ _ , _ , d ]]) = ⊥-elim (U≢Π (whrDet* (d , Uₙ) (D , Πₙ)))
Π-elim′ D (ℕᵣ D′) = ⊥-elim (ℕ≢Π (whrDet* (red D′ , ℕₙ) (D , Πₙ)))
Π-elim′ D (Emptyᵣ D′) = ⊥-elim (Empty≢Π (whrDet* (red D′ , Emptyₙ) (D , Πₙ)))
Π-elim′ D (ne′ K D′ neK K≡K) =
  ⊥-elim (Π≢ne neK (whrDet* (D , Πₙ) (red D′ , ne neK)))
Π-elim′ D (Πᵣ′ rF lF lG lF≤ lG≤ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  noemb (Πᵣ rF lF lG lF≤ lG≤ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext)
Π-elim′ D (∃ᵣ′ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (Π≢∃ (whrDet* (D , Πₙ) (red D′ , ∃ₙ)))
Π-elim′ {ι ¹} D (emb emb< x) with Π-elim′ D x
Π-elim′ {ι ¹} D (emb emb< x) | noemb x₁ = emb emb< (noemb x₁)
Π-elim′ {ι ¹} D (emb emb< x) | emb () x₁
Π-elim′ {∞} D (emb ∞< x) with Π-elim′ D x
Π-elim′ {∞} D (emb ∞< x) | noemb x₁ = emb ∞< (noemb x₁)
Π-elim′ {∞} D (emb ∞< x) | emb <l x₁ = emb {l′ = ι ¹} ∞< (emb <l x₁)

Π-elim : ∀ {Γ F G rF lF lG r lΠ l} → Γ ⊩⟨ l ⟩ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ r , ι lΠ ] → Γ ⊩⟨ l ⟩Π Π F ^ rF ° lF ▹ G ° lG ° lΠ ^[ r , lΠ ]
Π-elim [Π] = Π-elim′ (id (escape [Π])) [Π]

∃-elim′ : ∀ {l A Γ F G ll} → Γ ⊢ A ⇒* ∃ F ▹ G ^ [ % , ι ll ] → Γ ⊩⟨ l ⟩ A ^ [ % , ι ll ] → Γ ⊩⟨ l ⟩∃ A  ^ ll
∃-elim′ D (Emptyᵣ D′) = ⊥-elim (Empty≢∃ (whrDet* (red D′ , Emptyₙ) (D , ∃ₙ)))
∃-elim′ D (ne′ K D′ neK K≡K) =
  ⊥-elim (∃≢ne neK (whrDet* (D , ∃ₙ) (red D′ , ne neK)))
∃-elim′ D (Πᵣ′ rF lF lG _ _ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  ⊥-elim (Π≢∃ (whrDet* (red D′ , Πₙ) (D , ∃ₙ)))
∃-elim′ D (∃ᵣ′ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext) =
  noemb (∃ᵣ F G D′ ⊢F ⊢G A≡A [F] [G] G-ext)
∃-elim′ {ι ¹} D (emb emb< x) with ∃-elim′ D x
∃-elim′ {ι ¹} D (emb emb< x) | noemb x₁ = emb emb< (noemb x₁)
∃-elim′ {ι ¹} D (emb emb< x) | emb () x₁
∃-elim′ {∞} D (emb ∞< x) with ∃-elim′ D x
∃-elim′ {∞} D (emb ∞< x) | noemb x₁ = emb ∞< (noemb x₁)
∃-elim′ {∞} D (emb ∞< x) | emb <l x₁ = emb {l′ = ι ¹} ∞< (emb <l x₁)

∃-elim : ∀ {Γ F G l ll} → Γ ⊩⟨ l ⟩ ∃ F ▹ G ^ [ % , ι ll ] → Γ ⊩⟨ l ⟩∃ (∃ F ▹ G) ^ ll
∃-elim [∃] = ∃-elim′ (id (escape [∃])) [∃]

-- Extract a type and a level from a maybe embedding
extractMaybeEmb : ∀ {l ⊩⟨_⟩} → MaybeEmb l ⊩⟨_⟩ → ∃ λ l′ → ⊩⟨ l′ ⟩
extractMaybeEmb (noemb x) = _ , x
extractMaybeEmb (emb <l x) = extractMaybeEmb x

-- A view for constructor equality of types where embeddings are ignored
data ShapeView Γ : ∀ l l′ A B r r' (p : Γ ⊩⟨ l ⟩ A ^ r) (q : Γ ⊩⟨ l′ ⟩ B ^ r') → Set where
  Uᵥ : ∀ {A B l l′ ll ll′} UA UB → ShapeView Γ l l′ A B [ ! , ll ] [ ! , ll′ ] (Uᵣ UA) (Uᵣ UB)
  ℕᵥ : ∀ {A B l l′} ℕA ℕB → ShapeView Γ l l′ A B [ ! , ι ⁰ ] [ ! , ι ⁰ ] (ℕᵣ ℕA) (ℕᵣ ℕB)
  Emptyᵥ : ∀ {A B l l′ ll ll'} EmptyA EmptyB → ShapeView Γ l l′ A B [ % , ι ll ] [ % , ι ll' ] (Emptyᵣ EmptyA) (Emptyᵣ EmptyB)
  ne  : ∀ {A B l l′ r lr r' lr'} neA neB
      → ShapeView Γ l l′ A B [ r , ι lr ] [ r' , ι lr' ] (ne neA) (ne neB)
  Πᵥ : ∀ {A B l l′ r r' lΠ lΠ' } ΠA ΠB
    → ShapeView Γ l l′ A B [ r , ι lΠ ] [ r' , ι lΠ' ] (Πᵣ ΠA) (Πᵣ ΠB)
  ∃ᵥ : ∀ {A B l l′ ll ll'} ∃A ∃B
    → ShapeView Γ l l′ A B [ % , ι ll ] [ % , ι ll' ] (∃ᵣ ∃A) (∃ᵣ ∃B)
  emb⁰¹ : ∀ {A B r r' l p q}
        → ShapeView Γ (ι ⁰) l A B r r' p q
        → ShapeView Γ (ι ¹) l A B r r' (emb emb< p) q
  emb¹⁰ : ∀ {A B r r' l p q}
        → ShapeView Γ l (ι ⁰) A B r r' p q
        → ShapeView Γ l (ι ¹) A B r r' p (emb emb< q)
  emb¹∞ : ∀ {A B r r' l p q}
        → ShapeView Γ (ι ¹) l A B r r' p q
        → ShapeView Γ ∞ l A B r r' (emb ∞< p) q
  emb∞¹ : ∀ {A B r r' l p q}
        → ShapeView Γ l (ι ¹) A B r r' p q
        → ShapeView Γ l ∞ A B r r' p (emb ∞< q)

-- Construct a shape view from an equality
goodCases : ∀ {l l′ Γ A B r r'} ([A] : Γ ⊩⟨ l ⟩ A ^ r) ([B] : Γ ⊩⟨ l′ ⟩ B ^ r')
          → Γ ⊩⟨ l ⟩ A ≡ B ^ r / [A] → ShapeView Γ l l′ A B r r' [A] [B]
goodCases (Uᵣ UA) (Uᵣ UB) A≡B = Uᵥ UA UB
goodCases (Uᵣ′ _ _ _ _ _ _ ⊢Γ) (ℕᵣ D) D' = ⊥-elim (U≢ℕ (whrDet* (D' ,  Uₙ) (red D , ℕₙ)))
goodCases (Uᵣ′ _ _ _ _ _ _ ⊢Γ) (Emptyᵣ D) D' =  ⊥-elim (U≢Empty (whrDet* (D' ,  Uₙ) (red D , Emptyₙ)))
goodCases (Uᵣ′ _ _ _ _ _ _ ⊢Γ) (ne′ K D neK K≡K) D' = ⊥-elim (U≢ne neK (whrDet* (D' ,  Uₙ) (red D , ne neK)))
goodCases (Uᵣ′ _ _ _ _ _ _ ⊢Γ) (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) D' =
  ⊥-elim (U≢Π (whrDet* (D' , Uₙ) (red D , Πₙ)))
goodCases (Uᵣ′ _ _ _ _ _ _ ⊢Γ) (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) D' =
  ⊥-elim (U≢∃ (whrDet* (D' , Uₙ) (red D , ∃ₙ)))
goodCases (ℕᵣ D) (Uᵣ′ _ _ _ _ _ _ D') A≡B = ⊥-elim (U≢ℕ (whrDet* (red D' ,  Uₙ) (A≡B , ℕₙ)))
goodCases (ℕᵣ _) (Emptyᵣ D') D =
  ⊥-elim (ℕ≢Empty (whrDet* (D , ℕₙ) (red D' , Emptyₙ)))
goodCases (ℕᵣ ℕA) (ℕᵣ ℕB) A≡B = ℕᵥ ℕA ℕB
goodCases (ℕᵣ D) (ne′ K D₁ neK K≡K) A≡B =
  ⊥-elim (ℕ≢ne neK (whrDet* (A≡B , ℕₙ) (red D₁ , ne neK)))
goodCases (ℕᵣ D) (Πᵣ′ rF lF lG _ _ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) A≡B =
  ⊥-elim (ℕ≢Π (whrDet* (A≡B , ℕₙ) (red D₁ , Πₙ)))
goodCases (ℕᵣ D) (∃ᵣ′ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) A≡B =
  ⊥-elim (ℕ≢∃ (whrDet* (A≡B , ℕₙ) (red D₁ , ∃ₙ)))
goodCases (Emptyᵣ D) (Uᵣ′ _ _ _ _ _ _ D') A≡B = ⊥-elim (U≢Empty (whrDet* (red D' ,  Uₙ) (A≡B , Emptyₙ)))
goodCases (Emptyᵣ _) (ℕᵣ D') D =
   ⊥-elim (ℕ≢Empty (whrDet* (red D' , ℕₙ) (D , Emptyₙ)))
goodCases (Emptyᵣ EmptyA) (Emptyᵣ EmptyB) A≡B = Emptyᵥ EmptyA EmptyB
goodCases (Emptyᵣ D) (ne′ K D₁ neK K≡K) A≡B =
  ⊥-elim (Empty≢ne neK (whrDet* (A≡B , Emptyₙ) (red D₁ , ne neK)))
goodCases (Emptyᵣ D) (Πᵣ′ rF lF lG _ _ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) A≡B =
  ⊥-elim (Empty≢Π (whrDet* (A≡B , Emptyₙ) (red D₁ , Πₙ)))
goodCases (Emptyᵣ D) (∃ᵣ′ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) A≡B =
  ⊥-elim (Empty≢∃ (whrDet* (A≡B , Emptyₙ) (red D₁ , ∃ₙ)))
goodCases (ne′ K D neK K≡K) (Uᵣ′ _ _ _ _ _ _ D') (ne₌ M D'' neM K≡M) =
  ⊥-elim (U≢ne neM (whrDet* (red D' ,  Uₙ) (red D'' , ne neM)))
goodCases (ne′ K D neK K≡K) (ℕᵣ D₁) (ne₌ M D′ neM K≡M) =
  ⊥-elim (ℕ≢ne neM (whrDet* (red D₁ , ℕₙ) (red D′ , ne neM)))
goodCases (ne′ K D neK K≡K) (Emptyᵣ D₁) (ne₌ M D′ neM K≡M) =
  ⊥-elim (Empty≢ne neM (whrDet* (red D₁ , Emptyₙ) (red D′ , ne neM)))
goodCases (ne neA) (ne neB) A≡B = ne neA neB
goodCases (ne′ K D neK K≡K) (Πᵣ′ rF lF lG _ _ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) (ne₌ M D′ neM K≡M) =
  ⊥-elim (Π≢ne neM (whrDet* (red D₁ , Πₙ) (red D′ , ne neM)))
goodCases (ne′ K D neK K≡K) (∃ᵣ′ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext) (ne₌ M D′ neM K≡M) =
  ⊥-elim (∃≢ne neM (whrDet* (red D₁ , ∃ₙ) (red D′ , ne neM)))
goodCases (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Uᵣ′ _ _ _ _ _ _ D')
          (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (U≢Π (whrDet* (red D' ,  Uₙ) (D′ , Πₙ)))
goodCases (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (ℕᵣ D₁)
          (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (ℕ≢Π (whrDet* (red D₁ , ℕₙ) (D′ , Πₙ)))
goodCases (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Emptyᵣ D₁)
          (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (Empty≢Π (whrDet* (red D₁ , Emptyₙ) (D′ , Πₙ)))
goodCases (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (ne′ K D₁ neK K≡K)
          (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (Π≢ne neK (whrDet* (D′ , Πₙ) (red D₁ , ne neK)))
goodCases (Πᵣ ΠA) (Πᵣ ΠB) A≡B = Πᵥ ΠA ΠB
goodCases (Πᵣ′ rF lF lG _ _ 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′]) =
  ⊥-elim (Π≢∃ (whrDet* (D′ , Πₙ) (red D₁ , ∃ₙ)))
goodCases (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Uᵣ′ _ _ _ _ _ _ D')
          (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (U≢∃ (whrDet* (red D' ,  Uₙ) (D′ , ∃ₙ)))
goodCases (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (ℕᵣ D₁)
          (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (ℕ≢∃ (whrDet* (red D₁ , ℕₙ) (D′ , ∃ₙ)))
goodCases (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Emptyᵣ D₁)
          (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (Empty≢∃ (whrDet* (red D₁ , Emptyₙ) (D′ , ∃ₙ)))
goodCases (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (ne′ K D₁ neK K≡K)
          (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (∃≢ne neK (whrDet* (D′ , ∃ₙ) (red D₁ , ne neK)))
goodCases (∃ᵣ′ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁)
          (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ⊥-elim (Π≢∃ (whrDet* (red D , Πₙ) (D′ , ∃ₙ)))
goodCases (∃ᵣ ∃A) (∃ᵣ ∃B) A≡B = ∃ᵥ ∃A ∃B
goodCases {l} {ι ¹} [A] (emb emb< x) A≡B = emb¹⁰ (goodCases {l} {ι ⁰} [A] x A≡B)
goodCases {l} {∞} [A] (emb ∞< x) A≡B = emb∞¹ (goodCases {l} {ι ¹} [A] x A≡B)
goodCases {ι ¹} {l} (emb emb< x) [B] A≡B = emb⁰¹ (goodCases {ι ⁰} {l} x [B] A≡B)
goodCases {∞} {l} (emb ∞< x) [B] A≡B = emb¹∞ (goodCases {ι ¹} {l} x [B] A≡B)

-- Construct an shape view between two derivations of the same type
goodCasesRefl : ∀ {l l′ Γ A r r'} ([A] : Γ ⊩⟨ l ⟩ A ^ r) ([A′] : Γ ⊩⟨ l′ ⟩ A ^ r')
              → ShapeView Γ l l′ A A r r' [A] [A′]
goodCasesRefl [A] [A′] = goodCases [A] [A′] (reflEq [A])

-- A view for constructor equality between three types
data ShapeView₃ Γ : ∀ l l′ l″ A B C r1 r2 r3
                 (p : Γ ⊩⟨ l   ⟩ A ^ r1)
                 (q : Γ ⊩⟨ l′  ⟩ B ^ r2)
                 (r : Γ ⊩⟨ l″ ⟩ C ^ r3) → Set where
  Uᵥ : ∀ {A B C l l′ l″ ll ll′ ll″ } UA UB UC → ShapeView₃ Γ l l′ l″ A B C [ ! , ll ] [ ! , ll′ ] [ ! , ll″ ]
                                               (Uᵣ UA) (Uᵣ UB) (Uᵣ UC)
  ℕᵥ : ∀ {A B C l l′ l″} ℕA ℕB ℕC
    → ShapeView₃ Γ l l′ l″ A B C [ ! , ι ⁰ ] [ ! , ι ⁰ ] [ ! , ι ⁰ ] (ℕᵣ ℕA) (ℕᵣ ℕB) (ℕᵣ ℕC)
  Emptyᵥ : ∀ {A B C l l′ l″ ll ll′ ll″} EmptyA EmptyB EmptyC
    → ShapeView₃ Γ l l′ l″ A B C [ % , ι ll ] [ % , ι ll′ ] [ % , ι ll″ ] (Emptyᵣ EmptyA) (Emptyᵣ EmptyB) (Emptyᵣ EmptyC)
  ne  : ∀ {A B C r1 r2 r3 l1 l2 l3 l l′ l″} neA neB neC
      → ShapeView₃ Γ l l′ l″ A B C [ r1 , ι l1 ] [ r2 , ι l2 ] [ r3 , ι l3 ] (ne neA) (ne neB) (ne neC)
  Πᵥ : ∀ {A B C r1 r2 r3 lΠ1 lΠ2 lΠ3 l l′ l″} ΠA ΠB ΠC
    → ShapeView₃ Γ l l′ l″ A B C [ r1 , ι lΠ1 ] [ r2 , ι lΠ2 ] [ r3 , ι lΠ3 ] (Πᵣ ΠA) (Πᵣ ΠB) (Πᵣ ΠC)
  ∃ᵥ : ∀ {A B C l l′ l″ ll ll' ll''} ΠA ΠB ΠC
    → ShapeView₃ Γ l l′ l″ A B C [ % , ι ll ] [ % , ι ll' ] [ % , ι ll'' ] (∃ᵣ ΠA) (∃ᵣ ΠB) (∃ᵣ ΠC)
  emb⁰¹¹ : ∀ {A B C l l′ r1 r2 r3 p q r}
         → ShapeView₃ Γ (ι ⁰) l l′ A B C r1 r2 r3 p q r
         → ShapeView₃ Γ (ι ¹) l l′ A B C r1 r2 r3 (emb emb< p) q r
  emb¹⁰¹ : ∀ {A B C l l′ r1 r2 r3  p q r}
         → ShapeView₃ Γ l (ι ⁰) l′ A B C r1 r2 r3 p q r
         → ShapeView₃ Γ l (ι ¹) l′ A B C r1 r2 r3 p (emb emb< q) r
  emb¹¹⁰ : ∀ {A B C l l′ r1 r2 r3 p q r}
         → ShapeView₃ Γ l l′ (ι ⁰) A B C r1 r2 r3 p q r
         → ShapeView₃ Γ l l′ (ι ¹) A B C r1 r2 r3 p q (emb emb< r)
  emb¹∞∞ : ∀ {A B C l l′ r1 r2 r3 p q r}
         → ShapeView₃ Γ (ι ¹) l l′ A B C r1 r2 r3 p q r
         → ShapeView₃ Γ ∞ l l′ A B C r1 r2 r3 (emb ∞< p) q r
  emb∞¹∞ : ∀ {A B C l l′ r1 r2 r3  p q r}
         → ShapeView₃ Γ l (ι ¹) l′ A B C r1 r2 r3 p q r
         → ShapeView₃ Γ l ∞ l′ A B C r1 r2 r3 p (emb ∞< q) r
  emb∞∞¹ : ∀ {A B C l l′ r1 r2 r3 p q r}
         → ShapeView₃ Γ l l′ (ι ¹) A B C r1 r2 r3 p q r
         → ShapeView₃ Γ l l′ ∞ A B C r1 r2 r3 p q (emb ∞< r)

-- Combines two two-way views into a three-way view
combine : ∀ {Γ l l′ l″ l‴ A B C r1 r2 r2' r3 [A] [B] [B]′ [C]}
        → ShapeView Γ l l′ A B r1 r2 [A] [B]
        → ShapeView Γ l″ l‴ B C r2' r3 [B]′ [C]
        → ShapeView₃ Γ l l′ l‴ A B C r1 r2 r3 [A] [B] [C]
combine (Uᵥ UA UB) (Uᵥ UB' UC) = Uᵥ UA UB UC
combine (Uᵥ UA (Uᵣ r l′ l< PE.refl D)) (ℕᵥ ℕA ℕB) =
 ⊥-elim (U≢ℕ (whrDet* (red D ,  Uₙ) (red  ℕA , ℕₙ)))
combine (Uᵥ UA (Uᵣ r l′ l< PE.refl D)) (Emptyᵥ EmptyA EmptyB) =
 ⊥-elim (U≢Empty (whrDet* (red D ,  Uₙ) (red  EmptyA , Emptyₙ)))
combine (Uᵥ UA (Uᵣ r l′ l< PE.refl D)) (ne (ne K D' neK K≡K) neB) =
  ⊥-elim (U≢ne neK (whrDet* (red D ,  Uₙ) (red  D' , ne neK)))
combine (Uᵥ UA (Uᵣ r l′ l< PE.refl D)) (Πᵥ (Πᵣ rF lF lG _ _ F G D' ⊢F ⊢G A≡A [F] [G] G-ext) ΠB) =
 ⊥-elim (U≢Π (whrDet* (red D ,  Uₙ) (red  D' , Πₙ)))
combine (Uᵥ UA (Uᵣ r l′ l< PE.refl D)) (∃ᵥ (∃ᵣ F G D' ⊢F ⊢G A≡A [F] [G] G-ext) ∃B) =
 ⊥-elim (U≢∃ (whrDet* (red D ,  Uₙ) (red  D' , ∃ₙ)))
combine  (ℕᵥ ℕA ℕB) (Uᵥ (Uᵣ r l′ l< PE.refl D) UB) =
 ⊥-elim (U≢ℕ (whrDet* (red D ,  Uₙ) (red  ℕB , ℕₙ)))
combine  (ℕᵥ ℕA ℕB) (Emptyᵥ EmptyA EmptyB) =
   ⊥-elim (ℕ≢Empty (whrDet* (red ℕB , ℕₙ) (red EmptyA , Emptyₙ)))
combine  (ℕᵥ ℕA₁ ℕB₁) (ℕᵥ ℕA ℕB) = ℕᵥ ℕA₁ ℕB₁ ℕB
combine  (ℕᵥ ℕA ℕB) (ne (ne K D neK K≡K) neB) =
  ⊥-elim (ℕ≢ne neK (whrDet* (red ℕB , ℕₙ) (red D , ne neK)))
combine  (ℕᵥ ℕA ℕB) (Πᵥ (Πᵣ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ΠB) =
  ⊥-elim (ℕ≢Π (whrDet* (red ℕB , ℕₙ) (red D , Πₙ)))
combine  (ℕᵥ ℕA ℕB) (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ∃B) =
  ⊥-elim (ℕ≢∃ (whrDet* (red ℕB , ℕₙ) (red D , ∃ₙ)))
combine  (Emptyᵥ EmptyA EmptyB) (Uᵥ (Uᵣ r l′ l< PE.refl D) UB) =
 ⊥-elim (U≢Empty (whrDet* (red D ,  Uₙ) (red  EmptyB , Emptyₙ)))
combine  (Emptyᵥ EmptyA EmptyB) (ℕᵥ ℕA ℕB) =
   ⊥-elim (Empty≢ℕ (whrDet* (red EmptyB , Emptyₙ) (red ℕA , ℕₙ)))
combine  (Emptyᵥ EmptyA₁ EmptyB₁) (Emptyᵥ EmptyA EmptyB) = Emptyᵥ EmptyA₁ EmptyB₁ EmptyB
combine  (Emptyᵥ EmptyA EmptyB) (ne (ne K D neK K≡K) neB) =
   ⊥-elim (Empty≢ne neK (whrDet* (red EmptyB , Emptyₙ) (red D , ne neK)))
combine  (Emptyᵥ EmptyA EmptyB) (Πᵥ (Πᵣ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ΠB) =
   ⊥-elim (Empty≢Π (whrDet* (red EmptyB , Emptyₙ) (red D , Πₙ)))
combine  (Emptyᵥ EmptyA EmptyB) (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ∃B) =
   ⊥-elim (Empty≢∃ (whrDet* (red EmptyB , Emptyₙ) (red D , ∃ₙ)))
combine  (ne neA (ne K D' neK K≡K)) (Uᵥ (Uᵣ r l′ l< PE.refl D) UB) =
  ⊥-elim (U≢ne neK (whrDet* (red D ,  Uₙ) (red  D' , ne neK)))
combine  (ne neA (ne K D neK K≡K)) (ℕᵥ ℕA ℕB) =
  ⊥-elim (ℕ≢ne neK (whrDet* (red ℕA , ℕₙ) (red D , ne neK)))
combine  (ne neA (ne K D neK K≡K)) (Emptyᵥ EmptyA EmptyB) =
  ⊥-elim (Empty≢ne neK (whrDet* (red EmptyA , Emptyₙ) (red D , ne neK)))
combine  (ne neA₁ neB₁) (ne neA neB) = ne neA₁ neB₁ neB
combine  (ne neA (ne K D₁ neK K≡K)) (Πᵥ (Πᵣ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ΠB) =
  ⊥-elim (Π≢ne neK (whrDet* (red D , Πₙ) (red D₁ , ne neK)))
combine  (ne neA (ne K D₁ neK K≡K)) (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ∃B) =
  ⊥-elim (∃≢ne neK (whrDet* (red D , ∃ₙ) (red D₁ , ne neK)))
combine  (Πᵥ ΠA (Πᵣ rF lF lG _ _ F G D' ⊢F ⊢G A≡A [F] [G] G-ext)) (Uᵥ (Uᵣ r l′ l< PE.refl D) UB) =
 ⊥-elim (U≢Π (whrDet* (red D ,  Uₙ) (red  D' , Πₙ)))
combine  (Πᵥ ΠA (Πᵣ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (ℕᵥ ℕA ℕB) =
  ⊥-elim (ℕ≢Π (whrDet* (red ℕA , ℕₙ) (red D , Πₙ)))
combine  (Πᵥ ΠA (Πᵣ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (Emptyᵥ EmptyA EmptyB) =
  ⊥-elim (Empty≢Π (whrDet* (red EmptyA , Emptyₙ) (red D , Πₙ)))
combine  (Πᵥ ΠA (Πᵣ rF lF lG _ _ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext)) (ne (ne K D neK K≡K) neB) =
  ⊥-elim (Π≢ne neK (whrDet* (red D₁ , Πₙ) (red D , ne neK)))
combine  (Πᵥ ΠA₁ ΠB₁) (Πᵥ ΠA ΠB) = Πᵥ ΠA₁ ΠB₁ ΠB
combine  (Πᵥ ΠA (Πᵣ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext))
        (∃ᵥ (∃ᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁) ∃B) =
  ⊥-elim (Π≢∃ (whrDet* (red D , Πₙ) (red D₁ , ∃ₙ)))
combine  (∃ᵥ ∃A (∃ᵣ F G D' ⊢F ⊢G A≡A [F] [G] G-ext)) (Uᵥ (Uᵣ r l′ l< PE.refl D) UB) =
 ⊥-elim (U≢∃ (whrDet* (red D ,  Uₙ) (red  D' , ∃ₙ)))
combine  (∃ᵥ ∃A (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (ℕᵥ ℕA ℕB) =
  ⊥-elim (ℕ≢∃ (whrDet* (red ℕA , ℕₙ) (red D , ∃ₙ)))
combine  (∃ᵥ ∃A (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (Emptyᵥ EmptyA EmptyB) =
  ⊥-elim (Empty≢∃ (whrDet* (red EmptyA , Emptyₙ) (red D , ∃ₙ)))
combine  (∃ᵥ ∃A (∃ᵣ F G D₁ ⊢F ⊢G A≡A [F] [G] G-ext)) (ne (ne K D neK K≡K) neB) =
  ⊥-elim (∃≢ne neK (whrDet* (red D₁ , ∃ₙ) (red D , ne neK)))
combine  (∃ᵥ ΠA (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext))
        (Πᵥ (Πᵣ rF₁ lF₁ lG₁ _ _ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁) ∃B) =
  ⊥-elim (Π≢∃ (whrDet* (red D₁ , Πₙ) (red D , ∃ₙ)))
combine  (∃ᵥ ∃A ∃B) (∃ᵥ ∃A₁ ∃B₁) = ∃ᵥ ∃A ∃B ∃B₁
combine (emb⁰¹ [AB]) [BC] = emb⁰¹¹ (combine [AB] [BC])
combine (emb¹⁰ [AB]) [BC] = emb¹⁰¹ (combine [AB] [BC])
combine [AB] (emb⁰¹ [BC]) = combine [AB] [BC]
combine [AB] (emb¹⁰ [BC]) = emb¹¹⁰ (combine [AB] [BC])
combine (emb¹∞ [AB]) [BC] = emb¹∞∞ (combine [AB] [BC])
combine (emb∞¹ [AB]) [BC] = emb∞¹∞ (combine [AB] [BC])
combine [AB] (emb¹∞ [BC]) = combine [AB] [BC]
combine [AB] (emb∞¹ [BC]) = emb∞∞¹ (combine [AB] [BC])

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-

Smith Normal Form

Referrences:
  Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles,
  "Formalized linear algebra over Elementary Divisor Rings in Coq"
  (https://arxiv.org/abs/1601.07472)

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.IntegerMatrix.Smith where

open import Cubical.Algebra.IntegerMatrix.Smith.NormalForm public
open import Cubical.Algebra.IntegerMatrix.Smith.Normalization public using (smith)