diff --git a/properties/P000242.md b/properties/P000242.md
new file mode 100644
index 000000000..fc08d7924
--- /dev/null
+++ b/properties/P000242.md
@@ -0,0 +1,37 @@
+---
+uid: P000242
+name: Weakly contractible
+aliases:
+  - Homotopically trivial
+  - $C^\infty$
+refs:
+  - wikipedia: Weakly_contractible_space
+    name: Weakly contractible space on Wikipedia
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+  - zb: "0979.55010"
+    name: On the universal space for group actions with compact isotropy (Lück, Meintrup)
+  - zb: "1467.20042"
+    name: A stronger reformulation of Webb’s conjecture in terms of finite topological spaces (Piterman)
+  - zb: "0153.52905"
+    name: Theory of retracts (Borsuk)
+---
+
+For each integer $n\ge 0$ every continuous map $S^n\to X$ is homotopic to a constant map.
+
+Equivalently, $X$ is nonempty, {P37} and all [homotopy groups](https://en.wikipedia.org/wiki/Homotopy_group) $\pi_n(X)$ with $n\ge 1$ are trivial.
+In other words, $X$ is [weakly homotopy equivalent](https://en.wikipedia.org/wiki/Weak_equivalence_(homotopy_theory)) to {S162}.
+
+Notation above: $S^n$ is the unit sphere in $\mathbb R^{n+1}$.
+
+Defined as *weakly contractible* for example on page 2 in {{zb:0979.55010}}
+(accessible [here](https://www.academia.edu/53860578/On_the_universal_space_for_group_actions_with_compact_isotropy)).
+Defined as *homotopically trivial* on page 281 of {{zb:1467.20042}}.
+Borsuk uses the terminology $C^\infty$, defined as $X$ being *$n$-connected* for all $n\ge 0$
+(see page 30 of {{zb:0153.52905}}).
+
+----
+#### Meta-properties
+
+- This property is preserved by finite products (see Proposition 4.2 in {{zb:1044.55001}}).
+- This property is preserved by homotopy equivalences.
diff --git a/theorems/T000890.md b/theorems/T000890.md
new file mode 100644
index 000000000..c28f0b844
--- /dev/null
+++ b/theorems/T000890.md
@@ -0,0 +1,9 @@
+---
+uid: T000890
+if:
+  P000242: true
+then:
+  P000037: true
+---
+
+By definition.
diff --git a/theorems/T000891.md b/theorems/T000891.md
new file mode 100644
index 000000000..5835cf2a2
--- /dev/null
+++ b/theorems/T000891.md
@@ -0,0 +1,9 @@
+---
+uid: T000891
+if:
+  P000242: true
+then:
+  P000137: false
+---
+
+By definition.
diff --git a/theorems/T000892.md b/theorems/T000892.md
new file mode 100644
index 000000000..2789d708e
--- /dev/null
+++ b/theorems/T000892.md
@@ -0,0 +1,9 @@
+---
+uid: T000892
+if:
+  P000199: true
+then:
+  P000242: true
+---
+
+Follows since any homotopy equivalence is also a weak homotopy equivalence.
diff --git a/theorems/T000893.md b/theorems/T000893.md
new file mode 100644
index 000000000..d19c30ab3
--- /dev/null
+++ b/theorems/T000893.md
@@ -0,0 +1,9 @@
+---
+uid: T000893
+if:
+  P000242: true
+then:
+  P000200: true
+---
+
+By definition, since the first homotopy group is the fundamental group.