Канал про філософію математики. Як формальна мова використовується гомотопічна теорія типів, як імплементація — кубіки. Багато прози.