source/Fin/Bishop.lagda
source/Groups/Free.lagda
source/InjectiveTypes/Algebra.lagda
source/InjectiveTypes/Article.lagda
source/InjectiveTypes/Blackboard.lagda
source/InjectiveTypes/OverSmallMaps.lagda
source/InjectiveTypes/Structure.lagda
source/InjectiveTypes/WeakFactorizationSystem.lagda
source/Iterative/Multisets-Addendum.lagda
source/Iterative/Multisets.lagda
source/Iterative/Sets.lagda
source/Lifting/UnivalentWildCategory.lagda
source/MGS/Embeddings.lagda
source/MGS/Equivalences.lagda
source/MGS/FunExt-from-Univalence.lagda
source/MGS/HAE.lagda
source/MGS/Map-Classifiers.lagda
source/MGS/More-FunExt-Consequences.lagda
source/MGS/SIP.lagda
source/MGS/Solved-Exercises.lagda
source/MGS/Subsingleton-Truncation.lagda
source/Notation/General.lagda
source/NotionsOfDecidability/Decidable.lagda
source/NotionsOfDecidability/QuasiDecidable.lagda
source/OrderedTypes/FreeJoinSemiLattice.lagda
source/Ordinals/Closure.lagda
source/Ordinals/Injectivity.lagda
source/Ordinals/NotationInterpretation0.lagda
source/Ordinals/WellOrderArithmetic.lagda
source/Taboos/LPO.lagda
source/TypeTopology/DecidabilityOfNonContinuity.lagda
source/TypeTopology/DenseMapsProperties.lagda
source/TypeTopology/Density.lagda
source/TypeTopology/SquashedSum.lagda
source/TypeTopology/TotallySeparated.lagda
source/UF/Base.lagda
source/UF/Classifiers-Old.lagda
source/UF/Classifiers.lagda
source/UF/ConnectedTypes.lagda
source/UF/Embeddings.lagda
source/UF/Equiv.lagda
source/UF/EquivalenceExamples.lagda
source/UF/FunExt-Properties.lagda
source/UF/ImageAndSurjection-Variation.lagda
source/UF/ImageAndSurjection.lagda
source/UF/Knapp-UA.lagda
source/UF/PairFun.lagda
source/UF/Powerset-MultiUniverse.lagda
source/UF/Pullback.lagda
source/UF/SIP-Examples.lagda
source/UF/Size-TruncatedConnected.lagda
source/UF/Size.lagda
source/UF/SmallnessProperties.lagda
source/UF/Yoneda.lagda
source/Various/UnivalenceFromScratch.lagda
source/W/Properties.lagda
source/gist/InjectivesVersusAlgebras.lagda