Function path

pub fn path<F: Prop, X: Prop, Y: Prop>(
    _: Theory<F>,
    _: Qu<Inv<F>>,
    _: Ty<F, Pow<Y, X>>,
    _: Pow<Y, X>,
) -> And<F, Inv<F>>

Expand description

theory(f) ⋀ ~inv(f) ⋀ (f : x -> y) ⋀ (x -> y) => f ⋀ inv(f).

This makes it possible to get inverse map for free.

path