R. Tanaka, K. Mineshima, and D. Bekki, “Factivity and presupposition in Dependent Type Semantics”, JLM, vol. 5, no. 2, pp. 385–420, Nov. 2017.