From 3238405313e2d71bdb896beb8de3bd45cf0fcc90 Mon Sep 17 00:00:00 2001 From: cesarbm03 Date: Mon, 20 Nov 2023 15:49:18 -0500 Subject: [PATCH] formating --- src/simplicial-hott/10-rezk-types.rzk.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index b4dc022f..d709f2f9 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -944,8 +944,8 @@ In particular, every contractible type is Rezk ## Representable isomorphisms. -We prove [RS17, Proposition 10.11]. We firs need to access the fiberwise equivalence -with no extra data, and then define some helpers. +We prove [RS17, Proposition 10.11]. We firs need to access the fiberwise +equivalence with no extra data, and then define some helpers. ```rzk #def map-fiberwise-equiv