Files

.github
admin-utilities
latex
source
- Apartness
- BinarySystems
- CantorSchroederBernstein
- Cardinals
- Categories
- Circle
- CoNaturals
- ContinuityAxiom
- Coslice
- CrossedModules
- DedekindReals
- DiscreteGraphicMonoids
- DomainTheory
- Dominance
- Duploids
- Dyadics
- DyadicsInductive
- EffectfulForcing
- Factorial
- Field
- Fin
- Games
- GamesExperimental
- Groups
- InfinitePigeon
- InjectiveTypes
- Integers
- Iterative
- Lifting
- Locales
- MGS
- MLTT
- MetricSpaces
  - DedekindReals.lagda
  - Rationals.lagda
  - Type.lagda
  - index.lagda
- Modal
- Naturals
- Notation
- NotionsOfDecidability
- OrderedTypes
- Ordinals
- PCF
- PathSequences
- Quotient
- Rationals
- Relations
- Slice
- TWA
- Taboos
- TypeTopology
- UF
- Unsafe
- Various
- W
- WildCategories
- gist
- AllModulesIndex.lagda
- index.lagda
.gitignore
CODE-OF-CONDUCT.md
CONTRIBUTING.md
LICENSE
README.md
STATEMENT-OF-INCLUSION.md
count-agda-files-and-lines
imports.sh
indexupdatecount
typetopology.agda-lib

MetricSpaces

remove some spaces

Feb 6, 2025

6767b85 · Feb 6, 2025

Name		Name	Last commit message	Last commit date
parent directory ..
DedekindReals.lagda		DedekindReals.lagda	Unused imports (#317 )	Sep 8, 2024
Rationals.lagda		Rationals.lagda	Unused imports (#317 )	Sep 8, 2024
Type.lagda		Type.lagda	remove some spaces	Feb 6, 2025
index.lagda		index.lagda	move --exact-split to the lib file (this is now possible because ther…	Nov 1, 2023