Callan McGill (Mar 05 2022 at 05:59): Callan McGill (Mar 05 2022 at 05:59):Do any of you know anywhere that explains how the path_induction tactic of the HoTT library works?
Ali Caglayan (Mar 07 2022 at 01:51):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.
Ali Caglayan (Mar 07 2022 at 01:53):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