Synthetic homotopy theory lecture question

Question

In this lectureLogic and topology at 20:21 there is a statement that type isContr which means "is contractible" means that for a given type A and every element x and pointed element a of type A, there is a path from a to x ( first formula on the slide). As it of course is definition, it just means everything author may want to, but as ,,"is contractible" has well topological meaning, I would like to ask if it is true? Because at topological level "is contractible" means that every closed path ( loop ) has to be contractible and it is quite different. From other HTT lectures I know that it is a notion of homotopic equivalence to trivial path ( path(A,a,a) = Id) should be used so it looks like path operation is not well defined on this lecture or presenter at least forgot to mention it is a loop in fact...

Or do I do not understand anything?

Answer 1

In classical topology, a contractible space is one that's equipped with a basepoint and a homotopy from the identity map to the constant map at that basepoint, i.e. a point $a$ and for every point $x$ a path from $x$ to $a$, varying continuously with $x$. This is exactly what the HoTT definition of IsContr says, except that the "varying continuously" doesn't have to be said explicitly since inside of type theory everything is "continuous".

Answer 2

I suppose Voevodsky use isContr as "is Contractible" in a meaning that there is at least one element of that type. In fact it would be equivalent to saying that type is not empty. It became clear at the univalence axiom level where there's consequence that "unique existence equals to real excistence". So if some object is unique ( up to isomorphism which is equivalent to up to contractible fibration of type) then there is actually an element of it ( which is the point of we contact to) .