* the Kan extension seminar returns @ 2016-10-24 3:15 Emily Riehl [not found] ` <b1839da5-b0b2-a191-b66b-3adf9837b69d@gmail.com> 0 siblings, 1 reply; 2+ messages in thread From: Emily Riehl @ 2016-10-24 3:15 UTC (permalink / raw) To: categories In early 2014, the n-Category Café hosted the Kan Extension Seminar, a graduate reading course in category theory modeled after Daniel Kan’s eponymous reading course in algebraic topology at MIT. My experience with the seminar, described here: http://www.ams.org/notices/201411/rnoti-p1357.pdf <http://www.ams.org/notices/201411/rnoti-p1357.pdf> was overwhelming positive, so I’m delighted to announce that we’re back. Alexander Campbell, Brendan Fong, and I are organizing "Kan II" in early 2017 and we’re currently soliciting applications for seminar participants. Our plan is to read the following eight papers between mid January and mid May: * Hyland and Power, The category theoretic understanding of Universal Algebra: Lawvere Theories and Monads, * Freyd, Algebra valued functors in general and tensor products in particular * Beck, Distributive laws * Kelly, On the operads of J.P. May, * Kelly, Structures defined by finite limits in the enriched context, I * Kelly, On Clubs and Data-type Constructors * Lack and Rosicky, Notions of Lawvere Theory * Berger, Mellies, and Weber, Monads with arities and their associated theories We are seeking eight participants who will read and engage with all of the papers as well as prepare an oral presentation on one of them, followed by a blog post to be published on the n-Category Café. The course will conclude with a series of short public expository lectures given, by those able to attend, on July 16 in conjunction with the 2017 International Category Theory Conference at the University of British Columbia in Vancouver. More details, including information about how to apply, can be found on the seminar website: http://www.math.jhu.edu/~eriehl/kanII <http://www.math.jhu.edu/~eriehl/kanII> or by contacting any of the three of us. Applications are due November 30th. I hope you’ll help us spread the word by passing this message along to those who might be interested. On behalf of the organizers, Emily Riehl (eriehl@math.jhu.edu <mailto:eriehl@math.jhu.edu>) Alexander Campbell (alexanderpcampbell@gmail.com <mailto:alexanderpcampbell@gmail.com>) Brendan Fong (fo@seas.upenn.edu <mailto:fo@seas.upenn.edu>) — Assistant Professor, Dept. of Mathematics Johns Hopkins University www.math.jhu.edu/~eriehl [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 2+ messages in thread
[parent not found: <b1839da5-b0b2-a191-b66b-3adf9837b69d@gmail.com>]
* Re: the Kan extension seminar returns [not found] ` <b1839da5-b0b2-a191-b66b-3adf9837b69d@gmail.com> @ 2017-01-03 20:37 ` 1337777.OOO 0 siblings, 0 replies; 2+ messages in thread From: 1337777.OOO @ 2017-01-03 20:37 UTC (permalink / raw) To: johnm, Emily Riehl, categories, coq-club; +Cc: AVED.DeputyMinister 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 ^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2017-01-03 20:37 UTC | newest] Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2016-10-24 3:15 the Kan extension seminar returns Emily Riehl [not found] ` <b1839da5-b0b2-a191-b66b-3adf9837b69d@gmail.com> 2017-01-03 20:37 ` 1337777.OOO
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).