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.
1 parent e4cb462 commit a99058fCopy full SHA for a99058f
Cubical/Categories/Yoneda.agda
@@ -224,6 +224,7 @@ module _ {C : Category ℓ ℓ'} where
224
YO .F-id = makeNatTransPath λ i _ → λ f → ⋆IdR f i
225
YO .F-seq f g = makeNatTransPath λ i _ → λ h → ⋆Assoc h f g (~ i)
226
227
+
228
module _ {x} (F : Functor (C ^op) (SET ℓ')) where
229
yo-yo-yo : NatTrans (yo x) F → F .F-ob x .fst
230
yo-yo-yo α = α .N-ob _ id
0 commit comments