Got rid of almost all remaining TODOs.

Author: wkolowski

Base.v

@@ -545,19 +545,14 @@ Definition bijective {A B : Type} (f : A -> B) : Prop :=
   injective f /\ surjective f.
 
 Definition injectiveS {A B : Type} {SA : Setoid A} {SB : Setoid B} (f : A -> B) : Prop :=
-    forall a a' : A, f a == f a' -> a == a'.
+  forall a a' : A, f a == f a' -> a == a'.
 
 Definition surjectiveS {A B : Type} {S : Setoid B} (f : A -> B) : Prop :=
   forall b : B, exists a : A, f a == b.
 
 Definition bijectiveS {A B : Type} {SA : Setoid A} {SB : Setoid B} (f : A -> B) : Prop :=
   injectiveS f /\ surjectiveS f.
 
-Definition surjectiveS'
-  {A B : Type} {SA : Setoid A} {SB : Setoid B} (f : A -> B) : Prop :=
-    exists g : B -> A,
-      Proper (equiv ==> equiv) g /\ forall b : B, f (g b) == b.
-
 #[global] Hint Unfold injective surjective bijective injectiveS surjectiveS bijectiveS : core.
 
 (** Useful automation tactics. *)

Category/Enriched.v

@@ -21,7 +21,6 @@ Class Enriched (V : Monoidal) : Type :=
     forall A B : EOb, bimap (id (EHom A B)) (EId B) .> EComp A B B == right_unitor (EHom A B);
 }.
 
-(* TODO: Commented out because it takes too much time.
 #[refine]
 #[export]
 Instance Enriched_CoqSetoid
@@ -43,5 +42,4 @@ Proof.
   - now cbn.
   - now cbn.
   - now cbn.
-Defined.
-*)
+Defined.

Instances/CoqSet.v

@@ -23,7 +23,7 @@ Proof.
   - easy.
 Defined.
 
-Lemma CoqSet_isMono_inj :
+Lemma CoqSet_isMono :
   forall (A B : Ob CoqSet) (f : A -> B),
     isMono f <-> injective f.
 Proof.
@@ -33,7 +33,7 @@ Proof.
   - now apply H, H0.
 Defined.
 
-Lemma CoqSet_isEpi_sur :
+Lemma CoqSet_isEpi :
   forall (X Y : Type) (f : Hom X Y),
     isEpi f <-> surjective f.
 Proof.
@@ -52,17 +52,6 @@ Proof.
     now apply propositional_extensionality; intuition eauto.
 Qed.
 
-(* TODO : characterize and sections and isomorphisms of sets *)
-
-Lemma CoqSet_isIso_bij :
-  forall (A B : Type) (f : Hom A B),
-    isIso f <-> bijective f.
-Proof.
-  intros A B f.
-  unfold bijective.
-  rewrite isIso_iff_isMono_isRet, <- CoqSet_isMono_inj, <- CoqSet_isEpi_sur.
-Admitted.
-
 #[refine]
 #[export]
 Instance HasInit_CoqSet : HasInit CoqSet :=

Instances/Lin.v

@@ -132,46 +132,9 @@ Proof.
   now cbn; intuition.
 Defined.
 
-(* TODO : products of linear orders suck because of constructivity *)
-
-(*
-#[refine]
-#[export]
-Instance Lin_product (X Y : Lin) : Lin :=
-{
-  pos := Lin_product_Pos X Y
-}.
-Proof.
-  intros [x1 y1] [x2 y2]; cbn in *.
-  destruct (leq_total x1 x2), (leq_total x2 x1), (leq_total y1 y2), (leq_total y2 y1).
-  all: firstorder.
-Abort.
-
-Definition Lin_outl (X Y : Lin) : ProsHom (Lin_product X Y) X.
-Proof.
-  red. exists fst. destruct 1, H; try rewrite H; lin.
-Defined.
-
-Definition Lin_outr (X Y : Lin) : ProsHom (Lin_product X Y) Y.
-Proof.
-  red. exists snd. lin'. destruct a, a', H, H; cbn in *.
-Abort.
-*)
-
-(*
-#[refine]
-#[export]
-TODO: Instance HasProducts_Lin : HasProducts LinCat :=
-{
-  product := Lin_product;
-  outl := Pros_outl;
-  outr := Pros_outr;
-  fpair := @Pros_fpair
-}.
-Proof.
-  all: pos'; cat; try rewrite H; try rewrite H0; try destruct (y x); easy.
-Defined.
-*)
+(** Defining product of linear orders is not possible without LEM and coproducts
+    of linear orders don't exist because they are kidn of "connected" and
+    coproducts are all about creating objects which are "disconnected". *)
 
 #[refine]
 #[export]
@@ -194,37 +157,16 @@ Proof.
   - now intros [x1 | y1] [x2 | y2] [x3 | y3] H12 H23; cbn in *; eauto.
 Defined.
 
-#[refine]
-#[export]
-Instance Lin_coproduct (X Y : Lin) : Lin :=
-{
-  pos :=
-  {|
-    pros := Lin_Pros_coproduct X Y;
-  |}
-}.
-Proof.
-  all: now intros; repeat (try
-    match goal with
-    | p : _ + _ |- _ => destruct p
-    end;
-    my_simpl; try f_equal; lin').
-Defined.
-
-Definition Lin_finl (X Y : Lin) : ProsHom X (Lin_coproduct X Y).
-Proof.
-  now exists (CoqSetoid_finl X Y).
-Defined.
-
-Definition Lin_finr (X Y : Lin) : ProsHom Y (Lin_coproduct X Y).
+Lemma no_coproducts_Lin :
+  HasCoproducts LinCat -> False.
 Proof.
-  now exists (CoqSetoid_finr X Y).
-Defined.
-
-Definition Lin_copair
-  (A B X : Lin) (f : ProsHom A X) (g : ProsHom B X) : ProsHom (Lin_coproduct A B) X.
-Proof.
-  exists (CoqSetoid_copair f g).
-  intros [a1 | b1] [a2 | b2] H; cbn in *.
-  - now lin.
+  intros [? ? ? ? _]; cbn in *.
+  specialize (copair _ _ _ (finr Lin_term Lin_term) (finl Lin_term Lin_term)).
+  destruct copair as [[copair Heq] Hleq]; cbn in *.
+  destruct (finl Lin_term Lin_term) as [[f Hf1] Hf2]; cbn in *.
+  destruct (finr Lin_term Lin_term) as [[g Hg1] Hg2]; cbn in *.
+  pose (Hleq1 := Hleq (f tt) (g tt)).
+  pose (Hleq2 := Hleq (g tt) (f tt)).
+  destruct (leq_total (f tt) (g tt)).
+  - specialize (Hleq1 H).
 Abort.

Instances/Pros.v

@@ -218,8 +218,8 @@ Proof.
   now repeat split; cbn in *.
 Defined.
 
-Definition thin (C : Cat) : Prop :=
-  forall (X Y : Ob C) (f g : Hom X Y), f == g.
+(* Definition thin (C : Cat) : Prop :=
+  forall (X Y : Ob C) (f g : Hom X Y), f == g. *)
 
 #[refine]
 #[export]

Instances/Setoids.v

@@ -55,7 +55,7 @@ Proof.
   - now cbn; intros x; apply H, H0.
 Defined.
 
-Lemma CoqSetoid_isEpi :
+Lemma CoqSetoid_isEpi_surjectiveS :
   forall (X Y : Ob CoqSetoid) (f : Hom X Y),
     surjectiveS f -> isEpi f.
 Proof.
@@ -65,7 +65,7 @@ Proof.
   now apply Heq.
 Defined.
 
-Lemma CoqSetoid_surjectiveS :
+Lemma CoqSetoid_surjectiveS_isEpi :
   forall (X Y : Ob CoqSetoid) (f : Hom X Y),
     isEpi f -> surjectiveS f.
 Proof.
@@ -85,26 +85,13 @@ Proof.
   now intuition eexists.
 Defined.
 
-Lemma CoqSetoid_isSec :
-  forall (X Y : Ob CoqSetoid) (f : Hom X Y),
-    isSec f -> injectiveS f.
-Proof.
-  intros.
-  apply isMono_isSec in H.
-  now apply CoqSetoid_isMono.
-Defined.
-
-Lemma CoqSetoid_isRet :
+Lemma CoqSetoid_isEpi :
   forall (X Y : Ob CoqSetoid) (f : Hom X Y),
-    isRet f <-> surjectiveS' f.
+    isEpi f <-> surjectiveS f.
 Proof.
-  unfold isRet, surjectiveS.
-  split; cbn.
-  - intros [g H]. red.
-    exists g.
-    now setoid'.
-  - intros (g & H1 & H2).
-    now exists {| func := g; Proper_func := H1 |}.
+  split.
+  - now apply CoqSetoid_surjectiveS_isEpi.
+  - now apply CoqSetoid_isEpi_surjectiveS.
 Qed.
 
 #[export]

ReynoldsProgramme/ReflexiveGraphCategory.v

@@ -1,7 +1,6 @@
 Require Import JMeq ProofIrrelevance.
 
-(** TODO: work it out.
-    Remember: in a reflexive graph category, morphisms need NOT preserve
+(** Remember: in a reflexive graph category, morphisms need NOT preserve
     all relations. We just have to specify which morphisms preserve
     which relations.
 

ReynoldsProgramme/ReflexiveGraphCategory_v2.v

@@ -101,7 +101,6 @@ Proof.
   now setoid.
 Defined.
 
-(* TODO *)
 #[refine]
 #[export]
 Instance SetoidFunRel : ReflexiveGraphCategory :=

Universal/Colimit.v

@@ -100,8 +100,6 @@ Class HasColimits (C : Cat) : Type :=
 Arguments colimit  [C _ J] _.
 Arguments colimitMor [C _ J F] _.
 
-(* TODO : natural conditions for (co)limits *)
-
 #[refine]
 #[export]
 Instance CoconeImage

Universal/Limit.v

@@ -95,11 +95,9 @@ Class HasLimits (C : Cat) : Type :=
   ok : allLimits (@limit) (@limitMor);
 }.
 
-Arguments limit  [C _ J] _.
+Arguments limit    [C _ J] _.
 Arguments limitMor [C _ J F] _.
 
-(* TODO : natural conditions for (co)limits *)
-
 #[refine]
 #[export]
 Instance ConeImage
@@ -118,14 +116,16 @@ Definition isContinuous {C D : Cat} {F : Functor C D} : Prop :=
   forall (J : Cat) (Diagram : Functor J C) (K : Cone Diagram),
     isLimit' K -> isLimit' (ConeImage F K).
 
-(* Coercion wut {C D : Cat} (F : Functor C D) : Ob (FunCat C D) := F. *)
+(*
+Coercion wut {C D : Cat} (F : Functor C D) : Ob (FunCat C D) := F.
 
-(* Lemma isLimit_char
+Lemma isLimit_char
   (J C : Cat) (F : Functor J C)
   (K : Cone F) (del : forall K' : Cone F, ConeHom K' K) :
     @isLimit J C F K del
       <->
     forall c : Ob C,
       @isomorphic CoqSetoid (HomSetoid C c (apex K)) (HomSetoid (FunCat J C) (ConstFunctor c J) F).
 Proof.
-Abort. *)
+Abort.
+*)