Martin Escardo

Modular version of https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes

\begin{code}

{-# OPTIONS --safe --without-K #-}

module MGS.index where

import MGS.Basic-UF
import MGS.Choice
import MGS.Classifiers
import MGS.Embeddings
import MGS.Equivalence-Constructions
import MGS.Equivalence-Induction
import MGS.Equivalences
import MGS.FunExt-from-Univalence
import MGS.Function-Graphs
import MGS.HAE
import MGS.MLTT
import MGS.Map-Classifiers
import MGS.More-Exercise-Solutions
import MGS.More-FunExt-Consequences
import MGS.Partial-Functions
import MGS.Powerset
import MGS.Quotient
import MGS.Retracts
import MGS.SIP
import MGS.Size
import MGS.Solved-Exercises
import MGS.Subsingleton-Theorems
import MGS.Subsingleton-Truncation
import MGS.TypeTopology-Interface
import MGS.Unique-Existence
import MGS.Univalence
import MGS.Universe-Lifting
import MGS.Yoneda
import MGS.hlevels

\end{code}