The definition of propositional connectives and quantifiers in dependent type theory (higher-order logic):

http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf