(** * Morphisms in [set_cat] *)
Require Import Category.Core NaturalTransformation.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Category.Morphisms NaturalTransformation.Paths.
Require Import Category.Univalent.
Require Import SetCategory.Core.
Require Import HoTT.Basics HoTT.Types TruncType.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Local Open Scope path_scope.

Local Open Scope morphism_scope.
Local Open Scope category_scope.

Lemma isisomorphism_set_cat_natural_transformation_paths
      `{fs : Funext} (X : set_cat) C D F G
      (T1 T2 : morphism set_cat X (Build_HSet (@NaturalTransformation C D F G)))
      (H : forall x y, T1 x y = T2 x y)
      `{@IsIsomorphism set_cat _ _ T1}
: @IsIsomorphism set_cat _ _ T2.
fs: Funext
X: set_cat
C, D: PreCategory
F, G: Core.Functor C D
T1, T2: morphism set_cat X
  (Build_HSet (NaturalTransformation F G))
H: forall (x : X) (y : C), T1 x y = T2 x y
H0: IsIsomorphism T1
IsIsomorphism T2
Proof.
fs: Funext
X: set_cat
C, D: PreCategory
F, G: Core.Functor C D
T1, T2: morphism set_cat X
  (Build_HSet (NaturalTransformation F G))
H: forall (x : X) (y : C), T1 x y = T2 x y
H0: IsIsomorphism T1
IsIsomorphism T2
  exists (T1^-1)%morphism;
  abstract (
      first [ apply @iso_moveR_Vp
            | apply @iso_moveR_pV ];
      repeat first [ intro
                   | solve [ auto
                           | symmetry; auto ]
                   | apply @path_forall
                   | path_natural_transformation ]
    ).
Defined.

Section equiv_iso_set_cat.
  (** ** Isomorphisms in [set_cat] are equivalent to equivalences. *)
  Context `{Funext}.

  Definition isiso_isequiv s d (m : morphism set_cat s d)
             `{IsEquiv _ _ m}
  : IsIsomorphism m
    := Build_IsIsomorphism
         set_cat s d
         m m^-1%function
         (path_forall _ _ (eissect m))
         (path_forall _ _ (eisretr m)).

  Definition isequiv_isiso s d (m : morphism set_cat s d)
             `{IsIsomorphism _ _ _ m}
  : IsEquiv m
    := Build_IsEquiv
         _ _
         m m^-1%morphism
         (ap10 right_inverse)
         (ap10 left_inverse)
         (fun _ => path_ishprop _ _).

  Definition iso_equiv (s d : set_cat) (m : s <~> d)
  : s <~=~> d
    := Build_Isomorphic
         (@isiso_isequiv s d m _).

  #[export] Instance isequiv_isiso_isequiv s d
  : IsEquiv (@iso_equiv s d) | 0.
H: Funext
s, d: set_cat
IsEquiv (iso_equiv s d)
  Proof.
H: Funext
s, d: set_cat
IsEquiv (iso_equiv s d)
    refine (isequiv_adjointify
              (@iso_equiv s d)
              (fun m => Build_Equiv _ _ _ (@isequiv_isiso s d m m))
              _
              _);
    simpl in *;
    clear;
    abstract (
        intros [? ?]; simpl;
        unfold iso_equiv; simpl;
        apply ap;
        apply path_ishprop
      ).
  Defined.

  Lemma path_idtoequiv_idtoiso (s d : set_cat) (p : s = d)
  : iso_equiv s d (equiv_path _ _ (ap trunctype_type p)) = idtoiso set_cat p.
H: Funext
s, d: set_cat
p: s = d
iso_equiv s d (equiv_path s d (ap trunctype_type p)) =
idtoiso set_cat p
  Proof.
H: Funext
s, d: set_cat
p: s = d
iso_equiv s d (equiv_path s d (ap trunctype_type p)) =
idtoiso set_cat p
    apply path_isomorphic.
H: Funext
s, d: set_cat
p: s = d
iso_equiv s d (equiv_path s d (ap trunctype_type p)) =
idtoiso set_cat p
    case p.
H: Funext
s, d: set_cat
p: s = d
iso_equiv s s (equiv_path s s (ap trunctype_type 1)) =
idtoiso set_cat 1
    reflexivity.
  Defined.
End equiv_iso_set_cat.

Section equiv_iso_prop_cat.
  (** ** Isomorphisms in [prop_cat] are equivalent to equivalences. *)
  Context `{Funext}.

  Definition isiso_isequiv_prop s d (m : morphism prop_cat s d)
             `{IsEquiv _ _ m}
  : IsIsomorphism m
    := Build_IsIsomorphism
         prop_cat s d
         m m^-1%function
         (path_forall _ _ (eissect m))
         (path_forall _ _ (eisretr m)).

  Definition isequiv_isiso_prop s d (m : morphism prop_cat s d)
             `{IsIsomorphism _ _ _ m}
  : IsEquiv m
    := Build_IsEquiv
         _ _
         m m^-1%morphism
         (ap10 right_inverse)
         (ap10 left_inverse)
         (fun _ => path_ishprop _ _).

  Definition iso_equiv_prop (s d : prop_cat) (m : s <~> d)
  : s <~=~> d
    := Build_Isomorphic
         (@isiso_isequiv_prop s d m _).

  #[export] Instance isequiv_isiso_isequiv_prop s d
  : IsEquiv (@iso_equiv_prop s d) | 0.
H: Funext
s, d: prop_cat
IsEquiv (iso_equiv_prop s d)
  Proof.
H: Funext
s, d: prop_cat
IsEquiv (iso_equiv_prop s d)
    refine (isequiv_adjointify
              (@iso_equiv_prop s d)
              (fun m => Build_Equiv _ _ _ (@isequiv_isiso_prop s d m _))
              _
              _);
    simpl in *;
    clear;
    abstract (
        intros [? ?]; simpl;
        unfold iso_equiv_prop; simpl;
        apply ap;
        apply path_ishprop
      ).
  Defined.

  Lemma path_idtoequiv_idtoiso_prop (s d : prop_cat) (p : s = d)
  : iso_equiv_prop s d (equiv_path _ _ (ap trunctype_type p)) = idtoiso prop_cat p.
H: Funext
s, d: prop_cat
p: s = d
iso_equiv_prop s d
  (equiv_path s d (ap trunctype_type p)) =
idtoiso prop_cat p
  Proof.
H: Funext
s, d: prop_cat
p: s = d
iso_equiv_prop s d
  (equiv_path s d (ap trunctype_type p)) =
idtoiso prop_cat p
    apply path_isomorphic.
H: Funext
s, d: prop_cat
p: s = d
iso_equiv_prop s d
  (equiv_path s d (ap trunctype_type p)) =
idtoiso prop_cat p
    case p.
H: Funext
s, d: prop_cat
p: s = d
iso_equiv_prop s s
  (equiv_path s s (ap trunctype_type 1)) =
idtoiso prop_cat 1
    reflexivity.
  Defined.
End equiv_iso_prop_cat.

Local Close Scope morphism_scope.
Instance iscategory_set_cat `{Univalence}
: IsCategory set_cat.
H: Univalence
IsCategory set_cat
Proof.
H: Univalence
IsCategory set_cat
  intros C D.
H: Univalence
C, D: set_cat
IsEquiv (idtoiso set_cat (y:=D))
  eapply @isequiv_homotopic; [ | intro; apply path_idtoequiv_idtoiso ].
H: Univalence
C, D: set_cat
IsEquiv
  (fun x : C = D =>
   iso_equiv C D
     (equiv_path C D (ap trunctype_type x)))
  change (IsEquiv (iso_equiv C D o equiv_path C D o @ap _ _ trunctype_type C D)).
H: Univalence
C, D: set_cat
IsEquiv
  (iso_equiv C D o equiv_path C D o ap trunctype_type)
  typeclasses eauto.
Defined.

Instance iscategory_prop_cat `{Univalence}
: IsCategory prop_cat.
H: Univalence
IsCategory prop_cat
Proof.
H: Univalence
IsCategory prop_cat
  intros C D.
H: Univalence
C, D: prop_cat
IsEquiv (idtoiso prop_cat (y:=D))
  eapply @isequiv_homotopic; [ | intro; apply path_idtoequiv_idtoiso_prop ].
H: Univalence
C, D: prop_cat
IsEquiv
  (fun x : C = D =>
   iso_equiv_prop C D
     (equiv_path C D (ap trunctype_type x)))
  change (IsEquiv (iso_equiv_prop C D o equiv_path C D o @ap _ _ trunctype_type C D)).
H: Univalence
C, D: prop_cat
IsEquiv
  (iso_equiv_prop C D o equiv_path C D
   o ap trunctype_type)
  typeclasses eauto.
Defined.