Currently, the semantics of the imaginary inverse is inv(f) ~~ g justified by Rust not having inequality matching in the type system. This makes solutions by path semantical quality of the imaginary inverse kind of "patching" some lacking feature of the type system, which makes it difficult to interpret path semantical quality.
There is another semantics which is closer to the original intention behind path semantics and unifies it with higher category theory. In a higher category with two morphisms f : X -> Y and g : Y -> Z, the composition (g . f) : X -> Z has a notion of propositional equality to its normalized map as a 2-bimorphism. This requires an infinite regress of higher morphisms. Path semantical quality might be thought of as a way to "terminate" this infinite regression and expressing that ~(g . f) means it has a "solution". This way, the semantics does not depend on the imaginary inverse specifically, but holds for all higher category theory. Solutions of the imaginary inverse is just a special case.
E.g. ~f means it has some solution, but this does not imply ~inv(f). Therefore, both ~f and ~inv(f) are needed to express that the isomorphism is solved both ways.
Currently, the semantics of the imaginary inverse is
inv(f) ~~ gjustified by Rust not having inequality matching in the type system. This makes solutions by path semantical quality of the imaginary inverse kind of "patching" some lacking feature of the type system, which makes it difficult to interpret path semantical quality.There is another semantics which is closer to the original intention behind path semantics and unifies it with higher category theory. In a higher category with two morphisms
f : X -> Yandg : Y -> Z, the composition(g . f) : X -> Zhas a notion of propositional equality to its normalized map as a 2-bimorphism. This requires an infinite regress of higher morphisms. Path semantical quality might be thought of as a way to "terminate" this infinite regression and expressing that~(g . f)means it has a "solution". This way, the semantics does not depend on the imaginary inverse specifically, but holds for all higher category theory. Solutions of the imaginary inverse is just a special case.E.g.
~fmeans it has some solution, but this does not imply~inv(f). Therefore, both~fand~inv(f)are needed to express that the isomorphism is solved both ways.