Some facts and definitions about extensionality
We investigate the relations between the following extensionality principles
- Functional extensionality
- Equality of projections from diagonal
- Unicity of inverse bijections
- Bijectivity of bijective composition
Table of contents
1. Definitions
2. Functional extensionality <-> Equality of projections from diagonal
3. Functional extensionality <-> Unicity of inverse bijections
4. Functional extensionality <-> Bijectivity of bijective composition