Merge branch 'master' into ps/rr/basics_on_homotopy_cofibers

theories/Algebra/AbGroups/AbelianGroup.v

@@ -179,6 +179,13 @@ Proof.
   all: intro A; apply ispointedcat_group.
 Defined.
 
+(** [abgroup_group] is a functor *)
+Global Instance is0functor_abgroup_group : Is0Functor abgroup_group
+  := is0functor_induced _.
+
+Global Instance is1functor_abgroup_group : Is1Functor abgroup_group
+  := is1functor_induced _.
+
 (** Image of group homomorphisms between abelian groups *)
 Definition abgroup_image {A B : AbGroup} (f : A $-> B) : AbGroup
   := Build_AbGroup (grp_image f) _.

theories/Algebra/Groups/Group.v

@@ -453,6 +453,18 @@ Section GroupEquations.
   (** The inverse of the unit is the unit. *)
   Definition grp_inv_unit : mon_unit^ = mon_unit := inverse_mon_unit (G :=G).
 
+  Definition grp_inv_V_gg : x^ * (x * y) = y
+    := grp_assoc _ _ _ @ ap (.* y) (grp_inv_l x) @ grp_unit_l y.
+
+  Definition grp_inv_g_Vg : x * (x^ * y) = y
+    := grp_assoc _ _ _ @ ap (.* y) (grp_inv_r x) @ grp_unit_l y.
+
+  Definition grp_inv_gg_V : (x * y) * y^ = x
+    := (grp_assoc _ _ _)^ @ ap (x *.) (grp_inv_r y) @ grp_unit_r x.
+
+  Definition grp_inv_gV_g : (x * y^) * y = x
+    := (grp_assoc _ _ _)^ @ ap (x *.) (grp_inv_l y) @ grp_unit_r x.
+
 End GroupEquations.
 
 (** ** Cancelation lemmas *)
@@ -508,20 +520,29 @@ Section GroupMovement.
 
   (** *** Moving elements equal to unit. *)
 
-  Definition grp_moveL_1M : x * y^ = mon_unit <~> x = y
+  Definition grp_moveL_1M : x * y^ = 1 <~> x = y
     := equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gM.
 
-  Definition grp_moveL_1V : x * y = mon_unit <~> x = y^
-    := equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gV.
-
-  Definition grp_moveL_M1 : y^ * x = mon_unit <~> x = y
+  Definition grp_moveL_M1 : y^ * x = 1 <~> x = y
     := equiv_concat_r (grp_unit_r _) _ oE grp_moveL_Mg.
+
+  Definition grp_moveL_1V : x * y = 1 <~> x = y^
+    := equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gV.
+
+  Definition grp_moveL_V1 : y * x = 1 <~> x = y^
+    := equiv_concat_r (grp_unit_r _) _ oE grp_moveL_Vg.
 
-  Definition grp_moveR_1M : mon_unit = y * x^ <~> x = y
-    := (equiv_concat_l (grp_unit_l _) _)^-1%equiv oE grp_moveR_gM.
+  Definition grp_moveR_1M : 1 = y * x^ <~> x = y
+    := (equiv_concat_l (grp_unit_l _) _)^-1 oE grp_moveR_gM.
+
+  Definition grp_moveR_M1 : 1 = x^ * y <~> x = y
+    := (equiv_concat_l (grp_unit_r _) _)^-1 oE grp_moveR_Mg.
+
+  Definition grp_moveR_1V : 1 = y * x <~> x^ = y
+    := (equiv_concat_l (grp_unit_l _) _)^-1 oE grp_moveR_gV.
 
-  Definition grp_moveR_M1 : mon_unit = x^ * y <~> x = y
-    := (equiv_concat_l (grp_unit_r _) _)^-1%equiv oE grp_moveR_Mg.
+  Definition grp_moveR_V1 : mon_unit = x * y <~> x^ = y
+    := (equiv_concat_l (grp_unit_r _) _)^-1 oE grp_moveR_Vg.
 
   (** *** Cancelling elements equal to unit. *)
 

theories/Algebra/Groups/Kernel.v

@@ -57,7 +57,7 @@ Defined.
 
 (** ** Characterisation of group embeddings *)
 Proposition equiv_kernel_isembedding `{Univalence} {A B : Group} (f : A $-> B)
-  : (grp_kernel f = trivial_subgroup :> Subgroup A) <~> IsEmbedding f.
+  : (grp_kernel f = trivial_subgroup A :> Subgroup A) <~> IsEmbedding f.
 Proof.
   refine (_ oE (equiv_path_subgroup' _ _)^-1%equiv).
   apply equiv_iff_hprop_uncurried.

theories/Algebra/Groups/ShortExactSequence.v

@@ -52,6 +52,6 @@ Defined.
 (** A complex 0 -> A -> B is purely exact if and only if the kernel of the map A -> B is trivial. *)
 Definition equiv_grp_isexact_kernel `{Univalence} {A B : Group} (f : A $-> B)
   : IsExact purely (grp_trivial_rec A) f
-      <~> (grp_kernel f = trivial_subgroup :> Subgroup _)
+      <~> (grp_kernel f = trivial_subgroup A :> Subgroup _)
   := (equiv_kernel_isembedding f)^-1%equiv
        oE equiv_iff_hprop_uncurried (iff_grp_isexact_isembedding f).

theories/Algebra/Groups/Subgroup.v

@@ -178,7 +178,7 @@ Definition issig_subgroup {G : Group} : _ <~> Subgroup G
   := ltac:(issig).
 
 (** Trivial subgroup *)
-Definition trivial_subgroup {G} : Subgroup G.
+Definition trivial_subgroup G : Subgroup G.
 Proof.
   rapply (Build_Subgroup' (fun x => x = mon_unit)).
   1: reflexivity.
@@ -205,12 +205,16 @@ Proof.
 Defined.
 
 (** Every group is a (maximal) subgroup of itself *)
-Definition maximal_subgroup {G} : Subgroup G.
+Definition maximal_subgroup G : Subgroup G.
 Proof.
   rapply (Build_Subgroup G (fun x => Unit)).
   split; auto; exact _.
 Defined.
 
+(** We wish to coerce a group to its maximal subgroup. However, if we don't explicitly print [maximal_subgroup] things can get confusing, so we mark it as a coercion to be printed. *)
+Coercion maximal_subgroup : Group >-> Subgroup.
+Add Printing Coercion maximal_subgroup.
+
 (** Paths between subgroups correspond to homotopies between the underlying predicates. *) 
 Proposition equiv_path_subgroup `{F : Funext} {G : Group} (H K : Subgroup G)
   : (H == K) <~> (H = K).
@@ -368,7 +372,7 @@ Coercion normalsubgroup_subgroup : NormalSubgroup >-> Subgroup.
 Global Existing Instance normalsubgroup_isnormal.
 
 Definition equiv_symmetric_in_normalsubgroup {G : Group}
-  (N : NormalSubgroup G)
+  (N : Subgroup G) `{!IsNormalSubgroup N}
   : forall x y, N (x * y) <~> N (y * x).
 Proof.
   intros x y.
@@ -377,15 +381,12 @@ Proof.
 Defined.
 
 (** Our definiiton of normal subgroup implies the usual definition of invariance under conjugation. *)
-Definition isnormal_conjugate {G : Group} (N : NormalSubgroup G) {x y : G}
-  : N x -> N (y * x * y^).
+Definition isnormal_conj {G : Group} (N : Subgroup G)
+  `{!IsNormalSubgroup N} {x y : G}
+  : N x <~> N (y * x * y^).
 Proof.
-  intros n.
-  apply isnormal.
-  nrefine (transport N (grp_assoc _ _ _)^ _).
-  nrefine (transport (fun y => N (y * x)) (grp_inv_l _)^ _).
-  nrefine (transport N (grp_unit_l _)^ _).
-  exact n.
+  srefine (equiv_symmetric_in_normalsubgroup N _ _ oE _).
+  by rewrite grp_inv_V_gg.
 Defined.
 
 (** We can show a subgroup is normal if it is invariant under conjugation. *)
@@ -414,7 +415,7 @@ Definition equiv_isnormal_conjugate `{Funext} {G : Group} (N : Subgroup G)
 Proof.
   rapply equiv_iff_hprop.
   - intros is_normal x y.
-    exact (isnormal_conjugate (Build_NormalSubgroup G N is_normal)).
+    rapply isnormal_conj.
   - intros is_normal'.
     by snrapply Build_IsNormalSubgroup'.
 Defined.
@@ -473,7 +474,7 @@ Defined.
 
 (** The property of being the trivial subgroup is useful. *)
 Definition IsTrivialSubgroup {G : Group} (H : Subgroup G) : Type :=
-  forall x, H x <-> trivial_subgroup x.
+  forall x, H x <-> trivial_subgroup G x.
 Existing Class IsTrivialSubgroup.
 
 Global Instance istrivialsubgroup_trivial_subgroup {G : Group}

theories/Algebra/Rings/Ideal.v

@@ -143,7 +143,7 @@ End IdealElements.
 
 (** The trivial subgroup is a left ideal. *)
 Global Instance isleftideal_trivial_subgroup (R : Ring)
-  : IsLeftIdeal (R := R) trivial_subgroup.
+  : IsLeftIdeal (trivial_subgroup R).
 Proof.
   intros r x p.
   rhs_V nrapply (rng_mult_zero_r).
@@ -152,12 +152,12 @@ Defined.
 
 (** The trivial subgroup is a right ideal. *)
 Global Instance isrightideal_trivial_subgroup (R : Ring)
-  : IsRightIdeal (R := R) trivial_subgroup
+  : IsRightIdeal (trivial_subgroup R)
   := isleftideal_trivial_subgroup _.
 
 (** The trivial subgroup is an ideal. *)
 Global Instance isideal_trivial_subgroup (R : Ring)
-  : IsIdeal (R := R) trivial_subgroup
+  : IsIdeal (trivial_subgroup R)
   := {}.
 
 (** We call the trivial subgroup the "zero ideal". *)
@@ -167,17 +167,17 @@ Definition ideal_zero (R : Ring) : Ideal R := Build_Ideal R _ _.
 
 (** The maximal subgroup is a left ideal. *)
 Global Instance isleftideal_maximal_subgroup (R : Ring)
-  : IsLeftIdeal (R := R) maximal_subgroup
+  : IsLeftIdeal (maximal_subgroup R)
   := ltac:(done).
 
 (** The maximal subgroup is a right ideal. *)
 Global Instance isrightideal_maximal_subgroup (R : Ring)
-  : IsRightIdeal (R := R) maximal_subgroup
+  : IsRightIdeal (maximal_subgroup R)
   := isleftideal_maximal_subgroup _.
 
 (** The maximal subgroup is an ideal.  *)
 Global Instance isideal_maximal_subgroup (R : Ring)
-  : IsIdeal (R:=R) maximal_subgroup
+  : IsIdeal (maximal_subgroup R)
   := {}.
 
 (** We call the maximal subgroup the "unit ideal". *)

theories/Basics/Decidable.v

@@ -72,26 +72,49 @@ Global Existing Instance dec_paths.
 
 Class Stable P := stable : ~~P -> P.
 
-Global Instance stable_decidable P `{!Decidable P} : Stable P.
+(** We always have a map in the other direction. *)
+Definition not_not_unit {P : Type} : P -> ~~P
+  := fun x np => np x.
+
+Global Instance ishprop_stable_hprop `{Funext} P `{IsHProp P} : IsHProp (Stable P)
+  := istrunc_forall.
+
+Global Instance stable_decidable P `{Decidable P} : Stable P.
 Proof.
-  intros dn;destruct (dec P) as [p|n].
-  - assumption.
-  - apply Empty_rect,dn,n.
-Qed.
+  intros dn.
+  (* [dec P] either solves the goal or contradicts [dn]. *)
+  by destruct (dec P).
+Defined.
 
 Global Instance stable_negation P : Stable (~ P).
 Proof.
   intros nnnp p.
-  exact (nnnp (fun np => np p)).
+  exact (nnnp (not_not_unit p)).
 Defined.
 
 Definition iff_stable P `(Stable P) : ~~P <-> P.
 Proof.
   split.
   - apply stable.
-  - exact (fun x f => f x).
+  - exact not_not_unit.
+Defined.
+
+Definition stable_iff {A B} (f : A <-> B)
+  : Stable A -> Stable B.
+Proof.
+  intros stableA nnb.
+  destruct f as [f finv].
+  exact (f (stableA (fun na => nnb (fun b => na (finv b))))).
 Defined.
 
+Definition stable_equiv' {A B} (f : A <~> B)
+  : Stable A -> Stable B
+  := stable_iff f.
+
+Definition stable_equiv {A B} (f : A -> B) `{!IsEquiv f}
+  : Stable A -> Stable B
+  := stable_equiv' (Build_Equiv _ _ f _).
+
 (**
   Because [vm_compute] evaluates terms in [PROP] eagerly
   and does not remove dead code we

theories/Colimits/Pushout.v

@@ -168,6 +168,27 @@ Proof.
     apply ap, q.
 Defined.
 
+Definition functor_pushout_beta_pglue
+  {A B C} {f : A -> B} {g : A -> C}
+  {A' B' C'} {f' : A' -> B'} {g' : A' -> C'}
+  {h : A -> A'} {k : B -> B'} {l : C -> C'}
+  {p : k o f == f' o h} {q : l o g == g' o h}
+  (a : A)
+  : ap (functor_pushout h k l p q) (pglue a)
+    = ap pushl (p a) @ pglue (h a) @ ap pushr (q a)^.
+Proof.
+  lhs nrapply functor_coeq_beta_cglue.
+  symmetry.
+  snrapply ap011.
+  - apply whiskerR.
+    unfold pushl.
+    nrapply ap_compose.
+  - unfold pushr.
+    lhs nrapply ap_compose.
+    apply ap.
+    nrapply ap_V.
+Defined.
+
 Lemma functor_pushout_homotopic
   {A B C : Type} {f : A -> B} {g : A -> C}
   {A' B' C' : Type} {f' : A' -> B'} {g' : A' -> C'}
@@ -189,6 +210,44 @@ Proof.
   exact (j b).
 Defined.
 
+Definition functor_pushout_idmap {A B C : Type} {f : A -> B} {g : A -> C}
+  : functor_pushout (f:=f) (g:=g) idmap idmap idmap (fun _ => 1) (fun _ => 1) == idmap.
+Proof.
+  snrapply Pushout_ind.
+  1,2: reflexivity.
+  simpl.
+  intros a.
+  nrapply transport_paths_Flr'.
+  nrapply moveR_pM.
+  nrapply functor_pushout_beta_pglue.
+Defined.
+
+Definition functor_pushout_compose
+  {A B C f g A' B' C' f' g' A'' B'' C'' f'' g''}
+  (u : A -> A') (v : B -> B') (w : C -> C')
+  (u' : A' -> A'') (v' : B' -> B'') (w' : C' -> C'')
+  (p : v o f == f' o u) (q : w o g == g' o u)
+  (p' : v' o f' == f'' o u') (q' : w' o g' == g'' o u')
+  : functor_pushout (u' o u) (v' o v) (w' o w)
+      (fun x => ap v' (p x) @ p' (u x)) (fun x => ap w' (q x) @ q' (u x))
+    == functor_pushout u' v' w' p' q'
+      o functor_pushout u v w p q.
+Proof.
+  intros a.
+  rhs_V nrapply functor_coeq_compose.
+  snrapply functor_coeq_homotopy.
+  1: reflexivity.
+  1: apply functor_sum_compose.
+  1,2: intros x; simpl.
+  1,2: apply equiv_1p_q1.
+  1,2: lhs_V nrapply whiskerR.
+  1,3: nrapply ap_compose.
+  1,2: simpl.
+  1,2: lhs nrapply whiskerR.
+  1,3: nrapply ap_compose.
+  1,2: symmetry.
+  1,2: apply ap_pp.
+Defined.
 
 (** ** Equivalences *)
 

theories/Metatheory/TruncImpliesFunext.v

@@ -3,15 +3,15 @@
 Require Import HoTT.Basics HoTT.Truncations HoTT.Types.Bool.
 Require Import Metatheory.Core Metatheory.FunextVarieties Metatheory.ImpredicativeTruncation.
 
-(** ** An approach using the truncations defined as HITs *)
+(** Assuming that we have a propositional truncation operation with a definitional computation rule, we can prove function extensionality.  Since we can't assume we have a definitional computation rule, we work with the propositional truncation defined as a HIT, which does have a definitional computation rule. *)
 
 (** We can construct an interval type as [Trunc -1 Bool]. *)
 Local Definition interval := Trunc (-1) Bool.
 
 Local Definition interval_rec (P : Type) (a b : P) (p : a = b)
   : interval -> P.
 Proof.
-  (** We define this map by factoring it through the type [{ x : P & x = b}], which is a proposition since it is contractible. *)
+  (* We define this map by factoring it through the type [{ x : P & x = b}], which is a proposition since it is contractible. *)
   refine ((pr1 : { x : P & x = b } -> P) o _).
   apply Trunc_rec.
   intros [].
@@ -22,15 +22,15 @@ Defined.
 Local Definition seg : tr true = tr false :> interval
   := path_ishprop _ _.
 
-(** From an interval type, and thus from truncations, we can prove function extensionality. *)
+(** From an interval type, and thus from truncations, we can prove function extensionality. See IntervalImpliesFunext.v for an approach that works with an interval defined as a HIT. *)
 Definition funext_type_from_trunc : Funext_type
   := WeakFunext_implies_Funext (NaiveFunext_implies_WeakFunext
     (fun A P f g p =>
       let h := fun (x:interval) (a:A) =>
         interval_rec _ (f a) (g a) (p a) x
         in ap h seg)).
 
-(** ** An approach without using HITs *)
+(** ** Function extensionality implies an interval type *)
 
 (** Assuming [Funext] (and not propositional resizing), the construction [Trm] in ImpredicativeTruncation.v applied to [Bool] gives an interval type with definitional computation on the end points.  So we see that function extensionality is equivalent to the existence of an interval type. *)