From 3e77252ee72c1f1e35bbddf51ba00ffaf202a78f Mon Sep 17 00:00:00 2001 From: jlh <48520973+Jlh18@users.noreply.github.com> Date: Fri, 30 Jul 2021 11:27:08 +0100 Subject: [PATCH] Update Quest1.md --- Trinitarianism/Quest1.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Trinitarianism/Quest1.md b/Trinitarianism/Quest1.md index 5000e56..18b9d0c 100644 --- a/Trinitarianism/Quest1.md +++ b/Trinitarianism/Quest1.md @@ -117,9 +117,11 @@ This is called a _sigma type_, which has three interpretations: - the total space of the bundle `isEven` over `ℕ`, which is the space obtained by putting together all the fibers. Pictorially, it looks like + SigmaTypeOfIsEven + which can also be viewed as the subset of even naturals, since the fibers are either empty or singleton. (It is a _subsingleton bundle_).