feat(category.constructions): define comma category

hott/algebra/category/constructions/comma.hlean

@@ -0,0 +1,169 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.category.constructions.comma
+Authors: Floris van Doorn, Jakob von Raumer
+
+Comma category
+-/
+
+import ..functor cubical.pathover ..strict ..category
+
+open core eq functor equiv sigma sigma.ops is_trunc cubical iso
+
+namespace category
+
+  structure comma_object {A B C : Precategory} (S : A ⇒ C) (T : B ⇒ C) :=
+    (a : A)
+    (b : B)
+    (f : S a ⟶ T b)
+  abbreviation ob1 := @comma_object.a
+  abbreviation ob2 := @comma_object.b
+  abbreviation mor := @comma_object.f
+
+  variables {A B C : Precategory} (S : A ⇒ C) (T : B ⇒ C)
+
+  definition comma_object_sigma_char : (Σ(a : A) (b : B), S a ⟶ T b) ≃ comma_object S T :=
+  begin
+    fapply equiv.MK,
+    { intro u, exact comma_object.mk u.1 u.2.1 u.2.2},
+    { intro x, cases x with a b f, exact ⟨a, b, f⟩},
+    { intro x, cases x, reflexivity},
+    { intro u, cases u with u1 u2, cases u2, reflexivity},
+  end
+
+  theorem is_trunc_comma_object (n : trunc_index) [HA : is_trunc n A]
+    [HB : is_trunc n B] [H : Π(s d : C), is_trunc n (hom s d)] : is_trunc n (comma_object S T) :=
+  by apply is_trunc_equiv_closed;apply comma_object_sigma_char
+
+  variables {S T}
+  definition comma_object_eq' {x y : comma_object S T} (p : ob1 x = ob1 y) (q : ob2 x = ob2 y)
+    (r : mor x =[ap011 (@hom C C) (ap (to_fun_ob S) p) (ap (to_fun_ob T) q)] mor y) : x = y :=
+  begin
+    cases x with a b f, cases y with a' b' f', cases p, cases q,
+    esimp [ap011,congr,core.ap,subst] at r,
+    eapply (idp_rec_on r), reflexivity
+  end
+
+  -- definition comma_object_eq {x y : comma_object S T} (p : ob1 x = ob1 y) (q : ob2 x = ob2 y)
+  --   (r : T (hom_of_eq q) ∘ mor x ∘ S (inv_of_eq p) = mor y) : x = y :=
+  -- begin
+  --   fapply comma_object_eq' p q,
+  --   --cases x with a b f, cases y with a' b' f', cases p, cases q,
+  --   --esimp [ap011,congr,core.ap,subst] at r,
+  --   --eapply (idp_rec_on r), reflexivity
+  -- end
+
+
+  definition ap_ob1_comma_object_eq' (x y : comma_object S T) (p : ob1 x = ob1 y) (q : ob2 x = ob2 y)
+    (r : mor x =[ap011 (@hom C C) (ap (to_fun_ob S) p) (ap (to_fun_ob T) q)] mor y)
+    : ap ob1 (comma_object_eq' p q r) = p :=
+  begin
+    cases x with a b f, cases y with a' b' f', cases p, cases q,
+    eapply (idp_rec_on r), reflexivity
+  end
+
+  definition ap_ob2_comma_object_eq' (x y : comma_object S T) (p : ob1 x = ob1 y) (q : ob2 x = ob2 y)
+    (r : mor x =[ap011 (@hom C C) (ap (to_fun_ob S) p) (ap (to_fun_ob T) q)] mor y)
+    : ap ob2 (comma_object_eq' p q r) = q :=
+  begin
+    cases x with a b f, cases y with a' b' f', cases p, cases q,
+    eapply (idp_rec_on r), reflexivity
+  end
+
+  structure comma_morphism (x y : comma_object S T) :=
+  mk' ::
+    (g : ob1 x ⟶ ob1 y)
+    (h : ob2 x ⟶ ob2 y)
+    (p : T h ∘ mor x = mor y ∘ S g)
+    (p' : mor y ∘ S g = T h ∘ mor x)
+  abbreviation mor1 := @comma_morphism.g
+  abbreviation mor2 := @comma_morphism.h
+  abbreviation coh  := @comma_morphism.p
+  abbreviation coh' := @comma_morphism.p'
+
+  protected definition comma_morphism.mk [constructor] [reducible]
+    {x y : comma_object S T} (g h p) : comma_morphism x y :=
+  comma_morphism.mk' g h p p⁻¹
+
+  variables (x y z w : comma_object S T)
+  definition comma_morphism_sigma_char :
+    (Σ(g : ob1 x ⟶ ob1 y) (h : ob2 x ⟶ ob2 y), T h ∘ mor x = mor y ∘ S g) ≃ comma_morphism x y :=
+  begin
+    fapply equiv.MK,
+    { intro u, exact (comma_morphism.mk u.1 u.2.1 u.2.2)},
+    { intro f, cases f with g h p p', exact ⟨g, h, p⟩},
+    { intro f, cases f with g h p p', esimp,
+      apply ap (comma_morphism.mk' g h p), apply is_hprop.elim},
+    { intro u, cases u with u1 u2, cases u2 with u2 u3, reflexivity},
+  end
+
+  theorem is_trunc_comma_morphism (n : trunc_index) [H1 : is_trunc n (ob1 x ⟶ ob1 y)]
+    [H2 : is_trunc n (ob2 x ⟶ ob2 y)] [Hp : Πm1 m2, is_trunc n (T m2 ∘ mor x = mor y ∘ S m1)]
+    : is_trunc n (comma_morphism x y) :=
+  by apply is_trunc_equiv_closed; apply comma_morphism_sigma_char
+
+  variables {x y z w}
+  definition comma_morphism_eq {f f' : comma_morphism x y}
+    (p : mor1 f = mor1 f') (q : mor2 f = mor2 f') : f = f' :=
+  begin
+    cases f with g h p₁ p₁', cases f' with g' h' p₂ p₂', cases p, cases q,
+    apply ap011 (comma_morphism.mk' g' h'),
+      apply is_hprop.elim,
+      apply is_hprop.elim
+  end
+
+  definition comma_compose (g : comma_morphism y z) (f : comma_morphism x y) : comma_morphism x z :=
+  comma_morphism.mk
+    (mor1 g ∘ mor1 f)
+    (mor2 g ∘ mor2 f)
+    (by rewrite [+respect_comp,-assoc,coh,assoc,coh,-assoc])
+
+  local infix `∘∘`:60 := comma_compose
+
+  definition comma_id : comma_morphism x x :=
+  comma_morphism.mk id id (by rewrite [+respect_id,id_left,id_right])
+
+  theorem comma_assoc (h : comma_morphism z w) (g : comma_morphism y z) (f : comma_morphism x y) :
+    h ∘∘ (g ∘∘ f) = (h ∘∘ g) ∘∘ f :=
+  comma_morphism_eq !assoc !assoc
+
+  theorem comma_id_left (f : comma_morphism x y) : comma_id ∘∘ f = f :=
+  comma_morphism_eq !id_left !id_left
+
+  theorem comma_id_right (f : comma_morphism x y) : f ∘∘ comma_id = f :=
+  comma_morphism_eq !id_right !id_right
+
+  variables (S T)
+  definition comma_category [constructor] : Precategory :=
+  precategory.MK (comma_object S T)
+                 comma_morphism
+                 (λa b, !is_trunc_comma_morphism)
+                 (@comma_compose _ _ _ _ _)
+                 (@comma_id _ _ _ _ _)
+                 (@comma_assoc _ _ _ _ _)
+                 (@comma_id_left _ _ _ _ _)
+                 (@comma_id_right _ _ _ _ _)
+
+  --TODO: this definition doesn't use category structure of A and B
+  definition strict_precategory_comma [HA : strict_precategory A] [HB : strict_precategory B] :
+    strict_precategory (comma_object S T) :=
+  strict_precategory.mk (comma_category S T) !is_trunc_comma_object
+
+  -- definition is_univalent_comma (HA : is_univalent A) (HB : is_univalent B)
+  --   : is_univalent (comma_category S T) :=
+  -- begin
+  --   intros c d,
+  --   fapply adjointify,
+  --   { intro i, cases i with f s, cases s with g l r, cases f with fA fB fp, cases g with gA gB gp,
+  --     esimp at *, fapply comma_object_eq', unfold is_univalent at (HA, HB),
+  --       {apply iso_of_eq⁻¹ᶠ, exact (iso.MK fA gA (ap mor1 l) (ap mor1 r))},
+  --       {apply iso_of_eq⁻¹ᶠ, exact (iso.MK fB gB (ap mor2 l) (ap mor2 r))},
+  --       { apply sorry}},
+  --   { apply sorry},
+  --   { apply sorry},
+  -- end
+
+
+end category

hott/algebra/category/constructions/default.hlean

@@ -6,4 +6,4 @@ Module: algebra.category.constructions.default
 Authors: Floris van Doorn
 -/
 
-import .functor .hset .opposite .product
+import .functor .hset .opposite .product .comma

hott/algebra/category/constructions/functor.hlean

@@ -14,7 +14,7 @@ open eq functor is_trunc nat_trans iso is_equiv
 
 namespace category
 
-  definition precategory_functor [instance] [reducible] (D C : Precategory)
+  definition precategory_functor [instance] [reducible] [constructor] (D C : Precategory)
     : precategory (functor C D) :=
   precategory.mk (λa b, nat_trans a b)
                  (λ a b c g f, nat_trans.compose g f)

hott/algebra/category/iso.hlean

@@ -139,7 +139,8 @@ namespace iso
 
   attribute to_hom [coercion]
 
-  protected definition MK (f : a ⟶ b) (g : b ⟶ a) (H1 : g ∘ f = id) (H2 : f ∘ g = id) :=
+  protected definition MK [constructor] (f : a ⟶ b) (g : b ⟶ a)
+    (H1 : g ∘ f = id) (H2 : f ∘ g = id) :=
   @mk _ _ _ _ f (is_iso.mk H1 H2)
 
   definition to_inv (f : a ≅ b) : b ⟶ a :=

hott/algebra/category/precategory.hlean

@@ -53,7 +53,7 @@ namespace category
   abbreviation is_hset_hom := @precategory.is_hset_hom
 
   -- the constructor you want to use in practice
-  protected definition precategory.mk {ob : Type} (hom : ob → ob → Type)
+  protected definition precategory.mk [constructor] {ob : Type} (hom : ob → ob → Type)
     [hset : Π (a b : ob), is_hset (hom a b)]
     (comp : Π ⦃a b c : ob⦄, hom b c → hom a b → hom a c) (ID : Π (a : ob), hom a a)
     (ass : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b),
@@ -142,8 +142,8 @@ namespace category
     (carrier : Type)
     (struct : precategory carrier)
 
-  definition precategory.Mk [reducible] {ob} (C) : Precategory := Precategory.mk ob C
-  definition precategory.MK [reducible] (a b c d e f g h) : Precategory :=
+  definition precategory.Mk [reducible] [constructor] {ob} (C) : Precategory := Precategory.mk ob C
+  definition precategory.MK [reducible] [constructor] (a b c d e f g h) : Precategory :=
   Precategory.mk a (@precategory.mk _ b c d e f g h)
 
   abbreviation carrier := @Precategory.carrier

hott/init/default.hlean

@@ -22,6 +22,6 @@ namespace core
   export eq (idp idpath concat inverse transport ap ap10 cast tr_inv homotopy ap11 apd refl)
   export [declarations] function
   export equiv (to_inv to_right_inv to_left_inv)
-  export is_equiv (inv right_inv left_inv)
+  export is_equiv (inv right_inv left_inv adjointify)
   export [abbreviations] [declarations] is_trunc (trunctype hprop.mk hset.mk)
 end core

hott/init/ua.hlean

@@ -58,7 +58,7 @@ namespace equiv
   eq.transport P (ua H)
 
   -- we can "recurse" on equivalences, by replacing them by (equiv_of_eq _)
-  definition rec_on_ua {A B : Type} {P : A ≃ B → Type}
+  definition rec_on_ua [recursor] {A B : Type} {P : A ≃ B → Type}
     (f : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P f :=
   right_inv equiv_of_eq f ▸ H (ua f)