Add takeaways

agda/01-effectful/Monad.lagda.rst

@@ -23,12 +23,19 @@ Today, we shall:
   - present a general framework for modelling *algebraic* effects
   - meet a few monads (reader, writer, non-determinism, random, CPS, etc.)
 
-`Notions of computations determine monads`_:
+Vision: `Notions of computations determine monads`_
   1. syntax of effectful operations
   2. equational theory of effectful operations
   3. denotational semantics = quotiented syntax
   4. interpreter / monad!
 
+Takeaways:
+  - you will be *able* to define a monad (``return``, ``bind``) and its supporting operations
+  - you will be *able* to use the following monads: exceptions, reader, writer, state, non-determinism
+  - you will be *able* to relate an equational theory with a monadic presentation (normalization-by-evaluation)
+  - you will be *familiar* with algebraic effects
+  - you will be *familiar* with the most commonly used monads
+
 
 ************************************************
 Historical background

agda/02-dependent/Indexed.lagda.rst

@@ -34,6 +34,13 @@ Today, we shall:
 
 The vision: `The Proof Assistant as an Integrated Development Environment`_
 
+Takeaways:
+  - you will be *able* to use inductive families to encode structural invariants
+  - you will be *able* to write dependently-typed programs over inductive families
+  - you will be *able* to construct denotational models in type theory
+  - you will be *familiar* with the Yoneda lemma
+  - you will be *familiar* with the notion of functor and presheaf
+  - you will be *familiar* with normalization-by-evaluation for the simply-typed calculus
 
 ..
   ::
@@ -45,6 +52,7 @@ The vision: `The Proof Assistant as an Integrated Development Environment`_
 Typing ``sprintf``
 ************************************************
 
+
 ..
   ::
 
@@ -1258,15 +1266,18 @@ implementation::
 
 
 
-By defining a richly-structured model, we have seen how we could
-implement a typed model of the λ-calculus and manipulate binders in
-the model.
+************************************************
+Conclusion
+************************************************
+
+In the first and second part, we have seen how inductive types and
+families can be used to build initial models, supporting the
+definition of various interpretations in Agda itself.
+
+In the third part, we have seen how, by defining a richly-structured
+model, we could implement a typed model of the λ-calculus and
+manipulate binders in the model.
 
-Takeaways:
-  * You are *familiar* with the construction of denotational models in type theory
-  * You are *able* to define an inductive family that captures exactly some structural invariant
-  * You are *able* to write a dependently-typed program
-  * You are *familiar* with normalization-by-evaluation proofs for the simply-typed calculus
 
 **Exercises (difficulty: open ended):**
 
@@ -1284,9 +1295,10 @@ Takeaways:
      categorical semantics (described in the next section) provides
      the blueprint of the necessary proofs.
 
--------------------------------------
+
+************************************************
 Optional: Categorical spotting
--------------------------------------
+************************************************
 
 ..
   ::

agda/03-total/Recursion.lagda.rst

@@ -62,6 +62,14 @@ The vision: `Total Functional Programming`_
   - zealously pursued with dependent types by `Conor McBride <http://strictlypositive.org/>`_
   - at the origin of *all* of today's examples
 
+Takeaways:
+  - you will be *able* to reify a measure by indexing an inductive type
+  - you will be *able* to define your own induction principles
+  - you will be *able* to give a "step-indexed" interpretation of a general recursive function
+  - you will be *familiar* with the Bove-Capretta technique
+  - you will be *familiar* with the notion of monad morphism
+
+
 ************************************************
 First-order Unification
 ************************************************
@@ -483,6 +491,7 @@ underlying composition of substitutions::
 Structurally: most-general unifier
 --------------------------------------
 
+
 The implementation of the most-general unifier is exactly the same,
 excepted that termination has become self-evident: when performing the
 substitution (case ``amgu {suc k} _ _ (m , (σ ∷[ r / z ]))``), the