yoneda lemma

JetBrains · Jun 9, 2024 · f97cd5b · f97cd5b
1 parent e60c389
commit f97cd5b
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git a/src/Category/Limit.ard b/src/Category/Limit.ard
@@ -83,10 +83,13 @@
     | f_hinv => limUnique \lam j => inv o-assoc *> pmap (`∘ _) (L.limBeta L' j) *> L'.limBeta L j *> inv id-right
 
   \func transFuncMap {D : Precat} (L L' : Limit { | D => D }) (H : Functor L.J L'.J) (a : NatTrans (Comp L'.G H) L.G) : Hom L' L =>
-    limMap (\new Cone {
+    limMap cone
+  \where {
+    \func cone : Cone G L' => \new Cone {
       | coneMap j => a j ∘ L'.coneMap (H j)
       | coneCoh f => inv o-assoc *> pmap (`∘ _) (inv (a.natural f)) *> o-assoc *> pmap (_ ∘) (L'.coneCoh (H.Func f))
-    })
+    }
+  }
 }
 
 \meta Colimit G => Limit (Functor.op {G})

diff --git a/src/Category/Slice.ard b/src/Category/Slice.ard
@@ -1,5 +1,6 @@
 \import Category
 \import Category.Functor
+\import Category.Limit
 \import Paths
 \import Paths.Meta
 
@@ -22,4 +23,4 @@
   | Precat => SlicePrecat x
   | univalence => Cat.makeUnivalence \lam (e : Iso) =>
       \have e' => Functor.Func-iso {SlicePrecat.forget x} e
-      \in (ext (Cat.isotoid e', Cat.transport_Hom_iso-left e' _ (inv e.f.2)), simp_coe (Cat.transport_Hom_iso-right e' _ id-right))
+      \in (ext (Cat.isotoid e', Cat.transport_Hom_iso-left e' _ (inv e.f.2)), simp_coe (Cat.transport_Hom_iso-right e' _ id-right))