CMUのConstructive LogicのコースのProof Irrelevanceの資料 https://www.cs.cmu.edu/~fp/courses/15317-f08/lectures/08-irrelevance.pdf を読んでいる。
("Mathematics and Computation: Formal proofs are not just deduction steps" http://math.andrej.com/2016/08/30/formal-proofs-are-not-just-deduction-steps/ でリンクされていた資料)
AgdaのIrrelevanceの機能 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Irrelevance とか存在だけ知ってて、詳しいことは全く知らなかったのだけれど、こんな感じの延長で実現されているのかな？