Begin working on Hartogs numbers

coq-community / topology

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

Other

46 stars 10 forks source link

Begin working on Hartogs numbers #24

Closed Columbus240 closed 3 years ago

Columbus240 commented 3 years ago

Also:

Enable universe polymorphism, because otherwise some statements can’t be made.
Introduce the type [WO] of well-orders. This simplifies notation.

There are some holes that need to be filled in the proofs.

Related to issue #22

Columbus240 commented 3 years ago

I abandon this branch. The usual ordinal constructions of set-theory are hard to reproduce in type-theory. Universe conflicts etc. also make it hard to work with. Maybe I first have to study ordinals in ETCS or similar, before retrying the Hartog construction. I'll describe the long line differently.