namespace latin:/❚

fixmeta ur:?LF❚

theory Propositions =
  prop  : type❙
❚

theory Proofs =
  include ?Propositions❙
  ded   : prop ⟶ type❘# ⊦ 1  prec -5❘role Judgment❙
  
  inconsistent : type❘= {a} ⊦ a❘# ↯❘role Judgment❙
  inconsistentE : inconsistent ⟶ {a} ⊦ a❘= [p,a] p a❘# 1 inconE %I2❙
❚

theory Logic =
  include ?Propositions❙
  include ?Proofs❙
❚

theory Terms =
  term : type❙
❚

theory Types =
  tp: type❙
❚

theory Kinds =
  kd : type❙
❚

theory TypedTerms =
  include ?Types❙
  tm: tp ⟶ type❘# tm 1 prec -5❙
❚

theory SoftTypedTerms =
  include ?Terms❙
  include ?Types❙
  include ?Propositions❙
  of : term ⟶ tp ⟶ prop❘# 1 ⦂ 2 prec 30❙
❚

theory KindedTypes =
  include ?Kinds❙
  tf : kd ⟶ type❘# tf 1 prec -5❙
  tpk : kd❙
  realize ?Types❙
  tp = tf tpk❙
❚

theory UntypedLogic =
  include ?Logic❙
  include ?Terms❙
❚

theory TypedLogic =
  include ?Logic❙
  include ?TypedTerms❙
❚

theory SoftTypedLogic =
  include ?SoftTypedTerms❙
  include ?Logic❙
❚         

theory InternalPropositions =
  include ?TypedTerms❙
  bool: tp❙
  realize ?Propositions❙
  prop = tm bool❙
❚

theory InternalLogic =
  include ?InternalPropositions❙
  include ?Proofs❙
❚

theory InternalTypes =
  include ?UntypedLogic❙
  in : term ⟶ term ⟶ prop❘# 1 ∈ 2 prec 30❙
  realize ?SoftTypedTerms❙
  tp = term❙
  of = in❙
  
  total structure typesAsPredicates : ?SoftTypedTerms =
    include ?Terms❙
    include ?Propositions❙
    tp = term ⟶ prop❙
    of = [X,A] A X❙
  ❚
❚