Top 40 imports in TypeTopology:
750 MLTT.Spartan
533 UF.FunExt
427 UF.Subsingletons
315 UF.Equiv
312 UF.PropTrunc
253 UF.Base
201 UF.Subsingletons-FunExt
185 UF.SubtypeClassifier
170 UF.Sets
137 UF.Univalence
129 UF.EquivalenceExamples
118 UF.DiscreteAndSeparated
116 UF.Size
111 UF.Embeddings
102 UF.Logic
93 UF.UA-FunExt
87 Notation.Order
83 Locales.Frame
82 UF.Sets-Properties
82 UF.Retracts
78 DomainTheory.Basics.Dcpo
70 Naturals.Order
70 MLTT.Two-Properties
65 UF.ImageAndSurjection
62 MLTT.Plus-Properties
59 Notation.CanonicalMap
57 UF.ClassicalLogic
56 Slice.Family
53 Ordinals.Type
53 MLTT.List
49 UF.Subsingletons-Properties
49 Ordinals.Underlying
48 UF.Equiv-FunExt
46 Naturals.Properties
45 DomainTheory.Basics.Miscelanea
44 Naturals.Addition
42 UF.Powerset
41 DomainTheory.Basics.Pointed
41 CoNaturals.Type
