TN
Size: a a a
2021 June 05
2021 June 07
TN
UTF-8 in lstlisting
2021 June 08
TN
чето звезд маловато, ребята ну в самом деле 😊
2021 June 14
TN
Новости микрокубика:
def NonFibrant : V := I
def lower : V₁₁₂₁₂ := V₁₁₂₁₁
У нас еще пока нет Кан операций, только отрезок с алгеброй де Моргана, но зато в отличии от Агды, у нас есть свои вселенные Vₙ для non-fibrant претипов (так как нужно, а не так как в Агде).
def NonFibrant : V := I
def lower : V₁₁₂₁₂ := V₁₁₂₁₁
У нас еще пока нет Кан операций, только отрезок с алгеброй де Моргана, но зато в отличии от Агды, у нас есть свои вселенные Vₙ для non-fibrant претипов (так как нужно, а не так как в Агде).
TN
def hmtpy (A : U) (x y : A) (p : Path A x y) :
Path (Path A x x) (<_> x) (<i> p @ i /\ -i) :=
<j i> p @ j /\ i /\ -i
Path (Path A x x) (<_> x) (<i> p @ i /\ -i) :=
<j i> p @ j /\ i /\ -i
TN
Следующий шаг — Операции Кана на пустых системах, для полного встраивания MLTT, самая минимальная кубическая система.
2021 June 15
TN
TN
ее блог: https://abby.how/
2021 July 02
2021 July 05
TN
MLTT Internalization:
1) cubicatt/hcomptrans: 4.5s
2) anders: 0.04 s
N3000 church unfold:
1) cubicaltt/hcomptrans: 2.3 s
2) anders: 1.9 s
Functor category:
1) cubicaltt/hcomptrans: 2.6 s
2) anders: 0.4 s
1) cubicatt/hcomptrans: 4.5s
2) anders: 0.04 s
N3000 church unfold:
1) cubicaltt/hcomptrans: 2.3 s
2) anders: 1.9 s
Functor category:
1) cubicaltt/hcomptrans: 2.6 s
2) anders: 0.4 s
TN
STAY TUNED
TN
opam install anders
2021 July 06
TN
$ opam install anders
$ anders check experiments/mltt.anders
$ anders check experiments/mltt.anders
2021 July 08
TN
ОРИЕНТИРОВОЧНО 17 ЧИСЛО ИЮЛЬ 2021 В СУББОТУ. ПРОВЕРКА ДОМАШЕК НА https://t.me/groupoid