text:
module BasicIS4.Metatheory.DyadicGentzenSpinalNormalForm-HereditarySubstitution where

open import BasicIS4.Syntax.DyadicGentzenSpinalNormalForm public

-- Hereditary substitution and reduction.

mutual
  [_≔_]ⁿᶠ_ : ∀ {A B Γ Δ} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ B → Γ ∖ i ⁏ Δ ⊢ⁿᶠ B
  [ i ≔ s ]ⁿᶠ neⁿᶠ (spⁿᵉ j  xs y) with i ≟∈ j
  [ i ≔ s ]ⁿᶠ neⁿᶠ (spⁿᵉ .i xs y) | same   = reduce s ([ i ≔ s ]ˢᵖ xs) ([ i ≔ s ]ᵗᵖ y)
  [ i ≔ s ]ⁿᶠ neⁿᶠ (spⁿᵉ ._ xs y) | diff j = neⁿᶠ (spⁿᵉ j ([ i ≔ s ]ˢᵖ xs) ([ i ≔ s ]ᵗᵖ y))
  [ i ≔ s ]ⁿᶠ neⁿᶠ (mspⁿᵉ j xs y) = neⁿᶠ (mspⁿᵉ j ([ i ≔ s ]ˢᵖ xs) ([ i ≔ s ]ᵗᵖ y))
  [ i ≔ s ]ⁿᶠ lamⁿᶠ t             = lamⁿᶠ ([ pop i ≔ mono⊢ⁿᶠ weak⊆ s ]ⁿᶠ t)
  [ i ≔ s ]ⁿᶠ boxⁿᶠ t             = boxⁿᶠ t
  [ i ≔ s ]ⁿᶠ pairⁿᶠ t u          = pairⁿᶠ ([ i ≔ s ]ⁿᶠ t) ([ i ≔ s ]ⁿᶠ u)
  [ i ≔ s ]ⁿᶠ unitⁿᶠ              = unitⁿᶠ

  [_≔_]ˢᵖ_ : ∀ {A B C Γ Δ} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ B ⦙ C → Γ ∖ i ⁏ Δ ⊢ˢᵖ B ⦙ C
  [ i ≔ s ]ˢᵖ nilˢᵖ      = nilˢᵖ
  [ i ≔ s ]ˢᵖ appˢᵖ xs u = appˢᵖ ([ i ≔ s ]ˢᵖ xs) ([ i ≔ s ]ⁿᶠ u)
  [ i ≔ s ]ˢᵖ fstˢᵖ xs   = fstˢᵖ ([ i ≔ s ]ˢᵖ xs)
  [ i ≔ s ]ˢᵖ sndˢᵖ xs   = sndˢᵖ ([ i ≔ s ]ˢᵖ xs)

  [_≔_]ᵗᵖ_ : ∀ {A B C Γ Δ} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ∖ i ⁏ Δ ⊢ᵗᵖ B ⦙ C
  [ i ≔ s ]ᵗᵖ nilᵗᵖ     = nilᵗᵖ
  [ i ≔ s ]ᵗᵖ unboxᵗᵖ u = unboxᵗᵖ u′
    where u′ = [ i ≔ mmono⊢ⁿᶠ weak⊆ s ]ⁿᶠ u

  m[_≔_]ⁿᶠ_ : ∀ {A B Γ Δ} → (i : A ∈ Δ) → ∅ ⁏ Δ ∖ i ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ B → Γ ⁏ Δ ∖ i ⊢ⁿᶠ B
  m[ i ≔ s ]ⁿᶠ neⁿᶠ (spⁿᵉ j xs y)   = neⁿᶠ (spⁿᵉ j (m[ i ≔ s ]ˢᵖ xs) (m[ i ≔ s ]ᵗᵖ y))
  m[ i ≔ s ]ⁿᶠ neⁿᶠ (mspⁿᵉ j xs y)  with i ≟∈ j
  m[ i ≔ s ]ⁿᶠ neⁿᶠ (mspⁿᵉ .i xs y) | same   = reduce (mono⊢ⁿᶠ bot⊆ s) (m[ i ≔ s ]ˢᵖ xs) (m[ i ≔ s ]ᵗᵖ y)
  m[ i ≔ s ]ⁿᶠ neⁿᶠ (mspⁿᵉ ._ xs y) | diff j = neⁿᶠ (mspⁿᵉ j (m[ i ≔ s ]ˢᵖ xs) (m[ i ≔ s ]ᵗᵖ y))
  m[ i ≔ s ]ⁿᶠ lamⁿᶠ t              = lamⁿᶠ (m[ i ≔ s ]ⁿᶠ t)
  m[ i ≔ s ]ⁿᶠ boxⁿᶠ t              = boxⁿᶠ (m[ i ≔ s ]ⁿᶠ t)
  m[ i ≔ s ]ⁿᶠ pairⁿᶠ t u           = pairⁿᶠ (m[ i ≔ s ]ⁿᶠ t) (m[ i ≔ s ]ⁿᶠ u)
  m[ i ≔ s ]ⁿᶠ unitⁿᶠ               = unitⁿᶠ

  m[_≔_]ˢᵖ_ : ∀ {A B C Γ Δ} → (i : A ∈ Δ) → ∅ ⁏ Δ ∖ i ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ B ⦙ C → Γ ⁏ Δ ∖ i ⊢ˢᵖ B ⦙ C
  m[ i ≔ s ]ˢᵖ nilˢᵖ      = nilˢᵖ
  m[ i ≔ s ]ˢᵖ appˢᵖ xs u = appˢᵖ (m[ i ≔ s ]ˢᵖ xs) (m[ i ≔ s ]ⁿᶠ u)
  m[ i ≔ s ]ˢᵖ fstˢᵖ xs   = fstˢᵖ (m[ i ≔ s ]ˢᵖ xs)
  m[ i ≔ s ]ˢᵖ sndˢᵖ xs   = sndˢᵖ (m[ i ≔ s ]ˢᵖ xs)

  m[_≔_]ᵗᵖ_ : ∀ {A B C Γ Δ} → (i : A ∈ Δ) → ∅ ⁏ Δ ∖ i ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → Γ ⁏ Δ ∖ i ⊢ᵗᵖ B ⦙ C
  m[ i ≔ s ]ᵗᵖ nilᵗᵖ     = nilᵗᵖ
  m[ i ≔ s ]ᵗᵖ unboxᵗᵖ u = unboxᵗᵖ u′
    where u′ = m[ pop i ≔ mmono⊢ⁿᶠ weak⊆ s ]ⁿᶠ u

  reduce : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ A ⦙ B → Γ ⁏ Δ ⊢ᵗᵖ B ⦙ C → {{_ : Tyⁿᵉ C}} → Γ ⁏ Δ ⊢ⁿᶠ C
  reduce t                               nilˢᵖ        nilᵗᵖ       = t
  reduce (neⁿᶠ (spⁿᵉ i xs nilᵗᵖ))        nilˢᵖ        y           = neⁿᶠ (spⁿᵉ i xs y)
  reduce (neⁿᶠ (spⁿᵉ i xs (unboxᵗᵖ u)))  nilˢᵖ        y           = neⁿᶠ (spⁿᵉ i xs (unboxᵗᵖ u′))
    where u′ = reduce u nilˢᵖ (mmono⊢ᵗᵖ weak⊆ y)
  reduce (neⁿᶠ (mspⁿᵉ i xs nilᵗᵖ))       nilˢᵖ        y           = neⁿᶠ (mspⁿᵉ i xs y)
  reduce (neⁿᶠ (mspⁿᵉ i xs (unboxᵗᵖ u))) nilˢᵖ        y           = neⁿᶠ (mspⁿᵉ i xs (unboxᵗᵖ u′))
    where u′ = reduce u nilˢᵖ (mmono⊢ᵗᵖ weak⊆ y)
  reduce (neⁿᶠ t {{()}})                 (appˢᵖ xs u) y
  reduce (neⁿᶠ t {{()}})                 (fstˢᵖ xs)   y
  reduce (neⁿᶠ t {{()}})                 (sndˢᵖ xs)   y
  reduce (lamⁿᶠ t)                       (appˢᵖ xs u) y           = reduce ([ top ≔ u ]ⁿᶠ t) xs y
  reduce (boxⁿᶠ t)                       nilˢᵖ        (unboxᵗᵖ u) = m[ top ≔ t ]ⁿᶠ u
  reduce (pairⁿᶠ t u)                    (fstˢᵖ xs)   y           = reduce t xs y
  reduce (pairⁿᶠ t u)                    (sndˢᵖ xs)   y           = reduce u xs y

-- Reduction-based normal forms.

appⁿᶠ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ⁿᶠ A ▻ B → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ B
appⁿᶠ (neⁿᶠ t {{()}})
appⁿᶠ (lamⁿᶠ t) u = [ top ≔ u ]ⁿᶠ t

fstⁿᶠ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ⁿᶠ A ∧ B → Γ ⁏ Δ ⊢ⁿᶠ A
fstⁿᶠ (neⁿᶠ t {{()}})
fstⁿᶠ (pairⁿᶠ t u) = t

sndⁿᶠ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ⁿᶠ A ∧ B → Γ ⁏ Δ ⊢ⁿᶠ B
sndⁿᶠ (neⁿᶠ t {{()}})
sndⁿᶠ (pairⁿᶠ t u) = u

-- Useful equipment for deriving neutrals.

≪appˢᵖ : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A ▻ B → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ˢᵖ C ⦙ B
≪appˢᵖ nilˢᵖ        t = appˢᵖ nilˢᵖ t
≪appˢᵖ (appˢᵖ xs u) t = appˢᵖ (≪appˢᵖ xs t) u
≪appˢᵖ (fstˢᵖ xs)   t = fstˢᵖ (≪appˢᵖ xs t)
≪appˢᵖ (sndˢᵖ xs)   t = sndˢᵖ (≪appˢᵖ xs t)

≪fstˢᵖ : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A ∧ B → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A
≪fstˢᵖ nilˢᵖ        = fstˢᵖ nilˢᵖ
≪fstˢᵖ (appˢᵖ xs u) = appˢᵖ (≪fstˢᵖ xs) u
≪fstˢᵖ (fstˢᵖ xs)   = fstˢᵖ (≪fstˢᵖ xs)
≪fstˢᵖ (sndˢᵖ xs)   = sndˢᵖ (≪fstˢᵖ xs)

≪sndˢᵖ : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ˢᵖ C ⦙ A ∧ B → Γ ⁏ Δ ⊢ˢᵖ C ⦙ B
≪sndˢᵖ nilˢᵖ        = sndˢᵖ nilˢᵖ
≪sndˢᵖ (appˢᵖ xs u) = appˢᵖ (≪sndˢᵖ xs) u
≪sndˢᵖ (fstˢᵖ xs)   = fstˢᵖ (≪sndˢᵖ xs)
≪sndˢᵖ (sndˢᵖ xs)   = sndˢᵖ (≪sndˢᵖ xs)

-- Derived neutrals.

varⁿᵉ : ∀ {A Γ Δ} → A ∈ Γ → Γ ⁏ Δ ⊢ⁿᵉ A
varⁿᵉ i = spⁿᵉ i nilˢᵖ nilᵗᵖ

appⁿᵉ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ A ▻ B → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᵉ B
appⁿᵉ (spⁿᵉ i xs nilᵗᵖ)        t = spⁿᵉ i (≪appˢᵖ xs t) nilᵗᵖ
appⁿᵉ (spⁿᵉ i xs (unboxᵗᵖ u))  t = spⁿᵉ i xs (unboxᵗᵖ u′)
  where u′ = appⁿᶠ u (mmono⊢ⁿᶠ weak⊆ t)
appⁿᵉ (mspⁿᵉ i xs nilᵗᵖ)       t = mspⁿᵉ i (≪appˢᵖ xs t) nilᵗᵖ
appⁿᵉ (mspⁿᵉ i xs (unboxᵗᵖ u)) t = mspⁿᵉ i xs (unboxᵗᵖ u′)
  where u′ = appⁿᶠ u (mmono⊢ⁿᶠ weak⊆ t)

mvarⁿᵉ : ∀ {A Γ Δ} → A ∈ Δ → Γ ⁏ Δ ⊢ⁿᵉ A
mvarⁿᵉ i = mspⁿᵉ i nilˢᵖ nilᵗᵖ

fstⁿᵉ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ A ∧ B → Γ ⁏ Δ ⊢ⁿᵉ A
fstⁿᵉ (spⁿᵉ i xs nilᵗᵖ)        = spⁿᵉ i (≪fstˢᵖ xs) nilᵗᵖ
fstⁿᵉ (spⁿᵉ i xs (unboxᵗᵖ u))  = spⁿᵉ i xs (unboxᵗᵖ (fstⁿᶠ u))
fstⁿᵉ (mspⁿᵉ i xs nilᵗᵖ)       = mspⁿᵉ i (≪fstˢᵖ xs) nilᵗᵖ
fstⁿᵉ (mspⁿᵉ i xs (unboxᵗᵖ u)) = mspⁿᵉ i xs (unboxᵗᵖ (fstⁿᶠ u))

sndⁿᵉ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ A ∧ B → Γ ⁏ Δ ⊢ⁿᵉ B
sndⁿᵉ (spⁿᵉ i xs nilᵗᵖ)        = spⁿᵉ i (≪sndˢᵖ xs) nilᵗᵖ
sndⁿᵉ (spⁿᵉ i xs (unboxᵗᵖ u))  = spⁿᵉ i xs (unboxᵗᵖ (sndⁿᶠ u))
sndⁿᵉ (mspⁿᵉ i xs nilᵗᵖ)       = mspⁿᵉ i (≪sndˢᵖ xs) nilᵗᵖ
sndⁿᵉ (mspⁿᵉ i xs (unboxᵗᵖ u)) = mspⁿᵉ i xs (unboxᵗᵖ (sndⁿᶠ u))

-- Iterated expansion.

expand : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ⁿᶠ A
expand {α P}   t = neⁿᶠ t {{α P}}
expand {A ▻ B} t = lamⁿᶠ (expand (appⁿᵉ (mono⊢ⁿᵉ weak⊆ t) (expand (varⁿᵉ top))))
expand {□ A}   t = neⁿᶠ t {{□ A}}
expand {A ∧ B} t = pairⁿᶠ (expand (fstⁿᵉ t)) (expand (sndⁿᵉ t))
expand {⊤}    t = unitⁿᶠ

-- Expansion-based normal forms.

varⁿᶠ : ∀ {A Γ Δ} → A ∈ Γ → Γ ⁏ Δ ⊢ⁿᶠ A
varⁿᶠ i = expand (varⁿᵉ i)

mvarⁿᶠ : ∀ {A Γ Δ} → A ∈ Δ → Γ ⁏ Δ ⊢ⁿᶠ A
mvarⁿᶠ i = expand (mvarⁿᵉ i)

mutual
  unboxⁿᶠ : ∀ {A C Γ Δ} → Γ ⁏ Δ ⊢ⁿᶠ □ A → Γ ⁏ Δ , A ⊢ⁿᶠ C → Γ ⁏ Δ ⊢ⁿᶠ C
  unboxⁿᶠ (neⁿᶠ t)  u = expand (unboxⁿᵉ t u)
  unboxⁿᶠ (boxⁿᶠ t) u = m[ top ≔ t ]ⁿᶠ u

  unboxⁿᵉ : ∀ {A C Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ □ A → Γ ⁏ Δ , A ⊢ⁿᶠ C → Γ ⁏ Δ ⊢ⁿᵉ C
  unboxⁿᵉ (spⁿᵉ i xs nilᵗᵖ)        u = spⁿᵉ i xs (unboxᵗᵖ u)
  unboxⁿᵉ (spⁿᵉ i xs (unboxᵗᵖ t))  u = spⁿᵉ i xs (unboxᵗᵖ u′)
    where u′ = unboxⁿᶠ t (mmono⊢ⁿᶠ (keep (weak⊆)) u)
  unboxⁿᵉ (mspⁿᵉ i xs nilᵗᵖ)       u = mspⁿᵉ i xs (unboxᵗᵖ u)
  unboxⁿᵉ (mspⁿᵉ i xs (unboxᵗᵖ t)) u = mspⁿᵉ i xs (unboxᵗᵖ u′)
    where u′ = unboxⁿᶠ t (mmono⊢ⁿᶠ (keep (weak⊆)) u)

-- Translation from terms to normal forms.

tm→nf : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ⁿᶠ A
tm→nf (var i)     = varⁿᶠ i
tm→nf (lam t)     = lamⁿᶠ (tm→nf t)
tm→nf (app t u)   = appⁿᶠ (tm→nf t) (tm→nf u)
tm→nf (mvar i)    = mvarⁿᶠ i
tm→nf (box t)     = boxⁿᶠ (tm→nf t)
tm→nf (unbox t u) = unboxⁿᶠ (tm→nf t) (tm→nf u)
tm→nf (pair t u)  = pairⁿᶠ (tm→nf t) (tm→nf u)
tm→nf (fst t)     = fstⁿᶠ (tm→nf t)
tm→nf (snd t)     = sndⁿᶠ (tm→nf t)
tm→nf unit        = unitⁿᶠ

-- Normalisation by hereditary substitution.

norm : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A
norm = nf→tm ∘ tm→nf

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


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

open import Base
open import Algebra.Groups

{-
    The definition of G-sets.  Thanks to Daniel Grayson.
-}

module Algebra.GroupSets {i} (grp : group i) where

  private
    module G = group grp

  -- The right group action with respect to the group [grp].
  -- [Y] should be some set, but that condition is not needed
  -- in the definition.
  record action (Y : Set i) : Set i where
    constructor act[_,_,_]
    field
      _∙_ : Y → G.carrier → Y
      right-unit : ∀ y → y ∙ G.e ≡ y
      assoc : ∀ y p₁ p₂ → (y ∙ p₁) ∙ p₂ ≡ y ∙ (p₁ G.∙ p₂)

  {-
  action-eq : ∀ {Y} ⦃ _ : is-set Y ⦄ {act₁ act₂ : action Y}
    → action._∙_ act₁ ≡ action._∙_ act₂ → act₁ ≡ act₂
  action-eq ∙≡ =
  -}

  -- The definition of a G-set.  A set [carrier] equipped with
  -- a right group action with respect to [grp].
  record gset : Set (suc i) where
    constructor gset[_,_,_]
    field
      carrier : Set i
      act : action carrier
      set : is-set carrier
    open action act public

  -- A convenient tool to compare two G-sets.  Many data are
  -- just props and this function do the coversion for them
  -- for you.  You only need to show the non-trivial parts.
  gset-eq : ∀ {gs₁ gs₂ : gset} (carrier≡ : gset.carrier gs₁ ≡ gset.carrier gs₂)
    → (∙≡ : transport (λ Y → Y → G.carrier → Y) carrier≡ (action._∙_ (gset.act gs₁))
          ≡ action._∙_ (gset.act gs₂))
    → gs₁ ≡ gs₂
  gset-eq
    {gset[  Y , act[  ∙ , unit₁ , assoc₁ ] , set₁ ]}
    {gset[ ._ , act[ ._ , unit₂ , assoc₂ ] , set₂ ]}
    refl refl =
      gset[ Y , act[ ∙ , unit₁ , assoc₁ ] , set₁ ]
        ≡⟨ ap (λ unit → gset[ Y , act[ ∙ , unit , assoc₁ ] , set₁ ])
              $ prop-has-all-paths (Π-is-prop λ _ → set₁ _ _) _ _ ⟩
      gset[ Y , act[ ∙ , unit₂ , assoc₁ ] , set₁ ]
        ≡⟨ ap (λ assoc → gset[ Y , act[ ∙ , unit₂ , assoc ] , set₁ ])
              $ prop-has-all-paths (Π-is-prop λ _ → Π-is-prop λ _ → Π-is-prop λ _ → set₁ _ _) _ _ ⟩
      gset[ Y , act[ ∙ , unit₂ , assoc₂ ] , set₁ ]
        ≡⟨ ap (λ set → gset[ Y , act[ ∙ , unit₂ , assoc₂ ] , set ])
              $ prop-has-all-paths is-set-is-prop _ _ ⟩∎
      gset[ Y , act[ ∙ , unit₂ , assoc₂ ] , set₂ ]
        ∎

ext: agda

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
------------------------------------------------------------------------------
-- Proving properties without using pattern matching on refl
------------------------------------------------------------------------------

{-# OPTIONS --no-pattern-matching #-}
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}

module FOT.GroupTheory.NoPatternMatchingOnRefl where

open import GroupTheory.Base

------------------------------------------------------------------------------
-- From GroupTheory.PropertiesI

-- Congruence properties

-- The propositional equality is compatible with the binary operation.

·-leftCong : ∀ {a b c} → a ≡ b → a · c ≡ b · c
·-leftCong {a} {c = c} h = subst (λ t → a · c ≡ t · c) h refl

·-rightCong : ∀ {a b c} → b ≡ c → a · b ≡ a · c
·-rightCong {a} {b} h = subst (λ t → a · b ≡ a · t) h refl

-- The propositional equality is compatible with the inverse function.
⁻¹-cong : ∀ {a b} → a ≡ b → a ⁻¹ ≡ b ⁻¹
⁻¹-cong {a} h = subst (λ t → a ⁻¹ ≡ t ⁻¹) h refl

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --rewriting #-}
module Duality where

open import Data.Bool

open import Data.Nat hiding (compare)
open import Data.Nat.Properties
open import Data.Fin hiding (_+_)
open import Data.Product

open import Function

open import Relation.Binary.PropositionalEquality hiding (Extensionality)

open import Agda.Builtin.Equality.Rewrite

-- variables

variable
  n m : ℕ

open import Types.Direction

open import Auxiliary.Extensionality
open import Auxiliary.RewriteLemmas

----------------------------------------------------------------------
-- session types coinductively

import Types.COI as COI

----------------------------------------------------------------------
-- session type inductively with explicit rec

import Types.IND as IND

----------------------------------------------------------------------
-- provide an embedding of IND to COI

open COI
open IND hiding (_≈_ ; _≈'_ ; ≈-refl ; ≈'-refl ; ≈ᵗ-refl)

ind2coiT : IND.Type 0 → COI.Type
ind2coiS : IND.SType 0 → COI.SType
ind2coiG : IND.GType 0 → COI.STypeF COI.SType

ind2coiT TUnit = TUnit
ind2coiT TInt = TInt
ind2coiT (TPair it it₁) = TPair (ind2coiT it) (ind2coiT it₁)
ind2coiT (TChan st) = TChan (ind2coiS st)

ind2coiG (transmit d t ist) = transmit d (ind2coiT t) (ind2coiS ist)
ind2coiG (choice d m alt) = choice d m (ind2coiS ∘ alt)
ind2coiG end = end

SType.force (ind2coiS (gdd gst)) = ind2coiG gst
SType.force (ind2coiS (rec gst)) = ind2coiG (st-substG gst zero (rec gst))

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

{-# TERMINATING #-}
subst-weakenS : (s : IND.SType (suc n)) (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (s0 : IND.SType 0)
  → st-substS (weaken1'S (inject₁ j) s) (suc i) s0 ≡ weaken1'S j (st-substS s i s0)
subst-weakenG : (g : IND.GType (suc n)) (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (s0 : IND.SType 0)
  → st-substG (weaken1'G (inject₁ j) g) (suc i) s0 ≡ weaken1'G j (st-substG g i s0)
subst-weakenT : (t : IND.Type (suc n)) (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (s0 : IND.SType 0)
  → st-substT (weaken1'T (inject₁ j) t) (suc i) s0 ≡ weaken1'T j (st-substT t i s0)

subst-weakenS (gdd gst) i j le s0 = cong gdd (subst-weakenG gst i j le s0)
subst-weakenS (rec gst) i j le s0 = cong rec (subst-weakenG gst (suc i) (suc j) (s≤s le) s0)
subst-weakenS (var p x) zero zero le s0 = refl
subst-weakenS {suc n} (var p x) (suc i) zero le s0 = refl
subst-weakenS {suc n} (var p zero) (suc i) (suc j) le s0 = refl
subst-weakenS {suc n} (var p (suc x)) (suc i) (suc j) (s≤s le) s0 rewrite (weak-weakS j zero z≤n (st-substS (var p x) i s0))
  = cong (weaken1'S zero) (subst-weakenS (var p x) i j le s0)

subst-weakenG (transmit d t s) i j le s0 = cong₂ (transmit d) (subst-weakenT t i j le s0) (subst-weakenS s i j le s0)
subst-weakenG (choice d m alt) i j le s0 = cong (choice d m) (ext (λ m' → subst-weakenS (alt m') i j le s0 ))
subst-weakenG end i j le s0 = refl

subst-weakenT TUnit i j le s0 = refl
subst-weakenT TInt i j le s0 = refl
subst-weakenT (TPair t t₁) i j le s0 = cong₂ TPair (subst-weakenT t i j le s0) (subst-weakenT t₁ i j le s0)
subst-weakenT (TChan s) i j le s0 = cong TChan (subst-weakenS s i j le s0)

{-# TERMINATING #-}
subst-swap-dualT : ∀ {ist} → (t : IND.Type (suc n)) (i : Fin (suc n)) →
  st-substT t i ist ≡ st-substT (swap-polT i t) i (IND.dualS ist)
subst-swap-dualS : ∀ {ist} → (st : IND.SType (suc n)) (i : Fin (suc n)) →
  st-substS st i ist ≡ st-substS (swap-polS i st) i (IND.dualS ist)
subst-swap-dualG : ∀ {ist} → (gst : IND.GType (suc n)) (i : Fin (suc n)) →
  st-substG gst i ist ≡ st-substG (swap-polG i gst) i (IND.dualS ist)

subst-swap-dualT TUnit i = refl
subst-swap-dualT TInt i = refl
subst-swap-dualT (TPair ty ty₁) i = cong₂ TPair (subst-swap-dualT ty i) (subst-swap-dualT ty₁ i)
subst-swap-dualT (TChan x) i = cong TChan (subst-swap-dualS x i)

subst-swap-dualS (gdd gst) i = cong gdd (subst-swap-dualG gst i)
subst-swap-dualS (rec gst) i = cong rec (subst-swap-dualG gst (suc i))
subst-swap-dualS {n} {ist} (var p zero) zero = cong (weakenS n) (dual-if-dual p ist)
subst-swap-dualS {suc n} (var p zero) (suc i) = refl
subst-swap-dualS {suc n} (var p (suc x)) zero = refl
subst-swap-dualS {suc n}{ist} (var p (suc x)) (suc i)
  rewrite subst-weakenS (swap-polS i (var p x)) i zero z≤n (dualS ist)
  = cong (weaken1'S zero) (subst-swap-dualS ((var p x)) i)

subst-swap-dualG (transmit d t s) i = cong₂ (transmit d) (subst-swap-dualT t i) (subst-swap-dualS s i)
subst-swap-dualG (choice d m alt) i = cong (choice d m) (ext (λ x → subst-swap-dualS (alt x) i))
subst-swap-dualG end i = refl

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

swap-i-weakenS : (i : Fin (suc n)) (s : IND.SType n) → swap-polS i (weaken1'S i s) ≡ weaken1'S i s
swap-i-weakenG : (i : Fin (suc n)) (g : IND.GType n) → swap-polG i (weaken1'G i g) ≡ weaken1'G i g
swap-i-weakenT : (i : Fin (suc n)) (t : IND.TType n) → swap-polT i (weaken1'T i t) ≡ weaken1'T i t

swap-i-weakenS i (gdd gst) = cong gdd (swap-i-weakenG i gst)
swap-i-weakenS i (rec gst) = cong rec (swap-i-weakenG (suc i) gst)
swap-i-weakenS zero (var p zero) = refl
swap-i-weakenS (suc i) (var p zero) = refl
swap-i-weakenS zero (var p (suc x)) = refl
swap-i-weakenS (suc i) (var p (suc x)) = cong weaken1S (swap-i-weakenS i (var p x))

swap-i-weakenG i (transmit d t s) = cong₂ (transmit d) (swap-i-weakenT i t) (swap-i-weakenS i s)
swap-i-weakenG i (choice d m alt) = cong (choice d m) (ext (swap-i-weakenS i ∘ alt))
swap-i-weakenG i end = refl

swap-i-weakenT i TUnit = refl
swap-i-weakenT i TInt = refl
swap-i-weakenT i (TPair t₁ t₂) = cong₂ TPair (swap-i-weakenT i t₁) (swap-i-weakenT i t₂)
swap-i-weakenT i (TChan x) = cong TChan (swap-i-weakenS i x)

{-# TERMINATING #-}
subst-swapG : (ist : IND.SType 0) (i : Fin (suc (suc n))) (j : Fin′ i) (g : GType (suc (suc n))) →
  st-substG (swap-polG (inject j) g) i ist ≡ swap-polG (inject! j) (st-substG g i ist)
subst-swapS : (ist : IND.SType 0) (i : Fin (suc (suc n))) (j : Fin′ i) (s : IND.SType (suc (suc n))) →
  st-substS (swap-polS (inject j) s) i ist ≡ swap-polS (inject! j) (st-substS s i ist)
subst-swapT : (ist : IND.SType 0) (i : Fin (suc (suc n))) (j : Fin′ i) (g : IND.Type (suc (suc n))) →
  st-substT (swap-polT (inject j) g) i ist ≡ swap-polT (inject! j) (st-substT g i ist)

subst-swapG ist i j (transmit d t s) = cong₂ (transmit d) (subst-swapT ist i j t) (subst-swapS ist i j s)
subst-swapG ist i j (choice d m alt) = cong (choice d m) (ext (λ x → subst-swapS ist i j (alt x)))
subst-swapG ist i j end = refl

subst-swapS ist i j (gdd gst) = cong gdd (subst-swapG ist i j gst)
subst-swapS ist i j (rec gst) = cong rec (subst-swapG ist (suc i) (suc j) gst)
subst-swapS{zero} ist zero () (var p zero)
subst-swapS {zero} ist (suc zero) zero (var p zero) = refl
subst-swapS {zero} ist (suc zero) zero (var p (suc x))
  rewrite swap-i-weakenS zero (st-substS (var p x) zero ist) = refl
subst-swapS{suc n} ist (suc i) zero (var p zero) = refl
subst-swapS{suc n} ist (suc i) (suc j) (var p zero) = refl
subst-swapS{suc n} ist zero () (var p (suc x))
subst-swapS{suc n} ist (suc i) zero (var p (suc x))
  rewrite swap-i-weakenS zero (st-substS (var p x) i ist) = refl
subst-swapS{suc n} ist (suc i) (suc j) (var p (suc x))
  rewrite subst-weakenS (swap-polS (inject j) (var p x)) i zero z≤n ist
  | swap-weakenS (inject! j) (st-substS (var p x) i ist)
  = cong weaken1S (subst-swapS ist i j (var p x))

subst-swapT ist i j TUnit = refl
subst-swapT ist i j TInt = refl
subst-swapT ist i j (TPair t t₁) = cong₂ TPair (subst-swapT ist i j t) (subst-swapT ist i j t₁)
subst-swapT ist i j (TChan x) = cong TChan (subst-swapS ist i j x)

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

dual-recT' : (t : TType (suc n)) (i : Fin (suc n)) (ist : IND.SType 0)
  → st-substT (swap-polT i t) i (dualS ist) ≡ st-substT t i ist
dual-recG' : (g : GType (suc n)) (i : Fin (suc n)) (ist : IND.SType 0)
  → st-substG (swap-polG i g) i (dualS ist) ≡ st-substG g i ist
dual-recS' : (s : IND.SType (suc n)) (i : Fin (suc n)) (ist : IND.SType 0)
  → st-substS (swap-polS i s) i (dualS ist) ≡ st-substS s i ist

dual-recT' TUnit i ist = refl
dual-recT' TInt i ist = refl
dual-recT' (TPair t t₁) i ist = cong₂ TPair (dual-recT' t i ist) (dual-recT' t₁ i ist)
dual-recT' (TChan s) i ist = cong TChan (dual-recS' s i ist)

dual-recG' (transmit d t s) i ist = cong₂ (transmit d) (dual-recT' t i ist) (dual-recS' s i ist)
dual-recG' (choice d m alt) i ist = cong (choice d m) (ext (λ m' → dual-recS' (alt m') i ist))
dual-recG' end i ist = refl

dual-recS' (gdd gst) i ist = cong gdd (dual-recG' gst i ist)
dual-recS' (rec gst) i ist = cong rec (dual-recG' gst (suc i) ist)
dual-recS' (var p zero) zero ist rewrite (dual-if-dual p ist) = refl
dual-recS' (var p (suc x)) zero ist = trivial-subst-var p x (dualS ist) (ist)
dual-recS' (var p zero) (suc i) ist = trivial-subst-var' p i (dualS ist) (ist)
dual-recS' (var p (suc x)) (suc i) ist rewrite (subst-swap-dualS{ist = ist} (var p (suc x)) (suc i))
  = refl

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

-- show that the dualS function is compatible with unfolding
-- that is
-- COI.dual ∘ ind2coi ≈ ind2coi ∘ IND.dual

{-# TERMINATING #-}
dual-lemmaS : (s : IND.SType (suc n)) (j : Fin (suc n)) (s0 : IND.SType 0)
  → st-substS (dualS s) j s0 ≡ dualS (st-substS s j s0)
dual-lemmaG : (g : IND.GType (suc n)) (j : Fin (suc n)) (s0 : IND.SType 0)
  → st-substG (dualG g) j s0 ≡ dualG (st-substG g j s0)

dual-lemmaS (gdd gst) j s0 = cong gdd (dual-lemmaG gst j s0)
dual-lemmaS (rec gst) j s0 rewrite (subst-swapG s0 (suc j) zero (dualG gst)) =
  let rst = dual-lemmaG gst (suc j) s0 in cong rec (cong (swap-polG zero) rst)
dual-lemmaS {n} (var POS zero) zero s0          = sym (dual-weakenS' n s0)
dual-lemmaS {n} (var NEG zero) zero s0 rewrite (sym (dual-weakenS' n s0)) | (sym (dual-invS (weakenS n s0))) = refl
dual-lemmaS {suc n} (var POS zero) (suc j) s0 = refl
dual-lemmaS {suc n} (var NEG zero) (suc j) s0 = refl
dual-lemmaS {suc n} (var POS (suc x)) zero s0 = refl
dual-lemmaS {suc n} (var NEG (suc x)) zero s0 = refl
dual-lemmaS {suc n} (var POS (suc x)) (suc j) s0 rewrite (dual-weakenS zero (st-substS (var POS x) j s0)) = cong (weaken1'S zero) (dual-lemmaS (var POS x) j s0)
dual-lemmaS {suc n} (var NEG (suc x)) (suc j) s0 rewrite (dual-weakenS zero (st-substS (var NEG x) j s0)) = cong (weaken1'S zero) (dual-lemmaS (var NEG x) j s0)

dual-lemmaG (transmit d t s) j s0 = cong₂ (transmit (dual-dir d)) refl (dual-lemmaS s j s0)
dual-lemmaG (choice d m alt) j s0 = cong (choice (dual-dir d) m) (ext (λ m' → dual-lemmaS (alt m') j s0))
dual-lemmaG end j s0 = refl

----------------------------------------------------------------------
-- main result
dual-compatibleS : (ist : IND.SType 0) →
  COI.dual (ind2coiS ist) ≈ ind2coiS (IND.dualS ist)
dual-compatibleG : (gst : IND.GType 0) →
  COI.dualF (ind2coiG gst) ≈' ind2coiG (IND.dualG gst)

Equiv.force (dual-compatibleS (gdd gst)) = dual-compatibleG gst
Equiv.force (dual-compatibleS (rec gst))
  rewrite (dual-recG' (dualG gst) zero (rec gst))
          | dual-lemmaG gst zero (rec gst) = dual-compatibleG (st-substG gst zero (rec gst))

dual-compatibleG (transmit d t s) = eq-transmit (dual-dir d) ≈ᵗ-refl (dual-compatibleS s)
dual-compatibleG (choice d m alt) = eq-choice (dual-dir d) (dual-compatibleS ∘ alt)
dual-compatibleG end = eq-end

max_stars_repo_name: peterthiemann/dual-session

max_issues_repo_name: peterthiemann/dual-session

max_forks_repo_name: peterthiemann/dual-session


text:
open import Type

module Graph.Oper {ℓ₁ ℓ₂} {V : Type{ℓ₁}} where

open import Logic.Propositional
open import Graph{ℓ₁}{ℓ₂}(V)

_∪_ : Graph → Graph → Graph
(g₁ ∪ g₂) v₁ v₂ = g₁ v₁ v₂ ∨ g₂ v₁ v₂ -- TODO: lift1On2

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Eval where

open import Data.Empty
open import Data.Unit
open import Data.Unit.Core
open import Data.Nat renaming (_⊔_ to _⊔ℕ_)
open import Data.Sum renaming (map to _⊎→_)
open import Data.Product renaming (map to _×→_)
open import Data.Vec
open import Relation.Binary.PropositionalEquality

open import FT -- Finite Types

_∘_ = trans

mutual
  evalComb : {a b : FT} → a ⇛ b → ⟦ a ⟧ → ⟦ b ⟧
  evalComb unite₊⇛ (inj₁ ())
  evalComb unite₊⇛ (inj₂ y) = y
  evalComb uniti₊⇛ v = inj₂ v
  evalComb swap₊⇛ (inj₁ x) = inj₂ x
  evalComb swap₊⇛ (inj₂ y) = inj₁ y
  evalComb assocl₊⇛ (inj₁ x) = inj₁ (inj₁ x)
  evalComb assocl₊⇛ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
  evalComb assocl₊⇛ (inj₂ (inj₂ y)) = inj₂ y
  evalComb assocr₊⇛ (inj₁ (inj₁ x)) = inj₁ x
  evalComb assocr₊⇛ (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
  evalComb assocr₊⇛ (inj₂ y) = inj₂ (inj₂ y)
  evalComb unite⋆⇛ (tt , proj₂) = proj₂
  evalComb uniti⋆⇛ v = tt , v
  evalComb swap⋆⇛ (proj₁ , proj₂) = proj₂ , proj₁
  evalComb assocl⋆⇛ (proj₁ , proj₂ , proj₃) = (proj₁ , proj₂) , proj₃
  evalComb assocr⋆⇛ ((proj₁ , proj₂) , proj₃) = proj₁ , proj₂ , proj₃
  evalComb distz⇛ (() , proj₂)
  evalComb factorz⇛ ()
  evalComb dist⇛ (inj₁ x , proj₂) = inj₁ (x , proj₂)
  evalComb dist⇛ (inj₂ y , proj₂) = inj₂ (y , proj₂)
  evalComb factor⇛ (inj₁ (proj₁ , proj₂)) = inj₁ proj₁ , proj₂
  evalComb factor⇛ (inj₂ (proj₁ , proj₂)) = inj₂ proj₁ , proj₂
  evalComb id⇛ v = v
  evalComb (sym⇛ c) v = evalBComb c v
  evalComb (c₁ ◎ c₂) v = evalComb c₂ (evalComb c₁ v)
  evalComb (c ⊕ c₁) (inj₁ x) = inj₁ (evalComb c x)
  evalComb (c ⊕ c₁) (inj₂ y) = inj₂ (evalComb c₁ y)
  evalComb (c ⊗ c₁) (proj₁ , proj₂) = evalComb c proj₁ , evalComb c₁ proj₂

  evalBComb : {a b : FT} → a ⇛ b → ⟦ b ⟧ → ⟦ a ⟧
  evalBComb unite₊⇛ v = inj₂ v
  evalBComb uniti₊⇛ (inj₁ ())
  evalBComb uniti₊⇛ (inj₂ y) = y
  evalBComb swap₊⇛ (inj₁ x) = inj₂ x
  evalBComb swap₊⇛ (inj₂ y) = inj₁ y
  evalBComb assocl₊⇛ (inj₁ (inj₁ x)) = inj₁ x
  evalBComb assocl₊⇛ (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
  evalBComb assocl₊⇛ (inj₂ y) = inj₂ (inj₂ y)
  evalBComb assocr₊⇛ (inj₁ x) = inj₁ (inj₁ x)
  evalBComb assocr₊⇛ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
  evalBComb assocr₊⇛ (inj₂ (inj₂ y)) = inj₂ y
  evalBComb unite⋆⇛ x = tt , x
  evalBComb uniti⋆⇛ (tt , x) = x
  evalBComb swap⋆⇛ (x , y) = y , x
  evalBComb assocl⋆⇛ ((x , y) , z) = x , y , z
  evalBComb assocr⋆⇛ (x , y , z) = (x , y) , z
  evalBComb distz⇛ ()
  evalBComb factorz⇛ (() , _)
  evalBComb dist⇛ (inj₁ (proj₁ , proj₂)) = inj₁ proj₁ , proj₂
  evalBComb dist⇛ (inj₂ (proj₁ , proj₂)) = inj₂ proj₁ , proj₂
  evalBComb factor⇛ (inj₁ x , proj₂) = inj₁ (x , proj₂)
  evalBComb factor⇛ (inj₂ y , proj₂) = inj₂ (y , proj₂)
  evalBComb id⇛ x = x
  evalBComb (sym⇛ c) x = evalComb c x
  evalBComb (c ◎ c₁) x = evalBComb c (evalBComb c₁ x)
  evalBComb (c ⊕ c₁) (inj₁ x) = inj₁ (evalBComb c x)
  evalBComb (c ⊕ c₁) (inj₂ y) = inj₂ (evalBComb c₁ y)
  evalBComb (c ⊗ c₁) (proj₁ , proj₂) = evalBComb c proj₁ , evalBComb c₁ proj₂

mutual
  Comb∘BComb : {a b : FT} → (c : a ⇛ b) → ∀ x → evalBComb c (evalComb c x) ≡ x
  Comb∘BComb unite₊⇛ (inj₁ ())
  Comb∘BComb unite₊⇛ (inj₂ y) = refl
  Comb∘BComb uniti₊⇛ x = refl
  Comb∘BComb swap₊⇛ (inj₁ x) = refl
  Comb∘BComb swap₊⇛ (inj₂ y) = refl
  Comb∘BComb assocl₊⇛ (inj₁ x) = refl
  Comb∘BComb assocl₊⇛ (inj₂ (inj₁ x)) = refl
  Comb∘BComb assocl₊⇛ (inj₂ (inj₂ y)) = refl
  Comb∘BComb assocr₊⇛ (inj₁ (inj₁ x)) = refl
  Comb∘BComb assocr₊⇛ (inj₁ (inj₂ y)) = refl
  Comb∘BComb assocr₊⇛ (inj₂ y) = refl
  Comb∘BComb unite⋆⇛ (tt , y) = refl
  Comb∘BComb uniti⋆⇛ x = refl
  Comb∘BComb swap⋆⇛ (x , y) = refl
  Comb∘BComb assocl⋆⇛ (x , y , z) = refl
  Comb∘BComb assocr⋆⇛ ((x , y) , z) = refl
  Comb∘BComb distz⇛ (() , _)
  Comb∘BComb factorz⇛ ()
  Comb∘BComb dist⇛ (inj₁ x , y) = refl
  Comb∘BComb dist⇛ (inj₂ x , y) = refl
  Comb∘BComb factor⇛ (inj₁ (x , y)) = refl
  Comb∘BComb factor⇛ (inj₂ (x , y)) = refl
  Comb∘BComb id⇛ x = refl
  Comb∘BComb (sym⇛ c) x = BComb∘Comb c x
  Comb∘BComb (c₀ ◎ c₁) x =
    cong (evalBComb c₀)  (Comb∘BComb c₁ (evalComb c₀ x)) ∘ Comb∘BComb c₀ x
  Comb∘BComb (c₀ ⊕ c₁) (inj₁ x) = cong inj₁ (Comb∘BComb c₀ x)
  Comb∘BComb (c₀ ⊕ c₁) (inj₂ y) = cong inj₂ (Comb∘BComb c₁ y)
  Comb∘BComb (c₀ ⊗ c₁) (x , y) = cong₂ _,_ (Comb∘BComb c₀ x) (Comb∘BComb c₁ y)

  BComb∘Comb : {a b : FT} → (c : a ⇛ b) → ∀ x → evalComb c (evalBComb c x) ≡ x
  BComb∘Comb unite₊⇛ x = refl
  BComb∘Comb uniti₊⇛ (inj₁ ())
  BComb∘Comb uniti₊⇛ (inj₂ y) = refl
  BComb∘Comb swap₊⇛ (inj₁ x) = refl
  BComb∘Comb swap₊⇛ (inj₂ y) = refl
  BComb∘Comb assocl₊⇛ (inj₁ (inj₁ x)) = refl
  BComb∘Comb assocl₊⇛ (inj₁ (inj₂ y)) = refl
  BComb∘Comb assocl₊⇛ (inj₂ y) = refl
  BComb∘Comb assocr₊⇛ (inj₁ x) = refl
  BComb∘Comb assocr₊⇛ (inj₂ (inj₁ x)) = refl
  BComb∘Comb assocr₊⇛ (inj₂ (inj₂ y)) = refl
  BComb∘Comb unite⋆⇛ x = refl
  BComb∘Comb uniti⋆⇛ (tt , proj₂) = refl
  BComb∘Comb swap⋆⇛ (proj₁ , proj₂) = refl
  BComb∘Comb assocl⋆⇛ ((proj₁ , proj₂) , proj₃) = refl
  BComb∘Comb assocr⋆⇛ (proj₁ , proj₂ , proj₃) = refl
  BComb∘Comb distz⇛ ()
  BComb∘Comb factorz⇛ (() , _)
  BComb∘Comb dist⇛ (inj₁ (proj₁ , proj₂)) = refl
  BComb∘Comb dist⇛ (inj₂ (proj₁ , proj₂)) = refl
  BComb∘Comb factor⇛ (inj₁ x , proj₂) = refl
  BComb∘Comb factor⇛ (inj₂ y , proj₂) = refl
  BComb∘Comb id⇛ x = refl
  BComb∘Comb (sym⇛ c) x = Comb∘BComb c x
  BComb∘Comb (c₀ ◎ c₁) x =
    cong (evalComb c₁) (BComb∘Comb c₀ (evalBComb c₁ x)) ∘ BComb∘Comb c₁ x
  BComb∘Comb (c ⊕ c₁) (inj₁ x) = cong inj₁ (BComb∘Comb c x)
  BComb∘Comb (c ⊕ c₁) (inj₂ y) = cong inj₂ (BComb∘Comb c₁ y)
  BComb∘Comb (c ⊗ c₁) (x , y) = cong₂ _,_ (BComb∘Comb c x) (BComb∘Comb c₁ y)

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

-- evaluate the alternative interpretation; A needs to be a pointed type.
mutual
  evalComb′ : {a b : FT} {A : Set} {pt : A} → a ⇛ b → ⟦ a ⟧′ A → ⟦ b ⟧′ A
  evalComb′ unite₊⇛ (inj₁ ())
  evalComb′ unite₊⇛ (inj₂ y) = y
  evalComb′ uniti₊⇛ x = inj₂ x
  evalComb′ swap₊⇛ (inj₁ x) = inj₂ x
  evalComb′ swap₊⇛ (inj₂ y) = inj₁ y
  evalComb′ assocl₊⇛ (inj₁ x) = inj₁ (inj₁ x)
  evalComb′ assocl₊⇛ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
  evalComb′ assocl₊⇛ (inj₂ (inj₂ y)) = inj₂ y
  evalComb′ assocr₊⇛ (inj₁ (inj₁ x)) = inj₁ x
  evalComb′ assocr₊⇛ (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
  evalComb′ assocr₊⇛ (inj₂ y) = inj₂ (inj₂ y)
  evalComb′ unite⋆⇛ (_ , x) = x
  evalComb′ {pt = a} uniti⋆⇛ x = a , x
  evalComb′ swap⋆⇛ (x , y) = y , x
  evalComb′ assocl⋆⇛ (x , y , z) = (x , y) , z
  evalComb′ assocr⋆⇛ ((x , y) , z) = x , y , z
  evalComb′ distz⇛ (() , _)
  evalComb′ factorz⇛ ()
  evalComb′ dist⇛ (inj₁ x , z) = inj₁ (x , z)
  evalComb′ dist⇛ (inj₂ y , z) = inj₂ (y , z)
  evalComb′ factor⇛ (inj₁ (x , y)) = inj₁ x , y
  evalComb′ factor⇛ (inj₂ (x , y)) = inj₂ x , y
  evalComb′ id⇛ x = x
  evalComb′ {pt = a} (sym⇛ c) x = evalBComb′ {pt = a} c x
  evalComb′ {pt = a} (c₀ ◎ c₁) x = evalComb′ {pt = a} c₁ (evalComb′ {pt = a} c₀ x)
  evalComb′ {pt = a} (c₀ ⊕ c₁) (inj₁ x) = inj₁ (evalComb′ {pt = a} c₀ x)
  evalComb′ {pt = a} (c₀ ⊕ c₁) (inj₂ y) = inj₂ (evalComb′ {pt = a} c₁ y)
  evalComb′ {pt = a} (c₀ ⊗ c₁) (x , y) = evalComb′ {pt = a} c₀ x , evalComb′ {pt = a} c₁ y

  evalBComb′ : {a b : FT} {A : Set} {pt : A} → a ⇛ b → ⟦ b ⟧′ A → ⟦ a ⟧′ A
  evalBComb′ unite₊⇛ x = inj₂ x
  evalBComb′ uniti₊⇛ (inj₁ ())
  evalBComb′ uniti₊⇛ (inj₂ y) = y
  evalBComb′ swap₊⇛ (inj₁ x) = inj₂ x
  evalBComb′ swap₊⇛ (inj₂ y) = inj₁ y
  evalBComb′ assocl₊⇛ (inj₁ (inj₁ x)) = inj₁ x
  evalBComb′ assocl₊⇛ (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
  evalBComb′ assocl₊⇛ (inj₂ y) = inj₂ (inj₂ y)
  evalBComb′ assocr₊⇛ (inj₁ x) = inj₁ (inj₁ x)
  evalBComb′ assocr₊⇛ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
  evalBComb′ assocr₊⇛ (inj₂ (inj₂ y)) = inj₂ y
  evalBComb′ {pt = a} unite⋆⇛ x = a , x
  evalBComb′ uniti⋆⇛ (_ , y) = y
  evalBComb′ swap⋆⇛ (x , y) = y , x
  evalBComb′ assocl⋆⇛ ((x , y) , z) = x , y , z
  evalBComb′ assocr⋆⇛ (x , y , z) = (x , y) , z
  evalBComb′ distz⇛ ()
  evalBComb′ factorz⇛ (() , _)
  evalBComb′ dist⇛ (inj₁ (x , y)) = inj₁ x , y
  evalBComb′ dist⇛ (inj₂ (x , y)) = inj₂ x , y
  evalBComb′ factor⇛ (inj₁ x , z) = inj₁ (x , z)
  evalBComb′ factor⇛ (inj₂ y , z) = inj₂ (y , z)
  evalBComb′ id⇛ x = x
  evalBComb′ {pt = a} (sym⇛ c) x = evalComb′ {pt = a} c x
  evalBComb′ {pt = a} (c₀ ◎ c₁) x = evalBComb′ {pt = a} c₀ (evalBComb′ {pt = a} c₁ x)
  evalBComb′ {pt = a} (c₀ ⊕ c₁) (inj₁ x) = inj₁ (evalBComb′ {pt = a} c₀ x)
  evalBComb′ {pt = a} (c₀ ⊕ c₁) (inj₂ y) = inj₂ (evalBComb′ {pt = a} c₁ y)
  evalBComb′ {pt = a} (c₀ ⊗ c₁) (x , y) = evalBComb′ {pt = a} c₀ x , evalBComb′ {pt = a} c₁ y

---

SWAP12 SWAP23 SWAP13 : PLUS ONE (PLUS ONE ONE) ⇛ PLUS ONE (PLUS ONE ONE)
SWAP12 = assocl₊⇛ ◎ (swap₊⇛ ⊕ id⇛) ◎ assocr₊⇛
SWAP23 = id⇛ ⊕ swap₊⇛
SWAP13 = SWAP23 ◎ SWAP12 ◎ SWAP23

x121 = evalComb SWAP12 (inj₁ tt)         -- 0 -> 1
x122 = evalComb SWAP12 (inj₂ (inj₁ tt))  -- 1 -> 0
x123 = evalComb SWAP12 (inj₂ (inj₂ tt))  -- 2 -> 2

x231 = evalComb SWAP23 (inj₁ tt)         -- 0 -> 0
x232 = evalComb SWAP23 (inj₂ (inj₁ tt))  -- 1 -> 2
x233 = evalComb SWAP23 (inj₂ (inj₂ tt))  -- 2 -> 1

x131 = evalComb SWAP13 (inj₁ tt)         -- 0 -> 2
x132 = evalComb SWAP13 (inj₂ (inj₁ tt))  -- 1 -> 1
x133 = evalComb SWAP13 (inj₂ (inj₂ tt))  -- 2 -> 0

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Minimal.NaturalDeduction.NegativeTranslations (𝔏 : Signature) where
open Signature(𝔏)

open import Data.Either as Either using (Left ; Right)
open import Data.ListSized using (List)
import      Logic.Propositional as Meta
import      Logic.Predicate as Meta
import      Lvl
open import Formalization.PredicateLogic.Minimal.NaturalDeduction (𝔏)
import      Formalization.PredicateLogic.Classical.NaturalDeduction
private module Classical = Formalization.PredicateLogic.Classical.NaturalDeduction (𝔏)
open import Formalization.PredicateLogic.Syntax(𝔏)
open import Formalization.PredicateLogic.Syntax.NegativeTranslations(𝔏)
open import Formalization.PredicateLogic.Syntax.Substitution(𝔏)
open import Functional using (_∘_ ; _∘₂_ ; _∘₃_ ; _∘₄_ ; swap ; _←_)
open import Numeral.Finite
open import Numeral.Natural
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Sets.PredicateSet using (PredSet ; _∈_ ; _∉_ ; _∪_ ; _∪•_ ; _∖_ ; _⊆_ ; _⊇_ ; ∅ ; [≡]-to-[⊆] ; [≡]-to-[⊇] ; map ; unmap) renaming (•_ to · ; _≡_ to _≡ₛ_)
open import Structure.Relator
open import Type

-- TODO: Move this module
module _ where
  private variable ℓ : Lvl.Level
  private variable T A B : Type{ℓ}
  private variable S S₁ S₂ : PredSet{ℓ}(T)
  private variable f : A → B
  private variable x : T

  postulate map-preserves-union : (map f(S₁ ∪ S₂) ⊆ ((map f(S₁)) ∪ (map f(S₂))))

  postulate map-preserves-singleton : (map f(S₁ ∪ S₂) ⊆ ((map f(S₁)) ∪ (map f(S₂))))

  postulate map-preserves-union-singleton : (map f(S ∪ · x) ⊆ ((map f(S)) ∪ ·(f(x))))

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable args n vars : ℕ
private variable Γ Γ₁ Γ₂ : PredSet{ℓ}(Formula(vars))
private variable φ ψ γ φ₁ ψ₁ γ₁ φ₂ ψ₂ γ₂ φ₃ ψ₃ φ₄ ψ₄ φ₅ ψ₅ δ₁ δ₂ : Formula(vars)
private variable p : Prop(args)
private variable x : List(Term(vars))(args)

[⊢]-functionₗ : (Γ₁ ≡ₛ Γ₂) → ((Γ₁ ⊢_) ≡ₛ (Γ₂ ⊢_))
[⊢]-functionₗ Γ₁Γ₂ = Meta.[↔]-intro (weaken (Meta.[↔]-to-[←] Γ₁Γ₂)) (weaken (Meta.[↔]-to-[→] Γ₁Γ₂))

[⊢][→]-elim : ((Γ ∪ · φ) ⊢ ψ) → ((Γ ⊢ φ) → (Γ ⊢ ψ))
[⊢][→]-elim Γφψ Γφ = [∨]-elim Γφψ Γφψ ([∨]-introₗ Γφ)

[⟶]-intro-inverse : (Γ ⊢ (φ ⟶ ψ)) → ((Γ ∪ · φ) ⊢ ψ)
[⟶]-intro-inverse p = [⟶]-elim (direct (Right [≡]-intro)) (weaken-union p)

weaken-closure-union : (((Γ₁ ⊢_) ∪ Γ₂) ⊢ φ) → ((((Γ₁ ∪ Γ₂) ⊢_)) ⊢ φ)
weaken-closure-union {Γ₁ = Γ₁}{Γ₂ = Γ₂}{φ = φ} = weaken sub where
  sub : ((Γ₁ ⊢_) ∪ Γ₂) ⊆ ((Γ₁ ∪ Γ₂) ⊢_)
  sub (Left  p) = weaken-union p
  sub (Right p) = direct (Right p)

{-
assume-closure : ((Γ ⊢_) ⊢ φ) → (Γ ⊢ φ)
assume-closure (direct     p)     = p
assume-closure [⊤]-intro          = [⊤]-intro
assume-closure ([∧]-intro  p q)   = [∧]-intro (assume-closure p) (assume-closure q)
assume-closure ([∧]-elimₗ  p)     = [∧]-elimₗ (assume-closure p)
assume-closure ([∧]-elimᵣ  p)     = [∧]-elimᵣ (assume-closure p)
assume-closure ([∨]-introₗ p)     = [∨]-introₗ (assume-closure p)
assume-closure ([∨]-introᵣ p)     = [∨]-introᵣ (assume-closure p)
assume-closure ([∨]-elim   p q r) = [∨]-elim {!assume-closure(weaken-closure-union p)!} ([⟶]-elim (direct(Right [≡]-intro)) {!!}) (assume-closure r)
assume-closure ([⟶]-intro  p)     = [⟶]-intro (assume-closure {!weaken-closure-union p!})
assume-closure ([⟶]-elim   p q)   = [⟶]-elim (assume-closure p) (assume-closure q)
assume-closure ([Ɐ]-intro  p)     = [Ɐ]-intro (assume-closure p)
assume-closure ([Ɐ]-elim   p)     = [Ɐ]-elim (assume-closure p)
assume-closure ([∃]-intro  p)     = [∃]-intro (assume-closure p)
assume-closure ([∃]-elim   p q)   = [∃]-elim (assume-closure {!!}) (assume-closure q)
-}

-- 2.1.8B1
[¬¬]-intro-[⟶] : (Γ ⊢ (φ ⟶ (¬¬ φ)))
[¬¬]-intro-[⟶] = [⟶]-intro ([¬¬]-intro (direct (Right [≡]-intro)))

-- 2.1.8.A1
[⟶]-const : Γ ⊢ (φ ⟶ ψ ⟶ φ)
[⟶]-const = [⟶]-intro ([⟶]-intro (direct (Left (Right [≡]-intro))))

[⟶]-refl : Γ ⊢ (φ ⟶ φ)
[⟶]-refl = [⟶]-intro (direct (Right [≡]-intro))

[⟷]-refl : Γ ⊢ (φ ⟷ φ)
[⟷]-refl = [⟷]-intro (direct (Right [≡]-intro)) (direct (Right [≡]-intro))

[⟶]-trans : (Γ ⊢ ((φ ⟶ ψ) ⟶ (ψ ⟶ γ) ⟶ (φ ⟶ γ)))
[⟶]-trans = [⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-elim ([⟶]-elim (direct (Right [≡]-intro)) (direct (Left (Left (Right [≡]-intro))))) (direct (Left (Right [≡]-intro))))))

[⟶]-contrapositiveᵣ : (Γ ⊢ (φ ⟶ ψ) ⟶ ((¬ φ) ⟵ (¬ ψ)))
[⟶]-contrapositiveᵣ = [⟶]-trans

[⟶]-double-contrapositiveᵣ : (Γ ⊢ (φ ⟶ ψ) ⟶ ((¬¬ φ) ⟶ (¬¬ ψ)))
[⟶]-double-contrapositiveᵣ = [⟶]-intro ([⟶]-elim ([⟶]-elim (direct (Right [≡]-intro)) [⟶]-contrapositiveᵣ) [⟶]-contrapositiveᵣ)

[⟶]-elim₂ : (Γ ⊢ φ₁) → (Γ ⊢ φ₂) → (Γ ⊢ (φ₁ ⟶ φ₂ ⟶ ψ)) → (Γ ⊢ ψ)
[⟶]-elim₂ = swap(_∘_) [⟶]-elim ∘ (swap(_∘_) ∘ [⟶]-elim)

[⟶]-elim₃ : (Γ ⊢ φ₁) → (Γ ⊢ φ₂) → (Γ ⊢ φ₃) → (Γ ⊢ (φ₁ ⟶ φ₂ ⟶ φ₃ ⟶ ψ)) → (Γ ⊢ ψ)
[⟶]-elim₃ = swap(_∘_) [⟶]-elim ∘₂ (swap(_∘_) ∘₂ [⟶]-elim₂)

[⟶]-elim₄ : (Γ ⊢ φ₁) → (Γ ⊢ φ₂) → (Γ ⊢ φ₃) → (Γ ⊢ φ₄) → (Γ ⊢ (φ₁ ⟶ φ₂ ⟶ φ₃ ⟶ φ₄ ⟶ ψ)) → (Γ ⊢ ψ)
[⟶]-elim₄ = swap(_∘_) [⟶]-elim ∘₃ (swap(_∘_) ∘₃ [⟶]-elim₃)

[⟶]-elim₅ : (Γ ⊢ φ₁) → (Γ ⊢ φ₂) → (Γ ⊢ φ₃) → (Γ ⊢ φ₄) → (Γ ⊢ φ₅) → (Γ ⊢ (φ₁ ⟶ φ₂ ⟶ φ₃ ⟶ φ₄ ⟶ φ₅ ⟶ ψ)) → (Γ ⊢ ψ)
[⟶]-elim₅ = swap(_∘_) [⟶]-elim ∘₄ (swap(_∘_) ∘₄ [⟶]-elim₄)

-- 2.1.8B2
[¬¬¬]-elim : Γ ⊢ ((¬ ¬ ¬ φ) ⟶ (¬ φ))
[¬¬¬]-elim = [⟶]-intro ([⟶]-intro ([⟶]-elim ([¬¬]-intro (direct (Right [≡]-intro))) (direct (Left (Right [≡]-intro)))))

[∨]-introₗ-by-[¬∧] : Γ ⊢ ((¬ φ) ⟶ ¬(φ ∧ ψ))
[∨]-introₗ-by-[¬∧] = [⟶]-intro ([⟶]-intro ([⟶]-elim ([∧]-elimₗ (direct (Right [≡]-intro))) (direct (Left (Right [≡]-intro)))))

[∨]-introᵣ-by-[¬∧] : Γ ⊢ ((¬ ψ) ⟶ ¬(φ ∧ ψ))
[∨]-introᵣ-by-[¬∧] = [⟶]-intro ([⟶]-intro ([⟶]-elim ([∧]-elimᵣ (direct (Right [≡]-intro))) (direct (Left (Right [≡]-intro)))))

[∨]-introₗ-by-[¬¬∧¬] : Γ ⊢ (φ ⟶ ¬((¬ φ) ∧ (¬ ψ)))
[∨]-introₗ-by-[¬¬∧¬] = [⟶]-intro ([⟶]-intro ([⟶]-elim (direct (Left (Right [≡]-intro))) ([∧]-elimₗ (direct (Right [≡]-intro)))))

[∨]-introᵣ-by-[¬¬∧¬] : Γ ⊢ (ψ ⟶ ¬((¬ φ) ∧ (¬ ψ)))
[∨]-introᵣ-by-[¬¬∧¬] = [⟶]-intro ([⟶]-intro ([⟶]-elim (direct (Left (Right [≡]-intro))) ([∧]-elimᵣ (direct (Right [≡]-intro)))))

[∃]-intro-by-[¬Ɐ] : ∀{t} → (Γ ⊢ ((¬(substitute0 t φ)) ⟶ ¬(Ɐ φ)))
[∃]-intro-by-[¬Ɐ] = [⟶]-intro ([⟶]-intro ([⟶]-elim ([Ɐ]-elim (direct (Right [≡]-intro))) (direct (Left (Right [≡]-intro)))))

[∃]-intro-by-[¬Ɐ¬] : ∀{t} → (Γ ⊢ ((substitute0 t φ) ⟶ ¬(Ɐ(¬ φ))))
[∃]-intro-by-[¬Ɐ¬] = [⟶]-intro ([⟶]-intro ([⟶]-elim (direct (Left (Right [≡]-intro))) ([Ɐ]-elim (direct (Right [≡]-intro)))))

[∧]-map : Γ ⊢ ((φ₁ ⟶ φ₂) ⟶ (ψ₁ ⟶ ψ₂) ⟶ ((φ₁ ∧ ψ₁) ⟶ (φ₂ ∧ ψ₂)))
[∧]-map = [⟶]-intro ([⟶]-intro ([⟶]-intro ([∧]-intro ([⟶]-elim ([∧]-elimₗ (direct (Right [≡]-intro))) (direct (Left (Left (Right [≡]-intro))))) ([⟶]-elim ([∧]-elimᵣ (direct (Right [≡]-intro))) (direct (Left (Right [≡]-intro)))))))

[∨]-map : Γ ⊢ ((φ₁ ⟶ φ₂) ⟶ (ψ₁ ⟶ ψ₂) ⟶ ((φ₁ ∨ ψ₁) ⟶ (φ₂ ∨ ψ₂)))
[∨]-map = [⟶]-intro ([⟶]-intro ([⟶]-intro ([∨]-elim ([∨]-introₗ ([⟶]-intro-inverse (direct (Left (Left (Right [≡]-intro)))))) ([∨]-introᵣ ([⟶]-intro-inverse (direct (Left (Right [≡]-intro))))) (direct (Right [≡]-intro)))))

[Ɐ]-map : Γ ⊢ (Ɐ(φ₁ ⟶ φ₂) ⟶ ((Ɐ φ₁) ⟶ (Ɐ φ₂)))
[Ɐ]-map = [⟶]-intro ([⟶]-intro ([Ɐ]-intro ([⟶]-elim ([Ɐ]-elim (direct (Right [≡]-intro))) ([Ɐ]-elim(direct (Left (Right [≡]-intro)))))))

[⟶]-map : Γ ⊢ ((φ₁ ⟵ φ₂) ⟶ (ψ₁ ⟶ ψ₂) ⟶ ((φ₁ ⟶ ψ₁) ⟶ (φ₂ ⟶ ψ₂)))
[⟶]-map = [⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-elim ([⟶]-elim ([⟶]-elim (direct (Right [≡]-intro)) (direct (Left (Left (Left (Right [≡]-intro)))))) (direct (Left (Right [≡]-intro)))) (direct (Left (Left (Right [≡]-intro))))))))

[⟶]-map₂ : Γ ⊢ ((φ₁ ⟵ φ₂) ⟶ (ψ₁ ⟵ ψ₂) ⟶ (γ₁ ⟶ γ₂) ⟶ ((φ₁ ⟶ ψ₁ ⟶ γ₁) ⟶ (φ₂ ⟶ ψ₂ ⟶ γ₂)))
[⟶]-map₂ = [⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-elim₂ (direct (Left (Left (Right [≡]-intro)))) ([⟶]-elim₂ (direct (Left (Right [≡]-intro))) (direct (Right [≡]-intro)) [⟶]-map) [⟶]-map)))

[⟶]-map₃ : Γ ⊢ ((φ₁ ⟵ φ₂) ⟶ (ψ₁ ⟵ ψ₂) ⟶ (γ₁ ⟵ γ₂) ⟶ (δ₁ ⟶ δ₂) ⟶ ((φ₁ ⟶ ψ₁ ⟶ γ₁ ⟶ δ₁) ⟶ (φ₂ ⟶ ψ₂ ⟶ γ₂ ⟶ δ₂)))
[⟶]-map₃ = [⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-elim₃ (direct (Left (Left (Left (Right [≡]-intro))))) (direct (Left (Left (Right [≡]-intro)))) ([⟶]-elim₂ (direct (Left (Right [≡]-intro))) (direct (Right [≡]-intro)) [⟶]-map) [⟶]-map₂))))

[¬]-map : Γ ⊢ ((φ ⟵ ψ) ⟶ (¬ φ) ⟶ (¬ ψ))
[¬]-map = [⟶]-contrapositiveᵣ

[⟶]-trans₂ : (Γ ⊢ ((φ₁ ⟶ φ₂ ⟶ ψ) ⟶ (ψ ⟶ γ) ⟶ (φ₁ ⟶ φ₂ ⟶ γ)))
[⟶]-trans₂ = [⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-elim ([⟶]-elim₂ (direct (Left (Right [≡]-intro))) (direct (Right [≡]-intro)) (direct (Left (Left (Left (Right [≡]-intro)))))) (direct (Left (Left (Right [≡]-intro))))))))

-- 2.1.8B3
[¬¬]-preserve-[⟶] : Γ ⊢ (¬¬(φ ⟶ ψ) ⟶ ((¬¬ φ) ⟶ (¬¬ ψ)))
[¬¬]-preserve-[⟶] = [⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-elim ([⟶]-intro ([⟶]-elim ([⟶]-elim (direct (Left (Left (Right [≡]-intro)))) ([⟶]-elim (direct(Right [≡]-intro)) [⟶]-double-contrapositiveᵣ)) ([¬¬]-intro (direct (Left (Right [≡]-intro)))))) (direct (Left (Left (Right [≡]-intro)))))))

-- 2.1.8B4
[¬¬]-preserve-[∧] : Γ ⊢ (¬¬(φ ∧ ψ) ⟷ ((¬¬ φ) ∧ (¬¬ ψ)))
[¬¬]-preserve-[∧] {Γ = Γ}{φ = φ} =
  [⟷]-intro
    ([⟶]-intro ([⟶]-elim ([⟶]-intro ([⟶]-elim ([⟶]-intro ([⟶]-elim ([∧]-intro (direct (Left (Right [≡]-intro))) (direct (Right [≡]-intro))) (direct (Left (Left (Right [≡]-intro)))))) ([∧]-elimᵣ (direct (Left (Left (Right [≡]-intro))))))) ([∧]-elimₗ (direct (Left (Right [≡]-intro))))))
    ([∧]-intro
      ([⟶]-intro ([⟶]-elim ([⟶]-elim (direct (Right [≡]-intro)) [∨]-introₗ-by-[¬∧]) (direct (Left (Right [≡]-intro)))))
      ([⟶]-intro ([⟶]-elim ([⟶]-elim (direct (Right [≡]-intro)) [∨]-introᵣ-by-[¬∧]) (direct (Left (Right [≡]-intro)))))
    )

-- 2.1.8B5
[¬]-preserve-[∨][∧] : Γ ⊢ (¬(φ ∨ ψ) ⟷ ((¬ φ) ∧ (¬ ψ)))
[¬]-preserve-[∨][∧] =
  [⟷]-intro
    ([⟶]-intro ([∨]-elim
      ([⟶]-elim (direct (Right [≡]-intro)) ([∧]-elimₗ (direct (Left (Left (Right [≡]-intro))))))
      ([⟶]-elim (direct (Right [≡]-intro)) ([∧]-elimᵣ (direct (Left (Left (Right [≡]-intro))))))
      (direct (Right [≡]-intro))
    ))
    ([∧]-intro
      ([⟶]-intro ([⟶]-elim ([∨]-introₗ (direct (Right [≡]-intro))) (direct (Left (Right [≡]-intro)))))
      ([⟶]-intro ([⟶]-elim ([∨]-introᵣ (direct (Right [≡]-intro))) (direct (Left (Right [≡]-intro)))))
    )

-- 2.1.8B6
[¬¬]-preserve-[Ɐ] : Γ ⊢ (¬¬(Ɐ φ) ⟶ (Ɐ(¬¬ φ)))
[¬¬]-preserve-[Ɐ] = [⟶]-intro ([Ɐ]-intro ([⟶]-intro ([⟶]-elim ([⟶]-elim (direct (Right [≡]-intro)) [∃]-intro-by-[¬Ɐ]) (direct (Left (Right [≡]-intro))))))

[¬]-preserve-[∃][Ɐ] : Γ ⊢ (¬(∃ φ) ⟷ (Ɐ(¬ φ)))
[¬]-preserve-[∃][Ɐ] =
  [⟷]-intro
    ([⟶]-intro ([∃]-elim ([⟶]-intro-inverse ([Ɐ]-elim (direct (Left (Right [≡]-intro))))) (direct (Right [≡]-intro))))
    ([Ɐ]-intro ([⟶]-intro ([⟶]-elim ([∃]-intro (direct (Right [≡]-intro))) (direct (Left (Right [≡]-intro))))))

open import Lang.Instance

-- 2.3.1
data NegativeFragment : Formula(vars) → Type{ℓₚ Lvl.⊔ ℓₒ} where
  atom   : NegativeFragment(¬(p $ x))
  bottom : NegativeFragment{vars}(⊥)
  top    : NegativeFragment{vars}(⊤)
  and    : NegativeFragment(φ) → NegativeFragment(ψ) → NegativeFragment(φ ∧ ψ)
  impl   : NegativeFragment(φ) → NegativeFragment(ψ) → NegativeFragment(φ ⟶ ψ)
  all    : (∀{t} → NegativeFragment(substitute0 t φ)) → NegativeFragment(Ɐ φ)
pattern neg p = NegativeFragment.impl p bottom
instance _ = \{vars} {p}{args}{x} → atom{vars}{p = p}{args}{x = x}
instance _ = \{vars} → bottom{vars}
instance _ = \{vars} → top{vars}
instance _ = \{vars} {φ} ⦃ neg-φ ⦄ {ψ} ⦃ neg-ψ ⦄ → and{vars}{φ = φ}{ψ = ψ} neg-φ neg-ψ
instance _ = \{vars} {φ} ⦃ neg-φ ⦄ {ψ} ⦃ neg-ψ ⦄ → impl{vars}{φ = φ}{ψ = ψ} neg-φ neg-ψ
instance _ = \{vars} {φ} ⦃ neg-φ : ∀{_} → _ ⦄ → all{vars}{φ = φ} (\{t} → neg-φ{t})

-- 2.3.2
[¬¬]-elim-on-negativeFragment : NegativeFragment(φ) → (Γ ⊢ ((¬¬ φ) ⟶ φ))
[¬¬]-elim-on-negativeFragment atom             = [¬¬¬]-elim
[¬¬]-elim-on-negativeFragment bottom           = [¬¬]-intro [⟶]-refl
[¬¬]-elim-on-negativeFragment top              = [⟶]-intro [⊤]-intro
[¬¬]-elim-on-negativeFragment (and  negφ negψ) =
  [⟶]-intro ([∧]-intro
    ([⟶]-elim ([∧]-elimₗ([⟷]-elimᵣ (direct (Right [≡]-intro)) [¬¬]-preserve-[∧])) ([¬¬]-elim-on-negativeFragment negφ))
    ([⟶]-elim ([∧]-elimᵣ([⟷]-elimᵣ (direct (Right [≡]-intro)) [¬¬]-preserve-[∧])) ([¬¬]-elim-on-negativeFragment negψ))
  )
[¬¬]-elim-on-negativeFragment (impl negφ negψ) =
  [⟶]-intro ([⟶]-intro ([⟶]-elim
    ([⟶]-elim₂ (direct (Left (Right [≡]-intro))) ([¬¬]-intro (direct (Right [≡]-intro))) [¬¬]-preserve-[⟶])
    ([¬¬]-elim-on-negativeFragment negψ)
  ))
[¬¬]-elim-on-negativeFragment (all  negφ)      = [⟶]-intro ([Ɐ]-intro ([⟶]-elim ([⟶]-intro ([⟶]-elim ([⟶]-elim (direct (Right [≡]-intro)) [∃]-intro-by-[¬Ɐ]) (direct (Left (Right [≡]-intro))))) ([¬¬]-elim-on-negativeFragment negφ)))

Stable : ∀{ℓ}{vars} → Formula(vars) → Type
Stable{ℓ = ℓ} (φ) = ∀{Γ : PredSet{ℓ}(_)} → (Γ ⊢ (¬¬ φ ⟶ φ))

[¬]-stability : Stable{ℓ}(¬ φ)
[¬]-stability = [¬¬¬]-elim

-- [∨]-stability : Stable(φ) → Stable(ψ) → Stable{ℓ}(φ ∨ ψ)
-- [∨]-stability sφ sψ = [⟶]-intro ([∨]-elim ([∨]-introₗ {!!}) ([∨]-introᵣ {!!}) {!!})

[∨]-elim-by-[¬∧] : Stable(φ) → Stable(ψ) → Stable(γ) → (Γ ⊢ (((¬ φ) ⟶ γ) ⟶ ((¬ ψ) ⟶ γ) ⟶ ¬(φ ∧ ψ) ⟶ γ))
[∨]-elim-by-[¬∧] negφ negψ negγ = [⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-elim ([⟶]-intro ([⟶]-elim ([⟶]-elim₃ negφ negψ ([∧]-intro ([⟶]-elim (direct (Right [≡]-intro)) ([⟶]-elim (direct (Left (Left (Left (Right [≡]-intro))))) [⟶]-contrapositiveᵣ)) ([⟶]-elim (direct (Right [≡]-intro)) ([⟶]-elim (direct (Left (Left (Right [≡]-intro)))) [⟶]-contrapositiveᵣ))) [∧]-map) (direct (Left (Right [≡]-intro))))) negγ)))

[∨]-elim-by-[¬¬∧¬] : (∀{ℓ} → Stable{ℓ}(γ)) → (Γ ⊢ ((φ ⟶ γ) ⟶ (ψ ⟶ γ) ⟶ ¬((¬ φ) ∧ (¬ ψ)) ⟶ γ))
[∨]-elim-by-[¬¬∧¬] negγ = [⟶]-elim₅ (pp negγ) (pp negγ) [⟶]-refl [⟶]-refl ([∨]-elim-by-[¬∧] [¬]-stability [¬]-stability negγ) [⟶]-map₃ where
  pp : Stable(ψ) → (Γ ⊢ ((φ ⟶ ψ) ⟶ ((¬¬ φ) ⟶ ψ)))
  pp negψ = [⟶]-elim₂ [⟶]-double-contrapositiveᵣ negψ [⟶]-trans₂

[⟷]-to-[⟵] : (Γ ⊢ (φ ⟷ ψ)) → (Γ ⊢ (φ ⟵ ψ))
[⟷]-to-[⟵] p = [⟶]-intro ([⟷]-elimₗ (direct (Right [≡]-intro)) (weaken-union p))

[⟷]-to-[⟶] : (Γ ⊢ (φ ⟷ ψ)) → (Γ ⊢ (φ ⟶ ψ))
[⟷]-to-[⟶] p = [⟶]-intro ([⟷]-elimᵣ (direct (Right [≡]-intro)) (weaken-union p))

[Ɐ][→]-distributivity : Γ ⊢ (Ɐ(φ ⟶ ψ) ⟶ (Ɐ φ) ⟶ (Ɐ ψ))
[Ɐ][→]-distributivity = [⟶]-intro ([⟶]-intro ([Ɐ]-intro ([⟶]-elim ([Ɐ]-elim (direct (Right [≡]-intro))) ([Ɐ]-elim (direct (Left (Right [≡]-intro)))))))

[¬∃]-to-[∀¬] : Γ ⊢ (¬(∃ φ) ⟶ Ɐ(¬ φ))
[¬∃]-to-[∀¬] = [⟶]-intro ([Ɐ]-intro ([⟶]-intro ([⟶]-elim ([∃]-intro (direct (Right [≡]-intro))) (direct (Left (Right [≡]-intro))))))

[¬Ɐ]-to-[∃¬] : (∀{t} → Stable(substitute0 t φ)) → Stable(∃(¬ φ)) → (Γ ⊢ (¬(Ɐ φ) ⟶ ∃(¬ φ)))
[¬Ɐ]-to-[∃¬] negφ nege = [⟶]-intro ([⟶]-elim ([⟶]-intro ([⟶]-elim ([⟶]-elim₂ ([Ɐ]-intro negφ) ([⟶]-elim (direct (Right [≡]-intro)) [¬∃]-to-[∀¬]) [Ɐ][→]-distributivity) (direct (Left (Right [≡]-intro))))) nege)

{-
test : (Γ ⊢ (¬¬ φ ⟶ φ)) → (Γ ⊢ (¬ Ɐ(¬ φ))) → (Γ ⊢ ∃ φ)
test negφ p = [∃]-elim ([∃]-intro {![⟶]-intro negφ!}) ([⟶]-elim p test2)
-}

[∃]-elim-by-[¬¬∧¬] : (∀{t} → (Γ ∪ ·(substitute0 t φ)) ⊢ ψ) → (Γ ⊢ ¬(Ɐ(¬ φ))) → (Γ ⊢ ψ)
[∃]-elim-by-[¬¬∧¬] p q = [∃]-elim p {!!}

-- test : ∀{t} → (Γ₁ ≡ₛ Γ₂) → (Γ₁ ⊢ φ) → (Γ₂ ⊢ substitute0 t φ)
-- test p = {!p!}

{-
test : ∀{t} → (∀{Γ : PredSet{ℓ}(Formula(𝐒(vars)))} → (Γ ⊢ φ)) → (∀{Γ : PredSet{ℓ}(Formula(vars))} → (Γ ⊢ substitute0 t φ))
test {t = t} Γφ {Γ} with Γφ{unmap(substitute0 t) Γ}
... | direct     p     = direct p
... | [⊤]-intro        = [⊤]-intro
... | [∧]-intro  p q   = [∧]-intro {!test p!} {!!}
... | [∧]-elimₗ  p     = {!!}
... | [∧]-elimᵣ  p     = {!!}
... | [∨]-introₗ p     = {!!}
... | [∨]-introᵣ p     = {!!}
... | [∨]-elim   p q r = {!!}
... | [⟶]-intro  p     = {!!}
... | [⟶]-elim   p q   = {!!}
... | [Ɐ]-intro  p     = {!!}
... | [Ɐ]-elim   p     = {!!}
... | [∃]-intro  p     = {!!}
... | [∃]-elim   p q   = {!!}
-}

substitute0-negativeFragment : NegativeFragment(φ) → ∀{t} → NegativeFragment(substitute0 t φ)
substitute0-negativeFragment atom       = atom
substitute0-negativeFragment bottom     = bottom
substitute0-negativeFragment top        = top
substitute0-negativeFragment (and  p q) = and (substitute0-negativeFragment p) (substitute0-negativeFragment q)
substitute0-negativeFragment (impl p q) = impl (substitute0-negativeFragment p) (substitute0-negativeFragment q)
substitute0-negativeFragment (all  p)   = {!!} -- all (substitute0-negativeFragment p)

ggTrans-negativeFragment : NegativeFragment(ggTrans(φ))
ggTrans-negativeFragment {φ = p $ x} = neg atom
ggTrans-negativeFragment {φ = ⊤}     = top
ggTrans-negativeFragment {φ = ⊥}     = bottom
ggTrans-negativeFragment {φ = φ ∧ ψ} = and ggTrans-negativeFragment ggTrans-negativeFragment
ggTrans-negativeFragment {φ = φ ∨ ψ} = neg(and(neg ggTrans-negativeFragment) (neg ggTrans-negativeFragment))
ggTrans-negativeFragment {φ = φ ⟶ ψ} = impl ggTrans-negativeFragment ggTrans-negativeFragment
ggTrans-negativeFragment {φ = Ɐ φ}   = all (substitute0-negativeFragment (ggTrans-negativeFragment {φ = φ}))
ggTrans-negativeFragment {φ = ∃ φ}   = neg (all (neg (substitute0-negativeFragment (ggTrans-negativeFragment {φ = φ}))))

-- [¬¬]-elim-of-koTrans : (Γ ⊢ (¬¬ ggTrans(φ))) ← (Γ ⊢ (ggTrans φ))

ggTrans-substitute0 : ∀{t} → (ggTrans(substitute0 t φ) ≡ substitute0 t (ggTrans φ))
ggTrans-substitute0 {φ = P $ x} = [≡]-intro
ggTrans-substitute0 {φ = ⊤}     = [≡]-intro
ggTrans-substitute0 {φ = ⊥}     = [≡]-intro
ggTrans-substitute0 {φ = φ ∧ ψ}{t}
  rewrite ggTrans-substitute0 {φ = φ}{t}
  rewrite ggTrans-substitute0 {φ = ψ}{t}
  = [≡]-intro
ggTrans-substitute0 {φ = φ ∨ ψ}{t}
  rewrite ggTrans-substitute0 {φ = φ}{t}
  rewrite ggTrans-substitute0 {φ = ψ}{t}
  = [≡]-intro
ggTrans-substitute0 {φ = φ ⟶ ψ}{t}
  rewrite ggTrans-substitute0 {φ = φ}{t}
  rewrite ggTrans-substitute0 {φ = ψ}{t}
  = [≡]-intro
ggTrans-substitute0 {φ = Ɐ φ}{t} = {!!}
  -- rewrite ggTrans-substitute0 {φ = φ}{termVar𝐒 t}
  -- = [≡]-intro
ggTrans-substitute0 {φ = ∃ φ}{t} = {!!}
  -- rewrite ggTrans-substitute0 {φ = φ}{termVar𝐒 t}
  -- = [≡]-intro

koTrans-substitute0 : ∀{t} → (koTrans(substitute0 t φ) ≡ substitute0 t (koTrans φ))
koTrans-substitute0 {φ = f $ x} = [≡]-intro
koTrans-substitute0 {φ = ⊤}     = [≡]-intro
koTrans-substitute0 {φ = ⊥}     = [≡]-intro
koTrans-substitute0 {φ = φ ∧ ψ}{t}
  rewrite koTrans-substitute0 {φ = φ}{t}
  rewrite koTrans-substitute0 {φ = ψ}{t}
  = [≡]-intro
koTrans-substitute0 {φ = φ ∨ ψ}{t}
  rewrite koTrans-substitute0 {φ = φ}{t}
  rewrite koTrans-substitute0 {φ = ψ}{t}
  = [≡]-intro
koTrans-substitute0 {φ = φ ⟶ ψ}{t}
  rewrite koTrans-substitute0 {φ = φ}{t}
  rewrite koTrans-substitute0 {φ = ψ}{t}
  = [≡]-intro
koTrans-substitute0 {φ = Ɐ φ}{t} = {!!}
  -- rewrite koTrans-substitute0 {φ = φ}{termVar𝐒 t}
  -- = [≡]-intro
koTrans-substitute0 {φ = ∃ φ}{t} = {!!}
  -- rewrite koTrans-substitute0 {φ = φ}{termVar𝐒 t}
  -- = [≡]-intro

-- 2.3.4 (ii)
ggTrans-correctnessₗ : (Γ Classical.⊢ φ) ← (map ggTrans Γ ⊢ (ggTrans φ))
ggTrans-correctnessᵣ : (Γ Classical.⊢ φ) → (map ggTrans Γ ⊢ (ggTrans φ))

ggTrans-correctnessᵣ (Classical.direct p) = direct (Meta.[∃]-intro _ ⦃ Meta.[∧]-intro p [≡]-intro ⦄)
ggTrans-correctnessᵣ (Classical.[⊤]-intro) = [⊤]-intro
ggTrans-correctnessᵣ {Γ = Γ}{φ = φ} (Classical.[⊥]-elim p) = [⟶]-elim ([⟶]-intro(weaken{Γ₂ = (map ggTrans Γ) ∪ ·(ggTrans(¬ φ))} map-preserves-union-singleton (ggTrans-correctnessᵣ p))) ([¬¬]-elim-on-negativeFragment ggTrans-negativeFragment)
ggTrans-correctnessᵣ (Classical.[∧]-intro p q) = [∧]-intro (ggTrans-correctnessᵣ p) (ggTrans-correctnessᵣ q)
ggTrans-correctnessᵣ (Classical.[∧]-elimₗ p) = [∧]-elimₗ (ggTrans-correctnessᵣ p)
ggTrans-correctnessᵣ (Classical.[∧]-elimᵣ p) = [∧]-elimᵣ (ggTrans-correctnessᵣ p)
ggTrans-correctnessᵣ (Classical.[∨]-introₗ p) = [⟶]-elim (ggTrans-correctnessᵣ p) [∨]-introₗ-by-[¬¬∧¬]
ggTrans-correctnessᵣ (Classical.[∨]-introᵣ p) = [⟶]-elim (ggTrans-correctnessᵣ p) [∨]-introᵣ-by-[¬¬∧¬]
ggTrans-correctnessᵣ (Classical.[∨]-elim p q r) = [⟶]-elim₃ ([⟶]-intro(weaken map-preserves-union-singleton (ggTrans-correctnessᵣ p))) ([⟶]-intro(weaken map-preserves-union-singleton (ggTrans-correctnessᵣ q))) (ggTrans-correctnessᵣ r) ([∨]-elim-by-[¬¬∧¬] ([¬¬]-elim-on-negativeFragment ggTrans-negativeFragment))
ggTrans-correctnessᵣ (Classical.[⟶]-intro p) = [⟶]-intro (weaken map-preserves-union-singleton (ggTrans-correctnessᵣ p))
ggTrans-correctnessᵣ (Classical.[⟶]-elim p q) = [⟶]-elim (ggTrans-correctnessᵣ p) (ggTrans-correctnessᵣ q)
ggTrans-correctnessᵣ (Classical.[Ɐ]-intro p) = [Ɐ]-intro (substitute₁(_ ⊢_) ggTrans-substitute0 (ggTrans-correctnessᵣ p))
ggTrans-correctnessᵣ (Classical.[Ɐ]-elim p) = substitute₁ₗ(_ ⊢_) ggTrans-substitute0 ([Ɐ]-elim (ggTrans-correctnessᵣ p))
ggTrans-correctnessᵣ (Classical.[∃]-intro p) = [⟶]-elim (substitute₁(_ ⊢_) ggTrans-substitute0 (ggTrans-correctnessᵣ p)) [∃]-intro-by-[¬Ɐ¬]
ggTrans-correctnessᵣ (Classical.[∃]-elim p q) = [⟶]-elim ([⟶]-intro ([⟶]-elim ([Ɐ]-intro ([⟶]-intro ([⟶]-elim (weaken {!map-preserves-union-singleton!} (ggTrans-correctnessᵣ p)) (direct (Left (Right [≡]-intro)))))) (weaken-union (ggTrans-correctnessᵣ q)))) ([¬¬]-elim-on-negativeFragment ggTrans-negativeFragment)

koTrans-stability : Stable{ℓ}(koTrans(φ))
koTrans-stability {φ = f $ x} = [¬¬¬]-elim
koTrans-stability {φ = ⊤}     = [⟶]-intro [⊤]-intro
koTrans-stability {φ = ⊥}     = [⟶]-intro ([⟶]-elim [⟶]-refl (direct (Right [≡]-intro)))
koTrans-stability {φ = φ ∧ ψ} = [¬¬¬]-elim
koTrans-stability {φ = φ ∨ ψ} = [¬¬¬]-elim
koTrans-stability {φ = φ ⟶ ψ} = [¬¬¬]-elim
koTrans-stability {φ = Ɐ φ}   = [¬¬¬]-elim
koTrans-stability {φ = ∃ φ}   = [¬¬¬]-elim

{-
koTrans-to-[¬¬] : Γ ⊢ (koTrans(φ) ⟶ (¬¬ φ))
koTrans-to-[¬¬] {φ = f $ x} = [⟶]-refl
koTrans-to-[¬¬] {φ = ⊤}     = [¬¬]-intro-[⟶]
koTrans-to-[¬¬] {φ = ⊥}     = [¬¬]-intro-[⟶]
koTrans-to-[¬¬] {φ = φ ∧ ψ} = [⟶]-intro ([⟷]-elimₗ ([⟶]-elim₃ koTrans-to-[¬¬] koTrans-to-[¬¬] {!!} [∧]-map) [¬¬]-preserve-[∧])
koTrans-to-[¬¬] {φ = φ ∨ ψ} = {!!}
koTrans-to-[¬¬] {φ = φ ⟶ ψ} = {!!}
koTrans-to-[¬¬] {φ = Ɐ φ}   = {!!}
koTrans-to-[¬¬] {φ = ∃ φ}   = {!!}
-}

ggTrans-koTransₗ : Γ ⊢ ((ggTrans φ) ⟵ (koTrans φ))
ggTrans-koTransᵣ : Γ ⊢ ((ggTrans φ) ⟶ (koTrans φ))

[∧]-elimₗ-koTrans : (Γ ⊢ (koTrans(φ ∧ ψ) ⟶ koTrans(φ)))
[∧]-elimₗ-koTrans = [⟶]-intro ([∧]-elimₗ ([⟶]-elim₃ koTrans-stability koTrans-stability ([⟷]-elimᵣ (direct (Right [≡]-intro)) [¬¬]-preserve-[∧]) [∧]-map))

[∧]-elimᵣ-koTrans : (Γ ⊢ (koTrans(φ ∧ ψ) ⟶ koTrans(ψ)))
[∧]-elimᵣ-koTrans = [⟶]-intro ([∧]-elimᵣ ([⟶]-elim₃ koTrans-stability koTrans-stability ([⟷]-elimᵣ (direct (Right [≡]-intro)) [¬¬]-preserve-[∧]) [∧]-map))

-- [⟶]-elim-koTrans : (Γ ⊢ (koTrans(φ) ⟶ koTrans(φ ⟶ ψ) ⟶ koTrans(ψ)))

-- [⟶]-intro ([⟶]-elim ([∧]-elimₗ ([⟷]-elimᵣ ([⟶]-intro-inverse {![¬¬]-intro-[⟶]!}) [¬¬]-preserve-[∧])) koTrans-stability)
-- {![∧]-elimₗ(Meta.[↔]-to-[→] [¬¬][∧] Γφψ)!}

-- [¬]-preserve-[∨][∧] : Γ ⊢ (¬(φ ∨ ψ) ⟷ ((¬ φ) ∧ (¬ ψ)))

-- Alternative proof of the (_∧_)-case:
--   [⟶]-intro ([∧]-intro
--     ([⟶]-elim ([⟶]-elim (direct (Right [≡]-intro)) [∧]-elimₗ-koTrans) (weaken-union(ggTrans-koTransₗ {φ = φ})))
--     ([⟶]-elim ([⟶]-elim (direct (Right [≡]-intro)) [∧]-elimᵣ-koTrans) (weaken-union(ggTrans-koTransₗ {φ = ψ})))
--   )
ggTrans-koTransₗ {φ = P $ x} = [⟶]-refl
ggTrans-koTransₗ {φ = ⊤}     = [⟶]-refl
ggTrans-koTransₗ {φ = ⊥}     = [⟶]-refl
ggTrans-koTransₗ {φ = φ ∧ ψ} = [⟶]-elim₃
  ([⟶]-elim₂ ([⟷]-to-[⟶] [¬¬]-preserve-[∧]) ([⟶]-elim₂ koTrans-stability koTrans-stability [∧]-map) [⟶]-trans)
  [⟶]-refl
  ([⟶]-elim₂ (ggTrans-koTransₗ {φ = φ}) (ggTrans-koTransₗ {φ = ψ}) [∧]-map)
  [⟶]-map
ggTrans-koTransₗ {φ = φ ∨ ψ} = [⟶]-elim₃
  ([⟶]-elim ([⟷]-to-[⟵] [¬]-preserve-[∨][∧]) [⟶]-contrapositiveᵣ)
  [⟶]-refl
  ([⟶]-elim ([⟶]-elim₂ ([⟶]-elim (ggTrans-koTransₗ {φ = φ}) [¬]-map) ([⟶]-elim (ggTrans-koTransₗ {φ = ψ}) [¬]-map) [∧]-map) [¬]-map)
  [⟶]-map
ggTrans-koTransₗ {φ = φ ⟶ ψ} = [⟶]-elim₃
  (([⟶]-elim₂ [¬¬]-preserve-[⟶] ([⟶]-elim₂ [¬¬]-intro-[⟶] koTrans-stability [⟶]-map) [⟶]-trans))
  [⟶]-refl
  (([⟶]-elim₂ (ggTrans-koTransᵣ {φ = φ}) (ggTrans-koTransₗ {φ = ψ}) [⟶]-map))
  [⟶]-map
ggTrans-koTransₗ {Γ = Γ}{φ = Ɐ φ} = [⟶]-elim₃
  ([⟶]-elim₂ [¬¬]-preserve-[Ɐ] ([⟶]-elim ([Ɐ]-intro (substitute₁(\φ → Γ ⊢ ((¬¬ φ) ⟶ φ)) koTrans-substitute0 koTrans-stability)) ([Ɐ]-map {φ₂ = koTrans φ})) [⟶]-trans)
  [⟶]-refl
  ([⟶]-elim ([Ɐ]-intro (substitute₂(\a b → Γ ⊢ (a ⟵ b)) ggTrans-substitute0 koTrans-substitute0 (ggTrans-koTransₗ {φ = substitute0 _ φ}))) [Ɐ]-map)
  [⟶]-map
ggTrans-koTransₗ {φ = ∃ φ} = [⟶]-elim₃
  ([⟶]-elim ([⟷]-to-[⟵] [¬]-preserve-[∃][Ɐ]) [⟶]-contrapositiveᵣ)
  [⟶]-refl
  ([⟶]-elim ([⟶]-elim ([Ɐ]-intro ([⟶]-elim (substitute₂(\a b → _ ⊢ (a ⟵ b)) ggTrans-substitute0 koTrans-substitute0 (ggTrans-koTransₗ {φ = substitute0 _ φ})) [¬]-map)) [Ɐ]-map) [¬]-map)
  [⟶]-map

ggTrans-koTransᵣ {φ = P $ x} = [⟶]-refl
ggTrans-koTransᵣ {φ = ⊤}     = [⟶]-refl
ggTrans-koTransᵣ {φ = ⊥}     = [⟶]-refl
ggTrans-koTransᵣ {φ = φ ∧ ψ} =
  [⟶]-intro ([¬¬]-intro ([∧]-intro
    ([⟶]-elim ([∧]-elimₗ (direct (Right [≡]-intro))) (weaken-union(ggTrans-koTransᵣ {φ = φ})))
    ([⟶]-elim ([∧]-elimᵣ (direct (Right [≡]-intro))) (weaken-union(ggTrans-koTransᵣ {φ = ψ})))
  ))
ggTrans-koTransᵣ {φ = φ ∨ ψ} =
  [⟶]-intro ([¬¬]-intro ([⟶]-elim₃
    {!!}
    {!!}
    {!direct (Right [≡]-intro)!}
    ([∨]-elim-by-[¬¬∧¬] {!koTrans-stability!})
  ))
ggTrans-koTransᵣ {φ = φ ⟶ ψ} =
  [⟶]-intro ([¬¬]-intro ([⟶]-intro
    ([⟶]-elim
      ([⟶]-elim ([⟵]-elim (direct (Right [≡]-intro)) (weaken-union(weaken-union(ggTrans-koTransₗ {φ = φ})))) (direct (Left (Right [≡]-intro))))
      (weaken-union(weaken-union(ggTrans-koTransᵣ {φ = ψ})))
    )
  ))
ggTrans-koTransᵣ {φ = Ɐ φ}   = {!!}
ggTrans-koTransᵣ {φ = ∃ φ}   = {!!}


text:
module Cats.Category where

open import Level

import Cats.Category.Base as Base
import Cats.Category.Constructions.CCC as CCC
import Cats.Category.Constructions.Epi as Epi
import Cats.Category.Constructions.Equalizer as Equalizer
import Cats.Category.Constructions.Exponential as Exponential
import Cats.Category.Constructions.Iso as Iso
import Cats.Category.Constructions.Initial as Initial
import Cats.Category.Constructions.Mono as Mono
import Cats.Category.Constructions.Product as Product
import Cats.Category.Constructions.Terminal as Terminal
import Cats.Category.Constructions.Unique as Unique

Category : ∀ lo la l≈ → Set (suc (lo ⊔ la ⊔ l≈))
Category = Base.Category

module Category {lo la l≈} (Cat : Base.Category lo la l≈) where

  open Base.Category Cat public
  open Epi.Build Cat public
  open Equalizer.Build Cat public
  open Exponential.Build Cat public
  open Initial.Build Cat public
  open Iso.Build Cat public
  open Mono.Build Cat public
  open Product.Build Cat public
  open Terminal.Build Cat public
  open Unique.Build Cat public

open CCC public using (IsCCC)
open Exponential public using (HasExponentials)
open Initial public using (HasInitial)
open Product public using
  ( HasProducts ; HasBinaryProducts ; HasFiniteProducts
  ; HasProducts→HasBinaryProducts
  ; HasProducts→HasTerminal )
open Terminal public using (HasTerminal)

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.Equiv.Comp-Poly where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.Polynomials.Univariate.Base

open import Cubical.Algebra.Polynomials.Multivariate.Base
open import Cubical.Algebra.Polynomials.Multivariate.Properties
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly

private variable
  ℓ ℓ' : Level

module Comp-Poly-nm (A' : CommRing ℓ) (n m : ℕ) where
  private
    A = fst A'
  open CommRingStr (snd A')

  module Mr  = Nth-Poly-structure A' m
  module N+Mr = Nth-Poly-structure A' (n +n m)
  module N∘Mr  = Nth-Poly-structure (PolyCommRing A' m) n

-----------------------------------------------------------------------------
-- direct sens

  N∘M→N+M-b : (v : Vec ℕ n) → Poly A' m → Poly A' (n +n m)
  N∘M→N+M-b v = Poly-Rec-Set.f A' m (Poly A' (n +n m)) trunc
                0P
                (λ v' a → base (v ++ v') a)
                _Poly+_
                Poly+-assoc
                Poly+-Rid
                Poly+-comm
                (λ v' → base-0P (v ++ v'))
                (λ v' a b → base-Poly+ (v ++ v') a b)

  N∘M→N+M : Poly (PolyCommRing A' m) n → Poly A' (n +n m)
  N∘M→N+M = Poly-Rec-Set.f (PolyCommRing A' m) n (Poly A' (n +n m)) trunc
           0P
           N∘M→N+M-b
           _Poly+_
           Poly+-assoc
           Poly+-Rid
           Poly+-comm
           (λ _ → refl)
           (λ v a b → refl)

-- -----------------------------------------------------------------------------
-- -- Converse sens

  N+M→N∘M : Poly A' (n +n m) → Poly (PolyCommRing A' m) n
  N+M→N∘M = Poly-Rec-Set.f A' (n +n m) (Poly (PolyCommRing A' m) n) trunc
            0P
            (λ v a → let v , v'  = sep-vec n m v in
                      base v (base v' a))
            _Poly+_
            Poly+-assoc
            Poly+-Rid
            Poly+-comm
            (λ v → (cong (base (fst (sep-vec n m v))) (base-0P (snd (sep-vec n m v)))) ∙ (base-0P (fst (sep-vec n m v))))
            λ v a b → base-Poly+ (fst (sep-vec n m v)) (base (snd (sep-vec n m v)) a) (base (snd (sep-vec n m v)) b)
                       ∙ cong (base (fst (sep-vec n m v))) (base-Poly+ (snd (sep-vec n m v)) a b)

-----------------------------------------------------------------------------
-- Section

  e-sect : (P : Poly A' (n +n m)) → N∘M→N+M (N+M→N∘M P) ≡ P
  e-sect = Poly-Ind-Prop.f A' (n +n m)
           (λ P → N∘M→N+M (N+M→N∘M P) ≡ P)
           (λ _ → trunc _ _)
           refl
           (λ v a → cong (λ X → base X a) (sep-vec-id n m v))
           (λ {U V} ind-U ind-V → cong₂ _Poly+_ ind-U ind-V)

-----------------------------------------------------------------------------
-- Retraction

  e-retr : (P : Poly (PolyCommRing A' m) n) → N+M→N∘M (N∘M→N+M P) ≡ P
  e-retr = Poly-Ind-Prop.f (PolyCommRing A' m) n
           (λ P → N+M→N∘M (N∘M→N+M P) ≡ P)
           (λ _ → trunc _ _)
           refl
           (λ v → Poly-Ind-Prop.f A' m
                   (λ P → N+M→N∘M (N∘M→N+M (base v P)) ≡ base v P)
                   (λ _ → trunc _ _)
                   (sym (base-0P v))
                   (λ v' a → cong₂ base (sep-vec-fst n m v v') (cong (λ X → base X a) (sep-vec-snd n m v v')))
                   (λ {U V} ind-U ind-V → (cong₂ _Poly+_ ind-U ind-V) ∙ (base-Poly+ v U V)))
           (λ {U V} ind-U ind-V → cong₂ _Poly+_ ind-U ind-V )

-----------------------------------------------------------------------------
-- Morphism of ring

  map-0P : N∘M→N+M (0P) ≡ 0P
  map-0P = refl

  N∘M→N+M-gmorph : (P Q : Poly (PolyCommRing A' m) n) → N∘M→N+M ( P Poly+ Q) ≡ N∘M→N+M P Poly+ N∘M→N+M Q
  N∘M→N+M-gmorph = λ P Q → refl

  map-1P : N∘M→N+M (N∘Mr.1P) ≡ N+Mr.1P
  map-1P = cong (λ X → base X 1r) (rep-concat n m 0 )

  N∘M→N+M-rmorph : (P Q : Poly (PolyCommRing A' m) n) → N∘M→N+M ( P N∘Mr.Poly* Q) ≡ N∘M→N+M P N+Mr.Poly* N∘M→N+M Q
  N∘M→N+M-rmorph =
    -- Ind P
    Poly-Ind-Prop.f (PolyCommRing A' m) n
    (λ P → (Q : Poly (PolyCommRing A' m) n) → N∘M→N+M (P N∘Mr.Poly* Q) ≡ (N∘M→N+M P N+Mr.Poly* N∘M→N+M Q))
    (λ P p q i Q j → trunc _ _ (p Q) (q Q) i j)
    (λ Q → refl)
    (λ v → -- Ind Base P
           Poly-Ind-Prop.f A' m
           (λ P → (Q : Poly (PolyCommRing A' m) n) → N∘M→N+M (base v P N∘Mr.Poly* Q) ≡ (N∘M→N+M (base v P) N+Mr.Poly* N∘M→N+M Q))
           (λ P p q i Q j → trunc _ _ (p Q) (q Q) i j)
           (λ Q → cong (λ X → N∘M→N+M (X N∘Mr.Poly* Q)) (base-0P v))
           (λ v' a → -- Ind Q
                      Poly-Ind-Prop.f (PolyCommRing A' m) n
                      (λ Q → N∘M→N+M (base v (base v' a) N∘Mr.Poly* Q) ≡ (N∘M→N+M (base v (base v' a)) N+Mr.Poly* N∘M→N+M Q))
                      (λ _ → trunc _ _)
                      (sym (N+Mr.0PRightAnnihilatesPoly (N∘M→N+M (base v (base v' a)))))
                      (λ w → -- Ind base Q
                              Poly-Ind-Prop.f A' m
                              _
                              (λ _ → trunc _ _)
                              (sym (N+Mr.0PRightAnnihilatesPoly (N∘M→N+M (base v (base v' a)))))
                              (λ w' b → cong (λ X → base X (a · b)) (+n-vec-concat n m v w v' w'))
                              λ {U V} ind-U ind-V → cong (λ X → N∘M→N+M (base v (base v' a) N∘Mr.Poly* X)) (sym (base-Poly+ w U V))
                                                     ∙ cong₂ (_Poly+_ ) ind-U ind-V
                                                     ∙ sym (cong (λ X → N∘M→N+M (base v (base v' a)) N+Mr.Poly* N∘M→N+M X) (base-Poly+ w U V)) )
                              -- End Ind base Q
                      λ {U V} ind-U ind-V → cong₂ _Poly+_ ind-U ind-V)
                      -- End Ind Q
           λ {U V} ind-U ind-V Q → cong (λ X → N∘M→N+M (X N∘Mr.Poly* Q)) (sym (base-Poly+ v U V))
                                    ∙ cong₂ _Poly+_ (ind-U Q) (ind-V Q)
                                    ∙ sym (cong (λ X → (N∘M→N+M X) N+Mr.Poly* (N∘M→N+M Q)) (sym (base-Poly+ v U V)) ))
           -- End Ind base P
     λ {U V} ind-U ind-V Q → cong₂ _Poly+_ (ind-U Q) (ind-V Q)
     -- End Ind P

-----------------------------------------------------------------------------
-- Ring Equivalence

module _ (A' : CommRing ℓ) (n m : ℕ) where

  open Comp-Poly-nm A' n m

  CRE-PolyN∘M-PolyN+M : CommRingEquiv (PolyCommRing (PolyCommRing A' m) n) (PolyCommRing A' (n +n m))
  fst CRE-PolyN∘M-PolyN+M = isoToEquiv is
    where
    is : Iso _ _
    Iso.fun is = N∘M→N+M
    Iso.inv is = N+M→N∘M
    Iso.rightInv is = e-sect
    Iso.leftInv is = e-retr

  snd CRE-PolyN∘M-PolyN+M = makeIsRingHom map-1P N∘M→N+M-gmorph N∘M→N+M-rmorph

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
-- module directly.
------------------------------------------------------------------------

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

module Data.Star.Properties where

open import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
  public

{-# WARNING_ON_IMPORT
"Data.Star.Properties was deprecated in v0.16.
Use Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties instead."
#-}


text:
------------------------------------------------------------------------
-- The "always true" predicate, □
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Delay-monad.Sized.Always where

open import Prelude
open import Prelude.Size

open import Delay-monad.Sized
open import Delay-monad.Sized.Monad

-- The "always true" predicate, □.

mutual

  data □ {a p} {A : Size → Type a} (i : Size) (P : A ∞ → Type p) :
         Delay A ∞ → Type (a ⊔ p) where
    now   : ∀ {x} → P x → □ i P (now x)
    later : ∀ {x} → □′ i P (force x) → □ i P (later x)

  record □′ {a p} {A : Size → Type a} (i : Size) (P : A ∞ → Type p)
            (x : Delay A ∞) : Type (a ⊔ p) where
    coinductive
    field
      force : {j : Size< i} → □ j P x

open □′ public

-- □ is closed, in a certain sense, under bind.

□->>= :
  ∀ {i a b p q}
    {A : Size → Type a} {B : Size → Type b}
    {P : A ∞ → Type p} {Q : B ∞ → Type q}
    {x : Delay A ∞} {f : ∀ {i} → A i → Delay B i} →
  □ i P x → (∀ {x} → P x → □ i Q (f x)) → □ i Q (x >>= f)
□->>= (now P-x)   □-f = □-f P-x
□->>= (later □-x) □-f = later λ { .force → □->>= (force □-x) □-f }

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
open import Prelude

open import Level using (_⊔_; Lift; lift) renaming (suc to ls; zero to lz)
open import Data.String using (String)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Nat using (_≤_)

module RW.Data.RTrie.Insert
    where

  open import Relation.Binary.PropositionalEquality
    using (inspect; [_])

  open import RW.Data.RTrie.Decl
  import RW.Data.PMap (RTermᵢ ⊥) as IdxMap
  import RW.Data.PMap ℕ as ℕmap

  postulate
    trie-err : ∀{a}{A : Set a} → String → A

  open import RW.Utils.Monads
  open Monad {{...}}
  open Eq {{...}}

  I : ∀{a} → Set a → Set a
  I {a} = STₐ {lz} {a} (Σ ℕ (λ _ → Maybe ℕ))

  _<$>_ : ∀{a}{A B : Set a} → (A → B) → I A → I B
  f <$> ix = ix >>= (return ∘ f)

  --------------------
  -- Monadic boilerplate
  private
    getLbl : I (Maybe ℕ)
    getLbl = getₐ >>= return ∘ p2

    putLbl : ℕ → I Unit
    putLbl n = getₐ >>= λ x → putₐ (p1 x , just n)

    getCount : I ℕ
    getCount = p1 <$> getₐ

    putCount : ℕ → I Unit
    putCount x = getLbl >>= putₐ ∘ (_,_ x)

    ++count : I ℕ
    ++count = getCount <>= (putCount ∘ suc)

    CellCtx : Set _
    CellCtx = RTrie → Cell

    singleton : ∀{a}{A : Set a} → A → List A
    singleton x = x ∷ []

  applyBRule : Rule → ℕ → Maybe ℕ
  applyBRule (Tr m n) k with m ≟-ℕ k
  ...| yes _ = just n
  ...| no  _ = nothing
  applyBRule _ _ = nothing

  -- |Makes a new rule *without* checking anything.
  --  If the current label is nothing, returns a Gather
  --  If the current label is a (just l), return a Tr l.
  --
  --  Changes the state to the newly created label.
  makeRule : I Rule
  makeRule = getLbl
         >>= λ l → (++count <>= putLbl) -- increments the counter and set's it.
         >>= λ c′ → return $ maybe (flip Tr c′) (Gr c′) l

  -- |Given a list of rules, which arise from we reaching
  --  either a leaf node or a previously bound symbol,
  --  will apply one of such rules or create a new one.
  --
  --  In any case, this will change the current label either
  --  to a fresh one or by a transition in the list.
  handleRules : List Rule → I (List Rule)
  handleRules rs = getLbl >>= maybe (flip l≡just rs) (l≡nothing rs)
    where
      l≡just : ℕ → List Rule → I (List Rule)
      l≡just l [] = singleton <$> makeRule
      l≡just l (r ∷ rs) with applyBRule r l
      ...| just l′ = putLbl l′ >> return (r ∷ rs)
      ...| nothing = (_∷_ r) <$> l≡just l rs

      l≡nothing : List Rule → I (List Rule)
      l≡nothing [] = singleton <$> makeRule
      l≡nothing ((Gr k) ∷ rs) = putLbl k >> return ((Gr k) ∷ rs)
      l≡nothing (r ∷ rs)      = _∷_ r <$> l≡nothing rs

  -- |Given a cell and a NON-BINDING index, mIdx takes care
  --  of finding the trie we need to keep traversing and
  --  creating a reconstruction function, for when we
  --  finish modifying the mentioned trie.
  mIdx : Cell → RTermᵢ ⊥
       → I (CellCtx × RTrie)
  -- In the case we are inserting a ivarᵢ, we are going to merge the new btrie,
  -- which is going to be a leaf (TODO: why?), in the default branch.
  mIdx ((d , mh) , bs) (ivarᵢ _)
    = return $ (λ bt → (merge d bt , mh) , bs) , BTrieEmpty
    where
      merge : RTrie → RTrie → RTrie
      merge (Leaf as) (Leaf bs) = Leaf (as ++ bs)
      merge _ bt                = bt
  -- For the more general case, if tid ∉ mh, we add and entry (tid ↦ empty).
  -- After, we return mh(tid) and the context that modifies this exact entry.
  mIdx ((d , mh) , bs) tid
    = let mh′ , prf = IdxMap.alterPrf BTrieEmpty tid mh
    in return $ (λ f → (d , IdxMap.insert tid f mh) , bs)
              , (IdxMap.lkup' tid mh′ prf)

  -- |When we find a binding symbol, however, things can be a bit more tricky.
  --  This symbol is either registered, in which case we just add a fresh
  --  rule to it, or it is not registered in the map, where we add it with
  --  a fresh rule.
  mSym : Cell → ℕ
       → I (CellCtx × RTrie)
  mSym (mh , bs) tsym with ℕmap.lkup tsym bs
  ...| nothing = makeRule
             >>= λ r → return (const (mh , (tsym , r ∷ []) ∷ bs)
                              , BTrieEmpty)
  ...| just rs = handleRules rs
             >>= λ r → return (const (mh , ℕmap.insert tsym r bs)
                              , BTrieEmpty)

  -- |𝑴 chooses which traversal function to use.
  𝑴 : {A : Set}{{enA : Enum A}}
     → Cell → RTermᵢ A → I (CellCtx × RTrie)
  𝑴 {{enum aℕ _}} c tid with toSymbol tid | inspect toSymbol tid
  ...| nothing | [ prf ] = mIdx c (idx-cast tid prf)
  ...| just s  | _       = maybe (mSym c) enum-err (aℕ s)
    where postulate enum-err : I (CellCtx × RTrie)

  -- |Insertion of an (opened) term in a cell. Returns the altered cell.
  mutual
    insCell* : {A : Set}{{enA : Enum A}}
             → List (RTerm A) → List Cell → I (List Cell)
    insCell* [] _ = return []
    insCell* _ [] = return []
    insCell* (t ∷ ts) (b ∷ bs)
      = insCell (out t) b >>= λ b′ → (_∷_ b′) <$> insCell* ts bs

    -- Variation of insCell*, assuming we're always adding to empty cells.
    insCell*ε : {A : Set}{{enA : Enum A}} → List (RTerm A) → I (List Cell)
    insCell*ε [] = return []
    insCell*ε (t ∷ ts)
      = insCell (out t) ((Leaf [] , IdxMap.empty) , [])
      >>= λ b → (_∷_ b) <$> insCell*ε ts

    {-# TERMINATING #-}
    insCell : {A : Set}{{enA : Enum A}}
            → RTermᵢ A × List (RTerm A) → Cell → I Cell
    insCell (tid , tr) cell
      = 𝑴 cell tid
      >>= λ { (c , bt) → insCellAux tid tr bt >>= return ∘ c }
      where
        -- Note how if tid is a binding symbol, we don't do anything. That's
        -- because 𝑴 already took care of adding the rules in the correct place for us.
        tr≡[] : {A : Set}{{enA : Enum A}}
              → RTermᵢ A → I RTrie
        tr≡[] tid with toSymbol tid
        ...| nothing = (Leaf ∘ singleton) <$> makeRule
        ...| _       = return $ Fork []

        insCellAux : {A : Set}{{enA : Enum A}}
                   → RTermᵢ A → List (RTerm A) → RTrie
                   → I RTrie
        -- Inserting in a Leaf is impossible...
        insCellAux tid _  (Leaf r) = return (Leaf r)
        -- If we don't have recursive arguments in the term beeing inserted,
        -- we follow by tr≡[]
        insCellAux tid [] _        = tr≡[] tid
        -- Otherwise we simply add our recursive arguments.
        insCellAux tid tr (Fork [])
          = Fork <$> insCell*ε tr
        insCellAux tid tr (Fork ms)
          = Fork <$> insCell* tr ms

  -- |Insertion has to begin in a 1-cell fork.
  --  This gives some intuition that BTries should contain an arity, somewhere in their type.
  ins : {A : Set}{{enA : Enum A}} → RTerm A → RTrie → I RTrie
  ins t (Fork (cell ∷ []))
    = (Fork ∘ singleton) <$> insCell (out t) cell
  ins t (Fork [])
    = (Fork ∘ singleton) <$> insCell (out t) ((Leaf [] , IdxMap.empty) , [])
  ins t _ = trie-err "Insertion has to begin in a 1-cell fork"

  -- Interfacing
  {-# TERMINATING #-}
  insertTerm : {A : Set}{{enA : Enum A}} → Name → RTerm A → (ℕ × RTrie) → (ℕ × RTrie)
  insertTerm d term (n , Leaf r) = trie-err "Can't insert in a leaf"
  insertTerm d term (n , bt)
    = let bt′ , n′ , lbl = STₐ.run (ins term bt) (n + 1 , nothing)
      in maybe′ (λ l′ → l′ , substΣ l′ d bt′)
                (trie-err "empty final lbl")  lbl
    where
      open import Data.Maybe using (maybe′)

      -- Substitution boilerplate.

      sR : ℕ → Name → Rule → Rule
      sR k c (Tr m n) with n ≟-ℕ k
      ...| yes _ = Fr m c
      ...| no  _ = Tr m n
      sR _ _ r = r

      mutual
        sC : ℕ → Name → Cell → Cell
        sC k c ((d , mh) , bs)
          = (substΣ k c d
            , IdxMap.map (substΣ k c) mh)
          , ℕmap.map (Prelude.map (sR k c)) bs

        substΣ : ℕ → Name → RTrie → RTrie
        substΣ k c (Leaf rs) = Leaf (Prelude.map (sR k c) rs)
        substΣ k c (Fork ms) = Fork (Prelude.map (sC k c) ms)

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
-- Andreas, 2020-03-18, issue 4518, reported by strangeglyph

-- Better error message when parsing of LHS fails

open import Agda.Builtin.Nat using (Nat) -- forgot to import constructors

postulate
  foo : Nat

test : Set₁
test with foo
... | zero  = Set
... | suc n = Set

-- ERROR:
-- Could not parse the left-hand side test | suc n
-- NEW INFORMATION:
-- Problematic expression: (suc n)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

module abelian-subgroups where

import abelian-groups
import subgroups
open abelian-groups public
open subgroups public

{- Subsets of abelian groups -}

subset-Ab :
  (l : Level) {l1 : Level} (A : Ab l1) → UU ((lsuc l) ⊔ l1)
subset-Ab l A = subset-Group l (group-Ab A)

is-set-subset-Ab :
  (l : Level) {l1 : Level} (A : Ab l1) → is-set (subset-Ab l A)
is-set-subset-Ab l A = is-set-subset-Group l (group-Ab A)

{- Defining subgroups -}

contains-zero-subset-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : subset-Ab l2 A) → UU l2
contains-zero-subset-Ab A = contains-unit-subset-Group (group-Ab A)

is-prop-contains-zero-subset-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : subset-Ab l2 A) →
  is-prop (contains-zero-subset-Ab A P)
is-prop-contains-zero-subset-Ab A =
  is-prop-contains-unit-subset-Group (group-Ab A)

closed-under-add-subset-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : subset-Ab l2 A) → UU (l1 ⊔ l2)
closed-under-add-subset-Ab A =
  closed-under-mul-subset-Group (group-Ab A)

is-prop-closed-under-add-subset-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : subset-Ab l2 A) →
  is-prop (closed-under-add-subset-Ab A P)
is-prop-closed-under-add-subset-Ab A =
  is-prop-closed-under-mul-subset-Group (group-Ab A)

closed-under-neg-subset-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : subset-Ab l2 A) → UU (l1 ⊔ l2)
closed-under-neg-subset-Ab A =
  closed-under-inv-subset-Group (group-Ab A)

is-prop-closed-under-neg-subset-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : subset-Ab l2 A) →
  is-prop (closed-under-neg-subset-Ab A P)
is-prop-closed-under-neg-subset-Ab A =
  is-prop-closed-under-inv-subset-Group (group-Ab A)

is-subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : subset-Ab l2 A) → UU (l1 ⊔ l2)
is-subgroup-Ab A = is-subgroup-Group (group-Ab A)

is-prop-is-subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : subset-Ab l2 A) →
  is-prop (is-subgroup-Ab A P)
is-prop-is-subgroup-Ab A = is-prop-is-subgroup-Group (group-Ab A)

{- Introducing the type of all subgroups of a group G -}

Subgroup-Ab :
  (l : Level) {l1 : Level} (A : Ab l1) → UU ((lsuc l) ⊔ l1)
Subgroup-Ab l A = Subgroup l (group-Ab A)

subset-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) →
  ( Subgroup-Ab l2 A) → ( subset-Ab l2 A)
subset-Subgroup-Ab A = subset-Subgroup (group-Ab A)

is-emb-subset-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) → is-emb (subset-Subgroup-Ab {l2 = l2} A)
is-emb-subset-Subgroup-Ab A = is-emb-subset-Subgroup (group-Ab A)

type-subset-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  (type-Ab A → UU l2)
type-subset-Subgroup-Ab A = type-subset-Subgroup (group-Ab A)

is-prop-type-subset-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  (x : type-Ab A) → is-prop (type-subset-Subgroup-Ab A P x)
is-prop-type-subset-Subgroup-Ab A =
  is-prop-type-subset-Subgroup (group-Ab A)

is-subgroup-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  is-subgroup-Ab A (subset-Subgroup-Ab A P)
is-subgroup-Subgroup-Ab A = is-subgroup-Subgroup (group-Ab A)

contains-zero-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  contains-zero-subset-Ab A (subset-Subgroup-Ab A P)
contains-zero-Subgroup-Ab A = contains-unit-Subgroup (group-Ab A)

closed-under-add-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  closed-under-add-subset-Ab A (subset-Subgroup-Ab A P)
closed-under-add-Subgroup-Ab A = closed-under-mul-Subgroup (group-Ab A)

closed-under-neg-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  closed-under-neg-subset-Ab A (subset-Subgroup-Ab A P)
closed-under-neg-Subgroup-Ab A = closed-under-inv-Subgroup (group-Ab A)

{- Given a subgroup of an abelian group, we construct an abelian group -}

type-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) → UU (l1 ⊔ l2)
type-ab-Subgroup-Ab A =  type-group-Subgroup (group-Ab A)

incl-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  type-ab-Subgroup-Ab A P → type-Ab A
incl-ab-Subgroup-Ab A = incl-group-Subgroup (group-Ab A)

is-emb-incl-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  is-emb (incl-ab-Subgroup-Ab A P)
is-emb-incl-ab-Subgroup-Ab A = is-emb-incl-group-Subgroup (group-Ab A)

eq-subgroup-ab-eq-ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  {x y : type-ab-Subgroup-Ab A P} →
  Id (incl-ab-Subgroup-Ab A P x) (incl-ab-Subgroup-Ab A P y) → Id x y
eq-subgroup-ab-eq-ab A =
  eq-subgroup-eq-group (group-Ab A)

set-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) → Subgroup-Ab l2 A → UU-Set (l1 ⊔ l2)
set-ab-Subgroup-Ab A = set-group-Subgroup (group-Ab A)

zero-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) → type-ab-Subgroup-Ab A P
zero-ab-Subgroup-Ab A = unit-group-Subgroup (group-Ab A)

add-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  ( x y : type-ab-Subgroup-Ab A P) → type-ab-Subgroup-Ab A P
add-ab-Subgroup-Ab A = mul-group-Subgroup (group-Ab A)

neg-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  type-ab-Subgroup-Ab A P → type-ab-Subgroup-Ab A P
neg-ab-Subgroup-Ab A = inv-group-Subgroup (group-Ab A)

is-associative-add-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  ( x y z : type-ab-Subgroup-Ab A P) →
  Id (add-ab-Subgroup-Ab A P (add-ab-Subgroup-Ab A P x y) z)
     (add-ab-Subgroup-Ab A P x (add-ab-Subgroup-Ab A P y z))
is-associative-add-ab-Subgroup-Ab A =
  is-associative-mul-group-Subgroup (group-Ab A)

left-zero-law-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  ( x : type-ab-Subgroup-Ab A P) →
  Id (add-ab-Subgroup-Ab A P (zero-ab-Subgroup-Ab A P) x) x
left-zero-law-ab-Subgroup-Ab A =
  left-unit-law-group-Subgroup (group-Ab A)

right-zero-law-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  ( x : type-ab-Subgroup-Ab A P) →
  Id (add-ab-Subgroup-Ab A P x (zero-ab-Subgroup-Ab A P)) x
right-zero-law-ab-Subgroup-Ab A =
  right-unit-law-group-Subgroup (group-Ab A)

left-neg-law-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  ( x : type-ab-Subgroup-Ab A P) →
  Id ( add-ab-Subgroup-Ab A P (neg-ab-Subgroup-Ab A P x) x)
     ( zero-ab-Subgroup-Ab A P)
left-neg-law-ab-Subgroup-Ab A =
  left-inverse-law-group-Subgroup (group-Ab A)

right-neg-law-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  ( x : type-ab-Subgroup-Ab A P) →
  Id ( add-ab-Subgroup-Ab A P x (neg-ab-Subgroup-Ab A P x))
     ( zero-ab-Subgroup-Ab A P)
right-neg-law-ab-Subgroup-Ab A = right-inverse-law-group-Subgroup (group-Ab A)

is-commutative-add-ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  ( x y : type-ab-Subgroup-Ab A P) →
  Id ( add-ab-Subgroup-Ab A P x y) (add-ab-Subgroup-Ab A P y x)
is-commutative-add-ab-Subgroup-Ab A P (pair x p) (pair y q) =
  eq-subgroup-ab-eq-ab A P (is-commutative-add-Ab A x y)

ab-Subgroup-Ab :
  {l1 l2 : Level} (A : Ab l1) → Subgroup-Ab l2 A → Ab (l1 ⊔ l2)
ab-Subgroup-Ab A P =
  pair
    (group-Subgroup (group-Ab A) P) (is-commutative-add-ab-Subgroup-Ab A P)

{- We show that the inclusion from ab-Subgroup-Ab A P → A is a group
   homomorphism -}

preserves-add-incl-ab-Subgroup-Ab :
  { l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  preserves-add (ab-Subgroup-Ab A P) A (incl-ab-Subgroup-Ab A P)
preserves-add-incl-ab-Subgroup-Ab A =
  preserves-mul-incl-group-Subgroup (group-Ab A)

hom-ab-Subgroup-Ab :
  { l1 l2 : Level} (A : Ab l1) (P : Subgroup-Ab l2 A) →
  hom-Ab (ab-Subgroup-Ab A P) A
hom-ab-Subgroup-Ab A = hom-group-Subgroup (group-Ab A)

{- We define another type of subgroups of A as the type of group inclusions -}

emb-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) → UU (l1 ⊔ l2)
emb-Ab A B = emb-Group (group-Ab A) (group-Ab B)

emb-Ab-Slice :
  (l : Level) {l1 : Level} (A : Ab l1) → UU ((lsuc l) ⊔ l1)
emb-Ab-Slice l A = emb-Group-Slice l (group-Ab A)

emb-ab-slice-Subgroup-Ab :
  { l1 l2 : Level} (A : Ab l1) →
  Subgroup-Ab l2 A → emb-Ab-Slice (l1 ⊔ l2) A
emb-ab-slice-Subgroup-Ab A = emb-group-slice-Subgroup (group-Ab A)

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax Sub | S

type
  L : 0-ary
  T : 0-ary

term
  vr : L  ->  T
  sb : L.T  T  ->  T

theory
  (C) x y : T |> sb (a. x[], y[]) = x[]
  (L) x : T |> sb (a. vr(a), x[]) = x[]
  (R) a : L  x : L.T |> sb (b. x[b], vr(a[])) = x[a[]]
  (A) x : (L,L).T  y : L.T  z : T |> sb (a. sb (b. x[a,b], y[a]), z[]) = sb (b. sb (a. x[a, b], z[]), sb (a. y[a], z[]))
-}

module Sub.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import Sub.Signature

private
  variable
    Γ Δ Π : Ctx
    α : ST
    𝔛 : Familyₛ

-- Inductive term declaration
module S:Terms (𝔛 : Familyₛ) where

  data S : Familyₛ where
    var  : ℐ ⇾̣ S
    mvar : 𝔛 α Π → Sub S Π Γ → S α Γ

    vr : S L Γ → S T Γ
    sb : S T (L ∙ Γ) → S T Γ → S T Γ

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  Sᵃ : MetaAlg S
  Sᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (vrₒ ⋮ a)     → vr a
      (sbₒ ⋮ a , b) → sb a b
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module Sᵃ = MetaAlg Sᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : S ⇾̣ 𝒜
    𝕊 : Sub S Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞 (vr a)   = 𝑎𝑙𝑔 (vrₒ ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (sb a b) = 𝑎𝑙𝑔 (sbₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ Sᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ S α Γ) → 𝕤𝕖𝕞 (Sᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (vrₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (sbₒ ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ S ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : S ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ Sᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : S α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub S Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (vr a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (sb a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
S:Syn : Syntax
S:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = S:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open S:Terms 𝔛 in record
    { ⊥ = S ⋉ Sᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax S:Syn public
open S:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands Sᵃ public
open import SOAS.Metatheory S:Syn public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas