The Coq mailing list

["1337777.OOO" <1337777.ooo AT gmail.com>]

Proph

https://github.com/1337777/laozi/blob/master/laoziSolution2.v

solves some question of LAOZI [fn:1] which is how to program polymorph
coparametrism functors ( "comonad" ) ... Whatever is discovered, its
format, its communication is simultaneously some predictable logical
discovery and some random dia-para-logical discovery.

In particular this text programs the grammatical / inductive
(therefore free) description of polymorph coparametrism functor and
the conversion relations over the generated morphisms. This text is
based on earlier texts which describe functional-monoidal logic and
the decidable coherence of this logic.

Next this text programs the iterated comultiplication (DeClassifying)
and the corresponding deduced conversion relations over the morphisms.
Then the reduction relation and degradation lemmas are programmed and
deduced.

Finally the solution morphisms are programmed with their
(dependent-)destruction lemmas such to inner-instantiate the
object-indices. And the (non-congruent) resolution by cut elimination
/ desintegration technique is programmed and deduced : this deduction
is mostly-automated.

For instant first impression, the common saying that the counit
inner-cancels the comultiplication is written as :

#+BEGIN_EXAMPLE
| IterCancelInner :
    forall {trf : obV log -> obV log}
      (Vb Vb' : obV log) (vb : V(0 Vb' |- Vb )0)
      (W W_dft : obV log) (V0Vb' : obV log) (Vs : list (obV log))
      (vs : (hlist (toArrowV (trf:=trf)) (chain Vs)))
      (va : V(0 trf(last W_dft Vs) |- W )0)
      (v0b : V(0 V0Vb' |- (0 trf(head W_dft Vs) & Vb' )0 )0)
      (B : obMod) (A : obMod) (b : 'D(0 Vb |- [0 B ~> A ]0 )0)
      (A' : obMod)(a : 'D(0 W |- [0 A ~> A' ]0 )0),
      ( v0b o>| ( vb o>' b)  o>D (iterDeClassifying (V_dft := W_dft)
vs ( va o>' a)) )
        <~~ ( v0b o>| (vb o>| b o>Mod 'declfy )
                o>D (iterDeClassifying (V_dft := W_dft) vs (va o>|
'clfy o>Mod a) )
            : 'D(0 V0Vb' |- [0 B ~> 'D0| (iterDeClass0 (length Vs).-1 A') 
]0)0 )
#+END_EXAMPLE

Outline :

  * Grammatical description of polymorph coparametrism functor
  ** Importing the functional-monoidal logic
  ** Base generating graph
  ** Grammatical generation of the morhisms
  ** Decoding into the common sense : grammatical is indeed free
  ** Some notations
  ** More functional-monoidal logic
  ** The generated conversion relations over the morphisms

  * Iterated constructors
  ** Indexed list, lemmas
  ** Chained lists, lemmas
  ** Iterated constructors

  * Grade

  * Reduction
  ** Grammatical generation of the reduction relation
  ** Degradation lemmas

  * Solution
  ** Grammatical generation of the solution morphisms
  ** Containment of the solution morphisms into all the morphisms
  ** Destruction of morphisms with inner-instantiation of object-indices
  ** Iterated =DeClassifying= prefix

  * Resolution

Reviews :

[fn:1] ~1337777.OOO~
[[https://github.com/1337777/laozi/blob/master/laoziSolution2.v]]

-----

May some additional empty-rooms in the public UBC campus have their
doors unlocked during July 15 for the public 1337777 School ?

The public 1337777 School is seeking ministerial-review-and-payments
as school for the public, comparable to
https://team.inria.fr/marelle/coq-winter-school-2017/ . Such 1337777
School shall truly hold the motivation of maximizing the mathematical
memory and sensibility of each  and all of the public, contrary to the
common falsification of the other ministerial-reports which in reality
have none such motivation and even may sans-detours elect-by-random
...

paypal 
1337777.OOO AT gmail.com
 , wechatpay 
2796386464 AT qq.com
 , irc #OOO1337777