TODO

some minor fixes

a bit of work done while travelling to padova

- new notation.ma file with local and common notation
- o-bp have now a O as prefix, the same for o-cs
- BP_to_OBP proved to be a functor, not faitfull nor full (simply stated)

...

...

all pullbacks are attempted in sequence, removed many unfold

universe inconsistency fixed

SUBSETS_full up to universe inconsistency

faithful

CAT2

ceommented out metasenv

...

Sambin's result holds trivially since most of the fields of the objects of
the two categories are definitionally equal!

basic topologies are trivially o-basic topologies
the same for their morphisms

1. new coercion(s) from CPropi to CProp
2. fixed notation for subsetS
3. coercions still have problems: the coercion from objs1 REL is not
   accepted because it is identified with the coercion from objs1 SET

the new coercion behaviour (variants + composition with ID) and the new
discipline of declaring hints for carrier of structures (setoids and categories) and no
other hints simplified many passages

added notation for 'Vdash

if the user attempts to insert a duplicate coercions the system forbids it

unvariant also for coercions to funclass

- name mangling changed, added __ to separate additional number
- composing a coercion with an identity does not affect the body, and a variant is generated

no more universe inconsistency printed to stderr

coercions that are marked as variant are unfolded when inserted

Coercions graph is printed between real types and not approximated ones

o_continous_relations are really o_relation_pair... up to a bug of Matita
(a meta left in the metasenv :-(

o-basic_pairs are indeed examples of o-basic_topologies!
some more work is required to prove the same for morphisms

many changes regarding coercions:
- new `prefer coercion foo` command to reorder the list of coercions associated with a src >-> tgt pair
- rewritten coercions undoing mechanism
- coercion composition fixed (generates more coercions)
- librarySync rewritten, procedures to generate derived lemmas (eliminators, invertion lemmas, ...) are hooks registerd by other modules that can thus live anywhere (also in tactics/ like the one for inversion)
- manual fixed to talk about the new command
- coercions graph is drawn together with a list of coercions that makes their precedence visible (and can be altered with the prefer coercion command)
- dump-moo fixed to print coercions
- removed `Coercion attribute in XML files (YOU NEED TO RECOMPILE)

- Added new output in standard C.

Some work on o-algebras towards the proof that a and j are saturation/reduction
operators.

The new coercion from SET to Type0 with higher priority really helps a lot:
almost all explicit occurrences of carr have been removed.

more composites to make all happy!

eq over SET1 and SET no longer used

some more if/fi conversion due to the new . binding

unary_morphism_N : seoidN -> setoidN -> setoidN (was ... -> setoidN+1)
notation for . is now bound to fi instead of if (i.e. rewrites -> )

virtuals for () removed and bound to 'o'
memory changed, used similar symbols are presented first but not altering their original order

Just a snapshot.

coercions reordering implemented

updated

More work on concrete spaces.

Some work on concrete spaces.

Cool: only 8 universes in use.

1) Some reorganization.
2) Funny: the proof that basic_topologies are an example of o_basic_topology
   is immediate.

Some renaming to avoid confusion between saturations and o_saturations.

Fixing universe levels for saturations and (partially) basic_topologies.

The functor from BP to OBP has been defined (but no property proved yet).

Ok, even if not stated formally, now we know that the map from REL to OA is
a functor!

orelation_of_relation preserves equality and identities.

Basic pairs restored; require renaming to use them together with o-basic_pairs.

Some progress: everything works well now.

Ooops, I forgot to commit this in the previous 3-4 commits.

An hint moved to the right place.

No more daemons, no more exTs.

Great: some significant progress in fixing universe levels.

removing (only from the interface) functions related to ligatures that now live in the GUI

added help on virtuals and UTF-8 equivalence classes

expand ligatures after \n too

added := -> \def

added some memory to virtuals eq classes

...

1. CProp_n fixed to be equal to Type_n to better understand what is happening
   with universe levels
2. major proof step: I have proved (up to universe inconsistency :-( that
   every RELation induces an OA morphism. In particular, these means:
     A) having correctly defined the four images on subsets
     B) having proved the fundamental symmetry
     C) having proved the two fundamental adjunctions

Snapshot to try to understand something.

Some more progress, fighting universe inconsistencies.

Yet another universe problem :-(

...

Back to step 1: all files that used to pass now pass again.

More re-organization.

Basic pairs went through with no problems.

Universe level fixed (litterally).

Niceness was just a temporary illusion :-(

Much, much nicer now.

Some more re-organization.

More re-working.

More reorganization.

equivalence_relations made uniform w.r.t. universe level
However, there is still a bug related to universes, which I do not understand.

Final work for today.

removed duplicate notation

Some more painful work.

binary_meet is back again, with some effort

Many universe inconsistency avoided here and there.

The universe inconsistency comes from big union, that uses the existential.

Proof that \Omega \sup A is an overlap algebra, up to universe inconsistency :-(

o-algebra defined again

Categories and subsets compile again, hopefully with better universe levels.

WARNING: partial commit to try to understand something.
I have fixed the universes in categories, adding a new category (of level 2)
and trying to prove that powersets form a SET1.

Failing, so far.

Some more fixes. Boring and stupid!

Some fixes.

O-Basic Topologies do form a category.

A few more lines.

Some notes by Giovanni.

Some notes by Giovanni.

added some virtuals

bug fixed, all convertible was called without a metasenv

Just copied here from formal_topologies.ma.

More (ugly) work.

...

Beginning of o-basic_topologies.

Some clean up.

Concrete Spaces defined but... they require about 20m to type-check!

1 more lemma

one line