eviは証拠〈evidence〉の略記だとする。命題と証明の圏 $`{\bf Ded}`$ から集合圏への関手が定義できる。
- $`P\in |{\bf Ded}| \mapsto \mathrm{evi}(P) := {\bf Ded}(\top, P)`$
- $`(f:P \to Q) \text{ in }{\bf Ded} \mapsto \mathrm{evi}(f) := {\bf Ded}(\top, f)`$
この関手は、対象 $`\top`$ によって表現される表現可能関手となる。
反変の $`{\bf Ded}(\_, \bot)`$ を考えることも出来るし、相対圏に対して拡張することもできる。これは、演繹圏の集合圏への表現論になる。CPS変換とも関係する。
反変性に関してはド・モルガン双対／ゲルファント双対とも関係するだろう。米田埋め込みとも関係するだろう。
