Library UniMath.CategoryTheory.RepresentableFunctors.Precategories
Require Export UniMath.CategoryTheory.Core.Categories. Require Export UniMath.CategoryTheory.Core.Isos. Require Export UniMath.CategoryTheory.Core.Functors.
Require Export UniMath.CategoryTheory.Core.NaturalTransformations.
Require Export UniMath.CategoryTheory.Core.Univalence.
Require Export UniMath.CategoryTheory.opp_precat
UniMath.CategoryTheory.yoneda
UniMath.CategoryTheory.categories.HSET.Core
UniMath.CategoryTheory.categories.HSET.MonoEpiIso.
Require Export UniMath.Foundations.Preamble.
Require Export UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Local Open Scope cat.
Notation "a <-- b" := (@precategory_morphisms (opp_precat _) a b) : cat.
Definition src {C:precategory} {a b:C} (f:a-->b) : C := a.
Definition tar {C:precategory} {a b:C} (f:a-->b) : C := b.
Definition hom (C:precategory_data) : ob C -> ob C -> UU :=
λ c c', c --> c'.
Definition Hom (C : category) : ob C -> ob C -> hSet :=
λ c c', make_hSet (c --> c') (homset_property C _ _ ).
Ltac eqn_logic :=
abstract (
repeat (
try reflexivity;
try intro; try split; try apply id_right;
try apply id_left; try apply assoc;
try apply funextsec;
try apply homset_property;
try apply isasetunit;
try apply isapropunit;
try refine (two_arg_paths_f _ _);
try refine (total2_paths_f _ _);
try refine (nat_trans_ax _ _ _ _);
try refine (! nat_trans_ax _ _ _ _);
try apply functor_id;
try apply functor_comp;
try apply isaprop_is_nat_trans
)) using _L_.
Ltac set_logic :=
abstract (repeat (
try intro;
try apply isaset_total2;
try apply isasetdirprod;
try apply homset_property;
try apply impred_isaset;
try apply isasetaprop)) using _M_.
Notation "[ C , D ]" := (functor_category C D) : cat.
Definition oppositecategory (C : category) : category.
Show proof.
Notation "C '^op'" := (oppositecategory C) (at level 3, format "C ^op") : cat.
Definition precategory_obmor (C:precategory) : precategory_ob_mor :=
precategory_ob_mor_from_precategory_data (
precategory_data_from_precategory C).
Definition Functor_obmor {C D} (F:functor C D) := pr1 F.
Definition Functor_obj {C D} (F:functor C D) := pr1 (pr1 F).
Definition Functor_mor {C D} (F:functor C D) := pr2 (pr1 F).
Definition Functor_identity {C D} (F:functor C D) := functor_id F.
Definition Functor_compose {C D} (F:functor C D) := @functor_comp _ _ F.
Definition theUnivalenceProperty (C: univalent_category) := pr2 C : is_univalent C.
embeddings and isomorphism of categories
Definition categoryEmbedding (B C : category) := ∑ F:[B,C], fully_faithful F.
Definition embeddingToFunctor (B C : category) :
categoryEmbedding B C -> B ⟶ C
:= pr1.
Coercion embeddingToFunctor : categoryEmbedding >-> functor.
Definition categoryIsomorphism (B C : category) :=
∑ F:categoryEmbedding B C, isweq ((pr1 F : B ⟶ C) : ob B -> ob C).
Definition isomorphismToEmbedding (B C:category) :
categoryIsomorphism B C -> categoryEmbedding B C
:= pr1.
Coercion isomorphismToEmbedding : categoryIsomorphism >-> categoryEmbedding.
Definition isomorphismOnMor {B C:category} (F:categoryIsomorphism B C)
(b b':B) : Hom B b b' ≃ Hom C (F b) (F b')
:= make_weq _ (pr2 (pr1 F) b b').
Definition makecategory_ob_mor
(obj : UU)
(mor : obj -> obj -> UU) : precategory_ob_mor
:= make_precategory_ob_mor obj (λ i j:obj, mor i j).
Definition makecategory_data
(obj : UU)
(mor : obj -> obj -> UU)
(identity : ∏ i, mor i i)
(compose : ∏ i j k (f:mor i j) (g:mor j k), mor i k)
: precategory_data
:= make_precategory_data (makecategory_ob_mor obj mor) identity compose.
Definition makeFunctor {C D:category}
(obj : C -> D)
(mor : ∏ c c' : C, c --> c' -> obj c --> obj c')
(identity : ∏ c, mor c c (identity c) = identity (obj c))
(compax : ∏ (a b c : C) (f : a --> b) (g : b --> c),
mor a c (g ∘ f) = mor b c g ∘ mor a b f) :
C ⟶ D
:= (obj,, mor),, identity,, compax.
notation for dealing with functors, natural transformations, etc.
Definition functor_object_application {B C:category} (F : [B,C]) (b:B) : C
:= (F:_⟶_) b.
Notation "F ◾ b" := (functor_object_application F b) : cat.
Definition functor_mor_application {B C:category} {b b':B} (F:[B,C]) :
b --> b' -> F ◾ b --> F ◾ b'
:= λ f, # (F:_⟶_) f.
Notation "F ▭ f" := (functor_mor_application F f) : cat.
Definition arrow {C:category} (c : C) (X : [C^op,HSET]) : hSet := X ◾ c.
Notation "c ⇒ X" := (arrow c X) : cat.
Definition arrow' {C:category} (c : C) (X : [C^op^op,HSET]) : hSet := X ◾ c.
Notation "X ⇐ c" := (arrow' c X) : cat.
Definition arrow_morphism_composition {C:category} {c' c:C} {X:[C^op,HSET]} :
c'-->c -> c⇒X -> c'⇒X
:= λ f x, # (X:_⟶_) f x.
Notation "x ⟲ f" := (arrow_morphism_composition f x) (at level 50, left associativity) : cat.
Definition nattrans_arrow_composition {C:category} {X X':[C^op,HSET]} {c:C} :
c⇒X -> X-->X' -> c⇒X'
:= λ x q, (q:_ ⟹ _) c (x:(X:_⟶_) c:hSet).
Notation "q ⟳ x" := (nattrans_arrow_composition x q) (at level 50, left associativity) : cat.
Definition nattrans_object_application {B C:category} {F F' : [B,C]} (b:B) :
F --> F' -> F ◾ b --> F' ◾ b
:= λ p, (p:_ ⟹ _) b.
Notation "p ◽ b" := (nattrans_object_application b p) : cat.
Definition arrow_mor_id {C:category} {c:C} {X:[C^op,HSET]} (x:c⇒X) :
x ⟲ identity c = x
:= eqtohomot (functor_id X c) x.
Definition arrow_mor_mor_assoc {C:category} {c c' c'':C} {X:[C^op,HSET]}
(g:c''-->c') (f:c'-->c) (x:c⇒X) :
x ⟲ (f ∘ g) = (x ⟲ f) ⟲ g
:= eqtohomot (functor_comp X f g) x.
Definition nattrans_naturality {B C:category} {F F':[B, C]} {b b':B}
(p : F --> F') (f : b --> b') :
p ◽ b' ∘ F ▭ f = F' ▭ f ∘ p ◽ b
:= nat_trans_ax p _ _ f.
Definition comp_func_on_mor {A B C:category} (F:[A,B]) (G:[B,C]) {a a':A} (f:a-->a') :
F ∙ G ▭ f = G ▭ (F ▭ f).
Show proof.
reflexivity.
Definition nattrans_arrow_mor_assoc {C:category} {c' c:C} {X X':[C^op,HSET]}
(g:c'-->c) (x:c⇒X) (p:X-->X') :
p ⟳ (x ⟲ g) = (p ⟳ x) ⟲ g
:= eqtohomot (nat_trans_ax p _ _ g) x.
Definition nattrans_arrow_id {C:category} {c:C} {X:[C^op,HSET]} (x:c⇒X) :
nat_trans_id _ ⟳ x = x
:= idpath _.
Definition nattrans_nattrans_arrow_assoc {C:category} {c:C} {X X' X'':[C^op,HSET]}
(x:c⇒X) (p:X-->X') (q:X'-->X'') :
q ⟳ (p ⟳ x) = (q ∘ p) ⟳ x
:= idpath _.
Definition nattrans_nattrans_object_assoc {A B C:category}
(F:[A,B]) (G:[B, C]) {a a' : A} (f : a --> a') :
F ∙ G ▭ f = G ▭ (F ▭ f)
:= idpath _.
Lemma functor_on_id {B C:category} (F:[B,C]) (b:B) : F ▭ identity b = identity (F ◾ b).
Show proof.
Lemma functor_on_comp {B C:category} (F:[B,C]) {b b' b'':B} (g:b'-->b'') (f:b-->b') :
F ▭ (g ∘ f) = F ▭ g ∘ F ▭ f.
Show proof.
natural transformations and isomorphisms
Definition nat_iso {B C:category} (F G:[B,C]) := z_iso F G.
Definition makeNattrans {C D:category} {F G:[C,D]}
(mor : ∏ x : C, F ◾ x --> G ◾ x)
(eqn : ∏ c c' f, mor c' ∘ F ▭ f = G ▭ f ∘ mor c) :
F --> G
:= (mor,,eqn).
Definition makeNattrans_op {C D:category} {F G:[C^op,D]}
(mor : ∏ x : C, F ◾ x --> G ◾ x)
(eqn : ∏ c c' f, mor c' ∘ F ▭ f = G ▭ f ∘ mor c) :
F --> G
:= (mor,,eqn).
Definition makeNatiso {C D:category} {F G:[C,D]}
(mor : ∏ x : C, z_iso (F ◾ x) (G ◾ x))
(eqn : ∏ c c' f, mor c' ∘ F ▭ f = G ▭ f ∘ mor c) :
nat_iso F G.
Show proof.
Definition makeNatiso_op {C D:category} {F G:[C^op,D]}
(mor : ∏ x : C, z_iso (F ◾ x) (G ◾ x))
(eqn : ∏ c c' f, mor c' ∘ F ▭ f = G ▭ f ∘ mor c) :
nat_iso F G.
Show proof.
Lemma move_inv {C:category} {a a' b' b:C} {f : a --> b} {f' : a' --> b'}
{i : a --> a'} {i' : a' --> a} {j : b --> b'} {j' : b' --> b} :
is_inverse_in_precat i i' -> is_inverse_in_precat j j' ->
j ∘ f = f' ∘ i -> j' ∘ f' = f ∘ i'.
Show proof.
intros I J r. rewrite <- id_right. rewrite (! pr1 J). rewrite assoc.
apply (maponpaths (λ k, j' ∘ k)). rewrite <- assoc. rewrite r.
rewrite assoc. rewrite (pr2 I). rewrite id_left. reflexivity.
apply (maponpaths (λ k, j' ∘ k)). rewrite <- assoc. rewrite r.
rewrite assoc. rewrite (pr2 I). rewrite id_left. reflexivity.
Lemma weq_iff_z_iso_SET {X Y:HSET} (f:X-->Y) : is_z_isomorphism f <-> isweq f.
Show proof.
split.
- intro i. set (F := make_z_iso' f i).
refine (isweq_iso f (inv_from_z_iso F)
(λ x, eqtohomot (z_iso_inv_after_z_iso F) x)
(λ y, eqtohomot (z_iso_after_z_iso_inv F) y)).
- intro i.
apply (hset_equiv_is_z_iso X Y (_,,i)).
- intro i. set (F := make_z_iso' f i).
refine (isweq_iso f (inv_from_z_iso F)
(λ x, eqtohomot (z_iso_inv_after_z_iso F) x)
(λ y, eqtohomot (z_iso_after_z_iso_inv F) y)).
- intro i.
apply (hset_equiv_is_z_iso X Y (_,,i)).
Lemma weq_to_iso_SET {X Y:HSET} : z_iso X Y ≃ ((X:hSet) ≃ (Y:hSet)).
Show proof.
intros. apply weqfibtototal; intro f. apply weqiff.
- apply weq_iff_z_iso_SET.
- apply isaprop_is_z_isomorphism.
- apply isapropisweq.
- apply weq_iff_z_iso_SET.
- apply isaprop_is_z_isomorphism.
- apply isapropisweq.
Definition functor_to_opp_opp {C:category} : C ⟶ C^op^op
:= makeFunctor (λ c,c) (λ a b f,f) (λ c, idpath _) (λ a b c f g, idpath _).
Definition makeFunctor_op {C D:category}
(obj : ob C -> ob D)
(mor : ∏ a b : C, b --> a -> obj a --> obj b)
(identity : ∏ c, mor c c (identity c) = identity (obj c))
(compax : ∏ (a b c : C) (f : b --> a) (g : c --> b),
mor a c (f ∘ g) = mor b c g ∘ mor a b f) :
C^op ⟶ D
:= (obj,, mor),, identity,, compax.
Definition opp_ob {C:category} : ob C -> ob C^op
:= λ c, c.
Definition rm_opp_ob {C:category} : ob C^op -> ob C
:= λ c, c.
Definition opp_mor {C:category} {b c:C} : Hom C b c -> Hom C^op c b
:= λ f, f.
Definition rm_opp_mor {C:category} {b c:C} : Hom C^op b c -> Hom C c b
:= λ f, f.
Definition opp_mor_eq {C:category} {a b:C} (f g:a --> b) :
opp_mor f = opp_mor g -> f = g
:= idfun _.
Lemma opp_opp_precat_ob_mor (C : precategory_ob_mor) : C = opp_precat_ob_mor (opp_precat_ob_mor C).
Show proof.
induction C as [ob mor]. reflexivity.
Lemma opp_opp_precat_ob_mor_compute (C : precategory_ob_mor) :
idpath _ = maponpaths precategory_id_comp (opp_opp_precat_ob_mor C).
Show proof.
induction C as [ob mor]. reflexivity.
Lemma opp_opp_precat_data (C : precategory_data)
: C = opp_precat_data (opp_precat_data C).
Show proof.
induction C as [[ob mor] [id co]]. reflexivity.
Lemma opp_opp_precat (C:category) : C = C^op^op.
Show proof.
Definition functorOp {B C : category} : [B, C] ^op ⟶ [B ^op, C ^op].
Show proof.
unshelve refine (makeFunctor _ _ _ _).
{ exact functor_opp. }
{ intros H I p. exists (λ b, pr1 p b).
abstract (intros b b' f; simpl; exact (! nat_trans_ax p _ _ f)) using _L_. }
{ abstract (intros H; now apply (nat_trans_eq (homset_property _))). }
{ abstract (intros H J K p q; now apply (nat_trans_eq (homset_property _))). }
{ exact functor_opp. }
{ intros H I p. exists (λ b, pr1 p b).
abstract (intros b b' f; simpl; exact (! nat_trans_ax p _ _ f)) using _L_. }
{ abstract (intros H; now apply (nat_trans_eq (homset_property _))). }
{ abstract (intros H J K p q; now apply (nat_trans_eq (homset_property _))). }
Definition functorOp' {B C:category} : [B,C] ⟶ [B^op,C^op]^op.
Show proof.
Definition functorRmOp {B C : category} : [B ^op, C ^op] ⟶ [B, C] ^op.
Show proof.
unshelve refine (makeFunctor _ _ _ _).
{ exact functor_opp. }
{ intros H I p. exists (λ b, pr1 p b).
abstract (intros b b' f; simpl; exact (! nat_trans_ax p _ _ f)) using _L_. }
{ abstract (intros H; now apply (nat_trans_eq (homset_property _))) using _L_. }
{ abstract (intros H J K p q; now apply (nat_trans_eq (homset_property _))). }
{ exact functor_opp. }
{ intros H I p. exists (λ b, pr1 p b).
abstract (intros b b' f; simpl; exact (! nat_trans_ax p _ _ f)) using _L_. }
{ abstract (intros H; now apply (nat_trans_eq (homset_property _))) using _L_. }
{ abstract (intros H J K p q; now apply (nat_trans_eq (homset_property _))). }
Definition functorMvOp {B C:category} : [B,C^op] ⟶ [B^op,C]^op.
Show proof.
unshelve refine (makeFunctor _ _ _ _).
{ exact functor_opp. }
{ intros H I p. exists (λ b, pr1 p b).
abstract (intros b b' f; simpl; exact (! nat_trans_ax p _ _ f)) using _L_. }
{ abstract (intros H; now apply (nat_trans_eq (homset_property _))). }
{ abstract (intros H J K p q; now apply (nat_trans_eq (homset_property _))). }
{ exact functor_opp. }
{ intros H I p. exists (λ b, pr1 p b).
abstract (intros b b' f; simpl; exact (! nat_trans_ax p _ _ f)) using _L_. }
{ abstract (intros H; now apply (nat_trans_eq (homset_property _))). }
{ abstract (intros H J K p q; now apply (nat_trans_eq (homset_property _))). }
Lemma functorOpIso {B C:category} : categoryIsomorphism [B, C]^op [B^op, C^op].
Show proof.
unshelve refine (_,,_).
{ unshelve refine (_,,_).
{ exact functorOp. }
{ intros H H'. unshelve refine (isweq_iso _ _ _ _).
{ simpl. intros p. unshelve refine (makeNattrans _ _).
{ intros b. exact (pr1 p b). }
{ abstract (intros b b' f; simpl; exact (!nat_trans_ax p _ _ f)) using _L_. } }
{ abstract (intro p; apply nat_trans_eq;
[ apply homset_property
| intro b; reflexivity ]) using _L_. }
{ abstract (intro p; apply nat_trans_eq;
[ apply homset_property
| intro b; reflexivity ]) using _L_. }}}
{ simpl. unshelve refine (isweq_iso _ _ _ _).
{ exact (functor_opp : B^op ⟶ C^op -> B ⟶ C). }
{ abstract (intros H; simpl; apply (functor_eq _ _ (homset_property C));
unshelve refine (total2_paths_f _ _); reflexivity) using _L_. }
{ abstract (intros H; simpl; apply functor_eq;
[ exact (homset_property C^op)
| unshelve refine (total2_paths_f _ _); reflexivity]). } }
{ unshelve refine (_,,_).
{ exact functorOp. }
{ intros H H'. unshelve refine (isweq_iso _ _ _ _).
{ simpl. intros p. unshelve refine (makeNattrans _ _).
{ intros b. exact (pr1 p b). }
{ abstract (intros b b' f; simpl; exact (!nat_trans_ax p _ _ f)) using _L_. } }
{ abstract (intro p; apply nat_trans_eq;
[ apply homset_property
| intro b; reflexivity ]) using _L_. }
{ abstract (intro p; apply nat_trans_eq;
[ apply homset_property
| intro b; reflexivity ]) using _L_. }}}
{ simpl. unshelve refine (isweq_iso _ _ _ _).
{ exact (functor_opp : B^op ⟶ C^op -> B ⟶ C). }
{ abstract (intros H; simpl; apply (functor_eq _ _ (homset_property C));
unshelve refine (total2_paths_f _ _); reflexivity) using _L_. }
{ abstract (intros H; simpl; apply functor_eq;
[ exact (homset_property C^op)
| unshelve refine (total2_paths_f _ _); reflexivity]). } }
Definition functorOpEmb {B C:category} : categoryEmbedding [B, C]^op [B^op, C^op]
:= pr1 functorOpIso.
Lemma functor_op_rm_op_eq {C D:category} (F : C^op ⟶ D^op) :
functorOp (functorRmOp F) = F.
Show proof.
Lemma functor_rm_op_op_eq {C D:category} (F : C ⟶ D) :
functorRmOp (functorOp F) = F.
Show proof.
Lemma functor_op_op_eq {C D:category} (F : C ⟶ D) :
functorOp (functorOp F) = F.
Show proof.
Definition categoryWithStructure (C:category) (P:ob C -> UU) : category.
Show proof.
use makecategory.
- exact (∑ c:C, P c).
- intros x y. exact (pr1 x --> pr1 y).
- intros. apply homset_property.
- intros x. apply identity.
- intros x y z f g. exact (g ∘ f).
- intros. apply id_left.
- intros. apply id_right.
- intros. apply assoc.
- intros. apply assoc'.
- exact (∑ c:C, P c).
- intros x y. exact (pr1 x --> pr1 y).
- intros. apply homset_property.
- intros x. apply identity.
- intros x y z f g. exact (g ∘ f).
- intros. apply id_left.
- intros. apply id_right.
- intros. apply assoc.
- intros. apply assoc'.
Definition functorWithStructures {C:category} {P Q:ob C -> UU}
(F : ∏ c, P c -> Q c) : categoryWithStructure C P ⟶ categoryWithStructure C Q.
Show proof.
unshelve refine (makeFunctor _ _ _ _).
- exact (λ c, (pr1 c,, F (pr1 c) (pr2 c))).
- intros c c' f. exact f.
- reflexivity.
- reflexivity.
- exact (λ c, (pr1 c,, F (pr1 c) (pr2 c))).
- intros c c' f. exact f.
- reflexivity.
- reflexivity.
Definition addStructure {B C:category} {P:ob C -> UU}
(F:B⟶C) (h : ∏ b, P(F b)) : B ⟶ categoryWithStructure C P.
Show proof.
unshelve refine (makeFunctor _ _ _ _).
- intros b. exact (F b,,h b).
- intros b b' f. exact (# F f).
- abstract (intros b; simpl; apply functor_id) using _L_.
- abstract (intros b b' b'' f g; simpl; apply functor_comp) using _L_.
- intros b. exact (F b,,h b).
- intros b b' f. exact (# F f).
- abstract (intros b; simpl; apply functor_id) using _L_.
- abstract (intros b b' b'' f g; simpl; apply functor_comp) using _L_.
Lemma identityFunction : ∏ (T:HSET) (f:T-->T) (t:T:hSet), f = identity T -> f t = t.
Show proof.
Lemma identityFunction' : ∏ (T:HSET) (t:T:hSet), identity T t = t.
Show proof.
reflexivity.
Lemma functor_identity_object {C:category} (c:C) : functor_identity C ◾ c = c.
Show proof.
reflexivity.
Lemma functor_identity_arrow {C:category} {c c':C} (f:c-->c') : functor_identity C ▭ f = f.
Show proof.
reflexivity.
Definition constantFunctor (C:category) {D:category} (d:D) : [C,D].
Show proof.
unshelve refine (makeFunctor _ _ _ _).
- exact (λ _, d).
- intros c c' f; simpl. exact (identity d).
- intros c; simpl. reflexivity.
- abstract (simpl; intros a b c f g; apply pathsinv0, id_left) using _L_.
- exact (λ _, d).
- intros c c' f; simpl. exact (identity d).
- intros c; simpl. reflexivity.
- abstract (simpl; intros a b c f g; apply pathsinv0, id_left) using _L_.
Definition functor_composite_functor {A B C:category} (F:A⟶B) :
[B,C] ⟶ [A,C].
Show proof.
unshelve refine (makeFunctor _ _ _ _).
- exact (λ G, F ∙ G).
- intros G G' p; simpl.
unshelve refine (@makeNattrans A C (F ∙ G) (F ∙ G') (λ a, p ◽ (F ◾ a)) _).
abstract (
intros a a' f; rewrite 2? nattrans_nattrans_object_assoc;
exact (nattrans_naturality p (F ▭ f))) using _L_.
- abstract (
intros G; now apply (nat_trans_eq (homset_property C))) using _M_.
- abstract (
intros G G' G'' p q; now apply (nat_trans_eq (homset_property C))) using _N_.
- exact (λ G, F ∙ G).
- intros G G' p; simpl.
unshelve refine (@makeNattrans A C (F ∙ G) (F ∙ G') (λ a, p ◽ (F ◾ a)) _).
abstract (
intros a a' f; rewrite 2? nattrans_nattrans_object_assoc;
exact (nattrans_naturality p (F ▭ f))) using _L_.
- abstract (
intros G; now apply (nat_trans_eq (homset_property C))) using _M_.
- abstract (
intros G G' G'' p q; now apply (nat_trans_eq (homset_property C))) using _N_.
Definition ZeroMaps (C:category) :=
∑ (zero : ∏ a b:C, a --> b),
(∏ a b c, ∏ f:b --> c, f ∘ zero a b = zero a c)
×
(∏ a b c, ∏ f:c --> b, zero b a ∘ f = zero c a).
Definition is {C:category} (zero: ZeroMaps C) {a b:C} (f:a-->b)
:= f = pr1 zero _ _.
Definition ZeroMaps_opp (C:category) : ZeroMaps C -> ZeroMaps C^op
:= λ z, (λ a b, pr1 z b a) ,, pr2 (pr2 z) ,, pr1 (pr2 z).
Definition ZeroMaps_opp_opp (C:category) (zero:ZeroMaps C) :
ZeroMaps_opp C^op (ZeroMaps_opp C zero) = zero.
Show proof.
unshelve refine (total2_paths_f _ _).
- reflexivity.
- unshelve refine (total2_paths_f _ _); reflexivity.
- reflexivity.
- unshelve refine (total2_paths_f _ _); reflexivity.