We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
2 parents 6239fe0 + b9d60ad commit 5a49c6aCopy full SHA for 5a49c6a
src/Categories/Category/Instance/One.agda
@@ -24,7 +24,7 @@ module _ {o ℓ e : Level} where
24
One-⊤ : Terminal
25
One-⊤ = record { ⊤ = One ; ! = record { F₀ = λ _ → lift tt } }
26
27
--- not only is One terminal, it can be shifted anywhere else. Stronger veersion of !
+-- not only is One terminal, it can be shifted anywhere else. Stronger version of !
28
shift : {o ℓ e : Level} (o′ ℓ′ e′ : Level) → Functor (One {o} {ℓ} {e}) (One {o′} {ℓ′} {e′})
29
shift o′ ℓ′ e′ = _ -- so obvious, Agda can fill it all in automatically!
30
0 commit comments