natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
hom-set, hom-object, internal hom, exponential object, derived hom-space
loop space object, free loop space object, derived loop space
Linear implication is the most common version of implication/function type in linear logic/linear type theory.
The categorical semantics of linear implication is as the internal hom in the closed monoidal category of types.
Closely related is the multiplicative implication of bunched implication logic, though they behave somewhat differently.