Intuitionistic type theory in Twelf (try in the playground at: https://twelf.org/twelf-wasm/)

intuitionistic.elf

%% Intuitionistic type theory in Twelf by Brendan Zabarauskas
%%
%% Inspired by the examples found in “An Equational Logical Framework 
%% for Type Theories” https://arxiv.org/abs/2106.01484

tp : type.
el : tp -> type.

%% Equality

eq-tp : tp -> tp -> type.
eq-el : el A -> el A -> type.

% Reflexivity
eq-tp/refl : eq-tp A A.
eq-el/refl : eq-el X X.

% Symmetry
eq-tp/symm : eq-tp A B -> eq-tp B A.
eq-el/symm : eq-el X Y -> eq-el Y X.

% Transitivity
eq-tp/trans : eq-tp A B -> eq-tp B C -> eq-tp A C.
eq-el/trans : eq-el X Y -> eq-el Y Z -> eq-el X Z.

%% Natural numbers

nat : tp.
nat-zero : el nat.
nat-succ : el nat -> el nat.
nat-ind : {A : el nat -> tp} el (A nat-zero) -> ({n} el (A n) -> el (A (nat-succ n))) -> {n} el (A n).

eq-tp/nat : eq-tp nat nat.
eq-el/nat-β-zero : eq-el (nat-ind A Z S nat-zero) Z.
eq-el/nat-β-succ : eq-el (nat-ind A Z S (nat-succ N)) (S N (nat-ind A Z S N)).

%% Dependent functions

fun : {A : tp} (el A -> tp) -> tp.
fun-abs : ({x : el A} el (B x)) -> el (fun A B).
fun-app : el (fun A B) -> {x : el A} el (B x).

eq-tp/fun : eq-tp A1 A2 -> ({x} {y} eq-tp (B1 x) (B2 y)) -> eq-tp (fun A1 B1) (fun A2 B2).
eq-el/fun-β : eq-el (fun-app (fun-abs F) X) (F X).
eq-el/fun-η : eq-el F (fun-abs ([x] fun-app F x)).

% Dependent pairs

pair : {A : tp} (el A -> tp) -> tp.
pair-intro : {x : el A} el (B x) -> el (pair A B).
pair-fst : el (pair A B) -> el A.
pair-snd : {p : el (pair A B)} el (B (pair-fst p)).

eq-tp/pair : eq-tp A1 A2 -> ({x} {y} eq-tp (B1 x) (B2 y)) -> eq-tp (pair A1 B1) (pair A2 B2).
eq-el/pair-β-fst : eq-el (pair-fst (pair-intro X Y)) X.
% FIXME:
% eq-el/pair-β-snd : eq-el (pair-snd (pair-intro X Y)) Y.
%
%   Typing ambiguous -- unresolved constraints
%   X1 A B X Y (pair-fst (pair-intro X Y)) = B X;
%   X1 A B X Y X = B X.
%
% The definition of `pair-snd` uses `pair-fst`, which Twelf doesn't know how to reduce this when unifying.
% The conversion rules for `pair-fst` are defined using `eq-el`, but Twelf knows nothing about this relation.
%
eq-el/pair-η : eq-el P (pair-intro (pair-fst P) (pair-snd P)).

% Identity type

id : {A : tp} el A -> el A -> tp.
id-refl : {A : tp} {X : el A} el (id A X X).
% TODO: id-elim
eq-tp/id : eq-el X1 X2 -> eq-el Y1 Y2 -> eq-tp (id A X1 Y1) (id A X2 Y2).
% TODO: eq-el/id-β

% TODO: Tarskian-universes