From cd5fe3162ac5f29f6ccc5bb9fee9bb546033a231 Mon Sep 17 00:00:00 2001
From: Tempestas Ludi <tempestasludi@gmail.com>
Date: Wed, 29 Jan 2025 17:46:20 +0100
Subject: [PATCH] Move diagrams to a separate file

---
 TypeTheory/Auxiliary/SetsAndPresheaves.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/TypeTheory/Auxiliary/SetsAndPresheaves.v b/TypeTheory/Auxiliary/SetsAndPresheaves.v
index 9749ca7b..81dc165d 100644
--- 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.