The Coq mailing list

[1337 777 <1337777.ooo AT gmail.com>]

Proph Voevodsky

https://github.com/1337777/aigner/blob/master/aignerSolution.v

solves some question of Aigner [1] [2] which is how to program polymorph counting
modulo ("combinatorics", "groups"). Some finding is that the common encoding of
"cosets" as predicates is by chance/random and the reality is that "cosets" are
polymorph functors :

Variable V_ : forall (B : obB func) (A : obA func), obV log.
Variable f_ : forall B A, log.-V(0 V_ B A |- F[0 B ~> A ]0 )0.
Axiom Ax1 : forall (A A' : obA func) (g : log.-V(0 I |- A[0 A ~> A']0 )0),
      subarrow (F|1 A A' <o g) (f_ (F|0 A) A')
        -> forall (B : obB func), subarrow (f_ B A') (f_ B A o>`func` g).

The common definition of subgroup may require 3 closure axioms
( 1 \in G , x * y \in G , /_ y \in G ) , which may be erased to 2 closure
axioms ( 1 \in G , x * /_ y \in G ), which may be erased to 2 closure axioms
for finite groups ( 1 \in G , x * y \in G ) as in ssreflect [3]. This new
polymorph view is same as using these 2 closure axioms :
( 1 \in G , x \in G * y ), where now this right "coset" (G * y) is in reality
the action/composition arrow output (f_ B A o>`func` g) of the polymorh functor,
some <<coin>>. Some polymorph counting-modulo lemma (Cauchy) is possible ...

This solution also contains the programming of some logic of finite functions
and monotone functions, in the ssreflect style which is the programming of
specifications (reflections) for decidable predicates. This
logic-internalization of finite functions are sequences (in ssreflect:
{ffun aT -> rT}), such that extensional-equality of finite functions corresponds
to propositional equality of sequences. Monotone functions are quotient of
injective functions, therefore instead of manipulating predicates (the codomain)
in the old-style, one may hold monotone functions/arrows (monotone
sequences). Additionally Bauer-Cathlelay [9] may attempt to program the
enrichment-logic of the Dedekind real line for the ultrafilter monad ...

_____

This angle of view of polymorph groupoid action peut resoudre quelques questions
de Brown [4] ou Cisinski... et pourrait meme etre aussi critique que la
decouverte des <<schemas>> par Galois, puisqu'il est bien plus elegant, voire
indispensable pour y comprendre quelque chose de travailler avec des groupoides
fondamentaux par rapport a un paquet de points base convenable. De toutes les
choses de l'univers, j'ay decouvert un programme vaste et d'envergure, un
<<programme solution>> dont j'ay presente ici seulement une esquisse. Il
suffisait de voir de ses propres yeux et non avec des lunettes
brevetees. D'abord j'ay decouvert [5] que la tentative de deduction de la
coherence associative par Maclance n'est en fait pas la realite, puisque ce
fameux pentagone est en fait un carre recursif. Ensuite j'ay decouvert [6] que
les categories seulement-nommees par l'homologiste Maclane sont en fait le
polymorphisme naturel de la logique de Gentzen, ce qui permet une programmation
de la resolution congruente par elimination des coupures [7] qui servira de
technique de specification (reflection) pour semi-decider les questions de
coherence, en comparaison du style ssreflect. Ensuite j'ay decouvert [8] que
l'action de Galois pour la resolution modulo, est en fait une instance des
foncteurs polymorphes. La motivation est que les maths se font et se
communiquent dans un <<temps>> predit/deterministe (1337) et aussi dans un
<<moment>> aleatoire/random (777), sans la peur de jouer 100carats, alors la
question est : comment chercher un truc aleatoire ? ...

[1] Aigner ~Combinatorial Theory~ [[https://books.google.com/books?isbn=3642591019]]
[2] 1337777.OOO
[[https://github.com/1337777/aigner/blob/master/ocic04-where-is-combinatorics.pdf]]
[3] ~Mathematical Components~ [[https://math-comp.github.io/math-comp/]]
[4] Brown ~Topology and Groupoids~ [[http://www.groupoids.org.uk/]]
[5] 1337777.OOO [[https://github.com/1337777/dosen/blob/master/coherence2.v]]
[6] 1337777.OOO [[https://github.com/1337777/borceux/blob/master/borceuxSolution2.v]]
[7] 1337777.OOO [[https://github.com/1337777/dosen/blob/master/dosenSolution3.v]]
[8] 1337777.OOO [[https://github.com/1337777/aigner/blob/master/aignerSolution.v]]
[9] [[https://github.com/cathlelay/dedekind-reals]]