From e65b13a173a5e9196b6420300c6f3c6e912a14e6 Mon Sep 17 00:00:00 2001 From: Tashi Walde Date: Fri, 13 Oct 2023 21:04:00 +0200 Subject: [PATCH] Update src/simplicial-hott/04-right-orthogonal.rzk.md Co-authored-by: Fredrik Bakke --- src/simplicial-hott/04-right-orthogonal.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 95a5551e..a170619f 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -123,7 +123,7 @@ extension types. := has-contr-relative-extension-types-generalize extext I ψ ϕ ( \ _ → A') (\ _ → A) (\ _ → α) - ( has-contr-relative-extension-types-is-right-orthogonal-to-shape is-orth-α) + ( has-contr-relative-extension-types-is-right-orthogonal-to-shape is-orth-α) #end has-contr-relative-extension-types-iff-is-right-orthogonal ```