TN
Size: a a a
2020 April 28
2020 April 30
TN
7 pages HoTT-I
2020 May 04
2020 May 06
TN
Для студентов 4-го года обучения две книги
TN
Эти две книги достаточно чтобы: читать SGA 4, приравнивать мотивные и этальные когомологии, читать работы Воеводского, заниматься А^1-теорий гомотопий и т.д. Ну и подборку про модальные категории, но она не готова, лучше читать те работы, где они применяются, там они аксиоматизируются всегда как пререквизиты.
2020 May 19
AN
Thorsten Altenkirch (University of Nottingham): Coinduction in Agda
https://www.youtube.com/watch?v=-fhaZvgDaZk
https://www.youtube.com/watch?v=-fhaZvgDaZk
TN
where is bisimulation proof ? :-)
TN
No proof No coinduction :-)
TN
Altenkirch, McBride -- вторая культура
TN
-- Bisimilarity is equal to equality.
bisimilarityIsPath
(A: U) (xs ys: stream A) :
Path U (Bisimilar A xs ys) (Path (stream A) xs ys) =
isoPath (Bisimilar A xs ys)
(Path (stream A) xs ys)
(bisimilarityToPath A xs ys)
(PathToBisimilarity A xs ys)
(idToId A xs ys)
(bisimilarityToBisimilarity A xs ys)
bisimilarityIsPath
(A: U) (xs ys: stream A) :
Path U (Bisimilar A xs ys) (Path (stream A) xs ys) =
isoPath (Bisimilar A xs ys)
(Path (stream A) xs ys)
(bisimilarityToPath A xs ys)
(PathToBisimilarity A xs ys)
(idToId A xs ys)
(bisimilarityToBisimilarity A xs ys)
TN
вот основная теорема коиндукции
TN
один undefined осталось закрыть
TN
кто закроет ПЕРВЫЙ тому 100 баксов!