minor changes & dependency map

forked-from-1kasper · Nov 20, 2023 · 53d0bd9 · 53d0bd9
1 parent 0655b19
commit 53d0bd9
Show file tree

Hide file tree

Showing 4 changed files with 505 additions and 513 deletions.
diff --git a/GroundZero/HITs/Quotient.lean b/GroundZero/HITs/Quotient.lean
@@ -1,5 +1,4 @@
 import GroundZero.HITs.Trunc
-import GroundZero.HITs.Graph
 
 open GroundZero.Types.Id (ap)
 open GroundZero.Types.Equiv
@@ -9,7 +8,7 @@ open GroundZero.Types
 open GroundZero
 
 namespace GroundZero.HITs
-universe u v w u' v'
+universe u v w u' v' w'
 
 hott def Quot {A : Type u} (R : A → A → Prop v) := ∥Graph (λ x y, (R x y).1)∥₀
 

diff --git a/GroundZero/Types/Id.lean b/GroundZero/Types/Id.lean
@@ -3,7 +3,7 @@ import GroundZero.Proto
 namespace GroundZero.Types
 universe u v
 
-hott remark UIP {A : Type u} {a b : A} (p q : a = b) : Eq p q := Eq.refl p
+hott remark UIP {A : Type u} {a b : A} (p q : Eq a b) : Eq p q := Eq.refl p
 
 section
   variable (A : Sort u)

diff --git a/dependency-map.gv b/dependency-map.gv
@@ -113,8 +113,7 @@ digraph dependency_map {
       "HITs/Coequalizer",
       "HITs/Colimit",
       "HITs/Generalized",
-      "HITs/Pushout",
-      "HITs/Quotient"
+      "HITs/Pushout"
     }
     "HITs/Interval" -> {
       "Cubical/Cubes",