{X : Type u_3} →
  {Y : Type u_4} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        ContinuousMap.HomotopyEquiv X Y →
          (↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj { carrier := X, str := inst }) ≌
            ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj { carrier := Y, str := inst_1 }))