the Kan extension seminar returns

the Kan extension seminar returns

[Emily Riehl]

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/ ]

Re: the Kan extension seminar returns

[1337777.OOO]

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