Skip to content

Commit

Permalink
Update src/simplicial-hott/04-right-orthogonal.rzk.md
Browse files Browse the repository at this point in the history
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
  • Loading branch information
TashiWalde and fredrik-bakke committed Oct 13, 2023
1 parent ef6d3d0 commit e65b13a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/simplicial-hott/04-right-orthogonal.rzk.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
```
Expand Down

0 comments on commit e65b13a

Please sign in to comment.