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), 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/arXiv), 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/arXiv); stated $\infty$-categorically, $\top : 1 \to 2$ classifies 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.

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), 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/arXiv), 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/arXiv); 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.

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), 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/arXiv), or from viewing $\S$ as an $\infty$-topos. There, only fibrations are taken to interpret dependent types — 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/arXiv); stated $\infty$-categorically, $\top : 1 \to 2$ classifies 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.

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), 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/arXiv), 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/arXiv); stated $\infty$-categorically, $\top : 1 \to 2$ classifies 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.