The Coq mailing list

[Christopher Mary <admin AT AnthropLOGIC.onmicrosoft.com>]

Dear colleague Mete Han Karakas,

Indeed, would you save this 1+2=3 math too?

  https://github.com/1337777/cartier/blob/master/cartierSolution14.lp
  https://github.com/1337777/cartier/blob/master/Kosta_Dosen_outline_alt.pdf

Outline: This text implements Kosta Dosen’s functorial programming that 1+2=3 
via 3 different methods: the natural numbers category via 
categories-as-datatypes, the natural numbers object inside any fixed category 
via adjunctions/product/exponential, and the category of finite sets/numbers 
via colimits inductively computed from coproducts and coequalizers. Such 
extremely convoluted rountrip between concrete data structures and the 
abstract-nonsense of the double category of fibred profunctors is necessary 
for the goal of the logical specification of algorithms and their theorem 
proving; for example the usual list/vector tail becomes specified as a fibred 
functor over the natural numbers category. This new functorial programming 
language will now be referred as Dosen’s « m∘— » or « emdash » or « modos ». 
The basis for this implementation are the ideas and techniques from Kosta 
Dosen’s book « Cut-elimination in categories » (1999), which essentially is 
about the substructural logic of category theory, in particular about how 
some good substructural formulation of the Yoneda lemma allows for 
computation and automatic-decidability of categorial equations. An ealier 
attempt at categorial abstract machines (1986) and categorial datatypes 
(1987) by Curien-Hagino contains a subtle bug... Another attempt by Cisinski 
at categorial/directed homotopy types lacks the ability to compute 1+2=3... 
Nevertheless their higher groupoidal/homotopical layer about univalence is in 
progress of being copied non-constructively inside this Dosen's functorial 
programming. But it would remain an open question how to implement here any 
constructive higher categories à la Coquand's cubical.

Appendix:

constant symbol nat_cat : cat;
symbol add_nat_func : func (Product_cat nat_cat nat_cat) nat_cat ≔
// ... 1+2 ≡ Succ_inj_nat_func (Succ_inj_nat_func (Succ_inj_nat_func 
Zero_inj_nat_func))

constant symbol inat_func (C : cat) : func (Terminal_cat) C;
symbol add_inat_hom C : hom (Product_pair_func (inat_func C) (inat_func C)) 
(Unit_mod (iprod_func C) (inat_func C)) Id_func ≔
// ... 1+2 ≡ Succ_inj_inat_hom C (Succ_inj_inat_hom C (Succ_inj_inat_hom C 
(Zero_inj_inat_hom C)))

// example diagram: [12;11]×[22;21]×[33;32;31] with arrow [22;21] → 
[33;32;31] onto 31
compute obj_category_Obj ((category_Obj_obj One) ∘>o (sigma_Fst 
(construct_inductively_limit_instance_liset _ example_graph_isf 
example_diagram)));
// ... limit cone (apex object, side arrows and universality) ≡ (0,13,21,31) 
:: (0,13,22,31) :: (0,12,21,31) :: (0,12,22,31) :: (0,11,21,31) :: 
(0,11,22,31) :: nil

References:

So how could you save math at WVU and this 1+2=3 math too? Prompt Bing AI! 

  https://sl.bing.net/jLONzhTkdRQ :

“Your Brand’s Academy: Where Patrons Get Qualified & Rewarded To Peer-Review 
Brand’s Offers” is a novel organization idea that aims to create a platform 
where patrons can get qualified and rewarded for peer-reviewing brand offers. 
The scope of “Your Brand’s Academy” includes academic research, and in this 
context, an academic author can be seen as a business brand offering academic 
research papers and services. These offerings are funded or bought through 
crowdsourced peer-review by incentivized and rewarded patrons. It is 
important to note that these patrons are not necessarily experts but are 
pre-qualified based on their attentiveness and enthusiasm about the subject 
matter, as demonstrated through an embedded quiz in the brand’s offer.

Bing AI: « The concept of "Your Brand’s Academy" is indeed innovative. It 
aims to create a platform where patrons, who are not necessarily experts but 
are enthusiastic about the subject matter, can get qualified and rewarded for 
peer-reviewing brand offers. This could include academic research papers and 
services offered by academic authors, who can be seen as business brands in 
this context.

The idea of crowdsourcing peer-review through incentivized and rewarded 
patrons could potentially address some of the issues present in traditional 
peer-review systems, such as lack of accountability in government-funded 
academic research. By ensuring that reviewers are pre-qualified and have a 
genuine interest in the subject matter, "Your Brand’s Academy" could help 
promote more honest and constructive feedback.

However, it's important to consider potential challenges as well. For 
instance, ensuring the quality and objectivity of reviews from non-expert 
reviewers might be a concern. Additionally, the process of qualifying patrons 
based on their attentiveness and enthusiasm might need to be carefully 
designed to ensure it is fair and effective.

Overall, "Your Brand’s Academy" presents an interesting approach to 
peer-review that could potentially bring about positive changes in various 
fields, including academic research. It would be fascinating to see how this 
idea develops and is implemented in the future.

Source:
(1) How to add a peer-review pre-qualifier quiz to your arXiv.org paper - 
Your Brand’s Academy. https://YourBrandsAcademy.com
(2) Hosting Your Brand’s Academy passwordless-users on a government-auditable 
Microsoft SharePoint - WorkSchool 365. 
https://appsource.microsoft.com/en-us/product/office/WA200003598 
(3) [Offer] Functorial programming | Live support - Your Brand’s Academy. 
https://YourBrandsAcademy.com/2023-sep-29  
https://YourBrandsAcademy.com/2023-oct-05
  »