introduce dangerous implicit arguments

benediktahrens · Jan 30, 2014 · b78ed3d · b78ed3d
1 parent b04bf34
commit b78ed3d
Show file tree

Hide file tree

Showing 4 changed files with 55 additions and 10 deletions.
diff --git a/limits/products.v b/limits/products.v
@@ -140,7 +140,19 @@ End product_def.
 
 
 
+Section test.
 
+Variable C : precategory.
+Variable H : Products C.
+
+About ProductObject.
+Arguments ProductObject [C] c d {_}.
+About ProductObject.
+Local Notation "c 'x' d" := (ProductObject  c d )(at level 5).
+
+Check (fun c d : C => c x d).
+
+End test.
 
 
 

diff --git a/limits/products_from_pullbacks.v b/limits/products_from_pullbacks.v
@@ -26,12 +26,12 @@ Variable T : Terminal C.
 
 Definition UnivProductFromPullback (c d a : C) (f : a --> c) (g : a --> d):
 total2
-     (fun fg : a --> Pb T c d (TerminalArrow C T c) (TerminalArrow C T d) =>
-      dirprod (fg;; PullbackPr1 C (Pb T c d (TerminalArrow C T c) (TerminalArrow C T d)) == f)
-        (fg;; PullbackPr2 C (Pb T c d (TerminalArrow C T c) (TerminalArrow C T d)) == g)).
+     (fun fg : a --> Pb T c d (TerminalArrow c) (TerminalArrow d) =>
+      dirprod (fg;; PullbackPr1 C (Pb T c d (TerminalArrow c) (TerminalArrow d)) == f)
+        (fg;; PullbackPr2 C (Pb T c d (TerminalArrow c) (TerminalArrow d)) == g)).
 Proof.
   unfold Pullbacks in Pb.
-  exists (PullbackArrow _ (Pb _ _ _ (TerminalArrow C T c)(TerminalArrow C T d)) _ f g
+  exists (PullbackArrow _ (Pb _ _ _ (TerminalArrow c)(TerminalArrow d)) _ f g
        (ArrowsToTerminal _ _ _ _ _)).
   split. 
   apply PullbackArrow_PullbackPr1 .
@@ -42,7 +42,7 @@ Defined.
 
 Lemma isProductCone_PullbackCone (c d : C):
    isProductCone C c d 
-            (PullbackObject _ (Pb _ _ _ (TerminalArrow C T c)(TerminalArrow C T d)))
+            (PullbackObject _ (Pb _ _ _ (TerminalArrow c)(TerminalArrow (T:=T) d)))
    (PullbackPr1 _ _  ) (PullbackPr2 _ _ ).
 Proof.
   intros a f g.
@@ -57,11 +57,18 @@ Qed.
 Definition ProductCone_PullbackCone (c d : C) : ProductCone _ c d.
 Proof.
   exists
-  (tpair _ (PullbackObject _ (Pb _ _ _ (TerminalArrow C T c)(TerminalArrow C T d)))
+  (tpair _ (PullbackObject _ (Pb _ _ _ (TerminalArrow c)(TerminalArrow (T:=T) d)))
                (dirprodpair  (PullbackPr1 _ _  ) (PullbackPr2 _ _ ))).
  exact (isProductCone_PullbackCone c d).
 Defined.
 
+Definition ProductsFromPullbacks : Products C := ProductCone_PullbackCone.
+
+
+Arguments ProductObject [C] c d {_}.
+Local Notation "c 'x' d" := (ProductObject  c d )(at level 5).
+Check (fun c d : C => c x d).
+
 End product_from_pullback.
 
 
@@ -76,3 +83,5 @@ End product_from_pullback.
 
 
 
+
+
diff --git a/limits/terminal.v b/limits/terminal.v
@@ -69,4 +69,29 @@ Qed.
 
 End Terminal_Unique.
 
-End def_terminal.
+End def_terminal.
+
+
+Section test.
+Variable C : precategory.
+Variable T : Terminal C.
+
+About TerminalObject.
+
+Arguments TerminalObject [C]{_}.
+
+About TerminalObject.
+
+Check (fun a => a --> T).
+
+About TerminalArrow.
+
+Arguments TerminalArrow [C]{T} b.
+
+Check (fun a : C => TerminalArrow a).
+
+End test.
+
+Arguments TerminalObject [C]{_}.
+Arguments TerminalArrow [C]{T} b.
+
diff --git a/topos/topos.v b/topos/topos.v
@@ -33,9 +33,8 @@ 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 C T s ;; TrueArrow  => 
-                    isPullback C TrueArrow phi m (TerminalArrow _ _ s) H))).
-
+      total2 (fun H : m ;; phi == TerminalArrow s ;; TrueArrow  => 
+                    isPullback C phi TrueArrow m (TerminalArrow s) H))).
 
 Definition SubobjectClassifier :=  
     total2 (fun Omega : C =>