corrected parentheses in subobject classifier

benediktahrens · Jan 30, 2014 · caa4be7 · caa4be7
1 parent b78ed3d
commit caa4be7
Showing 1 changed file with 8 additions and 8 deletions.
diff --git a/topos/topos.v b/topos/topos.v
@@ -31,16 +31,16 @@ Variable C : precategory.
 Variable T : Terminal C.
 
 Definition isSubobjectClassifier (Omega : C) (TrueArrow : T --> Omega) :=
-    forall (s b : C) (m : mono C s b), iscontr (
-      total2 (fun phi : b --> Omega =>
-      total2 (fun H : m ;; phi == TerminalArrow s ;; TrueArrow  => 
-                    isPullback C phi TrueArrow m (TerminalArrow s) H))).
+    forall (s b : C) (m : mono C s b), iscontr (total2 
+         (fun phiH : total2 (fun phi : b --> Omega => 
+                   m ;; phi == TerminalArrow s ;; TrueArrow) =>
+                isPullback C (pr1 phiH) TrueArrow m (TerminalArrow s) (pr2 phiH))).
+
 
 Definition SubobjectClassifier :=  
-    total2 (fun Omega : C => 
-    total2 (fun TrueArrow : T --> Omega =>
-           isSubobjectClassifier Omega TrueArrow)).
-Definition Omega (S : SubobjectClassifier) : C := pr1 S.
+    total2 (fun OmegaTrueArrow : total2 (fun b => T --> b) =>
+           isSubobjectClassifier (pr1 OmegaTrueArrow) (pr2 OmegaTrueArrow)).
+Definition Omega (S : SubobjectClassifier) : C := pr1 (pr1 S).
 
 (* todo : prove unicity of subobject classifer *)