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

module Util where

open import Agda.Primitive       using (Level)
open import Data.Fin             using (Fin; #_) renaming (suc to fsuc)
open import Data.Bool            using (Bool; true; false; if_then_else_)
open import Data.List            using (List; concat; replicate; []; _∷_)
open import Data.Maybe           using (Maybe; just; nothing)
open import Data.Nat             using (ℕ; suc; _*_; _<ᵇ_)
open import Data.Product         using (_×_; _,_)
open import Data.Vec             using (Vec; _∷_; []) renaming (concat to cat; replicate to rep)
open import Function             using (_∘_)
open import Relation.Nullary     using (yes; no; ¬_)
open import Relation.Unary       using (Pred; Decidable)

repeat : {ℓ : Level} {A : Set ℓ} → (n : ℕ) → List A → List A
repeat n = concat ∘ replicate n

repeatV : {ℓ : Level} {A : Set ℓ} {k : ℕ} → (n : ℕ) → Vec A k → Vec A (n * k)
repeatV n = cat ∘ rep {n = n}

-- return index of first element that satisfies predicate or last element if none do
findIndex : {a ℓ : Level} {A : Set a} {n : ℕ} {P : Pred A ℓ} → Decidable P → Vec A (suc n) → Fin (suc n)
findIndex _ (x ∷ [])     = # 0
findIndex P (x ∷ y ∷ ys) with P x
... | yes _ = # 0
... | no  _ = fsuc (findIndex P (y ∷ ys))

-- Returns a list of all adjacent pairs in the original list.
pairs : {ℓ : Level} {A : Set ℓ} → List A → List (A × A)
pairs []           = []
pairs (x ∷ [])     = []
pairs (x ∷ y ∷ xs) = (x , y) ∷ pairs (y ∷ xs)

-- Basic Boolean Filter and Elem
filter : {ℓ : Level} {A : Set ℓ} → (A → Bool) → List A → List A
filter f []       = []
filter f (x ∷ xs) = if f x then x ∷ filter f xs else filter f xs

infix 4 _∈_via_
_∈_via_ : {ℓ : Level} {A : Set ℓ} → A → List A → (A → A → Bool) → Bool
x ∈ []     via f = false
x ∈ y ∷ ys via f = if f x y then true else x ∈ ys via f

concatMaybe : {ℓ : Level} {A : Set ℓ} → List (Maybe A) → List A
concatMaybe []             = []
concatMaybe (nothing ∷ xs) = concatMaybe xs
concatMaybe (just x  ∷ xs) = x ∷ concatMaybe xs

listMin : {ℓ : Level} {A : Set ℓ} → (A → ℕ) → List A → Maybe A
listMin f [] = nothing
listMin f (x ∷ xs) with listMin f xs
... | nothing = just x
... | just y  = if f x <ᵇ f y then just x else just y


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homomorphism proofs for negation over polynomials
------------------------------------------------------------------------

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

open import Tactic.RingSolver.Core.Polynomial.Parameters

module Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation
  {r₁ r₂ r₃ r₄}
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where

open import Data.Product          using (_,_)
open import Data.Vec              using (Vec)
open import Data.Nat              using (_<′_)
open import Data.Nat.Induction

open import Function

open Homomorphism homo
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
open import Tactic.RingSolver.Core.Polynomial.Reasoning to
open import Tactic.RingSolver.Core.Polynomial.Base from
open import Tactic.RingSolver.Core.Polynomial.Semantics homo

⊟-step-hom : ∀ {n} (a : Acc _<′_ n) → (xs : Poly n) → ∀ ρ → ⟦ ⊟-step a xs ⟧ ρ ≈ - (⟦ xs ⟧ ρ)
⊟-step-hom (acc _ ) (Κ x  ⊐ i≤n) ρ = -‿homo x
⊟-step-hom (acc wf) (⅀ xs ⊐ i≤n) ρ′ =
  let (ρ , ρs) = drop-1 i≤n ρ′
      neg-zero =
        begin
          0#
        ≈⟨ sym (zeroʳ _) ⟩
          - 0# * 0#
        ≈⟨ -‿*-distribˡ 0# 0# ⟩
          - (0# * 0#)
        ≈⟨ -‿cong (zeroˡ 0#) ⟩
          - 0#
        ∎
  in
  begin
    ⟦ poly-map (⊟-step (wf _ i≤n)) xs ⊐↓ i≤n ⟧ ρ′
  ≈⟨ ⊐↓-hom (poly-map (⊟-step (wf _ i≤n)) xs) i≤n ρ′ ⟩
    ⅀?⟦ poly-map (⊟-step  (wf _ i≤n)) xs ⟧ (ρ , ρs)
  ≈⟨ poly-mapR ρ ρs (⊟-step (wf _ i≤n)) -_ (-‿cong) (λ x y → *-comm x (- y) ⟨ trans ⟩ -‿*-distribˡ y x ⟨ trans ⟩ -‿cong (*-comm _ _)) (λ x y → sym (-‿+-comm x y)) (flip (⊟-step-hom (wf _ i≤n)) ρs) (sym neg-zero ) xs ⟩
    - ⅀⟦ xs ⟧ (ρ , ρs)
  ∎

⊟-hom : ∀ {n}
      → (xs : Poly n)
      → (Ρ : Vec Carrier n)
      → ⟦ ⊟ xs ⟧ Ρ ≈ - ⟦ xs ⟧ Ρ
⊟-hom = ⊟-step-hom (<′-wellFounded _)

ext: agda


text:
------------------------------------------------------------------------
-- Some simple substitution combinators
------------------------------------------------------------------------

-- Given a term type which supports weakening and transformation of
-- variables to terms various substitutions are defined and various
-- lemmas proved.

open import Data.Universe.Indexed

module deBruijn.Substitution.Function.Simple
  {i u e} {Uni : IndexedUniverse i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Function.Basics
open import deBruijn.Substitution.Function.Map
open import Function as F using (_$_)
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open P.≡-Reasoning

-- Simple substitutions.

record Simple {t} (T : Term-like t) : Set (i ⊔ u ⊔ e ⊔ t) where

  open Term-like T

  field

    -- Weakens terms.
    weaken : ∀ {Γ} {σ : Type Γ} → [ T ⟶ T ] ŵk[ σ ]

  -- A synonym.

  weaken[_] : ∀ {Γ} (σ : Type Γ) → [ T ⟶ T ] ŵk[ σ ]
  weaken[_] _ = weaken

  field

    -- Takes variables to terms.
    var : [ Var ⟶⁼ T ]

    -- A property relating weaken and var.
    weaken-var : ∀ {Γ σ τ} (x : Γ ∋ τ) →
                 weaken[ σ ] · (var · x) ≅-⊢ var · suc[ σ ] x

  -- Weakens substitutions.

  wk-subst : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk[ σ ])
  wk-subst ρ = map weaken ρ

  wk-subst[_] : ∀ {Γ Δ} σ {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk[ σ ])
  wk-subst[ _ ] = wk-subst

  -- N-ary weakening of substitutions.

  wk-subst⁺ : ∀ {Γ Δ} Δ⁺ {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk⁺ Δ⁺)
  wk-subst⁺ ε        ρ = ρ
  wk-subst⁺ (Δ⁺ ▻ σ) ρ = wk-subst (wk-subst⁺ Δ⁺ ρ)

  wk-subst₊ : ∀ {Γ Δ} Δ₊ {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk₊ Δ₊)
  wk-subst₊ ε        ρ = ρ
  wk-subst₊ (σ ◅ Δ₊) ρ = wk-subst₊ Δ₊ (wk-subst ρ)

  -- Lifting.

  infixl 10 _↑_
  infix  10 _↑

  _↑_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → ∀ σ → Sub T (ρ̂ ↑̂ σ)
  ρ ↑ _ =
    P.subst (Sub T)
            (≅-⇨̂-⇒-≡ $ ▻̂-cong P.refl P.refl
                         (P.sym $ corresponds var zero))
            (wk-subst ρ ▻⇨ var · zero)

  _↑ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ↑̂ σ)
  ρ ↑ = ρ ↑ _

  -- N-ary lifting.

  infixl 10 _↑⁺_ _↑₊_

  _↑⁺_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → ∀ Γ⁺ → Sub T (ρ̂ ↑̂⁺ Γ⁺)
  ρ ↑⁺ ε        = ρ
  ρ ↑⁺ (Γ⁺ ▻ σ) = (ρ ↑⁺ Γ⁺) ↑

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

  -- The identity substitution.

  id[_] : ∀ Γ → Sub T îd[ Γ ]
  id[ ε     ] = ε⇨
  id[ Γ ▻ σ ] = id[ Γ ] ↑

  id : ∀ {Γ} → Sub T îd[ Γ ]
  id = id[ _ ]

  -- N-ary weakening.

  wk⁺ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Sub T (ŵk⁺ Γ⁺)
  wk⁺ ε        = id
  wk⁺ (Γ⁺ ▻ σ) = wk-subst (wk⁺ Γ⁺)

  wk₊ : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → Sub T (ŵk₊ Γ₊)
  wk₊ Γ₊ = wk-subst₊ Γ₊ id

  -- Weakening.

  wk[_] : ∀ {Γ} (σ : Type Γ) → Sub T ŵk[ σ ]
  wk[ σ ] = wk⁺ (ε ▻ σ)

  wk : ∀ {Γ} {σ : Type Γ} → Sub T ŵk[ σ ]
  wk = wk[ _ ]

  private

    -- Three possible definitions of wk coincide definitionally.

    coincide₁ : ∀ {Γ} {σ : Type Γ} → wk⁺ (ε ▻ σ) ≡ wk₊ (σ ◅ ε)
    coincide₁ = P.refl

    coincide₂ : ∀ {Γ} {σ : Type Γ} → wk⁺ (ε ▻ σ) ≡ wk-subst id
    coincide₂ = P.refl

  -- A substitution which only replaces the first variable.

  sub : ∀ {Γ σ} (t : Γ ⊢ σ) → Sub T (ŝub ⟦ t ⟧)
  sub t = id ▻⇨ t

  abstract

    -- Unfolding lemma for _↑.

    unfold-↑ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) →
               ρ ↑ σ ≅-⇨ wk-subst[ σ / ρ ] ρ ▻⇨[ σ ] var · zero
    unfold-↑ _ =
      drop-subst-Sub F.id
        (≅-⇨̂-⇒-≡ $ ▻̂-cong P.refl P.refl (P.sym $ corresponds var zero))

  -- Some congruence lemmas.

  weaken-cong : ∀ {Γ₁ σ₁ τ₁} {t₁ : Γ₁ ⊢ τ₁}
                  {Γ₂ σ₂ τ₂} {t₂ : Γ₂ ⊢ τ₂} →
                σ₁ ≅-Type σ₂ → t₁ ≅-⊢ t₂ →
                weaken[ σ₁ ] · t₁ ≅-⊢ weaken[ σ₂ ] · t₂
  weaken-cong P.refl P.refl = P.refl

  var-cong : ∀ {Γ₁ σ₁} {x₁ : Γ₁ ∋ σ₁}
               {Γ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} →
               x₁ ≅-∋ x₂ → var · x₁ ≅-⊢ var · x₂
  var-cong P.refl = P.refl

  wk-subst-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                    {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
                  σ₁ ≅-Type σ₂ → ρ₁ ≅-⇨ ρ₂ →
                  wk-subst[ σ₁ ] ρ₁ ≅-⇨ wk-subst[ σ₂ ] ρ₂
  wk-subst-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] =
    [ P.refl ]

  abstract

    wk-subst⁺-cong : ∀ {Γ₁ Δ₁ Γ⁺₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                       {Γ₂ Δ₂ Γ⁺₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
                     Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ₁ ≅-⇨ ρ₂ →
                     wk-subst⁺ Γ⁺₁ ρ₁ ≅-⇨ wk-subst⁺ Γ⁺₂ ρ₂
    wk-subst⁺-cong {Γ⁺₁ = ε} {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] =
      [ P.refl ]
    wk-subst⁺-cong {Γ⁺₁ = Γ⁺₁ ▻ σ} P.refl ρ₁≅ρ₂ =
      wk-subst-cong (P.refl {x = [ σ ]})
                    (wk-subst⁺-cong (P.refl {x = [ Γ⁺₁ ]}) ρ₁≅ρ₂)

    wk-subst₊-cong : ∀ {Γ₁ Δ₁ Γ₊₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                       {Γ₂ Δ₂ Γ₊₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
                     Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ₁ ≅-⇨ ρ₂ →
                     wk-subst₊ Γ₊₁ ρ₁ ≅-⇨ wk-subst₊ Γ₊₂ ρ₂
    wk-subst₊-cong {Γ₊₁ = ε} {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] =
      [ P.refl ]
    wk-subst₊-cong {Γ₊₁ = σ ◅ Γ₊₁} P.refl ρ₁≅ρ₂ =
      wk-subst₊-cong (P.refl {x = [ Γ₊₁ ]}) (wk-subst-cong P.refl ρ₁≅ρ₂)

    ↑-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {σ₁}
               {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {σ₂} →
             ρ₁ ≅-⇨ ρ₂ → σ₁ ≅-Type σ₂ → ρ₁ ↑ σ₁ ≅-⇨ ρ₂ ↑ σ₂
    ↑-cong {ρ₁ = ρ₁} {σ₁} {ρ₂ = ρ₂} {σ₂} ρ₁≅ρ₂ σ₁≅σ₂ =
      let lemma = /-cong σ₁≅σ₂ ρ₁≅ρ₂ in
      ρ₁ ↑ σ₁                               ≅-⟶⟨ unfold-↑ ρ₁ ⟩
      wk-subst ρ₁ ▻⇨ var · zero[ σ₁ / ρ₁ ]  ≅-⟶⟨ ▻⇨-cong σ₁≅σ₂ (wk-subst-cong lemma ρ₁≅ρ₂) (var-cong (zero-cong lemma)) ⟩
      wk-subst ρ₂ ▻⇨ var · zero[ σ₂ / ρ₂ ]  ≅-⟶⟨ sym-⟶ $ unfold-↑ ρ₂ ⟩
      ρ₂ ↑ σ₂                               ∎-⟶

    ↑⁺-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {Γ⁺₁}
                {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {Γ⁺₂} →
              ρ₁ ≅-⇨ ρ₂ → Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ₁ ↑⁺ Γ⁺₁ ≅-⇨ ρ₂ ↑⁺ Γ⁺₂
    ↑⁺-cong {ρ₁ = _ , _} {Γ⁺₁ = ε} {ρ₂ = ._ , _} [ P.refl ] P.refl =
      [ P.refl ]
    ↑⁺-cong {Γ⁺₁ = Γ⁺ ▻ σ} ρ₁≅ρ₂ P.refl =
      ↑-cong (↑⁺-cong ρ₁≅ρ₂ (P.refl {x = [ Γ⁺ ]})) P.refl

    ↑₊-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {Γ₊₁}
                {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {Γ₊₂} →
              ρ₁ ≅-⇨ ρ₂ → Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ₁ ↑₊ Γ₊₁ ≅-⇨ ρ₂ ↑₊ Γ₊₂
    ↑₊-cong {ρ₁ = _ , _} {Γ₊₁ = ε} {ρ₂ = ._ , _} [ P.refl ] P.refl =
      [ P.refl ]
    ↑₊-cong {Γ₊₁ = σ ◅ Γ₊} ρ₁≅ρ₂ P.refl =
      ↑₊-cong (↑-cong ρ₁≅ρ₂ P.refl) (P.refl {x = [ Γ₊ ]})

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

  wk⁺-cong : ∀ {Γ₁} {Γ⁺₁ : Ctxt⁺ Γ₁} {Γ₂} {Γ⁺₂ : Ctxt⁺ Γ₂} →
             Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → wk⁺ Γ⁺₁ ≅-⇨ wk⁺ Γ⁺₂
  wk⁺-cong P.refl = [ P.refl ]

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

  wk-cong : ∀ {Γ₁} {σ₁ : Type Γ₁} {Γ₂} {σ₂ : Type Γ₂} →
            σ₁ ≅-Type σ₂ → wk[ σ₁ ] ≅-⇨ wk[ σ₂ ]
  wk-cong P.refl = [ P.refl ]

  sub-cong : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁} {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
             t₁ ≅-⊢ t₂ → sub t₁ ≅-⇨ sub t₂
  sub-cong P.refl = [ P.refl ]

  abstract

    -- Some lemmas relating variables to lifting.

    /∋-↑ : ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ▻ σ ∋ τ) (ρ : Sub T ρ̂) →
           x /∋ ρ ↑ ≅-⊢ x /∋ (wk-subst[ σ / ρ ] ρ ▻⇨ var · zero)
    /∋-↑ x ρ = /∋-cong (P.refl {x = [ x ]}) (unfold-↑ ρ)

    zero-/∋-↑ : ∀ {Γ Δ} σ {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) →
                zero[ σ ] /∋ ρ ↑ ≅-⊢ var · zero[ σ / ρ ]
    zero-/∋-↑ σ ρ = begin
      [ zero[ σ ] /∋ ρ ↑                        ]  ≡⟨ /∋-↑ zero[ σ ] ρ ⟩
      [ zero[ σ ] /∋ (wk-subst ρ ▻⇨ var · zero) ]  ≡⟨ P.refl ⟩
      [ var · zero                              ]  ∎

    suc-/∋-↑ : ∀ {Γ Δ τ} σ {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ τ) (ρ : Sub T ρ̂) →
               suc[ σ ] x /∋ ρ ↑ ≅-⊢ x /∋ wk-subst[ σ / ρ ] ρ
    suc-/∋-↑ σ x ρ = begin
      [ suc[ σ ] x /∋ ρ ↑                        ]  ≡⟨ /∋-↑ (suc[ σ ] x) ρ ⟩
      [ suc[ σ ] x /∋ (wk-subst ρ ▻⇨ var · zero) ]  ≡⟨ P.refl ⟩
      [ x /∋ wk-subst ρ                          ]  ∎

  -- One can weaken either before or after looking up a variable.
  -- (Note that this lemma holds definitionally, unlike the
  -- corresponding lemma in deBruijn.Substitution.Data.Simple.)

  /∋-wk-subst : ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ τ) (ρ : Sub T ρ̂) →
                x /∋ wk-subst[ σ ] ρ ≅-⊢ weaken[ σ ] · (x /∋ ρ)
  /∋-wk-subst x ρ = P.refl

  abstract

    -- A corollary.

    /∋-wk-subst-var :
      ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ}
      (ρ : Sub T ρ̂) (x : Γ ∋ τ) (y : Δ ∋ τ / ρ) →
      x /∋               ρ ≅-⊢ var ·          y →
      x /∋ wk-subst[ σ ] ρ ≅-⊢ var · suc[ σ ] y
    /∋-wk-subst-var ρ x y hyp = begin
      [ x /∋ wk-subst ρ    ]  ≡⟨ P.refl ⟩
      [ weaken · (x /∋ ρ)  ]  ≡⟨ weaken-cong P.refl hyp ⟩
      [ weaken · (var · y) ]  ≡⟨ weaken-var y ⟩
      [ var · suc y        ]  ∎

    -- The identity substitution has no effect.

    /-id : ∀ {Γ} (σ : Type Γ) → σ / id ≅-Type σ
    /-id σ = P.refl

    /⁺-id : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Γ⁺ /⁺ id ≅-Ctxt⁺ Γ⁺
    /⁺-id Γ⁺ = begin
      [ Γ⁺ /⁺ id ]  ≡⟨ P.refl ⟩
      [ Γ⁺ /̂⁺ îd ]  ≡⟨ /̂⁺-îd Γ⁺ ⟩
      [ Γ⁺       ]  ∎

    /₊-id : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → Γ₊ /₊ id ≅-Ctxt₊ Γ₊
    /₊-id Γ₊ = begin
      [ Γ₊ /₊ id ]  ≡⟨ P.refl ⟩
      [ Γ₊ /̂₊ îd ]  ≡⟨ /̂₊-îd Γ₊ ⟩
      [ Γ₊       ]  ∎

    mutual

      /∋-id : ∀ {Γ σ} (x : Γ ∋ σ) → x /∋ id ≅-⊢ var · x
      /∋-id {Γ = ε}     ()
      /∋-id {Γ = Γ ▻ σ} x = begin
        [ x /∋ id ↑               ]  ≡⟨ /∋-↑ x id ⟩
        [ x /∋ (wk ▻⇨ var · zero) ]  ≡⟨ lemma x ⟩
        [ var · x                 ]  ∎
        where
        lemma : ∀ {τ} (x : Γ ▻ σ ∋ τ) →
                x /∋ (wk[ σ ] ▻⇨ var · zero) ≅-⊢ var · x
        lemma zero    = P.refl
        lemma (suc x) = /∋-wk x

      -- Weakening a variable is equivalent to incrementing it.

      /∋-wk : ∀ {Γ σ τ} (x : Γ ∋ τ) →
              x /∋ wk[ σ ] ≅-⊢ var · suc[ σ ] x
      /∋-wk x = /∋-wk-subst-var id x x (/∋-id x)

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

    id-↑⁺ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → id ↑⁺ Γ⁺ ≅-⇨ id[ Γ ++⁺ Γ⁺ ]
    id-↑⁺ ε        = id ∎-⟶
    id-↑⁺ (Γ⁺ ▻ σ) =
      (id ↑⁺ Γ⁺) ↑  ≅-⟶⟨ ↑-cong (id-↑⁺ Γ⁺) P.refl ⟩
      id ↑          ∎-⟶

    id-↑₊ : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → id ↑₊ Γ₊ ≅-⇨ id[ Γ ++₊ Γ₊ ]
    id-↑₊ ε        = id ∎-⟶
    id-↑₊ (σ ◅ Γ₊) =
      id ↑ ↑₊ Γ₊  ≅-⟶⟨ [ P.refl ] ⟩
      id   ↑₊ Γ₊  ≅-⟶⟨ id-↑₊ Γ₊ ⟩
      id          ∎-⟶

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

    /∋-id-↑⁺ : ∀ {Γ} Γ⁺ {σ} (x : Γ ++⁺ Γ⁺ ∋ σ) →
               x /∋ id ↑⁺ Γ⁺ ≅-⊢ var · x
    /∋-id-↑⁺ Γ⁺ x = begin
      [ x /∋ id ↑⁺ Γ⁺ ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) (id-↑⁺ Γ⁺) ⟩
      [ x /∋ id       ]  ≡⟨ /∋-id x ⟩
      [ var · x       ]  ∎

    /∋-id-↑₊ : ∀ {Γ} Γ₊ {σ} (x : Γ ++₊ Γ₊ ∋ σ) →
               x /∋ id ↑₊ Γ₊ ≅-⊢ var · x
    /∋-id-↑₊ Γ₊ x = begin
      [ x /∋ id ↑₊ Γ₊ ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) (id-↑₊ Γ₊) ⟩
      [ x /∋ id       ]  ≡⟨ /∋-id x ⟩
      [ var · x       ]  ∎

    -- If ρ is morally a renaming, then "deep application" of ρ to a
    -- variable is still a variable.

    /∋-↑⁺ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
            (ρ : Sub T ρ̂) (f : [ Var ⟶ Var ] ρ̂) →
            (∀ {σ} (x : Γ ∋ σ) → x /∋ ρ ≅-⊢ var · (f · x)) →
            ∀ Γ⁺ {σ} (x : Γ ++⁺ Γ⁺ ∋ σ) →
            x /∋ ρ ↑⁺ Γ⁺ ≅-⊢ var · (lift f Γ⁺ · x)
    /∋-↑⁺ ρ f hyp ε        x    = hyp x
    /∋-↑⁺ ρ f hyp (Γ⁺ ▻ σ) zero = begin
      [ zero[ σ ] /∋ (ρ ↑⁺ Γ⁺) ↑ ]  ≡⟨ zero-/∋-↑ σ (ρ ↑⁺ Γ⁺) ⟩
      [ var · zero               ]  ∎
    /∋-↑⁺ ρ f hyp (Γ⁺ ▻ σ) (suc x) = begin
      [ suc[ σ ] x /∋ (ρ ↑⁺ Γ⁺) ↑        ]  ≡⟨ suc-/∋-↑ σ x (ρ ↑⁺ Γ⁺) ⟩
      [ x /∋ wk-subst (ρ ↑⁺ Γ⁺)          ]  ≡⟨ P.refl ⟩
      [ weaken · (x /∋ ρ ↑⁺ Γ⁺)          ]  ≡⟨ weaken-cong P.refl (/∋-↑⁺ ρ f hyp Γ⁺ x) ⟩
      [ weaken · (var · (lift f Γ⁺ · x)) ]  ≡⟨ weaken-var (lift f Γ⁺ · x) ⟩
      [ var · suc (lift f Γ⁺ · x)        ]  ∎

    -- "Deep weakening" of a variable can be expressed without
    -- reference to the weaken function.

    /∋-wk-↑⁺ : ∀ {Γ σ} Γ⁺ {τ} (x : Γ ++⁺ Γ⁺ ∋ τ) →
               x /∋ wk[ σ ] ↑⁺ Γ⁺ ≅-⊢
               var · (lift weaken∋[ σ ] Γ⁺ · x)
    /∋-wk-↑⁺ = /∋-↑⁺ wk weaken∋ /∋-wk

    /∋-wk-↑⁺-↑⁺ : ∀ {Γ σ} Γ⁺ Γ⁺⁺ {τ} (x : Γ ++⁺ Γ⁺ ++⁺ Γ⁺⁺ ∋ τ) →
                  x /∋ wk[ σ ] ↑⁺ Γ⁺ ↑⁺ Γ⁺⁺ ≅-⊢
                  var · (lift (lift weaken∋[ σ ] Γ⁺) Γ⁺⁺ · x)
    /∋-wk-↑⁺-↑⁺ Γ⁺ = /∋-↑⁺ (wk ↑⁺ Γ⁺) (lift weaken∋ Γ⁺) (/∋-wk-↑⁺ Γ⁺)

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

    ↑⁺-⁺++⁺ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) Γ⁺ Γ⁺⁺ →
              ρ ↑⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺) ≅-⇨ ρ ↑⁺ Γ⁺ ↑⁺ Γ⁺⁺
    ↑⁺-⁺++⁺ ρ Γ⁺ ε         = ρ ↑⁺ Γ⁺ ∎-⟶
    ↑⁺-⁺++⁺ ρ Γ⁺ (Γ⁺⁺ ▻ σ) =
      (ρ ↑⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺)) ↑  ≅-⟶⟨ ↑-cong (↑⁺-⁺++⁺ ρ Γ⁺ Γ⁺⁺)
                                          (drop-subst-Type F.id (++⁺-++⁺ Γ⁺ Γ⁺⁺)) ⟩
      (ρ ↑⁺ Γ⁺ ↑⁺ Γ⁺⁺) ↑      ∎-⟶

    ↑₊-₊++₊ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) Γ₊ Γ₊₊ →
              ρ ↑₊ (Γ₊ ₊++₊ Γ₊₊) ≅-⇨ ρ ↑₊ Γ₊ ↑₊ Γ₊₊
    ↑₊-₊++₊ ρ ε        Γ₊₊ = ρ ↑₊ Γ₊₊ ∎-⟶
    ↑₊-₊++₊ ρ (σ ◅ Γ₊) Γ₊₊ =
      ρ ↑ ↑₊ (Γ₊ ₊++₊ Γ₊₊)  ≅-⟶⟨ ↑₊-₊++₊ (ρ ↑) Γ₊ Γ₊₊ ⟩
      ρ ↑ ↑₊ Γ₊ ↑₊ Γ₊₊      ∎-⟶

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


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

syntax Empty | E

type
  𝟘 : 0-ary

term
  abort : 𝟘  ->  α

theory
  (𝟘η) e : 𝟘  c : α |> abort(e) = c
-}

module Empty.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import Empty.Signature
open import Empty.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution E:Syn
open import SOAS.Metatheory.SecondOrder.Equality E:Syn

private
  variable
    α β γ τ : ET
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ E) α Γ → (𝔐 ▷ E) α Γ → Set where
  𝟘η : ⁅ 𝟘 ⁆ ⁅ α ⁆̣ ▹ ∅ ⊢ abort 𝔞 ≋ₐ 𝔟

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-# OPTIONS --guardedness-preserving-type-constructors #-}
module Issue602 where

infixl 6 _⊔_

postulate
  Level : Set
  zero  : Level
  suc   : Level → Level
  _⊔_   : Level → Level → Level

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

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

data CoNat : Set0 where
  z : CoNat
  s : ∞ CoNat → CoNat

record A : Set2 where
  field
    f : Set1

record B (a : ∞ A) : Set1 where
  field
    f : A.f (♭ a)

postulate
  a : A

e : CoNat → A
e z = a
e (s n) = record
  { f = B (♯ e (♭ n))
  }

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

open import Categories.Category
open import Categories.Functor.Bifunctor

module Categories.Diagram.End {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  (F : Bifunctor (Category.op C) C D) where

private
  module D = Category D
  open D
  open HomReasoning
  open Equiv
  variable
    A B : Obj
    f g : A ⇒ B

open import Level

open import Categories.Diagram.Wedge F
open import Categories.NaturalTransformation.Dinatural

record End : Set (levelOfTerm F) where
  field
    wedge : Wedge

  module wedge = Wedge wedge
  open wedge public
  open Wedge

  field
    factor    : (W : Wedge) → E W ⇒ wedge.E
    universal : ∀ {W : Wedge} {A} → wedge.dinatural.α A ∘ factor W ≈ dinatural.α W A
    unique    : ∀ {W : Wedge} {g : E W ⇒ wedge.E} → (∀ {A} → wedge.dinatural.α A ∘ g ≈ dinatural.α W A) → factor W ≈ g

  η-id : factor wedge ≈ D.id
  η-id = unique identityʳ

  unique′ :(∀ {A} → wedge.dinatural.α A ∘ f ≈ wedge.dinatural.α A ∘ g) → f ≈ g
  unique′ {f = f} {g = g} eq = ⟺ (unique {W = Wedge-∘ wedge f} refl) ○ unique (⟺ eq)

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 #-}

-- A "canonical" presentation of limits in Setoid.
--
-- These limits are obviously isomorphic to those created by
-- the Completeness proof, but are far less unweildy to work with.
-- This isomorphism is witnessed by Categories.Diagram.Pullback.up-to-iso

module Categories.Category.Instance.Properties.Setoids.Limits.Canonical where

open import Level
open import Data.Product using (_,_; _×_; map; zip; proj₁; proj₂; <_,_>)
open import Function.Equality as SΠ renaming (id to ⟶-id)
open import Relation.Binary.Bundles using (Setoid)
import Relation.Binary.Reasoning.Setoid as SR

open import Categories.Category.Instance.Setoids
open import Categories.Diagram.Pullback

open Setoid renaming (_≈_ to [_][_≈_])

--------------------------------------------------------------------------------
-- Pullbacks

record FiberProduct {o ℓ} {X Y Z : Setoid o ℓ} (f : X ⟶ Z) (g : Y ⟶ Z) : Set (o ⊔ ℓ) where
  constructor mk-×
  field
    elem₁ : Carrier X
    elem₂ : Carrier Y
    commute : [ Z ][ f ⟨$⟩ elem₁ ≈ g ⟨$⟩ elem₂ ]

open FiberProduct

FP-≈ : ∀ {o ℓ} {X Y Z : Setoid o ℓ} {f : X ⟶ Z} {g : Y ⟶ Z} → (fb₁ fb₂ : FiberProduct f g) → Set ℓ
FP-≈ {X = X} {Y} p q = [ X ][ elem₁ p ≈ elem₁ q ] × [ Y ][ elem₂ p ≈ elem₂ q ]

pullback : ∀ (o ℓ : Level) {X Y Z : Setoid (o ⊔ ℓ) ℓ} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Pullback (Setoids (o ⊔ ℓ) ℓ) f g
pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record
  { P = record
    { Carrier = FiberProduct f g
    ; _≈_ =  FP-≈
    ; isEquivalence = record
      { refl = X.refl , Y.refl
      ; sym = map X.sym Y.sym
      ; trans = zip X.trans Y.trans
      }
    }
    ; p₁ = record { _⟨$⟩_ = elem₁ ; cong = proj₁ }
    ; p₂ = record { _⟨$⟩_ = elem₂ ; cong = proj₂ }
    ; isPullback = record
      { commute = λ {p} {q} (eq₁ , eq₂) → trans Z (cong f eq₁) (commute q)
      ; universal = λ {A} {h₁} {h₂} eq → record
        { _⟨$⟩_ = λ a → record
          { elem₁ = h₁ ⟨$⟩ a
          ; elem₂ = h₂ ⟨$⟩ a
          ; commute = eq (refl A)
          }
        ; cong = < cong h₁ , cong h₂ >
        }
      ; unique = λ eq₁ eq₂ x≈y → eq₁ x≈y , eq₂ x≈y
      ; p₁∘universal≈h₁ = λ {_} {h₁} {_} eq → cong h₁ eq
      ; p₂∘universal≈h₂ = λ {_} {_} {h₂} eq → cong h₂ eq
      }
    }
    where
      module X = Setoid X
      module Y = Setoid Y


text:
module Scratch (FunctionName : Set) where

open import Oscar.Data.Fin using (Fin; zero; suc; thick?)

open import Data.Nat using (ℕ; suc; zero)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂; cong; sym; trans)
open import Function using (_∘_; flip)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (∃; _,_; _×_)
open import Data.Empty using (⊥-elim)
open import Data.Vec using (Vec; []; _∷_)

data Term (n : ℕ) : Set where
  i : (x : Fin n) -> Term n
  leaf : Term n
  _fork_ : (s t : Term n) -> Term n
  function : FunctionName → ∀ {f} → Vec (Term n) f → Term n

Term-function-inj-FunctionName : ∀ {fn₁ fn₂} {n N₁ N₂} {ts₁ : Vec (Term n) N₁} {ts₂ : Vec (Term n) N₂} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → fn₁ ≡ fn₂
Term-function-inj-FunctionName refl = refl

Term-function-inj-VecSize : ∀ {fn₁ fn₂} {n N₁ N₂} {ts₁ : Vec (Term n) N₁} {ts₂ : Vec (Term n) N₂} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → N₁ ≡ N₂
Term-function-inj-VecSize refl = refl

Term-function-inj-Vector : ∀ {fn₁ fn₂} {n N} {ts₁ : Vec (Term n) N} {ts₂ : Vec (Term n) N} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → ts₁ ≡ ts₂
Term-function-inj-Vector refl = refl

Term-fork-inj-left : ∀ {n} {l₁ r₁ l₂ r₂ : Term n} → l₁ fork r₁ ≡ l₂ fork r₂ → l₁ ≡ l₂
Term-fork-inj-left refl = refl

Term-fork-inj-right : ∀ {n} {l₁ r₁ l₂ r₂ : Term n} → l₁ fork r₁ ≡ l₂ fork r₂ → r₁ ≡ r₂
Term-fork-inj-right refl = refl

open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)

Term-function-inj-HetVector : ∀ {fn₁ fn₂} {n N₁ N₂} {ts₁ : Vec (Term n) N₁} {ts₂ : Vec (Term n) N₂} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → ts₁ ≅ ts₂
Term-function-inj-HetVector refl = refl

_~>_ : (m n : ℕ) -> Set
m ~> n = Fin m -> Term n

▹ : ∀ {m n} -> (r : Fin m -> Fin n) -> Fin m -> Term n
▹ r = i ∘ r

record Substitution (T : ℕ → Set) : Set where
  field
    _◃_ : ∀ {m n} -> (f : m ~> n) -> T m -> T n

open Substitution ⦃ … ⦄ public

{-# DISPLAY Substitution._◃_ _ = _◃_ #-}

mutual

  instance SubstitutionTerm : Substitution Term
  Substitution._◃_ SubstitutionTerm = _◃′_ where
    _◃′_ : ∀ {m n} -> (f : m ~> n) -> Term m -> Term n
    f ◃′ i x = f x
    f ◃′ leaf = leaf
    f ◃′ (s fork t) = (f ◃ s) fork (f ◃ t)
    f ◃′ (function fn ts) = function fn (f ◃ ts)

  instance SubstitutionVecTerm : ∀ {N} → Substitution (flip Vec N ∘ Term )
  Substitution._◃_ (SubstitutionVecTerm {N}) = _◃′_ where
    _◃′_ : ∀ {m n} -> (f : m ~> n) -> Vec (Term m) N -> Vec (Term n) N
    f ◃′ [] = []
    f ◃′ (t ∷ ts) = f ◃ t ∷ f ◃ ts

_≐_ : {m n : ℕ} -> (Fin m -> Term n) -> (Fin m -> Term n) -> Set
f ≐ g = ∀ x -> f x ≡ g x

record SubstitutionExtensionality (T : ℕ → Set) ⦃ _ : Substitution T ⦄ : Set₁ where
  field
    ◃ext : ∀ {m n} {f g : Fin m -> Term n} -> f ≐ g -> (t : T m) -> f ◃ t ≡ g ◃ t

open SubstitutionExtensionality ⦃ … ⦄ public

mutual

  instance SubstitutionExtensionalityTerm : SubstitutionExtensionality Term
  SubstitutionExtensionality.◃ext SubstitutionExtensionalityTerm = ◃ext′ where
    ◃ext′ : ∀ {m n} {f g : Fin m -> Term n} -> f ≐ g -> ∀ t -> f ◃ t ≡ g ◃ t
    ◃ext′ p (i x) = p x
    ◃ext′ p leaf = refl
    ◃ext′ p (s fork t) = cong₂ _fork_ (◃ext p s) (◃ext p t)
    ◃ext′ p (function fn ts) = cong (function fn) (◃ext p ts)

  instance SubstitutionExtensionalityVecTerm : ∀ {N} → SubstitutionExtensionality (flip Vec N ∘ Term)
  SubstitutionExtensionality.◃ext (SubstitutionExtensionalityVecTerm {N}) = λ x → ◃ext′ x where
    ◃ext′ : ∀ {m n} {f g : Fin m -> Term n} -> f ≐ g -> ∀ {N} (t : Vec (Term m) N) -> f ◃ t ≡ g ◃ t
    ◃ext′ p [] = refl
    ◃ext′ p (t ∷ ts) = cong₂ _∷_ (◃ext p t) (◃ext p ts)

_◇_ : ∀ {l m n : ℕ } -> (f : Fin m -> Term n) (g : Fin l -> Term m) -> Fin l -> Term n
f ◇ g = (f ◃_) ∘ g

≐-cong : ∀ {m n o} {f : m ~> n} {g} (h : _ ~> o) -> f ≐ g -> (h ◇ f) ≐ (h ◇ g)
≐-cong h f≐g t = cong (h ◃_) (f≐g t)

≐-sym : ∀ {m n} {f : m ~> n} {g} -> f ≐ g -> g ≐ f
≐-sym f≐g = sym ∘ f≐g

module Sub where
  record Fact1 (T : ℕ → Set) ⦃ _ : Substitution T ⦄ : Set where
    field
      fact1 : ∀ {n} -> (t : T n) -> i ◃ t ≡ t

  open Fact1 ⦃ … ⦄ public

  mutual

    instance Fact1Term : Fact1 Term
    Fact1.fact1 Fact1Term (i x) = refl
    Fact1.fact1 Fact1Term leaf = refl
    Fact1.fact1 Fact1Term (s fork t) = cong₂ _fork_ (fact1 s) (fact1 t)
    Fact1.fact1 Fact1Term (function fn ts) = cong (function fn) (fact1 ts)

    instance Fact1TermVec : ∀ {N} → Fact1 (flip Vec N ∘ Term)
    Fact1.fact1 Fact1TermVec [] = refl
    Fact1.fact1 Fact1TermVec (t ∷ ts) = cong₂ _∷_ (fact1 t) (fact1 ts)

  record Fact2 (T : ℕ → Set) ⦃ _ : Substitution T ⦄ : Set where
    field
      -- ⦃ s ⦄ : Substitution T
      fact2 : ∀ {l m n} -> {f : Fin m -> Term n} {g : _} (t : T l) → (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)

  open Fact2 ⦃ … ⦄ public

  mutual

    instance Fact2Term : Fact2 Term
    -- Fact2.s Fact2Term = SubstitutionTerm
    Fact2.fact2 Fact2Term (i x) = refl
    Fact2.fact2 Fact2Term leaf = refl
    Fact2.fact2 Fact2Term (s fork t) = cong₂ _fork_ (fact2 s) (fact2 t)
    Fact2.fact2 Fact2Term {f = f} {g = g} (function fn ts) = cong (function fn) (fact2 {f = f} {g = g} ts) -- fact2 ts

    instance Fact2TermVec : ∀ {N} → Fact2 (flip Vec N ∘ Term)
    -- Fact2.s Fact2TermVec = SubstitutionVecTerm
    Fact2.fact2 Fact2TermVec [] = refl
    Fact2.fact2 Fact2TermVec (t ∷ ts) = cong₂ _∷_ (fact2 t) (fact2 ts)

  fact3 : ∀ {l m n} (f : Fin m -> Term n) (r : Fin l -> Fin m) -> (f ◇ (▹ r)) ≡ (f ∘ r)
  fact3 f r = refl

◃ext' : ∀ {m n o} {f : Fin m -> Term n}{g : Fin m -> Term o}{h} -> f ≐ (h ◇ g) -> ∀ (t : Term _) -> f ◃ t ≡ h ◃ (g ◃ t)
◃ext' p t = trans (◃ext p t) (Sub.fact2 t)

open import Data.Maybe using (Maybe; nothing; just; functor; maybe′)
open import Category.Monad
import Level
open RawMonad (Data.Maybe.monad {Level.zero})

record Check (T : ℕ → Set) : Set where
  field
    check : ∀{n} (x : Fin (suc n)) (t : T (suc n)) -> Maybe (T n)

open Check ⦃ … ⦄ public

_<*>_ = _⊛_

mutual

  instance CheckTerm : Check Term
  Check.check CheckTerm x (i y) = i <$> thick? x y
  Check.check CheckTerm x leaf = just leaf
  Check.check CheckTerm x (s fork t) = _fork_ <$> check x s ⊛ check x t
  Check.check CheckTerm x (function fn ts) = ⦇ (function fn) (check x ts) ⦈

  instance CheckTermVec : ∀ {N} → Check (flip Vec N ∘ Term)
  Check.check CheckTermVec x [] = just []
  Check.check CheckTermVec x (t ∷ ts) = ⦇ check x t ∷ check x ts ⦈

_for_ : ∀ {n} (t' : Term n) (x : Fin (suc n)) -> Fin (suc n) -> Term n
(t' for x) y = maybe′ i t' (thick? x y)

data AList : ℕ -> ℕ -> Set where
  anil : ∀ {n} -> AList n n
  _asnoc_/_ : ∀ {m n} (σ : AList m n) (t' : Term m) (x : Fin (suc m))
               -> AList (suc m) n

sub : ∀ {m n} (σ : AList m n) -> Fin m -> Term n
sub anil = i
sub (σ asnoc t' / x) = sub σ ◇ (t' for x)

_++_ : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> AList l n
ρ ++ anil = ρ
ρ ++ (σ asnoc t' / x) = (ρ ++ σ) asnoc t' / x

++-assoc : ∀ {l m n o} (ρ : AList l m) (σ : AList n _) (τ : AList o _) -> ρ ++ (σ ++ τ) ≡ (ρ ++ σ) ++ τ
++-assoc ρ σ anil = refl
++-assoc ρ σ (τ asnoc t / x) = cong (λ s -> s asnoc t / x) (++-assoc ρ σ τ)

module SubList where
  anil-id-l : ∀ {m n} (σ : AList m n) -> anil ++ σ ≡ σ
  anil-id-l anil = refl
  anil-id-l (σ asnoc t' / x) = cong (λ σ -> σ asnoc t' / x) (anil-id-l σ)

  fact1 : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> sub (ρ ++ σ) ≐ (sub ρ ◇ sub σ)
  fact1 ρ anil v = refl
  fact1 {suc l} {m} {n} r (s asnoc t' / x) v = trans hyp-on-terms ◃-assoc
    where
      t = (t' for x) v
      hyp-on-terms = ◃ext (fact1 r s) t
      ◃-assoc = Sub.fact2 t

_∃asnoc_/_ : ∀ {m} (a : ∃ (AList m)) (t' : Term m) (x : Fin (suc m))
  -> ∃ (AList (suc m))
(n , σ) ∃asnoc t' / x = n , σ asnoc t' / x

flexFlex : ∀ {m} (x y : Fin m) -> ∃ (AList m)
flexFlex {suc m} x y with thick? x y
...              | just y' = m , anil asnoc i y' / x
...              | nothing = suc m , anil
flexFlex {zero} () _

flexRigid : ∀ {m} (x : Fin m) (t : Term m) -> Maybe (∃(AList m))
flexRigid {suc m} x t with check x t
...                   | just t' = just (m , anil asnoc t' / x)
...                   | nothing = nothing
flexRigid {zero} () _

-- module Scratch where

-- open import Prelude

-- open import Agda.Builtin.Size

-- open import Tactic.Nat

-- postulate
--   Domain : Set

-- record Interpretation : Set where
--   field
--     V : Nat → Domain
--     F : (arity name : Nat) → Vec Domain arity → Domain
--     P : (arity name : Nat) → Vec Domain arity → Bool

-- data Term {i : Size} : Set where
--   variable : Nat → Term
--   function : (arity name : Nat) → {j : Size< i} → Vec (Term {j}) arity → Term {i}

-- interpretTerm : Interpretation → {i : Size} → Term {i} → Domain
-- interpretTerm I (variable v) = Interpretation.V I v
-- interpretTerm I (function arity name {j} domA) = Interpretation.F I arity name (interpretTerm I <$> domA)

-- data Formula : Set where
--   atomic : (arity name : Nat) → Vec Term arity → Formula
--   logical : Formula →
--             Formula →
--             Formula
--   quantified : Nat → Formula → Formula

-- infix 40 _⊗_
-- _⊗_ : Formula → Formula → Formula
-- _⊗_ a b = logical a b

-- ~ : Formula → Formula
-- ~ a = logical a a

-- infix 50 _⊃_
-- _⊃_ : Formula → Formula → Formula
-- _⊃_ p q = ~ (~ p ⊗ q)

-- data Literal : Formula → Set where
--   Latomic : (arity name : Nat) → (terms : Vec Term arity) → Literal (atomic arity name terms)
--   logical : (arity name : Nat) → (terms : Vec Term arity) → Literal (logical (atomic arity name terms) (atomic arity name terms))

-- record Sequent : Set where
--   constructor _⊢_
--   field
--     premises : List Formula
--     conclusion : Formula

-- data _∈_ {A : Set} (a : A) : List A → Set where
--   here : (as : List A) → a ∈ (a ∷ as)
--   there : (x : A) (as : List A) → a ∈ (x ∷ as)

-- record SimpleNDProblem (s : Sequent) : Set where
--   field
--     simpleConclusion : Literal (Sequent.conclusion s)
--     simplePremises : ∀ p → p ∈ Sequent.premises s → Literal p

-- record _≞_/_ (I : Interpretation) (I₀ : Interpretation) (v₀ : Nat) : Set where
--   field
--     lawV : (v : Nat) → (v ≡ v₀ → ⊥) → Interpretation.V I v ≡ Interpretation.V I₀ v
--     lawF : (arity name : Nat) → (domA : Vec Domain arity) → Interpretation.F I arity name domA ≡ Interpretation.F I₀ arity name domA
--     lawP : (arity name : Nat) → (domA : Vec Domain arity) → Interpretation.P I arity name domA ≡ Interpretation.P I₀ arity name domA

-- record Satisfaction (A : Set) : Set₁ where
--   field
--     _⊨_ : Interpretation → A → Set

--   postulate _⊨?_ : (I : Interpretation) → (φ : A) → Dec (I ⊨ φ)

--   _⊭_ : Interpretation → A → Set
--   I ⊭ x = I ⊨ x → ⊥

-- open Satisfaction ⦃ … ⦄

-- instance
--   SatisfactionFormula : Satisfaction Formula
--   Satisfaction._⊨_ SatisfactionFormula = _⊨ᴹ_ where
--     _⊨ᴹ_ : Interpretation → Formula → Set
--     _⊨ᴹ_ I₀ (quantified v₀ φ) = (I : Interpretation) → I ≞ I₀ / v₀ → I ⊨ᴹ φ
--     _⊨ᴹ_ I₀ (atomic arity name domA) = Interpretation.P I₀ arity name (interpretTerm I₀ <$> domA) ≡ true
--     _⊨ᴹ_ I₀ (logical φ₁ φ₂) = (I₀ ⊨ᴹ φ₁ → ⊥) × (I₀ ⊨ᴹ φ₂ → ⊥)
--     {-# DISPLAY _⊨ᴹ_ I f = I ⊨ f #-}

-- record Validity (A : Set) : Set₁ where
--   field
--     ⊨_ : A → Set

--   ⊭_ : A → Set
--   ⊭ x = ⊨ x → ⊥

-- open Validity ⦃ … ⦄

-- instance
--   ValidityFormula : Validity Formula
--   Validity.⊨_ ValidityFormula φ = (I : Interpretation) → I ⊨ φ

-- instance
--   SatisfactionSequent : Satisfaction Sequent
--   Satisfaction._⊨_ SatisfactionSequent I (premises ⊢ conclusion) = (_ : (premise : Formula) → premise ∈ premises → I ⊨ premise) →  I ⊨ conclusion

--   ValiditySequent : Validity Sequent
--   Validity.⊨_ ValiditySequent sequent = (I : Interpretation) → I ⊨ sequent

-- negationElimination : (I : Interpretation) (φ : Formula) → I ⊨ (φ ⊗ φ) ⊗ (φ ⊗ φ) → I ⊨ φ
-- negationElimination I φ (x , y) with I ⊨? φ
-- negationElimination I φ (x₁ , y) | yes x = x
-- negationElimination I φ (x₁ , y) | no x = ⊥-elim (x₁ (x , x))

-- -- logical (logical (logical p p) q) (logical (logical p p) q)
-- conditionalization : (I : Interpretation) (p q : Formula) → I ⊨ q → I ⊨ ((p ∷ []) ⊢ p ⊃ q)
-- conditionalization I p q ⊨q -⊨p = let ⊨p = -⊨p p (here []) in (λ { (x , ~q) → ~q ⊨q}) , (λ { (x , y) → y ⊨q})

-- modusPonens : (I : Interpretation) (p q : Formula) → I ⊨ p → I ⊨ ((p ⊗ p) ⊗ q) ⊗ ((p ⊗ p) ⊗ q) → I ⊨ q
-- modusPonens I p q P (~[~p&~p&~q] , ~[~p&~p&~q]²) with I ⊨? q
-- modusPonens I p q P (~[~p&~p&~q] , ~[~p&~p&~q]²) | yes x = x
-- modusPonens I p q P (~[~p&~p&~q] , ~[~p&~p&~q]²) | no x = ⊥-elim (~[~p&~p&~q] ((λ { (x₁ , y) → y P}) , (λ x₁ → x x₁)))

-- theorem1a : (s : Sequent) → SimpleNDProblem s → ⊨ s → Either (Sequent.conclusion s ∈ Sequent.premises s) (Σ _ λ q → q ∈ Sequent.premises s × ~ q ∈ Sequent.premises s)
-- theorem1a ([] ⊢ atomic arity name x) record { simpleConclusion = (Latomic .arity .name .x) ; simplePremises = simplePremises } x₂ = {!!}
-- theorem1a ((x₁ ∷ premises) ⊢ atomic arity name x) record { simpleConclusion = (Latomic .arity .name .x) ; simplePremises = simplePremises } x₂ = {!!}
-- theorem1a (premises ⊢ logical .(atomic arity name terms) .(atomic arity name terms)) record { simpleConclusion = (logical arity name terms) ; simplePremises = simplePremises } x₁ = {!!}
-- theorem1a (premises ⊢ quantified x conclusion) record { simpleConclusion = () ; simplePremises = simplePremises } x₂

-- theorem1b : (s : Sequent) → SimpleNDProblem s → Either (Sequent.conclusion s ∈ Sequent.premises s) (Σ _ λ q → q ∈ Sequent.premises s × ~ q ∈ Sequent.premises s) → ⊨ s
-- theorem1b s x (left x₁) I x₂ = x₂ (Sequent.conclusion s) x₁
-- theorem1b s x (right (x₁ , x₂ , y)) I x₃ = let ~q = x₃ (~ x₁) y in let q = x₃ x₁ x₂ in ⊥-elim (fst ~q q)

-- {-
-- p ≡ q
-- p -> q & q -> p
-- (~p v q) & (~q v p)
-- ~(p & ~q) & ~(q & ~p)
-- ~(~~p & ~q) & ~(~~q & ~p)

-- bicondit elim is just simplification

-- modus ponens
-- p , (p ⊗ (q ⊗ q)) ⊗ (p ⊗ (q ⊗ q)) --> q

-- ~(~p & q)
-- p or ~q

-- p -> q
-- ~p v q
-- ~(p & ~q)
-- ~(p & ~q) & ~(p & ~q)
-- ~(~~p & ~q) & ~(~~p & ~q)
-- (~~p & ~q) ⊗ (~~p & ~q)
-- (~p ⊗ q) ⊗ (~p ⊗ q)
-- ((p ⊗ p) ⊗ q) ⊗ ((p ⊗ p) ⊗ q)
-- -}

-- {-
-- conditionalization p -> q from q, with discharge p
-- (p ∷ [] ⊢ q) ⊨ (∅ ⊢ q)
-- -}

-- --data ReasonerState : List Sequent → List Sequent → Set

-- {-
-- p <-> q
-- p -> q and q -> p
-- ~p v q  and  ~q or p
-- ~(p and ~q) and ~(q and ~p)
-- (p and ~q) ⊗ (q and ~p)
-- ((p ⊗ p) ⊗ q) ⊗ ((q ⊗ q) ⊗ p)

-- p -> q
-- ~p v q
-- ~(p and ~q)
-- ~(p and ~q) and ~(p and ~q)
-- ((p ⊗ p) ⊗ q) ⊗ ((p ⊗ p) ⊗ q)
-- but this is just simplification

-- p , p -> q ⊢ q
-- p , ((p ⊗ p) ⊗ q) ⊗ ((p ⊗ p) ⊗ q) ⊢ q

-- p , q <-- p & q

-- p <-- ~~p
-- p <-- (p ⊗ p) ⊗ (p ⊗ p)
-- -}

-- -- PorNotP : (I : Interpretation) (P : Formula) → I ⊨ (logical (logical P (logical P P)) (logical P (logical P P)))
-- -- PorNotP I P = (λ { (x , y) → y (x , x)}) , (λ { (x , y) → y (x , x)})

-- -- IFTHEN : Formula → Formula → Formula
-- -- IFTHEN P Q = logical (logical (logical P P) Q) (logical (logical P P) Q)

-- -- EXISTS : Nat → Formula → Formula
-- -- EXISTS n φ = (logical (quantified n (logical φ φ)) (quantified n (logical φ φ)))

-- -- F : Nat → Formula
-- -- F n = atomic 1 0 (variable n ∷ [])

-- -- Fa : Formula
-- -- Fa = F 0

-- -- ∃xFx : Formula
-- -- ∃xFx = EXISTS 1 (F 1)

-- -- IfFaThenExistsFa : (I : Interpretation) → I ⊨ (IFTHEN Fa ∃xFx)
-- -- IfFaThenExistsFa I = (λ { (I⊭~Fa , I⊭∃xFx) → I⊭~Fa ((λ x → I⊭∃xFx ((λ x₁ → fst (x₁ {!!} {!!}) {!!}) , (λ x₁ → {!!}))) , {!!})}) , (λ { (x , y) → {!!}})

-- -- NotPAndNotNotP : (I : Interpretation) (P : Formula) → I ⊨ (logical P (logical P P))
-- -- NotPAndNotNotP = {!!}

-- -- -- Valid : Formula → Set₁
-- -- -- Valid φ = (I : Interpretation) → I Satisfies φ

-- -- -- -- data SkolemFormula {ι : Size} (α : Alphabet) : Set where
-- -- -- --   atomic : Predication α → SkolemFormula α
-- -- -- --   logical : {ι¹ : Size< ι} → SkolemFormula {ι¹} α → {ι² : Size< ι} → SkolemFormula {ι²} α → SkolemFormula {ι} α

-- -- -- -- record Alphabet₊ᵥ (α : Alphabet) : Set where
-- -- -- --   constructor α₊ᵥ⟨_⟩
-- -- -- --   field
-- -- -- --     alphabet : Alphabet
-- -- -- --     .one-variable-is-added : (number ∘ variables $ alphabet) ≡ suc (number ∘ variables $ α)
-- -- -- --     .there-are-no-functions-of-maximal-arity : number (functions alphabet) zero ≡ zero
-- -- -- --     .shifted-function-matches : ∀ {ytira₀ ytira₁} → finToNat ytira₁ ≡ finToNat ytira₀ → number (functions alphabet) (suc ytira₁) ≡ number (functions α) ytira₀
-- -- -- -- open Alphabet₊ᵥ

-- -- -- -- record Alphabet₊ₛ (α : Alphabet) : Set where
-- -- -- --   constructor α₊ₛ⟨_⟩
-- -- -- --   field
-- -- -- --     alphabet : Alphabet
-- -- -- -- open Alphabet₊ₛ

-- -- -- -- {-
-- -- -- --   toSkolemFormula
-- -- -- --   ∀x(F x v₀ v₁) ⟿ F v₀ v₁ v₂
-- -- -- --   ∃x(F x v₀ v₁) ⟿ F (s₀͍₂ v₀ v₁) v₀ v₁
-- -- -- --   ∀x(F x (s₀͍₂ v₀ v₁) v₁) ⟿ F v₀ (s₀͍₂ v₁ v₂) v₂
-- -- -- --   ∃x(F x (s₀͍₂ v₀ v₁) v₁) ⟿ F (s₀͍₂ v₀ v₁) (s₁͍₂ v₁ v₂) v₂
-- -- -- --   F v₀ ⊗ G v₀ ⟿ F v₀ ⊗ G v₀
-- -- -- --   ∀x(F x v₀ v₁) ⊗ ∀x(G x (s₀͍₂ x v₁) v₁) ⟿ F v₀ v₂ v₃ ⊗ G v₁ (s₀͍₂ v₀ v₃) v₃

-- -- -- --   ∀x(F x v₀ v₁) ⊗ ∃x(G x (s₀͍₂ x v₁) v₁) ⟿ F v₀ v₁ v₂ ⊗ G (s₀͍₁ v₂) (s₁͍₂ (s₀͍₂ v₂) v₂) v₂

-- -- -- --   Φ₀ = ∃x(G x (s₀͍₂ x v₁) v₁) has alphabet of 2 variables, skolem functions: 0, 0, 1
-- -- -- --   this is existential {α₊ₛ} Φ₁, where
-- -- -- --     Φ₁ = G (s₀͍₂ v₀ v₁) (s₁͍₂ (s₀͍₂ v₀ v₁)) v₁
-- -- -- --     α₊ₛ = ⟨ 2 , 0 ∷ 0 ∷ 2 ∷ [] ⟩

-- -- -- --   maybe Φ₋₁ = ∀y∃x(G x (s₀͍₂ x v₀) v₀)
-- -- -- --    and  Φ₋₂ = ∀z∀y∃x(G x (s₀͍₂ x z) z), finally having no free variables, but nevertheless having skolem functions! these are user-defined functions, so this notion of Alphabet is somehow wrong. we have also left out constants (i.e. user-defined skolem-functions of arity 0)

-- -- -- --   Instead, take the alphabet as defining
-- -- -- --     a stack of free variables
-- -- -- --     a matrix (triangle?) of skolem functions

-- -- -- --   Let's try to reverse Φ₁ from a Skolem to a 1st-order formula. Is there a unique way to do it?
-- -- -- --   Φ₀' = ∀x(G (s₀͍₂ x v₀) (s₁͍₂ (s₀͍₂ x v₀)) v₀

-- -- -- --   Nope!

-- -- -- --   toSkolemFormula of

-- -- -- -- -}

-- -- -- -- -- toSkolemFormula (logical Φ₁ Φ₂) ⟿
-- -- -- -- --   let α' , φ₁ = toSkolemFormula Φ₁
-- -- -- -- --       Φ₂' = transcodeToAugmentedAlphabet Φ₂ α'
-- -- -- -- --       α'' , φ₂' = toSkolemFormula Φ₂'
-- -- -- -- --       φ₁' = transcodeToAugmentedAlphabet φ₁ α''

-- -- -- -- {-
-- -- -- -- given Δv = #varibles α' - #variables α
-- -- -- -- for every variable v in α, v in Φ, v stays the same in Φ'
-- -- -- -- for the added variable v⁺ in α₊ - α, v⁺ in Φ, v⁺ ⟿ v⁺ + Δv in transcode (universal {α₊} Φ)
-- -- -- -- α'₊ = α' + 1 variable
-- -- -- -- -}

-- -- -- -- -- record AddVariable (A : Alphabet → Set) : Set where
-- -- -- -- --   field
-- -- -- -- --     addVariableToAlphabet : {α : Alphabet} → A α → {α₊ : Alphabet} → Alphabet₊ᵥ α₊ → A α₊

-- -- -- -- -- instance
-- -- -- -- --   AddVariableFirstOrderFormula : AddVariable FirstOrderFormula
-- -- -- -- --   AddVariableFirstOrderFormula = {!!}

-- -- -- -- -- #variables = number ∘ variables

-- -- -- -- -- #functions_ofArity_ : Alphabet → Nat → Nat
-- -- -- -- -- #functions α⟨ V⟨ #variables ⟩ , S⟨ #functions ⟩ ⟩ ofArity arity = if′ lessNat arity (suc #variables) then #functions (natToFin arity) else 0

-- -- -- -- -- record _⊇_ (α' α : Alphabet) : Set where
-- -- -- -- --   field
-- -- -- -- --     at-least-as-many-variables : #variables α' ≥ #variables α
-- -- -- -- --     at-least-as-many-functions : ∀ {arity} → arity < #variables α → #functions α' ofArity arity ≥ #functions α ofArity arity

-- -- -- -- -- record AddAlphabet (α-top α-bottom : Alphabet) : Set where
-- -- -- -- --   field
-- -- -- -- --     alphabet : Alphabet

-- -- -- -- -- record Transcodeable (A : Alphabet → Set) : Set where
-- -- -- -- --   field
-- -- -- -- --     transcode : {α' α : Alphabet} → ⦃ _ : α' ⊇ α ⦄ → A α → A α'

-- -- -- -- -- open Transcodeable ⦃ … ⦄

-- -- -- -- -- record TransferAlphabet {α' α : Alphabet} (α'⊇α : α' ⊇ α) (α₊ : Alphabet₊ᵥ α) (Φ : FirstOrderFormula (alphabet α₊)) : Set where
-- -- -- -- --   field
-- -- -- -- --     alphabet : Alphabet
-- -- -- -- --     firstOrderFormula : FirstOrderFormula alphabet

-- -- -- -- -- instance
-- -- -- -- --   TranscodeablePredication : Transcodeable Predication
-- -- -- -- --   TranscodeablePredication = {!!}

-- -- -- -- --   TranscodeableAlphabet+Variable : Transcodeable Alphabet₊ᵥ
-- -- -- -- --   TranscodeableAlphabet+Variable = {!!}

-- -- -- -- --   TranscodeableSkolemFormula : Transcodeable SkolemFormula
-- -- -- -- --   TranscodeableSkolemFormula = {!!}

-- -- -- -- --   TranscodeableFirstOrderFormula : Transcodeable FirstOrderFormula
-- -- -- -- --   Transcodeable.transcode TranscodeableFirstOrderFormula (atomic p) = atomic (transcode p)
-- -- -- -- --   Transcodeable.transcode TranscodeableFirstOrderFormula (logical Φ₁ Φ₂) = logical (transcode Φ₁) (transcode Φ₂)
-- -- -- -- --   Transcodeable.transcode TranscodeableFirstOrderFormula {α'} {α} ⦃ α'⊇α ⦄ (universal {α₊} Φ) = {!!} -- universal {_} {_} {transcode α₊} (transcode Φ)

-- -- -- -- --   Transcodeable.transcode TranscodeableFirstOrderFormula (existential Φ) = {!!}

-- -- -- -- -- --(α' α : Alphabet) (α'⊇α : α' ⊇ α) (α₊ : Alphabet+Variable α) (Φ : FirstOrderFormula (alphabet α₊)) → Σ _ λ (α''' : Alphabet) → FirstOrderFormula α'''

-- -- -- -- -- --FirstOrderFormula (alphabet α₊)
-- -- -- -- -- {-
-- -- -- -- -- -}

-- -- -- -- -- -- --transcodeIntoAugmentedAlphabet :

-- -- -- -- -- -- --toSkolemFormula : {α : Alphabet} → FirstOrderFormula α → Σ _ λ (α¹ : AugmentedAlphabet α) → SkolemFormula (alphabet α¹)

-- -- -- -- -- -- --record IsEquivalentFormulas {α₀ : Alphabet} (φ₀ : SkolemFormula α₀) {α₁ : Alphabet} (Φ₁ : FirstOrderFormula α₁) : Set where
-- -- -- -- -- -- --  field
-- -- -- -- -- -- --    .atomicCase : {p : Predication α₀} → φ₀ ≡ atomic p → Φ₁ ≡ atomic p

-- -- -- -- -- -- -- --
-- -- -- -- -- -- -- -- record Alphabet+Alphabet (α₀ α₁ α₂ : Alphabet) : Set where
-- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- --     alphabet :

-- -- -- -- -- -- -- -- ∀xφ₁(x) ⊗ φ₂ ⟿ ∀x(φ₁ ⊗ φ₂)

-- -- -- -- -- -- -- -- hasQuantifiers : FirstOrderFormula α → Bool

-- -- -- -- -- -- -- --record Skolemization {α : Alphabet} (φ : FirstOrderFormula α) : Set where
-- -- -- -- -- -- -- --  field
-- -- -- -- -- -- -- --    alphabet : Alphabet
-- -- -- -- -- -- -- --    skolemization : SkolemFormula alphabet

-- -- -- -- -- -- -- record _IsAugmentationOf_ (α₁ α₀ : Alphabet) : Set where

-- -- -- -- -- -- -- record AugmentedAlphabet (α : Alphabet) : Set where
-- -- -- -- -- -- --   constructor ⟨_⟩
-- -- -- -- -- -- --   field
-- -- -- -- -- -- --     alphabet : Alphabet
-- -- -- -- -- -- --     ..laws : alphabet ≡ α
-- -- -- -- -- -- -- open AugmentedAlphabet

-- -- -- -- -- -- -- trivialAugmentation : (α : Alphabet) → AugmentedAlphabet α
-- -- -- -- -- -- -- trivialAugmentation = {!!}

-- -- -- -- -- -- -- record DisjointRelativeUnion {α : Alphabet} (α¹ α² : AugmentedAlphabet α) : Set where
-- -- -- -- -- -- --   constructor ⟨_⟩
-- -- -- -- -- -- --   field
-- -- -- -- -- -- --     augmentation : AugmentedAlphabet α
-- -- -- -- -- -- --     .laws : {!!}
-- -- -- -- -- -- -- open DisjointRelativeUnion

-- -- -- -- -- -- -- disjointRelativeUnion : {α : Alphabet} → (α¹ α² : AugmentedAlphabet α) → DisjointRelativeUnion α¹ α²
-- -- -- -- -- -- -- disjointRelativeUnion = {!!}

-- -- -- -- -- -- -- -- inAugmentedAlphabet : {α : Alphabet} → (α¹ : AugmentedAlphabet α) → SkolemFormula α → SkolemFormula (alphabet α¹)
-- -- -- -- -- -- -- -- inAugmentedAlphabet = {!!}

-- -- -- -- -- -- -- -- toSkolemFormula : {α : Alphabet} → FirstOrderFormula α → Σ _ λ (α¹ : AugmentedAlphabet α) → SkolemFormula (alphabet α¹)
-- -- -- -- -- -- -- -- toSkolemFormula {α₀} (atomic 𝑃) = trivialAugmentation α₀ , atomic 𝑃
-- -- -- -- -- -- -- -- toSkolemFormula {α₀} (logical φ₁ φ₂) with toSkolemFormula φ₁ | toSkolemFormula φ₂
-- -- -- -- -- -- -- -- toSkolemFormula {α₀} (logical φ₁ φ₂) | α¹ , Φ₁ | α² , Φ₂ = augmentation (disjointRelativeUnion α¹ α²) , logical {!inAugmentedAlphabet (augmentation (disjointRelativeUnion α¹ α²)) Φ₁!} {!Φ₂!}
-- -- -- -- -- -- -- -- toSkolemFormula {α₀} (universal x) = {!!}
-- -- -- -- -- -- -- -- toSkolemFormula {α₀} (existential x) = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula : ∀ {alphabet₀} → QFormula alphabet₀ → Σ _ λ alphabet₁ → NQFormula alphabet₁
-- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (atomic name terms) = alphabet₀ , atomic name terms
-- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (logical formula₁ formula₂) with toNQFormula formula₁ | toNQFormula formula₂
-- -- -- -- -- -- -- -- -- -- -- -- -- -- ... | alphabet₁ , nqFormula₁ | alphabet₂ , nqFormula₂ = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (universal formula) = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (existential formula) = {!!}

-- -- -- -- -- -- -- -- -- -- -- --VariableName = Fin ∘ |v|
-- -- -- -- -- -- -- -- -- -- -- --FunctionArity = Fin ∘ suc ∘ size
-- -- -- -- -- -- -- -- -- -- -- --FunctionName = λ alphabet ytira → Fin (|f| alphabet ytira)

-- -- -- -- -- -- -- -- -- -- -- -- record Alphabet : Set where
-- -- -- -- -- -- -- -- -- -- -- --   constructor ⟨_,_⟩
-- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- --     |v| : Nat -- number of variables
-- -- -- -- -- -- -- -- -- -- -- --     |f| : Fin (suc |v|) → Nat -- number of functions of each arity, |v| through 0

-- -- -- -- -- -- -- -- -- -- -- -- open Alphabet

-- -- -- -- -- -- -- -- -- -- -- -- -- VariableName = Fin ∘ |v|
-- -- -- -- -- -- -- -- -- -- -- -- -- FunctionArity = Fin ∘ suc ∘ |v|
-- -- -- -- -- -- -- -- -- -- -- -- -- FunctionName = λ alphabet ytira → Fin (|f| alphabet ytira)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- data Term {i : Size} (alphabet : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- --   variable : VariableName alphabet → Term alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- --   function : ∀ {arity : FunctionArity alphabet} →
-- -- -- -- -- -- -- -- -- -- -- -- -- --              FunctionName alphabet (natToFin (|v| alphabet) - arity) →
-- -- -- -- -- -- -- -- -- -- -- -- -- --              ∀ {j : Size< i} → Vec (Term {j} alphabet) (finToNat arity) →
-- -- -- -- -- -- -- -- -- -- -- -- -- --              Term {i} alphabet

-- -- -- -- -- -- -- -- -- -- -- -- -- -- PredicateArity = Nat
-- -- -- -- -- -- -- -- -- -- -- -- -- -- PredicateName = Nat

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- a zeroth-order formula? (i.e. no quantifiers)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- data NQFormula {i : Size} (alphabet : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- --   atomic : PredicateName → ∀ {arity} → Vec (Term alphabet) arity → NQFormula alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- --   logical : {j : Size< i} → NQFormula {j} alphabet → {k : Size< i} → NQFormula {k} alphabet → NQFormula {i} alphabet

-- -- -- -- -- -- -- -- -- -- -- -- -- -- record AugmentedByVariable (alphabet₀ alphabet₁ : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- --     one-variable-is-added : |v| alphabet₁ ≡ suc (|v| alphabet₀)
-- -- -- -- -- -- -- -- -- -- -- -- -- --     function-domain-is-zero-at-new-variable : |f| alphabet₁ zero ≡ 0
-- -- -- -- -- -- -- -- -- -- -- -- -- --     shifted-function-matches : ∀ {ytira₀ ytira₁} → finToNat ytira₁ ≡ finToNat ytira₀ → |f| alphabet₁ (suc ytira₁) ≡ |f| alphabet₀ ytira₀

-- -- -- -- -- -- -- -- -- -- -- -- -- -- record AugmentVariables (alphabet₀ : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- --     alphabet₁ : Alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- --     augmentation : AugmentedByVariable alphabet₀ alphabet₁

-- -- -- -- -- -- -- -- -- -- -- -- -- -- open AugmentVariables

-- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentVariables : (alphabet : Alphabet) → AugmentVariables alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentVariables ⟨ |v| , |f| ⟩ =
-- -- -- -- -- -- -- -- -- -- -- -- -- --   record
-- -- -- -- -- -- -- -- -- -- -- -- -- --   { alphabet₁ = ⟨ suc |v| , (λ { zero → zero ; (suc ytira) → |f| ytira}) ⟩
-- -- -- -- -- -- -- -- -- -- -- -- -- --   ; augmentation =
-- -- -- -- -- -- -- -- -- -- -- -- -- --     record
-- -- -- -- -- -- -- -- -- -- -- -- -- --     { one-variable-is-added = refl
-- -- -- -- -- -- -- -- -- -- -- -- -- --     ; function-domain-is-zero-at-new-variable = refl
-- -- -- -- -- -- -- -- -- -- -- -- -- --     ; shifted-function-matches = cong |f| ∘ finToNat-inj } }

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |f|₀ = |f|₀ + 1
-- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentFunctions : Alphabet → Alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentFunctions ⟨ |v| , |f| ⟩ = ⟨ |v| , (λ { zero → suc (|f| zero) ; (suc ytira) → |f| (suc ytira) }) ⟩

-- -- -- -- -- -- -- -- -- -- -- -- -- -- data QFormula {i : Size} (alphabet : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- --   atomic : PredicateName → ∀ {arity} → Vec (Term alphabet) arity → QFormula alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- --   logical : {j : Size< i} → QFormula {j} alphabet → {k : Size< i} → QFormula {k} alphabet → QFormula {i} alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- --   universal : QFormula (alphabet₁ (augmentVariables alphabet)) → QFormula alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- --   existential : QFormula (augmentFunctions alphabet) → QFormula alphabet

-- -- -- -- -- -- -- -- -- -- -- -- -- -- record Assignment (alphabet : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- --   constructor ⟨_,_⟩
-- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- --     μ : VariableName alphabet → Domain
-- -- -- -- -- -- -- -- -- -- -- -- -- --     𝑓 : ∀ {arity} → FunctionName alphabet arity → Vec Domain (finToNat arity) → Domain

-- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateTerm : ∀ {i alphabet} → Assignment alphabet → Term {i} alphabet → Domain
-- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateTerm ⟨ μ , _ ⟩ (variable x) = μ x
-- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateTerm 𝑎@(⟨ μ , 𝑓 ⟩) (function f x) = 𝑓 f (evaluateTerm 𝑎 <$> x)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- record Interpretation (alphabet : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- --   constructor ⟨_,_⟩
-- -- -- -- -- -- -- -- -- -- -- -- -- --   open Assignment
-- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- --     𝑎 : Assignment alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- --     𝑃 : PredicateName → ∀ {arity} → Vec Domain arity → Bool

-- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateNQFormula : ∀ {i alphabet} → Interpretation alphabet → NQFormula {i} alphabet → Bool
-- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateNQFormula ⟨ 𝑎 , 𝑃 ⟩ (atomic name terms) = 𝑃 name $ evaluateTerm 𝑎 <$> terms
-- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateNQFormula I (logical formula₁ formula₂) = not (evaluateNQFormula I formula₁) && not (evaluateNQFormula I formula₂)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula : ∀ {alphabet₀} → QFormula alphabet₀ → Σ _ λ alphabet₁ → NQFormula alphabet₁
-- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (atomic name terms) = alphabet₀ , atomic name terms
-- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (logical formula₁ formula₂) with toNQFormula formula₁ | toNQFormula formula₂
-- -- -- -- -- -- -- -- -- -- -- -- -- -- ... | alphabet₁ , nqFormula₁ | alphabet₂ , nqFormula₂ = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (universal formula) = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (existential formula) = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- record IsADisjointUnionOfNQFormulas
-- -- -- -- -- -- -- -- -- -- -- -- -- --        {alphabet₁ alphabet₂ alphabet₁₊₂ : Alphabet}
-- -- -- -- -- -- -- -- -- -- -- -- -- --        (formula₁ : NQFormula alphabet₁)
-- -- -- -- -- -- -- -- -- -- -- -- -- --        (formula₂ : NQFormula alphabet₂)
-- -- -- -- -- -- -- -- -- -- -- -- -- --        (formula₁₊₂ : NQFormula alphabet₁₊₂)
-- -- -- -- -- -- -- -- -- -- -- -- -- --        : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- --     alphabet-size : |v| alphabet₁₊₂ ≡ |v| alphabet₁ + |v| alphabet₂
-- -- -- -- -- -- -- -- -- -- -- -- -- --     --|f| alphabet₁₊₂ ytira

-- -- -- -- -- -- -- -- -- -- -- -- -- -- ----record AlphabetSummed  (alphabet₀ alphabet₁ : Alphabet)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- -- -- -- -- -- -- -- -- -- -- -- -- -- --addAlphabets : Alphabet → Alphabet → Alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- --addAlphabets ⟨ |v|₁ , |f|₁ ⟩ ⟨ |v|₂ , |f|₂ ⟩ = ⟨ (|v|₁ + |v|₂) , (λ x → if′ finToNat x ≤? |v|₁ && finToNat x ≤? |v|₂ then {!!} else {!!}) ⟩

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- sup : ∀ {alphabet₁} → Formula alphabet₁ → ∀ {alphabet₂} → Formula alphabet₂ → Σ _ λ alphabet₁₊₂ → Formula alphabet₁₊₂ × Formula alphabet₁₊₂
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- sup {⟨ |v|₁ , |a|₁ , |f|₁ ⟩} φ₁ {⟨ |v|₂ , |a|₂ , |f|₂ ⟩} φ₂ = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- pnf : ∀ {alphabet} → Formula alphabet → Σ _ λ alphabet+ → Formula₀ alphabet+
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- pnf = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --universal (P 0) = ∀ x → P x
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- (∀ x ∃ y (P x y)) ∨ (∀ x ∃ y (P x y))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- P x₀ (s₀͍₁ x₀) ∨ P x₁ (s₁͍₁ x₁)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   extended|f| : (arity : Arity) → Vec ℕ (suc |a|) → Vec ℕ (++arity (max arity |a|))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   extended|f| = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- add a variable to the alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentVariables : Alphabet → Alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentVariables = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- increaseTabulationAtN : ∀ {n} → Fin n → (Fin n → Nat) → Fin n → Nat
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- increaseTabulationAtN = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record AugmentedFunctions {|a| : Arity} (arity : Arity) (|f| : Vec ℕ (++arity |a|)) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     maxA : ℕ
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     maxA-law : max arity |a| ≡ maxA
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     ++|f| : Vec ℕ maxA
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     f-law : increaseTabulationAt arity (indexVec |f|)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- {-

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- define
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- a ⊗ b ≡ False a and False b

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- now, we can define
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- ¬a = a ⊗ a ≡ False a and False a
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- a ∨ b = ¬(a ⊗ b) ≡ False (False a and False b) and False (False a and False b)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- a ∧ b = ¬(¬a ∨ ¬b) = ¬(¬(¬a ⊗ ¬b)) = ¬a ⊗ ¬b = False (False a and False a) and False (False b and False b)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- a → b = ¬a ∨ b = (a ⊗ a) ∨ b = ¬((a ⊗ a) ⊗ b) = ((a ⊗ a) ⊗ b) ⊗ ((a ⊗ a) ⊗ b)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- conversion to prenex
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- ∀xF ⊗ G ⟿ ∃x(F ⊗ wk(G))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- ∃xF ⊗ G ⟿ ∀x(F ⊗ wk(G))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- F ⊗ ∀xG ⟿ ∃x(wk(F) ⊗ G)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- F ⊗ ∃xG ⟿ ∀x(wk(F) ⊗ G)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- ========================
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- (a ⊗ ∀xB) ⊗ c ⟿ ∃x(wk(a) ⊗ B) ⊗ c ⟿ ∀x((wk(a) ⊗ B) ⊗ wk(c))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF : (arity : Arity) → ∀ {|a| : Arity} → Vec ℕ (++arity |a|) → Vec ℕ (++arity (max arity |a|))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f|
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --  with decBool (lessNat |a| arity)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f| | yes x with compare arity |a|
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {.(suc (k + arity))} |f| | yes x | less (diff k refl) = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {.arity} |f| | yes x | equal refl with lessNat arity arity
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {.arity} |f| | yes x | equal refl | false = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF zero {.zero} |f| | yes true | equal refl | true = {!!} ∷ []
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF (suc arity) {.(suc arity)} |f| | yes true | equal refl | true = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f| | yes x | greater gt = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f| | no x with decBool (lessNat arity |a|)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f| | no x₁ | yes x = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f| | no x₁ | no x = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- = case arity <? |a| of λ { false → {!!} ; true → {!!} }

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- add a function of a given arity to the alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentFunctions : Arity → Alphabet → Alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentFunctions arity ⟨ |v| , |a| , |f| ⟩ = ⟨ |v| , max arity |a| , augmentF arity |f| ⟩

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record Alphabet : Set where

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data DomainSignifier : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   free : Nat → DomainSignifier

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data PartiallyAppliedFunction : Nat → Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   constant : PartiallyAppliedFunction 0
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   function : ∀ {n} → PartiallyAppliedFunction 0 → PartiallyAppliedFunction (suc n)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- Term = PartiallyAppliedFunction 0

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data PartialyAppliedPredicate : Nat → Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   statement : PartialyAppliedPredicate 0
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   partial : ∀

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record Language : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   field

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- Name = String

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record Function : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     name : Name
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     number-of-arguments : Nat

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- Vec

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data Function : Set where

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data Term : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   function : Function →

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data Sentence : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   predication : Name →

-- -- -- -- {-

-- -- -- -- record Variables : Set where
-- -- -- --   constructor V⟨_⟩
-- -- -- --   field
-- -- -- --     number : Nat
-- -- -- -- open Variables

-- -- -- -- record Functions (υ : Variables) : Set where
-- -- -- --   constructor S⟨_⟩
-- -- -- --   field
-- -- -- --     number : Fin (suc (number υ)) → Nat
-- -- -- -- open Functions

-- -- -- -- record Alphabet : Set where
-- -- -- --   constructor α⟨_,_⟩
-- -- -- --   field
-- -- -- --     variables : Variables
-- -- -- --     functions : Functions variables
-- -- -- -- open Alphabet

-- -- -- -- record Variable (α : Alphabet) : Set where
-- -- -- --   constructor v⟨_⟩
-- -- -- --   field
-- -- -- --     name : Fin (number (variables α))
-- -- -- -- open Variable

-- -- -- -- record Function (α : Alphabet) : Set where
-- -- -- --   constructor s⟨_,_⟩
-- -- -- --   field
-- -- -- --     arity : Fin ∘ suc ∘ number ∘ variables $ α
-- -- -- --     name : Fin $ number (functions α) arity
-- -- -- -- open Function

-- -- -- -- data Term (𝑽 : Nat) : Set where
-- -- -- --   variable : Fin 𝑽 → Term 𝑽
-- -- -- --   function : (𝑓 : Function α) → {ι₋₁ : Size< ι₀} → Vec (Term {ι₋₁} α) (finToNat (arity 𝑓)) →
-- -- -- --              Term {ι₀} α

-- -- -- -- record Predication (alphabet : Alphabet) : Set where
-- -- -- --   constructor P⟨_,_,_⟩
-- -- -- --   field
-- -- -- --     name : Nat
-- -- -- --     arity : Nat
-- -- -- --     terms : Vec (Term alphabet) arity
-- -- -- -- open Predication
-- -- -- -- -}


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

module Data.Binary.Operations.Semantics where

open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Binary.Definitions
open import Data.Binary.Operations.Unary
import Data.List as List

2* : ℕ → ℕ
2* x = x ℕ.+ x
{-# INLINE 2* #-}

_∷⇓_ : Bit → ℕ → ℕ
O ∷⇓ xs = 2* xs
I ∷⇓ xs = suc (2* xs)
{-# INLINE _∷⇓_ #-}

⟦_⇓⟧⁺ : 𝔹⁺ → ℕ
⟦_⇓⟧⁺ = List.foldr _∷⇓_ 1
{-# INLINE ⟦_⇓⟧⁺ #-}

⟦_⇓⟧ : 𝔹 → ℕ
⟦ 0ᵇ ⇓⟧ = 0
⟦ 0< xs ⇓⟧ = ⟦ xs ⇓⟧⁺

⟦_⇑⟧ : ℕ → 𝔹
⟦ zero ⇑⟧ = 0ᵇ
⟦ suc n ⇑⟧ = inc ⟦ n ⇑⟧

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
module Support.Nat where

open import Support

data _<_ : (n m : ℕ) → Set where
  Z<Sn : {n : ℕ} → zero < suc n
  raise< : {n m : ℕ} (n<m : n < m) → suc n < suc m

infix 5 _>_
_>_ : (m n : ℕ) → Set
_>_ = flip _<_

infixr 7 _+_
_+_ : (n m : ℕ) → ℕ
zero + m = m
suc n + m = suc (n + m)

infixr 9 _*_
_*_ : (n m : ℕ) → ℕ
zero * m = zero
(suc n) * m = m + n * m

+-is-nondecreasingʳ : ∀ (n m : ℕ) → n < suc (n + m)
+-is-nondecreasingʳ zero m = Z<Sn
+-is-nondecreasingʳ (suc y) m = raise< (+-is-nondecreasingʳ y m)

+-idˡ : ∀ a → 0 + a ≣ a
+-idˡ a = ≣-refl

+-idʳ : ∀ a → a + 0 ≣ a
+-idʳ zero = ≣-refl
+-idʳ (suc y) = ≣-cong suc (+-idʳ y)

+-assocˡ : ∀ a b c → (a + b) + c ≣ a + (b + c)
+-assocˡ zero b c = ≣-refl
+-assocˡ (suc a) b c = ≣-cong suc (+-assocˡ a b c)

+-assocʳ : ∀ a b c → a + (b + c) ≣ (a + b) + c
+-assocʳ zero b c = ≣-refl
+-assocʳ (suc a) b c = ≣-cong suc (+-assocʳ a b c)

+-sucˡ : ∀ a b → suc a + b ≣ suc (a + b)
+-sucˡ a b = ≣-refl

+-sucʳ : ∀ a b → a + suc b ≣ suc (a + b)
+-sucʳ zero b = ≣-refl
+-sucʳ (suc y) b = ≣-cong suc (+-sucʳ y b)

+-comm : ∀ a b → a + b ≣ b + a
+-comm a zero = +-idʳ a
+-comm a (suc y) = ≣-trans (≣-cong suc (+-comm a y)) (+-sucʳ a y)

*-killˡ : ∀ a → 0 * a ≣ 0
*-killˡ a = ≣-refl

*-killʳ : ∀ a → a * 0 ≣ 0
*-killʳ zero = ≣-refl
*-killʳ (suc y) = *-killʳ y

*-idˡ : ∀ a → 1 * a ≣ a
*-idˡ a = +-idʳ a

*-idʳ : ∀ a → a * 1 ≣ a
*-idʳ zero = ≣-refl
*-idʳ (suc y) = ≣-cong suc (*-idʳ y)

*-dist-+ˡ : ∀ a b c → a * (b + c) ≣ a * b + a * c
*-dist-+ˡ zero b c = ≣-refl
*-dist-+ˡ (suc y) b c =
  begin
    (b + c) + y * (b + c)
  ≈⟨ ≣-cong (_+_ (b + c)) (*-dist-+ˡ y b c) ⟩
    (b + c) + y * b + y * c
  ≈⟨ +-assocʳ (b + c) (y * b) (y * c) ⟩
    ((b + c) + y * b) + y * c
  ≈⟨ ≣-cong (λ x → (x + y * b) + y * c) (+-comm b c) ⟩
    ((c + b) + y * b) + y * c
  ≈⟨ ≣-cong (λ x → x + y * c) (+-assocˡ c b (y * b)) ⟩
    (c + b + y * b) + y * c
  ≈⟨ ≣-cong (λ x → x + y * c) (+-comm c (b + y * b)) ⟩
    ((b + y * b) + c) + y * c
  ≈⟨ +-assocˡ (b + y * b) c (y * c) ⟩
    (b + y * b) + c + y * c
  ∎
  where open ≣-reasoning ℕ

*-dist-+ʳ : ∀ a b c → (a + b) * c ≣ a * c + b * c
*-dist-+ʳ zero b c = ≣-refl
*-dist-+ʳ (suc y) b c = ≣-trans (+-assocʳ c (y * c) (b * c)) (≣-cong (_+_ c) (*-dist-+ʳ y b c))

*-assocˡ : ∀ a b c → (a * b) * c ≣ a * (b * c)
*-assocˡ zero b c = ≣-refl
*-assocˡ (suc y) b c = ≣-trans (≣-cong (_+_ (b * c)) (*-assocˡ y b c))
                         (*-dist-+ʳ b (y * b) c)

*-assocʳ : ∀ a b c → (a * b) * c ≣ a * (b * c)
*-assocʳ zero b c = ≣-refl
*-assocʳ (suc y) b c = ≣-trans (≣-cong (_+_ (b * c)) (*-assocʳ y b c))
                         (*-dist-+ʳ b (y * b) c)

*-sucˡ : ∀ a b → (suc a) * b ≣ b + a * b
*-sucˡ a b = ≣-refl

*-sucʳ : ∀ a b → a * (suc b) ≣ a + a * b
*-sucʳ zero b = ≣-refl
*-sucʳ (suc y) b = ≣-cong suc (
    begin
      b + y * suc b
    ≈⟨ ≣-cong (_+_ b) (*-sucʳ y b) ⟩
      b + y + y * b
    ≈⟨ +-assocʳ b y (y * b) ⟩
      (b + y) + y * b
    ≈⟨ ≣-cong (λ x → x + y * b) (+-comm b y) ⟩
      (y + b) + y * b
    ≈⟨ +-assocˡ y b (y * b) ⟩
      y + b + y * b
    ∎)
  where open ≣-reasoning ℕ

*-comm : ∀ a b → a * b ≣ b * a
*-comm a zero = *-killʳ a
*-comm a (suc y) =
    begin
      a * suc y
    ≈⟨ *-sucʳ a y ⟩
      a + a * y
    ≈⟨ ≣-cong (_+_ a) (*-comm a y) ⟩
      a + y * a
    ∎
  where open ≣-reasoning ℕ
<-irref : ∀ {n} → ¬ (n < n)
<-irref (raise< n<m) = <-irref n<m

<-trans : ∀ {l m n} → (l < m) → (m < n) → (l < n)
<-trans Z<Sn (raise< n<m) = Z<Sn
<-trans (raise< n<m) (raise< n<m') = raise< (<-trans n<m n<m')

<-trans-assoc : ∀ {a b c d} → {a<b : a < b} {b<c : b < c} {c<d : c < d} → <-trans a<b (<-trans b<c c<d) ≣ <-trans (<-trans a<b b<c) c<d
<-trans-assoc {a<b = Z<Sn} {raise< b<c} {raise< c<d} = ≣-refl
<-trans-assoc {a<b = raise< a<b} {raise< b<c} {raise< c<d} = ≣-cong raise< <-trans-assoc

<-unsucʳ : ∀ {m n} → m < suc n → Either (m ≣ n) (m < n)
<-unsucʳ (Z<Sn {zero}) = inl ≣-refl
<-unsucʳ (Z<Sn {suc y}) = inr Z<Sn
<-unsucʳ (raise< {n} {zero} ())
<-unsucʳ (raise< {n} {suc y} n<m) = (≣-cong suc +++ raise<) (<-unsucʳ n<m)

<-unsucˡ : ∀ {m n} → suc m < n → m < n
<-unsucˡ (raise< {zero} Z<Pn) = Z<Sn
<-unsucˡ (raise< {suc y} Sy<Pn) = raise< (<-unsucˡ Sy<Pn)

<-sucˡ : ∀ {m n} → m < n → Either (suc m ≣ n) (suc m < n)
<-sucˡ (Z<Sn {zero}) = inl ≣-refl
<-sucˡ (Z<Sn {suc y}) = inr (raise< Z<Sn)
<-sucˡ (raise< n<m) = (≣-cong suc +++ raise<) (<-sucˡ n<m)

<-sucʳ : ∀ {m n} → m < n → m < suc n
<-sucʳ Z<Sn = Z<Sn
<-sucʳ (raise< Pm<Pn) = raise< (<-sucʳ Pm<Pn)

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module _ where

A : Set₁
A = Set

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- Conat properties
------------------------------------------------------------------------------

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

module FOTC.Data.Conat.PropertiesI where

open import FOTC.Base
open import FOTC.Data.Conat
open import FOTC.Data.Nat

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, then the
-- Conat predicate is also a pre-fixed point of the functional NatF,
-- i.e.
--
-- NatF Conat ≤ Conat (see FOTC.Data.Conat.Type).
Conat-in : ∀ {n} →
           n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n') →
           Conat n
Conat-in h = Conat-coind A h' h
  where
  A : D → Set
  A n = n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n')

  h' : ∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')
  h' (inj₁ n≡0)              = inj₁ n≡0
  h' (inj₂ (n' , prf , Cn')) = inj₂ (n' , prf , Conat-out Cn')

0-Conat : Conat zero
0-Conat = Conat-coind A h refl
  where
  A : D → Set
  A n = n ≡ zero

  h : ∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')
  h An = inj₁ An

-- Adapted from (Sander 1992, p. 57).
∞-Conat : Conat ∞
∞-Conat = Conat-coind A h refl
  where
  A : D → Set
  A n = n ≡ ∞

  h : ∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')
  h An = inj₂ (∞ , trans An ∞-eq , refl)

N→Conat : ∀ {n} → N n → Conat n
N→Conat Nn = Conat-coind N h Nn
  where
  h : ∀ {m} → N m → m ≡ zero ∨ (∃[ m' ] m ≡ succ₁ m' ∧ N m')
  h nzero          = inj₁ refl
  h (nsucc {m} Nm) = inj₂ (m , refl , Nm)

-- A different proof.
N→Conat' : ∀ {n} → N n → Conat n
N→Conat' nzero          = Conat-in (inj₁ refl)
N→Conat' (nsucc {n} Nn) = Conat-in (inj₂ (n , refl , (N→Conat' Nn)))

------------------------------------------------------------------------------
-- References
--
-- Sander, Herbert P. (1992). A Logic of Functional Programs with an
-- Application to Concurrency. PhD thesis. Department of Computer
-- Sciences: Chalmers University of Technology and University of
-- Gothenburg.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Everything where
-- The development can almost entirely be type-checked using --safe,
-- We mark modules that use the TERMINATING pragma with (**)
-- And one module that uses --rewriting with (*).
-- These are the only modules that Agda does not accept ass --safe.

--  # First we summarize the library we use by Rouvoet et al '20, CPP.
--
--  Our work contributes various improvements to the library.
--  In particular, its generalization relations whose underlying
--  equivalence is not propositional equality.
--  But also various additions to the parts of the library
--  mentioned below.

-- Core defines what a proof-relevant ternary relation (Rel₃).
import Relation.Ternary.Core

-- Structures defines type classes for ternary relations.
-- A PRSA is a commutative monoid and should implement:
--   - IsPartialMonoid <: IsPartialSemigroup
--   - IsCommutative
import Relation.Ternary.Structures

-- The overloaded syntax of separation logic comes from:
import Relation.Ternary.Structures.Syntax

-- Resource aware versions of data types that we use are defined generically
-- in Relation.Ternary.Data:
import Relation.Ternary.Data.Bigstar             -- 'Star' in figure 5 of the paper
import Relation.Ternary.Data.Bigplus             -- 'Plus'
import Relation.Ternary.Data.ReflexiveTransitive -- 'IStar'

-- The computational structures from the library that we use in the paper
import Relation.Ternary.Functor
import Relation.Ternary.Monad

-- # We make the following additions to the library, that we describe in the paper.

-- A generic PRSA for list separation modulo permutations.
-- It is generic in the sense that it is parameterized in a PRSA on its elements.
-- We prove that it is a PRSA, with various additional properties that are
-- crucial for the model construction in the paper.
import Relation.Ternary.Construct.Bag
import Relation.Ternary.Construct.Bag.Properties

-- A generic PRSA Exchange, that generalizes the interface composition relation.
import Relation.Ternary.Construct.Exchange

-- Its construction is generic in 2 PRSAs that obey some properties.
-- These properties are formalized as type-classes on ternary relations
import Relation.Ternary.Structures.Positive
import Relation.Ternary.Structures.Crosssplit

-- We added the writer monad construction described in the paper.
import Relation.Ternary.Monad.Writer

-- # We then formalize the typed language CF, and typed bytecode,
-- and implement the typed compilation backend.

-- The model:
-- The bag separation implements the 'disjoint' and the 'overlapping' context
-- separation from the paper, depending on how you instantiate it.
-- The instantiation is done in the JVM model construction.
-- Here we also instantiate Exchange to obtain interface composition.
import JVM.Model

-- Syntax of bytecode
import JVM.Types
import JVM.Syntax.Instructions
import JVM.Syntax.Bytecode

-- The Compiler monad
import JVM.Compiler.Monad

-- The source language
import CF.Types
import CF.Syntax           -- co-contextual
import CF.Syntax.Hoisted   -- co-contextual without local variable introductions
import CF.Syntax.DeBruijn  -- contextual

import CF.Transform.Hoist               -- hoisting local variable declarations (**)
import CF.Transform.UnCo                -- contextualizing (**)
import CF.Transform.Compile.Expressions -- compiling expressions
import CF.Transform.Compile.Statements  -- compiling statements
import CF.Transform.Compile.ToJVM       -- typeclass for type translation
import JVM.Transform.Noooops            -- bytecode optimization that removes nops
import JVM.Transform.Assemble           -- bytecode translation to absolute jumps (*)
import JVM.Printer                      -- printer for co-contextual bytecode to Jasmin (not verified) (**)

-- Example compilations.
-- These can be run by first compiling them using `make examples`.
-- The output will be in _build/bin/
import CF.Examples.Ex1 -- (*,**)
import CF.Examples.Ex2 -- (*,**)


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

module Data.Fin.Injective where

open import Prelude

open import Data.Fin.Base
open import Data.Fin.Properties using (discreteFin)

open import Data.Nat
open import Data.Nat.Properties using (+-comm)

open import Function.Injective

private
  variable n m : ℕ

infix 4 _≢ᶠ_ _≡ᶠ_
_≢ᶠ_ _≡ᶠ_ : Fin n → Fin n → Type _
n ≢ᶠ m = T (not (discreteFin n m .does))
n ≡ᶠ m = T (discreteFin n m .does)

_F↣_ : ℕ → ℕ → Type
n F↣ m = Σ[ f ⦂ (Fin n → Fin m) ] × ∀ {x y} → x ≢ᶠ y → f x ≢ᶠ f y

shift : (x y : Fin (suc n)) → x ≢ᶠ y → Fin n
shift          f0     (fs y)  x≢y = y
shift {suc _}  (fs x)  f0     x≢y = f0
shift {suc _}  (fs x)  (fs y)  x≢y = fs (shift x y x≢y)

shift-inj : ∀ (x y z : Fin (suc n)) x≢y x≢z → y ≢ᶠ z → shift x y x≢y ≢ᶠ shift x z x≢z
shift-inj          f0     (fs y)  (fs z)  x≢y x≢z x+y≢x+z = x+y≢x+z
shift-inj {suc _}  (fs x)  f0     (fs z)  x≢y x≢z x+y≢x+z = tt
shift-inj {suc _}  (fs x)  (fs y)  f0     x≢y x≢z x+y≢x+z = tt
shift-inj {suc _}  (fs x)  (fs y)  (fs z)  x≢y x≢z x+y≢x+z = shift-inj x y z x≢y x≢z x+y≢x+z

shrink : suc n F↣ suc m → n F↣ m
shrink (f , inj) .fst  x  = shift (f f0) (f (fs x)) (inj tt)
shrink (f , inj) .snd  p  = shift-inj (f f0) (f (fs _)) (f (fs _)) (inj tt) (inj tt) (inj p)

¬plus-inj : ∀ n m → ¬ (suc (n + m) F↣ m)
¬plus-inj zero     zero     (f , _)  = f f0
¬plus-inj zero     (suc m)  inj      = ¬plus-inj zero m (shrink inj)
¬plus-inj (suc n)  m        (f , p)  = ¬plus-inj n m (f ∘ fs , p)

toFin-inj : (Fin n ↣ Fin m) → n F↣ m
toFin-inj f .fst = f .fst
toFin-inj (f , inj) .snd {x} {y} x≢ᶠy with discreteFin x y | discreteFin (f x) (f y)
... | no ¬p  | yes p  = ¬p (inj _ _ p)
... | no _   | no _   = tt

n≢sn+m : ∀ n m → Fin n ≢ Fin (suc (n + m))
n≢sn+m n m n≡m =
  ¬plus-inj m n
    (toFin-inj
      (subst
        (_↣ Fin n)
        (n≡m ; cong (Fin ∘ suc) (+-comm n m))
        refl-↣))

Fin-inj : Injective Fin
Fin-inj n m eq with compare n m
... | equal _        = refl
... | less     n  k  = ⊥-elim (n≢sn+m n k eq)
... | greater  m  k  = ⊥-elim (n≢sn+m m k (sym eq))

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module _ where

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

postulate
  C : Set → Set

record R (F : Nat → Set) : Set where
  field
    n : Nat
    ⦃ iC ⦄ : C (F n)

postulate
  T : Nat → Set
  instance
    iCT5 : C (T 5)

module _ (n m : Nat) where
  foo : n ≡ suc m → Nat → Set
  foo refl p = Nat
    where
      bar : R T
      R.n bar = 5

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda