Телеграмм чат группы groupoid страница 3

Size: a a a

groupoid.space

72 membersпожаловаться на группу

2017 November 15

Tonpa Namdak in groupoid.space

ISOMORPHISMS BETWEEN LEFT AND RIGHT ADJOINTS
http://www.math.uchicago.edu/~may/PAPERS/FormalFinalMarch.pdf

источник

04:08пожаловаться #1

Tonpa Namdak in groupoid.space

Small Induction Recursion. P. Hancock, C. McBride, N. Ghani, L. Malatesta, T. Altenkirch
http://www.cs.nott.ac.uk/~psztxa/publ/tlca13-small-ir.pdf

источник

04:09пожаловаться #2

Tonpa Namdak in groupoid.space

Жао Хуй Луо. ECC. Extendent Calculus of Constructions.
http://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-118/ECS-LFCS-90-118.pdf

источник

04:11пожаловаться #3

Tonpa Namdak in groupoid.space

Calculus of Inductive Constructions, PTS
http://www4.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf

источник

04:12пожаловаться #4

Tonpa Namdak in groupoid.space

Histo- and Dynamorphisms Revisited, Ralf Hinze Nicolas Wu
http://www.cs.ox.ac.uk/people/nicolas.wu/publications/Histomorphisms.pdf

источник

04:13пожаловаться #5

Tonpa Namdak in groupoid.space

Equality is typable in Semi-Full Pure Type Systems
http://pauillac.inria.fr/~herbelin/articles/lics-SilHer10-pts-typed-conv.pdf

источник

04:13пожаловаться #6

Tonpa Namdak in groupoid.space

Pure Type Systems without Explicit Contexts, Herman Geuvers
http://robbertkrebbers.nl/research/articles/gammainf.pdf

источник

04:13пожаловаться #7

Tonpa Namdak in groupoid.space

A Syntactical Approach to Weak ω-Groupoids
http://www.cs.nott.ac.uk/~psztxa/publ/weakomega2.pdf

источник

04:14пожаловаться #8

Tonpa Namdak in groupoid.space

TYPE THEORY AND HOMOTOPY. STEVE AWODEY
https://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf

источник

04:17пожаловаться #9

Tonpa Namdak in groupoid.space

Cubical Homotopy Type Theory. Steve Awodey CMU
http://www.helsinki.fi/lc2015/materials/slides_awodey.pdf

источник

04:17пожаловаться #10

2017 November 17

ID:402926333 in groupoid.space

лучше меньше ненужных лемм в глобальном пространстве

источник

01:43пожаловаться #11

ID:402926333 in groupoid.space

т.е. они были глобальными но использовались в 1 месте

источник

01:44пожаловаться #12

ID:402926333 in groupoid.space

мы пока не знаем какие леммы нужны а какие нет, в этом плане сигма из 2 полезных функций легче для понимания чем лапша из лемм которые всё равно просто имплементейшон детейлс

источник

01:45пожаловаться #13

Tonpa Namdak in groupoid.space

now I see your point!

источник

01:45пожаловаться #14

ID:402926333 in groupoid.space

sig2propeq кстати это просто пример как pathSig3 юзать

источник

01:46пожаловаться #15

Tonpa Namdak in groupoid.space

а как тогда на счет перенести pathSig2 и pathSig в sigma_neo ?