The Coq mailing list

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

Proph

https://github.com/1337777/chu/blob/master/chuSolution.v

solves some question of 楚 [fn:1] which is how to program contextual
limits of polymorph functors.

This angle of view is that limits are described by some logical
equalizers conditions onto some computational products data, which is
that the logical cone-condition onto the two computational
precone-morphisms data corresponds to the logical
containment-in-the-limit-subobject-of-the-product condition onto the
one computational pairing-morphism data.

Therefore oneself does not lack some very-complicated-induction scheme
(beyond induction-induction) on the whole limit. Instead oneself may
primo erase/extract some logical equalizers/cone-conditions by
assuming some erasure/extraction scheme as axiom, then secondo
dissolve by reformulating the with-cuts cone-conditions on the two
projections into some cut-free cone-condition on the single
projection, finally tertio resolve by cut-elimination into some
decidable only-congruence-style solution.

Moreover this decidability technique shall generalize to limits where
the indexing graph is finite or well-founded. Finally, memo that any
total-limit (general Kan extension) simply-axiomitize some bijection
property of multiple-limits ("pointwise" Kan extension) : (multiple
copairings <=> one contextual multiple-cone) , whose equational
formulation is similar to the equational formulation for the common
limits. Indeed this property says no-more-than some
commutation-of-polymorph-quantifiers bijection : (multiple
contextual-cones <=> one contextual multiple-cone). Therefore this
decidability technique shall generalize to Kan extensions.

[fn:1] ~楚~ 
[[https://github.com/1337777/chu/blob/master/ocic03-what-is-normal.djvu]]

-----

老子

https://github.com/1337777/gongji/blob/master/gongji.ml4

这 解决 《Coppel [fn:2]》的 一些 问题 ： 如何 编程 数学 入 计算机的 《公鸡》。

我 正在访着 复旦大学的《 IAS 》《 http://www.connes70.fudan.edu.cn/ 》, 从 3 月 23 日 到
4 月 7 日 : 有没有 一个人 能完成 这个 翻译 为 一个 真正的 非伪造 市场 吗？ 有没有 一个人 可以 澄清 之意义《 不再
几何的 证明 在几何 》对 计算机的 《 公鸡 》 吗？

例 :《
Add ML Path "./".
Declare ML Module "gongji".
Tactic Notation "同一" := reflexivity.

定义 d1 : nat := 5.

定义 三 : nat := 3.

引理 l1 : ( 若 true 回 nat 则 2 旁 1337 ) + 三 = d1.
  同一.
完毕.
 》

[fn:2] ~Coppel~ «A Chinese-English mathematics primer»
[[http://catalogue.nla.gov.au/Record/1337321]]

-----

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