**No, it’s not “inconsistent up to homotopy”** — by combining the (strict) subobject classifier with the idea that contractible=trivial, you’re mixing two different logical languages for simplicial sets, in a way that doesn’t really make sense.

**The subobject classifier is the “object of truth-values” of $\newcommand{\S}{\mathrm{sSet}}\S$ as a (strict 1-)topos** — logically this can be seen as part of the interpretation of higher-order logic (IHOL) (see e.g. the [Lambek–Scott book](https://www.cambridge.org/se/universitypress/subjects/mathematics/logic-categories-and-sets/introduction-higher-order-categorical-logic?format=PB&isbn=9780521356534)), or any of various forms of dependent type theory with a universe of propositions; but crucially, in all of these, arbitrary morphisms can be used to interpret “dependent types”, and equality is interpreted using a strict equaliser.  **In this logic, $\Omega$ is an object of truth-values, but is not trivial.**

On the other hand, **the idea that “contractible $\Rightarrow$ all elements equal” comes from the homotopy-theoretic interpretations of type theory** (see e.g. Kapulkin–Lumsdaine 2012/2021, [JEMS](https://doi.org/10.4171/jems/1050)/[arXiv](https://arxiv.org/abs/1211.2851)), **or from viewing $\S$ as an $\infty$-topos.**  There, *only fibrations* are taken to interpret dependent types, or (roughly equivalently) reindexing is modelled by *homotopy* pullbacks — and this is what makes it possible to interpret equality to as homotopy.  But the canonical map $\top : 1 \to \Omega$ which 1-categorically classifies subobjects is *not* a fibration (indeed, it’s an equivalence); so in this logic, the classifying property of $\Omega$ isn’t visible. **In this logic, $\Omega$ is indeed trivial, but it’s not an object of truth-values** — in fact the object of truth-values is simply $2$, since up to homotopy, LEM holds (Kapulkin–Lumsdaine 2020, [TAC](http://www.tac.mta.ca/tac/volumes/35/40/35-40abs.html)/[arXiv](https://arxiv.org/abs/2006.13694)); stated $\infty$-categorically, $\top : 1 \to 2$ classifies $\infty$-monomorphisms (that is, $(-1)$-connected maps).

There are various reasonable ways to give a type theory combining these two interpretations (“2-level type theory” and “strict equality”, “strict propositions” are good keywords for this).  **Under such a language, both the above views of $\Omega$ will be visible together — but it can’t allow combining them to derive any kind of contradiction**, since we know $\S$ is consistent in each of these languages.  In particular, the universal family of propositions over $\Omega$ will be a “strict type/predicate”, and universal among strict proposition-valued predicates; and its elements will indeed be equal up to “weak equality”/“homotopy”; but strict predicates will not generally respect weak equality, so no inconsistency or triviality results.