Certified Programming with Dependent Types, CAS 763, 2019

Read the following sections of the Agda documentation:

• Function Types
• Implicit Arguments
• Data Types

Also have a first look at:

• Pattern Matching Lambda (to be aware that there is more to that than mentioned in PLFA)
• Record Types (up to “Record modules”)

• Isomorphisms — at least read this. You will need to create isomorphisms in the following sections.
• Connectives and Negation: These correspond closely to the explanations of the Curry-Howard correspondance for propositional logic given in the Wednesday lecture.
• Quantifiers: Curry-Howard correspondance for predicate logic.