text:
open import Type
open import Logic.Classical as Logic using (Classical)
open import Logic.Predicate as Logic using ()

module Formalization.ClassicalPropositionalLogic.SequentCalculus ⦃ classical : ∀{ℓ} → Logic.∀ₗ(Classical{ℓ}) ⦄ where

import      Lvl
open import Data
open import Data.Boolean
import      Data.Boolean.Operators
open import Data.Boolean.Stmt
open import Data.Either as Either using (_‖_ ; Left ; Right)
open import Data.List
open import Data.List.Functions using () renaming (singleton to · ; _++_ to _∪_)
open import Data.List.Relation.Permutation
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
private module BoolOp = Data.Boolean.Operators.Logic
open import Functional as Fn
open import Function.Names using (_⊜_)
open import Logic
open import Logic.Propositional as Logic using (_←_)
open import Logic.Propositional.Theorems as Logic using ()
open import Logic.Predicate.Theorems as Logic using ()
open import Relator.Equals renaming (_≡_ to _≡ₑ_)
open import Relator.Equals.Proofs
open import Relator.Equals.Proofs.Equiv
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Type
open import Syntax.Implication hiding (_⇒_)
open import Type.Size.Countable

private variable ℓₚ ℓ ℓ₁ ℓ₂ : Lvl.Level

open import Formalization.ClassicalPropositionalLogic.Syntax
open import Formalization.ClassicalPropositionalLogic.Syntax.Proofs
open import Formalization.ClassicalPropositionalLogic.Semantics
open import Formalization.ClassicalPropositionalLogic.Semantics.Proofs
import      Formalization.ClassicalPropositionalLogic.TruthTable as TruthTable

_∪·_ : ∀{T : Type{ℓ}} → List(T) → T → List(T)
_∪·_ = Fn.swap(_⊰_)
infixl 1000 _∪·_

module _ {ℓₚ} {P : Type{ℓₚ}} where
  private variable Γ Γ₁ Γ₂ Γ₃ Δ Δ₁ Δ₂ Δ₃ : List(Formula(P))
  private variable φ φ₁ φ₂ ψ A B C : Formula(P)
  private variable p : P

  data _⇒_ : List(Formula(P)) → List(Formula(P)) → Stmt{Lvl.𝐒(ℓₚ)} where
    axiom : ((·(• p)) ⇒ (·(• p)))

    weakenₗ : (Γ ⇒ Δ) → ((Γ ∪· A) ⇒ Δ)
    permuteₗ : .(Γ₁ permutes Γ₂) → (Γ₁ ⇒ Δ) → (Γ₂ ⇒ Δ)
    contractₗ : ((Γ ∪· A ∪· A) ⇒ Δ) → ((Γ ∪· A) ⇒ Δ)
    ⊥ₗ : (Γ ∪· ⊥) ⇒ ∅
    ∧ₗₗ : ((Γ ∪· A) ⇒ Δ) → ((Γ ∪· (A ∧ B)) ⇒ Δ)
    ∧ₗᵣ : ((Γ ∪· B) ⇒ Δ) → ((Γ ∪· (A ∧ B)) ⇒ Δ)
    ∨ₗ : ((Γ ∪· A) ⇒ Δ) → ((Γ ∪· B) ⇒ Δ) → ((Γ ∪· (A ∨ B)) ⇒ Δ)
    ⟶ₗ : (Γ ⇒ (Δ ∪· A)) → ((Γ ∪· B) ⇒ Δ) → ((Γ ∪· (A ⟶ B)) ⇒ Δ)
    ¬ₗ : (Γ ⇒ (Δ ∪· A)) → ((Γ ∪· (¬ A)) ⇒ Δ)

    weakenᵣ : (Γ ⇒ Δ) → (Γ ⇒ (Δ ∪· A))
    permuteᵣ : .(Δ₁ permutes Δ₂) → (Γ ⇒ Δ₁) → (Γ ⇒ Δ₂)
    contractᵣ : (Γ ⇒ (Δ ∪· A ∪· A)) → (Γ ⇒ (Δ ∪· A))
    ⊤ᵣ : ∅ ⇒ (Δ ∪· ⊤)
    ∧ᵣ : (Γ ⇒ (Δ ∪· A)) → (Γ ⇒ (Δ ∪· B)) → (Γ ⇒ (Δ ∪· (A ∧ B)))
    ∨ᵣₗ : (Γ ⇒ (Δ ∪· A)) → (Γ ⇒ (Δ ∪· (A ∨ B)))
    ∨ᵣᵣ : (Γ ⇒ (Δ ∪· B)) → (Γ ⇒ (Δ ∪· (A ∨ B)))
    ⟶ᵣ : ((Γ ∪· A) ⇒ (Δ ∪· B)) → (Γ ⇒ (Δ ∪· (A ⟶ B)))
    ¬ᵣ : ((Γ ∪· A) ⇒ Δ) → (Γ ⇒ (Δ ∪· (¬ A)))

  permute : .(Γ₁ permutes Γ₂) → .(Δ₁ permutes Δ₂) → (Γ₁ ⇒ Δ₁) → (Γ₂ ⇒ Δ₂)
  permute permΓ permΔ ΓΔ = permuteₗ permΓ (permuteᵣ permΔ ΓΔ)

  open import Data.List.Equiv.Id
  open import Data.List.Relation.Membership
  open import Data.List.Proofs
  open import Structure.Operator.Properties

  refl : (· A) ⇒ (· A)
  refl {• x} = axiom
  refl {⊤} = weakenₗ ⊤ᵣ
  refl {⊥} = weakenᵣ ⊥ₗ
  refl {¬ A} = ¬ᵣ (permuteₗ(_permutes_.swap) (¬ₗ refl))
  refl {A ∧ B} = ∧ᵣ (∧ₗₗ refl) (∧ₗᵣ refl)
  refl {A ∨ B} = ∨ₗ (∨ᵣₗ refl) (∨ᵣᵣ refl)
  refl {A ⟶ B} = ⟶ᵣ (permuteₗ(_permutes_.swap) (⟶ₗ (permuteᵣ(_permutes_.swap) (weakenᵣ refl)) (permuteₗ(_permutes_.swap) (weakenₗ refl))))
  refl {A ⟷ B} = {!!}

  --[⇒]-trans : (Γ₁ ⇒ Γ₂) → (Γ₂ ⇒ Γ₃) → (Γ₁ ⇒ Γ₃)
  --[⇒]-trans p12 p23 = {!-c -t 10!}

  [⇒][++]ᵣ-weakenₗ : (Γ₂ ⇒ Δ) → ((Γ₁ ∪ Γ₂) ⇒ Δ)
  [⇒][++]ᵣ-weakenₗ {Γ₁ = ∅}       p = p
  [⇒][++]ᵣ-weakenₗ {Γ₁ = φ₁ ⊰ Γ₁} p = weakenₗ([⇒][++]ᵣ-weakenₗ {Γ₁ = Γ₁} p)

  [⇒][++]ₗ-weakenₗ : (Γ₁ ⇒ Δ) → ((Γ₁ ∪ Γ₂) ⇒ Δ)
  [⇒][++]ₗ-weakenₗ {Γ₁ = Γ₁}{Δ = Δ}{Γ₂ = Γ₂} Γ₁Δ = permuteₗ (sub₂(_≡ₑ_)(_permutes_) (commutativity(_∪_) ⦃ {!!} ⦄ {Γ₂}{Γ₁})) ([⇒][++]ᵣ-weakenₗ {Γ₁ = Γ₂} Γ₁Δ)

  [⇒][++]-weakenᵣ : (Γ ⇒ Δ₂) → (Γ ⇒ (Δ₁ ∪ Δ₂))
  [⇒][++]-weakenᵣ {Δ₁ = ∅}       p = p
  [⇒][++]-weakenᵣ {Δ₁ = φ₁ ⊰ Δ₁} p = weakenᵣ([⇒][++]-weakenᵣ {Δ₁ = Δ₁} p)

  [⇒][⊥]-arbitrary : ((Γ ∪· ⊥) ⇒ Δ)
  [⇒][⊥]-arbitrary {Γ = Γ}{Δ = Δ} = permuteᵣ (sub₂(_≡ₑ_)(_permutes_) (identityᵣ(_∪_)(∅))) ([⇒][++]-weakenᵣ{Δ₂ = ∅}{Δ} ⊥ₗ)

  [⇒]-nonempty-reflexivity : ((φ ⊰ Γ) ⇒ (φ ⊰ Γ))
  [⇒]-nonempty-reflexivity {Γ = ∅}     = refl
  [⇒]-nonempty-reflexivity {Γ = φ ⊰ Γ} = weakenₗ (weakenᵣ ([⇒]-nonempty-reflexivity {Γ = Γ}))

  {- TODO: Maybe not
  [⇒]-symmetric-by-side : ((Γ₁ ⇒ Δ) → (Γ₂ ⇒ Δ)) → ((Δ ⇒ Γ₂) → (Δ ⇒ Γ₁))
  [⇒]-symmetric-by-side p axiom = {!!}
  [⇒]-symmetric-by-side p (weakenₗ q) = {!!}
  [⇒]-symmetric-by-side p (permuteₗ x q) = {!!}
  [⇒]-symmetric-by-side p (contractₗ q) = {!!}
  [⇒]-symmetric-by-side p ⊥ₗ = [⇒][⊥]-arbitrary
  [⇒]-symmetric-by-side p (∧ₗₗ q) = {!!}
  [⇒]-symmetric-by-side p (∧ₗᵣ q) = {!!}
  [⇒]-symmetric-by-side p (∨ₗ q q₁) = {!!}
  [⇒]-symmetric-by-side p (⟶ₗ q q₁) = {!!}
  [⇒]-symmetric-by-side p (weakenᵣ q) = {!!}
  [⇒]-symmetric-by-side p (permuteᵣ x q) = {!!}
  [⇒]-symmetric-by-side p (contractᵣ q) = [⇒]-symmetric-by-side (weakenₗ ∘ p) q
  [⇒]-symmetric-by-side p (∧ᵣ q q₁) = {!!}
  [⇒]-symmetric-by-side p (∨ᵣₗ q) = {!!}
  [⇒]-symmetric-by-side p (∨ᵣᵣ q) = {!!}
  [⇒]-symmetric-by-side p (⟶ᵣ q) = {!!}
  -}

  open import Structure.Function

  [⇒]-super : ((Γ₁ ∪· φ₁) ⊇ (Γ₂ ∪· φ₂)) → ((Γ₁ ∪· φ₁) ⇒ (Γ₂ ∪· φ₂))
  [⇒]-super {Γ₁ = Γ₁}      {Γ₂ = φ₂ ⊰ Γ₂}    p = weakenᵣ ([⇒]-super {Γ₁ = Γ₁} {Γ₂ = Γ₂} (p ∘ skip))
  [⇒]-super {Γ₁ = ∅}       {Γ₂ = ∅}          p with use [≡]-intro ← p (use [≡]-intro) = refl
  [⇒]-super {Γ₁ = φ₁ ⊰ Γ₁} {Γ₂ = ∅}{φ₂ = φ₂} p with p (use [≡]-intro)
  ... | use [≡]-intro = permuteₗ Proofs.postpend-prepend-permutes (permuteₗ(sub₂(_≡ₑ_)(_permutes_) (symmetry(_≡ₑ_) (congruence₁(φ₁ ⊰_) (postpend-[++] {a = φ₂}{l = Γ₁})))) (weakenₗ ([⇒][++]ᵣ-weakenₗ{Γ₁ = Γ₁} refl)))
  ... | skip q = weakenₗ([⇒]-super {Γ₁ = Γ₁} {Γ₂ = ∅} \{(use [≡]-intro) → q ; (skip ())})

  [⇒]-membership : (φ ∈ Γ) → (Γ ⇒ (· φ))
  [⇒]-membership (use [≡]-intro) = [⇒][++]ₗ-weakenₗ refl
  [⇒]-membership (skip p) = weakenₗ([⇒]-membership p)

  Inconsistent : List(Formula(P)) → Type
  Inconsistent(Γ) = Γ ⇒ ∅

  test : ∅ ⇒ ·((A ∧ B) ⟶ A)
  test {A = A}{B = B} =
    refl                ⇒-start
    ((· A) ⇒ (· A))      ⇒-[ ∧ₗₗ ]
    (·(A ∧ B) ⇒ (· A))   ⇒-[ ⟶ᵣ ]
    (∅ ⇒ ·((A ∧ B) ⟶ A)) ⇒-end

  --test2 : ∅ ⇒ ·(A ∨ (¬ A))

  test3 : ∅ ⇒ ·(((¬ ¬ A) ⟶ (¬ ¬ B)) ⟶ (¬ ¬(A ⟶ B)))
  test3{A = A}{B = B} =
    • (
      refl                                     ⇒-start
      ((· A)                  ⇒ (· A))          ⇒-[ weakenᵣ ]
      ((· A)                  ⇒ ((· A) ∪· B))   ⇒-[ permuteᵣ _permutes_.swap ]
      ((· A)                  ⇒ ((· B) ∪· A))   ⇒-[ ¬ₗ ]
      (((· A) ∪· (¬ A))       ⇒ (· B))          ⇒-[ permuteₗ _permutes_.swap ]
      ((·(¬ A) ∪· A)          ⇒ (· B))          ⇒-[ ⟶ᵣ ]
      (·(¬ A)                 ⇒ ·(A ⟶ B))       ⇒-[ ¬ₗ ]
      ((·(¬ A) ∪· ¬(A ⟶ B))   ⇒ ∅)              ⇒-[ permuteₗ _permutes_.swap ]
      ((·(¬(A ⟶ B)) ∪· (¬ A)) ⇒ ∅)              ⇒-[ ¬ᵣ ]
      (·(¬(A ⟶ B))            ⇒ (∅ ∪· (¬ ¬ A))) ⇒-end
    )
    • (
      refl ⇒-start
      ((· B)                    ⇒ (· B))    ⇒-[ weakenₗ ]
      (((· B) ∪· A)             ⇒ (· B))    ⇒-[ ⟶ᵣ ]
      ((· B)                    ⇒ ·(A ⟶ B)) ⇒-[ ¬ₗ ]
      (((· B) ∪· ¬(A ⟶ B))      ⇒ ∅)        ⇒-[ permuteₗ _permutes_.swap ]
      ((·(¬(A ⟶ B)) ∪· B)       ⇒ ∅)        ⇒-[ ¬ᵣ ]
      (·(¬(A ⟶ B))              ⇒ ·(¬ B))   ⇒-[ ¬ₗ ]
      ((·(¬(A ⟶ B)) ∪· (¬ ¬ B)) ⇒ ∅)        ⇒-end
    )
    ⇒₂-[ ⟶ₗ ]
    ((·(¬(A ⟶ B)) ∪· ((¬ ¬ A) ⟶ (¬ ¬ B))) ⇒ ∅)                                     ⇒-[ permuteₗ _permutes_.swap ]
    ((·((¬ ¬ A) ⟶ (¬ ¬ B)) ∪· ¬(A ⟶ B))   ⇒ ∅)                                     ⇒-[ ¬ᵣ ]
    (·((¬ ¬ A) ⟶ (¬ ¬ B))                 ⇒ ·(¬ ¬(A ⟶ B)))                         ⇒-[ ⟶ᵣ ]
    (∅                                    ⇒ ·(((¬ ¬ A) ⟶ (¬ ¬ B)) ⟶ (¬ ¬(A ⟶ B)))) ⇒-end

  test4 : (∅ ⇒ ·(((A ⟶ B) ⟶ A) ⟶ A))
  test4 {A = A}{B = B} =
    • (
      refl ⇒-start
      ((· A) ⇒ (· A))              ⇒-[ weakenᵣ ]
      ((· A) ⇒ ((· A) ∪· B))       ⇒-[ ⟶ᵣ ]
      (∅     ⇒ ((· A) ∪· (A ⟶ B))) ⇒-end
    )
    • ((· A) ⇒ (· A))              :-[ refl ]
    ⇒₂-[ ⟶ₗ ]
    ((∅ ∪· ((A ⟶ B) ⟶ A)) ⇒ (∅ ∪· A))             ⇒-[ ⟶ᵣ ]
    (∅                    ⇒ ·(((A ⟶ B) ⟶ A) ⟶ A)) ⇒-end

  -- ⟶ᵣ (¬ᵣ (permuteₗ _permutes_.swap (⟶ₗ (¬ᵣ (permuteₗ _permutes_.swap (¬ₗ (⟶ᵣ (permuteₗ _permutes_.swap (¬ₗ (permuteᵣ _permutes_.swap (weakenᵣ axiom)))))))) (¬ₗ (¬ᵣ (permuteₗ _permutes_.swap (¬ₗ (⟶ᵣ (weakenₗ axiom)))))))))

  {-
  [∧]-intro : ((Γ ∪· A ∪· B) ⇒ (Γ ∪· (A ∧ B)))
  [∧]-intro = ∧ᵣ ([⇒]-super skip) ([⇒]-super (p ↦ {!!}))

  [∧]-elimₗ : ((Γ ∪· (A ∧ B)) ⇒ (Γ ∪· A))
  [∧]-elimₗ = {!!}
  -}

  {-
  test : (Γ ⇒ Δ₁) → .(Δ₁ permutes Δ₂) → (Δ₂ ⇒ Δ₃) → (Γ ⇒ Δ₃)

  [∧]-intro : (Γ ⇒ ·(A)) → (Γ ⇒ ·(B)) → (Γ ⇒ ·(A ∧ B))
  [∧]-intro = ∧ᵣ

  [∧]-elimₗ : (Γ ⇒ Δ ∪· (A ∧ B)) → (Γ ⇒ (Δ ∪· A))
  [∧]-elimₗ axiom = ∧ₗₗ axiom
  [∧]-elimₗ (weakenₗ p) = weakenₗ ([∧]-elimₗ p)
  [∧]-elimₗ (permuteₗ x p) = permuteₗ x ([∧]-elimₗ p)
  [∧]-elimₗ (contractₗ p) = contractₗ ([∧]-elimₗ p)
  [∧]-elimₗ (∧ₗₗ p) = ∧ₗₗ ([∧]-elimₗ p)
  [∧]-elimₗ (∧ₗᵣ p) = ∧ₗᵣ ([∧]-elimₗ p)
  [∧]-elimₗ (∨ₗ p q) = ∨ₗ ([∧]-elimₗ p) ([∧]-elimₗ q)
  [∧]-elimₗ (⟶ₗ p q) = ⟶ₗ (permuteᵣ _permutes_.swap ([∧]-elimₗ(permuteᵣ _permutes_.swap p))) ([∧]-elimₗ q)
  [∧]-elimₗ (weakenᵣ p) = weakenᵣ p
  [∧]-elimₗ (permuteᵣ x p) = test p x {!!}
  [∧]-elimₗ (contractᵣ p) = contractᵣ([∧]-elimₗ(permuteᵣ _permutes_.swap ([∧]-elimₗ p)))
  [∧]-elimₗ (∧ᵣ p q) = p
  -}

  {-
  soundness : (Γ ⇒ Δ) → ((_∈ Γ) ⊨₊ (_∈ Δ))
  soundness axiom          𝔐Γ = 𝔐Γ
  soundness (weakenₗ p)    𝔐Γ = soundness p (𝔐Γ ∘ skip)
  soundness (permuteₗ x p) 𝔐Γ = {!!}
  soundness (contractₗ p)  𝔐Γ = {!!}
  soundness ⊥ₗ             𝔐Γ ()
  soundness (∧ₗₗ p) 𝔐Γ {elem} (use [≡]-intro) = soundness p (q ↦ 𝔐Γ {!!}) (use [≡]-intro)
  -- 𝔐Γ{elem} {!soundness p ? ?!}
  -- soundness p {!!} (use {!!})
  soundness (∧ₗₗ p) 𝔐Γ (skip q) = {!!}
  soundness (∧ₗᵣ p)        𝔐Γ = {!!}
  soundness (∨ₗ p q)       𝔐Γ = {!!}
  soundness (⟶ₗ p q)       𝔐Γ = soundness p (𝔐Γ ∘ skip) ∘ skip
  soundness (weakenᵣ p)    𝔐Γ = {!!}
  soundness (permuteᵣ x p) 𝔐Γ = {!!}
  soundness (contractᵣ p)  𝔐Γ = soundness p 𝔐Γ ∘ skip
  soundness (∧ᵣ p q)       𝔐Γ = {!!}
  soundness (∨ᵣₗ p)        𝔐Γ = {!!}
  soundness (∨ᵣᵣ p)        𝔐Γ = {!!}
  soundness (⟶ᵣ p)         𝔐Γ = {!!}
  -}

{-
  excluded-middle : Γ ⇒ (Δ ∪ ·(A ∨ (¬ A)))
  excluded-middle = ∨ᵣₗ {!!}

  soundness : (Γ ⇒ Δ) → (Γ ⊨₊ Δ)
  soundness axiom = id
  soundness (weakenₗ p) 𝔐Γ = soundness p (𝔐Γ ∘ Left)
  soundness (∧ₗₗ p) 𝔐Γ e = soundness p (\{(Left Γelem) → 𝔐Γ(Left Γelem) ; (Right [≡]-intro) → 𝔐Γ (Right {!!})}) e
  soundness (∧ₗᵣ p) 𝔐Γ e = soundness p (\{(Left Γelem) → 𝔐Γ (Left Γelem) ; (Right [≡]-intro) → 𝔐Γ (Right {!!})}) e
  soundness (∨ₗ p q) 𝔐Γ e = soundness p (\{(Left r) → 𝔐Γ (Left r) ; (Right r) → {!!}}) e
  soundness (⟶ₗ p q) 𝔐Γ = soundness p (𝔐Γ ∘ Left) ∘ Left
  soundness (weakenᵣ p) 𝔐Γ (Left Δelem)      = soundness p 𝔐Γ Δelem
  soundness (weakenᵣ p) 𝔐Γ (Right [≡]-intro) = {!!}
  soundness (∧ᵣ p q) 𝔐Γ (Left Δelem)      = soundness p 𝔐Γ (Left Δelem)
  soundness (∧ᵣ p q) 𝔐Γ (Right [≡]-intro) = Logic.[∧]-intro (soundness p 𝔐Γ (Right [≡]-intro)) (soundness q 𝔐Γ (Right [≡]-intro))
  soundness (∨ᵣₗ p) 𝔐Γ e = {!!}
  soundness (∨ᵣᵣ p) 𝔐Γ e = {!!}
  soundness (⟶ᵣ p) 𝔐Γ (Left x) = {!!}
  soundness (⟶ᵣ p) 𝔐Γ (Right [≡]-intro) = {!soundness p ? ?!}
-}

  module _ (cut : ∀{Γ₁ Γ₂ Δ₁ Δ₂}{φ} → (Γ₁ ⇒ (Δ₁ ∪· φ)) → ((Γ₂ ∪· φ) ⇒ Δ₂) → ((Γ₁ ∪ Γ₂) ⇒ (Δ₁ ∪ Δ₂))) where
    open import Formalization.ClassicalPropositionalLogic.NaturalDeduction

    open import Data.List.Relation.Quantification
    open import Lang.Instance
    open import Sets.PredicateSet as PredSet using (PredSet)
    open import Sets.PredicateSet.Listable
    open import Type.Properties.MereProposition

    ¬ᵣ-⊥ : ((Γ ∪· A) ⇒ (· ⊥)) → (Γ ⇒ (Δ ∪· (¬ A)))
    ¬ᵣ-⊥ {Γ = Γ}{A = A}{Δ = Δ} p = permute{Γ₁ = Γ ∪ Γ}{Γ₂ = Γ} {!!} {!!} (cut{Γ₁ = Γ}{Γ₂ = Γ}{Δ₁ = Δ}{Δ₂ = ·(¬ A)} {!!} {!!})

    from-naturalDeduction : ∀{Γ} ⦃ _ : Listable{ℓ}(Γ) ⦄ → (Γ ⊢ φ) → (list(Γ) ⇒ (· φ))
    to-naturalDeduction : (Γ ⇒ (· φ)) → ((_∈ Γ) ⊢ φ)

    from-naturalDeduction (direct x) = [⇒]-membership(Listable.proof infer x)
    from-naturalDeduction [⊤]-intro          = [⇒][++]ₗ-weakenₗ ⊤ᵣ
    from-naturalDeduction ([⊥]-intro  p q)   = {!!}
    from-naturalDeduction ([⊥]-elim   p)     = {!from-naturalDeduction p!}
    from-naturalDeduction {Γ = Γ} ([¬]-intro  p)     = {!(permuteₗ (list-[∪·] {Γ = Γ}) (from-naturalDeduction ⦃ ? ⦄ p))!}
    from-naturalDeduction ([¬]-elim   p)     = {!!}
    from-naturalDeduction ([∧]-intro  p q)   = ∧ᵣ (from-naturalDeduction p) (from-naturalDeduction q)
    from-naturalDeduction ([∧]-elimₗ  p)     = permute permₗ permᵣ (cut (from-naturalDeduction p) (∧ₗₗ refl)) where
      permₗ = sub₂(_≡ₑ_)(_permutes_) (identityᵣ(_∪_)(∅))
      permᵣ = sub₂(_≡ₑ_)(_permutes_) (identityₗ(_∪_)(∅))
    from-naturalDeduction ([∧]-elimᵣ  p)     = permute permₗ permᵣ (cut (from-naturalDeduction p) (∧ₗᵣ refl)) where
      permₗ = sub₂(_≡ₑ_)(_permutes_) (identityᵣ(_∪_)(∅))
      permᵣ = sub₂(_≡ₑ_)(_permutes_) (identityₗ(_∪_)(∅))
    from-naturalDeduction ([∨]-introₗ p)     = ∨ᵣₗ (from-naturalDeduction p)
    from-naturalDeduction ([∨]-introᵣ p)     = ∨ᵣᵣ (from-naturalDeduction p)
    from-naturalDeduction ([∨]-elim   p q r) = {!!}
    from-naturalDeduction {Γ = Γ} ([⟶]-intro  p)     = ⟶ᵣ (permuteₗ (list-[∪·] {S = Γ}) (from-naturalDeduction ⦃ {!!} ⦄ p))
    from-naturalDeduction ([⟶]-elim   p q)   = {!!} -- permute {!!} {!!} (cut (from-naturalDeduction p) {!cut (from-naturalDeduction q) ?!})
    from-naturalDeduction ([⟷]-intro  p q)   = {!!}
    from-naturalDeduction ([⟷]-elimₗ  p q)   = {!!}
    from-naturalDeduction ([⟷]-elimᵣ  p q)   = {!!}

    {-
    from-naturalDeduction : ((_∈ Γ) ⊢ φ) → (Γ ⇒ (· φ))
    from-naturalDeduction (direct (use {x = x}{l = l} [≡]-intro)) = [⇒][++]ₗ-weakenₗ {Γ₁ = · x}{Γ₂ = l} axiom
    from-naturalDeduction (direct (skip x)) = weakenₗ(from-naturalDeduction (direct x))
    from-naturalDeduction [⊤]-intro = [⇒][++]ₗ-weakenₗ ⊤ᵣ
    from-naturalDeduction ([⊥]-intro p q) = {!!}
    from-naturalDeduction ([⊥]-elim p) = {!!}
    from-naturalDeduction ([¬]-intro p) = {!!}
    from-naturalDeduction ([¬]-elim p) = {!!}
    from-naturalDeduction ([∧]-intro p q) = ∧ᵣ (from-naturalDeduction p) (from-naturalDeduction q)
    from-naturalDeduction ([∧]-elimₗ p) = permute permₗ permᵣ (cut (from-naturalDeduction p) (∧ₗₗ axiom)) where
      permₗ = sub₂(_≡ₑ_)(_permutes_) (identityᵣ(_∪_)(∅))
      permᵣ = sub₂(_≡ₑ_)(_permutes_) (identityₗ(_∪_)(∅))
    from-naturalDeduction ([∧]-elimᵣ p) = permute permₗ permᵣ (cut (from-naturalDeduction p) (∧ₗᵣ axiom)) where
      permₗ = sub₂(_≡ₑ_)(_permutes_) (identityᵣ(_∪_)(∅))
      permᵣ = sub₂(_≡ₑ_)(_permutes_) (identityₗ(_∪_)(∅))
    from-naturalDeduction ([∨]-introₗ p) = ∨ᵣₗ (from-naturalDeduction p)
    from-naturalDeduction ([∨]-introᵣ p) = ∨ᵣᵣ (from-naturalDeduction p)
    from-naturalDeduction ([∨]-elim p q r) = {!!}
    from-naturalDeduction ([⟶]-intro p) = ⟶ᵣ {!from-naturalDeduction p!}
    from-naturalDeduction ([⟶]-elim p q) = {!!}
    from-naturalDeduction ([⟷]-intro p q) = {!!}
    from-naturalDeduction ([⟷]-elimₗ p q) = {!!}
    from-naturalDeduction ([⟷]-elimᵣ p q) = {!!}
    -}

{-    to-naturalDeduction axiom = direct (use [≡]-intro)
    to-naturalDeduction (weakenₗ p) = {!!}
    to-naturalDeduction (permuteₗ x p) = {!!}
    to-naturalDeduction (contractₗ p) = {!!}
    to-naturalDeduction (∧ₗₗ p) = {!!}
    to-naturalDeduction (∧ₗᵣ p) = {!!}
    to-naturalDeduction (∨ₗ p p₁) = {!!}
    to-naturalDeduction (⟶ₗ p p₁) = {!!}
    to-naturalDeduction (weakenᵣ p) = {!!}
    to-naturalDeduction (permuteᵣ x p) = {!!}
    to-naturalDeduction (contractᵣ p) = {!!}
    to-naturalDeduction (∧ᵣ p p₁) = [∧]-intro (to-naturalDeduction p) (to-naturalDeduction p₁)
    to-naturalDeduction (∨ᵣₗ p) = [∨]-introₗ (to-naturalDeduction p)
    to-naturalDeduction (∨ᵣᵣ p) = [∨]-introᵣ (to-naturalDeduction p)
    to-naturalDeduction (⟶ᵣ p) = [⟶]-intro {!to-naturalDeduction p!}
-}

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:
open import Prelude

module Bij where
  record bij (From To : Set) : Set where
    field
      convert : From → To
      inj     : ∀{f1 f2} → convert f1 == convert f2 → f1 == f2
      surj    : (t : To) → Σ[ f ∈ From ] (convert f == t)

  convert-inv : ∀{F T : Set} {{bijFT : bij F T}} → T → F
  convert-inv {{bijFT}} t with bij.surj bijFT t
  ... | f , _ = f

  convert-inv-inj : ∀{F T : Set} {{bijFT : bij F T}} {t1 t2 : T} →
                      convert-inv {{bijFT}} t1 == convert-inv {{bijFT}} t2 →
                      t1 == t2
  convert-inv-inj ⦃ bijFT = bijFT ⦄ {t1} {t2} eq
    with bij.surj bijFT t1 | bij.surj bijFT t2
  ... | _ , p1 | _ , p2
    rewrite eq = ! p1 · p2

  convert-inv-surj : ∀{F T : Set} {{bijFT : bij F T}} (f : F) →
                       Σ[ t ∈ T ] (convert-inv {{bijFT}} t == f)
  convert-inv-surj ⦃ bijFT = bijFT ⦄ f with expr-eq (λ _ → bij.convert bijFT f)
  ... | t , teq with expr-eq (λ _ → bij.surj bijFT t)
  ... | (_ , seq) , refl = _ , bij.inj bijFT (seq · teq)

  convert-bij1 : ∀{F T : Set} {{bijFT : bij F T}} {f : F} →
                   convert-inv (bij.convert bijFT f) == f
  convert-bij1 ⦃ bijFT = bijFT ⦄ {f} with expr-eq (λ _ → convert-inv-surj f)
  ... | (_ , eq) , refl = eq

  convert-bij2 : ∀{F T : Set} {{bijFT : bij F T}} {t : T} →
                   bij.convert bijFT (convert-inv t) == t
  convert-bij2 ⦃ bijFT = bijFT ⦄ {t} with expr-eq (λ _ → bij.surj bijFT t)
  ... | (_ , eq) , refl = eq

ext: agda

max_stars_repo_name: nickcollins/dependent-dicts-agda

max_issues_repo_name: nickcollins/dependent-dicts-agda

max_forks_repo_name: nickcollins/dependent-dicts-agda


text:
module Control.Monad.Identity where

open import Prelude
open import Container.Foldable
open import Container.Traversable

record Identity {a} (A : Set a) : Set a where
  constructor mkIdentity
  field
    runIdentity : A

open Identity public

instance
  FunctorId : ∀ {a} → Functor (Identity {a})
  runIdentity (fmap {{FunctorId}} f m) = f (runIdentity m)

  ApplicativeId : ∀ {a} → Applicative (Identity {a})
  runIdentity (pure {{ApplicativeId}} x) = x
  runIdentity (_<*>_ {{ApplicativeId}} mf mx) = runIdentity mf (runIdentity mx)

  MonadId : ∀ {a} → Monad (Identity {a})
  _>>=_ {{MonadId}} m f = f (runIdentity m)

  FunctorId′ : ∀ {a b} → Functor′ {a} {b} Identity
  runIdentity (fmap′ {{FunctorId′}} f m) = f (runIdentity m)

  ApplicativeId′ : ∀ {a b} → Applicative′ {a} {b} Identity
  runIdentity (_<*>′_ {{ApplicativeId′}} mf mx) = runIdentity mf (runIdentity mx)

  MonadId′ : ∀ {a b} → Monad′ {a} {b} Identity
  _>>=′_ {{MonadId′}} m f = f (runIdentity m)

  FoldableId : ∀ {a w} → Foldable {w = w} (Identity {a})
  foldMap {{FoldableId}} f m = f (runIdentity m)

  TraversableId : ∀ {a} → Traversable (Identity {a})
  traverse {{TraversableId}} f m = pure mkIdentity <*> f (runIdentity m)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


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

module Extensions.Fin.TypedSubstitution where

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

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

-- Abstract typing contexts over T-types.
--
-- A typing context Ctx n maps n free variables to types containing up
-- to n free variables each.
module Context where

  infixr 5 _∷_

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

  -- Operations on context that require weakening of types.
  record WeakenOps (T : ℕ → Set) : Set where

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

    infixr 5 _i∷_

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

    -- Shorthand for extending contexts with variables that are typed
    -- independently of themselves.
    _i∷_ : ∀ {n} → T n → Ctx T n → Ctx T (1 + n)
    a i∷ Γ = weaken a ∷ Γ

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

open Context

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

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

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

  infix 4 _⊢_∈_

  field
    _⊢_∈_ : Typing Tp₂ Tm Tp₁   -- the associated typing

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

    -- Operations on the (source) Tp₁-context.
    weakenOps : WeakenOps Tp₁

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

  infix 4 _⇒_⊢_

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

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

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

  field

    -- Weakens well-typed Ts.
    weaken : ∀ {n} {Δ : Ctx Tp₂ n} {t a b} → Δ ⊢ t ∈ a →
             b ∷ Δ ⊢ S.weaken t ∈ C.weaken a

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

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

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

  infixr 5 _/∷_ _/i∷_

  -- Extension.
  _/∷_ : ∀ {m n} {Γ : Ctx Tp₁ m} {Δ : Ctx Tp₂ n} {t a b σ} →
         b ∷ Δ ⊢ t ∈ a / (t S./∷ σ) → Γ ⇒ Δ ⊢ σ → a ∷ Γ ⇒ b ∷ Δ ⊢ (t S./∷ σ)
  t∈a/t∷σ /∷ σ-wt =
    t∈a/t∷σ ∷ gmap₂ (subst (_⊢_∈_ _ _) (weaken-/ _) ∘ weaken) σ-wt

  -- A variant of extension tailored to _i∷_.
  _/i∷_ : ∀ {m n} {Γ : Ctx Tp₁ m} {Δ : Ctx Tp₂ n} {t a b σ} →
          b ∷ Δ ⊢ t ∈ C.weaken (a / σ) → Γ ⇒ Δ ⊢ σ → a i∷ Γ ⇒ b ∷ Δ ⊢ (t S./∷ σ)
  t∈a/σ /i∷ σ-wt =
    (subst (_⊢_∈_ _ _) (weaken-/ _) t∈a/σ) /∷ σ-wt

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

  field extensionTyped : ExtensionTyped simple typedSub

  open TypedSub typedSub
  open ExtensionTyped extensionTyped public
  private
    module S  = SimpleExt simple
    module L₀ = Lemmas₀ (record { simple = simple })
    module C  = WeakenOps weakenOps
  open C using (_i∷_)

  field

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

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

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

  infix 10 _↑ _↑i

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

  -- A variant of lifting tailored to _i∷_.
  _↑i : ∀ {m n} {Γ : Ctx Tp m} {Δ : Ctx Tp n} {σ} → Γ ⇒ Δ ⊢ σ → ∀ {a} →
        a i∷ Γ ⇒ a / σ i∷ Δ ⊢ σ S.↑
  σ-wt ↑i = var zero /i∷ σ-wt

  -- The identity substitution.
  id : ∀ {n} {Γ : Ctx Tp n} → Γ ⇒ Γ ⊢ S.id
  id {zero}          = []
  id {suc n} {a ∷ Γ} =
    subst₂ (λ Δ σ → a ∷ Γ ⇒ Δ ⊢ σ)
           (cong (flip _∷_ Γ) (id-vanishes a)) (L₀.id-↑⋆ 1) (id ↑)
    where
      id-vanishes′ : ∀ {n} (a : Tp (1 + n)) → a / S.id S.↑ ≡ a
      id-vanishes′ a = begin
        a / S.id S.↑  ≡⟨ cong (_/_ a) (L₀.id-↑⋆ 1) ⟩
        a / S.id      ≡⟨ id-vanishes a ⟩
        a             ∎

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

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

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

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

  -- A variant of single-variable substitution that handles
  -- self-dependently typed variables.
  sub′ : ∀ {n} {Γ : Ctx Tp n} {t a} → Γ ⊢ t ∈ a / S.sub t →
         a ∷ Γ ⇒ Γ ⊢ S.sub t
  sub′ t∈a[/t] = t∈a[/t] ∷ gmap₂₂ (subst (_⊢_∈_ _ _) id-wk-sub-vanishes) id

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

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

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

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

  open SimpleTyped simpleTyped public

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

-- Abstract variable typings.
module VarTyping {Tp} (weakenOps : Context.WeakenOps Tp) where
  open WeakenOps weakenOps

  infix 4 _⊢Var_∈_

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

-- Abstract typed variable substitutions (α-renamings).
record TypedVarSubst (Tp : ℕ → Set) : Set where
  field
    application : Application Tp Fin
    weakenOps   : WeakenOps Tp

  open VarTyping weakenOps public

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

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

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

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

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

  open ExtAppLemmas appLemmas hiding (var; weaken; /-wk; id-vanishes; subst)

  -- Extensions of renamings.
  extensionTyped : ExtensionTyped VarLemmas.simple typedSub
  extensionTyped = record
    { weaken          = weaken
    ; wk-commutes     = wk-commutes
    ; /-wk            = /-wk
    }
    where
      open Applicative.Morphism using (op-<$>)

      weaken : ∀ {n} {Γ : Ctx Tp n} {x a b} → Γ ⊢Var x ∈ a →
               b ∷ Γ ⊢Var suc x ∈ C.weaken a
      weaken (var x) =
        subst (_⊢Var_∈_ _ _) (op-<$> (lookup-morphism x) _ _) (var (suc x))

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

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

-- Context-replacing substitutions.
record ContextSub (Tp₁ Tp₂ Tm : ℕ → Set) : Set₁ where
  infix 4 _⊢_∈_

  field
    _⊢_∈_ : Typing Tp₂ Tm Tp₁   -- the associated typing

    -- Simple Tm-substitutions (e.g. id).
    simple : Simple Tm

    -- Operations on the (source) Tp₁-context.
    weakenOps : WeakenOps Tp₁

  open Simple    simple    using (id)
  open WeakenOps weakenOps using (toVec)

  infix 4 _⇒_⊢-id

  -- Context-replacing substitutions.
  --
  -- An alternative representation for substitutions that only change
  -- the context of a well-typed Tm-term, i.e. where the underlying
  -- untyped substitution is the identity.
  _⇒_⊢-id : ∀ {n} → Ctx Tp₁ n → Ctx Tp₂ n → Set
  Γ ⇒ Δ ⊢-id = All₂ (λ t a → Δ ⊢ t ∈ a) id (toVec Γ)

-- Equivalences between (simple) typed substitutions and their
-- context-replacing counterparts.
record Equivalence {Tp₁ Tp₂ Tm} (simple : Simple Tm)
                   (typedSub : TypedSub Tp₁ Tp₂ Tm) : Set where

  open Simple     simple
  open TypedSub   typedSub

  -- The type of context substitutions participating in this
  -- equivalence.
  contextSub : ContextSub Tp₁ Tp₂ Tm
  contextSub = record
    { _⊢_∈_     = _⊢_∈_
    ; simple    = simple
    ; weakenOps = weakenOps
    }

  open ContextSub contextSub hiding (_⊢_∈_; simple)

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

  -- There is a context substitution for every typed identity
  -- substitution.
  sound : ∀ {n} {Γ : Ctx Tp₁ n} {Δ : Ctx Tp₂ n} → Γ ⇒ Δ ⊢-id → Γ ⇒ Δ ⊢ id
  sound ρ = map₂ (subst (_⊢_∈_ _ _) (sym (id-vanishes _))) ρ

  -- There is a context substitution for every typed identity
  -- substitution.
  complete : ∀ {n} {Γ : Ctx Tp₁ n} {Δ : Ctx Tp₂ n} → Γ ⇒ Δ ⊢ id → Γ ⇒ Δ ⊢-id
  complete σ-wt = map₂ (subst (_⊢_∈_ _ _) (id-vanishes _)) σ-wt

-- Variants of some simple typed substitutions.
record ContextSimple {Tp Tm} (simple : Simple Tm)
                     (typedSub : TypedSub Tp Tp Tm) : Set where

  field simpleTyped : SimpleTyped simple typedSub

  open TypedSub typedSub hiding (_⊢_∈_)
  private
    module U = SimpleExt simple
    module C = WeakenOps weakenOps
    module S = SimpleTyped simpleTyped
  open C using (_i∷_)

  equivalence : Equivalence simple typedSub
  equivalence = record { id-vanishes = S.id-vanishes }

  open Equivalence equivalence public
  open ContextSub  contextSub  public

  infixr 5 _/∷_
  infix 10 _↑

  -- Extension.
  _/∷_ : ∀ {n} {Γ : Ctx Tp n} {Δ : Ctx Tp n} {a b} →
         b ∷ Δ ⊢ U.var zero ∈ a → Γ ⇒ Δ ⊢-id → a ∷ Γ ⇒ b ∷ Δ ⊢-id
  z∈a /∷ σ-wt = z∈a ∷ gmap₂ S.weaken σ-wt

  -- Lifting.
  _↑ : ∀ {n} {Γ : Ctx Tp n} {Δ : Ctx Tp n} → Γ ⇒ Δ ⊢-id → ∀ {a} →
       a ∷ Γ ⇒ a ∷ Δ ⊢-id
  ρ ↑ = S.var zero /∷ ρ

  -- The identity substitution.
  id : ∀ {n} {Γ : Ctx Tp n} → Γ ⇒ Γ ⊢-id
  id = complete S.id


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed applicative functors
------------------------------------------------------------------------

-- Note that currently the applicative functor laws are not included
-- here.

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

module Category.Applicative.Indexed where

open import Category.Functor using (RawFunctor)
open import Data.Product using (_×_; _,_)
open import Function
open import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_)

private
  variable
    a b c i f : Level
    A : Set a
    B : Set b
    C : Set c

IFun : Set i → (ℓ : Level) → Set (i ⊔ suc ℓ)
IFun I ℓ = I → I → Set ℓ → Set ℓ

------------------------------------------------------------------------
-- Type, and usual combinators

record RawIApplicative {I : Set i} (F : IFun I f) :
                       Set (i ⊔ suc f) where
  infixl 4 _⊛_ _<⊛_ _⊛>_
  infix  4 _⊗_

  field
    pure : ∀ {i} → A → F i i A
    _⊛_  : ∀ {i j k} → F i j (A → B) → F j k A → F i k B

  rawFunctor : ∀ {i j} → RawFunctor (F i j)
  rawFunctor = record
    { _<$>_ = λ g x → pure g ⊛ x
    }

  private
    open module RF {i j : I} =
           RawFunctor (rawFunctor {i = i} {j = j})
           public

  _<⊛_ : ∀ {i j k} → F i j A → F j k B → F i k A
  x <⊛ y = const <$> x ⊛ y

  _⊛>_ : ∀ {i j k} → F i j A → F j k B → F i k B
  x ⊛> y = flip const <$> x ⊛ y

  _⊗_ : ∀ {i j k} → F i j A → F j k B → F i k (A × B)
  x ⊗ y = (_,_) <$> x ⊛ y

  zipWith : ∀ {i j k} → (A → B → C) → F i j A → F j k B → F i k C
  zipWith f x y = f <$> x ⊛ y

  zip : ∀ {i j k} → F i j A → F j k B → F i k (A × B)
  zip = zipWith _,_

------------------------------------------------------------------------
-- Applicative with a zero

record RawIApplicativeZero
       {I : Set i} (F : IFun I f) :
       Set (i ⊔ suc f) where
  field
    applicative : RawIApplicative F
    ∅           : ∀ {i j} → F i j A

  open RawIApplicative applicative public

------------------------------------------------------------------------
-- Alternative functors: `F i j A` is a monoid

record RawIAlternative
       {I : Set i} (F : IFun I f) :
       Set (i ⊔ suc f) where
  infixr 3 _∣_
  field
    applicativeZero : RawIApplicativeZero F
    _∣_             : ∀ {i j} → F i j A → F i j A → F i j A

  open RawIApplicativeZero applicativeZero public

------------------------------------------------------------------------
-- Applicative functor morphisms, specialised to propositional
-- equality.

record Morphism {I : Set i} {F₁ F₂ : IFun I f}
                (A₁ : RawIApplicative F₁)
                (A₂ : RawIApplicative F₂) : Set (i ⊔ suc f) where
  module A₁ = RawIApplicative A₁
  module A₂ = RawIApplicative A₂
  field
    op      : ∀ {i j} → F₁ i j A → F₂ i j A
    op-pure : ∀ {i} (x : A) → op (A₁.pure {i = i} x) ≡ A₂.pure x
    op-⊛    : ∀ {i j k} (f : F₁ i j (A → B)) (x : F₁ j k A) →
              op (f A₁.⊛ x) ≡ (op f A₂.⊛ op x)

  op-<$> : ∀ {i j} (f : A → B) (x : F₁ i j A) →
           op (f A₁.<$> x) ≡ (f A₂.<$> op x)
  op-<$> f x = begin
    op (A₁._⊛_ (A₁.pure f) x)       ≡⟨ op-⊛ _ _ ⟩
    A₂._⊛_ (op (A₁.pure f)) (op x)  ≡⟨ P.cong₂ A₂._⊛_ (op-pure _) P.refl ⟩
    A₂._⊛_ (A₂.pure f) (op x)       ∎
    where open P.≡-Reasoning


text:
import Fragment.Algebra.Algebra
import Fragment.Algebra.Free
import Fragment.Algebra.Free.Atoms
import Fragment.Algebra.Free.Base
import Fragment.Algebra.Free.Evaluation
import Fragment.Algebra.Free.Monad
import Fragment.Algebra.Free.Properties
import Fragment.Algebra.Free.Syntax
import Fragment.Algebra.Homomorphism
import Fragment.Algebra.Homomorphism.Base
import Fragment.Algebra.Homomorphism.Definitions
import Fragment.Algebra.Homomorphism.Equivalence
import Fragment.Algebra.Homomorphism.Properties
import Fragment.Algebra.Homomorphism.Setoid
import Fragment.Algebra.Properties
import Fragment.Algebra.Quotient
import Fragment.Algebra.Signature
import Fragment.Equational.Coproduct
import Fragment.Equational.FreeExtension
import Fragment.Equational.FreeExtension.Base
import Fragment.Equational.FreeExtension.Properties
import Fragment.Equational.FreeExtension.Synthetic
import Fragment.Equational.Model
import Fragment.Equational.Model.Base
import Fragment.Equational.Model.Properties
import Fragment.Equational.Model.Satisfaction
import Fragment.Equational.Model.Synthetic
import Fragment.Equational.Structures
import Fragment.Equational.Theory
import Fragment.Equational.Theory.Base
import Fragment.Equational.Theory.Bundles
import Fragment.Equational.Theory.Combinators
import Fragment.Equational.Theory.Laws
import Fragment.Examples.CSemigroup.Arith.Atomic
import Fragment.Examples.CSemigroup.Arith.Base
import Fragment.Examples.CSemigroup.Arith.Functions
import Fragment.Examples.CSemigroup.Arith.Reasoning
import Fragment.Examples.CSemigroup.Types
import Fragment.Examples.Semigroup.Arith.Atomic
import Fragment.Examples.Semigroup.Arith.Base
import Fragment.Examples.Semigroup.Arith.Functions
import Fragment.Examples.Semigroup.Arith.Reasoning
import Fragment.Examples.Semigroup.Types
import Fragment.Extensions.CSemigroup
import Fragment.Extensions.CSemigroup.Base
import Fragment.Extensions.CSemigroup.Monomial
import Fragment.Extensions.CSemigroup.Nat
-- import Fragment.Extensions.Combinators
import Fragment.Extensions.Semigroup
import Fragment.Prelude
import Fragment.Setoid.Morphism
import Fragment.Setoid.Morphism.Base
import Fragment.Setoid.Morphism.Properties
import Fragment.Setoid.Morphism.Setoid
import Fragment.Tactic.Fragment
import Fragment.Tactic.Utils

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.List

data Singleton : List Bool → Set where
  singleton : ∀ b → Singleton (b ∷ [])

Works : (bs : List Bool) → Singleton bs → Set₁
Works bs s with s
... | singleton b with Set
Works .(b ∷ []) s | singleton b | _ = Set

Fails : (bs : List Bool) → Singleton bs → Set₁
Fails bs        s with singleton b ← s with Set
Fails .(b ∷ []) s | _ = Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Level
open import Categories.Category using (Category; _[_,_])

-- Various conclusions that can be drawn from Yoneda
-- over a particular Category C
module Categories.Yoneda.Properties {o ℓ e : Level} (C : Category o ℓ e) where

open import Function.Base using (_$_)
open import Function.Bundles using (Inverse)
open import Function.Equality using (Π; _⟨$⟩_; cong)
open import Relation.Binary.Bundles using (module Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidR
open import Data.Product using (_,_; Σ)

open import Categories.Category.Product
open import Categories.Category.Construction.Presheaves
open import Categories.Category.Construction.Functors
open import Categories.Category.Instance.Setoids
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties using (Full; Faithful; FullyFaithful)
open import Categories.Functor.Hom using (module Hom; Hom[_][-,_]; Hom[_][-,-])
open import Categories.Functor.Bifunctor
open import Categories.Functor.Presheaf
open import Categories.Functor.Construction.LiftSetoids
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
open import Categories.Yoneda

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
import Categories.NaturalTransformation.Hom as NT-Hom

open Category C using (module HomReasoning; id; _∘_; identityˡ; identityʳ; Obj; ∘-resp-≈ˡ; ∘-resp-≈ʳ)
open HomReasoning
open NaturalTransformation using (η; commute)
open Yoneda C using (embed; yoneda-inverse; module yoneda)
private
  module CE = Category.Equiv C using (refl)
  module C = Category C using (op; id)

YoFull : Full embed
YoFull {X} {Y} = record
  { from             = record { _⟨$⟩_ = λ ε → η ε X ⟨$⟩ id ; cong = λ i≈j → i≈j CE.refl }
  ; right-inverse-of = λ ε {x} {z} {y} z≈y →
    begin
      (η ε X ⟨$⟩ id) ∘ z      ≈˘⟨ identityˡ ⟩
      id ∘ (η ε X ⟨$⟩ id) ∘ z ≈˘⟨ commute ε z CE.refl ⟩
      η ε x ⟨$⟩ id ∘ id ∘ z   ≈⟨ cong (η ε x) (identityˡ ○ identityˡ ○ z≈y) ⟩
      η ε x ⟨$⟩ y             ∎
  }

YoFaithful : Faithful embed
YoFaithful f g pres-≈ = begin
  f      ≈˘⟨ identityʳ ⟩
  f ∘ id ≈⟨ pres-≈ CE.refl ⟩
  g ∘ id ≈⟨ identityʳ ⟩
  g      ∎

YoFullyFaithful : FullyFaithful embed
YoFullyFaithful = YoFull , YoFaithful

open Mor C using (_≅_)

yoneda-iso : ∀ {A B : Obj} → NaturalIsomorphism Hom[ C ][-, A ] Hom[ C ][-, B ] → A ≅ B
yoneda-iso {A} {B} niso = record
  { from = ⇒.η A ⟨$⟩ id
  ; to   = ⇐.η B ⟨$⟩ id
  ; iso  = record
    { isoˡ = begin
      (⇐.η B ⟨$⟩ id) ∘ (⇒.η A ⟨$⟩ id)      ≈˘⟨ identityˡ ⟩
      id ∘ (⇐.η B ⟨$⟩ id) ∘ (⇒.η A ⟨$⟩ id) ≈⟨  B⇒A.inverseʳ F⇐G CE.refl  ⟩
      ⇐.η A ⟨$⟩ (⇒.η A ⟨$⟩ id)             ≈⟨ isoX.isoˡ CE.refl ⟩
      id                                   ∎
    ; isoʳ = begin
      (⇒.η A ⟨$⟩ id) ∘ (⇐.η B ⟨$⟩ id)      ≈˘⟨ identityˡ ⟩
      id ∘ (⇒.η A ⟨$⟩ id) ∘ (⇐.η B ⟨$⟩ id) ≈⟨  A⇒B.inverseʳ F⇒G CE.refl ⟩
      ⇒.η B ⟨$⟩ (⇐.η B ⟨$⟩ id)             ≈⟨ isoX.isoʳ CE.refl ⟩
      id                                   ∎
    }
  }
  where
  open NaturalIsomorphism niso
  A⇒B = yoneda-inverse A (Functor.F₀ embed B)
  B⇒A = yoneda-inverse B (Functor.F₀ embed A)
  module A⇒B = Inverse A⇒B using (inverseʳ)
  module B⇒A = Inverse B⇒A using (inverseʳ)
  module isoX {X} = Mor.Iso (iso X) using (isoʳ; isoˡ)

module _ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} where
  private
    module D = Category D using (id)

    module _ {F G : Functor D C} where
      private
        module F = Functor F using (₀; ₁; identity)
        module G = Functor G using (₀; ₁; identity)
        Hom[-,F-] : Bifunctor C.op D (Setoids ℓ e)
        Hom[-,F-] = Hom[ C ][-,-] ∘F (idF ⁂ F)

        Hom[-,G-] : Bifunctor C.op D (Setoids ℓ e)
        Hom[-,G-] = Hom[ C ][-,-] ∘F (idF ⁂ G)

      nat-appʳ : ∀ X → NaturalTransformation Hom[-,F-] Hom[-,G-] →
                       NaturalTransformation Hom[ C ][-, F.₀ X ] Hom[ C ][-, G.₀ X ]
      nat-appʳ X α = ntHelper record
        { η       = λ Y → η α (Y , X)
        ; commute = λ {_ Y} f eq → cong (η α (Y , X)) (∘-resp-≈ˡ (⟺ F.identity)) ○ commute α (f , D.id) eq ○ ∘-resp-≈ˡ G.identity
        }

      transform : NaturalTransformation Hom[-,F-] Hom[-,G-] → NaturalTransformation F G
      transform α = ntHelper record
        { η       = λ X → η α (F.₀ X , X) ⟨$⟩ id
        ; commute = λ {X Y} f → begin
          (η α (F.₀ Y , Y) ⟨$⟩ id) ∘ F.₁ f       ≈˘⟨ identityˡ ⟩
          id ∘ (η α (F.₀ Y , Y) ⟨$⟩ id) ∘ F.₁ f  ≈˘⟨ lower (yoneda.⇒.commute {Y = Hom[ C ][-, G.₀ Y ] , _} (idN , F.₁ f) {nat-appʳ Y α} {nat-appʳ Y α} (cong (η α _))) ⟩
          η α (F.₀ X , Y) ⟨$⟩ F.₁ f ∘ id         ≈⟨ cong (η α (F.₀ X , Y)) (∘-resp-≈ʳ (⟺ identityˡ)) ⟩
          η α (F.₀ X , Y) ⟨$⟩ F.₁ f ∘ id ∘ id    ≈⟨ commute α (id , f) CE.refl ⟩
          G.₁ f ∘ (η α (F.₀ X , X) ⟨$⟩ id) ∘ id  ≈⟨ refl⟩∘⟨ identityʳ ⟩
          G.₁ f ∘ (η α (F.₀ X , X) ⟨$⟩ id)      ∎
        }

  module _ (F G : Functor D C) where
    private
      module F = Functor F using (₀)
      module G = Functor G using (₀)
      Hom[-,F-] : Bifunctor C.op D (Setoids ℓ e)
      Hom[-,F-] = Hom[ C ][-,-] ∘F (idF ⁂ F)

      Hom[-,G-] : Bifunctor C.op D (Setoids ℓ e)
      Hom[-,G-] = Hom[ C ][-,-] ∘F (idF ⁂ G)

    -- The implicits given below are sometimes needed (yellow), sometimes make an enormous difference in
    -- typechecking time. For example, in yoneda.⇒.commute, "nat-appʳ X F⇐G" is needed, while
    -- nat-appʳ {F = G} {F} X F⇐G makes a huge difference in checking time.
    yoneda-NI : NaturalIsomorphism Hom[-,F-] Hom[-,G-] → NaturalIsomorphism F G
    yoneda-NI ni = record
      { F⇒G = transform F⇒G
      ; F⇐G = transform F⇐G
      ; iso = λ X → record
        { isoˡ = begin
          (⇐.η (G.₀ X , X) ⟨$⟩ id) ∘ (⇒.η (F.₀ X , X) ⟨$⟩ id)      ≈⟨ introˡ CE.refl ⟩
          id ∘ (⇐.η (G.₀ X , X) ⟨$⟩ id) ∘ (⇒.η (F.₀ X , X) ⟨$⟩ id) ≈˘⟨ lower {e} (yoneda.⇒.commute {Y = Hom[ C ][-, F.₀ X ] , _}
                                                                                (idN , (⇒.η (F.₀ X , X) ⟨$⟩ id))
                                                                                {nat-appʳ {F = G} {F} X F⇐G}
                                                                                {nat-appʳ {F = G} {F} X F⇐G}
                                                                                (cong (⇐.η (_ , X) ))) ⟩
          ⇐.η (F.₀ X , X) ⟨$⟩ (⇒.η (F.₀ X , X) ⟨$⟩ id) ∘ id        ≈⟨ cong (⇐.η _) identityʳ ⟩
          ⇐.η (F.₀ X , X) ⟨$⟩ (⇒.η (F.₀ X , X) ⟨$⟩ id)             ≈⟨ iso.isoˡ _ CE.refl ⟩
          id                                                  ∎
        ; isoʳ = begin
          (⇒.η (F.₀ X , X) ⟨$⟩ id) ∘ (⇐.η (G.₀ X , X) ⟨$⟩ id)      ≈⟨ introˡ CE.refl ⟩
          id ∘ (⇒.η (F.₀ X , X) ⟨$⟩ id) ∘ (⇐.η (G.₀ X , X) ⟨$⟩ id) ≈˘⟨ lower {e} (yoneda.⇒.commute {Y = Hom[ C ][-, G.₀ X ] , _}
                                                                                (idN , (⇐.η (G.₀ X , X) ⟨$⟩ C.id))
                                                                                {nat-appʳ {F = F} {G} X F⇒G}
                                                                                {nat-appʳ {F = F} {G} X F⇒G}
                                                                                (cong (⇒.η _))) ⟩
          ⇒.η (G.₀ X , X) ⟨$⟩ (⇐.η (G.₀ X , X) ⟨$⟩ id) ∘ id        ≈⟨ cong (⇒.η _) identityʳ ⟩
          ⇒.η (G.₀ X , X) ⟨$⟩ (⇐.η (G.₀ X , X) ⟨$⟩ id)             ≈⟨ iso.isoʳ _ CE.refl ⟩
          id                                                      ∎
        }
      }
      where
      open NaturalIsomorphism ni using (F⇒G; F⇐G; module ⇐; module ⇒; module iso)
      open MR C using (introˡ)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import Categories.Category using (Category; module Commutation)
open import Categories.Category.Cartesian using (Cartesian)

-- Defines the following properties of a Category:
-- Cartesian.SymmetricMonoidal
--    a Cartesian category is Symmetric Monoidal if its induced monoidal structure is symmetric

module Categories.Category.Cartesian.SymmetricMonoidal {o ℓ e} (𝒞 : Category o ℓ e) (cartesian : Cartesian 𝒞) where

open import Data.Product using (_,_)

open Category 𝒞
open Commutation 𝒞
open HomReasoning

open import Categories.Category.BinaryProducts 𝒞 using (module BinaryProducts)
open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
open import Categories.Category.Monoidal using (Monoidal)
import Categories.Category.Monoidal.Symmetric as Sym

open import Categories.NaturalTransformation using (ntHelper)

private
  variable
    W X Y Z : Obj

open Cartesian cartesian using (products)
open CartesianMonoidal cartesian using (monoidal)
open Sym monoidal using (Symmetric; symmetricHelper)
open Monoidal monoidal using (_⊗₀_; _⊗₁_; module associator)
open BinaryProducts products

private
  B : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X
  B = swap

hexagon : [ (X ⊗₀ Y) ⊗₀ Z ⇒ Y ⊗₀ Z ⊗₀ X ]⟨
            B  ⊗₁ id                    ⇒⟨ (Y ⊗₀ X) ⊗₀ Z ⟩
            associator.from             ⇒⟨ Y ⊗₀ X ⊗₀ Z ⟩
            id ⊗₁ B
          ≈ associator.from             ⇒⟨ X ⊗₀ Y ⊗₀ Z ⟩
            B                           ⇒⟨ (Y ⊗₀ Z) ⊗₀ X ⟩
            associator.from
          ⟩
hexagon = begin
      id ⊗₁ swap ∘ assocˡ ∘ swap ⊗₁ id                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟩
      id ⊗₁ swap ∘ assocˡ ∘ ⟨ ⟨ π₂ ∘ π₁ , π₁ ∘ π₁ ⟩ , id ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟩
      id ⊗₁ swap ∘ ⟨ π₂ ∘ π₁ , ⟨ π₁ ∘ π₁ , id ∘ π₂ ⟩ ⟩          ≈⟨ ⁂∘⟨⟩ ⟩
      ⟨ id ∘ π₂ ∘ π₁ , swap ∘ ⟨ π₁ ∘ π₁ , id ∘ π₂ ⟩ ⟩           ≈⟨ ⟨⟩-cong₂ identityˡ swap∘⟨⟩ ⟩
      ⟨ π₂ ∘ π₁ , ⟨ id ∘ π₂ , π₁ ∘ π₁ ⟩ ⟩                       ≈⟨ ⟨⟩-congˡ (⟨⟩-congʳ identityˡ) ⟩
      ⟨ π₂ ∘ π₁ , ⟨ π₂ , π₁ ∘ π₁ ⟩ ⟩                            ≈˘⟨ assocˡ∘⟨⟩ ⟩
      assocˡ ∘ ⟨ ⟨ π₂ ∘ π₁ , π₂ ⟩ , π₁ ∘ π₁ ⟩                   ≈˘⟨ refl⟩∘⟨ swap∘⟨⟩ ⟩
      assocˡ ∘ swap ∘ assocˡ                                    ∎

symmetric : Symmetric
symmetric = symmetricHelper record
  { braiding    = record
    { F⇒G = ntHelper record
      { η       = λ _ → swap
      ; commute = λ _ → swap∘⁂
      }
    ; F⇐G = ntHelper record
      { η       = λ _ → swap
      ; commute = λ _ → swap∘⁂
      }
    ; iso = λ _ → record
      { isoˡ = swap∘swap
      ; isoʳ = swap∘swap
      }
    }
  ; commutative = swap∘swap
  ; hexagon     = hexagon
  }


text:
module plfa-exercises.Practice4 where

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_ ; ∃-syntax; ∃; _,_) -- renaming (_,_ to ⟨_,_⟩)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; _≤?_; _≟_; s≤s; z≤n)
open import Data.Nat.Binary.Properties using (≰⇒>)
open import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total)
open import Data.Maybe using (Maybe; just; nothing; maybe; _>>=_; from-just; From-just)
open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not)
open import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness; from-yes; From-yes)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Unit using (⊤; tt)

--data OrderedTree (A : Set) : (smallest middle biggest : ℕ) → Set where
--  leaf : ∀ (n : ℕ) → A → OrderedTree A n n
--  node : ∀ {s₁ m₁ b₁ s₂ m₂ b₂ : ℕ}
--       → (m : ℕ)
--       → b₁ ≤ m
--       → m ≤ s₂
--       → OrderedTree A s₁ m₁ b₁
--       → OrderedTree A s₂ m₂ b₂
--       → OrderedTree A s₁ m b₂
--
---- node 7 _ _ (leaf 5 300) (leaf 10 200)
----middle_values_in_node_are_smaller :
--
--insert_left : ∀ {s m b : ℕ} → (n : ℕ) → A → OrderedTree A s m b

data BST : ℕ → ℕ → Set where
  leaf : ∀ {l u : ℕ} → l ≤ u → BST l u
  node : ∀ {l l₀ u₁ u : ℕ} (d : ℕ)
       → BST l₀ d
       → BST d  u₁
       → l  ≤ l₀ -- This overcomplicates some stuff in later code. Better get rid off it
       → u₁ ≤ u
       → BST l u

-- node {l = 0} {u = 30} 5 (leaf {2} {5} _) (leaf {5} {6} _)

-- If we use the long definition of BST this function gets short, otherwise it's quite complicated
widen : ∀ {l l' u u' : ℕ}
      → BST l' u'
      → l ≤ l'
      → u' ≤ u
      → BST l u
widen (leaf l'≤u') l≤l' u'≤u = leaf (≤-trans l≤l' (≤-trans l'≤u' u'≤u))
widen (node d left right l'≤l₀ u₁≤u') l≤l' u'≤u = node d left right (≤-trans l≤l' l'≤l₀) (≤-trans u₁≤u' u'≤u)

-- node {l = 0} {u = 30} 5 (leaf {2} {5} _) (widen (leaf {23} {29} _) _ _) z≤n _

a-tree : BST 0 30 -- A tree with a single node!!
--a-tree = node 5 (leaf 2≤5) (leaf 5≤30) z≤n 30≤30
a-tree = node 5 (leaf 2≤5) (widen (leaf 23≤29) 5≤23 29≤30) z≤n 30≤30
--a-tree = node {l = 0} {u = 30} 5 (leaf {2} {5} 2≤5) (widen (leaf {23} {29} 23≤29) 5≤23 29≤30) z≤n 30≤30
  where
    --2≤5   = toWitness {Q =  2 ≤?  5} tt
    2≤5   = from-yes ( 2 ≤?  5)
    23≤29 = from-yes (23 ≤? 29)
    5≤23  = from-yes ( 5 ≤? 23)
    29≤30 = from-yes (29 ≤? 30)
    30≤30 = from-yes (30 ≤? 30)

binary-search : ∀ {l u : ℕ} → (n : ℕ) → l ≤ n → n ≤ u → BST l u → Maybe (∃[ l' ] (∃[ u' ] (BST l' u')))
binary-search _ _ _ (leaf _) = nothing
binary-search n l≤n n≤u (node {l'} {l₀} {u₁} {u'} d left right l'≤l₀ u₁≤u') with d ≟ n
--binary-search n _ _ (node {_} {l} {_} {u} d left right l≤l₀ u₁≤u) with d ≟ n
...             | yes d=n = just (l' , u' , node d left right l'≤l₀ u₁≤u')
...             | no  d≠n  with ≤-total n d | l₀ ≤? n | n ≤? u₁
...                           | inj₁ n≤d | yes l₀≤n | _         = binary-search n l₀≤n n≤d left
...                           | inj₁ n≤d | no ¬l₀≤n | _         = nothing -- This shouldn't exist if the definition of BST wasn't so overcomcomplicated
...                           | inj₂ d≤n | _        | yes n≤u₁  = binary-search n d≤n n≤u₁ right
...                           | inj₂ d≤n | _        | no ¬n≤u₁  = nothing

smaller : ℕ → ℕ → Bool
smaller m n with m ≤? n
...            | yes m≤n = true
...            | _       = false

_≤ℕ_ : ∀ (m n : ℕ) → From-yes (m ≤? n)
m ≤ℕ n = from-yes (m ≤? n)

--_ : Maybe (∃ (λ l' → ∃ (BST l')))
--_ = binary-search 5 _ _ a-tree ≡ nothing
  --where
    --5≤30 = from-yes (5 ≤? 30)
_ : binary-search 2 z≤n (2 ≤ℕ 30) a-tree ≡ nothing
_ = refl

_ : binary-search 5 z≤n (5 ≤ℕ 30) a-tree ≡ just (0 , 30 , node 5 _ _ _ _)
_ = refl

insert : ∀ {l u} (d : ℕ) → l ≤ d → d ≤ u → BST l u → BST l u
insert d l≤d d≤u (leaf _) = node d (leaf l≤d) (leaf d≤u) ≤-refl ≤-refl
insert d l≤d d≤u (node {_} {l₀} m left right l≤m m≤u) with ≤-total m d
...                | inj₁ m≤d = node m (insert d ? ? left) right l≤m m≤u -- This shouldn't exist if the definition of BST wasn't so overcomcomplicated
...                | inj₂ d≤m = ?

-- ≰⇒> ¬3≤4


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Translation between different formalisations of syntax.

module BasicIS4.Syntax.Translation where

open import BasicIS4.Syntax.Common public

import BasicIS4.Syntax.ClosedHilbertSequential as CHS
import BasicIS4.Syntax.ClosedHilbert as CH
import BasicIS4.Syntax.HilbertSequential as HS
import BasicIS4.Syntax.Hilbert as H
import BasicIS4.Syntax.Gentzen as G
import BasicIS4.Syntax.DyadicHilbertSequential as DHS
import BasicIS4.Syntax.DyadicHilbert as DH
import BasicIS4.Syntax.DyadicGentzen as DG
import BasicIS4.Syntax.LabelledGentzen as LG

open HS using () renaming (_⊦⊢_ to HS⟨_⊦⊢_⟩ ; _⊢_ to HS⟨_⊢_⟩) public
open H using () renaming (_⊢_ to H⟨_⊢_⟩ ; _⊢⋆_ to H⟨_⊢⋆_⟩) public
open G using () renaming (_⊢_ to G⟨_⊢_⟩ ; _⊢⋆_ to G⟨_⊢⋆_⟩) public
open DHS using () renaming (_⊦⊢_ to DHS⟨_⊦⊢_⟩ ; _⊢_ to DHS⟨_⊢_⟩) public
open DH using () renaming (_⊢_ to DH⟨_⊢_⟩) public
open DG using () renaming (_⊢_ to DG⟨_⊢_⟩ ; _⊢⋆_ to DG⟨_⊢⋆_⟩) public
open LG using (_↝_ ; _◎_ ; _◎⋆_) renaming (_⊢_ to LG⟨_⊢_⟩ ; _⊢⋆_ to LG⟨_⊢⋆_⟩) public

-- Available translations.
--
--       ┌─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┐
--       │ CHS │ CH  │ HS  │ H   │ G   │ DHS │ DH  │ DG  │ LG  │
-- ┌─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┤
-- │ CHS │     │ d   │ d   │ ∘   │ ∘   │ ∘   │ ∘   │ ∘   │ ∘   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┤
-- │ CH  │ d   │     │ ∘   │ d   │ ∘   │ ∘   │ ∘   │ ∘   │ ∘   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┤
-- │ HS  │ d   │ ∘   │     │ d   │ ∘   │ d   │ ∘   │ ∘   │ ∘   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┤
-- │ H   │ ∘   │ d   │ d   │     │ d   │ ∘   │ d   │ ∘   │ ∘   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┤
-- │ G   │ ∘   │ ∘   │ ∘   │ d   │     │ ∘   │ ∘   │ d   │ d   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┤
-- │ DHS │ ∘   │ ∘   │ d   │ ∘   │ ∘   │     │ d   │ ∘   │ ∘   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┤
-- │ DH  │ ∘   │ ∘   │ ∘   │ d   │ ∘   │ d   │     │ d   │ ∘   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┤
-- │ DG  │ ∘   │ ∘   │ ∘   │ ∘   │ ∘!  │ ∘   │ d   │     │ ∘   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┼─────┤
-- │ LG  │ ∘   │ ∘   │ ∘   │ WIP │ WIP │ ∘   │ ∘   │ ∘   │     │
-- └─────┴─────┴─────┴─────┴─────┴─────┴─────┴─────┴─────┴─────┘
--
-- d   : Direct translation.
-- ∘   : Composition of translations.
-- ∘!  : Composition; direct translation fails the termination check.
-- WIP : Work in progress.

-- Translation from closed Hilbert-style sequential to closed Hilbert-style.

chs→ch : ∀ {A} → CHS.⊢ A → CH.⊢ A
chs→ch (Ξ , ts) = chs⊦→ch ts top
  where
    chs⊦→ch : ∀ {A Ξ} → CHS.⊦⊢ Ξ → A ∈ Ξ → CH.⊢ A
    chs⊦→ch (CHS.mp i j ts) top     = CH.app (chs⊦→ch ts i) (chs⊦→ch ts j)
    chs⊦→ch (CHS.ci ts)     top     = CH.ci
    chs⊦→ch (CHS.ck ts)     top     = CH.ck
    chs⊦→ch (CHS.cs ts)     top     = CH.cs
    chs⊦→ch (CHS.nec ss ts) top     = CH.box (chs⊦→ch ss top)
    chs⊦→ch (CHS.cdist ts)  top     = CH.cdist
    chs⊦→ch (CHS.cup ts)    top     = CH.cup
    chs⊦→ch (CHS.cdown ts)  top     = CH.cdown
    chs⊦→ch (CHS.cpair ts)  top     = CH.cpair
    chs⊦→ch (CHS.cfst ts)   top     = CH.cfst
    chs⊦→ch (CHS.csnd ts)   top     = CH.csnd
    chs⊦→ch (CHS.unit ts)   top     = CH.unit
    chs⊦→ch (CHS.mp i j ts) (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.ci ts)     (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.ck ts)     (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.cs ts)     (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.nec ss ts) (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.cdist ts)  (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.cup ts)    (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.cdown ts)  (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.cpair ts)  (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.cfst ts)   (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.csnd ts)   (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.unit ts)   (pop k) = chs⊦→ch ts k

-- Translation from closed Hilbert-style to closed Hilbert-style sequential.

ch→chs : ∀ {A} → CH.⊢ A → CHS.⊢ A
ch→chs (CH.app t u) = CHS.app (ch→chs t) (ch→chs u)
ch→chs CH.ci        = ∅ , CHS.ci CHS.nil
ch→chs CH.ck        = ∅ , CHS.ck CHS.nil
ch→chs CH.cs        = ∅ , CHS.cs CHS.nil
ch→chs (CH.box t)   = CHS.box (ch→chs t)
ch→chs CH.cdist     = ∅ , CHS.cdist CHS.nil
ch→chs CH.cup       = ∅ , CHS.cup CHS.nil
ch→chs CH.cdown     = ∅ , CHS.cdown CHS.nil
ch→chs CH.cpair     = ∅ , CHS.cpair CHS.nil
ch→chs CH.cfst      = ∅ , CHS.cfst CHS.nil
ch→chs CH.csnd      = ∅ , CHS.csnd CHS.nil
ch→chs CH.unit      = ∅ , CHS.unit CHS.nil

-- Translation from Hilbert-style sequential to Hilbert-style.

hs→h : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → H⟨ Γ ⊢ A ⟩
hs→h (Ξ , ts) = hs⊦→h ts top
  where
    hs⊦→h : ∀ {A Ξ Γ} → HS⟨ Γ ⊦⊢ Ξ ⟩ → A ∈ Ξ → H⟨ Γ ⊢ A ⟩
    hs⊦→h (HS.var i ts)  top     = H.var i
    hs⊦→h (HS.mp i j ts) top     = H.app (hs⊦→h ts i) (hs⊦→h ts j)
    hs⊦→h (HS.ci ts)     top     = H.ci
    hs⊦→h (HS.ck ts)     top     = H.ck
    hs⊦→h (HS.cs ts)     top     = H.cs
    hs⊦→h (HS.nec ss ts) top     = H.box (hs⊦→h ss top)
    hs⊦→h (HS.cdist ts)  top     = H.cdist
    hs⊦→h (HS.cup ts)    top     = H.cup
    hs⊦→h (HS.cdown ts)  top     = H.cdown
    hs⊦→h (HS.cpair ts)  top     = H.cpair
    hs⊦→h (HS.cfst ts)   top     = H.cfst
    hs⊦→h (HS.csnd ts)   top     = H.csnd
    hs⊦→h (HS.unit ts)   top     = H.unit
    hs⊦→h (HS.var i ts)  (pop k) = hs⊦→h ts k
    hs⊦→h (HS.mp i j ts) (pop k) = hs⊦→h ts k
    hs⊦→h (HS.ci ts)     (pop k) = hs⊦→h ts k
    hs⊦→h (HS.ck ts)     (pop k) = hs⊦→h ts k
    hs⊦→h (HS.cs ts)     (pop k) = hs⊦→h ts k
    hs⊦→h (HS.nec ss ts) (pop k) = hs⊦→h ts k
    hs⊦→h (HS.cdist ts)  (pop k) = hs⊦→h ts k
    hs⊦→h (HS.cup ts)    (pop k) = hs⊦→h ts k
    hs⊦→h (HS.cdown ts)  (pop k) = hs⊦→h ts k
    hs⊦→h (HS.cpair ts)  (pop k) = hs⊦→h ts k
    hs⊦→h (HS.cfst ts)   (pop k) = hs⊦→h ts k
    hs⊦→h (HS.csnd ts)   (pop k) = hs⊦→h ts k
    hs⊦→h (HS.unit ts)   (pop k) = hs⊦→h ts k

-- Translation from Hilbert-style to Hilbert-style sequential.

h→hs : ∀ {A Γ} → H⟨ Γ ⊢ A ⟩ → HS⟨ Γ ⊢ A ⟩
h→hs (H.var i)   = ∅ , HS.var i HS.nil
h→hs (H.app t u) = HS.app (h→hs t) (h→hs u)
h→hs H.ci        = ∅ , HS.ci HS.nil
h→hs H.ck        = ∅ , HS.ck HS.nil
h→hs H.cs        = ∅ , HS.cs HS.nil
h→hs (H.box t)   = HS.box (h→hs t)
h→hs H.cdist     = ∅ , HS.cdist HS.nil
h→hs H.cup       = ∅ , HS.cup HS.nil
h→hs H.cdown     = ∅ , HS.cdown HS.nil
h→hs H.cpair     = ∅ , HS.cpair HS.nil
h→hs H.cfst      = ∅ , HS.cfst HS.nil
h→hs H.csnd      = ∅ , HS.csnd HS.nil
h→hs H.unit      = ∅ , HS.unit HS.nil

-- Translation from dyadic Hilbert-style sequential to dyadic Hilbert-style.

dhs→dh : ∀ {A Γ Δ} → DHS⟨ Γ ⁏ Δ ⊢ A ⟩ → DH⟨ Γ ⁏ Δ ⊢ A ⟩
dhs→dh (Ξ , ts) = dhs⊦→dh ts top
  where
    dhs⊦→dh : ∀ {A Ξ Γ Δ} → DHS⟨ Γ ⁏ Δ ⊦⊢ Ξ ⟩ → A ∈ Ξ → DH⟨ Γ ⁏ Δ ⊢ A ⟩
    dhs⊦→dh (DHS.var i ts)  top     = DH.var i
    dhs⊦→dh (DHS.mp i j ts) top     = DH.app (dhs⊦→dh ts i) (dhs⊦→dh ts j)
    dhs⊦→dh (DHS.ci ts)     top     = DH.ci
    dhs⊦→dh (DHS.ck ts)     top     = DH.ck
    dhs⊦→dh (DHS.cs ts)     top     = DH.cs
    dhs⊦→dh (DHS.mvar i ts) top     = DH.mvar i
    dhs⊦→dh (DHS.nec ss ts) top     = DH.box (dhs⊦→dh ss top)
    dhs⊦→dh (DHS.cdist ts)  top     = DH.cdist
    dhs⊦→dh (DHS.cup ts)    top     = DH.cup
    dhs⊦→dh (DHS.cdown ts)  top     = DH.cdown
    dhs⊦→dh (DHS.cpair ts)  top     = DH.cpair
    dhs⊦→dh (DHS.cfst ts)   top     = DH.cfst
    dhs⊦→dh (DHS.csnd ts)   top     = DH.csnd
    dhs⊦→dh (DHS.unit ts)   top     = DH.unit
    dhs⊦→dh (DHS.var i ts)  (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.mp i j ts) (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.ci ts)     (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.ck ts)     (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.cs ts)     (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.mvar i ts) (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.nec ss ts) (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.cdist ts)  (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.cup ts)    (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.cdown ts)  (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.cpair ts)  (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.cfst ts)   (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.csnd ts)   (pop k) = dhs⊦→dh ts k
    dhs⊦→dh (DHS.unit ts)   (pop k) = dhs⊦→dh ts k

-- Translation from dyadic Hilbert-style to dyadic Hilbert-style sequential

dh→dhs : ∀ {A Γ Δ} → DH⟨ Γ ⁏ Δ ⊢ A ⟩ → DHS⟨ Γ ⁏ Δ ⊢ A ⟩
dh→dhs (DH.var i)   = ∅ , DHS.var i DHS.nil
dh→dhs (DH.app t u) = DHS.app (dh→dhs t) (dh→dhs u)
dh→dhs DH.ci        = ∅ , DHS.ci DHS.nil
dh→dhs DH.ck        = ∅ , DHS.ck DHS.nil
dh→dhs DH.cs        = ∅ , DHS.cs DHS.nil
dh→dhs (DH.mvar i)  = ∅ , DHS.mvar i DHS.nil
dh→dhs (DH.box t)   = DHS.box (dh→dhs t)
dh→dhs DH.cdist     = ∅ , DHS.cdist DHS.nil
dh→dhs DH.cup       = ∅ , DHS.cup DHS.nil
dh→dhs DH.cdown     = ∅ , DHS.cdown DHS.nil
dh→dhs DH.cpair     = ∅ , DHS.cpair DHS.nil
dh→dhs DH.cfst      = ∅ , DHS.cfst DHS.nil
dh→dhs DH.csnd      = ∅ , DHS.csnd DHS.nil
dh→dhs DH.unit      = ∅ , DHS.unit DHS.nil

-- Deduction and detachment theorems for Hilbert-style sequential.

hs-lam : ∀ {A B Γ} → HS⟨ Γ , A ⊢ B ⟩ → HS⟨ Γ ⊢ A ▻ B ⟩
hs-lam = h→hs ∘ H.lam ∘ hs→h

hs-lam⋆₀ : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → HS⟨ ∅ ⊢ Γ ▻⋯▻ A ⟩
hs-lam⋆₀ = h→hs ∘ H.lam⋆₀ ∘ hs→h

hs-det : ∀ {A B Γ} → HS⟨ Γ ⊢ A ▻ B ⟩ → HS⟨ Γ , A ⊢ B ⟩
hs-det = h→hs ∘ H.det ∘ hs→h

hs-det⋆₀ : ∀ {A Γ} → HS⟨ ∅ ⊢ Γ ▻⋯▻ A ⟩ → HS⟨ Γ ⊢ A ⟩
hs-det⋆₀ = h→hs ∘ H.det⋆₀ ∘ hs→h

-- Deduction and detachment theorems for dyadic Hilbert-style sequential.

dhs-lam : ∀ {A B Γ Δ} → DHS⟨ Γ , A ⁏ Δ ⊢ B ⟩ → DHS⟨ Γ ⁏ Δ ⊢ A ▻ B ⟩
dhs-lam = dh→dhs ∘ DH.lam ∘ dhs→dh

dhs-lam⋆₀ : ∀ {A Γ Δ} → DHS⟨ Γ ⁏ Δ ⊢ A ⟩ → DHS⟨ ∅ ⁏ Δ ⊢ Γ ▻⋯▻ A ⟩
dhs-lam⋆₀ = dh→dhs ∘ DH.lam⋆₀ ∘ dhs→dh

dhs-mlam : ∀ {A B Γ Δ} → DHS⟨ Γ ⁏ Δ , A ⊢ B ⟩ → DHS⟨ Γ ⁏ Δ ⊢ □ A ▻ B ⟩
dhs-mlam = dh→dhs ∘ DH.mlam ∘ dhs→dh

dhs-mlam⋆₀ : ∀ {Δ A Γ} → DHS⟨ Γ ⁏ Δ ⊢ A ⟩ → DHS⟨ Γ ⁏ ∅ ⊢ □⋆ Δ ▻⋯▻ A ⟩
dhs-mlam⋆₀ = dh→dhs ∘ DH.mlam⋆₀ ∘ dhs→dh

dhs-det : ∀ {A B Γ Δ} → DHS⟨ Γ ⁏ Δ ⊢ A ▻ B ⟩ → DHS⟨ Γ , A ⁏ Δ ⊢ B ⟩
dhs-det = dh→dhs ∘ DH.det ∘ dhs→dh

dhs-det⋆₀ : ∀ {A Γ Δ} → DHS⟨ ∅ ⁏ Δ ⊢ Γ ▻⋯▻ A ⟩ → DHS⟨ Γ ⁏ Δ ⊢ A ⟩
dhs-det⋆₀ = dh→dhs ∘ DH.det⋆₀ ∘ dhs→dh

dhs-mdet : ∀ {A B Γ Δ} → DHS⟨ Γ ⁏ Δ ⊢ □ A ▻ B ⟩ → DHS⟨ Γ ⁏ Δ , A ⊢ B ⟩
dhs-mdet = dh→dhs ∘ DH.mdet ∘ dhs→dh

dhs-mdet⋆₀ : ∀ {Δ A Γ} → DHS⟨ Γ ⁏ ∅ ⊢ □⋆ Δ ▻⋯▻ A ⟩ → DHS⟨ Γ ⁏ Δ ⊢ A ⟩
dhs-mdet⋆₀ = dh→dhs ∘ DH.mdet⋆₀ ∘ dhs→dh

-- Context manipulation for dyadic Hilbert-style sequential.

dhs-merge : ∀ {Δ A Γ} → DHS⟨ Γ ⁏ Δ ⊢ A ⟩ → DHS⟨ Γ ⧺ (□⋆ Δ) ⁏ ∅ ⊢ A ⟩
dhs-merge {Δ} = dh→dhs ∘ DH.merge ∘ dhs→dh

dhs-split : ∀ {Δ A Γ} → DHS⟨ Γ ⧺ (□⋆ Δ) ⁏ ∅ ⊢ A ⟩ → DHS⟨ Γ ⁏ Δ ⊢ A ⟩
dhs-split {Δ} = dh→dhs ∘ DH.split ∘ dhs→dh

-- Translation from closed Hilbert-style sequential to Hilbert-style sequential.

chs→hs₀ : ∀ {A} → CHS.⊢ A → HS⟨ ∅ ⊢ A ⟩
chs→hs₀ (Ξ , ts) = Ξ , chs⊦→hs⊦ ts
  where
    chs⊦→hs⊦ : ∀ {Ξ} → CHS.⊦⊢ Ξ → HS⟨ ∅ ⊦⊢ Ξ ⟩
    chs⊦→hs⊦ CHS.nil         = HS.nil
    chs⊦→hs⊦ (CHS.mp i j ts) = HS.mp i j (chs⊦→hs⊦ ts)
    chs⊦→hs⊦ (CHS.ci ts)     = HS.ci (chs⊦→hs⊦ ts)
    chs⊦→hs⊦ (CHS.ck ts)     = HS.ck (chs⊦→hs⊦ ts)
    chs⊦→hs⊦ (CHS.cs ts)     = HS.cs (chs⊦→hs⊦ ts)
    chs⊦→hs⊦ (CHS.cpair ts)  = HS.cpair (chs⊦→hs⊦ ts)
    chs⊦→hs⊦ (CHS.cfst ts)   = HS.cfst (chs⊦→hs⊦ ts)
    chs⊦→hs⊦ (CHS.csnd ts)   = HS.csnd (chs⊦→hs⊦ ts)
    chs⊦→hs⊦ (CHS.unit ts)   = HS.unit (chs⊦→hs⊦ ts)
    chs⊦→hs⊦ (CHS.nec ss ts) = HS.nec (chs⊦→hs⊦ ss) (chs⊦→hs⊦ ts)
    chs⊦→hs⊦ (CHS.cdist ts)  = HS.cdist (chs⊦→hs⊦ ts)
    chs⊦→hs⊦ (CHS.cup ts)    = HS.cup (chs⊦→hs⊦ ts)
    chs⊦→hs⊦ (CHS.cdown ts)  = HS.cdown (chs⊦→hs⊦ ts)

chs→hs : ∀ {A Γ} → CHS.⊢ Γ ▻⋯▻ A → HS⟨ Γ ⊢ A ⟩
chs→hs t = hs-det⋆₀ (chs→hs₀ t)

-- Translation from Hilbert-style sequential to closed Hilbert-style sequential.

hs₀→chs : ∀ {A} → HS⟨ ∅ ⊢ A ⟩ → CHS.⊢ A
hs₀→chs (Ξ , ts) = Ξ , hs₀⊦→chs⊦ ts
  where
    hs₀⊦→chs⊦ : ∀ {Ξ} → HS⟨ ∅ ⊦⊢ Ξ ⟩ → CHS.⊦⊢ Ξ
    hs₀⊦→chs⊦ HS.nil         = CHS.nil
    hs₀⊦→chs⊦ (HS.var () ts)
    hs₀⊦→chs⊦ (HS.mp i j ts) = CHS.mp i j (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.ci ts)     = CHS.ci (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.ck ts)     = CHS.ck (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.cs ts)     = CHS.cs (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.cpair ts)  = CHS.cpair (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.cfst ts)   = CHS.cfst (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.csnd ts)   = CHS.csnd (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.unit ts)   = CHS.unit (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.nec ss ts) = CHS.nec (hs₀⊦→chs⊦ ss) (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.cdist ts)  = CHS.cdist (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.cup ts)    = CHS.cup (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.cdown ts)  = CHS.cdown (hs₀⊦→chs⊦ ts)

hs→chs : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → CHS.⊢ Γ ▻⋯▻ A
hs→chs t = hs₀→chs (hs-lam⋆₀ t)

-- Translation from dyadic Hilbert-style sequential to Hilbert-style sequential.

dhs₀→hs : ∀ {A Γ} → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩ → HS⟨ Γ ⊢ A ⟩
dhs₀→hs (Ξ , ts) = Ξ , dhs₀⊦→hs⊦ ts
  where
    dhs₀⊦→hs⊦ : ∀ {Ξ Γ} → DHS⟨ Γ ⁏ ∅ ⊦⊢ Ξ ⟩ → HS⟨ Γ ⊦⊢ Ξ ⟩
    dhs₀⊦→hs⊦ DHS.nil          = HS.nil
    dhs₀⊦→hs⊦ (DHS.var i ts)   = HS.var i (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.mp i j ts)  = HS.mp i j (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.ci ts)      = HS.ci (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.ck ts)      = HS.ck (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.cs ts)      = HS.cs (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.mvar () ts)
    dhs₀⊦→hs⊦ (DHS.nec ss ts)  = HS.nec (dhs₀⊦→hs⊦ ss) (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.cdist ts)   = HS.cdist (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.cup ts)     = HS.cup (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.cdown ts)   = HS.cdown (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.cpair ts)   = HS.cpair (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.cfst ts)    = HS.cfst (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.csnd ts)    = HS.csnd (dhs₀⊦→hs⊦ ts)
    dhs₀⊦→hs⊦ (DHS.unit ts)    = HS.unit (dhs₀⊦→hs⊦ ts)

dhs→hs : ∀ {A Γ Δ} → DHS⟨ Γ ⁏ Δ ⊢ A ⟩ → HS⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩
dhs→hs = dhs₀→hs ∘ dhs-merge

-- Translation from Hilbert-style sequential to dyadic Hilbert-style sequential.

hs→dhs₀ : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩
hs→dhs₀ (Ξ , ts) = Ξ , hs⊦→dhs₀⊦ ts
  where
    hs⊦→dhs₀⊦ : ∀ {Ξ Γ} → HS⟨ Γ ⊦⊢ Ξ ⟩ → DHS⟨ Γ ⁏ ∅ ⊦⊢ Ξ ⟩
    hs⊦→dhs₀⊦ HS.nil         = DHS.nil
    hs⊦→dhs₀⊦ (HS.var i ts)  = DHS.var i (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.mp i j ts) = DHS.mp i j (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.ci ts)     = DHS.ci (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.ck ts)     = DHS.ck (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.cs ts)     = DHS.cs (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.nec ss ts) = DHS.nec (hs⊦→dhs₀⊦ ss) (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.cdist ts)  = DHS.cdist (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.cup ts)    = DHS.cup (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.cdown ts)  = DHS.cdown (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.cpair ts)  = DHS.cpair (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.cfst ts)   = DHS.cfst (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.csnd ts)   = DHS.csnd (hs⊦→dhs₀⊦ ts)
    hs⊦→dhs₀⊦ (HS.unit ts)   = DHS.unit (hs⊦→dhs₀⊦ ts)

hs→dhs : ∀ {A Γ Δ} → HS⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩ → DHS⟨ Γ ⁏ Δ ⊢ A ⟩
hs→dhs = dhs-split ∘ hs→dhs₀

-- Translation from closed Hilbert-style to Hilbert-style.

ch→h₀ : ∀ {A} → CH.⊢ A → H⟨ ∅ ⊢ A ⟩
ch→h₀ (CH.app t u) = H.app (ch→h₀ t) (ch→h₀ u)
ch→h₀ CH.ci        = H.ci
ch→h₀ CH.ck        = H.ck
ch→h₀ CH.cs        = H.cs
ch→h₀ CH.cpair     = H.cpair
ch→h₀ CH.cfst      = H.cfst
ch→h₀ CH.csnd      = H.csnd
ch→h₀ CH.unit      = H.unit
ch→h₀ (CH.box t)   = H.box (ch→h₀ t)
ch→h₀ CH.cdist     = H.cdist
ch→h₀ CH.cup       = H.cup
ch→h₀ CH.cdown     = H.cdown

ch→h : ∀ {A Γ} → CH.⊢ Γ ▻⋯▻ A → H⟨ Γ ⊢ A ⟩
ch→h t = H.det⋆₀ (ch→h₀ t)

-- Translation from Hilbert-style to closed Hilbert-style.

h₀→ch : ∀ {A} → H⟨ ∅ ⊢ A ⟩ → CH.⊢ A
h₀→ch (H.var ())
h₀→ch (H.app t u) = CH.app (h₀→ch t) (h₀→ch u)
h₀→ch H.ci        = CH.ci
h₀→ch H.ck        = CH.ck
h₀→ch H.cs        = CH.cs
h₀→ch H.cpair     = CH.cpair
h₀→ch H.cfst      = CH.cfst
h₀→ch H.csnd      = CH.csnd
h₀→ch H.unit      = CH.unit
h₀→ch (H.box t)   = CH.box (h₀→ch t)
h₀→ch H.cdist     = CH.cdist
h₀→ch H.cup       = CH.cup
h₀→ch H.cdown     = CH.cdown

h→ch : ∀ {A Γ} → H⟨ Γ ⊢ A ⟩ → CH.⊢ Γ ▻⋯▻ A
h→ch t = h₀→ch (H.lam⋆₀ t)

-- Translation from dyadic Hilbert-style to Hilbert-style.

dh₀→h : ∀ {A Γ} → DH⟨ Γ ⁏ ∅ ⊢ A ⟩ → H⟨ Γ ⊢ A ⟩
dh₀→h (DH.var i)   = H.var i
dh₀→h (DH.app t u) = H.app (dh₀→h t) (dh₀→h u)
dh₀→h DH.ci        = H.ci
dh₀→h DH.ck        = H.ck
dh₀→h DH.cs        = H.cs
dh₀→h (DH.mvar ())
dh₀→h (DH.box t)   = H.box (dh₀→h t)
dh₀→h DH.cdist     = H.cdist
dh₀→h DH.cup       = H.cup
dh₀→h DH.cdown     = H.cdown
dh₀→h DH.cpair     = H.cpair
dh₀→h DH.cfst      = H.cfst
dh₀→h DH.csnd      = H.csnd
dh₀→h DH.unit      = H.unit

dh→h : ∀ {A Γ Δ} → DH⟨ Γ ⁏ Δ ⊢ A ⟩ → H⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩
dh→h = dh₀→h ∘ DH.merge

-- Translation from Hilbert-style to dyadic Hilbert-style.

h→dh₀ : ∀ {A Γ} → H⟨ Γ ⊢ A ⟩ → DH⟨ Γ ⁏ ∅ ⊢ A ⟩
h→dh₀ (H.var i)   = DH.var i
h→dh₀ (H.app t u) = DH.app (h→dh₀ t) (h→dh₀ u)
h→dh₀ H.ci        = DH.ci
h→dh₀ H.ck        = DH.ck
h→dh₀ H.cs        = DH.cs
h→dh₀ (H.box t)   = DH.box (h→dh₀ t)
h→dh₀ H.cdist     = DH.cdist
h→dh₀ H.cup       = DH.cup
h→dh₀ H.cdown     = DH.cdown
h→dh₀ H.cpair     = DH.cpair
h→dh₀ H.cfst      = DH.cfst
h→dh₀ H.csnd      = DH.csnd
h→dh₀ H.unit      = DH.unit

h→dh : ∀ {A Γ Δ} → H⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩ → DH⟨ Γ ⁏ Δ ⊢ A ⟩
h→dh = DH.split ∘ h→dh₀

-- Translation from Hilbert-style to Gentzen-style.

h→g : ∀ {A Γ} → H⟨ Γ ⊢ A ⟩ → G⟨ Γ ⊢ A ⟩
h→g (H.var i)   = G.var i
h→g (H.app t u) = G.app (h→g t) (h→g u)
h→g H.ci        = G.ci
h→g H.ck        = G.ck
h→g H.cs        = G.cs
h→g (H.box t)   = G.box (h→g t)
h→g H.cdist     = G.cdist
h→g H.cup       = G.cup
h→g H.cdown     = G.cdown
h→g H.cpair     = G.cpair
h→g H.cfst      = G.cfst
h→g H.csnd      = G.csnd
h→g H.unit      = G.unit

-- Translation from Gentzen-style to Hilbert-style.

mutual
  g→h : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → H⟨ Γ ⊢ A ⟩
  g→h (G.var i)         = H.var i
  g→h (G.lam t)         = H.lam (g→h t)
  g→h (G.app t u)       = H.app (g→h t) (g→h u)
  g→h (G.multibox ts u) = H.multibox (g→h⋆ ts) (g→h u)
  g→h (G.down t)        = H.down (g→h t)
  g→h (G.pair t u)      = H.pair (g→h t) (g→h u)
  g→h (G.fst t)         = H.fst (g→h t)
  g→h (G.snd t)         = H.snd (g→h t)
  g→h G.unit            = H.unit

  g→h⋆ : ∀ {Ξ Γ} → G⟨ Γ ⊢⋆ Ξ ⟩ → H⟨ Γ ⊢⋆ Ξ ⟩
  g→h⋆ {∅}     ∙        = ∙
  g→h⋆ {Ξ , A} (ts , t) = g→h⋆ ts , g→h t

-- Translation from dyadic Hilbert-style to dyadic Gentzen-style.

dh→dg : ∀ {A Γ Δ} → DH⟨ Γ ⁏ Δ ⊢ A ⟩ → DG⟨ Γ ⁏ Δ ⊢ A ⟩
dh→dg (DH.var i)   = DG.var i
dh→dg (DH.app t u) = DG.app (dh→dg t) (dh→dg u)
dh→dg DH.ci        = DG.ci
dh→dg DH.ck        = DG.ck
dh→dg DH.cs        = DG.cs
dh→dg (DH.mvar i)  = DG.mvar i
dh→dg (DH.box t)   = DG.box (dh→dg t)
dh→dg DH.cdist     = DG.cdist
dh→dg DH.cup       = DG.cup
dh→dg DH.cdown     = DG.cdown
dh→dg DH.cpair     = DG.cpair
dh→dg DH.cfst      = DG.cfst
dh→dg DH.csnd      = DG.csnd
dh→dg DH.unit      = DG.unit

-- Translation from dyadic Gentzen-style to dyadic Hilbert-style.

dg→dh : ∀ {A Γ Δ} → DG⟨ Γ ⁏ Δ ⊢ A ⟩ → DH⟨ Γ ⁏ Δ ⊢ A ⟩
dg→dh (DG.var i)     = DH.var i
dg→dh (DG.lam t)     = DH.lam (dg→dh t)
dg→dh (DG.app t u)   = DH.app (dg→dh t) (dg→dh u)
dg→dh (DG.mvar i)    = DH.mvar i
dg→dh (DG.box t)     = DH.box (dg→dh t)
dg→dh (DG.unbox t u) = DH.unbox (dg→dh t) (dg→dh u)
dg→dh (DG.pair t u)  = DH.pair (dg→dh t) (dg→dh u)
dg→dh (DG.fst t)     = DH.fst (dg→dh t)
dg→dh (DG.snd t)     = DH.snd (dg→dh t)
dg→dh DG.unit        = DH.unit

-- Translation from Gentzen-style to dyadic Gentzen-style.

mutual
  g→dg₀ : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → DG⟨ Γ ⁏ ∅ ⊢ A ⟩
  g→dg₀ (G.var i)         = DG.var i
  g→dg₀ (G.lam t)         = DG.lam (g→dg₀ t)
  g→dg₀ (G.app t u)       = DG.app (g→dg₀ t) (g→dg₀ u)
  g→dg₀ (G.multibox ts u) = DG.multibox (g→dg₀⋆ ts) (g→dg₀ u)
  g→dg₀ (G.down t)        = DG.down (g→dg₀ t)
  g→dg₀ (G.pair t u)      = DG.pair (g→dg₀ t) (g→dg₀ u)
  g→dg₀ (G.fst t)         = DG.fst (g→dg₀ t)
  g→dg₀ (G.snd t)         = DG.snd (g→dg₀ t)
  g→dg₀ G.unit            = DG.unit

  g→dg₀⋆ : ∀ {Ξ Γ} → G⟨ Γ ⊢⋆ Ξ ⟩ → DG⟨ Γ ⁏ ∅ ⊢⋆ Ξ ⟩
  g→dg₀⋆ {∅}     ∙        = ∙
  g→dg₀⋆ {Ξ , A} (ts , t) = g→dg₀⋆ ts , g→dg₀ t

g→dg : ∀ {A Γ Δ} → G⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩ → DG⟨ Γ ⁏ Δ ⊢ A ⟩
g→dg = DG.split ∘ g→dg₀

-- Translation from Hilbert-style to labelled Gentzen-style.

h→lg : ∀ {x A Γ Λ} → H⟨ Γ ⊢ A ⟩ → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩
h→lg (H.var i)   = LG.var i
h→lg (H.app t u) = LG.app (h→lg t) (h→lg u)
h→lg H.ci        = LG.ci
h→lg H.ck        = LG.ck
h→lg H.cs        = LG.cs
h→lg (H.box t)   = LG.box (h→lg t)
h→lg H.cdist     = LG.cdist
h→lg H.cup       = LG.cup
h→lg H.cdown     = LG.cdown
h→lg H.cpair     = LG.cpair
h→lg H.cfst      = LG.cfst
h→lg H.csnd      = LG.csnd
h→lg H.unit      = LG.unit

-- Translation from labelled Gentzen-style to Hilbert-style.

-- FIXME: Stronger hypothesis?
postulate
  h-oops : ∀ {x A Γ Λ} → (∀ {y} → LG⟨ Γ ⁏ Λ , x ↝ y ⊢ A ◎ y ⟩) → H⟨ Γ ⊢ □ A ⟩

lg→h : ∀ {x A Γ Λ} → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩ → H⟨ Γ ⊢ A ⟩
lg→h (LG.var i)    = H.var i
lg→h (LG.lam t)    = H.lam (lg→h t)
lg→h (LG.app t u)  = H.app (lg→h t) (lg→h u)
lg→h (LG.scan t)   = h-oops t
lg→h (LG.move t u) = H.down (lg→h t)
lg→h (LG.pair t u) = H.pair (lg→h t) (lg→h u)
lg→h (LG.fst t)    = H.fst (lg→h t)
lg→h (LG.snd t)    = H.snd (lg→h t)
lg→h LG.unit       = H.unit

-- Translation from Gentzen-style to labelled Gentzen-style.

mutual
  g→lg : ∀ {x A Γ Λ} → G⟨ Γ ⊢ A ⟩ → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩
  g→lg (G.var i)         = LG.var i
  g→lg (G.lam t)         = LG.lam (g→lg t)
  g→lg (G.app t u)       = LG.app (g→lg t) (g→lg u)
  g→lg (G.multibox ts u) = LG.multibox (g→lg⋆ ts) (g→lg u)
  g→lg (G.down t)        = LG.move (g→lg t) LG.rrefl
  g→lg (G.pair t u)      = LG.pair (g→lg t) (g→lg u)
  g→lg (G.fst t)         = LG.fst (g→lg t)
  g→lg (G.snd t)         = LG.snd (g→lg t)
  g→lg G.unit            = LG.unit

  g→lg⋆ : ∀ {x Ξ Γ Λ} → G⟨ Γ ⊢⋆ Ξ ⟩ → LG⟨ Γ ⁏ Λ ⊢⋆ Ξ ◎⋆ x ⟩
  g→lg⋆ {x} {∅}     ∙        = ∙
  g→lg⋆ {x} {Ξ , A} (ts , t) = g→lg⋆ ts , g→lg t

-- Translation from labelled Gentzen-style to Gentzen-style.

-- FIXME: Stronger hypothesis?
postulate
  g-oops : ∀ {x A Γ Λ} → (∀ {y} → LG⟨ Γ ⁏ Λ , x ↝ y ⊢ A ◎ y ⟩) → G⟨ Γ ⊢ □ A ⟩

lg→g : ∀ {x A Γ Λ} → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩ → G⟨ Γ ⊢ A ⟩
lg→g (LG.var i)    = G.var i
lg→g (LG.lam t)    = G.lam (lg→g t)
lg→g (LG.app t u)  = G.app (lg→g t) (lg→g u)
lg→g (LG.scan t)   = g-oops t
lg→g (LG.move t u) = G.down (lg→g t)
lg→g (LG.pair t u) = G.pair (lg→g t) (lg→g u)
lg→g (LG.fst t)    = G.fst (lg→g t)
lg→g (LG.snd t)    = G.snd (lg→g t)
lg→g LG.unit       = G.unit

-- Additional translations from closed Hilbert-style sequential.

chs→h₀ : ∀ {A} → CHS.⊢ A → H⟨ ∅ ⊢ A ⟩
chs→h₀ = ch→h₀ ∘ chs→ch

chs→h : ∀ {A Γ} → CHS.⊢ Γ ▻⋯▻ A → H⟨ Γ ⊢ A ⟩
chs→h = ch→h ∘ chs→ch

chs→g₀ : ∀ {A} → CHS.⊢ A → G⟨ ∅ ⊢ A ⟩
chs→g₀ = h→g ∘ chs→h₀

chs→g : ∀ {A Γ} → CHS.⊢ Γ ▻⋯▻ A → G⟨ Γ ⊢ A ⟩
chs→g = h→g ∘ chs→h

chs→dhs₀₀ : ∀ {A} → CHS.⊢ A → DHS⟨ ∅ ⁏ ∅ ⊢ A ⟩
chs→dhs₀₀ = hs→dhs₀ ∘ chs→hs₀

chs→dhs₀ : ∀ {A Γ} → CHS.⊢ Γ ▻⋯▻ A → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩
chs→dhs₀ = hs→dhs₀ ∘ chs→hs

chs→dhs : ∀ {A Γ Δ} → CHS.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A → DHS⟨ Γ ⁏ Δ ⊢ A ⟩
chs→dhs = hs→dhs ∘ chs→hs

chs→dh₀₀ : ∀ {A} → CHS.⊢ A → DH⟨ ∅ ⁏ ∅ ⊢ A ⟩
chs→dh₀₀ = h→dh₀ ∘ chs→h₀

chs→dh₀ : ∀ {A Γ} → CHS.⊢ Γ ▻⋯▻ A → DH⟨ Γ ⁏ ∅ ⊢ A ⟩
chs→dh₀ = h→dh₀ ∘ chs→h

chs→dh : ∀ {A Γ Δ} → CHS.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A → DH⟨ Γ ⁏ Δ ⊢ A ⟩
chs→dh = h→dh ∘ chs→h

chs→dg₀₀ : ∀ {A} → CHS.⊢ A → DG⟨ ∅ ⁏ ∅ ⊢ A ⟩
chs→dg₀₀ = g→dg₀ ∘ chs→g₀

chs→dg₀ : ∀ {A Γ} → CHS.⊢ Γ ▻⋯▻ A → DG⟨ Γ ⁏ ∅ ⊢ A ⟩
chs→dg₀ = g→dg₀ ∘ chs→g

chs→dg : ∀ {A Γ Δ} → CHS.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A → DG⟨ Γ ⁏ Δ ⊢ A ⟩
chs→dg = g→dg ∘ chs→g

chs→lg₀ : ∀ {x A Λ} → CHS.⊢ A → LG⟨ ∅ ⁏ Λ ⊢ A ◎ x ⟩
chs→lg₀ = g→lg ∘ chs→g₀

chs→lg : ∀ {x A Γ Λ} → CHS.⊢ Γ ▻⋯▻ A → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩
chs→lg = g→lg ∘ chs→g

-- Additional translations from closed Hilbert-style.

ch→hs₀ : ∀ {A} → CH.⊢ A → HS⟨ ∅ ⊢ A ⟩
ch→hs₀ = chs→hs ∘ ch→chs

ch→hs : ∀ {A Γ} → CH.⊢ Γ ▻⋯▻ A → HS⟨ Γ ⊢ A ⟩
ch→hs = chs→hs ∘ ch→chs

ch→g₀ : ∀ {A} → CH.⊢ A → G⟨ ∅ ⊢ A ⟩
ch→g₀ = h→g ∘ ch→h₀

ch→g : ∀ {A Γ} → CH.⊢ Γ ▻⋯▻ A → G⟨ Γ ⊢ A ⟩
ch→g = h→g ∘ ch→h

ch→dhs₀₀ : ∀ {A} → CH.⊢ A → DHS⟨ ∅ ⁏ ∅ ⊢ A ⟩
ch→dhs₀₀ = hs→dhs₀ ∘ ch→hs₀

ch→dhs₀ : ∀ {A Γ} → CH.⊢ Γ ▻⋯▻ A → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩
ch→dhs₀ = hs→dhs₀ ∘ ch→hs

ch→dhs : ∀ {A Γ Δ} → CH.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A → DHS⟨ Γ ⁏ Δ ⊢ A ⟩
ch→dhs = hs→dhs ∘ ch→hs

ch→dh₀₀ : ∀ {A} → CH.⊢ A → DH⟨ ∅ ⁏ ∅ ⊢ A ⟩
ch→dh₀₀ = h→dh₀ ∘ ch→h₀

ch→dh₀ : ∀ {A Γ} → CH.⊢ Γ ▻⋯▻ A → DH⟨ Γ ⁏ ∅ ⊢ A ⟩
ch→dh₀ = h→dh₀ ∘ ch→h

ch→dh : ∀ {A Γ Δ} → CH.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A → DH⟨ Γ ⁏ Δ ⊢ A ⟩
ch→dh = h→dh ∘ ch→h

ch→dg₀₀ : ∀ {A} → CH.⊢ A → DG⟨ ∅ ⁏ ∅ ⊢ A ⟩
ch→dg₀₀ = g→dg₀ ∘ ch→g₀

ch→dg₀ : ∀ {A Γ} → CH.⊢ Γ ▻⋯▻ A → DG⟨ Γ ⁏ ∅ ⊢ A ⟩
ch→dg₀ = g→dg₀ ∘ ch→g

ch→dg : ∀ {A Γ Δ} → CH.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A → DG⟨ Γ ⁏ Δ ⊢ A ⟩
ch→dg = g→dg ∘ ch→g

ch→lg₀ : ∀ {x A Λ} → CH.⊢ A → LG⟨ ∅ ⁏ Λ ⊢ A ◎ x ⟩
ch→lg₀ = g→lg ∘ ch→g₀

ch→lg : ∀ {x A Γ Λ} → CH.⊢ Γ ▻⋯▻ A → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩
ch→lg = g→lg ∘ ch→g

-- Additional translations from Hilbert-style sequential.

hs₀→ch : ∀ {A} → HS⟨ ∅ ⊢ A ⟩ → CH.⊢ A
hs₀→ch = chs→ch ∘ hs₀→chs

hs→ch : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → CH.⊢ Γ ▻⋯▻ A
hs→ch = chs→ch ∘ hs→chs

hs→g : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → G⟨ Γ ⊢ A ⟩
hs→g = h→g ∘ hs→h

hs→dh₀ : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → DH⟨ Γ ⁏ ∅ ⊢ A ⟩
hs→dh₀ = h→dh₀ ∘ hs→h

hs→dh : ∀ {A Γ Δ} → HS⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩ → DH⟨ Γ ⁏ Δ ⊢ A ⟩
hs→dh = h→dh ∘ hs→h

hs→dg₀ : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → DG⟨ Γ ⁏ ∅ ⊢ A ⟩
hs→dg₀ = dh→dg ∘ hs→dh₀

hs→dg : ∀ {A Γ Δ} → HS⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩ → DG⟨ Γ ⁏ Δ ⊢ A ⟩
hs→dg = dh→dg ∘ hs→dh

hs→lg : ∀ {x A Γ Λ} → HS⟨ Γ ⊢ A ⟩ → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩
hs→lg = h→lg ∘ hs→h

-- Additional translations from Hilbert-style.

h₀→chs : ∀ {A} → H⟨ ∅ ⊢ A ⟩ → CHS.⊢ A
h₀→chs = ch→chs ∘ h₀→ch

h→chs : ∀ {A Γ} → H⟨ Γ ⊢ A ⟩ → CHS.⊢ Γ ▻⋯▻ A
h→chs = ch→chs ∘ h→ch

h→dhs₀ : ∀ {A Γ} → H⟨ Γ ⊢ A ⟩ → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩
h→dhs₀ = hs→dhs₀ ∘ h→hs

h→dhs : ∀ {A Γ Δ} → H⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩ → DHS⟨ Γ ⁏ Δ ⊢ A ⟩
h→dhs = hs→dhs ∘ h→hs

h→dg₀ : ∀ {A Γ} → H⟨ Γ ⊢ A ⟩ → DG⟨ Γ ⁏ ∅ ⊢ A ⟩
h→dg₀ = dh→dg ∘ h→dh₀

h→dg : ∀ {A Γ Δ} → H⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩ → DG⟨ Γ ⁏ Δ ⊢ A ⟩
h→dg = dh→dg ∘ h→dh

-- Additional translations from Gentzen-style.

g₀→chs : ∀ {A} → G⟨ ∅ ⊢ A ⟩ → CHS.⊢ A
g₀→chs = h₀→chs ∘ g→h

g→chs : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → CHS.⊢ Γ ▻⋯▻ A
g→chs = h→chs ∘ g→h

g₀→ch : ∀ {A} → G⟨ ∅ ⊢ A ⟩ → CH.⊢ A
g₀→ch = h₀→ch ∘ g→h

g→ch : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → CH.⊢ Γ ▻⋯▻ A
g→ch = h→ch ∘ g→h

g→hs : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → HS⟨ Γ ⊢ A ⟩
g→hs = h→hs ∘ g→h

g→dhs₀ : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩
g→dhs₀ = h→dhs₀ ∘ g→h

g→dhs : ∀ {A Γ Δ} → G⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩ → DHS⟨ Γ ⁏ Δ ⊢ A ⟩
g→dhs = h→dhs ∘ g→h

g→dh₀ : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → DH⟨ Γ ⁏ ∅ ⊢ A ⟩
g→dh₀ = h→dh₀ ∘ g→h

g→dh : ∀ {A Γ Δ} → G⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩ → DH⟨ Γ ⁏ Δ ⊢ A ⟩
g→dh = h→dh ∘ g→h

-- Additional translations from dyadic Hilbert-style sequential.

dhs₀₀→chs : ∀ {A} → DHS⟨ ∅ ⁏ ∅ ⊢ A ⟩ → CHS.⊢ A
dhs₀₀→chs = hs₀→chs ∘ dhs₀→hs

dhs₀→chs : ∀ {A Γ} → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩ → CHS.⊢ Γ ▻⋯▻ A
dhs₀→chs = hs→chs ∘ dhs₀→hs

dhs→chs : ∀ {A Γ Δ} → DHS⟨ Γ ⁏ Δ ⊢ A ⟩ → CHS.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A
dhs→chs = hs→chs ∘ dhs→hs

dhs₀₀→ch : ∀ {A} → DHS⟨ ∅ ⁏ ∅ ⊢ A ⟩ → CH.⊢ A
dhs₀₀→ch = hs₀→ch ∘ dhs₀→hs

dhs₀→ch : ∀ {A Γ} → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩ → CH.⊢ Γ ▻⋯▻ A
dhs₀→ch = hs→ch ∘ dhs₀→hs

dhs→ch : ∀ {A Γ Δ} → DHS⟨ Γ ⁏ Δ ⊢ A ⟩ → CH.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A
dhs→ch = hs→ch ∘ dhs→hs

dhs₀→h : ∀ {A Γ} → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩ → H⟨ Γ ⊢ A ⟩
dhs₀→h = hs→h ∘ dhs₀→hs

dhs→h : ∀ {A Γ Δ} → DHS⟨ Γ ⁏ Δ ⊢ A ⟩ → H⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩
dhs→h = hs→h ∘ dhs→hs

dhs₀→g : ∀ {A Γ} → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩ → G⟨ Γ ⊢ A ⟩
dhs₀→g = hs→g ∘ dhs₀→hs

dhs→g : ∀ {A Γ Δ} → DHS⟨ Γ ⁏ Δ ⊢ A ⟩ → G⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩
dhs→g = hs→g ∘ dhs→hs

dhs→dg : ∀ {A Γ Δ} → DHS⟨ Γ ⁏ Δ ⊢ A ⟩ → DG⟨ Γ ⁏ Δ ⊢ A ⟩
dhs→dg = dh→dg ∘ dhs→dh

dhs₀→lg : ∀ {x A Γ Λ} → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩ → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩
dhs₀→lg = hs→lg ∘ dhs₀→hs

dhs→lg : ∀ {x A Γ Δ Λ} → DHS⟨ Γ ⁏ Δ ⊢ A ⟩ → LG⟨ Γ ⧺ (□⋆ Δ) ⁏ Λ ⊢ A ◎ x ⟩
dhs→lg = hs→lg ∘ dhs→hs

-- Additional translations from dyadic Hilbert-style.

dh₀₀→chs : ∀ {A} → DH⟨ ∅ ⁏ ∅ ⊢ A ⟩ → CHS.⊢ A
dh₀₀→chs = h₀→chs ∘ dh₀→h

dh₀→chs : ∀ {A Γ} → DH⟨ Γ ⁏ ∅ ⊢ A ⟩ → CHS.⊢ Γ ▻⋯▻ A
dh₀→chs = h→chs ∘ dh₀→h

dh→chs : ∀ {A Γ Δ} → DH⟨ Γ ⁏ Δ ⊢ A ⟩ → CHS.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A
dh→chs = h→chs ∘ dh→h

dh₀₀→ch : ∀ {A} → DH⟨ ∅ ⁏ ∅ ⊢ A ⟩ → CH.⊢ A
dh₀₀→ch = h₀→ch ∘ dh₀→h

dh₀→ch : ∀ {A Γ} → DH⟨ Γ ⁏ ∅ ⊢ A ⟩ → CH.⊢ Γ ▻⋯▻ A
dh₀→ch = h→ch ∘ dh₀→h

dh→ch : ∀ {A Γ Δ} → DH⟨ Γ ⁏ Δ ⊢ A ⟩ → CH.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A
dh→ch = h→ch ∘ dh→h

dh₀→hs : ∀ {A Γ} → DH⟨ Γ ⁏ ∅ ⊢ A ⟩ → HS⟨ Γ ⊢ A ⟩
dh₀→hs = h→hs ∘ dh₀→h

dh→hs : ∀ {A Γ Δ} → DH⟨ Γ ⁏ Δ ⊢ A ⟩ → HS⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩
dh→hs = h→hs ∘ dh→h

dh₀→g : ∀ {A Γ} → DH⟨ Γ ⁏ ∅ ⊢ A ⟩ → G⟨ Γ ⊢ A ⟩
dh₀→g = h→g ∘ dh₀→h

dh→g : ∀ {A Γ Δ} → DH⟨ Γ ⁏ Δ ⊢ A ⟩ → G⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩
dh→g = h→g ∘ dh→h

dh₀→lg : ∀ {x A Γ Λ} → DH⟨ Γ ⁏ ∅ ⊢ A ⟩ → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩
dh₀→lg = h→lg ∘ dh₀→h

dh→lg : ∀ {x A Γ Δ Λ} → DH⟨ Γ ⁏ Δ ⊢ A ⟩ → LG⟨ Γ ⧺ (□⋆ Δ) ⁏ Λ ⊢ A ◎ x ⟩
dh→lg = h→lg ∘ dh→h

-- Additional translations from dyadic Gentzen-style.

dg₀₀→chs : ∀ {A} → DG⟨ ∅ ⁏ ∅ ⊢ A ⟩ → CHS.⊢ A
dg₀₀→chs = dh₀→chs ∘ dg→dh

dg₀→chs : ∀ {A Γ} → DG⟨ Γ ⁏ ∅ ⊢ A ⟩ → CHS.⊢ Γ ▻⋯▻ A
dg₀→chs = dh→chs ∘ dg→dh

dg→chs : ∀ {A Γ Δ} → DG⟨ Γ ⁏ Δ ⊢ A ⟩ → CHS.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A
dg→chs = dh→chs ∘ dg→dh

dg₀₀→ch : ∀ {A} → DG⟨ ∅ ⁏ ∅ ⊢ A ⟩ → CH.⊢ A
dg₀₀→ch = dh₀→ch ∘ dg→dh

dg₀→ch : ∀ {A Γ} → DG⟨ Γ ⁏ ∅ ⊢ A ⟩ → CH.⊢ Γ ▻⋯▻ A
dg₀→ch = dh→ch ∘ dg→dh

dg→ch : ∀ {A Γ Δ} → DG⟨ Γ ⁏ Δ ⊢ A ⟩ → CH.⊢ Γ ⧺ (□⋆ Δ) ▻⋯▻ A
dg→ch = dh→ch ∘ dg→dh

dg₀→hs : ∀ {A Γ} → DG⟨ Γ ⁏ ∅ ⊢ A ⟩ → HS⟨ Γ ⊢ A ⟩
dg₀→hs = dh₀→hs ∘ dg→dh

dg→hs : ∀ {A Γ Δ} → DG⟨ Γ ⁏ Δ ⊢ A ⟩ → HS⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩
dg→hs = dh→hs ∘ dg→dh

dg₀→h : ∀ {A Γ} → DG⟨ Γ ⁏ ∅ ⊢ A ⟩ → H⟨ Γ ⊢ A ⟩
dg₀→h = dh₀→h ∘ dg→dh

dg→h : ∀ {A Γ Δ} → DG⟨ Γ ⁏ Δ ⊢ A ⟩ → H⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩
dg→h = dh→h ∘ dg→dh

-- NOTE: Direct translation fails the termination check.
dg₀→g : ∀ {A Γ} → DG⟨ Γ ⁏ ∅ ⊢ A ⟩ → G⟨ Γ ⊢ A ⟩
dg₀→g = h→g ∘ dg₀→h

dg→g : ∀ {A Γ Δ} → DG⟨ Γ ⁏ Δ ⊢ A ⟩ → G⟨ Γ ⧺ (□⋆ Δ) ⊢ A ⟩
dg→g = h→g ∘ dg→h

dg→dhs : ∀ {A Γ Δ} → DG⟨ Γ ⁏ Δ ⊢ A ⟩ → DHS⟨ Γ ⁏ Δ ⊢ A ⟩
dg→dhs = dh→dhs ∘ dg→dh

dg₀→lg : ∀ {x A Γ Λ} → DG⟨ Γ ⁏ ∅ ⊢ A ⟩ → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩
dg₀→lg = g→lg ∘ dg₀→g

dg→lg : ∀ {x A Γ Δ Λ} → DG⟨ Γ ⁏ Δ ⊢ A ⟩ → LG⟨ Γ ⧺ (□⋆ Δ) ⁏ Λ ⊢ A ◎ x ⟩
dg→lg = g→lg ∘ dg→g

-- Additional translations from labelled Gentzen-style.

lg₀→chs : ∀ {x A Λ} → LG⟨ ∅ ⁏ Λ ⊢ A ◎ x ⟩ → CHS.⊢ A
lg₀→chs = h₀→chs ∘ lg→h

lg→chs : ∀ {x A Γ Λ} → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩ → CHS.⊢ Γ ▻⋯▻ A
lg→chs = h→chs ∘ lg→h

lg₀→ch : ∀ {x A Λ} → LG⟨ ∅ ⁏ Λ ⊢ A ◎ x ⟩ → CH.⊢ A
lg₀→ch = h₀→ch ∘ lg→h

lg→ch : ∀ {x A Γ Λ} → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩ → CH.⊢ Γ ▻⋯▻ A
lg→ch = h→ch ∘ lg→h

lg→hs : ∀ {x A Γ Λ} → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩ → HS⟨ Γ ⊢ A ⟩
lg→hs = h→hs ∘ lg→h

lg→dhs₀ : ∀ {x A Γ Λ} → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩ → DHS⟨ Γ ⁏ ∅ ⊢ A ⟩
lg→dhs₀ = h→dhs₀ ∘ lg→h

lg→dhs : ∀ {x A Γ Δ Λ} → LG⟨ Γ ⧺ (□⋆ Δ) ⁏ Λ ⊢ A ◎ x ⟩ → DHS⟨ Γ ⁏ Δ ⊢ A ⟩
lg→dhs = h→dhs ∘ lg→h

lg→dh₀ : ∀ {x A Γ Λ} → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩ → DH⟨ Γ ⁏ ∅ ⊢ A ⟩
lg→dh₀ = h→dh₀ ∘ lg→h

lg→dh : ∀ {x A Γ Δ Λ} → LG⟨ Γ ⧺ (□⋆ Δ) ⁏ Λ ⊢ A ◎ x ⟩ → DH⟨ Γ ⁏ Δ ⊢ A ⟩
lg→dh = h→dh ∘ lg→h

lg→dg₀ : ∀ {x A Γ Λ} → LG⟨ Γ ⁏ Λ ⊢ A ◎ x ⟩ → DG⟨ Γ ⁏ ∅ ⊢ A ⟩
lg→dg₀ = h→dg₀ ∘ lg→h

lg→dg : ∀ {x A Γ Δ Λ} → LG⟨ Γ ⧺ (□⋆ Δ) ⁏ Λ ⊢ A ◎ x ⟩ → DG⟨ Γ ⁏ Δ ⊢ A ⟩
lg→dg = h→dg ∘ lg→h

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module PiQ.AuxLemmas where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Data.Maybe
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import PiQ.Syntax
open import PiQ.Opsem

Lemma₁ : ∀ {A B C D v v' κ κ'} {c : A ↔ B} {c' : C ↔ D}
       → ［ c ∣ v ∣ κ ］◁ ↦ ⟨ c' ∣ v' ∣ κ' ⟩◁
       → A ≡ C × B ≡ D
Lemma₁ ↦⃖₁ = refl , refl
Lemma₁ ↦⃖₂ = refl , refl
Lemma₁ ↦⃖ηₓ₁ = refl , refl
Lemma₁ ↦⃖εₓ = refl , refl

Lemma₂ : ∀ {A B v v' κ κ'} {c c' : A ↔ B}
       → ［ c ∣ v ∣ κ ］◁ ↦ ⟨ c' ∣ v' ∣ κ' ⟩◁
       → c ≡ c' × κ ≡ κ'
Lemma₂ ↦⃖₁ = refl , refl
Lemma₂ ↦⃖₂ = refl , refl
Lemma₂ ↦⃖ηₓ₁ = refl , refl
Lemma₂ ↦⃖εₓ = refl , refl

Lemma₃ : ∀ {A B v v' κ} {c : A ↔ B}
       → ［ c ∣ v ∣ κ ］◁ ↦ ⟨ c ∣ v' ∣ κ ⟩◁
       → base c ⊎ dual c ⊎ A ≡ B
Lemma₃ (↦⃖₁ {b = b}) = inj₁ b
Lemma₃ ↦⃖₂ = inj₂ (inj₂ refl)
Lemma₃ ↦⃖ηₓ₁ = inj₂ (inj₁ tt)
Lemma₃ ↦⃖εₓ = inj₂ (inj₁ tt)

Lemma₄ : ∀ {A v v' κ} {c : A ↔ A}
       → ［ c ∣ v ∣ κ ］◁ ↦ ⟨ c ∣ v' ∣ κ ⟩◁
       → base c ⊎ c ≡ id↔
Lemma₄ (↦⃖₁ {b = b}) = inj₁ b
Lemma₄ ↦⃖₂ = inj₂ refl

Lemma₅ : ∀ {A B C D v v' κ κ'} {c : A ↔ B} {c' : C ↔ D}
       → ［ c ∣ v ∣ κ ］◁ ↦ ［ c' ∣ v' ∣ κ' ］▷
       → A ≡ C × B ≡ D
Lemma₅ ↦η₊₁ = refl , refl
Lemma₅ ↦η₊₂ = refl , refl

Lemma₆ : ∀ {A B v v' κ κ'} {c c' : A ↔ B}
       → ［ c ∣ v ∣ κ ］◁ ↦ ［ c' ∣ v' ∣ κ' ］▷
       → c ≡ c' × κ ≡ κ'
Lemma₆ ↦η₊₁ = refl , refl
Lemma₆ ↦η₊₂ = refl , refl

Lemma₇ : ∀ {A B v v' κ} {c : A ↔ B}
       → ［ c ∣ v ∣ κ ］◁ ↦ ［ c ∣ v' ∣ κ ］▷
       →  A ≡ 𝟘
Lemma₇ ↦η₊₁ = refl
Lemma₇ ↦η₊₂ = refl

Lemma₈ : ∀ {A B v κ} {c : A ↔ B}
       → ［ c ∣ v ∣ κ ］◁ ↦ ⊠
       → ¬ (base c)
Lemma₈ ↦⃖ηₓ₂ ()

Lemma₉ : ∀ {A B} {κ : Context} {v : ⟦ B ⟧} {v' : ⟦ A ⟧} {c : A ↔ B}
       → ［ c ∣ v ∣ κ ］◁ ↦ ⟨ c ∣ v' ∣ κ ⟩◁
       → ［ c ∣ v ∣ κ ］◁ ↦ ⊠
       → ⊥
Lemma₉ r' r with Lemma₈ r
Lemma₉ (↦⃖₁ {b = b}) r | nb = nb b
Lemma₉ (↦⃖ηₓ₁ {eq = eq}) (↦⃖ηₓ₂ {neq = neq}) | _ = ⊥-elim (neq eq)

Lemma₁₀ : ∀ {A B C D v v' κ κ'} {c : A ↔ B} {c' : C ↔ D}
        → ⟨ c ∣ v ∣ κ ⟩▷ ↦ ［ c' ∣ v' ∣ κ' ］▷
        → (A ≡ C × B ≡ D)
Lemma₁₀ ↦⃗₁ = refl , refl
Lemma₁₀ ↦⃗₂ = refl , refl
Lemma₁₀ ↦⃗ηₓ = refl , refl
Lemma₁₀ ↦⃗εₓ₁ = refl , refl

Lemma₁₁ : ∀ {A B v v' κ κ'} {c c' : A ↔ B}
        → ⟨ c ∣ v ∣ κ ⟩▷ ↦ ［ c' ∣ v' ∣ κ' ］▷
        → c ≡ c' × κ ≡ κ'
Lemma₁₁ ↦⃗₁ = refl , refl
Lemma₁₁ ↦⃗₂ = refl , refl
Lemma₁₁ ↦⃗ηₓ = refl , refl
Lemma₁₁ ↦⃗εₓ₁ = refl , refl

Lemma₁₂ : ∀ {A B v v' κ} {c : A ↔ B}
        → (r : ⟨ c ∣ v ∣ κ ⟩▷ ↦ ［ c ∣ v' ∣ κ ］▷)
        → base c ⊎ dual c ⊎ A ≡ B
Lemma₁₂ (↦⃗₁ {b = b}) = inj₁ b
Lemma₁₂ ↦⃗₂ = inj₂ (inj₂ refl)
Lemma₁₂ ↦⃗ηₓ = inj₂ (inj₁ tt)
Lemma₁₂ ↦⃗εₓ₁ = inj₂ (inj₁ tt)

Lemma₁₃ : ∀ {A v v' κ} {c : A ↔ A}
        → (r : ⟨ c ∣ v ∣ κ ⟩▷ ↦ ［ c ∣ v' ∣ κ ］▷)
        → base c ⊎ c ≡ id↔
Lemma₁₃ (↦⃗₁ {b = b}) = inj₁ b
Lemma₁₃ ↦⃗₂ = inj₂ refl


text:
{-# OPTIONS --universe-polymorphism #-}

module NiceGoals where

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

postulate
  Level : Set
  zero : Level
  suc  : (i : Level) → Level
  _⊔_ : Level → Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX _⊔_ #-}

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

record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Carrier → Carrier → Set ℓ
    _∙_     : Carrier → Carrier → Carrier
    ε       : Carrier

module M (rm : RawMonoid zero zero) where

  open RawMonoid rm

  thm : ∀ x → x ∙ ε ≈ x
  thm = {!!}

  -- agda2-goal-and-context:

  -- rm : RawMonoid zero zero
  -- ------------------------
  -- Goal: (x : RawMonoid.Carrier rm) →
  --       RawMonoid._≈_ rm (RawMonoid._∙_ rm x (RawMonoid.ε rm)) x

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

record RawMonoid′ : Set₁ where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set
    _≈_     : Carrier → Carrier → Set
    _∙_     : Carrier → Carrier → Carrier
    ε       : Carrier

module M′ (rm : RawMonoid′) where

  open RawMonoid′ rm

  thm′ : ∀ x → x ∙ ε ≈ x
  thm′ = {!!}

  -- agda2-goal-and-context:

  -- rm : RawMonoid′
  -- ---------------
  -- Goal: (x : Carrier) → x ∙ ε ≈ x

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

-- UP isn't relevant.

record RawMonoid″ (Carrier : Set) : Set₁ where
  infixl 7 _∙_
  infix  4 _≈_
  field
    _≈_     : Carrier → Carrier → Set
    _∙_     : Carrier → Carrier → Carrier
    ε       : Carrier

data Bool : Set where
  true false : Bool

data List (A : Set) : Set where
  []  :                        List A
  _∷_ : (x : A)(xs : List A) → List A

module M″ (rm : RawMonoid″ (List Bool)) where

  open RawMonoid″ rm

  thm″ : ∀ x → x ∙ ε ≈ x
  thm″ = {!!}

  -- agda2-goal-and-context:

  -- rm : RawMonoid″ (List Bool)
  -- ---------------------------
  -- Goal: (x : List Bool) →
  --       RawMonoid″._≈_ rm (RawMonoid″._∙_ rm x (RawMonoid″.ε rm)) x

module M₁ (Z : Set₁) where

  postulate
    P : Set
    Q : Set → Set

module M₂ (X Y : Set) where

  module M₁′ = M₁ Set
  open M₁′

  p : P
  p = {!!}

  q : Q X
  q = {!!}

postulate X : Set

pp : M₂.M₁′.P X X
pp = {!!}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
open import FRP.JS.Nat using ( ℕ ; suc ; _+_ ; _≟_ ; _<_ )
open import FRP.JS.Array using ( Array ; IArray ; [] ; _∷_ ; array ; ⟨⟩ ; ⟨_ ; _,_ ; _⟩ ; lookup ; lookup? ; map ; filter ; _≟[_]_ ; _⊆[_]_ ; _++_ )
open import FRP.JS.Bool using ( Bool ; not )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing ) renaming ( _≟[_]_ to _≟?[_]_ )
open import FRP.JS.QUnit using ( TestSuite ; ok ; test ; _,_ )

module FRP.JS.Test.Array where

infixr 2 _≟*_

_≟*_ : Array ℕ → Array ℕ → Bool
xs ≟* ys = xs ≟[ _≟_ ] ys

_⊆*_ : Array ℕ → Array ℕ → Bool
xs ⊆* ys = xs ⊆[ _≟_ ] ys

_≟?_ : Maybe ℕ → Maybe ℕ → Bool
xs ≟? ys = xs ≟?[ _≟_ ] ys

iincr : ∀ {m n} → IArray ℕ m n → IArray ℕ m n
iincr []       = []
iincr (n ∷ ns) = suc n ∷ iincr ns

incr : Array ℕ → Array ℕ
incr (array ns) = array (iincr ns)

⟨0⟩ = ⟨ 0 ⟩
⟨1⟩ = ⟨ 1 ⟩
⟨2⟩ = ⟨ 2 ⟩
⟨3⟩ = ⟨ 3 ⟩
⟨0,1⟩ = ⟨ 0 , 1 ⟩
⟨0,2⟩ = ⟨ 0 , 2 ⟩
⟨1,2⟩ = ⟨ 1 , 2 ⟩
⟨2,3⟩ = ⟨ 2 , 3 ⟩
⟨0,1,2⟩ = ⟨ 0 , 1 , 2 ⟩

tests : TestSuite
tests =
  ( test "≟"
    ( ok "⟨⟩ ≟ ⟨⟩" (⟨⟩ ≟* ⟨⟩)
    , ok "⟨⟩ ≟ ⟨0⟩" (not (⟨⟩ ≟* ⟨0⟩))
    , ok "⟨0⟩ ≟ ⟨⟩" (not (⟨0⟩ ≟* ⟨⟩))
    , ok "⟨0⟩ ≟ ⟨0⟩" (⟨0⟩ ≟* ⟨0⟩)
    , ok "⟨⟩ ≟ ⟨0,1⟩" (not (⟨⟩ ≟* ⟨0,1⟩))
    , ok "⟨0,1⟩ ≟ ⟨⟩" (not (⟨0,1⟩ ≟* ⟨⟩))
    , ok "⟨1⟩ ≟ ⟨0,1⟩" (not (⟨1⟩ ≟* ⟨0,1⟩))
    , ok "⟨0⟩ ≟ ⟨0,1⟩" (not (⟨0⟩ ≟* ⟨0,1⟩))
    , ok "⟨0,1⟩ ≟ ⟨0,1⟩" (⟨0,1⟩ ≟* ⟨0,1⟩)
    , ok "⟨0,1⟩ ≟ ⟨0,2⟩" (not (⟨0,1⟩ ≟* ⟨0,2⟩))
    , ok "⟨0,1⟩ ≟ ⟨1,2⟩" (not (⟨0,1⟩ ≟* ⟨1,2⟩)) )
  , test "⊆"
    ( ok "⟨⟩ ⊆ ⟨⟩" (⟨⟩ ⊆* ⟨⟩)
    , ok "⟨⟩ ⊆ ⟨0⟩" (⟨⟩ ⊆* ⟨0⟩)
    , ok "⟨0⟩ ⊆ ⟨⟩" (not (⟨0⟩ ⊆* ⟨⟩))
    , ok "⟨0⟩ ⊆ ⟨0⟩" (⟨0⟩ ⊆* ⟨0⟩)
    , ok "⟨⟩ ⊆ ⟨0,1⟩" (⟨⟩ ⊆* ⟨0,1⟩)
    , ok "⟨0,1⟩ ⊆ ⟨⟩" (not (⟨0,1⟩ ⊆* ⟨⟩))
    , ok "⟨1⟩ ⊆ ⟨0,1⟩" (not (⟨1⟩ ⊆* ⟨0,1⟩))
    , ok "⟨0⟩ ⊆ ⟨0,1⟩" (⟨0⟩ ⊆* ⟨0,1⟩)
    , ok "⟨0,1⟩ ⊆ ⟨0,1⟩" (⟨0,1⟩ ⊆* ⟨0,1⟩)
    , ok "⟨0,1⟩ ⊆ ⟨0,2⟩" (not (⟨0,1⟩ ⊆* ⟨0,2⟩))
    , ok "⟨0,1⟩ ⊆ ⟨1,2⟩" (not (⟨0,1⟩ ⊆* ⟨1,2⟩)) )
  , test "++"
    ( ok "⟨⟩ ++ ⟨⟩" (⟨⟩ ++ ⟨⟩ ≟* ⟨⟩)
    , ok "⟨⟩ ++ ⟨2⟩" (⟨⟩ ++ ⟨2⟩ ≟* ⟨2⟩)
    , ok "⟨⟩ ++ ⟨1,2⟩" (⟨⟩ ++ ⟨1,2⟩ ≟* ⟨1,2⟩)
    , ok "⟨0⟩ ++ ⟨⟩" (⟨0⟩ ++ ⟨⟩ ≟* ⟨0⟩)
    , ok "⟨0⟩ ++ ⟨2⟩" (⟨0⟩ ++ ⟨2⟩ ≟* ⟨0,2⟩)
    , ok "⟨0⟩ ++ ⟨1,2⟩" (⟨0⟩ ++ ⟨1,2⟩ ≟* ⟨0,1,2⟩)
    , ok "⟨0,1⟩ ++ ⟨⟩" (⟨0,1⟩ ++ ⟨⟩ ≟* ⟨0,1⟩)
    , ok "⟨0,1⟩ ++ ⟨2⟩" (⟨0,1⟩ ++ ⟨2⟩ ≟* ⟨0,1,2⟩) )
  , test "lookup"
    ( ok "lookup? ⟨1,2⟩ 0" (lookup? ⟨1,2⟩ 0 ≟? just 1)
    , ok "lookup? ⟨1,2⟩ 1" (lookup? ⟨1,2⟩ 1 ≟? just 2)
    , ok "lookup? ⟨1,2⟩ 2" (lookup? ⟨1,2⟩ 2 ≟? nothing)
    , ok "lookup ⟨1,2⟩ 0" (lookup ⟨1,2⟩ 0 ≟ 1)
    , ok "lookup ⟨1,2⟩ 1" (lookup ⟨1,2⟩ 1 ≟ 2) )
  , test "map"
    ( ok "map suc ⟨⟩" (map suc ⟨⟩ ≟* ⟨⟩)
    , ok "map suc ⟨1⟩" (map suc ⟨1⟩ ≟* ⟨2⟩)
    , ok "map suc ⟨1,2⟩" (map suc ⟨1,2⟩ ≟* ⟨2,3⟩)
    , ok "incr ⟨⟩" (map suc ⟨⟩ ≟* incr ⟨⟩)
    , ok "incr ⟨1⟩" (map suc ⟨1⟩ ≟* incr ⟨1⟩)
    , ok "incr ⟨1,2⟩" (map suc ⟨1,2⟩ ≟* incr ⟨1,2⟩) )
  , test "filter"
    ( ok "filter 0< ⟨1,2⟩" (filter (_<_ 0) ⟨1,2⟩ ≟* ⟨1,2⟩)
    , ok "filter 1< ⟨1,2⟩" (filter (_<_ 1) ⟨1,2⟩ ≟* ⟨2⟩)
    , ok "filter 2< ⟨1,2⟩" (filter (_<_ 2) ⟨1,2⟩ ≟* ⟨⟩) ) )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
variable
  S : Set

data D (A : Set) : Set1 where
  d : S → D A


text:
-- Andreas, 2020-04-19, issue #4560, raised by Andrea
-- Having both matching on constructor and copattern matching
-- for non-eta records leads to loss of subject reduction.

open import Agda.Builtin.Equality

postulate
  A : Set
  a : A

record R : Set where
  constructor con
  no-eta-equality
  field
    X Y : A

foo : R → A
foo (con x y) = x

-- Expected error here:
-- Pattern matching on no-eta record types is by default not allowed
-- when checking that the pattern con x y has type R

bar : R
bar .R.X = a
bar .R.Y = a

test : foo bar ≡ a
test = refl

-- Problem was:
-- foo bar != a of type A
-- when checking that the expression refl has type foo bar ≡ a

max_forks_repo_name: shlevy/agda


text:
open import Prelude
open import core
open import contexts

module lemmas-freshG where
  -- the def above buries the sort of obvious pattern matching we'd like to
  -- do on the freshness in the conclusion, so we need lemmas that extract
  -- it for each constructor
  freshΓ-asc : {A : Set} → {Γ : A ctx} → ∀{e τ} → freshΓ Γ (e ·: τ) → freshΓ Γ e
  freshΓ-asc fr x x₁ with fr x x₁
  freshΓ-asc fr x x₁ | FRHAsc qq = qq

  freshΓ-ap1 : {A : Set} → {Γ : A ctx} → ∀{e1 e2} → freshΓ Γ (e1 ∘ e2) → freshΓ Γ e1
  freshΓ-ap1 fr x y with fr x y
  freshΓ-ap1 fr x y | FRHAp qq qq₁ = qq

  freshΓ-ap2 : {A : Set} → {Γ : A ctx} → ∀{e1 e2} → freshΓ Γ (e1 ∘ e2) → freshΓ Γ e2
  freshΓ-ap2 fr x y with fr x y
  freshΓ-ap2 fr x y | FRHAp qq qq₁ = qq₁

  freshΓ-nehole : {A : Set} → {Γ : A ctx} → ∀{e u} → freshΓ Γ (⦇⌜ e ⌟⦈[ u ]) → freshΓ Γ e
  freshΓ-nehole fr x y with fr x y
  freshΓ-nehole fr x y | FRHNEHole qq = qq

  freshΓ-lam1 : {A : Set} → {Γ : A ctx} → ∀{e x} → freshΓ Γ (·λ x e) → freshΓ Γ e
  freshΓ-lam1 fr x y with fr x y
  freshΓ-lam1 fr x y | FRHLam1 x₂ qq = qq

  freshΓ-lam2 : {A : Set} → {Γ : A ctx} → ∀{e τ x} → freshΓ Γ (·λ_[_]_ x τ e) → freshΓ Γ e
  freshΓ-lam2 fr x y with fr x y
  freshΓ-lam2 fr x y | FRHLam2 x₂ qq = qq

  lem-fresh-lam1 : ∀{x e} → freshe x (·λ x e) → ⊥
  lem-fresh-lam1 (FRHLam1 x₁ f) = x₁ refl

  lem-fresh-lam2 : ∀{x τ e} → freshe x (·λ x [ τ ] e) → ⊥
  lem-fresh-lam2 (FRHLam2 x₁ f) = x₁ refl

  freshΓ-pair1 : {A : Set} → {Γ : A ctx} → ∀{e1 e2} → freshΓ Γ ⟨ e1 , e2 ⟩ → freshΓ Γ e1
  freshΓ-pair1 fr x y with fr x y
  freshΓ-pair1 fr x y | FRHPair qq qq₁ = qq

  freshΓ-pair2 : {A : Set} → {Γ : A ctx} → ∀{e1 e2} → freshΓ Γ ⟨ e1 , e2 ⟩ → freshΓ Γ e2
  freshΓ-pair2 fr x y with fr x y
  freshΓ-pair2 fr x y | FRHPair qq qq₁ = qq₁

  freshΓ-fst : {A : Set} → {Γ : A ctx} → ∀{e} → freshΓ Γ (fst e) → freshΓ Γ e
  freshΓ-fst fr x x₁ with fr x x₁
  freshΓ-fst fr x x₁ | FRHFst qq = qq

  freshΓ-snd : {A : Set} → {Γ : A ctx} → ∀{e} → freshΓ Γ (snd e) → freshΓ Γ e
  freshΓ-snd fr x x₁ with fr x x₁
  freshΓ-snd fr x x₁ | FRHSnd qq = qq

  fresh-freshΓ : {A : Set} {τ : A} → ∀{x e} → freshe x e → freshΓ (■ (x , τ)) e
  fresh-freshΓ fr x y with lem-dom-eq y
  fresh-freshΓ fr x y | refl = fr

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
open import Data.Nat --using (ℕ; suc; zero; _≤?_; _≤_; s≤s; z≤n)
open import Data.Bool using (true; false)
--open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary -- using (Dec; yes; no; _because_)
open import Relation.Nullary.Decidable --using (True; fromWitness)
--open import Data.Unit using (tt)

-- stack exec -- agda -c --ghc-dont-call-ghc --no-main nats.agda

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : (x : A) → Maybe A
{-# COMPILE GHC Maybe = data Maybe (Nothing | Just) #-}

n-3 : (n : ℕ) → .{3≤n : True (3 ≤? n)} → ℕ
n-3 (suc (suc (suc n))) = n

exportFunc : ℕ → Maybe ℕ
exportFunc n with 3 ≤? n
... | yes 3≤n = just (n-3 n {fromWitness 3≤n})
... | no ¬3≤n = nothing
{-# COMPILE GHC exportFunc as exportFunc #-}


text:
module dependentProduct2 where

postulate A : Set
postulate B : A -> Set

data AB : Set where
  p : (a : A) -> B a -> AB

π0 : AB -> A
π0 (p a b) = a

π1 : (ab : AB) -> B (π0 ab)
π1 (p a b) = b

postulate a : A
postulate b : B a

ab : AB
ab = p a b

postulate ab' : AB

a' : A
a' = π0 ab'

b' : B a'
b' = π1 ab'

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics