Skip to content

Draft: Slice v functors

Daniel Gratzerrequested to merge
hott/hott-set-theory:slice-v-functors into master

This shows that V/x ~ x -> V. Currently we just have the two functors. It remains to show that they're equivalences.

Merge request reports