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.