System T, a formulation of Church's Simple Theory of Types in Agda. From ~( http://publish.uwo.ca/~jbell/types.pdf ); Church's paper at ~( https://www.classes.cs.uchicago.edu/archive/2007/spring/32001-1/papers/church-1940.pdf )

T.agda

{- A straightforward version of Church’s simple type theory is the following system T -}
module T where

open import Data.Nat

-- The type of contexts.
data Γ (X : Set) : Set where
  ε : Γ X
  _::_ : (γ : Γ X) → X → Γ X
infixl 4 _::_

-- Types:
data Type : Set where
  Ι : Type -- The type of individuals
  Ω : Type -- The type of propositions
  _==>_ : Type → Type → Type -- Function types
infixr 4 _==>_

-- Variables (using de Bruijn Indexes).
data Var : Set where
  mkVar : ℕ → Var

-- Terms:
data Term : Set where
  var : Var → Term -- Variables
  _[_] : Term → Term → Term -- Function Application
  Λ_∙_ : Var → Term → Term -- λ Abstraction
  _==_ : Term → Term → Term -- Equality
  
  -- Extension of T by Henkin [1963]
  ⊤ : Term
  ⊥ : Term
  _⇒_ : Term → Term → Term
  _∧_ : Term → Term → Term
  _∨_ : Term → Term → Term
  for_all : Var → Type → Term → Term
  exist : Var → Type → Term → Term
 
open import Data.Product

data _∈_ (t : (Var × Type)) : Γ (Var × Type) → Set where
  here : ∀ {Γ} → t ∈ (Γ :: t)
  there : ∀ {Γ σ} → t ∈ Γ → t ∈ (Γ :: σ)
infix 3 _∈_

data _⊢_∶_ : Γ (Var × Type) → Term → Type → Set where
  var : {γ : Γ (Var × Type)}{x : Var}{τ : Type} →
              (x , τ) ∈ γ →
              -----------------
              γ ⊢ var x ∶ τ
              
  lam : {γ : Γ (Var × Type)}{x : Var}{M : Term}{σ τ : Type} →
             (γ :: (x , τ)) ⊢ M ∶ σ →
             ---------------
             γ ⊢ Λ x ∙ M ∶ (σ ==> τ)
             
  app : {γ : Γ (Var × Type)}{M N : Term}{σ τ : Type} →
             (γ ⊢ M ∶ (σ ==> τ)) →
             γ ⊢ N ∶ σ →
             ---------------------
             γ ⊢ M [ N ] ∶ τ

  eq : {γ : Γ (Var × Type)}{t u : Term}{α : Type} →
       (γ ⊢ t ∶ α) →
       (γ ⊢ u ∶ α) →
       --------------
       (γ ⊢ t == u ∶ Ω)
         
  true : {γ : Γ (Var × Type)} →
         ----------------------
         (γ ⊢ ⊤ ∶ Ω)

  falsum : {γ : Γ (Var × Type)} →
           ----------------------
           (γ ⊢ ⊥ ∶ Ω)
           
  impl : {γ : Γ (Var × Type)}{α β : Term} →
         (γ ⊢ α ∶ Ω) →
         (γ ⊢ β ∶ Ω) →
         --------------
         (γ ⊢ α ⇒ β ∶ Ω)

  conj : {γ : Γ (Var × Type)}{α β : Term} →
         (γ ⊢ α ∶ Ω) →
         (γ ⊢ β ∶ Ω) →
         --------------
         (γ ⊢ α ∧ β ∶ Ω)

  disj : {γ : Γ (Var × Type)}{α β : Term} →
         (γ ⊢ α ∶ Ω) →
         (γ ⊢ β ∶ Ω) →
         --------------
         (γ ⊢ α ∨ β ∶ Ω)

  for_all : {γ : Γ (Var × Type)}{x : Var}{τ : Type}{α : Term} →
            (γ :: (x , τ)) ⊢ α ∶ Ω →
            -------------------------
            (γ ⊢ for_all x τ α ∶ Ω)
            
  exist : {γ : Γ (Var × Type)}{x : Var}{τ : Type}{α : Term} →
          (γ :: (x , τ)) ⊢ α ∶ Ω →
          -------------------------
          (γ ⊢ exist x τ α ∶ Ω)       
infix 3 _⊢_∶_