Commit 2026-01-08 12:28 d971c5d0

View on Github →

feat(FundamentalGroupoid/InducedMaps): generalize to different universes (#33445) Also simplify the proof

Estimated changes

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

modified def FundamentalGroupoidFunctor.equivOfHomotopyEquiv

modified def FundamentalGroupoidFunctor.homotopicMapsNatIso

added theorem Path.Homotopic.map_trans_evalAt

Modified Mathlib/Topology/Homotopy/Path.lean

added theorem Path.Homotopic.pathCast

added def Path.Homotopy.pathCast

Modified Mathlib/Topology/Path.lean