• Organization
• Participants
• Notes (from Matthieu)
• 8.10
• 8.11
• Multiple universe hierarchies (Matthieu Sozeau)
• Reals (Vincent Semeria):
• Coq Platform (Michael Soegtrop)
• opam packages and bench (Guillaume Claret)
• Universe Polymorphism, HoTT & math-comp (Andreas Lynge)