HoTT本のログ
P3
型は
∞-グルーポイド
とみなす
Chapter 1 Type Theoty
依存型
#ログ・記録・メモ