Yes, program is a term of art. It means a "term" in the type theory under consideration. A type theory is essentially a programming language with a fancy type s

Yes, program is a term of art. It means a "term" in the type theory under consideration. A type theory is essentially a programming language with a fancy type system, and there are many type theories, just as there are many programming languages. It does allow for functions without computable rules. In the case of the axiom of choice, one postulates as an axiom a program with a type that says something like "give me a type A and an A-indexed family of types, P : A -> Type, such that for all a:A, the type P a is non-empty, and I'll give you a function f : (a : A) -> P a". As far as I know, there is still no one comprehensive book on type theory. I think the type theory parts of the homotopy type theory book (https://hottheory.files.wordpress.com/2013/03/hott-online-611-ga1a258c.pdf https://hottheory.files.wordpress.com/2013/03/hott-online-61...) are quite good. Chapter 1 gives the basics of dependent type theory. Chapter 2 is about the groupoid interpretation of type theory and is quite nice. Chapter 3 is about "logical things" in type theory (things like axiom of choice). Chapter 5 is about inductive types which are quite central to type theory (these are generalizations of algebraic data types like trees and lists from functional programming languages).