From fbbf87bba9a6556e30e7cd05be7035ce75c5ffc9 Mon Sep 17 00:00:00 2001 From: jlh <48520973+Jlh18@users.noreply.github.com> Date: Thu, 16 Sep 2021 11:26:30 +0100 Subject: [PATCH] Update Quest0Part0.md --- 1FundamentalGroup/Quest0Part0.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/1FundamentalGroup/Quest0Part0.md b/1FundamentalGroup/Quest0Part0.md index 14898b9..5933a58 100644 --- a/1FundamentalGroup/Quest0Part0.md +++ b/1FundamentalGroup/Quest0Part0.md @@ -32,7 +32,7 @@ in the first case `Type` is the space of spaces.
Further details -This is called a __higher inductive type_ (HIT), which generally +This is called a _higher inductive type_ (HIT), which generally follows the format of - `data`