Removed stale dead code in [category_of_elements]

Author: peterlefanulumsdaine

TypeTheory/Categories/category_of_elements.v

@@ -225,92 +225,3 @@ Proof.
 Defined.
 
 End category_of_elements.
-
-
-(*
-Section category_of_elements.
-
-Variable C : precategory.
-Variable F : functor C (opp_precat HSET).
-
-Definition precategory_of_elements_ob_mor : precategory_ob_mor.
-Proof.
-  exists (∑ c : C, pr1 (F c)).
-  intros ca c'a'.
-  exact (∑ f : pr1 ca --> pr1 c'a', #F (f) (pr2 c'a') = (pr2 ca)).
-Defined.
-
-Definition precategory_of_elements_data : precategory_data.
-Proof.
-  exists precategory_of_elements_ob_mor.
-  split.
-  - intro c. 
-    exists (identity (pr1 c)).
-    eapply pathscomp0. 
-    + rewrite (functor_id F). apply idpath.
-    + apply idpath.
-  - intros a b c f g.
-    exists (pr1 f ;; pr1 g).
-    rewrite functor_comp. unfold compose; simpl in *.
-    unfold compose. simpl.
-    rewrite (pr2 g). rewrite (pr2 f).
-    apply idpath.
-Defined.
-  
-Lemma is_precategory_precategory_of_elements : is_precategory precategory_of_elements_data.
-Proof.
-  repeat split; intros;
-  simpl in *.
-  - apply total2_paths_second_isaprop.
-    + apply setproperty.
-    + apply id_left.
-  - apply total2_paths_second_isaprop.
-    + apply setproperty.
-    + apply id_right.
-  - apply total2_paths_second_isaprop.
-    + apply setproperty.
-    + apply assoc.
-Qed.
-
-Definition precategory_of_elements : precategory 
-  := tpair _ _ is_precategory_precategory_of_elements.
-
-Local Notation "∫" := precategory_of_elements.
-(* written \int in agda input mode *)
-
-(** first projection gives a (forgetful) functor **)
-
-Definition proj_functor_data : functor_data ∫ C.
-Proof.
-  exists (@pr1 _ _ ).
-  exact (λ a b, @pr1 _ _ ).
-Defined.
-
-Lemma is_functor_proj : is_functor proj_functor_data.
-Proof.
-  split; unfold functor_idax, functor_compax; intros;
-  simpl in *; apply idpath.
-Qed.
-
-Definition proj_functor : functor _ _ := tpair _ _ is_functor_proj.
-
-(* need that ∫ F is saturated if C is *)
-
-
-(* next steps *)
-
-(**
-
-∫ ------> RC (∫)---> ∫ (F_RC)     with F_RC : RC(C) --> Set
-|           |       /
-|           |      /
-v           v     /
-C ------> RC (C) 
-
-*)
-
-(* need functoriality of RC, or at least action on functors *)
-
-
-End category_of_elements.
-*)