nLab dependent correspondence



In dependent type theory, given types AA and BB, a correspondence is a type family x:A,y:BR(x,y)typex\colon A, y \colon B \vdash R(x, y) \; \mathrm{type}. A dependent correspondence is like such an correspondence but where we allow BB to also depend on x:Ax\colon A.


In dependent type theory (homotopy type theory), given a type AA and a type family x:AB(x)typex\colon A \vdash B(x) \; \mathrm{type}, a dependent correspondence is a type family x:A,y:B(x)R(x,y)typex\colon A, y\colon B(x) \vdash R(x, y) \; \mathrm{type}.


  • Every correspondence is a dependent correspondence where BB does not depend upon AA.

  • Every dependent anafunction is a dependent correspondence x:A,y:B(x)R(x,y)x\colon A, y\colon B(x) \vdash R(x, y) which comes with a family of witnesses

    x:Ap(x):isContr( y:B(x)R(x,y))x \colon A \vdash p(x) \colon \mathrm{isContr}\left(\sum_{y\colon B(x)} R(x, y) \right)

    that for each element x:Ax\colon A, the dependent sum type y:B(x)R(x,y)\sum_{y\colon B(x)} R(x, y) is a contractible type.

 See also

Created on January 7, 2023 at 05:01:52. See the history of this page for a list of all contributions to it.