text:
module MGU where

--open import Agda.Builtin.Nat using () renaming (Nat to ℕ)
open import Agda.Primitive
open import Agda.Builtin.Equality

open import Prelude.Product using (Σ; _,_; fst; snd; _×_; curry; uncurry)
open import Prelude.Equality using (_≡_; eqReasoningStep; _∎; sym; trans; cong)
open import Prelude.Function using (_∘_)
open import Prelude.Empty using (⊥)
open import Prelude.Sum using () renaming (Either to _⊎_)
open import Prelude.Maybe using (Maybe; just; nothing)

∃ : ∀ {a b} {A : Set a} (B : A → Set b) → Set (a ⊔ b)
∃ = Σ _

open import Prelude using (_$_)

open import Relation.Binary
open import Algebra
open import Category.Applicative.Predicate

open import Prolegomenon

--record IsTermSubstitution {ℓᵗ} {ℓ⁼ᵗ} {ℓˢ} {ℓ⁼ˢ}

record IsSetoid {c} {ℓ} {Carrier : Set c} (_≈_ : Rel Carrier ℓ) : Set (c ⊔ ℓ) where
  field
    isEquivalence : IsEquivalence _≈_

  setoid : Setoid c ℓ
  setoid = record { Carrier = Carrier ; _≈_ = _≈_ ; isEquivalence = isEquivalence }

  open Setoid setoid public

open IsSetoid ⦃ … ⦄

open import Algebra.Structures
--open IsMonoid ⦃ … ⦄

record IsTermSubstitution {ℓᵗ} {ℓ⁼ᵗ} {ℓˢ} {ℓ⁼ˢ}
       (Term : Setoid ℓᵗ ℓ⁼ᵗ)
       (Substitution : Monoid ℓˢ ℓ⁼ˢ)
  : Set (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ) where

  open Setoid Term public using () renaming
    (Carrier to T
    ;_≈_ to _=ᵗ_)

  open Monoid Substitution public using () renaming
    (Carrier to S
    ;_≈_ to _=ˢ_
    ;_∙_ to _∙_
    ;ε to ∅)

  infixl 6 _▹_
  field
    _▹_ : T → S → T
    ▹-=ˢ-to-ᵗ : ∀ {s s′} → s =ˢ s′ → (t : T) → (t ▹ s) =ᵗ (t ▹ s′)
    ▹-=ᵗ-to-=ˢ : ∀ {s s′} → ((t : T) → t ▹ s =ᵗ t ▹ s′) → s =ˢ s′
    ▹-extracts-∙ : (t : T) (s₁ s₂ : S) → t ▹ s₁ ∙ s₂ =ᵗ t ▹ s₁ ▹ s₂

open IsTermSubstitution ⦃ … ⦄

record TermSubstitution ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
  field
    Term : Setoid ℓᵗ ℓ⁼ᵗ
    Substitution : Monoid ℓˢ ℓ⁼ˢ
    isTermSubstitution : IsTermSubstitution Term Substitution

  open IsTermSubstitution isTermSubstitution public

open import Relation.Unary
import Relation.Binary.Indexed as I

open import Relation.Nullary

record 𝓩ero (A : Set) : Set where
  field
    𝓩 : A

open 𝓩ero ⦃ … ⦄

instance 𝓩eroLevel : 𝓩ero Level
𝓩ero.𝓩 𝓩eroLevel = lzero

open import Agda.Builtin.Nat
instance 𝓩eroNat : 𝓩ero Nat
𝓩ero.𝓩 𝓩eroNat = zero

record IsSeparableInto {sx s x} (SX : Set sx) (S : Set s) (X : Set x) : Set (s ⊔ x ⊔ sx) where
  field
    break : SX → S × X
    combine : S → X → SX
    iso : ∀ sx → uncurry combine (break sx) ≡ sx

record Separableoid sx s x : Set (lsuc (sx ⊔ s ⊔ x)) where
  field
    SX : Set sx
    S : Set s
    X : Set x
    separable : IsSeparableInto SX S X

_AND_ = _×_

NOT_ = ¬_

_NAND_ : ∀ {a b} (A : Set a) (B : Set b) → Set ((a ⊔ b))
_NAND_ A B = (NOT A) × (NOT B)

_OR_ : ∀ {a b} (A : Set a) (B : Set b) → Set ((a ⊔ b))
_OR_ A B = NOT (A NAND B)

_XOR_ : ∀ {a b} (A : Set a) (B : Set b) → Set ((a ⊔ b))
_XOR_ A B = (A OR B) AND (NOT (A AND B))

asdf : (A B : Set) → Dec A → A XOR B → Prelude.Either A (¬ ¬ B)
asdf A B x (¬[¬A×¬B] , ¬[A×B]) with x
asdf A B x (¬[¬A×¬B] , ¬[A×B]) | yes p = _⊎_.left p
asdf A B x (¬[¬A×¬B] , ¬[A×B]) | no ¬p = _⊎_.right (λ {x₁ → ¬[¬A×¬B] (¬p , x₁)})

import Data.Empty
frf : Dec Data.Empty.⊥
frf = no (λ x → x)

{-
record LAW (A : Set) (B : Set) (E : EITHER A B) : Set where
  open import Data.Empty
  open EITHER E
  ¬A→B : ¬ A → ¬ ¬ B
  ¬A→B ¬a ¬b with e
  ... | ei = ei (λ {(a , ¬b) → ¬a a})
-}

record FiniteMembership : Set where

open import Data.List

module _ {ℓ} {A : Set ℓ} where

  listMembers : List A → Pred A ℓ
  listMembers [] x₁ = Prelude.⊥′
  listMembers (x ∷ xs) y = (y ≡ x) OR (listMembers xs y)

  _∈L_ : A → List A → Set ℓ
  x ∈L xs = x ∈ listMembers xs

  data _inL_ (y : A) : List A → Set where
    [] : ∀ {xs} → y inL (y ∷ xs)
    _∷_ : ∀ {x xs} → (ys : y inL xs) → y inL (x ∷ xs)

  ListMembers : List A → Pred A lzero
  ListMembers xs = _inL xs

  _∈LL_ : A → List A → Set
  x ∈LL xs = x ∈ ListMembers xs

  toLL : (y : A) (xs : List A) → y ∈L xs → y ∈LL xs
  toLL y [] x = Prelude.⊥′-elim x
  toLL y (x ∷ xs) y∈Lxxs = {!!} -- toLL y xs x₁

record Boolean (True : Set) (False : Set) : Set where
  field
    bool : True XOR False

{-
record L {ℓ} (A : Set ℓ) : Set ℓ where
  inductive
  field
    EMPTY : Set
    empty : L A
    head : A XOR ⊥
    tail : {!!}
-}
{-
    head : A XOR Prelude.⊥
    tail :
    empty : Prelude.⊥′
    list : EITHER Prelude.⊥′ (L A)
-}

record FreeVariableoid ℓᵛ∈ᵗ ℓᵛ∈ˢ⁺ ℓᵛ∈ˢ⁻ ℓᵛ ℓ⁼ᵛ ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ
       ⦃ termSubstitution : TermSubstitution ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ ⦄
  : Set (lsuc (ℓᵛ∈ᵗ ⊔ ℓᵛ∈ˢ⁺ ⊔ ℓᵛ∈ˢ⁻ ⊔ ℓᵛ ⊔ ℓ⁼ᵛ ⊔ ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
  -- open TermSubstitution termSubstitution
  field
    Variable : Setoid ℓᵛ ℓ⁼ᵛ
    TermStructure : Set

  open Setoid Variable public using () renaming
    (Carrier to V
    ;_≈_ to _=ᵛ_)

  field
    termVariables : T → Pred V ℓᵛ∈ᵗ
    termStructure : T → Set
    substitutionSourceVariables : S → Pred V ℓᵛ∈ˢ⁺
    substitutionTargetVariables : S → Pred V ℓᵛ∈ˢ⁻

  _ᵛ∈ᵗ_ : V → T → Set ℓᵛ∈ᵗ
  _ᵛ∈ᵗ_ v t = v ∈ termVariables t

  field
    termNumberOfVariables : (t : T) → ∃ λ (vs : List V) → (∀ v → (v ∈L vs → v ᵛ∈ᵗ t) × (v ᵛ∈ᵗ t → v ∈L vs))
    elementsDefineVariables : (t : T) → V

  _ᵛ∈ˢ⁺_ : V → S → Set ℓᵛ∈ˢ⁺
  _ᵛ∈ˢ⁺_ v s = v ∈ substitutionSourceVariables s

  _ᵛ∈ˢ⁻_ : V → S → Set ℓᵛ∈ˢ⁻
  _ᵛ∈ˢ⁻_ v s = v ∈ substitutionTargetVariables s

  field
    foo : ∀ {v t s} → v ᵛ∈ᵗ t → ¬ v ᵛ∈ˢ⁺ s → v ᵛ∈ᵗ (t ▹ s)
    isSep : IsSeparableInto T TermStructure V

record CorrectTermSubstitution ℓᵛ∈ᵗ ℓᵛ∈ˢ⁺ ℓᵛ∈ˢ⁻ ℓᵛ ℓ⁼ᵛ ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ
       ⦃ termSubstitution : TermSubstitution ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ ⦄
  : Set (lsuc (ℓᵛ∈ᵗ ⊔ ℓᵛ∈ˢ⁺ ⊔ ℓᵛ∈ˢ⁻ ⊔ ℓᵛ ⊔ ℓ⁼ᵛ ⊔ ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
  -- open TermSubstitution termSubstitution
  field
    Variable : Setoid ℓᵛ ℓ⁼ᵛ

  open Setoid Variable public using () renaming
    (Carrier to V
    ;_≈_ to _=ᵛ_)

  field
    termVariables : T → Pred V ℓᵛ∈ᵗ
    substitutionSourceVariables : S → Pred V ℓᵛ∈ˢ⁺
    substitutionTargetVariables : S → Pred V ℓᵛ∈ˢ⁻

  _ᵛ∈ᵗ_ : V → T → Set ℓᵛ∈ᵗ
  _ᵛ∈ᵗ_ v t = v ∈ termVariables t

  _ᵛ∈ˢ⁺_ : V → S → Set ℓᵛ∈ˢ⁺
  _ᵛ∈ˢ⁺_ v s = v ∈ substitutionSourceVariables s

  _ᵛ∈ˢ⁻_ : V → S → Set ℓᵛ∈ˢ⁻
  _ᵛ∈ˢ⁻_ v s = v ∈ substitutionTargetVariables s

  field
    foo : ∀ {v t s} → v ᵛ∈ᵗ t → ¬ v ᵛ∈ˢ⁺ s → v ᵛ∈ᵗ (t ▹ s)

  data D : Set where

data IsRight {a b} {A : Set a} {B : Set b} (e : _⊎_ A B) : Set (a ⊔ b) where
  right : B → IsRight e

module MostGeneralMGU where

  record Unificationoid {ℓᵗ} {ℓ⁼ᵗ} {ℓˢ} {ℓ⁼ˢ}
         ⦃ termSubstitution : TermSubstitution ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ ⦄
    : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
    -- open TermSubstitution termSubstitution
    Property : ∀ {ℓ} → Set (ℓˢ ⊔ lsuc ℓ)
    Property {ℓ} = S → Set ℓ

    Nothing : ∀ {ℓ} → (P : Property {ℓ}) → Set (ℓ ⊔ ℓˢ)
    Nothing P = ∀ s → P s → ⊥

    IsUnifier : (t₁ t₂ : T) → Property
    IsUnifier t₁ t₂ s = t₁ ▹ s =ᵗ t₂ ▹ s

    field
      unify : (t₁ t₂ : T) → Nothing (IsUnifier t₁ t₂) ⊎ ∃ (IsUnifier t₁ t₂)

    unifier : (t₁ t₂ : T) → Maybe S
    unifier t₁ t₂ with unify t₁ t₂
    unifier t₁ t₂ | _⊎_.left x = nothing
    unifier t₁ t₂ | _⊎_.right (x , _) = just x

    unifier-is-correct : (t₁ t₂ : T) → Nothing (IsUnifier t₁ t₂) → unifier t₁ t₂ ≡ nothing
    unifier-is-correct = {!!}

  record IsMostGeneralUnification ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ
         ⦃ termSubstitution : TermSubstitution ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ ⦄
         (unificationoid : Unificationoid ⦃ termSubstitution ⦄)
    : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
    --open TermSubstitution termSubstitution
    open Unificationoid unificationoid

    _≤_ : (s₋ : S) (s₊ : S) → Set (ℓˢ ⊔ ℓ⁼ˢ)
    _≤_ s₋ s₊ = ∃ λ s → s ∙ s₊ =ˢ s₋

    MostGenerally : ∀ {ℓ} (P : Property {ℓ}) → Property
    MostGenerally P s₊ = ∀ s₋ → P s₋ → s₋ ≤ s₊

    field
      isMguIfUnifier : (t₁ t₂ : T) → (ru : IsRight (unify t₁ t₂)) →
        Prelude.case ru of λ {((right (u , _))) → MostGenerally (IsUnifier t₁ t₂) u}
      --mgu : (t₁ t₂ : T) → Nothing (IsUnifier t₁ t₂) ⊎ ∃ (MostGenerally $ IsUnifier t₁ t₂)

    mgu : (t₁ t₂ : T) → Maybe S
    mgu = unifier

  record MostGeneralUnificationoid ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ
         ⦃ termSubstitution : TermSubstitution ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ ⦄
    : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
    -- open TermSubstitution termSubstitution
    Property : ∀ {ℓ} → Set (ℓˢ ⊔ lsuc ℓ)
    Property {ℓ} = S → Set ℓ

    Nothing : ∀ {ℓ} → (P : Property {ℓ}) → Set (ℓ ⊔ ℓˢ)
    Nothing P = ∀ s → P s → ⊥

    IsUnifier : (t₁ t₂ : T) → Property
    IsUnifier t₁ t₂ s = t₁ ▹ s =ᵗ t₂ ▹ s

    _≤_ : (s₋ : S) (s₊ : S) → Set (ℓˢ ⊔ ℓ⁼ˢ)
    _≤_ s₋ s₊ = ∃ λ s → s ∙ s₊ =ˢ s₋

    MostGenerally : ∀ {ℓ} (P : Property {ℓ}) → Property
    MostGenerally P s₊ = P s₊ × ∀ s₋ → P s₋ → s₋ ≤ s₊

    field
      mgu : (t₁ t₂ : T) → Nothing (IsUnifier t₁ t₂) ⊎ ∃ (MostGenerally $ IsUnifier t₁ t₂)

--   record PairUnification ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ
--          ⦃ termSubstitution : TermSubstitution ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ ⦄
--     : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
--     --open TermSubstitution termSubstitution
--     Property : ∀ {ℓ} → Set (ℓˢ ⊔ lsuc ℓ)
--     Property {ℓ} = S × S → Set ℓ

--     Nothing : ∀ {ℓ} → (P : Property {ℓ}) → Set (ℓ ⊔ ℓˢ)
--     Nothing P = ∀ u → P u → ⊥

--     IsUnifier : (t₁ t₂ : T) → Property
--     IsUnifier t₁ t₂ u = let (s₁ , s₂) = u in t₁ ▹ s₁ =ᵗ t₂ ▹ s₂

--     infix 4 _≤_
--     _≤_ : (s₋ : S × S) (s₊ : S × S) → Set (ℓˢ ⊔ ℓ⁼ˢ)
--     _≤_ u₋ u₊ =
--       let s₋₁ , s₋₂ = u₋
--           s₊₁ , s₊₂ = u₊ in
--       ∃ λ s → s ∙ s₊₁ =ˢ s₋₁ × s ∙ s₊₂ =ˢ s₋₂

--     MostGenerally : ∀ {ℓ} (P : Property {ℓ}) → Property
--     MostGenerally P u₊ = P u₊ × ∀ u₋ → P u₋ → u₋ ≤ u₊

-- {-
--   mgu f(x,y) f(y,x)

--   x → w , y → z || x → z , y → w

--   mgu f(x,y) f(g(y),x)

--   x → g(z) || y → z , x → y

--   mgu f(x,y) f(y,z)

--   x → y , y → z || ∅              ≥₂
--   x → w , y → z || y → w          ≥₂
--   x → w , y → v || y → w , z → v  ≥₂
--   y → v || y → x , z → v  ≥₂
--   ∅ || y → x , z → y

--   x → w , y → v , z → v || y → w , z → v
--   x → y , y → f(z) || z → f(z)

--   f(x  , g(x,y)     ,w)
--   x → g(z)
--   w →? v

--   f(g(z), g(g(z),y) ,v)
--   v →? w

--   possible unifers:
--   x → g(z)    , w → v      ||
--   x → g(h(a)) , w → v      || z → h(a)
--   x → g(z)                 || z → h(y) , v → w

-- -}

--     field
--       mgu : (t₁ t₂ : T)
--             → Nothing (IsUnifier t₁ t₂) ⊎ ∃ (MostGenerally (IsUnifier t₁ t₂))

-- -- record Something ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
-- --   field
-- --     Terminus : Setoid ℓᵗ ℓ⁼ᵗ
-- --     Simplex : Monoid ℓˢ ℓ⁼ˢ

-- --   open Setoid Terminus public using () renaming
-- --     (Carrier to T
-- --     ;_≈_ to _=T=_)

-- --   open Monoid Simplex public using () renaming
-- --     (Carrier to S
-- --     ;_≈_ to _=S=_
-- --     ;_∙_ to _∙_
-- --     ;ε to ∅)

-- --   infixl 6 _▹_
-- --   field
-- --     _▹_ : T → S → T
-- --     -- equivalence of S implies substitutivity in (T,▹)
-- --     ▹-=S=-to-=T= : ∀ {s s′} → s =S= s′ → (t : T) → t ▹ s =T= t ▹ s′
-- --     -- applications of simplexi are equivalent across all termini only when the simplexi are equivalent
-- --     -- that is, equivalence of S is as compact is it can be while still respecting equivalence in (T,▹)
-- --     ▹-=T=-to-=S= : ∀ {s s′} → ((t : T) → t ▹ s =T= t ▹ s′) → s =S= s′
-- --     -- S extracts to ▹ in (T,∙)
-- --     ▹-∙-compositional : (t : T) (s₁ s₂ : S) → t ▹ s₁ ∙ s₂ =T= t ▹ s₁ ▹ s₂

-- -- -- module NotIndexed where

-- -- --   record MGU ℓᵗ ℓ⁼ᵗ ℓˢ ℓ⁼ˢ : Set (lsuc (ℓᵗ ⊔ ℓ⁼ᵗ ⊔ ℓˢ ⊔ ℓ⁼ˢ)) where
-- -- --     infixr 8 _◃_
-- -- --     --infixr 9 _◇_
-- -- --     field
-- -- --       𝓣erm : Setoid ℓᵗ ℓ⁼ᵗ

-- -- --     open Setoid 𝓣erm public using () renaming (Carrier to 𝓣; _≈_ to _=ᵗ_)

-- -- --     field
-- -- --       𝓢ubstition : Semigroup ℓˢ ℓ⁼ˢ -- TODO Monoid?

-- -- --     open Semigroup 𝓢ubstition public using () renaming
-- -- --       (Carrier to 𝓢
-- -- --       ;_≈_ to _=ˢ_
-- -- --       ; _∙_ to _◇_)

-- -- --     --field
-- -- --     --  𝓼ubstitute : RawPApplicative (λ x x₁ → {!!})

-- -- --     _◃'_ : 𝓢 → 𝓣 → 𝓣
-- -- --     _◃'_ = {!!}

-- -- --     field
-- -- --       _◃_ : 𝓢 → 𝓣 → 𝓣
-- -- --       ◃-=ˢ-to-=ᵗ : ∀ {𝒮 𝒮′} → 𝒮 =ˢ 𝒮′ → (𝒯 : 𝓣) → 𝒮 ◃ 𝒯 =ᵗ 𝒮′ ◃ 𝒯
-- -- --       ◃-=ᵗ-to-=ˢ : ∀ {𝒮 𝒮′} → ((𝒯 : 𝓣) → 𝒮 ◃ 𝒯 =ᵗ 𝒮′ ◃ 𝒯) → 𝒮 =ˢ 𝒮′

-- -- --     field

-- -- --       --_◇_ : 𝓢 → 𝓢 → 𝓢
-- -- --       ◇-compositional : (𝒯 : 𝓣) (𝒮₁ 𝒮₂ : 𝓢) → (𝒮₂ ◇ 𝒮₁) ◃ 𝒯 =ᵗ 𝒮₂ ◃ 𝒮₁ ◃ 𝒯

-- -- --     ◇-associative : (𝒮₁ 𝒮₂ 𝒮₃ : 𝓢) → 𝒮₃ ◇ (𝒮₂ ◇ 𝒮₁) =ˢ (𝒮₃ ◇ 𝒮₂) ◇ 𝒮₁
-- -- --     ◇-associative 𝒮₁ 𝒮₂ 𝒮₃ = {!!}

-- -- --     Property : ∀ {ℓ} → Set (ℓˢ ⊔ lsuc ℓ)
-- -- --     Property {ℓ} = 𝓢 → Set ℓ

-- -- --     Nothing : ∀ {ℓ} → (P : Property {ℓ}) → Set (ℓ ⊔ ℓˢ)
-- -- --     Nothing P = ∀ 𝒮 → P 𝒮 → ⊥

-- -- --     Unifies : (𝒯₁ 𝒯₂ : 𝓣) → Property
-- -- --     Unifies 𝒯₁ 𝒯₂ 𝒮 = 𝒮 ◃ 𝒯₁ ≡ 𝒮 ◃ 𝒯₂

-- -- --     _≤_ : (σ₋ : 𝓢) (σ₊ : 𝓢) → Set (ℓˢ ⊔ ℓ⁼ˢ)
-- -- --     _≤_ σ₋ σ₊ = ∃ λ σ → σ ◇ σ₊ =ˢ σ₋

-- -- --     Max : ∀ {ℓ} (P : Property {ℓ}) → Property
-- -- --     Max P σ₊ = P σ₊ × ∀ σ₋ → P σ₋ → σ₋ ≤ σ₊

-- -- --     field
-- -- --       mgu : (𝒯₁ 𝒯₂ : 𝓣) → Nothing (Unifies 𝒯₁ 𝒯₂) ⊎ ∃ λ (σ : 𝓢) → Max (Unifies 𝒯₁ 𝒯₂) σ

-- -- -- -- module Indexed where

-- -- -- --   record MGU ℓⁱ ℓᵛ ℓᵗ ℓˢ : Set (lsuc (ℓⁱ ⊔ ℓᵛ ⊔ ℓᵗ ⊔ ℓˢ)) where
-- -- -- --     field
-- -- -- --       𝓲 : Set ℓⁱ
-- -- -- --       𝓥 : 𝓲 → Set ℓᵛ
-- -- -- --       𝓣 : 𝓲 → Set ℓᵗ

-- -- -- --     _↦_ : (s t : 𝓲) → Set (ℓᵛ ⊔ ℓᵗ)
-- -- -- --     _↦_ s t = 𝓥 s → 𝓣 t

-- -- -- --     infix 14 _≐_
-- -- -- --     _≐_ : {s t : 𝓲} → s ↦ t → s ↦ t → Set (ℓᵛ ⊔ ℓᵗ)
-- -- -- --     _≐_ σ σ′ = ∀ x → σ x ≡ σ′ x

-- -- -- --     field
-- -- -- --       _◃_ : ∀ {s t} → s ↦ t → 𝓣 s → 𝓣 t
-- -- -- --       ≐-◃-identity : {!!}

-- -- -- --     _◇_ : ∀ {r s t : 𝓲} → (σ₂ : s ↦ t) (σ₁ : r ↦ s) → r ↦ t
-- -- -- --     _◇_ σ₂ σ₁ = (σ₂ ◃_) ∘ σ₁

-- -- -- --     field
-- -- -- --       𝓢 : 𝓲 → 𝓲 → Set ℓˢ
-- -- -- --       sub : ∀ {s t} → 𝓢 s t → s ↦ t

-- -- -- -- --     Property : ∀ {ℓ} → 𝓲 → Set (lsuc ℓ ⊔ ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)
-- -- -- -- --     Property {ℓ} s = ∀ {t} → s ↦ t → Set ℓ

-- -- -- -- --     Nothing : ∀ {ℓ m} → (P : Property {ℓ} m) → Set (ℓ ⊔ ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)
-- -- -- -- --     Nothing P = ∀ {n} f → P {n} f → ⊥

-- -- -- -- --     Unifies : ∀ {i} (t₁ t₂ : 𝓣 i) → Property i
-- -- -- -- --     Unifies t₁ t₂ f = f ◃ t₁ ≡ f ◃ t₂

-- -- -- -- --     _≤_ : ∀ {m n n'} (f : m ↦ n) (g : m ↦ n') → Set (ℓⱽ ⊔ ℓᵀ)
-- -- -- -- --     _≤_ f g = ∃ λ f' → f ≐ (f' ◇ g)

-- -- -- -- --     Max : ∀ {ℓ m} (P : Property {ℓ} m) → Property m
-- -- -- -- --     Max P = (λ f → P f × (∀ {n} f' → P {n} f' → f' ≤ f))

-- -- -- -- --     field
-- -- -- -- --       mgu : ∀ {m} (t₁ t₂ : 𝓣 m) →
-- -- -- -- --             Nothing (Unifies t₁ t₂) ⊎ (∃ λ n → ∃ λ (σ : 𝓢 m n) → (Max (Unifies t₁ t₂)) (sub σ))

-- -- -- -- -- -- -- -- open import Prelude.Function
-- -- -- -- -- -- -- -- open import Relation.Binary.HeterogeneousEquality.Core as H using (_≅_ ; ≅-to-≡)
-- -- -- -- -- -- -- -- open import Prelude.Equality

-- -- -- -- -- -- -- -- record MGU-addIndex-to-noIndex* {ℓⁱ ℓⱽ ℓᵀ ℓˢ}
-- -- -- -- -- -- -- --                             (m : MGU-addIndex ℓⁱ ℓⱽ ℓᵀ ℓˢ) : Set (lsuc (ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)) where
-- -- -- -- -- -- -- --   open MGU-addIndex m
-- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- --     𝓥ᵢ : Set (ℓⁱ ⊔ ℓⱽ)
-- -- -- -- -- -- -- --     𝓣ᵢ : Set (ℓⁱ ⊔ ℓᵀ)
-- -- -- -- -- -- -- --     𝓼ᵢ : Set (ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- --     to∃𝓥 : 𝓥ᵢ → ∃ 𝓥
-- -- -- -- -- -- -- --     to∃𝓣 : 𝓣ᵢ → ∃ 𝓣
-- -- -- -- -- -- -- --     to𝓥ᵢ : ∃ 𝓥 → 𝓥ᵢ
-- -- -- -- -- -- -- --     to𝓣ᵢ : ∃ 𝓣 → 𝓣ᵢ
-- -- -- -- -- -- -- --     iso∃𝓥 : (∃𝒱 : ∃ 𝓥) → to∃𝓥 (to𝓥ᵢ ∃𝒱) ≡ ∃𝒱
-- -- -- -- -- -- -- --     iso𝓥ᵢ : (𝒱ᵢ : 𝓥ᵢ) → to𝓥ᵢ (to∃𝓥 𝒱ᵢ) ≡ 𝒱ᵢ
-- -- -- -- -- -- -- --     iso∃𝓣 : (∃𝒯 : ∃ 𝓣) → to∃𝓣 (to𝓣ᵢ ∃𝒯) ≡ ∃𝒯
-- -- -- -- -- -- -- --     iso𝓣ᵢ : (𝒯ᵢ : 𝓣ᵢ) → to𝓣ᵢ (to∃𝓣 𝒯ᵢ) ≡ 𝒯ᵢ
-- -- -- -- -- -- -- --     inj𝓥 : ∀ {a b} → 𝓥 a ≡ 𝓥 b → a ≡ b
-- -- -- -- -- -- -- --     inj𝓣 : ∀ {a b} → 𝓣 a ≡ 𝓣 b → a ≡ b
-- -- -- -- -- -- -- --     mag : (𝓥ᵢ → 𝓣ᵢ) → ∀ {s} t → 𝓥 s → 𝓣 t
-- -- -- -- -- -- -- --     to∃𝓣𝓣 : 𝓣ᵢ → 𝓣ᵢ → ∃ λ i → 𝓣 i × 𝓣 i
-- -- -- -- -- -- -- --     max𝓣ᵢ : ∀ {m} n → (tm : 𝓣 m) → (((𝓣 n → 𝓣 m) × (𝓥 n → 𝓥 m)) ⊎ 𝓣 n)
-- -- -- -- -- -- -- --     max𝓲 : ∀ m n → ((𝓣 n → 𝓣 m) × (𝓥 n → 𝓥 m)) ⊎ ((𝓣 m → 𝓣 n) × (𝓥 m → 𝓥 n))
-- -- -- -- -- -- -- --     apply𝓼 : 𝓣ᵢ → (𝓥ᵢ → 𝓣ᵢ) → ∃ λ s → ∃ λ t → (𝓥 s → 𝓣 t) × 𝓣 s
-- -- -- -- -- -- -- --     to𝓼 : 𝓼ᵢ → ∃ λ s → ∃ λ t → 𝓥 s → 𝓣 t
-- -- -- -- -- -- -- --     to𝓼' : 𝓼ᵢ → 𝓣ᵢ → ∃ λ s → ∃ λ t → (𝓥 s → 𝓣 t) × 𝓣 s
-- -- -- -- -- -- -- --     to◇ : 𝓼ᵢ → 𝓼ᵢ → ∃ λ r → ∃ λ s → ∃ λ t → (𝓥 s → 𝓣 t) × (𝓥 r → 𝓣 s)
-- -- -- -- -- -- -- --     to= : 𝓼ᵢ → 𝓼ᵢ → ∃ λ s → ∃ λ t → (𝓥 s → 𝓣 t) × (𝓥 s → 𝓣 t)
-- -- -- -- -- -- -- --     to𝓼ᵢ : ∀ {r t} → (𝓥 r → 𝓣 t) → 𝓼ᵢ
-- -- -- -- -- -- -- --     {{ eqi }} : Eq 𝓲

-- -- -- -- -- -- -- --   to-noIndex : MGU-noIndex* (ℓⁱ ⊔ ℓⱽ) (ℓⁱ ⊔ ℓᵀ) (ℓⁱ ⊔ ℓˢ)
-- -- -- -- -- -- -- --   to-noIndex = go where
-- -- -- -- -- -- -- --     go : MGU-noIndex* _ _ _
-- -- -- -- -- -- -- --     MGU-noIndex*.𝓥 go = 𝓥ᵢ
-- -- -- -- -- -- -- --     MGU-noIndex*.𝓣 go = 𝓣ᵢ
-- -- -- -- -- -- -- --     MGU-noIndex*.𝓼 go = 𝓼ᵢ -- ∃ λ s → ∃ λ t → s ↦ t
-- -- -- -- -- -- -- --     MGU-noIndex*._≐_ go s1 s2 with to= s1 s2
-- -- -- -- -- -- -- --     ... | (s , t , vstt1 , vstt2) = {!_≐_ vstt1 vstt2!}
-- -- -- -- -- -- -- --     MGU-noIndex*._◃_ go f x with to𝓼' f x
-- -- -- -- -- -- -- --     MGU-noIndex*._◃_ go _ _ | (s , t , f , term) = to𝓣ᵢ $ _ , f ◃ term
-- -- -- -- -- -- -- --     MGU-noIndex*._◇_ go s1 s2 with to◇ s1 s2
-- -- -- -- -- -- -- --     ... | (r , s , t , vstt , vrts) = to𝓼ᵢ $ vstt ◇ vrts
-- -- -- -- -- -- -- --     MGU-noIndex*.mgu go = {!!}
-- -- -- -- -- -- -- -- --     MGU-noIndex*.𝓥 go = {!𝓥ᵢ!}
-- -- -- -- -- -- -- -- --     MGU-noIndex*.𝓣 go = 𝓣ᵢ
-- -- -- -- -- -- -- -- --     MGU-noIndex*.𝓼 go = {!!} -- ∃ λ s → ∃ λ t → s ↦ t -- ∃ λ s → ∃ λ t → 𝓥 s → 𝓣 t
-- -- -- -- -- -- -- -- --     MGU-noIndex*._≐_ go (s₁ , t₁ , f₁) (s₂ , t₂ , f₂) = {!!} -- ∃ λ (s-refl : s₁ ≡ s₂) → ∃ λ (t-refl : t₁ ≡ t₂) → (∀ x → f₁ x ≡ (Prelude.transport (λ i → 𝓥 s₂ → 𝓣 i) (sym t-refl) f₂) (Prelude.transport _ s-refl x))
-- -- -- -- -- -- -- -- --     {-
-- -- -- -- -- -- -- -- --     MGU-noIndex*._◃_ go (s , t , f) 𝒯 = {!_◃_ f!}
-- -- -- -- -- -- -- -- --     ∀ s t → 𝓣ᵢ → (𝓣 s → 𝓣 t) → 𝓣 s
-- -- -- -- -- -- -- -- --     ∀ s t → 𝓣ᵢ → (𝓣 s → 𝓣 t) → 𝓣ᵢ
-- -- -- -- -- -- -- -- --     𝓣 s
-- -- -- -- -- -- -- -- --     -}

-- -- -- -- -- -- -- -- --     MGU-noIndex*._◃_ go (s , t , f) 𝒯 with to∃𝓣 𝒯
-- -- -- -- -- -- -- -- --     MGU-noIndex*._◃_ go (s , t , f) 𝒯 | (s2 , ttt) with s == s2
-- -- -- -- -- -- -- -- --     (go MGU-noIndex*.◃ (.s , t , f)) 𝒯 | s , 𝒯s | (Prelude.yes refl) = to𝓣ᵢ (_ , _◃_ {s} {t} f 𝒯s)
-- -- -- -- -- -- -- -- --     (go MGU-noIndex*.◃ (s , t , f)) 𝒯 | s2 , ttt | (Prelude.no x) = 𝒯

-- -- -- -- -- -- -- -- --     MGU-noIndex*._◇_ go (s , t , f) (p , r , g) with max𝓲 r s
-- -- -- -- -- -- -- -- --     MGU-noIndex*._◇_ go (s , t , f) (p , r , g) | _⊎_.left (T , V) = {!!}
-- -- -- -- -- -- -- -- --     MGU-noIndex*._◇_ go (s , t , f) (p , r , g) | _⊎_.right (T , V) = _ , _ , f ◇ (T ∘ g) -- f ◃_ ∘ (T ∘ g)
-- -- -- -- -- -- -- -- --     {-
-- -- -- -- -- -- -- -- --     = _ , _ , f ◃_ ∘ (λ x → {!max𝓣ᵢ s₁ (g x)!}) -- _ , _ , f ◃_ ∘ (λ x → {!g x!})
-- -- -- -- -- -- -- -- --     -}

-- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- --     MGU-noIndex*._◇_ go (s₁ , t₁ , f) (s₂ , t₂ , g) with t₂ == s₁
-- -- -- -- -- -- -- -- --     MGU-noIndex*._◇_ go (s₁ , t₁ , f) (s₂ , t₂ , g) | (Prelude.yes refl) = s₂ , t₁ , f ◃_ ∘ g
-- -- -- -- -- -- -- -- --     MGU-noIndex*._◇_ go (s₁ , t₁ , f) (s₂ , t₂ , g) | (Prelude.no x) = s₂ , t₂ , g
-- -- -- -- -- -- -- -- -- -}
-- -- -- -- -- -- -- -- --     -- = s₂ , t₁ , {!(f ◃_)!}
-- -- -- -- -- -- -- -- --     MGU-noIndex*.mgu go t₁ t₂ with to∃𝓣𝓣 t₁ t₂
-- -- -- -- -- -- -- -- --     … | i , tt₁ , tt₂ with mgu tt₁ tt₂
-- -- -- -- -- -- -- -- --     MGU-noIndex*.mgu go t₁ t₂ | i , tt₁ , tt₂ | (_⊎_.left x) = {!!}
-- -- -- -- -- -- -- -- --     MGU-noIndex*.mgu go t₁ t₂ | i , tt₁ , tt₂ | (_⊎_.right (i₂ , σ , subσ-refl , ff)) with to∃𝓣 t₁ | to∃𝓣 t₂
-- -- -- -- -- -- -- -- --     MGU-noIndex*.mgu go t₁ t₂ | i , tt₁ , tt₂ | (_⊎_.right (i₂ , σ , subσ-refl , ff)) | (fst₁ , snd₁) | (fst₂ , snd₂) = _⊎_.right ((_ , _ , sub σ) , {!!} , {!!}) -- _⊎_.right ((i , i₂ , sub σ) , {!subσ-refl!} , {!!})

-- -- -- -- -- -- -- -- -- record MGU-noIndex-to-addIndex {ℓⁱ ℓⱽ ℓᵀ ℓˢ}
-- -- -- -- -- -- -- -- --                             (m : MGU-noIndex ℓⱽ ℓᵀ ℓˢ) : Set (lsuc (ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)) where
-- -- -- -- -- -- -- -- --   open MGU-noIndex m
-- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- --     𝓲 : Set ℓⁱ
-- -- -- -- -- -- -- -- --     𝓥ᵢ : 𝓲 → Set ℓⱽ
-- -- -- -- -- -- -- -- --     𝓣ᵢ : 𝓲 → Set ℓᵀ
-- -- -- -- -- -- -- -- --     to𝓥 : ∃ 𝓥ᵢ → 𝓥
-- -- -- -- -- -- -- -- --     to𝓣 : ∃ 𝓣ᵢ → 𝓣
-- -- -- -- -- -- -- -- --     to∃𝓥ᵢ : 𝓥 → ∃ 𝓥ᵢ
-- -- -- -- -- -- -- -- --     to∃𝓣ᵢ : 𝓣 → ∃ 𝓣ᵢ
-- -- -- -- -- -- -- -- --     inj𝓥 : ∀ {a b} → 𝓥ᵢ a ≡ 𝓥ᵢ b → a ≡ b
-- -- -- -- -- -- -- -- --     inj𝓣 : ∀ {a b} → 𝓣ᵢ a ≡ 𝓣ᵢ b → a ≡ b
-- -- -- -- -- -- -- -- --     mag : ∀ {s t} → (𝓥ᵢ s → 𝓣ᵢ t) → 𝓥 → 𝓣
-- -- -- -- -- -- -- -- --     {-
-- -- -- -- -- -- -- -- --     iso∃𝓥 : (∃𝒱 : ∃ 𝓥) → to∃𝓥 (to𝓥ᵢ ∃𝒱) ≡ ∃𝒱
-- -- -- -- -- -- -- -- --     iso𝓥ᵢ : (𝒱ᵢ : 𝓥ᵢ) → to𝓥ᵢ (to∃𝓥 𝒱ᵢ) ≡ 𝒱ᵢ
-- -- -- -- -- -- -- -- --     iso∃𝓣 : (∃𝒯 : ∃ 𝓣) → to∃𝓣 (to𝓣ᵢ ∃𝒯) ≡ ∃𝒯
-- -- -- -- -- -- -- -- --     iso𝓣ᵢ : (𝒯ᵢ : 𝓣ᵢ) → to𝓣ᵢ (to∃𝓣 𝒯ᵢ) ≡ 𝒯ᵢ
-- -- -- -- -- -- -- -- --     mag : (𝓥ᵢ → 𝓣ᵢ) → ∀ {s} t → 𝓥 s → 𝓣 t
-- -- -- -- -- -- -- -- --     -}

-- -- -- -- -- -- -- -- --   to-addIndex : MGU-addIndex ℓⁱ ℓⱽ ℓᵀ ℓˢ
-- -- -- -- -- -- -- -- --   to-addIndex = go where
-- -- -- -- -- -- -- -- --     go : MGU-addIndex ℓⁱ ℓⱽ ℓᵀ ℓˢ
-- -- -- -- -- -- -- -- --     MGU-addIndex.𝓲 go = 𝓲
-- -- -- -- -- -- -- -- --     MGU-addIndex.𝓥 go = 𝓥ᵢ
-- -- -- -- -- -- -- -- --     MGU-addIndex.𝓣 go = 𝓣ᵢ
-- -- -- -- -- -- -- -- --     MGU-addIndex._◃_ go {s} {t} f x = Prelude.transport 𝓣ᵢ {!!} $ snd ∘ to∃𝓣ᵢ $ _◃_ (λ v → to𝓣 (t , f (Prelude.transport 𝓥ᵢ (inj𝓥 {_} {_} {!!}) (snd $ to∃𝓥ᵢ v)))) (to𝓣 (s , x)) -- let Ti , Tit = to∃𝓣ᵢ $ _◃_ (λ v → to𝓣 (t , f {!!})) (to𝓣 (s , x)) in {!!}
-- -- -- -- -- -- -- -- --     MGU-addIndex.𝓢 go = {!!}
-- -- -- -- -- -- -- -- --     MGU-addIndex.sub go = {!!}
-- -- -- -- -- -- -- -- --     MGU-addIndex.mgu go = {!!}

-- -- -- -- -- -- -- -- -- record MGU-addIndex-to-noIndex {ℓⁱ ℓⱽ ℓᵀ ℓˢ}
-- -- -- -- -- -- -- -- --                             (m : MGU-addIndex ℓⁱ ℓⱽ ℓᵀ ℓˢ) : Set (lsuc (ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)) where
-- -- -- -- -- -- -- -- --   open MGU-addIndex m
-- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- --     𝓥ᵢ : Set (ℓⁱ ⊔ ℓⱽ)
-- -- -- -- -- -- -- -- --     𝓣ᵢ : Set (ℓⁱ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- --     to∃𝓥 : 𝓥ᵢ → ∃ 𝓥
-- -- -- -- -- -- -- -- --     to∃𝓣 : 𝓣ᵢ → ∃ 𝓣
-- -- -- -- -- -- -- -- --     to𝓥ᵢ : ∃ 𝓥 → 𝓥ᵢ
-- -- -- -- -- -- -- -- --     to𝓣ᵢ : ∃ 𝓣 → 𝓣ᵢ
-- -- -- -- -- -- -- -- --     iso∃𝓥 : (∃𝒱 : ∃ 𝓥) → to∃𝓥 (to𝓥ᵢ ∃𝒱) ≡ ∃𝒱
-- -- -- -- -- -- -- -- --     iso𝓥ᵢ : (𝒱ᵢ : 𝓥ᵢ) → to𝓥ᵢ (to∃𝓥 𝒱ᵢ) ≡ 𝒱ᵢ
-- -- -- -- -- -- -- -- --     iso∃𝓣 : (∃𝒯 : ∃ 𝓣) → to∃𝓣 (to𝓣ᵢ ∃𝒯) ≡ ∃𝒯
-- -- -- -- -- -- -- -- --     iso𝓣ᵢ : (𝒯ᵢ : 𝓣ᵢ) → to𝓣ᵢ (to∃𝓣 𝒯ᵢ) ≡ 𝒯ᵢ
-- -- -- -- -- -- -- -- --     inj𝓥 : ∀ {a b} → 𝓥 a ≡ 𝓥 b → a ≡ b
-- -- -- -- -- -- -- -- --     inj𝓣 : ∀ {a b} → 𝓣 a ≡ 𝓣 b → a ≡ b
-- -- -- -- -- -- -- -- --     mag : (𝓥ᵢ → 𝓣ᵢ) → ∀ {s} t → 𝓥 s → 𝓣 t

-- -- -- -- -- -- -- -- --   to-noIndex : MGU-noIndex (ℓⁱ ⊔ ℓⱽ) (ℓⁱ ⊔ ℓᵀ) ℓˢ
-- -- -- -- -- -- -- -- --   to-noIndex = go where
-- -- -- -- -- -- -- -- --     go : MGU-noIndex _ _ _
-- -- -- -- -- -- -- -- --     MGU-noIndex.𝓥 go = 𝓥ᵢ
-- -- -- -- -- -- -- -- --     MGU-noIndex.𝓣 go = 𝓣ᵢ
-- -- -- -- -- -- -- -- --     MGU-noIndex._◃_ go 𝓈 𝒯ᵢ with to∃𝓣 𝒯ᵢ | Prelude.graphAt to∃𝓣 𝒯ᵢ | (Prelude.curry $ snd ∘ to∃𝓣 ∘ 𝓈 ∘ to𝓥ᵢ) (fst $ to∃𝓣 𝒯ᵢ) | Prelude.graphAt (Prelude.curry $ snd ∘ to∃𝓣 ∘ 𝓈 ∘ to𝓥ᵢ) (fst $ to∃𝓣 𝒯ᵢ)
-- -- -- -- -- -- -- -- --     … | s , 𝒯s | Prelude.ingraph eq | 𝓈' | Prelude.ingraph refl with cong fst eq
-- -- -- -- -- -- -- -- --     (go MGU-noIndex.◃ 𝓈) 𝒯ᵢ | .(fst (to∃𝓣 𝒯ᵢ)) , 𝒯s | (Prelude.ingraph eq) | _ | (Prelude.ingraph refl) | refl with cong fst eq
-- -- -- -- -- -- -- -- --     (go MGU-noIndex.◃ 𝓈) 𝒯ᵢ | .(fst (to∃𝓣 _ 𝒯ᵢ)) , 𝒯s | (Prelude.ingraph eq) | 𝓈' | (Prelude.ingraph refl) | refl | refl rewrite Prelude.sym eq with _◃_ {_} {{!!}} (λ v → 𝓈' (Prelude.transport 𝓥 (cong fst (sym eq)) {!!})) (snd ∘ to∃𝓣 $ 𝒯ᵢ)
-- -- -- -- -- -- -- -- --     … | dfsf = to𝓣ᵢ (_ , dfsf)
-- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- --     … | s , 𝒯s | Prelude.ingraph eq | 𝓈' | Prelude.ingraph refl with _◃_ {fst (to∃𝓣 𝒯ᵢ)} {s} (λ v → Prelude.transport 𝓣 {!!} (𝓈' (Prelude.transport 𝓥 (cong fst eq) v))) (snd ∘ to∃𝓣 $ 𝒯ᵢ)
-- -- -- -- -- -- -- -- --     … | dd = to𝓣ᵢ (_ , dd)
-- -- -- -- -- -- -- -- -- -}
-- -- -- -- -- -- -- -- --     MGU-noIndex.𝓢 go = {!!}
-- -- -- -- -- -- -- -- --     MGU-noIndex.sub go = {!!}
-- -- -- -- -- -- -- -- --     MGU-noIndex.mgu go = {!!}

-- -- -- -- -- -- -- -- -- -- MGU-addIndex-to-noIndex : ∀ {ℓⁱ ℓⱽ ℓᵀ ℓˢ} →
-- -- -- -- -- -- -- -- -- --                             (m : MGU-addIndex ℓⁱ ℓⱽ ℓᵀ ℓˢ)
-- -- -- -- -- -- -- -- -- --                             (open MGU-addIndex m)
-- -- -- -- -- -- -- -- -- --                             (𝓥ᵢ : Set (ℓⁱ ⊔ ℓⱽ))
-- -- -- -- -- -- -- -- -- --                             (𝓣ᵢ : Set (ℓⁱ ⊔ ℓᵀ))
-- -- -- -- -- -- -- -- -- --                             (to∃𝓥 : 𝓥ᵢ → ∃ 𝓥)
-- -- -- -- -- -- -- -- -- --                             (to∃𝓣 : 𝓣ᵢ → ∃ 𝓣)
-- -- -- -- -- -- -- -- -- --                             (to𝓥ᵢ : ∃ 𝓥 → 𝓥ᵢ)
-- -- -- -- -- -- -- -- -- --                             (to𝓣ᵢ : ∃ 𝓣 → 𝓣ᵢ)
-- -- -- -- -- -- -- -- -- --                             (iso∃𝓥 : (∃𝒱 : ∃ 𝓥) → to∃𝓥 (to𝓥ᵢ ∃𝒱) ≡ ∃𝒱)
-- -- -- -- -- -- -- -- -- --                             (iso𝓥ᵢ : (𝒱ᵢ : 𝓥ᵢ) → to𝓥ᵢ (to∃𝓥 𝒱ᵢ) ≡ 𝒱ᵢ)
-- -- -- -- -- -- -- -- -- --                             (iso∃𝓣 : (∃𝒯 : ∃ 𝓣) → to∃𝓣 (to𝓣ᵢ ∃𝒯) ≡ ∃𝒯)
-- -- -- -- -- -- -- -- -- --                             (iso𝓣ᵢ : (𝒯ᵢ : 𝓣ᵢ) → to𝓣ᵢ (to∃𝓣 𝒯ᵢ) ≡ 𝒯ᵢ)
-- -- -- -- -- -- -- -- -- --                             → MGU-noIndex (ℓⁱ ⊔ ℓⱽ) (ℓⁱ ⊔ ℓᵀ) ℓˢ
-- -- -- -- -- -- -- -- -- -- MGU-addIndex-to-noIndex {ℓⁱ} {ℓⱽ} {ℓᵀ} {ℓˢ} m = go where
-- -- -- -- -- -- -- -- -- --   open MGU-addIndex m
-- -- -- -- -- -- -- -- -- --   go : MGU-noIndex _ _ _
-- -- -- -- -- -- -- -- -- --   go = {!!}

-- -- -- -- -- -- -- -- -- -- --  open import Relation.Binary.HeterogeneousEquality.Core as H using (_≅_ ; ≅-to-≡)
-- -- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- -- --   𝓼 = ∃ 𝓥 → ∃ 𝓣

-- -- -- -- -- -- -- -- -- --   _∶_↦_ : 𝓼 → 𝓲 → 𝓲 → Set (ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- --   _∶_↦_ 𝓈 s t = ((𝒱ₛ : 𝓥 s) → ∃ λ (𝒯ₜ : 𝓣 t) → 𝓈 (s , 𝒱ₛ) ≡ (t , 𝒯ₜ))
-- -- -- -- -- -- -- -- -- -- -}
-- -- -- -- -- -- -- -- -- -- --   go : MGU-noIndex _ _ _
-- -- -- -- -- -- -- -- -- -- --   MGU-noIndex.𝓥 go = ∃ 𝓥
-- -- -- -- -- -- -- -- -- -- --   MGU-noIndex.𝓣 go = ∃ 𝓣
-- -- -- -- -- -- -- -- -- -- --   MGU-noIndex._≐_ go f g = (𝒾 : 𝓲) (𝒱 : 𝓥 𝒾) → f (𝒾 , 𝒱) ≡ g (𝒾 , 𝒱)
-- -- -- -- -- -- -- -- -- -- --   MGU-noIndex._◃_ go 𝓈 (𝒾 , 𝒯) = 𝒾 , _◃_ {𝒾} {𝒾} (λ v → (Prelude.transport _ (≅-to-≡ $ snd (mag (fst (𝓈 (𝒾 , v))) (( (𝒾 ))) (snd (𝓈 (𝒾 , v))))) $
-- -- -- -- -- -- -- -- -- -- --                                                            snd (𝓈 (𝒾 , v)))
-- -- -- -- -- -- -- -- -- -- --                                                           {!!}) {!!}
-- -- -- -- -- -- -- -- -- -- --   -- (snd ∘ (λ (𝒱 : 𝓥 𝒾) → 𝓈 (𝒾 , 𝒱)))
-- -- -- -- -- -- -- -- -- -- --   -- fst (𝓈 (s , {!!})) , _◃_ {s} {fst (𝓈 (s , _))} (λ v → {!𝓈 (s , v)!}) {!𝒯ₛ!}
-- -- -- -- -- -- -- -- -- -- --   -- Have: {s t : 𝓲} → (𝓥 s → 𝓣 t) → 𝓣 s → 𝓣 t
-- -- -- -- -- -- -- -- -- -- --   -- λ (𝒱 : 𝓥 𝒾) → 𝓈 (𝒾 , 𝒱)
-- -- -- -- -- -- -- -- -- -- --   MGU-noIndex.𝓢 go = {!!}
-- -- -- -- -- -- -- -- -- -- --   MGU-noIndex.sub go = {!sub {s} {t}!}
-- -- -- -- -- -- -- -- -- -- --   MGU-noIndex.mgu go = {!!}
-- -- -- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex.𝓥 (MGU-addIndex-to-noIndex m) = let open MGU-addIndex m in ∃ 𝓥
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex.𝓣 (MGU-addIndex-to-noIndex m) = let open MGU-addIndex m in ∃ 𝓣
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex._≐_ (MGU-addIndex-to-noIndex m) f g = {!let open MGU-addIndex m in ∀ (s t : 𝓲) → (𝒯ₜ : 𝓣 fst (f (s , 𝓥 s)) ≡ t →  ≡ g → Set !} -- ∀ {s t} → (f g : s ↦ t) → f ≐ g
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex._◃_ (MGU-addIndex-to-noIndex m) = {!let open MGU-addIndex m in _◃_!}
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex.𝓢 (MGU-addIndex-to-noIndex m) = {!!}
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex.sub (MGU-addIndex-to-noIndex m) = {!!}
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex.mgu (MGU-addIndex-to-noIndex m) = {!!}
-- -- -- -- -- -- -- -- -- -- -- -}
-- -- -- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex.𝓥 (MGU-addIndex-to-noIndex record { 𝓲 = 𝓲 ; 𝓥 = 𝓥 ; 𝓣 = 𝓣 ; _◃_ = _◃_ ; ◃ext = ◃ext ; 𝓢 = 𝓢 ; sub = sub ; mgu = mgu }) = ∃ 𝓥
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex.𝓣 (MGU-addIndex-to-noIndex record { 𝓲 = 𝓲 ; 𝓥 = 𝓥 ; 𝓣 = 𝓣 ; _◃_ = _◃_ ; ◃ext = ◃ext ; 𝓢 = 𝓢 ; sub = sub ; mgu = mgu }) = ∃ 𝓣
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex._≐_ (MGU-addIndex-to-noIndex m@(record { 𝓲 = 𝓲 ; 𝓥 = 𝓥 ; 𝓣 = 𝓣 ; _◃_ = _◃_ ; ◃ext = ◃ext ; 𝓢 = 𝓢 ; sub = sub ; mgu = mgu })) f g = {!!} -- (i : 𝓲) → MGU-addIndex._≐_ m (λ v → {!snd $ f (i , v)!}) (λ v → {!!})
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex._◃_ (MGU-addIndex-to-noIndex record { 𝓲 = 𝓲 ; 𝓥 = 𝓥 ; 𝓣 = 𝓣 ; _◃_ = _◃_ ; ◃ext = ◃ext ; 𝓢 = 𝓢 ; sub = sub ; mgu = mgu }) = {!!}
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex.𝓢 (MGU-addIndex-to-noIndex record { 𝓲 = 𝓲 ; 𝓥 = 𝓥 ; 𝓣 = 𝓣 ; _◃_ = _◃_ ; ◃ext = ◃ext ; 𝓢 = 𝓢 ; sub = sub ; mgu = mgu }) = {!!}
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex.sub (MGU-addIndex-to-noIndex record { 𝓲 = 𝓲 ; 𝓥 = 𝓥 ; 𝓣 = 𝓣 ; _◃_ = _◃_ ; ◃ext = ◃ext ; 𝓢 = 𝓢 ; sub = sub ; mgu = mgu }) = {!!}
-- -- -- -- -- -- -- -- -- -- -- MGU-noIndex.mgu (MGU-addIndex-to-noIndex record { 𝓲 = 𝓲 ; 𝓥 = 𝓥 ; 𝓣 = 𝓣 ; _◃_ = _◃_ ; ◃ext = ◃ext ; 𝓢 = 𝓢 ; sub = sub ; mgu = mgu }) = {!!}
-- -- -- -- -- -- -- -- -- -- -- -}

-- -- -- -- -- -- -- -- -- -- -- record MGU⋆ ℓⁱ ℓⱽ ℓᵀ ℓˢ : Set (lsuc (ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ ⊔ ℓˢ)) where
-- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- --     𝓲
-- -- -- -- -- -- -- -- -- -- --       : Set ℓⁱ

-- -- -- -- -- -- -- -- -- -- --     𝓥 -- variables
-- -- -- -- -- -- -- -- -- -- --       : 𝓲 → Set ℓⱽ

-- -- -- -- -- -- -- -- -- -- --     𝓣 -- terms
-- -- -- -- -- -- -- -- -- -- --       : 𝓲 → Set ℓᵀ

-- -- -- -- -- -- -- -- -- -- --   -- substitution
-- -- -- -- -- -- -- -- -- -- --   _↦_ : (s t : 𝓲) → Set (ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- -- --   _↦_ s t = 𝓥 s → 𝓣 t

-- -- -- -- -- -- -- -- -- -- --   infix 14 _≐_
-- -- -- -- -- -- -- -- -- -- --   _≐_ : {s t : 𝓲} → s ↦ t → s ↦ t → Set (ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- -- --   _≐_ f g = ∀ x → f x ≡ g x

-- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- --     -- substitution applied to a term
-- -- -- -- -- -- -- -- -- -- --     _◃_ : ∀ {s t} → s ↦ t → 𝓣 s → 𝓣 t
-- -- -- -- -- -- -- -- -- -- --     -- applying extentionally-equal subsitutions preserves equality of terms
-- -- -- -- -- -- -- -- -- -- --     ◃ext : ∀ {s t} {f g : s ↦ t} → f ≐ g → ∀ t → f ◃ t ≡ g ◃ t

-- -- -- -- -- -- -- -- -- -- --   _◇_ : ∀ {r s t : 𝓲} → (f : s ↦ t) (g : r ↦ s) → r ↦ t
-- -- -- -- -- -- -- -- -- -- --   _◇_ f g = (f ◃_) ∘ g

-- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- --     𝓢 : 𝓲 → 𝓲 → Set ℓˢ
-- -- -- -- -- -- -- -- -- -- --     sub : ∀ {s t} → 𝓢 s t → s ↦ t

-- -- -- -- -- -- -- -- -- -- --   Property : ∀ {ℓ} → 𝓲 → Set (lsuc ℓ ⊔ ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- -- --   Property {ℓ} s = ∀ {t} → s ↦ t → Set ℓ

-- -- -- -- -- -- -- -- -- -- --   Nothing : ∀ {ℓ m} → (P : Property {ℓ} m) → Set (ℓ ⊔ ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- -- --   Nothing P = ∀ {n} f → P {n} f → ⊥

-- -- -- -- -- -- -- -- -- -- --   Unifies : ∀ {i} (t₁ t₂ : 𝓣 i) → Property i
-- -- -- -- -- -- -- -- -- -- --   Unifies t₁ t₂ f = f ◃ t₁ ≡ f ◃ t₂

-- -- -- -- -- -- -- -- -- -- --   _≤_ : ∀ {m n n'} (f : m ↦ n) (g : m ↦ n') → Set (ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- -- --   _≤_ f g = ∃ λ f' → f ≐ (f' ◇ g)

-- -- -- -- -- -- -- -- -- -- --   Max : ∀ {ℓ m} (P : Property {ℓ} m) → Property m
-- -- -- -- -- -- -- -- -- -- --   Max P = (λ f → P f × (∀ {n} f' → P {n} f' → f' ≤ f))

-- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- --     mgu : ∀ {m} (t₁ t₂ : 𝓣 m) →
-- -- -- -- -- -- -- -- -- -- --           Nothing (Unifies t₁ t₂) ⊎ (∃ λ n → ∃ λ (σ : 𝓢 m n) → (Max (Unifies t₁ t₂)) (sub σ))

-- -- -- -- -- -- -- -- -- -- -- record MGU ℓⁱ ℓⱽ ℓᵀ ℓˢ : Set (lsuc (ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ ⊔ ℓˢ)) where
-- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- --     𝓲
-- -- -- -- -- -- -- -- -- -- --       : Set ℓⁱ

-- -- -- -- -- -- -- -- -- -- --     𝓥 -- variables
-- -- -- -- -- -- -- -- -- -- --       : 𝓲 → Set ℓⱽ

-- -- -- -- -- -- -- -- -- -- --     𝓣 -- terms
-- -- -- -- -- -- -- -- -- -- --       : 𝓲 → Set ℓᵀ

-- -- -- -- -- -- -- -- -- -- --   -- substitution
-- -- -- -- -- -- -- -- -- -- --   _↦_ : (s t : 𝓲) → Set (ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- -- --   _↦_ s t = 𝓥 s → 𝓣 t

-- -- -- -- -- -- -- -- -- -- --   infix 14 _≐_
-- -- -- -- -- -- -- -- -- -- --   _≐_ : {s t : 𝓲} → s ↦ t → s ↦ t → Set (ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- -- --   _≐_ f g = ∀ x → f x ≡ g x

-- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- --     -- substitution applied to a term
-- -- -- -- -- -- -- -- -- -- --     _◃_ : ∀ {s t} → s ↦ t → 𝓣 s → 𝓣 t
-- -- -- -- -- -- -- -- -- -- --     -- applying extentionally-equal subsitutions preserves equality of terms
-- -- -- -- -- -- -- -- -- -- --     ◃ext : ∀ {s t} {f g : s ↦ t} → f ≐ g → ∀ t → f ◃ t ≡ g ◃ t

-- -- -- -- -- -- -- -- -- -- --   _◇_ : ∀ {r s t : 𝓲} → (f : s ↦ t) (g : r ↦ s) → r ↦ t
-- -- -- -- -- -- -- -- -- -- --   _◇_ f g = (f ◃_) ∘ g

-- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- --     𝓢 : 𝓲 → 𝓲 → Set ℓˢ
-- -- -- -- -- -- -- -- -- -- --     sub : ∀ {s t} → 𝓢 s t → s ↦ t
-- -- -- -- -- -- -- -- -- -- --     mgu : ∀ {m} → (s t : 𝓣 m) → Maybe (∃ (𝓢 m))

-- -- -- -- -- -- -- -- -- -- --   Property⋆ : ∀ {ℓ} → 𝓲 → Set (lsuc ℓ ⊔ ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- -- --   Property⋆ {ℓ} s = ∀ {t} → s ↦ t → Set ℓ

-- -- -- -- -- -- -- -- -- -- --   Property : ∀ {ℓ} → 𝓲 → Set (lsuc ℓ ⊔ ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- -- --   Property {ℓ} s = Σ (Property⋆ {ℓ} s) λ P → ∀ {s f g} → f ≐ g → P {s} f → P g

-- -- -- -- -- -- -- -- -- -- --   Nothing : ∀ {ℓ m} → (P : Property {ℓ} m) → Set (ℓ ⊔ ℓⁱ ⊔ ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- -- --   Nothing P = ∀ {n} f → fst P {n} f → ⊥

-- -- -- -- -- -- -- -- -- -- --   Unifies : ∀ {i} (t₁ t₂ : 𝓣 i) → Property i
-- -- -- -- -- -- -- -- -- -- --   Unifies t₁ t₂ = (λ {_} f → f ◃ t₁ ≡ f ◃ t₂) , λ {_} {f} {g} f≐g f◃t₁=f◃t₂ →
-- -- -- -- -- -- -- -- -- -- --       g ◃ t₁
-- -- -- -- -- -- -- -- -- -- --     ≡⟨ sym (◃ext f≐g t₁) ⟩
-- -- -- -- -- -- -- -- -- -- --       f ◃ t₁
-- -- -- -- -- -- -- -- -- -- --     ≡⟨ f◃t₁=f◃t₂ ⟩
-- -- -- -- -- -- -- -- -- -- --       f ◃ t₂
-- -- -- -- -- -- -- -- -- -- --     ≡⟨ ◃ext f≐g t₂ ⟩
-- -- -- -- -- -- -- -- -- -- --       g ◃ t₂
-- -- -- -- -- -- -- -- -- -- --     ∎

-- -- -- -- -- -- -- -- -- -- --   _≤_ : ∀ {m n n'} (f : m ↦ n) (g : m ↦ n') → Set (ℓⱽ ⊔ ℓᵀ)
-- -- -- -- -- -- -- -- -- -- --   _≤_ f g = ∃ λ f' → f ≐ (f' ◇ g)

-- -- -- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- -- -- --   Max : ∀ {ℓ m} (P : Property {ℓ} m) → Property m
-- -- -- -- -- -- -- -- -- -- --   Max P' =
-- -- -- -- -- -- -- -- -- -- --     let open Σ P' using () renaming (fst to P; snd to Peq) in
-- -- -- -- -- -- -- -- -- -- --     let lemma1 : {m : 𝓲} {f : _ ↦ m} {g : _ ↦ m} →
-- -- -- -- -- -- -- -- -- -- --                  f ≐ g →
-- -- -- -- -- -- -- -- -- -- --                  P f × ({n : 𝓲} (f' : _ ↦ n) → P f' → f' ≤ f) →
-- -- -- -- -- -- -- -- -- -- --                  P g × ({n : 𝓲} (f' : _ ↦ n) → P f' → f' ≤ g)
-- -- -- -- -- -- -- -- -- -- --         lemma1 {_} {_} {g} f≐g = λ { (Pf , MaxPf) →
-- -- -- -- -- -- -- -- -- -- --           Peq f≐g Pf , λ {_} →
-- -- -- -- -- -- -- -- -- -- --             let lemma2 : ∀ {n} f' → P {n} f' → ∃ λ f0 → f' ≐ (f0 ◇ g)
-- -- -- -- -- -- -- -- -- -- --                 lemma2 f' Pf' =
-- -- -- -- -- -- -- -- -- -- --                   let f0 = fst (MaxPf f' Pf')
-- -- -- -- -- -- -- -- -- -- --                       f'≐f0◇f = snd (MaxPf f' Pf') in
-- -- -- -- -- -- -- -- -- -- --                   f0 , λ x → trans (f'≐f0◇f x) (cong (f0 ◃_) (f≐g x)) in
-- -- -- -- -- -- -- -- -- -- --             lemma2 } in
-- -- -- -- -- -- -- -- -- -- --     --(λ {_} f → P f × (∀ {n} f' → P {n} f' → f' ≤ f)) , λ {_} {_} {_} → lemma1
-- -- -- -- -- -- -- -- -- -- --     (λ f → P f × (∀ {n} f' → P {n} f' → f' ≤ f)) , lemma1
-- -- -- -- -- -- -- -- -- -- -- -}

-- -- -- -- -- -- -- -- -- -- --   Max : ∀ {ℓ m} (P : Property {ℓ} m) → Property⋆ m
-- -- -- -- -- -- -- -- -- -- --   Max P' =
-- -- -- -- -- -- -- -- -- -- --     let open Σ P' using () renaming (fst to P) in
-- -- -- -- -- -- -- -- -- -- --     (λ f → P f × (∀ {n} f' → P {n} f' → f' ≤ f))

-- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- -- -- --     mgu-c : ∀ {m} (t₁ t₂ : 𝓣 m) →
-- -- -- -- -- -- -- -- -- -- --             (∃ λ n → ∃ λ σ → fst (Max (Unifies t₁ t₂)) (sub σ) × mgu t₁ t₂ ≡ just (n , σ))
-- -- -- -- -- -- -- -- -- -- --             ⊎ (Nothing (Unifies t₁ t₂)                         × mgu t₁ t₂ ≡ nothing)

-- -- -- -- -- -- -- -- -- -- -- -}
-- -- -- -- -- -- -- -- -- -- --     mgu-c : ∀ {m} (t₁ t₂ : 𝓣 m) →
-- -- -- -- -- -- -- -- -- -- --             (∃ λ n → ∃ λ σ → (Max (Unifies t₁ t₂)) (sub σ) × mgu t₁ t₂ ≡ just (n , σ))
-- -- -- -- -- -- -- -- -- -- --             ⊎ (Nothing (Unifies t₁ t₂)                     × mgu t₁ t₂ ≡ nothing)

-- -- -- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- -- -- --     -- trivial substitution
-- -- -- -- -- -- -- -- -- -- --     -- ▹ : ∀ {s t} → (𝓥 s → 𝓥 t) → s ↦ t

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


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

module Experiment.ListConstruction where

open import Level renaming (zero to lzero; suc to lsuc)

data ⊥ : Set where

record ⊤ : Set where
  constructor tt

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

module Inductive where
  data List (A : Set) : Set where
    [] : List A
    _∷_ : A → List A → List A

data Bool : Set where
  true false : Bool

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

∃ : ∀ {a b} {A : Set a} (B : A → Set b) → Set (a ⊔ b)
∃ {a} {b} {A} B = Σ A B

if : ∀ {p} {P : Bool → Set p} → ∀ b → P true → P false → P b
if true  t e = t
if false t e = e

_⊎_ : (A B : Set) → Set
A ⊎ B = ∃ λ b → if b A B

inj₁ : {A B : Set} → A → A ⊎ B
inj₁ x = true , x

inj₂ : {A B : Set} → B → A ⊎ B
inj₂ x = false , x

⊎-elim : ∀ {p} {A B : Set} {P : A ⊎ B → Set p} →
  (∀ x → P (inj₁ x)) → (∀ y → P (inj₂ y)) → ∀ s → P s
⊎-elim x y (true  , snd) = x snd
⊎-elim x y (false , snd) = y snd

_×_ : (A B : Set) → Set
A × B = ∀ b → if b A B

proj₁ : {A B : Set} → A × B → A
proj₁ x = x true

proj₂ : {A B : Set} → A × B → B
proj₂ x = x false

Fin : ℕ → Set
Fin zero    = ⊥
Fin (suc n) = ⊤ ⊎ Fin n

Vec : Set → ℕ → Set
Vec A n = Fin n → A

module VecList where
  List : Set → Set
  List A = ∃ λ n → Vec A n

ext: agda


text:
module Cats.Ditrans where

open import Level using (Level ; _⊔_)

open import Cats.Category
open import Cats.Category.Setoids using (Setoids)
open import Cats.Profunctor

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
  where

  private
    module C = Category C
    open Category D

  record Ditrans (F G : Profunctor C C D) : Set (lo ⊔ la ⊔ la′ ⊔ l≈′)
    where
    field
      dicomponent : ∀ c → pobj F c c ⇒ pobj G c c
      dinatural : ∀ {a b} (f : a C.⇒ b)
        → pmap₂ G f ∘ dicomponent a ∘ pmap₁ F f
        ≈ pmap₁ G f ∘ dicomponent b ∘ pmap₂ F f

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
-- {-# OPTIONS --sized-types #-} -- no longer necessary
-- {-# OPTIONS --termination-depth=2 #-} -- not necessary!
-- {-# OPTIONS -v tc.size.solve:60 --show-implicit #-}
-- {-# OPTIONS -v term:5 #-}
module Issue709 where

open import Common.Size

data Bool : Set where true false : Bool

postulate
  A : Set
  _<=_ : A → A → Bool

data List {i : Size} : Set where
  []   : List
  cons : (j : Size< i) → A → List {j} → List {i}

module If where

  if_then_else_ : {A : Set} → Bool → A → A → A
  if true  then t else e = t
  if false then t else e = e

  merge : ∀ {i j} → List {i} → List {j} → List -- {∞}
  merge {i} {j} []             ys  = ys
  merge {i} {j} (cons i' x xs) []  = cons _ x xs
  merge {i} {j} (cons i' x xs) (cons j' y ys) =
    if x <= y
    then cons _ x (merge xs (cons _ y ys))
    else cons _ y (merge (cons _ x xs) ys)

module Succeeds where

  merge : ∀ {i j} → List {i} → List {j} → List
  merge          []            ys  = ys
  merge         (cons i' x xs) []  = cons _ x xs
  merge {i} {j} (cons i' x xs) (cons j' y ys) with x <= y
  ... | true  = cons _ x (merge {i'} {j} -- removing this implicit application makes it not termination check
                                xs (cons _ y ys))
  ... | false = cons _ y (merge (cons _ x xs) ys)

module NeedsTerminationDepthTwo where

  merge : ∀ {i j} → List {i} → List {j} → List
  merge          []            ys  = ys
  merge          (cons j x xs) []  = cons _ x xs
  merge {i} {i'} (cons j x xs) (cons j' y ys) with x <= y
  ... | true  = cons _ x (merge xs (cons _ y ys))
  ... | false = cons _ y (merge (cons _ x xs) ys)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas and James, Nov 2011 and Oct 2012
-- {-# OPTIONS --no-coverage-check #-}
-- {-# OPTIONS -v tc.lhs:20 -v tc.cover.top:20 #-}
module FlexInterpreter where

open import Common.MAlonzo

data Ty : Set where
  nat : Ty
  arr : Ty -> Ty -> Ty

data Exp : Ty -> Set where
  zero : Exp nat
  suc  : Exp (arr nat nat)
  pred : Exp (arr nat nat)
  app  : {a b : Ty} -> Exp (arr a b) -> Exp a -> Exp b

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

Sem : Ty -> Set
Sem nat = Nat
Sem (arr a b) = Sem a -> Sem b

eval' : (a : Ty) -> Exp a -> Sem a
eval' ._ zero = zero
eval' ._ suc  = suc
eval' b (app f e) = eval' _ f (eval' _ e)
eval' .(arr nat nat) pred zero = zero
eval' ._ pred (suc n) = n

eval : {a : Ty} -> Exp a -> Sem a
eval zero         = zero
eval suc          = suc
eval pred zero    = zero
eval pred (suc n) = n
eval (app f e)    = eval f (eval e)

main = mainDefault

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}
-- The option is supplied to force a real error to pass the regression test.
module MetaOccursInItself where

data List (A : Set) : Set where
  nil  : List A
  _::_ : A -> List A -> List A

data One : Set where one : One

postulate
  f : (A : Set) -> (A -> List A) -> One

err : One
err = f _ (\x -> x)

max_stars_repo_name: dagit/agda

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
module HelloWorldPrim where

open import IO.Primitive
open import Data.String

main = putStrLn (toCostring "Hello World!")


text:
module Category.Monad.Either {i}(Exc : Set i)(I : Set i) where

open import Level hiding (lift)
open import Data.Sum

open import Category.Monad
open import Category.Monad.Predicate
open import Relation.Unary
open import Relation.Unary.PredicateTransformer

pattern left x = inj₁ x
pattern right x = inj₂ x

EitherT : Pt I i → Pt I i
EitherT M P = M (λ i → Exc ⊎ P i)

module EitherT {M : Pt I i}(Mon : RawPMonad {ℓ = i} M) where

  private module Mon = RawPMonad Mon

  -- right-biased sum
  open RawPMonad
  monad : RawPMonad {ℓ = i} (EitherT M)
  return? monad px = Mon.return? (right px)
  _=<?_ monad {P}{Q} f px = g Mon.=<? px
    where
      g : (λ i → Exc ⊎ P i) ⊆ EitherT M Q
      g (left x) = Mon.return? (left x)
      g (right y) = f y

  _recoverWith_ : ∀ {P i} → EitherT M P i → (∀ {i} → Exc → EitherT M P i) → EitherT M P i
  _recoverWith_ {P} c f = g Mon.=<? c
    where
      g : (λ i → Exc ⊎ P i) ⊆ EitherT M P
      g (left x) = f x
      g (right y) = Mon.return? (right y)

  lift : ∀ {P} → M P ⊆ EitherT M P
  lift x = (λ z → Mon.return? (right z)) Mon.=<? x


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

module Categories.Kan.Duality where

open import Level

open import Categories.Category
open import Categories.Functor
open import Categories.NaturalTransformation
open import Categories.Kan

private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e
    F G : Functor C D

module _ {F : Functor C D} {G : Functor C E} where
  private
    module F = Functor F
    module G = Functor G

  coLan⇒Ran : Lan F.op G.op → Ran F G
  coLan⇒Ran lan = record
    { R        = L.op
    ; ε        = η.op
    ; δ        = λ M α → NaturalTransformation.op (σ (Functor.op M) (NaturalTransformation.op α))
    ; δ-unique = λ δ′ eq → σ-unique (NaturalTransformation.op δ′) eq
    ; commutes = λ M α → commutes (Functor.op M) (NaturalTransformation.op α)
    }
    where open Lan lan

  coRan⇒Lan : Ran F.op G.op → Lan F G
  coRan⇒Lan ran = record
    { L        = R.op
    ; η        = ε.op
    ; σ        = λ M α → NaturalTransformation.op (δ (Functor.op M) (NaturalTransformation.op α))
    ; σ-unique = λ σ′ eq → δ-unique (NaturalTransformation.op σ′) eq
    ; commutes = λ M α → commutes (Functor.op M) (NaturalTransformation.op α)
    }
    where open Ran ran

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
open import Type

module Relator.ReflexiveTransitiveClosure {ℓ₁ ℓ₂} {T : Type{ℓ₁}} (_▫_ : T → T → Type{ℓ₂}) where

open import Graph.Walk
open import Graph.Walk.Proofs
import      Lvl
open import Logic
open import Logic.Propositional
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Syntax.Function

-- Reflexive closure of a relation.
-- Constructs a reflexive relation from an existing relation.
-- Sometimes also notated ((_▫_) ∪ (_▫⁰_)) for a relation (_▫_).
data ReflexiveClosure : T → T → Type{ℓ₁ Lvl.⊔ ℓ₂} where
  super : Names.Subrelation(_▫_)(ReflexiveClosure)
  refl  : Names.Reflexivity(ReflexiveClosure)

-- Symmetric closure of a relation.
-- Constructs a symmetric relation from an existing relation.
-- Sometimes also notated (_▫⁻¹_) or (Converse(_▫_) ∪ (_▫_)) for a relation (_▫_).
SymmetricClosure : T → T → Type{ℓ₂}
SymmetricClosure a b = (b ▫ a) ∨ (a ▫ b)

-- Reflexive-transitive closure of a relation.
-- Constructs a reflexive and transitive relation from an existing relation.
-- Sometimes also notated (_▫*_) for a relation (_▫_).
data ReflexiveTransitiveClosure : T → T → Type{ℓ₁ Lvl.⊔ ℓ₂} where
  super : Names.Subrelation(_▫_)(ReflexiveTransitiveClosure)
  refl  : Names.Reflexivity(ReflexiveTransitiveClosure)
  trans : Names.Transitivity(ReflexiveTransitiveClosure)
infixl 1000 trans

-- Transitive closure of a relation.
-- Constructs a transitive relation from an existing relation.
-- Sometimes also notated (_▫⁺_) for a relation (_▫_).
data TransitiveClosure : T → T → Type{ℓ₁ Lvl.⊔ ℓ₂} where
  super : Names.Subrelation(_▫_)(TransitiveClosure)
  trans : Names.Transitivity(TransitiveClosure)

module _ where
  open import Numeral.Natural

  -- Sometimes also notated (_▫ⁿ_) for a relation (_▫_).
  data FiniteTransitiveClosure : ℕ → T → T → Type{ℓ₁ Lvl.⊔ ℓ₂} where
    base : ∀{a} → (a ▫ a) → (FiniteTransitiveClosure 𝟎 a a)
    step : ∀{a b c} → (a ▫ b) → ∀{n} → (FiniteTransitiveClosure n b c) → (FiniteTransitiveClosure (𝐒(n)) a c)

instance
  ReflexiveTransitiveClosure-reflexivity : Reflexivity(ReflexiveTransitiveClosure)
  ReflexiveTransitiveClosure-reflexivity = intro refl

instance
  ReflexiveTransitiveClosure-transitivity : Transitivity(ReflexiveTransitiveClosure)
  ReflexiveTransitiveClosure-transitivity = intro trans

-- The "prepend"-property of reflexive-transitive closure
ReflexiveTransitiveClosure-prepend : ∀{a b c} → (a ▫ b) → ReflexiveTransitiveClosure b c → ReflexiveTransitiveClosure a c
ReflexiveTransitiveClosure-prepend ab bc = trans (super ab) bc

-- A reflexive-transitive closure is the same as a path.
ReflexiveTransitiveClosure-Path-equivalence : ∀{a b} → (ReflexiveTransitiveClosure a b) ↔ (Walk(_▫_) a b)
ReflexiveTransitiveClosure-Path-equivalence = [↔]-intro l r where
  r : ∀{a b} → ReflexiveTransitiveClosure a b → Walk(_▫_) a b
  r ReflexiveTransitiveClosure.refl              = reflexivity(Walk(_▫_))
  r (ReflexiveTransitiveClosure.super ab)        = sub₂(_▫_)(Walk(_▫_)) ab
  r (ReflexiveTransitiveClosure.trans rab1 rb1b) = transitivity(Walk(_▫_)) (r rab1) (r rb1b)

  l : ∀{a b} → Walk(_▫_) a b → ReflexiveTransitiveClosure a b
  l Walk.at        = ReflexiveTransitiveClosure.refl
  l (Walk.prepend ab1 sb1b) = ReflexiveTransitiveClosure-prepend ab1 (l sb1b)

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:
{-# OPTIONS --without-K #-}

open import HoTT

module homotopy.AnyUniversalCoverIsPathSet {i} (A : Type i)
  -- (A-conn : is-connected 0 A)
  where

  open Cover

  module _
    (a₁ : A)
    -- A universal covering (defined as being simply connected).
    {j} (univ-cov : Cover A j)
    (univ-cov-univ : is-universal univ-cov)
    (a⇑₁ : Fiber univ-cov a₁)
    where

    private
      -- One-to-one mapping between the universal cover
      -- and the truncated path spaces from one point.

      [path] : ∀ (a⇑₁ a⇑₂ : TotalSpace univ-cov) → a⇑₁ =₀ a⇑₂
      [path] a⇑₁ a⇑₂ = –> (Trunc=-equiv [ a⇑₁ ] [ a⇑₂ ])
        (contr-has-all-paths univ-cov-univ [ a⇑₁ ] [ a⇑₂ ])

      [path]-has-all-paths :
        ∀ {a⇑₁ a⇑₂ : TotalSpace univ-cov}
        → has-all-paths (a⇑₁ =₀ a⇑₂)
      [path]-has-all-paths {a⇑₁} {a⇑₂} =
        coe (ap has-all-paths $ ua (Trunc=-equiv [ a⇑₁ ] [ a⇑₂ ]))
        $ contr-has-all-paths (raise-level -2 univ-cov-univ [ a⇑₁ ] [ a⇑₂ ])

      to : ∀ {a₂} → Fiber univ-cov a₂ → a₁ =₀ a₂
      to {a₂} a⇑₂ = ap₀ fst ([path] (a₁ , a⇑₁) (a₂ , a⇑₂))

      from : ∀ {a₂} → a₁ =₀ a₂ → Fiber univ-cov a₂
      from p = cover-trace univ-cov a⇑₁ p

      to-from : ∀ {a₂} (p : a₁ =₀ a₂) → to (from p) == p
      to-from = Trunc-elim
        (λ _ → =-preserves-set Trunc-level)
        (λ p → lemma p)
        where
          lemma : ∀ {a₂} (p : a₁ == a₂) → to (from [ p ]) == [ p ]
          lemma idp =
            ap₀ fst ([path] (a₁ , a⇑₁) (a₁ , a⇑₁))
              =⟨ ap (ap₀ fst)
                    $ [path]-has-all-paths
                      ([path] (a₁ , a⇑₁) (a₁ , a⇑₁))
                      (idp₀ :> ((a₁ , a⇑₁) =₀ (a₁ , a⇑₁))) ⟩
            (idp₀ :> (a₁ =₀ a₁))
              ∎

      from-to : ∀ {a₂} (a⇑₂ : Fiber univ-cov a₂) → from (to a⇑₂) == a⇑₂
      from-to {a₂} a⇑₂ = Trunc-elim
        (λ p → =-preserves-set
                {x = from (ap₀ fst p)}
                {y = a⇑₂}
                (Fiber-level univ-cov a₂))
        (λ p → to-transp $ snd= p)
        ([path] (a₁ , a⇑₁) (a₂ , a⇑₂))

    theorem : ∀ a₂ → Fiber univ-cov a₂ ≃ (a₁ =₀ a₂)
    theorem a₂ = to , is-eq _ from to-from from-to

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
open import Nat
open import Prelude
open import core
open import contexts
open import synth-unicity
open import lemmas-matching

module elaboration-unicity where
  mutual
    elaboration-unicity-synth : {Γ : tctx} {e : hexp} {τ1 τ2 : htyp} {d1 d2 : ihexp} {Δ1 Δ2 : hctx} →
                            Γ ⊢ e ⇒ τ1 ~> d1 ⊣ Δ1 →
                            Γ ⊢ e ⇒ τ2 ~> d2 ⊣ Δ2 →
                            τ1 == τ2 × d1 == d2 × Δ1 == Δ2
    elaboration-unicity-synth ESConst ESConst = refl , refl , refl
    elaboration-unicity-synth (ESVar {Γ = Γ} x₁) (ESVar x₂) = ctxunicity {Γ = Γ} x₁ x₂ , refl , refl
    elaboration-unicity-synth (ESLam apt1 d1) (ESLam apt2 d2)
      with elaboration-unicity-synth d1 d2
    ... | ih1 , ih2 , ih3 = ap1 _ ih1  , ap1 _ ih2 , ih3
    elaboration-unicity-synth (ESAp _ _ x x₁ x₂ x₃) (ESAp _ _ x₄ x₅ x₆ x₇)
      with synthunicity x x₄
    ... | refl with match-unicity x₁ x₅
    ... | refl with elaboration-unicity-ana x₂ x₆
    ... | refl , refl , refl with elaboration-unicity-ana x₃ x₇
    ... | refl , refl , refl = refl , refl , refl
    elaboration-unicity-synth ESEHole ESEHole = refl , refl , refl
    elaboration-unicity-synth (ESNEHole _ d1) (ESNEHole _ d2)
      with elaboration-unicity-synth d1 d2
    ... | ih1 , ih2 , ih3 = refl , ap1 _ ih2 , ap1 _ ih3
    elaboration-unicity-synth (ESAsc x) (ESAsc x₁)
      with elaboration-unicity-ana x x₁
    ... | refl , refl , refl = refl , refl , refl

    elaboration-unicity-ana : {Γ : tctx} {e : hexp} {τ τ1 τ2 : htyp} {d1 d2 : ihexp} {Δ1 Δ2 : hctx} →
                          Γ ⊢ e ⇐ τ ~> d1 :: τ1 ⊣ Δ1  →
                          Γ ⊢ e ⇐ τ ~> d2 :: τ2 ⊣ Δ2 →
                          d1 == d2 × τ1 == τ2 × Δ1 == Δ2
    elaboration-unicity-ana (EALam x₁ m D1) (EALam x₂ m2 D2)
      with match-unicity m m2
    ... | refl with elaboration-unicity-ana D1 D2
    ... | refl , refl , refl = refl , refl , refl
    elaboration-unicity-ana (EALam x₁ m D1) (EASubsume x₂ x₃ () x₅)
    elaboration-unicity-ana (EASubsume x₁ x₂ () x₄) (EALam x₅ m D2)
    elaboration-unicity-ana (EASubsume x x₁ x₂ x₃) (EASubsume x₄ x₅ x₆ x₇)
      with elaboration-unicity-synth x₂ x₆
    ... | refl , refl , refl = refl , refl , refl
    elaboration-unicity-ana (EASubsume x x₁ x₂ x₃) EAEHole = abort (x _ refl)
    elaboration-unicity-ana (EASubsume x x₁ x₂ x₃) (EANEHole _ x₄) = abort (x₁ _ _ refl)
    elaboration-unicity-ana EAEHole (EASubsume x x₁ x₂ x₃) = abort (x _ refl)
    elaboration-unicity-ana EAEHole EAEHole = refl , refl , refl
    elaboration-unicity-ana (EANEHole _ x) (EASubsume x₁ x₂ x₃ x₄) = abort (x₂ _ _ refl)
    elaboration-unicity-ana (EANEHole _ x) (EANEHole _ x₁)
      with elaboration-unicity-synth x x₁
    ... | refl , refl , refl = refl , refl , refl

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
module Esterel.Lang where

open import Esterel.Environment as Env
  using (Env)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)

open import Data.List
  using (List)
open import Data.Nat as Nat
  using (ℕ)

data s/l : Set where
  num : ℕ → s/l
  seq-ref : (x : SeqVar) → s/l
  shr-ref : (s : SharedVar) → s/l

data Expr : Set where
  plus : List s/l → Expr

data Ctrl : Set where
  GO : Ctrl
  WAIT : Ctrl

data Term : Set where
  nothin         : Term
  pause          : Term
  signl          : (S : Signal) → (p : Term) → Term
  present_∣⇒_∣⇒_ : (S : Signal) → (p : Term) → (q : Term) → Term
  emit           : (S : Signal) → Term
  _∥_            : (p : Term) → (q : Term) → Term
  loop           : (p : Term) → Term
  loopˢ          : (p : Term) → (q : Term) → Term
  _>>_           : (p : Term) → (q : Term) → Term
  suspend        : (p : Term) → (S : Signal) → Term
  trap           : (p : Term) → Term
  exit           : (n : ℕ) → Term
  shared_≔_in:_  : (s : SharedVar) → (e : Expr) → (p : Term) → Term
  _⇐_            : (s : SharedVar) → (e : Expr) → Term
  var_≔_in:_     : (x : SeqVar) → (e : Expr) → (p : Term) → Term
  _≔_            : (x : SeqVar) → (e : Expr) → Term
  if_∣⇒_∣⇒_      : (x : SeqVar) → (p : Term) → (q : Term) → Term
  ρ⟨_,_⟩·_        : (θ : Env) → (A : Ctrl) → (p : Term) → Term

infix  20 _⇐_
infix  20 _≔_
infix  17 if_∣⇒_∣⇒_
infixr 15 _>>_
infixr 13 _∥_
infix  11 present_∣⇒_∣⇒_
infix  10 shared_≔_in:_
infix  10 var_≔_in:_
infix   6 ρ⟨_,_⟩·_

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists where every pair of elements are related (symmetrically)
------------------------------------------------------------------------

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

open import Relation.Binary using (Rel)

module Data.List.Relation.Unary.AllPairs
       {a ℓ} {A : Set a} {R : Rel A ℓ} where

open import Data.List.Base using (List; []; _∷_)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.Product as Prod using (_,_; _×_; uncurry; <_,_>)
open import Function using (id; _∘_)
open import Level using (_⊔_)
open import Relation.Binary as B using (Rel; _⇒_)
open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
open import Relation.Nullary using (yes; no)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)

------------------------------------------------------------------------
-- Definition

open import Data.List.Relation.Unary.AllPairs.Core public

------------------------------------------------------------------------
-- Operations

head : ∀ {x xs} → AllPairs R (x ∷ xs) → All (R x) xs
head (px ∷ pxs) = px

tail : ∀ {x xs} → AllPairs R (x ∷ xs) → AllPairs R xs
tail (px ∷ pxs) = pxs

uncons : ∀ {x xs} → AllPairs R (x ∷ xs) → All (R x) xs × AllPairs R xs
uncons = < head , tail >

module _ {q} {S : Rel A q} where

  map : R ⇒ S → AllPairs R ⊆ AllPairs S
  map ~₁⇒~₂ [] = []
  map ~₁⇒~₂ (x~xs ∷ pxs) = All.map ~₁⇒~₂ x~xs ∷ (map ~₁⇒~₂ pxs)

module _ {s t} {S : Rel A s} {T : Rel A t} where

  zipWith : R ∩ᵇ S ⇒ T → AllPairs R ∩ᵘ AllPairs S ⊆ AllPairs T
  zipWith f ([] , [])             = []
  zipWith f (px ∷ pxs , qx ∷ qxs) = All.zipWith f (px , qx) ∷ zipWith f (pxs , qxs)

  unzipWith : T ⇒ R ∩ᵇ S → AllPairs T ⊆ AllPairs R ∩ᵘ AllPairs S
  unzipWith f []         = [] , []
  unzipWith f (rx ∷ rxs) = Prod.zip _∷_ _∷_ (All.unzipWith f rx) (unzipWith f rxs)

module _ {s} {S : Rel A s} where

  zip : AllPairs R ∩ᵘ AllPairs S ⊆ AllPairs (R ∩ᵇ S)
  zip = zipWith id

  unzip : AllPairs (R ∩ᵇ S) ⊆ AllPairs R ∩ᵘ AllPairs S
  unzip = unzipWith id

------------------------------------------------------------------------
-- Properties of predicates preserved by AllPairs

allPairs? : B.Decidable R → U.Decidable (AllPairs R)
allPairs? R? []       = yes []
allPairs? R? (x ∷ xs) =
  Dec.map′ (uncurry _∷_) uncons (All.all (R? x) xs ×-dec allPairs? R? xs)

irrelevant : B.Irrelevant R → U.Irrelevant (AllPairs R)
irrelevant irr []           []           = refl
irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
  cong₂ _∷_ (All.irrelevant irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)

satisfiable : U.Satisfiable (AllPairs R)
satisfiable = [] , []


text:
------------------------------------------------------------------------------
-- From inductive PA to standard axiomatic PA
------------------------------------------------------------------------------

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

-- From the definition of PA using Agda data types and primitive
-- recursive functions for addition and multiplication, we can prove
-- the following axioms (see (Machover 1996, p. 263) and (Hájek and
-- Pudlák 1998, p. 28)):

-- PA₁. 0 ≠ n'
-- PA₂. m' = n' → m = n
-- PA₃. 0 + n = n
-- PA₄. m' + n = (m + n)'
-- PA₅. 0 * n = 0
-- PA₆. m' * n = n + (m * n)
-- Axiom of induction:
-- φ(0) → (∀n.φ(n) → φ(succ n)) → ∀n.φ(n), for any formulae φ

module PA.Inductive2Standard where

open import PA.Inductive.Base

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

PA₁ : ∀ {n} → zero ≢ succ n
PA₁ ()

PA₂ : ∀ {m n} → succ m ≡ succ n → m ≡ n
PA₂ refl = refl

PA₃ : ∀ n → zero + n ≡ n
PA₃ n = refl

PA₄ : ∀ m n → succ m + n ≡ succ (m + n)
PA₄ m n = refl

PA₅ : ∀ n → zero * n ≡ zero
PA₅ n = refl

PA₆ : ∀ m n → succ m * n ≡ n + m * n
PA₆ m n = refl

------------------------------------------------------------------------------
-- References
--
-- Machover, Moshé (1996). Set theory, Logic and their
-- Limitations. Cambridge University Press.

-- Hájek, Petr and Pudlák, Pavel (1998). Metamathematics of
-- First-Order Arithmetic. 2nd printing. Springer.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --without-K --safe #-}
open import Level
open import Categories.Category using (Category)

module Categories.NaturalTransformation.Hom {o ℓ e : Level} (C : Category o ℓ e) where

-- open import Function using (_$_; Inverse) -- else there's a conflict with the import below
-- open import Function.Equality using (Π; _⟨$⟩_; cong)
-- open import Relation.Binary 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.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)

-- import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR

open Category C
open HomReasoning
open MR C
open NaturalTransformation
private
  module CE = Category.Equiv C
  module C = Category C

Hom[A,C]⇒Hom[B,C] : {A B : Obj} → (A ⇒ B) → NaturalTransformation Hom[ C ][-, A ] Hom[ C ][-, B ]
Hom[A,C]⇒Hom[B,C] {A} A⇒B = ntHelper record
  { η       = λ X → record { _⟨$⟩_ = λ X⇒A → A⇒B ∘ X⇒A ; cong = ∘-resp-≈ʳ }
  ; commute = λ f {g} {h} g≈h → begin
      A⇒B ∘ id ∘ g ∘ f   ≈˘⟨ assoc ⟩
      (A⇒B ∘ id) ∘ g ∘ f ≈⟨ id-comm ⟩∘⟨ g≈h ⟩∘⟨refl ⟩
      (id ∘ A⇒B) ∘ h ∘ f ≈⟨ assoc ○ ⟺ (∘-resp-≈ʳ assoc) ⟩ -- TODO: MR.Reassociate
      id ∘ (A⇒B ∘ h) ∘ f ∎
  }

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
open import Relation.Binary.Core

module BBHeap.Push.Properties {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BBHeap _≤_
open import BBHeap.Equality.Properties _≤_
open import BBHeap.Push _≤_ tot≤ trans≤
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.Nat
open import Data.List
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import List.Permutation.Base.Equivalence A
open import Order.Total _≤_ tot≤

mutual
  lemma-push⋘# : {b : Bound}{x y : A}{l r : BBHeap (val y)}(b≤x : LeB b (val x))(b≤y : LeB b (val y))(l⋘r : l ⋘ r) → # (push⋘ b≤x b≤y l⋘r) ≡ suc (# l + # r)
  lemma-push⋘# b≤x _ lf⋘ = refl
  lemma-push⋘# {x = x} b≤x b≤y (ll⋘ {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ =  refl
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = refl
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _
      with # (push⋘ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁) | lemma-push⋘# (lexy y₁≤x) (lexy refl≤) l₁⋘r₁
  ... | ._ | refl = refl
  lemma-push⋘# b≤x b≤y (ll⋘ y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂) | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x
      with # (push⋘ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂) | lemma-push⋘# (lexy y₂≤x) (lexy refl≤) l₂⋘r₂
  ... | ._ | refl = refl
  lemma-push⋘# {x = x} b≤x b≤y (lr⋘ {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ = refl
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = refl
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _
      with # (push⋙ (lexy y₁≤x) (lexy refl≤) l₁⋙r₁) | lemma-push⋙# (lexy y₁≤x) (lexy refl≤) l₁⋙r₁
  ... | ._ | refl = refl
  lemma-push⋘# b≤x b≤y (lr⋘ y≤y₁ y≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂) | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x
      with # (push⋘ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂) | lemma-push⋘# (lexy y₂≤x) (lexy refl≤) l₂⋘r₂
  ... | ._ | refl = refl

  lemma-push⋙# : {b : Bound}{x y : A}{l r : BBHeap (val y)}(b≤x : LeB b (val x))(b≤y : LeB b (val y))(l⋙r : l ⋙ r) → # (push⋙ b≤x b≤y l⋙r) ≡ suc (# l + # r)
  lemma-push⋙# {x = x} b≤x b≤y (⋙lf {x = z} y≤z)
      with tot≤ x z
  ... | inj₁ x≤z = refl
  ... | inj₂ z≤x = refl
  lemma-push⋙# {x = x} b≤x b≤y (⋙rl {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ = refl
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = refl
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _
      with # (push⋘ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁) | lemma-push⋘# (lexy y₁≤x) (lexy refl≤) l₁⋘r₁
  ... | ._ | refl = refl
  lemma-push⋙# b≤x b≤y (⋙rl y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂) | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x
      with # (push⋘ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂) | lemma-push⋘# (lexy y₂≤x) (lexy refl≤) l₂⋘r₂
  ... | ._ | refl = refl
  lemma-push⋙# {x = x} b≤x b≤y (⋙rr {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ = refl
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = refl
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _
      with # (push⋘ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁) | lemma-push⋘# (lexy y₁≤x) (lexy refl≤) l₁⋘r₁
  ... | ._ | refl = refl
  lemma-push⋙# b≤x b≤y (⋙rr y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂) | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x
      with # (push⋙ (lexy y₂≤x) (lexy refl≤) l₂⋙r₂) | lemma-push⋙# (lexy y₂≤x) (lexy refl≤) l₂⋙r₂
  ... | ._ | refl = refl

lemma-push# : {b : Bound}{x : A}(b≤x : LeB b (val x))(h : BBHeap b) → # (push b≤x h) ≡ # h
lemma-push# b≤x leaf = refl
lemma-push# b≤x (left b≤y l⋘r) = lemma-push⋘# b≤x b≤y l⋘r
lemma-push# b≤x (right b≤y l⋙r) = lemma-push⋙# b≤x b≤y l⋙r

mutual
  lemma-push⋘∼ : {b : Bound}{x y : A}{l r : BBHeap (val y)}(b≤x : LeB b (val x))(b≤y : LeB b (val y))(l⋘r : l ⋘ r) → flatten (push⋘ b≤x b≤y l⋘r) ∼ (x ∷ (flatten l ++ flatten r))
  lemma-push⋘∼ b≤x _ lf⋘ = ∼x /head /head ∼[]
  lemma-push⋘∼ {x = x} b≤x b≤y (ll⋘ {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ =  refl∼
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let pl'∼xfl₁fr₁ = lemma-push⋘∼ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁ ;
                        fpl'fr'∼xfl₁fr₁fr' = lemma++∼r pl'∼xfl₁fr₁
                   in ∼x /head (/tail /head) fpl'fr'∼xfl₁fr₁fr'
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = refl∼
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let pr'∼xfl₂fr₂ = lemma-push⋘∼ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂ ;
                        fl' = flatten (left (lexy y₂≤y₁) l₁⋘r₁) ;
                        fl'fpr'∼fl'xfl₂fr₂ = lemma++∼l {xs = fl'} pr'∼xfl₂fr₂ ;
                        xfl'fr'/y₂⟶xfl'fl₂fr₂ = lemma++/l {xs = x ∷ fl'} /head ;
                        fl'xfl₂fr₂/x⟶fl'fl₂fr₂ = lemma++/ {xs = fl'};
                        fl'xfl₂fr₂∼xfl'fl₂fr₂ = ∼x fl'xfl₂fr₂/x⟶fl'fl₂fr₂ /head refl∼ ;
                        fl'fpr'∼xfl'fl₂fr₂ = trans∼ fl'fpr'∼fl'xfl₂fr₂  fl'xfl₂fr₂∼xfl'fl₂fr₂
                   in ∼x /head xfl'fr'/y₂⟶xfl'fl₂fr₂ fl'fpr'∼xfl'fl₂fr₂
  lemma-push⋘∼ {x = x} b≤x b≤y (lr⋘ {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ = refl∼
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let pl'∼xfl₁fr₁ = lemma-push⋙∼ (lexy y₁≤x) (lexy refl≤) l₁⋙r₁ ;
                        fpl'fr'∼xfl₁fr₁fr' = lemma++∼r pl'∼xfl₁fr₁
                   in ∼x /head (/tail /head) fpl'fr'∼xfl₁fr₁fr'
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = refl∼
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let pr'∼xfl₂fr₂ = lemma-push⋘∼ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂ ;
                        fl' = flatten (right (lexy y₂≤y₁) l₁⋙r₁) ;
                        fl'fpr'∼fl'xfl₂fr₂ = lemma++∼l {xs = fl'} pr'∼xfl₂fr₂ ;
                        xfl'fr'/y₂⟶xfl'fl₂fr₂ = lemma++/l {xs = x ∷ fl'} /head ;
                        fl'xfl₂fr₂/x⟶fl'fl₂fr₂ = lemma++/ {xs = fl'};
                        fl'xfl₂fr₂∼xfl'fl₂fr₂ = ∼x fl'xfl₂fr₂/x⟶fl'fl₂fr₂ /head refl∼ ;
                        fl'fpr'∼xfl'fl₂fr₂ = trans∼ fl'fpr'∼fl'xfl₂fr₂  fl'xfl₂fr₂∼xfl'fl₂fr₂
                   in ∼x /head xfl'fr'/y₂⟶xfl'fl₂fr₂ fl'fpr'∼xfl'fl₂fr₂

  lemma-push⋙∼ : {b : Bound}{x y : A}{l r : BBHeap (val y)}(b≤x : LeB b (val x))(b≤y : LeB b (val y))(l⋙r : l ⋙ r) → flatten (push⋙ b≤x b≤y l⋙r) ∼ (x ∷ (flatten l ++ flatten r))
  lemma-push⋙∼ {x = x} b≤x b≤y (⋙lf {x = z} y≤z)
      with tot≤ x z
  ... | inj₁ x≤z = ∼x /head /head (∼x /head /head ∼[])
  ... | inj₂ z≤x = ∼x (/tail /head) /head (∼x /head /head ∼[])
  lemma-push⋙∼ {x = x} b≤x b≤y (⋙rl {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ = refl∼
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let pl'∼xfl₁fr₁ = lemma-push⋘∼ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁ ;
                        fpl'fr'∼xfl₁fr₁fr' = lemma++∼r pl'∼xfl₁fr₁
                   in ∼x /head (/tail /head) fpl'fr'∼xfl₁fr₁fr'
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = refl∼
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let pr'∼xfl₂fr₂ = lemma-push⋘∼ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂ ;
                        fl' = flatten (left (lexy y₂≤y₁) l₁⋘r₁) ;
                        fl'fpr'∼fl'xfl₂fr₂ = lemma++∼l {xs = fl'} pr'∼xfl₂fr₂ ;
                        xfl'fr'/y₂⟶xfl'fl₂fr₂ = lemma++/l {xs = x ∷ fl'} /head ;
                        fl'xfl₂fr₂/x⟶fl'fl₂fr₂ = lemma++/ {xs = fl'};
                        fl'xfl₂fr₂∼xfl'fl₂fr₂ = ∼x fl'xfl₂fr₂/x⟶fl'fl₂fr₂ /head refl∼ ;
                        fl'fpr'∼xfl'fl₂fr₂ = trans∼ fl'fpr'∼fl'xfl₂fr₂  fl'xfl₂fr₂∼xfl'fl₂fr₂
                   in ∼x /head xfl'fr'/y₂⟶xfl'fl₂fr₂ fl'fpr'∼xfl'fl₂fr₂
  lemma-push⋙∼ {x = x} b≤x b≤y (⋙rr {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ = refl∼
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let pl'∼xfl₁fr₁ = lemma-push⋘∼ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁ ;
                        fpl'fr'∼xfl₁fr₁fr' = lemma++∼r pl'∼xfl₁fr₁
                   in ∼x /head (/tail /head) fpl'fr'∼xfl₁fr₁fr'
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = refl∼
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let pr'∼xfl₂fr₂ = lemma-push⋙∼ (lexy y₂≤x) (lexy refl≤) l₂⋙r₂ ;
                        fl' = flatten (left (lexy y₂≤y₁) l₁⋘r₁) ;
                        fl'fpr'∼fl'xfl₂fr₂ = lemma++∼l {xs = fl'} pr'∼xfl₂fr₂ ;
                        xfl'fr'/y₂⟶xfl'fl₂fr₂ = lemma++/l {xs = x ∷ fl'} /head ;
                        fl'xfl₂fr₂/x⟶fl'fl₂fr₂ = lemma++/ {xs = fl'};
                        fl'xfl₂fr₂∼xfl'fl₂fr₂ = ∼x fl'xfl₂fr₂/x⟶fl'fl₂fr₂ /head refl∼ ;
                        fl'fpr'∼xfl'fl₂fr₂ = trans∼ fl'fpr'∼fl'xfl₂fr₂  fl'xfl₂fr₂∼xfl'fl₂fr₂
                   in ∼x /head xfl'fr'/y₂⟶xfl'fl₂fr₂ fl'fpr'∼xfl'fl₂fr₂

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Abstract.Types.EpochConfig
open        WithAbsVote

-- Here we establish the properties necessary to achieve consensus
-- just like we see them on paper: stating facts about the state of
-- the system and reasoning about which QC's exist in the system.
-- This module is a stepping stone to the properties we want;
-- you should probably not be importing it directly, see 'LibraBFT.Abstract.Properties'
-- instead.
--
-- The module 'LibraBFT.Abstract.Properties' proves that the invariants
-- presented here can be obtained from reasoning about sent votes,
-- which provides a much easier-to-prove interface to an implementation.

module LibraBFT.Abstract.RecordChain.Assumptions
    (UID    : Set)
    (_≟UID_ : (u₀ u₁ : UID) → Dec (u₀ ≡ u₁))
    (NodeId : Set)
    (𝓔      : EpochConfig UID NodeId)
    (𝓥      : VoteEvidence UID NodeId 𝓔)
  where

  open import LibraBFT.Abstract.Types           UID        NodeId 𝓔
  open import LibraBFT.Abstract.System          UID _≟UID_ NodeId 𝓔 𝓥
  open import LibraBFT.Abstract.Records         UID _≟UID_ NodeId 𝓔 𝓥
  open import LibraBFT.Abstract.Records.Extends UID _≟UID_ NodeId 𝓔 𝓥
  open import LibraBFT.Abstract.RecordChain     UID _≟UID_ NodeId 𝓔 𝓥
  open        EpochConfig 𝓔

  module _ {ℓ}(InSys : Record → Set ℓ) where

   -- Another important predicate of a "valid" RecordStoreState is the fact
   -- that α's n-th vote is always the same.
   VotesOnlyOnceRule : Set ℓ
   VotesOnlyOnceRule
      -- Given an honest α
      = (α : Member) → Meta-Honest-Member α
      -- For all system states where q and q' exist,
      → ∀{q q'} → (q∈𝓢 : InSys (Q q)) → (q'∈𝓢 : InSys (Q q'))
      -- such that α voted for q and q'; if α says it's the same vote, then it's the same vote.
      → (v  : α ∈QC q)(v' : α ∈QC q')
      → abs-vRound (∈QC-Vote q v) ≡ abs-vRound (∈QC-Vote q' v')
      -----------------
      → ∈QC-Vote q v ≡ ∈QC-Vote q' v'

  module _ {ℓ}(InSys  : Record → Set ℓ) where

   -- The preferred-round rule (aka locked-round-rule) is a critical
   -- aspect of LibraBFT's correctness. It states that an honest node α will cast
   -- votes for blocks b only if prevRound(b) ≥ preferred_round(α), where preferred_round(α)
   -- is defined as $max { round b | b is the head of a 2-chain }$.
   --
   -- Operationally, α can ensure it obeys this rule as follows: it keeps a counter
   -- preferred_round, initialized at 0 and, whenever α receives a QC q that forms a
   -- 2-chain:
   --
   --  Fig1
   --
   --    I ← ⋯ ← b₁ ← q₁ ← b ← q
   --        ⌞₋₋₋₋₋₋₋₋₋₋₋₋₋₋₋₋₋⌟
   --                2-chain
   --
   -- it checks whether round(b₁) , which is the head of the 2-chain above,
   -- is greater than its previously known preferred_round; if so, α updates
   -- it.  Note that α doesn't need to cast a vote in q, above, to have its
   -- preferred_round updated.  All that matters is that α has seen q.
   --
   -- We are encoding the rules governing Libra nodes as invariants in the
   -- state of other nodes. Hence, the PreferredRoundRule below states an invariant
   -- on the state of β, if α respects the preferred-round-rule.
   --
   -- Let the state of β be as below, such that α did cast votes for q
   -- and q' in that order (α is honest here!):
   --
   --
   --  Fig2
   --                            3-chain
   --        ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⌝
   --        |        2-chain            |          α knows of the 2-chain because
   --        ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⌝        |          it voted at the 3-chain.
   --    I ← ⋯ ← b₂ ← q₂ ← b₁ ← q₁ ← b ← q
   --         ↖
   --           ⋯ ← b₁' ← q₁' ← b' ← q'
   --
   -- Then, since α is honest and follows the preferred-round rule, we know that
   -- round(b₂) ≤ round(b₁') because, by seeing that α voted on q, we know that α
   -- has seen the 2-chain above, hence, α's preferred_round was at least round(b₂) at
   -- the time α cast its vote for b.
   --
   -- After casting a vote for b, α cast a vote for b', which means that α must have
   -- checked that round(b₂) ≤ prevRound(b'), as stated by the preferred round rule.
   --
   -- The invariant below states that, since α is honest, we can trust that these
   -- checks have been performed and we can infer this information solely
   -- by seeing α has knowledge of the 2-chain in Fig2 above.
   --
   PreferredRoundRule : Set ℓ
   PreferredRoundRule
     = ∀(α : Member) → Meta-Honest-Member α
     → ∀{q q'}(q∈𝓢 : InSys (Q q))(q'∈𝓢 : InSys (Q q'))
     → {rc : RecordChain (Q q)}{n : ℕ}(c3 : 𝕂-chain Contig (3 + n) rc)
     → (v : α ∈QC q) -- α knows of the 2-chain because it voted on the tail of the 3-chain!
     → (rc' : RecordChain (Q q'))
     → (v' : α ∈QC q')
     → abs-vRound (∈QC-Vote q v) < abs-vRound (∈QC-Vote q' v')
     → NonInjective-≡ bId ⊎ (getRound (kchainBlock (suc (suc zero)) c3) ≤ prevRound rc')

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Primitive

infixr 5 _,_
record Pair
  {a} (A : Set a) {b} (B : Set b)
  : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B

data Constraint
  {a} {A : Set a} (x : A)
  : Set where
  instance _ : Constraint x

record Outer
  l {a} {A : Set a} (x : A)
  : Set (lsuc l) where
  constructor #
  field type : Set l

record Inner
  {l} {a} {A : Set a} (x : A) {{_ : Constraint x}} (outer : Outer l x)
  : Set l where
  field value : Outer.type outer

module Class
  {l} {a} {A : Set a} (x : A) (C : Set l)
  where
  class = Inner x (# C)
  method : {{_ : class}} → C
  method {{INSTANCE}} = Inner.value INSTANCE

module Beekeeper
  {i} {I : Set i}
  (A : I -> Set)
  (B : I -> Set)
  (x : I)
  = Class (x , A , B)
          (A x -> B x)

module Indexed
  {a b b?} {I : Set}
  {A : I -> Set a}
  (mkA : ∀ {x} -> A x)
  (B : I -> Set b)
  (toB : ∀ {x} -> A x -> B x)
  (B? : ∀ {x} -> B x -> Set b?)
  = Class ((λ {x} -> toB {x}) , (λ {x} -> B? {x}))
          (∀ {x} -> B? (toB (mkA {x})))

module Unindexed
  {a b}
  {A : Set a}
  (mkA : A)
  {B : Set b}
  (toB : A -> B)
  (B? : B -> Set)
  = Class (mkA , toB , B?)
          (B? (toB mkA))

module _
  {a b} {I : Set}
  {A : I -> Set a}
  {mkA : ∀ {x} -> A x}
  {B : I -> Set b}
  {toB : ∀ {x} -> A x -> B x}
  {B? : ∀ {x} -> B x -> Set}
  {{_ : Indexed.class mkA B toB B?}}
  where
  postulate
    instance iToUnindexed : ∀ {x} -> Unindexed.class (mkA {x}) toB B?

postulate
  I : Set

data A
  a (x : I)
  : Set a where
  mkA : A a x

record B
  b (x : I)
  : Set (lsuc b) where
  field ?? : Set b
open B public

postulate
  toB : ∀ {a b x} -> A a x -> B b x
  instance
    iIndexedAB : ∀ {a b} -> Indexed.class (mkA {a}) (B b) toB (B.??)
  b : Level
  x : I
  myB : B b x

error : myB .??
error = {!Beekeeper.method _ _ _ _ _!}
-- Location of the error: src/full/Agda/TypeChecking/Substitute.hs:98


text:
module FRP.LTL.ISet where

open import FRP.LTL.ISet.Core public using ( ISet ; ⟨_⟩ ; ⟦_⟧ )

-- Propositional logic

open import FRP.LTL.ISet.Unit public using ( T )
open import FRP.LTL.ISet.Empty public using ( F )
open import FRP.LTL.ISet.Product public using ( _∧_ ; fst ; snd ; _&&&_ )
open import FRP.LTL.ISet.Sum public using ( _∨_ )
open import FRP.LTL.ISet.Stateless public using ( _⇒_ )

-- LTL

open import FRP.LTL.ISet.Next public using ( ○ )
open import FRP.LTL.ISet.Future public using ( ◇ )
open import FRP.LTL.ISet.Globally public using ( □ ; [_] )
open import FRP.LTL.ISet.Until public using ( _U_ )
open import FRP.LTL.ISet.Causal public using ( _⊵_ ; arr ; identity ; _⋙_ )
open import FRP.LTL.ISet.Decoupled public using ( _▹_ )

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
------------------------------------------------------------------------
-- Propositional equality, with some extra bells and whistles
-- definable in Cubical Agda
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

module Equality.Propositional.Cubical where

import Equality.Path as P

open import Equality.Propositional

open Equality.Propositional public using (refl; equivalence-relation⁺)

-- A family of implementations of P.Equality-with-paths.

private

  equality-with-paths′ :
    ∀ {a p} → P.Equality-with-paths a p equivalence-relation⁺
  equality-with-paths′ =
    P.Equality-with-J⇒Equality-with-paths equality-with-J

-- A family of implementations of P.Equality-with-paths.
--
-- The definition has been expanded in order to ensure that it does
-- not reduce (unless a projection is applied to it).

equality-with-paths :
  ∀ {a p} → P.Equality-with-paths a p equivalence-relation⁺
equality-with-paths         .P.Equality-with-paths.equality-with-J   = equality-with-paths′         .P.Equality-with-paths.equality-with-J
equality-with-paths {p = p} .P.Equality-with-paths.to-path           = equality-with-paths′ {p = p} .P.Equality-with-paths.to-path
equality-with-paths {p = p} .P.Equality-with-paths.from-path         = equality-with-paths′ {p = p} .P.Equality-with-paths.from-path
equality-with-paths {p = p} .P.Equality-with-paths.to-path∘from-path = equality-with-paths′ {p = p} .P.Equality-with-paths.to-path∘from-path
equality-with-paths {p = p} .P.Equality-with-paths.from-path∘to-path = equality-with-paths′ {p = p} .P.Equality-with-paths.from-path∘to-path
equality-with-paths {p = p} .P.Equality-with-paths.to-path-refl      = equality-with-paths′ {p = p} .P.Equality-with-paths.to-path-refl
equality-with-paths {p = p} .P.Equality-with-paths.from-path-refl    = equality-with-paths′ {p = p} .P.Equality-with-paths.from-path-refl

open P.Derived-definitions-and-properties equality-with-paths public
  hiding (refl)

open import Equality.Path.Isomorphisms equality-with-paths public

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

module Categories.Category.Finite.Fin where

open import Level
open import Data.Nat using (ℕ)
open import Data.Vec as Vec using (Vec)
open import Data.List
open import Data.Fin
open import Data.Fin.Properties
open import Axiom.UniquenessOfIdentityProofs
open import Relation.Binary using (Rel ; Decidable)
open import Relation.Binary.PropositionalEquality as ≡

open import Categories.Category

record Arrow (n : ℕ) (∣_⇒_∣ : Fin n → Fin n → ℕ) : Set where
  field
    dom : Fin n
    cod : Fin n
    arr : Fin ∣ dom ⇒ cod ∣

-- a hasShape of a finite catgegory
--
-- Classically, a finite category has a finite number of objects and a finite number
-- of morphisms. However, in this library, we cannot conveniently count the number of
-- objects and morphisms, because morphisms are identified up to the underlying
-- equivalence and objects have no general notion of identity. As a result, the
-- classical definition fails.
--
-- Nevetheless, if we know precisely what the objects and morphisms are, then we might
-- be able to count them. As a result, finite categories are just adjoint equivalent
-- to some category with a finite hasShape. Motivated by this idea, we can consider a
-- category with both objects and morphisms represented by Fin. We know Fin has
-- decidable equality and consequently also UIP. This allows us to operate
-- classically. We additionally require categorical axioms and thus ensure all shapes
-- form categories.
record HasFinCatShape (n : ℕ) (∣_⇒_∣ : Fin n → Fin n → ℕ) : Set where
  infix  4 _⇒_
  infixr 9 _∘_

  _⇒_ : Rel (Fin n) 0ℓ
  a ⇒ b = Fin ∣ a ⇒ b ∣

  field
    id  : ∀ {a} → a ⇒ a
    _∘_ : ∀ {a b c} → b ⇒ c → a ⇒ b → a ⇒ c

  field
    assoc     : ∀ {a b c d} {f : a ⇒ b} {g : b ⇒ c} {h : c ⇒ d} → (h ∘ g) ∘ f ≡ h ∘ (g ∘ f)
    identityˡ : ∀ {a b} {f : a ⇒ b} → id ∘ f ≡ f
    identityʳ : ∀ {a b} {f : a ⇒ b} → f ∘ id ≡ f

  objects : List (Fin n)
  objects = allFin n

  wrap-arr : ∀ {d c} (f : Fin ∣ d ⇒ c ∣) → Arrow n ∣_⇒_∣
  wrap-arr f = record { arr = f }

  morphisms : List (Arrow n ∣_⇒_∣)
  morphisms = concatMap (λ d → concatMap (λ c → tabulate (wrap-arr {d} {c})) objects) objects

  Obj-≟ : Decidable {A = Fin n} _≡_
  Obj-≟ = _≟_

  objects-vec : Vec (Fin n) n
  objects-vec = Vec.allFin n

  ⇒-≟ : ∀ {a b} → Decidable {A = a ⇒ b} _≡_
  ⇒-≟ = _≟_

  Obj-UIP : UIP (Fin n)
  Obj-UIP = Decidable⇒UIP.≡-irrelevant Obj-≟

  ⇒-UIP : ∀ {a b} → UIP (a ⇒ b)
  ⇒-UIP = Decidable⇒UIP.≡-irrelevant ⇒-≟

record FinCatShape : Set where
  infix 9 ∣_⇒_∣

  field
    size     : ℕ
    ∣_⇒_∣    : Fin size → Fin size → ℕ
    hasShape : HasFinCatShape size ∣_⇒_∣

  open HasFinCatShape hasShape public

FinCategory : FinCatShape → Category 0ℓ 0ℓ 0ℓ
FinCategory s = record
  { Obj       = Fin size
  ; _⇒_       = _⇒_
  ; _≈_       = _≡_
  ; id        = id
  ; _∘_       = _∘_
  ; assoc     = assoc
  ; sym-assoc = sym assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identityˡ
  ; equiv     = ≡.isEquivalence
  ; ∘-resp-≈  = cong₂ _∘_
  }
  where open FinCatShape s


text:
postulate
  T : Set → Set
  X : Set

  Class : Set → Set
  member : ∀ {A} {{C : Class A}} → A → A

  iX : Class X
  iT : ∀ {A} {{CA : Class A}} → Class (T A)

-- Should get type Class (T X),
-- not {{_ : Class X}} → Class (T X)
iTX = iT {A = X}

-- Fails if not expanding instance argument in iTX
f : T X → T X
f = member


text:
{-# OPTIONS --safe #-}
module Cubical.Data.NatPlusOne.MoreNats.AssocNat.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Empty
open import Cubical.Data.Unit
open import Cubical.Data.Nat hiding (_+_)

infixl 6 _+₁_

data ℕ₊₁ : Type where
  one : ℕ₊₁
  _+₁_ : ℕ₊₁ → ℕ₊₁ → ℕ₊₁
  assoc : (a b c : ℕ₊₁) →  a +₁ (b +₁ c) ≡ a +₁ b +₁ c
  trunc : isSet ℕ₊₁

module Elim {ℓ'} {B : ℕ₊₁ → Type ℓ'}
  (one* : B one) (_+₁*_ : {m n : ℕ₊₁} → B m → B n → B (m +₁ n))
  (assoc* : {x y z : ℕ₊₁} (x' : B x) (y' : B y) (z' : B z)
            → PathP (λ i → B (assoc x y z i))
            (x' +₁* (y' +₁* z')) ((x' +₁* y') +₁* z'))
  (trunc* : (n : ℕ₊₁) → isSet (B n)) where

  f : (n : ℕ₊₁) → B n
  f one = one*
  f (m +₁ n) = f m +₁* f n
  f (assoc x y z i) = assoc* (f x) (f y) (f z) i
  f (trunc m n p q i j) =
    isOfHLevel→isOfHLevelDep 2 trunc* (f m) (f n)
    (cong f p) (cong f q) (trunc m n p q) i j

module ElimProp {ℓ'} {B : ℕ₊₁ → Type ℓ'} (BProp : {n : ℕ₊₁} → isProp (B n))
  (one* : B one) (_+₁*_ : {m n : ℕ₊₁} → B m → B n → B (m +₁ n)) where

  f : (n : ℕ₊₁) → B n
  f = Elim.f {B = B} one* _+₁*_
        (λ {x} {y} {z} x' y' z' →
          toPathP (BProp (transport (λ i → B (assoc x y z i))
          (x' +₁* (y' +₁* z'))) ((x' +₁* y') +₁* z')))
        λ n → isProp→isSet BProp

module Rec {ℓ'} {B : Type ℓ'} (BType : isSet B)
  (one* : B) (_+₁*_ : B → B → B)
  (assoc* : (a b c : B) → a +₁* (b +₁* c) ≡ (a +₁* b) +₁* c) where

  f : ℕ₊₁ → B
  f = Elim.f one* (λ m n → m +₁* n) assoc* λ _ → BType

private
  constraintNumber : ℕ → Type
  constraintNumber zero = ⊥
  constraintNumber (suc _) = Unit

  fromNat' : (n : ℕ) ⦃ _ : constraintNumber n ⦄ → ℕ₊₁
  fromNat' zero ⦃ () ⦄
  fromNat' (suc zero) = one
  fromNat' (suc (suc n)) = fromNat' (suc n) +₁ one

instance
  NumN : HasFromNat ℕ₊₁
  NumN = record { Constraint = constraintNumber ; fromNat = fromNat' }

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Common.Prelude

data Wrap (A : Set) : Set where wrap : A → Wrap A

appWrap : ∀ {A B : Set} → (A → B) → Wrap A → B
appWrap f (wrap a) = f a

app : ∀ {A B : Set} → (A → B) → A → B
app f a = appWrap f (wrap a)

works : Nat
works = (λ _ → 42) ((λ _ → tt) 13)

-- (λ _ → tt) is erased but `app` tries to apply it
buggy : Nat
buggy = app (λ _ → 42) (app (λ _ → tt) 13)

main : IO ⊤
main = printNat buggy

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Issue1280 where

open import Common.Prelude
open import Common.Reflection

infixr 5 _∷_

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

test : Vec _ _
test = 0 ∷ []

quoteTest : Term
quoteTest = quoteTerm test

unquoteTest = unquote (give quoteTest)

data Foo (A : Set) : Set where
  foo : Foo A

ok : Foo Nat
ok = unquote (give (quoteTerm (foo {Nat})))

-- This shouldn't type-check. The term `bad` is type-checked because
-- the implicit argument of `foo` is missing when using quoteTerm.
bad : Foo Bool
bad = unquote (give (quoteTerm (foo {Nat})))


text:
module Control.Monad.Zero where

open import Prelude

record MonadZero {a b} (M : Set a → Set b) : Set (lsuc a ⊔ b) where
  instance constructor mkMonadZero
  field overlap {{super-zero}}  : FunctorZero M
        overlap {{super-monad}} : Monad M

open MonadZero public

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.NatPlusOne.Base where

open import Cubical.Core.Primitives
open import Cubical.Data.Nat
open import Cubical.Data.Empty

record ℕ₊₁ : Type₀ where
  constructor 1+_
  field
    n : ℕ

pattern one = 1+ zero
pattern 2+_ n = 1+ (suc n)

-1+_ : ℕ₊₁ → ℕ
-1+ (1+ n) = n

ℕ₊₁→ℕ : ℕ₊₁ → ℕ
ℕ₊₁→ℕ (1+ n) = suc n

suc₊₁ : ℕ₊₁ → ℕ₊₁
suc₊₁ (1+ n) = 1+ (suc n)

-- Natural number literals for ℕ₊₁

open import Cubical.Data.Nat.Literals public

instance
  fromNatℕ₊₁ : HasFromNat ℕ₊₁
  fromNatℕ₊₁ = record { Constraint = λ { zero → ⊥ ; _ → Unit }
                      ; fromNat = λ { (suc n) → 1+ n } }

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------------
-- Arithmetic properties (using induction on the FOTC natural numbers type)
------------------------------------------------------------------------------

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

-- Usually our proofs use pattern matching instead of the induction
-- principle associated with the FOTC natural numbers. The following
-- examples show some proofs using it.

module FOTC.Data.Nat.PropertiesByInductionATP where

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

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

+-leftIdentity : ∀ n → zero + n ≡ n
+-leftIdentity n = +-0x n

-- See Issue https://github.com/asr/apia/issues/81 .
+-rightIdentityA : D → Set
+-rightIdentityA i = i + zero ≡ i
{-# ATP definition +-rightIdentityA #-}

+-rightIdentity : ∀ {n} → N n → n + zero ≡ n
+-rightIdentity Nn = N-ind +-rightIdentityA A0 is Nn
  where
  postulate A0 : +-rightIdentityA zero
  {-# ATP prove A0 #-}

  postulate is : ∀ {i} → +-rightIdentityA i → +-rightIdentityA (succ₁ i)
  {-# ATP prove is #-}

-- See Issue https://github.com/asr/apia/issues/81 .
+-NA : D → D → Set
+-NA n i = N (i + n)
{-# ATP definition +-NA #-}

+-N : ∀ {m n} → N m → N n → N (m + n)
+-N {n = n} Nm Nn = N-ind (+-NA n) A0 is Nm
  where
  postulate A0 : +-NA n zero
  {-# ATP prove A0 #-}

  postulate is : ∀ {i} → +-NA n i → +-NA n (succ₁ i)
  {-# ATP prove is #-}

-- See Issue https://github.com/asr/apia/issues/81 .
+-assocA : D → D → D → Set
+-assocA n o i = i + n + o ≡ i + (n + o)
{-# ATP definition +-assocA #-}

+-assoc : ∀ {m} → N m → ∀ n o → m + n + o ≡ m + (n + o)
+-assoc Nm n o = N-ind (+-assocA n o) A0 is Nm
  where
  postulate A0 : +-assocA n o zero
  {-# ATP prove A0 #-}

  postulate is : ∀ {i} → +-assocA n o i → +-assocA n o (succ₁ i)
  {-# ATP prove is #-}

-- A proof without use ATPs definitions.
+-assoc' : ∀ {m} → N m → ∀ n o → m + n + o ≡ m + (n + o)
+-assoc' Nm n o = N-ind A A0 is Nm
  where
  A : D → Set
  A i = i + n + o ≡ i + (n + o)

  postulate A0 : zero + n + o ≡ zero + (n + o)
  {-# ATP prove A0 #-}

  postulate is : ∀ {i} →
                 i + n + o ≡ i + (n + o) →
                 succ₁ i + n + o ≡ succ₁ i + (n + o)
  {-# ATP prove is #-}

-- See Issue https://github.com/asr/apia/issues/81 .
x+Sy≡S[x+y]A : D → D → Set
x+Sy≡S[x+y]A n i = i + succ₁ n ≡ succ₁ (i + n)
{-# ATP definition x+Sy≡S[x+y]A #-}

x+Sy≡S[x+y] : ∀ {m} → N m → ∀ n → m + succ₁ n ≡ succ₁ (m + n)
x+Sy≡S[x+y] Nm n = N-ind (x+Sy≡S[x+y]A n) A0 is Nm
  where
  postulate A0 : x+Sy≡S[x+y]A n zero
  {-# ATP prove A0 #-}

  postulate is : ∀ {i} → x+Sy≡S[x+y]A n i → x+Sy≡S[x+y]A n (succ₁ i)
  {-# ATP prove is #-}

-- See Issue https://github.com/asr/apia/issues/81 .
+-commA : D → D → Set
+-commA n i = i + n ≡ n + i
{-# ATP definition +-commA #-}

+-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
+-comm {n = n} Nm Nn = N-ind (+-commA n) A0 is Nm
  where
  postulate A0 : +-commA n zero
  {-# ATP prove A0 +-rightIdentity #-}

  postulate is : ∀ {i} → +-commA n i → +-commA n (succ₁ i)
  {-# ATP prove is x+Sy≡S[x+y] #-}


text:
module Bootstrap.SimpleInductive where

open import Data.List using (applyUpTo)

open import Prelude

data ConstrData' : Set where
  Self : ConstrData'
  Other : String → ConstrData'

ConstrData = String × List ConstrData'
InductiveData = String × List ConstrData

private
  ℕ⊎Sshow : ℕ ⊎ String → String
  ℕ⊎Sshow (inj₁ x) = show x
  ℕ⊎Sshow (inj₂ y) = y

  ℕ⊎Ssuc : ℕ ⊎ String → ℕ ⊎ String
  ℕ⊎Ssuc (inj₁ x) = inj₁ (suc x)
  ℕ⊎Ssuc (inj₂ y) = inj₂ y

  constrDataToPrefix : (ℕ ⊎ String → String) → ℕ ⊎ String → Char → ConstrData → String
  constrDataToPrefix term n _ (_    , [])         = term n
  constrDataToPrefix term n c (name , x ∷ constr) =
    show c <+> "_ :" <+> (case x of λ { Self → ℕ⊎Sshow n ; (Other y) → y }) <+>
    constrDataToPrefix term (ℕ⊎Ssuc n) c (name , constr)

  constrDataToConstrPrefix : ℕ ⊎ String → Char → ConstrData → String
  constrDataToConstrPrefix = constrDataToPrefix (λ _ → "")

  constrDataToTypeAnn : ℕ ⊎ String → Char → ConstrData → String
  constrDataToTypeAnn = constrDataToPrefix ℕ⊎Sshow

  kthConstr : ℕ → InductiveData → String
  kthConstr k (name , constrs) with lookupMaybe k constrs
  ... | Maybe.just c@(_ , constr) =
    constrDataToConstrPrefix (inj₂ name) 'λ' c <+> -- constructor arguments
    "Λ _ : *" <+>
    unwords (flip mapWithIndex constrs -- abstract arguments
      (λ k constr → "λ _ :" <+> constrDataToTypeAnn (inj₁ k) 'Π' constr)) <+>
    -- apply all abstract arguments to self constructors and leave the others alone
    -- then pass the results to the k-th abstract constructor
    applyTo currentConstr
      (zipWith
        (λ where
          i Self → applyTo
            ("<" + show i <+> show (length constrs) + ">")
            abstractConstrs
          i (Other x) → show i)
        (applyUpTo ((length constrs + length constr) ∸_) $ length constr) constr)
    where
      currentConstr = show (length constrs ∸ k ∸ 1)

      abstractConstrs : List String
      abstractConstrs = reverse $ applyUpTo show $ length constrs

      applyTo : String → List String → String
      applyTo f fs = foldl (λ s l → "[" + s <+> l + "]") f fs
  kthConstr k constrs | nothing = "Error: no such constructor"

  kthConstrType : String → ℕ → List ConstrData → String
  kthConstrType name k constrs with lookupMaybe k constrs
  ... | just x = constrDataToTypeAnn (inj₂ name) 'Π' x
  ... | nothing = "Error: no such constructor"

  typeDecl : String → List ConstrData → String
  typeDecl name constrs =
    "∀ _ : *" <+>
    unwords (flip mapWithIndex constrs (λ k constr →
      "Π _ :" <+> constrDataToTypeAnn (inj₁ k) 'Π' constr)) <+>
    show (length constrs)

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

simpleInductive : InductiveData → String
simpleInductive d@(name , constrs) =
  "let" <+> name <+> ":=" <+> typeDecl name constrs + "." +
  unwords (flip mapWithIndex constrs
    (λ k constr →
      "let" <+> proj₁ constr <+> ":=" <+> kthConstr k d <+> ":" <+>
      kthConstrType name k constrs + "."))

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille