Isomorphism of (pre)categories

Definition is_catiso {A B : precategory_data}
(F : functor A B)
:= (fully_faithful F) × (isweq (functor_on_objects F)).

Definition catiso (A B : precategory_data)
:= total2 (λ F : functor A B, is_catiso F).

Lemma isaprop_is_catiso
{A B : precategory_data}
{F : functor A B}
: isaprop (is_catiso F).
Proof.
apply isapropdirprod.
- apply isaprop_fully_faithful.
- apply isapropisweq.
Defined.

Definition functor_from_catiso (A B : precategory_data)
(F : catiso A B)
: functor A B := pr1 F.
Coercion functor_from_catiso :
catiso >-> functor.

Definition identity_catiso (A : precategory_data)
: catiso A A.
Proof.
use tpair.
- exact (functor_identity A).
- use tpair.
+ apply identity_functor_is_fully_faithful.
+ apply idisweq.
Defined.

Definition catiso_ob_weq {A B : precategory_data}
(F : catiso A B)
: (ob A) (ob B)
:= make_weq (functor_on_objects F) (pr2 (pr2 F)).

Definition catiso_to_precategory_ob_path {A B : precategory_data}
(F : catiso A B)
: ob A = ob B
:= (invmap (univalence _ _) (catiso_ob_weq F)).

Definition catiso_fully_faithful_weq {A B : precategory_data}
(F : catiso A B)
: a a' : A, (a --> a') (F a --> F a')
:= λ a a', (make_weq (functor_on_morphisms F) (pr1 (pr2 F) a a')).

Lemma catiso_fully_faithful_path {A B : precategory_data}
(F : catiso A B)
: a a' : A, (a --> a') = (F a --> F a').
Proof.
intros a a'.
apply (invmap (univalence _ _)).
apply (catiso_fully_faithful_weq F).
Defined.

Construction of a map (catiso A B) -> (A = B)

Lemma correct_hom {A B : precategory_data}
(F : catiso A B)
: a a' : A,
F a --> F a'
= (eqweqmap (catiso_to_precategory_ob_path F) a) -->
(eqweqmap (catiso_to_precategory_ob_path F) a').
Proof.
intros a a'.
assert (W := (!(homotweqinvweq (univalence _ _)) (catiso_ob_weq F))).
exact (maponpaths (λ T, (pr1weq T) a --> (pr1weq T) a') W ).
Defined.

Lemma eqweq_ob_path_is_functor_app {A B : precategory_data}
(F : catiso A B)
: a : A, eqweqmap (catiso_to_precategory_ob_path F) a = F a.
Proof.
intros a.
exact (! toforallpaths (λ _ : A, B) F
(pr1 (eqweqmap (invmap (univalence A B) (catiso_ob_weq F))))
(maponpaths pr1 (! homotweqinvweq (univalence A B) (catiso_ob_weq F))) a).
Defined.

Lemma eqweq_ob_path_is_functor_app_compute
(A B : precategory)
(F : catiso A B)
(a a' : A)
(f : B F a, F a' ):
eqweq_ob_path_is_functor_app F a =
! toforallpaths (λ _ : A, B) F
(pr1weq (eqweqmap (invmap (univalence A B) (catiso_ob_weq F))))
(maponpaths pr1weq (! homotweqinvweq (univalence A B) (catiso_ob_weq F))) a.
Proof.
unfold eqweq_ob_path_is_functor_app.
Abort.

Lemma eqweq_maponpaths_mor {A B : precategory}
(F G : A B) (p : F = G) (a a' : A) (f : F a --> F a')
: eqweqmap (maponpaths (λ T : A B, (pr1 T) a --> (pr1 T) a') p) f
= (idtomor _ _ (!toforallpaths _ _ _ (maponpaths pr1 p) a))
· f
· (idtomor _ _ (toforallpaths _ _ _ (maponpaths pr1 p) a')).
Proof.
induction p.
rewrite id_left.
rewrite id_right.
reflexivity.
Defined.

Lemma eqweq_correct_hom_is_comp {A B : precategory}
(F : catiso A B)
: a a' : A, f : F a --> F a',
eqweqmap (correct_hom F _ _) f
= (idtomor _ _ (eqweq_ob_path_is_functor_app F a))
· f
· (idtomor _ _ (!eqweq_ob_path_is_functor_app F a')).
Proof.
intros a a' f.
rewrite (eqweq_maponpaths_mor _ _
(! homotweqinvweq (univalence A B) (catiso_ob_weq F))
a a').
apply maponpaths. apply maponpaths.
unfold eqweq_ob_path_is_functor_app.
rewrite pathsinv0inv0.
reflexivity.
Defined.

Lemma eqweq_fully_faithful_is_functor_app {A B : precategory_data}
(F : catiso A B)
: a a' : A,
eqweqmap (catiso_fully_faithful_path F a a')
= catiso_fully_faithful_weq F _ _.
Proof.
intros a a'.
unfold catiso_fully_faithful_path.

assert (W := (@homotweqinvweq _ _ (univalence (a --> a') (F a --> F a')))).
simpl in W.
rewrite W.

reflexivity.
Defined.

Lemma transport_mor {A B : UU} (B1 : B B UU) (p : A = B) :
a a' : A,
B1 (eqweqmap p a) (eqweqmap p a')
= (transportb (λ T, T T UU) p B1) a a'.
Proof.
induction p.
reflexivity.
Defined.

Lemma catiso_to_precategory_mor_path {A B : precategory_data}
(F : catiso A B)
: a a', (precategory_morphisms (C:=A)) a a'
= transportb (λ T, T T UU) (catiso_to_precategory_ob_path F)
(precategory_morphisms (C:=B)) a a'.
Proof.
intros a.
intros a'.

eapply pathscomp0. apply (catiso_fully_faithful_path F).
eapply pathscomp0. apply correct_hom.
eapply pathscomp0. apply transport_mor.

reflexivity.
Defined.

Lemma catiso_to_precategory_mor_path_funext {A B : precategory_data}
(F : catiso A B)
: (precategory_morphisms (C:=A))
= transportb (λ T, T T UU) (catiso_to_precategory_ob_path F)
(precategory_morphisms (C:=B)).
Proof.
apply (pr1 (weqfunextsec _ _ _)).
intros a.
apply (pr1 (weqfunextsec _ _ _)).
intros a'.
apply (catiso_to_precategory_mor_path F).
Defined.

Definition catiso_to_precategory_ob_mor_path {A B : precategory_data}
(F : catiso A B)
: precategory_ob_mor_from_precategory_data A = precategory_ob_mor_from_precategory_data B
:= total2_paths_b (catiso_to_precategory_ob_path F) (catiso_to_precategory_mor_path_funext F).

Lemma transport_id {A0 B0 : UU} (p0 : A0 = B0)
(A1 : A0 A0 UU) (B1 : B0 B0 UU) (p1 : A1 = transportb _ p0 B1)
(idB : b : B0, B1 b b)
: a : A0,
(transportb (X := total2 (λ T, T T UU))
(λ T, a, (pr2 T) a a)
(total2_paths2_b p0 p1) idB) a
= (eqweqmap ( (transport_mor B1 p0 _ _)
@ !weqtoforallpaths _ _ _ (weqtoforallpaths _ _ _ p1 a) a))
(idB (eqweqmap p0 a)).
Proof.
intro.
induction p0.
change (transportb _ _ _) with B1 in p1.
induction p1.
simpl.
reflexivity.
Defined.

Lemma correct_hom_on_id {A B : precategory}
(F : catiso A B)
: a,
identity ((eqweqmap (catiso_to_precategory_ob_path F)) a) =
(eqweqmap (correct_hom F a a)) (identity (F a)).
Proof.
intros a.

apply pathsinv0.
eapply pathscomp0. apply eqweq_correct_hom_is_comp.

induction (eqweq_ob_path_is_functor_app F a).
simpl.
rewrite 2 id_right.
reflexivity.
Defined.

Lemma catiso_to_precategory_id_path {A B : precategory}
(F : catiso A B)
: a : A,
(transportb (X := total2 (λ T, T T UU))
(λ T, a, (pr2 T) a a)
(total2_paths2_b (catiso_to_precategory_ob_path F)
(catiso_to_precategory_mor_path_funext F))
identity) a
= identity a.
Proof.
intros a.

eapply pathscomp0. apply transport_id.

unfold catiso_to_precategory_mor_path_funext.
unfold catiso_to_precategory_mor_path.
unfold weqfunextsec.
simpl (pr1 _).
rewrite !(homotweqinvweq (weqtoforallpaths _ _ _)).

rewrite pathscomp_inv.
rewrite pathscomp_inv.
rewrite path_assoc.
rewrite path_assoc.
rewrite pathscomp0rid.
rewrite pathsinv0r.
simpl.

apply pathsweq1'.
rewrite <- pathscomp_inv.
rewrite eqweqmap_pathsinv0.
rewrite invinv.

rewrite <- eqweqmap_pathscomp0.

rewrite (eqweq_fully_faithful_is_functor_app F a a).
simpl.

rewrite functor_id.
apply correct_hom_on_id.
Defined.

Lemma transport_comp_target {A0 B0 : UU} (p0 : A0 = B0)
(A1 : A0 A0 UU) (B1 : B0 B0 UU) (p1 : A1 = transportb (λ T, T T UU) p0 B1)
: a a' a'' : A0,
( B1 (eqweqmap p0 a) (eqweqmap p0 a')
B1 (eqweqmap p0 a') (eqweqmap p0 a'')
B1 (eqweqmap p0 a) (eqweqmap p0 a''))
( A1 a a' A1 a' a'' A1 a a'').
Proof.
intros a a' a''.
intros Bhom.
intros f g.

set (X := λ a a', (transport_mor B1 p0 a a')
@ (! weqtoforallpaths _ _ _ (weqtoforallpaths _ _ _ p1 a) a') ).

apply (eqweqmap (X a a'')).
apply Bhom.

apply (eqweqmap (! X a a')).
exact f.

apply (eqweqmap (! X a' a'')).
exact g.
Defined.

Lemma transport_comp {A0 B0 : UU} (p0 : A0 = B0)
(A1 : A0 A0 UU) (B1 : B0 B0 UU) (p1 : A1 = transportb _ p0 B1)
(compB : b b' b'' : B0, B1 b b' B1 b' b'' B1 b b'')
: a a' a'' : A0,
(transportb (X := total2 (λ T, T T UU))
(λ T, a b c, (pr2 T) a b (pr2 T) b c (pr2 T) a c)
(total2_paths2_b p0 p1) compB)
a a' a''
= transport_comp_target p0 A1 B1 p1 a a' a''
(compB (eqweqmap p0 a) (eqweqmap p0 a') (eqweqmap p0 a'')).
Proof.
intros.
induction p0.
change (A1 = B1) in p1.
induction p1.
reflexivity.
Defined.

Lemma correct_hom_on_comp {A B : precategory}
(F : catiso A B)
: a a' a'', f : F a --> F a', g : F a' --> F a'',
(eqweqmap (correct_hom F _ _)) f
· (eqweqmap (correct_hom F _ _)) g
= (eqweqmap (correct_hom F _ _)) (f · g).
Proof.
intros a a' a'' f g.
rewrite !eqweq_correct_hom_is_comp.
induction (eqweq_ob_path_is_functor_app F a).
induction (eqweq_ob_path_is_functor_app F a').
induction (eqweq_ob_path_is_functor_app F a'').
rewrite 3 id_left.
simpl.
rewrite 3 id_right.
reflexivity.
Defined.

Lemma catiso_to_precategory_comp_path {A B : precategory}
(F : catiso A B)
: a a' a'' : A,
(transportb (X := total2 (λ T, T T UU))
(λ T, a b c : (pr1 T), (pr2 T) a b (pr2 T) b c (pr2 T) a c)
(total2_paths2_b (catiso_to_precategory_ob_path F)
(catiso_to_precategory_mor_path_funext F))
(@compose B)) a a' a''
= (@compose A a a' a'').
Proof.
intros a a' a''.

eapply pathscomp0. apply transport_comp.
apply funextsec. intros f.
apply funextsec. intros g.

unfold transport_comp_target.

unfold catiso_to_precategory_mor_path_funext.
simpl.

set (W := homotweqinvweq
(weqtoforallpaths (λ _ : A, A UU)
precategory_morphisms
(transportb (λ T, T T UU)
(catiso_to_precategory_ob_path F)
precategory_morphisms))).
simpl in W. rewrite !W. clear W.

set (W := homotweqinvweq
(weqtoforallpaths (λ _ : A, UU)
(precategory_morphisms a)
(transportb (λ T, T T UU)
(catiso_to_precategory_ob_path F)
precategory_morphisms a))).
simpl in W. rewrite !W. clear W.

set (W := homotweqinvweq
(weqtoforallpaths (λ _ : A, UU)
(precategory_morphisms a')
(transportb (λ T, T T UU)
(catiso_to_precategory_ob_path F)
precategory_morphisms a'))).
simpl in W. rewrite !W. clear W.

unfold catiso_to_precategory_mor_path.
rewrite !pathscomp0rid.
rewrite !pathscomp_inv.
rewrite !pathsinv0inv0.
rewrite path_assoc.
rewrite path_assoc.
rewrite pathsinv0r.
simpl.
rewrite <- path_assoc.
rewrite <- path_assoc.
rewrite pathsinv0r.
rewrite pathscomp0rid.
rewrite <- path_assoc.
rewrite <- path_assoc.
rewrite pathsinv0r.
rewrite pathscomp0rid.
rewrite <- pathscomp_inv.

apply pathsweq1'.
rewrite eqweqmap_pathsinv0.
rewrite invinv.

rewrite <- !eqweqmap_pathscomp0.
rewrite !eqweq_fully_faithful_is_functor_app.
simpl.
rewrite functor_comp.

apply (correct_hom_on_comp F).
Defined.

Lemma catiso_to_precategory_data_path {A B : precategory}
(F : catiso A B)
: precategory_data_from_precategory A
= precategory_data_from_precategory B.
Proof.
destruct A as [[[Ao Am] [Ai Ac]] Aax].
destruct B as [[[Bo Bm] [Bi Bc]] Bax].

eapply total2_paths_b. Unshelve.
2: { simpl. exact (catiso_to_precategory_ob_mor_path F). }
apply pathsinv0.
eapply pathscomp0.
apply (transportb_dirprod _ _ _ _ _ (catiso_to_precategory_ob_mor_path F)).
apply dirprodeq.
- apply funextsec.
intros a.
apply (catiso_to_precategory_id_path F).
- apply funextsec.
intro.
apply funextsec.
intro.
apply funextsec.
intro.
apply (catiso_to_precategory_comp_path F).
Defined.

Lemma catiso_to_precategory_path {A B : precategory}
(hs : has_homsets A)
(F : catiso A B)
: A = B.
Proof.
eapply total2_paths_b. Unshelve.
2: { simpl. exact (catiso_to_precategory_data_path F). }
apply proofirrelevance.
apply isaprop_is_precategory.
apply hs.
Defined.

Definition inv_catiso
{C D : category}
(F : catiso C D)
: D C.
Proof.
use make_functor.
- use tpair.
+ exact (invweq (catiso_ob_weq F)).
+ intros X Y f ; cbn.
refine (invmap
(catiso_fully_faithful_weq F
(invmap (catiso_ob_weq F) X)
(invmap (catiso_ob_weq F) Y))
_).
exact ((idtoiso (homotweqinvweq (catiso_ob_weq F) X))
· f
· idtoiso (!(homotweqinvweq (catiso_ob_weq F) Y))).
- split.
+ intro X ; cbn.
rewrite id_right.
etrans.
{
apply maponpaths.
exact (!(maponpaths pr1
(idtoiso_concat D _ _ _
(homotweqinvweq (catiso_ob_weq F) X)
(! homotweqinvweq (catiso_ob_weq F) X)))).
}
rewrite pathsinv0r ; cbn.
apply invmap_eq ; cbn.
rewrite functor_id.
reflexivity.
+ intros X Y Z f g ; cbn.
apply invmap_eq ; cbn.
rewrite functor_comp.
pose (homotweqinvweq
(catiso_fully_faithful_weq F
(invmap (catiso_ob_weq F) X)
(invmap (catiso_ob_weq F) Y))) as p.
cbn in p.
rewrite p ; clear p.
pose (homotweqinvweq
(catiso_fully_faithful_weq F
(invmap (catiso_ob_weq F) Y)
(invmap (catiso_ob_weq F) Z))) as p.
cbn in p.
rewrite p ; clear p.
rewrite <- !assoc.
repeat (apply (maponpaths (λ z, _ · (f · z)))).
refine (!(id_left _) @ _).
rewrite !assoc.
repeat (apply (maponpaths (λ z, z · _))).
rewrite idtoiso_inv.
cbn.
rewrite iso_after_iso_inv.
reflexivity.
Defined.