Minimal intuitionistic first-order logic (SOGAT) [ag-0008]

{-# OPTIONS --safe --without-K #-}
module ag-0008 where

open import MLTT.Spartan
open import UF.Subsingletons

record minimal-intuitionistic-first-order-logic : 𝓤₁ ̇  where
  field
    For : 𝓤₀ ̇
    Tm : 𝓤₀ ̇
    _⊃_ : For → For → For
    All : (Tm → For) → For
    Eq : Tm → Tm → For

    Pf : For → 𝓤₀ ̇
    Pf-is-prop : (A : For) → is-prop (Pf A)

    intro⊃ : {A B : For} → (Pf A → Pf B) → Pf (A ⊃ B)
    elim⊃ : {A B : For} → Pf (A ⊃ B) → (Pf A → Pf B)

    intro∀ : {A : Tm → For} → ((𝑡 : Tm) → Pf (A 𝑡)) → Pf (All A)
    elim∀ : {A : Tm → For} → Pf (All A) → ((𝑡 : Tm) → Pf (A 𝑡))

    introEq : {t : Tm} → Pf (Eq t t)
    elimEq : {t t' : Tm} → (A : Tm → For) → Pf (Eq t t') → Pf (A t) → Pf (A t')

一樣參照 first-order lambda calculus 的過程，加上 contexts、加上 substitutions，相應的 first-order 等式跟改寫。