From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9479 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: [TYPES/announce] Tenure-Track Research and Teaching Positions at University of British Columbia, Vancouver, Canada Date: Sun, 31 Dec 2017 20:37:07 +0800 Message-ID: References: <8CD7DB5F-B95E-4FBA-B93E-0AAFB99ABDE9@cs.ubc.ca> Reply-To: coq-club@inria.fr NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Trace: blaine.gmane.org 1514723753 12058 195.159.176.226 (31 Dec 2017 12:35:53 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Sun, 31 Dec 2017 12:35:53 +0000 (UTC) To: Ronald Garcia , types-list@lists.seas.upenn.edu, coq-club@inria.fr, categories@mta.ca Original-X-From: coq-club-owner@inria.fr Sun Dec 31 13:35:48 2017 Return-path: Envelope-to: gsmlcc-coq-club@gmane.org Original-Received: from mxfilter-048035.atla03.us.yomura.com ([107.189.48.35]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1eVcq0-0002BO-0L for gsmlcc-coq-club@gmane.org; Sun, 31 Dec 2017 13:35:36 +0100 X-Yomura-MXScrub: 1.0 Original-Received: from mail2-relais-roc.national.inria.fr (unknown [192.134.164.83]) by mxfilter-048035.atla03.us.yomura.com (Halon) with ESMTPS id 53ff9533-ee27-11e7-94e8-b499baabecb2; Sun, 31 Dec 2017 12:37:14 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.45,486,1508796000"; d="scan'208";a="307258701" Original-Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 31 Dec 2017 13:37:13 +0100 Original-Received: by sympa.inria.fr (Postfix, from userid 20132) id 69C3B823B6; Sun, 31 Dec 2017 13:37:13 +0100 (CET) Original-Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id B265182355 for ; Sun, 31 Dec 2017 13:37:11 +0100 (CET) Authentication-Results: mail3-smtp-sop.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-it0-f65.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AmYc+FRHIQCqOpJ/mA3zePJ1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ7yp8SwAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+?= =?us-ascii?q?NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjD?= =?us-ascii?q?QhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj?= =?us-ascii?q?8KODw38G/XhMJ+j79Vrgy9qBJw2IPUfJiVOeBicq/BYd8XR2xMVdtRWSxbBYO8?= =?us-ascii?q?apMCA+QcMetWoYTwpVkDoBm8CAW2He3h0yZGinHr1qA9zugsHw/L0Q4iEt8Msn?= =?us-ascii?q?nYttL1NKAVUe2uw6nIyC/Mb/JS2Tvn9IfIdRUhrOiKULltf8TRzkwvGBnEjlWW?= =?us-ascii?q?sYHlJyma1+QVs2eB6+psT+evhHA/pw5rpzig3MYtio7Pho4P1l/E8iB5zJ46Jd?= =?us-ascii?q?25VE57YcOkH4BKuy6GMIt2R9suQmFvuCYn1r0GpIW0czYQxJs7wB7fbuSLc4eJ?= =?us-ascii?q?4hL/SumePy10i25ieL X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CgAABC2Uhaf0HWVdFcAQIIAgEMAQEBA?= =?us-ascii?q?QECAQEBAQgBAQEBghiBTQE+dCcHhACZO4t+jmMDXAojhElPAkqDXwdDFAEBAQE?= =?us-ascii?q?BAQEBAQESAQEJCwsIJjGCOCKCSgMDIx0BGwUFDAgDDAYDAgsDAgMHAh8HAgIiA?= =?us-ascii?q?REBBQEcBgEJCRYFiXoBAxUQjC2RHUCMEIIFBQEcgwsFg1gKGScNDSErghcBAQE?= =?us-ascii?q?BBgEBAQEBAQEZAgYSfYJ9ghKBVoRlMoIMgSMBGIFWgxeCZQWTMZAaAQKIAY0yg?= =?us-ascii?q?nyRAY0kiUsUBSCBFzaBcW+BBIF3CQqCMg8cGYEPTDQ3hlAEgkYBAQE?= X-IPAS-Result: =?us-ascii?q?A0CgAABC2Uhaf0HWVdFcAQIIAgEMAQEBAQECAQEBAQgBAQE?= =?us-ascii?q?BghiBTQE+dCcHhACZO4t+jmMDXAojhElPAkqDXwdDFAEBAQEBAQEBAQESAQEJC?= =?us-ascii?q?wsIJjGCOCKCSgMDIx0BGwUFDAgDDAYDAgsDAgMHAh8HAgIiAREBBQEcBgEJCRY?= =?us-ascii?q?FiXoBAxUQjC2RHUCMEIIFBQEcgwsFg1gKGScNDSErghcBAQEBBgEBAQEBAQEZA?= =?us-ascii?q?gYSfYJ9ghKBVoRlMoIMgSMBGIFWgxeCZQWTMZAaAQKIAY0ygnyRAY0kiUsUBSC?= =?us-ascii?q?BFzaBcW+BBIF3CQqCMg8cGYEPTDQ3hlAEgkYBAQE?= X-IronPort-AV: E=Sophos;i="5.45,486,1508796000"; d="scan'208";a="249772355" Original-Received: from mail-it0-f65.google.com ([209.85.214.65]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 31 Dec 2017 13:37:10 +0100 Original-Received: by mail-it0-f65.google.com with SMTP id f190so35435888ita.5 for ; Sun, 31 Dec 2017 04:37:10 -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 :content-transfer-encoding; bh=hFP/mmLpIl0uVlAyblfTD4tfRPARxFVq9xhxY980jCM=; b=HurUPd2xzr0vXFBfdmgZ2VP+zRqQUMNJm0oNruE7lLKIoJzgMyo33BL3qESlNGZglV WXpwCKXQnH2fva/Sp8iOZtYEBnUgJ+OXu7Xi4MlmDfO8m/fUhrXW8xaM+UbYeI39UMlV 0z1TCo/8ZP/Qt4SCzwUjmjCbV1/eJ/Zh9Fx7GiYN/R4SrxXsXJqr92YGrUHw5YmaUoQ5 1fJP0qDaaZLTmzyWIKhTzINPY1AI8p1z0VOT5r7aRKfa03+NrxYoMd2Y8ROakNkGl85t XhNsxK9b1ZahBRzlGwTncos7z9+3XGEnNOjIyRy1jjAnWd1orfos6ZcnyHri7wWl3ywM Itsw== 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:content-transfer-encoding; bh=hFP/mmLpIl0uVlAyblfTD4tfRPARxFVq9xhxY980jCM=; b=t3WwmQl+iGZ1BBWOZTsoBmSxe0jh35V6WoJC5ILXKW6PLzIh19cpQf3qXwFptDVnht aRXjeXqP9mX4lpa7pvAn1YE+tNho9LLMFWV7B2UFJB5SgcF2ksSQufylFdWE9yceMmEr pwrNXpc27iYQ2gIApxiuwLQSklXknbwS4kTOutqe4HPmZYzhtubNx2KF65zEITU+DInH RajtumxTaSA6k9AsjsozaIOIz1ZD53me7mTZJXykvCcKm8ZZE2d983x5LYhMowtanX26 fQSOukMhTpWD+HvZv4FEkgPK1gRWAWymHT9jYiCdDI9dhw6OnN+Q9CMfzDmqIHprRLal IXqw== X-Gm-Message-State: AKGB3mJlRx2M1XM0s//wnWwwwyrIfY7AjXR096vfT9jOqGeq6aGe2ESw KV09NKofTim6X9yZXYGTWcj2sLF40/serdZ4IjA= X-Google-Smtp-Source: ACJfBovSoU5SOd3cryELh44LiSDSiNaFUVsmWFPTBBn3gizQ8uLZJuZUctg8MF4z5MVNuFdfFE9zLDGPuJdHED/JwkM= X-Received: by 10.36.73.9 with SMTP id z9mr53362577ita.36.1514723828142; Sun, 31 Dec 2017 04:37:08 -0800 (PST) Original-Received: by 10.2.37.197 with HTTP; Sun, 31 Dec 2017 04:37:07 -0800 (PST) In-Reply-To: <8CD7DB5F-B95E-4FBA-B93E-0AAFB99ABDE9@cs.ubc.ca> X-Loop: coq-club@inria.fr X-Sequence: 15596 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: 2018-01-14 Xref: news.gmane.org gmane.science.mathematics.logic.coq.club:20100 gmane.science.mathematics.categories:9479 Archived-At: Proph https://gitee.com/OOO1337777/cartier/blob/master/cartierSolution3.v solves half of some question of Cartier which is how to program grammatical polymorph metafunctors-full-subcategory containing-equalizers generated by some views ( "complete" ) ... The ends is to start from some generating/views data and then to add equalizers of morphisms ; but where are those equalizers ? Oneself could get them as metafunctors on this generating data, as long as oneself grammatically distinguishes whatever-is-interesting . In contrast from the earlier grammatical presentation of pairing-projections (product), now the equalizer-objects do depend on the morphisms . BUT THIS DEPENDENCE NEED-NOT BE GRAMMATICAL ! This dependence could be expressed via the sense-decoding ( "Yoneda" ) of the grammatical morphisms . The grammatical objects/morphisms are simultaneously-mutually presented with their sense-decoding ; this could be done via some common inductive-recursive presentation or alternatively by inferring the sense-decoding computation into extra indexes of the type-family of the object/morphisms . The conversion-relation shall convert across two morphisms whose sense-decoding indexes are not syntactically/grammatically-the-same. But oneself does show that, by logical-deduction, these two sense-decoding are indeed propositionally equal ( "soundness lemma" ) . Finally, some linear total/asymptotic grade is defined on the morphisms and the tactics-automated degradation lemma shows that each of the conversion indeed degrades the redex morphism . For instant first impression , the conversion-relation constructor which says that the inclusion/restriction (projection) morphisms cancels the corestriction (pairing) morphism , is written as : #+BEGIN_EXAMPLE | Pairing_Project1 : forall Yoneda00_L Yoneda01_L (L : @obCoMod Yoneda00_L Yoneda01_L) Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F) Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G), forall Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )= 0) Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0), forall Yoneda10_ff (ff : 'CoMod(0 L ~> F @ Yoneda10_ff )0), forall (Yoneda10_ff_eq : forall A : obIndexer, proj1_sig Yoneda10_transfL A \o proj1_sig Yoneda10_ff A =3D1 proj1_sig Yoneda10_transfR A \o proj1_sig Yoneda10_ff A), forall ( _transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0 ) ( _transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0 ) Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z) Yoneda10_zz (zz : 'CoMod(0 F ~> Z @ Yoneda10_zz )0), ( ( ff o>CoMod zz ) : 'CoMod(0 L ~> Z @ Yoneda10_PolyCoMod Yoneda10_ff Yoneda10_zz )0 ) <~~ ( ( ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> ) o>CoMod ( ~_1 @ _transfL , _transfR o>CoMod zz ) ) : 'CoMod(0 L ~> Z @ Yoneda10_PolyCoMod (Yoneda10_Pairing Yoneda10_f= f_eq) (Yoneda10_Project1 Yoneda10_transfL Yoneda10_transfR Yoneda10_zz)= )0 ) #+END_EXAMPLE KEYWORDS : 1337777.OOO ; COQ ; cut-elimination ; equalizers ; polymorph metafunctors-grammar ; modos OUTLINE : * Generating-views data * Grammatical presentation of objects and morphisms , with sense-decoding as metafunctors and metatransformations ** Grammatical presentation of objects ** Grammatical presentation of morphisms * Grammatical conversions of morphisms , which infer the same sense-decod= ing ** Grammatical conversions of morphisms ** Same sense-decoding for convertible morphisms ** Linear total/asymptotic grade and the degradation lemma * Solution ** Solution morphisms without polymorphism ** Destruction of morphisms with inner-instantiation of object-indexes * Polymorphism/cut-elimination by computational/total/asymptotic/reduction/(multi-step) resolution ----- EPILOGUE : Now there is enough data (for multiple masters-engineering) to confirm the presence of some MODOS grammar, which is some style of "substructural topos" ... where oneself could present grammatical polymorph views-data ( "sheaves" ) , grammatical polymorph generating-views ( "presentable category" ) , grammatical polymorph internal functors ( "internal category" ) , grammatical polymorph images ( "regular category" ) , grammatical polymorph unions ( "coherent category" ) ... ----- Memo ( "prealables d'un debat" ) ref the unavoidable question : what is the ends / added-value / product in mathematics ? The ends are commonly described as research , which is the engineering of some computational logical computer program or physical prototype ( "correct" ) , and education , which is the knowing-and-teaching of random-moment dia-para-computalogical discoveries ( "ideas" ) . But where is the money/pay ? Surprisingly even persons capable of very complex mathematics can "bug" ( forced-fool-and-theft/lie/falsification ) on such small questions ... reacting with completely pre-formated one-liners . - whether public review of mathematical-ends is some unlimited creation of resource/money/pay ? ( for example , https://github.com/1337777/cartier/issues ) - whether public-university registered-students shall have public choice of who is their paid-teachers and where is their paid classroom/videostream/book ? ( for example , https://www.youtube.com/watch?v=3DBhWHxiqQzrI&t=3D26m11s ) - whether if 99% of transfer of value occurs via information-knowledge then for sure 99% of theft occurs via information-knowledge ? ( for example , promotion/publisher by some interdependent-tribalistic hidden "reviewer" is qualifiable as misappropriation of public funds ) ... or is ubc not public ? ----- BUY RECURSIVE T-SQUARE paypal.me/1337777 ; =E5=BE=AE=E4=BF=A1=E6=94=AF=E4= =BB=98 2796386464@qq.com ; eth 0x54810dcb93b37DBE874694407f78959Fa222D920 ; amazon amazon.com/hz/wishlist/ls/28SN02HR4EB8W ; irc #OOO1337777