Tanaka, R.; Mineshima, K.; Bekki, D. Factivity and Presupposition in Dependent Type Semantics. JLM 2017, 5, 385–420.