Merge branch 'master' into ps/rr/tensor_preserves_coequalizers

theories/Algebra/AbGroups/Abelianization.v

@@ -415,3 +415,28 @@ Proof.
   - exact _.
   - symmetry; apply homotopic_isabelianization.
 Defined.
+
+(** ** Functoriality *)
+
+Global Instance is0functor_abel : Is0Functor abel.
+Proof.
+  snrapply Build_Is0Functor.
+  intros A B f.
+  snrapply grp_homo_abel_rec.
+  refine (_ $o f).
+  exact abel_unit.
+Defined.
+
+Global Instance is1functor_abel : Is1Functor abel.
+Proof.
+  snrapply Build_Is1Functor.
+  - intros A B f g p.
+    unfold abel.
+    rapply Abel_ind_hprop.
+    intros x.
+    exact (ap abel_in (p x)).
+  - intros A.
+    by rapply Abel_ind_hprop.
+  - intros A B C f g.
+    by rapply Abel_ind_hprop.
+Defined.

theories/Algebra/AbGroups/FreeAbelianGroup.v

@@ -1,6 +1,6 @@
 Require Import Basics.Overture Basics.Tactics Basics.Equivalences.
 Require Import Types.Sigma Types.Forall Types.Paths.
-Require Import WildCat.Core WildCat.EquivGpd.
+Require Import WildCat.Core WildCat.EquivGpd WildCat.Universe.
 Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Abelianization.
 Require Import Algebra.Groups.FreeGroup.
 Require Import Spaces.List.Core.
@@ -59,3 +59,7 @@ Proof.
   exists (abel_unit (G:=FreeGroup S) o freegroup_in).
   srapply isfreeabgroupon_isabelianization_isfreegroup.
 Defined.
+
+(** Functoriality follows from the functoriality of [abel] and [FreeGroup]. *)
+Global Instance is0functor_freeabgroup : Is0Functor FreeAbGroup := _.
+Global Instance is1functor_freeabgroup : Is1Functor FreeAbGroup := _.

theories/Algebra/Groups/FreeGroup.v

@@ -1,5 +1,5 @@
 Require Import Basics Types Group Subgroup
-  WildCat.Core Colimits.Coeq
+  WildCat.Core WildCat.Universe Colimits.Coeq
   Truncations.Core Truncations.SeparatedTrunc
   Spaces.List.Core Spaces.List.Theory.
 
@@ -535,3 +535,26 @@ Section FreeGroupGenerated.
   Defined.
 
 End FreeGroupGenerated.
+
+(** ** Functoriality *)
+
+Global Instance is0functor_freegroup : Is0Functor FreeGroup.
+Proof.
+  snrapply Build_Is0Functor.
+  intros X Y f.
+  snrapply FreeGroup_rec.
+  exact (freegroup_in o f).
+Defined.
+
+Global Instance is1functor_freegroup : Is1Functor FreeGroup.
+Proof.
+  snrapply Build_Is1Functor.
+  - intros X Y f g p.
+    snrapply FreeGroup_ind_homotopy.
+    intros x.
+    exact (ap freegroup_in (p x)).
+  - intros X.
+    by snrapply FreeGroup_ind_homotopy.
+  - intros X Y Z f g.
+    by snrapply FreeGroup_ind_homotopy.
+Defined.

theories/Algebra/Groups/QuotientGroup.v

@@ -19,10 +19,10 @@ Local Open Scope wc_iso_scope.
 
 Section GroupCongruenceQuotient.
 
-  Context {G : Group} {R : Relation G}
-    `{is_mere_relation _ R, !IsCongruence R,
-      !Reflexive R, !Symmetric R, !Transitive R}.
+  (** A congruence on a group is a relation satisfying [R x x' -> R y y' -> R (x * y) (x' * y')].  Because we also require that [R] is reflexive, we also know that [R y y' -> R (x * y) (x * y')] for any [x], and similarly for multiplication on the right by [x].  We don't need to assume that [R] is symmetric or transitive. *)
+  Context {G : Group} {R : Relation G} `{!IsCongruence R, !Reflexive R}.
 
+  (** The type underlying the quotient group is [Quotient R]. *)
   Definition CongruenceQuotient := G / R.
 
   Global Instance congquot_sgop : SgOp CongruenceQuotient.
@@ -53,19 +53,21 @@ Section GroupCongruenceQuotient.
 
   Global Instance congquot_negate : Negate CongruenceQuotient.
   Proof.
-    srapply Quotient_functor.
-    1: apply negate.
-    intros x y p.
+    srapply Quotient_rec.
+    1: exact (class_of R o negate).
+    intros x y p; cbn.
+    symmetry.
     rewrite <- (left_identity (-x)).
     destruct (left_inverse y).
     set (-y * y * -x).
     rewrite <- (right_identity (-y)).
     destruct (right_inverse x).
     unfold g; clear g.
     rewrite <- simple_associativity.
+    apply qglue.
     apply iscong; try reflexivity.
     apply iscong; try reflexivity.
-    by symmetry.
+    exact p.
   Defined.
 
   Global Instance congquot_sgop_associative : Associative congquot_sgop.

theories/Basics.v

@@ -8,6 +8,7 @@ Require Export Basics.Utf8.
 Require Export Basics.Notations.
 Require Export Basics.Tactics.
 Require Export Basics.Classes.
+Require Export Basics.Iff.
 
 Require Export Basics.Nat.
 Require Export Basics.Numeral.

theories/Basics/Decidable.v

@@ -3,7 +3,8 @@ Require Import
   Basics.Overture
   Basics.PathGroupoids
   Basics.Trunc
-  Basics.Tactics.
+  Basics.Tactics
+  Basics.Iff.
 Local Open Scope trunc_scope.
 Local Open Scope path_scope.
 
@@ -27,8 +28,9 @@ Ltac decide_type A :=
   end.
 
 Ltac decide :=
-  match goal with
+  multimatch goal with
   | [|- ?A] => decide_type A
+  | [|- ~ ?A] => decide_type A
   end.
 
 Definition decidable_true {A : Type} `{Decidable A}
@@ -84,6 +86,13 @@ Proof.
   exact (nnnp (fun np => np p)).
 Defined.
 
+Definition iff_stable P `(Stable P) : ~~P <-> P.
+Proof.
+  split.
+  - apply stable.
+  - exact (fun x f => f x).
+Defined.
+
 (**
   Because [vm_compute] evaluates terms in [PROP] eagerly
   and does not remove dead code we
@@ -121,21 +130,21 @@ Global Instance decidable_empty : Decidable Empty
 
 (** ** Transfer along equivalences *)
 
-Definition decidable_iff {A B} (f : A -> B) (f' : B -> A)
+Definition decidable_iff {A B} (f : A <-> B)
   : Decidable A -> Decidable B.
 Proof.
   intros [a|na].
-  - exact (inl (f a)).
-  - exact (inr (fun b => na (f' b))).
+  - exact (inl (fst f a)).
+  - exact (inr (fun b => na (snd f b))).
 Defined.
 
-Definition decidable_equiv (A : Type) {B : Type} (f : A -> B) `{IsEquiv A B f}
-  : Decidable A -> Decidable B
-  := decidable_iff f f^-1.
-
 Definition decidable_equiv' (A : Type) {B : Type} (f : A <~> B)
 : Decidable A -> Decidable B
-  := decidable_equiv A f.
+  := decidable_iff f.
+
+Definition decidable_equiv (A : Type) {B : Type} (f : A -> B) `{!IsEquiv f}
+: Decidable A -> Decidable B
+  := decidable_equiv' _ (Build_Equiv _ _ f _).
 
 Definition decidablepaths_equiv
            (A : Type) {B : Type} (f : A -> B) `{IsEquiv A B f}
@@ -260,3 +269,37 @@ Proof.
   - elim (nd d').
   - apply ap, path_forall; intros p; elim (nd p).
 Defined.
+
+(** ** Logical Laws *)
+
+(** Various logical laws don't hold constructively as they do classically due to a required use of excluded middle. For us, this means that some laws require further assumptions on the decidability of propositions. *)
+
+(** Here we give the dual De Morgan's Law which complements the one given in Iff.v.  One direction requires that one of the two propositions be decidable, while the other direction needs no assumption.  We state the latter property first, to avoid duplication in the proof. *)
+Definition not_prod_sum_not A B : ~ A + ~ B -> ~ (A * B).
+Proof.
+  intros [na|nb] [a b].
+  - exact (na a).
+  - exact (nb b).
+Defined.
+
+Definition iff_not_prod A B `{Decidable A}
+  : ~ (A * B) <-> ~ A + ~ B.
+Proof.
+  split.
+  - intros np.
+    destruct (dec A) as [a|na].
+    + exact (inr (fun b => np (a, b))).
+    + exact (inl na).
+  - apply not_prod_sum_not.
+Defined.
+
+Definition iff_not_prod' A B `{Decidable B}
+  : ~ (A * B) <-> ~ A + ~ B.
+Proof.
+  split.
+  - intros np.
+    destruct (dec B) as [b|nb].
+    + exact (inl (fun a => np (a, b))).
+    + exact (inr nb).
+  - apply not_prod_sum_not.
+Defined.

theories/Basics/Equivalences.v

@@ -80,9 +80,6 @@ Ltac change_apply_equiv_compose :=
     change ((f oE g) x) with (f (g x))
   end.
 
-Definition iff_equiv {A B : Type} (f : A <~> B)
-  : A <-> B := (equiv_fun f, f^-1).
-
 (** Transporting is an equivalence. *)
 Section EquivTransport.
 

theories/Basics/Iff.v

@@ -0,0 +1,60 @@
+Require Import Basics.Overture Basics.Tactics.
+
+Local Set Universe Minimization ToSet.
+
+(** * If and only if *)
+
+(** ** Definition *)
+
+(** [iff A B], written [A <-> B], expresses the logical equivalence of [A] and [B] *)
+Definition iff (A B : Type) := prod (A -> B) (B -> A).
+
+Notation "A <-> B" := (iff A B) : type_scope.
+
+(** ** Basic Properties *)
+
+(** Everything is logically equivlaent to itself. *)
+Definition iff_refl {A} : A <-> A
+  := (idmap , idmap).
+
+(** [iff] is a reflexive relation. *)
+Global Instance iff_reflexive : Reflexive iff | 1
+  := @iff_refl.
+
+(** Logical equivalences can be inverted. *)
+Definition iff_inverse {A B} : (A <-> B) -> (B <-> A)
+  :=  fun f => (snd f , fst f).
+
+(** [iff] is a symmetric relation. *)
+Global Instance symmetric_iff : Symmetric iff | 1
+  := @iff_inverse.
+
+(** Logical equivalences can be composed. *)
+Definition iff_compose {A B C} (f : A <-> B) (g : B <-> C) : A <-> C
+  := (fst g o fst f , snd f o snd g).
+
+(** [iff] is a transitive relation. *)
+Global Instance transitive_iff : Transitive iff | 1
+  := @iff_compose.
+
+(** Any equivalence can be considered a logical equivalence by discarding everything but the maps. We make this a coercion so that equivalences can be used in place of logical equivalences. *)
+Coercion iff_equiv {A B : Type} (f : A <~> B)
+  : A <-> B := (equiv_fun f, f^-1).
+
+(** ** Logical Laws *)
+
+(** One of De Morgan's Laws.  The dual statement about negating a product appears in Decidable.v due to decidability requirements. *)
+Definition iff_not_sum A B : ~ (A + B) <-> ~ A * ~ B.
+Proof.
+  split.
+  - intros ns.
+    exact (ns o inl, ns o inr).
+  - by intros []; snrapply sum_ind.
+Defined.
+
+Definition iff_contradiction A : A * ~A <-> Empty.
+Proof.
+  split.
+  - intros [a na]; exact (na a).
+  - intros e; exact (Empty_rec _ e).
+Defined.

theories/Basics/Overture.v

@@ -73,13 +73,6 @@ Notation conj := pair (only parsing).
 
 #[export] Hint Resolve pair inl inr : core.
 
-(** If and only if *)
-
-(** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
-Definition iff (A B : Type) := prod (A -> B) (B -> A).
-
-Notation "A <-> B" := (iff A B) : type_scope.
-
 (** ** Type classes *)
 
 (** This command prevents Coq from trying to guess the values of existential variables while doing typeclass resolution.  If you don't know what that means, ignore it. *)
@@ -224,20 +217,6 @@ Notation "g 'o' f" := (compose g%function f%function) : function_scope.
 (** This definition helps guide typeclass inference. *)
 Definition Compose {A B C : Type} (g : B -> C) (f : A -> B) : A -> C := compose g f.
 
-(** Composition of logical equivalences *)
-Global Instance iff_compose : Transitive iff | 1
-  := fun A B C f g => (fst g o fst f , snd f o snd g).
-Arguments iff_compose {A B C} f g : rename.
-
-(** While we're at it, inverses of logical equivalences *)
-Global Instance iff_inverse : Symmetric iff | 1
-  := fun A B f => (snd f , fst f).
-Arguments iff_inverse {A B} f : rename.
-
-(** And reflexivity of them *)
-Global Instance iff_reflexive : Reflexive iff | 1
-  := fun A => (idmap , idmap).
-
 (** Dependent composition of functions. *)
 Definition composeD {A B C} (g : forall b, C b) (f : A -> B) := fun x : A => g (f x).
 

theories/Basics/Trunc.v

@@ -7,7 +7,8 @@ Require Import
   Basics.Contractible
   Basics.Equivalences
   Basics.Tactics
-  Basics.Nat.
+  Basics.Nat
+  Basics.Iff.
 
 Local Set Universe Minimization ToSet.
 

theories/Categories/Structure/IdentityPrinciple.v

@@ -2,7 +2,7 @@
 Require Import Category.Core Category.Univalent Category.Morphisms.
 Require Import Structure.Core.
 Require Import Types.Sigma Trunc Equivalences.
-Require Import Basics.Tactics.
+Require Import Basics.Iff Basics.Tactics.
 
 Set Universe Polymorphism.
 Set Implicit Arguments.

theories/PropResizing/Nat.v

@@ -149,8 +149,7 @@ Section AssumeStuff.
     Qed.
 
     Definition graph_unsucc_equiv_vert@{} : vert A <~> vert B
-      := equiv_unfunctor_sum_l@{s s s s s  s Set Set Set Set}
-                              f Ha Hb.
+      := equiv_unfunctor_sum_l@{s s s s s s} f Ha Hb.
 
     Definition graph_unsucc_equiv_edge@{} (x y : vert A)
       : iff@{s s s} (edge A x y) (edge B (graph_unsucc_equiv_vert x) (graph_unsucc_equiv_vert y)).

theories/Spaces/Finite/Fin.v

@@ -267,7 +267,7 @@ Proof.
   assert (p' := (moveL_equiv_V _ _ p)^).
   exists y.
   destruct y as [y|[]].
-  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set}
+  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set}
               (fin_transpose_last_with m (inl y) oE e)
               _ _ ; _).
     { intros a. ev_equiv.
@@ -286,7 +286,7 @@ Proof.
     * rewrite unfunctor_sum_l_beta.
       apply fin_transpose_last_with_invol.
     * refine (fin_transpose_last_with_last _ _ @ p^).
-  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set} e _ _ ; _).
+  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set} e _ _ ; _).
     { intros a.
       destruct (is_inl_or_is_inr (e (inl a))) as [l|r].
       - exact l.

theories/Spaces/Int.v

@@ -124,8 +124,9 @@ Proof.
   2-4,6-8: right; intros; discriminate.
   2: by left.
   1,2: nrapply decidable_iff.
-  1,4: nrapply ap.
-  1,3: intros H; by injection H.
+  1,3: split.
+  1,3: nrapply ap.
+  1,2: intros H; by injection H.
   1,2: exact _.
 Defined.