Skip to content

Commit

Permalink
typo
Browse files Browse the repository at this point in the history
  • Loading branch information
@martinescardo
martinescardo committed Sep 6, 2023
1 parent 65a75c9 commit fc2c7ec
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion source/InjectiveTypes/Sigma.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ including universe levels.
For the moment I am not going to work any further with this (until I
really need it).

For motivation, the reader should check the file
For motivation, the reader should check [1].

Two big improvements here are that

Expand Down

0 comments on commit fc2c7ec

Please sign in to comment.