When considering topological spaces with algebraic structures, there are certain properties which are invariant under homotopy equivalence, such as homotopy-associativity, and others that are not, such as strict associativity. A natural question is: which properties, in general, are homotopy invariant? As this involves a general notion of "property", it is a question of mathematical logic, and in particular suggests that we need a system of logical notation which is somehow well-adapted to the homotopical context. Such a system was introduced by Voevodsky under the name Homotopy Type Theory. I will discuss a sort of toy version of this, which is the case of "first-order homotopical logic", in which we can very thoroughly work out this question of homotopy-invariance. The proof of the resulting homotopy-invariance theorem involves some interesting ("fibrational") structures coming from categorical logic.