{-
  Possible options for today:

  1. (Un-)countability and introduction to
     alternate mathematical universes (so-called toposes),
     particularly one in which there are
     fewer real numbers than natural numbers
     [great basis for an Agda project, but
     right now not in Agda]

  2. Program verification
     - Basic example
     - Insertion sort
     - Implementing a toy programming
       language ("the Hello World of Agda")

  3. Issues with standard Agda,
     introduction to Cubical Agda

  4. Exercises :-)

  5. Stop
-}


{-
  Within the standard topos, it holds that:
   
    Within the standard topos, we can have a look at the following
    toposes:
    1. Set
    2. Eff
    We will notice: These two toposes are not the same.

    Withing the effective topos (Eff), we can have a look at
    the following toposes:
    1. Set
    2. Eff
    We will notice: These two toposes are* the same.
    (More precisely: This is only true if everywhere we replace Eff
    by Eff', where Eff' is a close cousin of Eff. The difference
    between Eff and Eff' is only visible in constructive mathematics,
    not in classical mathematics.)

    Withing the topos Sh(ℝ), we can have a look at
    the following toposes:
    1. Set
    2. Sh(ℝ)
    We will notice: These two toposes are not the same.
-}