feat(functor): prove sorry's, and shorten some proofs

hott/algebra/category/adjoint.hlean

@@ -52,7 +52,8 @@ namespace category
 
   definition full (F : C ⇒ D) := Π⦃c c' : C⦄ (g : F c ⟶ F c'), ∃(f : c ⟶ c'), F f = g
 
-  definition fully_faithful [reducible] (F : C ⇒ D) := Π⦃c c' : C⦄, is_equiv (@to_fun_hom _ _ F c c')
+  definition fully_faithful [reducible] (F : C ⇒ D) :=
+  Π⦃c c' : C⦄, is_equiv (@(to_fun_hom F) c c')
 
   definition split_essentially_surjective (F : C ⇒ D) :=
   Π⦃d : D⦄, Σ(c : C), F c ≅ d
@@ -103,7 +104,7 @@ namespace category
   sorry
 
   definition full_of_fully_faithful (H : fully_faithful F) : full F :=
-  sorry --λc c' g, trunc.elim _ _
+  sorry --  λc c' g, exists.intro ((@(to_fun_hom F) c c')⁻¹ g) _
 
   definition faithful_of_fully_faithful (H : fully_faithful F) : faithful F :=
   λc c' f f' p, is_injective_of_is_embedding p

hott/algebra/category/functor.hlean

@@ -61,21 +61,12 @@ namespace functor
     {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) (pF : F₁ ∼ F₂)
     (pH : Π(a b : C) (f : hom a b), hom_of_eq (pF b) ∘ H₁ a b f ∘ inv_of_eq (pF a) = H₂ a b f)
       : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ :=
-  functor_mk_eq' id₁ id₂ comp₁ comp₂ (eq_of_homotopy pF)
+  begin
-    (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (λf,
+    fapply functor_mk_eq',
-      begin
+    { exact eq_of_homotopy pF},
-        apply concat, rotate_left 1, exact (pH c c' f),
+    { refine eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (λf, _))), intros,
-        apply concat, rotate_left 1, apply transport_hom,
+      rewrite [+pi_transport_constant,-pH,-transport_hom]}
-        apply concat, rotate_left 1,
+  end
-        exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c c') f),
-        apply (apd10' f),
-        apply concat, rotate_left 1, esimp,
-        exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c) c'),
-        apply (apd10' c'),
-        apply concat, rotate_left 1, esimp,
-        exact (pi_transport_constant (eq_of_homotopy pF) H₁ c),
-        esimp
-      end))))
 
   definition functor_eq {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ ∼ to_fun_ob F₂),
     (Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) → F₁ = F₂ :=
@@ -138,17 +129,9 @@ namespace functor
         exact (S.1), exact (S.2.1),
         -- TODO(Leo): investigate why we need to use relaxed-exact (rexact) tactic here
         exact (pr₁ S.2.2), rexact (pr₂ S.2.2)},
-      {intro F,
+      {intro F, cases F with d1 d2 d3 d4, exact ⟨d1, d2, (d3, @d4)⟩},
-        cases F with d1 d2 d3 d4,
+      {intro F, cases F, reflexivity},
-        exact ⟨d1, d2, (d3, @d4)⟩},
+      {intro S, cases S with d1 S2, cases S2 with d2 P1, cases P1, reflexivity},
-      {intro F,
-        cases F,
-        reflexivity},
-      {intro S,
-        cases S with d1 S2,
-        cases S2 with d2 P1,
-        cases P1,
-        reflexivity},
   end
 
   section
@@ -192,23 +175,20 @@ namespace functor
     exact r,
   end
 
-  -- definition ap010_functor_eq' {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ = to_fun_ob F₂)
+  definition ap010_apd01111_functor {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
-  --   (q : p ▸ F₁ = F₂) (c : C) :
+    {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} {id₁ id₂ comp₁ comp₂}
-  --   ap to_fun_ob (functor_eq (apd10 p) (λa b f, _)) = p := sorry
+    (pF : F₁ = F₂) (pH : pF ▸ H₁ = H₂) (pid : cast (apd011 _ pF pH) id₁ = id₂)
-  -- begin
+    (pcomp : cast (apd0111 _ pF pH pid) comp₁ = comp₂) (c : C)
-  --   cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros p q,
+      : ap010 to_fun_ob (apd01111 functor.mk pF pH pid pcomp) c = ap10 pF c :=
-  --   cases p, clear e_1 e_2,
+  by cases pF; cases pH; cases pid; cases pcomp; apply idp
-  -- end
 
-  -- TODO: remove sorry
+definition ap010_functor_eq {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ∼ to_fun_ob F₂)
-  definition ap010_functor_eq {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ∼ to_fun_ob F₂)
     (q : (λ(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a)) ∼3 to_fun_hom F₂) (c : C) :
     ap010 to_fun_ob (functor_eq p q) c = p c :=
   begin
-    cases F₂, revert q, eapply (homotopy.rec_on p), clear p, esimp, intro p q,
+    cases F₁ with F₁o F₁h F₁id F₁comp, cases F₂ with F₂o F₂h F₂id F₂comp,
-    apply sorry,
+    esimp [functor_eq,functor_mk_eq,functor_mk_eq'],
-    --apply (homotopy3.rec_on q), clear q, intro q,
+    rewrite [ap010_apd01111_functor,↑ap10,{apd10 (eq_of_homotopy p)}right_inv apd10]
-    --cases p, --TODO: report: this fails
   end
 
   definition ap010_functor_mk_eq_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)}
@@ -217,7 +197,10 @@ namespace functor
   ap010 to_fun_ob (functor_mk_eq_constant id₁ id₂ comp₁ comp₂ pH) c = idp :=
   !ap010_functor_eq
 
-  --do we need this theorem?
+  definition ap010_assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) (a : A) :
+    ap010 to_fun_ob (assoc H G F) a = idp :=
+  by apply ap010_functor_mk_eq_constant
+
   definition compose_pentagon (K : D ⇒ E) (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
     (calc K ∘f H ∘f G ∘f F = (K ∘f H) ∘f G ∘f F : functor.assoc
       ... = ((K ∘f H) ∘f G) ∘f F : functor.assoc)
@@ -225,20 +208,21 @@ namespace functor
     (calc K ∘f H ∘f G ∘f F = K ∘f (H ∘f G) ∘f F : ap (λx, K ∘f x) !functor.assoc
       ... = (K ∘f H ∘f G) ∘f F : functor.assoc
       ... = ((K ∘f H) ∘f G) ∘f F : ap (λx, x ∘f F) !functor.assoc) :=
-  sorry
+  begin
-  -- begin
+  have lem1  : Π{F₁ F₂ : A ⇒ D} (p : F₁ = F₂) (a : A),
-  -- apply functor_eq2,
+    ap010 to_fun_ob (ap (λx, K ∘f x) p) a = ap (to_fun_ob K) (ap010 to_fun_ob p a),
-  -- intro a,
+      by intros; cases p; esimp,
-  -- rewrite +ap010_con,
+  have lem2 : Π{F₁ F₂ : B ⇒ E} (p : F₁ = F₂) (a : A),
-  -- -- rewrite +ap010_ap,
+    ap010 to_fun_ob (ap (λx, x ∘f F) p) a = ap010 to_fun_ob p (F a),
-  -- -- apply sorry
+      by intros; cases p; esimp,
-  -- /-to prove this we need a stronger ap010-lemma, something like
+  apply functor_eq2,
-  --     ap010 (λy, to_fun_ob (f y)) (functor_mk_eq_constant ...) c = idp
+  intro a, esimp,
-  --   or something another way of getting ap out of ap010
+  rewrite [+ap010_con,lem1,lem2,
-  -- -/
+            ap010_assoc K H (G ∘f F) a,
-  -- --rewrite +ap010_ap,
+            ap010_assoc (K ∘f H) G F a,
-  -- --unfold functor.assoc,
+            ap010_assoc H G F a,
-  -- --rewrite ap010_functor_mk_eq_constant,
+            ap010_assoc K H G (F a),
-  -- end
+            ap010_assoc K (H ∘f G) F a],
+  end
 
 end functor

hott/arity.hlean

@@ -131,7 +131,7 @@ namespace eq
 
   /- some properties of these variants of ap -/
 
-  -- we only prove what is needed somewhere
+  -- we only prove what we currently need
 
   definition ap010_con (f : X → Πa, B a) (p : x = x') (q : x' = x'') :
     ap010 f (p ⬝ q) a = ap010 f p a ⬝ ap010 f q a :=