Move diagrams to a separate file

UniMath · Jan 29, 2025 · cd5fe31 · cd5fe31
1 parent 39b2adc
commit cd5fe31
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/TypeTheory/Auxiliary/SetsAndPresheaves.v b/TypeTheory/Auxiliary/SetsAndPresheaves.v
@@ -262,7 +262,7 @@ Proof.
   transparent assert
        (XH : (∏ a : C^op,
         LimCone
-          (@Colimits.diagram_pointwise C^op HSET
+          (@Diagrams.diagram_pointwise C^op HSET
              pullback_graph XT1 a))).
     { intro. apply LimConeHSET.  }
     specialize (XR XH).
@@ -278,7 +278,7 @@ Proof.
     specialize (XR S).
     simpl in XR.
     transparent assert (HC
-      :  (cone (@Colimits.diagram_pointwise C^op HSET
+      :  (cone (@Diagrams.diagram_pointwise C^op HSET
                     pullback_graph (pullback_diagram (preShv C) f g) c) S)).
     { use make_cone.
       apply three_rec_dep; cbn.