Symbol Reference: ifᵈₑₚ / simple_if / IF..FI — Dependent Conditional Branching (ifᵈₑₚ) & Simple Conditional

Personal Symbol Reference Page in MKTD1 & MKTD2 (Morse-Kelley + Tarski + Dunaev) — All Personal Symbol Pages → | Full Symbol Registry →

Formula Display:
Proof Trees:

ifᵈₑₚ / simple_if / IF..FI \(\mathsf{if}_{\mathsf{dep}} \; / \; \mathsf{if}\) — Dependent Conditional Branching (ifᵈₑₚ) & Simple Conditional

Eliminates a Boolean condition b : Bool into a dependent type family Tₑ : Bool → Type (Entry DefDependentConditional (3.24)), where the true branch has type Tₑ(⊤) and the false branch has type Tₑ(⊥).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
ifᵈₑₚ / simple_if / IF..FI
\(\mathsf{if}_{\mathsf{dep}} \; / \; \mathsf{if}\)
Category Conditionals & Dependent Elimination
SML AST Constructor EIfDep / ifDep_axm_entry [Dependent Conditional, foundations.ML / entries.ML:DefDependentConditional (3.24)]
Constructor Arguments 1. Type family Tₑ : Bool → Type; 2. Condition b : Bool; 3. True branch t₁ : ⟦Tₑ(⊤)⟧; 4. False branch t₂ : ⟦Tₑ(⊥)⟧
Metatype / Signature ∀(Tₑ : Bool → Type). ∀(b : Bool). Tₑ(⊤) → Tₑ(⊥) → Tₑ(b)
Binder Status No — Dependent Conditional Functional Symbol
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mathsf{if}_{\mathsf{dep}} \; / \; \mathsf{if}
How to Understand It

Notation & Semantics of ifᵈₑₚ (Directive 13 & Entries DefSimpleConditional (3.23)–DefDependentConditional (3.24)):

  • Unicode Subscript Rendering: In Unicode formula mode, the dependent conditional is rendered with true Unicode subscript/modifier letters as ifᵈₑₚ, and its branch parameters use Unicode subscripts Tₑ, t₁, t₂.
  • LaTeX Rendering: In LaTeX mode, it renders via MathJax as \mathsf{if}_{\mathsf{dep}} with branch parameters T_e, t_1, t_2.
  • Dependent Typing Rule (Entry DefDependentConditional (3.24)): Given a family of types Tₑ : Bool → Type, a Boolean b : Bool, a true-branch witness t₁ : Tₑ(⊤), and a false-branch witness t₂ : Tₑ(⊥), the term ifᵈₑₚ(Tₑ, b, t₁, t₂) has type Tₑ(b) and satisfies the beta-reduction laws ifᵈₑₚ(Tₑ, ⊤, t₁, t₂) = t₁ and ifᵈₑₚ(Tₑ, ⊥, t₁, t₂) = t₂ (verified in Variant 2 as thm_85_if_dep_true_branch and thm_86_if_dep_false_branch).
Canonical Law / Usage (ifᵈₑₚ(Tₑ, ⊤, t₁, t₂) = t₁) ∧ (ifᵈₑₚ(Tₑ, ⊥, t₁, t₂) = t₂)
Related Symbols & Kernel Entries