Face duality for polyhedral cones ($\tau ⟷C^{\vee }\cap {\tau }^{\perp }$)

For a closed polyhedral cone $C$, the maps $\tau \mapsto C^{\vee }\cap {\tau }^{\perp }$ and $\nu \mapsto C\cap {\nu }^{\perp }$ give inverse order-reversing bijections on faces. Choose a exposing functional in the relative interior of the dual face. The bipolar identity and an exposing functional for the original face show that applying the maps twice returns that face.

// Target: geometry-and-topology.bigb