Recently I have read some meta-level dependent type theory (Typst source). It might be time to re-read `leantt` paper, and start reading `lean4lean` paper/source.
The author `ice1000` has strong interest in QIIT (Quotient Inductive-Inductive Types) and QIIR (Quotient Inductive-Inductive Recursion), he has implemented `overlap` in Aya with termination check and confluence check.
Aya has a philosophy that the kernel could include pattern matching, but at the cost of no generation and translation of eliminators at present. In principle this is feasible, without `overlap`, it could be implemented by "theory of signatures", with `overlap`, it needs "Coherent and concurrent elimination for initial algebras" which I find fascinating, and have read [yeasin2011initial].
The author also has a great article on TT & Cat [zhang2021type]. His recommendation of [gundry2013tutorial] is also worth reading.
In the process of learning Topos, I wish to have a better understanding of Logic. Particularly, Curry–Howard–Lambek correspondance, Propositional truncation, and Paraconsistent logic are on the plate.
Although remotely related, I'll place Introduction to Formal Reasoning (COMP2065) in this section so I won't lose track of it.