A potential mistake in homotopy level lecture?

[HuStmpHrrr]

I am watching your lectures and they are very helpful. in lecture 3, something got me confused. around 33:35, when discussing hProp, you showed that g is constructed from f by composing two paths. but it appears to me that the contraction already gives a path, namely the center, which immediately satisfies the requirement. the mistake seems due to a wrong conversion of iscontr. could you please clarify?

[andrejbauer]

Yeah, you're completely right. I could just use π₁(f x y) to get a point from x to y right away.

There really scary bit is that nobody in the class raised their hand and told me I made a mistake.

[HuStmpHrrr]

thank you for confirming. it's a scary bit but also an encouraging bit as it shows that indeed everybody needs proof assistants!