Do any of you know anywhere that explains how the path_induction tactic of the HoTT library works?
Well I wouldn't really use the path_induction tactic in practice. All it is doing is calling
destruct on a path in the context. First it introduces all the variables it can, then it looks for any variables of the path type, if it has found some it tries
induction (which is really just
destruct since there is no IH). I think you are better off calling
destruct on your path hypotheses yourself.
By the way there is a HoTT zulip if you are interested: https://hott.zulipchat.com/
Last updated: Sep 26 2023 at 12:02 UTC