From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9065 Path: news.gmane.org!.POSTED!not-for-mail From: "1337777.OOO" <1337777.ooo@gmail.com> Newsgroups: gmane.science.mathematics.logic.coq.club,gmane.science.mathematics.categories Subject: Re: the Kan extension seminar returns Date: Tue, 3 Jan 2017 15:37:38 -0500 Message-ID: References: Reply-To: coq-club@inria.fr NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 X-Trace: blaine.gmane.org 1483475870 30977 195.159.176.226 (3 Jan 2017 20:37:50 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Tue, 3 Jan 2017 20:37:50 +0000 (UTC) Cc: AVED.DeputyMinister@gov.bc.ca To: johnm@math.ubc.ca, Emily Riehl , categories@mta.ca, coq-club@inria.fr Original-X-From: coq-club-owner@inria.fr Tue Jan 03 21:37:43 2017 Return-path: Envelope-to: gsmlcc-coq-club@gmane.org Original-Received: from mail2-relais-roc.national.inria.fr ([192.134.164.83]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1cOVq2-00079u-MY for gsmlcc-coq-club@gmane.org; Tue, 03 Jan 2017 21:37:42 +0100 X-IronPort-AV: E=Sophos;i="5.33,456,1477954800"; d="scan'208";a="252732569" Original-Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 03 Jan 2017 21:37:45 +0100 Original-Received: by sympa.inria.fr (Postfix, from userid 20132) id CB015800B9; Tue, 3 Jan 2017 21:37:45 +0100 (CET) Original-Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 8F5AD800B6 for ; Tue, 3 Jan 2017 21:37:41 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=1337777.ooo@gmail.com; spf=Pass smtp.mailfrom=1337777.ooo@gmail.com; spf=None smtp.helo=postmaster@mail-oi0-f67.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AAFrekRwXWXnPBSzXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?0ewfIJqq85mqBkHD//Il1AaPBtSHrasfwLON4+igATVGusnR9ihaMdRlbFwst4?= =?us-ascii?q?Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVIm?= =?us-ascii?q?bsy8IIPZjty22uau4NWTJlwQ3HvuKY91eRexrQPUnswfnYskN6w6jBDA5jNlfu?= =?us-ascii?q?VS1CtSJF+Tm16o692x8Z5n2yFZp/Jn9c5dF6j2YvJ8BbdREDkpNHo06dbDsAXK?= =?us-ascii?q?CwCGojMXVXxTmR5VCSDE6gv7V9H/qHjUrO14jWPDZpapEu9rHxOFyO0jHEaz03?= =?us-ascii?q?hYaGF/92bQosN1haNf5hmmokoskMbvfIiJOa8mLevmdtQASD8EB54JWg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BpAQCQCmxYbEPaVdFeDg8BBQELARgGD?= =?us-ascii?q?IIWdwEBAQEBHyEBPYEMB7k6KoV4AoFFB0MQAQEBAQEBAQEBAQESCwsLBx8wgjM?= =?us-ascii?q?EARUBBIIXBiMEGQEbFgcBAwwGBQsPAiYCAiEBAREBBQEcBgESCBOIOQEDGA6ic?= =?us-ascii?q?j+MAoFrGAUBHIMJBYNjChknDQ0gJ4IQAQEBAQEBAQEBAQEBAQEBAQEBGAIBBRJ?= =?us-ascii?q?5hTqDdG2CToR8gl0BBJACikY0AQGGU4Zxg3mQVYlzhwQUHoEUNoF5EoNCgU5ZI?= =?us-ascii?q?DSGAQRqgU8BAQE?= X-IPAS-Result: =?us-ascii?q?A0BpAQCQCmxYbEPaVdFeDg8BBQELARgGDIIWdwEBAQEBHyE?= =?us-ascii?q?BPYEMB7k6KoV4AoFFB0MQAQEBAQEBAQEBAQESCwsLBx8wgjMEARUBBIIXBiMEG?= =?us-ascii?q?QEbFgcBAwwGBQsPAiYCAiEBAREBBQEcBgESCBOIOQEDGA6icj+MAoFrGAUBHIM?= =?us-ascii?q?JBYNjChknDQ0gJ4IQAQEBAQEBAQEBAQEBAQEBAQEBGAIBBRJ5hTqDdG2CToR8g?= =?us-ascii?q?l0BBJACikY0AQGGU4Zxg3mQVYlzhwQUHoEUNoF5EoNCgU5ZIDSGAQRqgU8BAQE?= X-IronPort-AV: E=Sophos;i="5.33,456,1477954800"; d="scan'208";a="252732557" Original-Received: from mail-oi0-f67.google.com ([209.85.218.67]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 03 Jan 2017 21:37:40 +0100 Original-Received: by mail-oi0-f67.google.com with SMTP id f201so71959342oib.0 for ; Tue, 03 Jan 2017 12:37:40 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=4xwquLgEog/SqUApGJIvhOmE1paeALHCBCNvCWzBlKg=; b=SxdBh3J95kk+a6VwgWAt9CgmKiyjrYm/Tz0U3b358SZ8z6sIoRSDCNkko95CQd8t9D FJL8olJNUWg+acAHE7lXqiMrJ2AXumw2IKFzZ0kxCJzCovefZ5WT8kwAS/jXaRRYjAn/ MqsNl7M1DV9tcrRDuewY1j4Bb03oWmkSlaPFVvR9+WuvrC6cpmAEl6yII2uWL0YwiyKL 9IAdzc6Lxo4TsJkxPQFHUQdmsgIhm3zZutRrW0ux03p8y4h2HwJqFOUqur3qEJfXexVf IuTdiaZhRaS6mzef4hvFpnziF8Pbna5fhRendIBZ+av42H+WzLDA6/XhcHUzJ5+Wx3oe FXYA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=4xwquLgEog/SqUApGJIvhOmE1paeALHCBCNvCWzBlKg=; b=Rq+Vgta1RiJVzB4ZXtjbcqJZ1EqwKU+t08WYWsmll5ONtDc51ZDm7v86MY74xetV/k UVTyYwEDWD04NUf9GPrLwrHIyZOFAP6j8OLToxl7eiJn5kzmOmRB3k60Q/ZEhqF11IOy KuwdcJfR1nCy1DzIzL5IXSDd4i/U1GENsrs/5e66/bWwYtGdQQJV0wcoknvmzD6CKqzx zCZ8k7p5HKKnE8SU2M3y6hVxLxz6ZvJzxX8hlIE9RlR8ktls5NLyhJQuCHQ3Tyv2Slxa LWDN/2CHjxqT0GTZROGiykJcvqqDjTHcJ5krFruvZrZUqdynZzfSDY+9TpaL8H7axmoN yIAw== X-Gm-Message-State: AIkVDXJ5HamgJClXXq52qSbx+QWYQ/aVJHxrnAm64MOfeI2tnMrU4WNUsa0/K5POJb6rlIMI7OqPQ0ivRIj2jw== X-Received: by 10.157.16.16 with SMTP id h16mr33787129ote.40.1483475858726; Tue, 03 Jan 2017 12:37:38 -0800 (PST) Original-Received: by 10.202.8.67 with HTTP; Tue, 3 Jan 2017 12:37:38 -0800 (PST) In-Reply-To: X-Loop: coq-club@inria.fr X-Sequence: 14246 Errors-to: coq-club-owner@inria.fr Precedence: list Precedence: bulk Original-Sender: coq-club-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: X-Gmane-Expiry: 2017-01-17 Xref: news.gmane.org gmane.science.mathematics.logic.coq.club:18739 gmane.science.mathematics.categories:9065 Archived-At: 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@gmail.com , wechatpay 2796386464@qq.com , irc #OOO1337777