Library UniMath.CategoryTheory.Categories.KaroubiEnvelope.UnivalentKaroubi

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Categories.HSET.Core.
Require Import UniMath.CategoryTheory.Categories.HSET.Univalence.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.FullSubcategory.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Limits.Equalizers.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Presheaf.
Require Import UniMath.CategoryTheory.yoneda.

Require Import UniMath.CategoryTheory.IdempotentsAndSplitting.Retracts.
Require Import UniMath.CategoryTheory.IdempotentsAndSplitting.Set.
Require Import UniMath.CategoryTheory.IdempotentsAndSplitting.FunctorCategory.
Require Import UniMath.CategoryTheory.IdempotentsAndSplitting.Fullsub.
Require Import UniMath.CategoryTheory.Categories.KaroubiEnvelope.Core.

Local Open Scope cat.

1. The univalent Karoubi envelope

1.1. The category

Section RetractsOfPresheaves.

  Context {X : category}.

  Definition presheaf_is_retract (F : [X^op, SET]) : UU
    := ∃ (x : X), retraction F (yoneda X x).

  Lemma isaprop_presheaf_is_retract (F : [X^op, SET])
    : isaprop (presheaf_is_retract F).
  Show proof.
    apply isapropishinh.

  Lemma representable_presheaf_is_retract
    : ∏ x : X, presheaf_is_retract (yoneda X x).
  Show proof.
    intro x.
    apply hinhpr.
    exists x.
    use make_retraction.
    - apply identity.
    - apply identity.
    - apply id_left.

End RetractsOfPresheaves.

Section DefinitionOfKaroubi.

  Context (X : category).

  Definition univalent_karoubi_cat
    : category
    := full_subcat [X^op, SET] presheaf_is_retract.

  Lemma is_univalent_karoubi_cat
    : is_univalent univalent_karoubi_cat.
  Show proof.
    apply is_univalent_full_subcat.
    - apply is_univalent_functor_category, is_univalent_HSET.
    - intro ; apply isaprop_presheaf_is_retract.

End DefinitionOfKaroubi.

Section HelperLemmas.

  Lemma univalent_karoubi_eq_on_mor
    {X : category} {o₁ o₂ : univalent_karoubi_cat X} (f g : _⟦o₁, o₂⟧)
    : pr1 f = pr1 g → f = g.
  Show proof.
    intro p.
    use subtypePath.
    {
      intro.
      apply isapropunit.
    }
    exact p.

End HelperLemmas.

1.2. The fully faithful embedding

Section EmbeddingIntoKaroubi.

  Context (X : category).

  Let KE : category := univalent_karoubi_cat X.

  Definition embedding_into_karoubi_data
    : functor_data X KE.
  Show proof.
    use make_functor_data.
    - intro x.
      exists (yoneda X x).
      apply representable_presheaf_is_retract.
    - intros x₀ x₁ f.
      exact (#(yoneda X) f ,, tt).

  Lemma embedding_into_karoubi_is_functor
    : is_functor embedding_into_karoubi_data.
  Show proof.
    split ; intro ; intros
    ; apply univalent_karoubi_eq_on_mor ; apply (yoneda X).

  Definition embedding_into_karoubi
    : X ⟶ KE.
  Show proof.
    use make_functor.
    - exact embedding_into_karoubi_data.
    - apply embedding_into_karoubi_is_functor.

  Local Lemma univalent_karoubi_eq_on_mor_from_embedding
    {x₁ x₂ : X}
    (f : KE⟦embedding_into_karoubi x₁, embedding_into_karoubi x₂⟧)
    (g : X ⟦x₁, x₂⟧)
    : (#(yoneda X) g = pr1 f) ≃ #(yoneda X) g ,, tt = f.
  Show proof.
    use weq_iso.
    - intro p.
      apply (univalent_karoubi_eq_on_mor (#embedding_into_karoubi g) f).
      exact p.
    - intro p.
      induction p.
      apply idpath.
    - intro ; apply homset_property.
    - intro.
      use proofirrelevance.
      apply (homset_property KE (embedding_into_karoubi _) (embedding_into_karoubi _)).

  Corollary embedding_into_karoubi_is_fully_faithful
    : fully_faithful embedding_into_karoubi.
  Show proof.
    intros x₁ x₂.
    intro f.
    use iscontrweqf.
    - exact (∑ g : X ⟦x₁, x₂⟧, #(yoneda X) g = pr1 f).
    - unfold hfiber.
      use weqfibtototal.
      intro.
      apply univalent_karoubi_eq_on_mor_from_embedding.
    - exact (yoneda_fully_faithful X x₁ x₂ (pr1 f)).

End EmbeddingIntoKaroubi.

1.3. Every idempotent in the karoubi envelope splits

Section SplitIdempotents.

  Context {C : category}.
  Context (X : univalent_karoubi_cat C).
  Context (f : idempotent X).

  Definition univalent_karoubi_split_idempotent_presheaf
    : PreShv C
    := Equalizers_PreShv _ _ (identity _) (pr1 (idempotent_morphism f)).

  Definition univalent_karoubi_split_idempotent_presheaf_retraction
    : retraction univalent_karoubi_split_idempotent_presheaf (pr1 X).
  Show proof.
    use make_retraction.
    - apply EqualizerArrow.
    - refine (EqualizerIn _ _ (pr1 (idempotent_morphism f)) _).
      refine (id_right _ @ !base_paths _ _ (idempotent_is_idempotent f)).
    - abstract (
        apply EqualizerInsEq;
        refine (assoc' _ _ _ @ _);
        refine (maponpaths _ (EqualizerCommutes _ _ _ _) @ _);
        refine (_ @ !id_left _);
        refine (_ @ id_right _);
        exact (!EqualizerEqAr _)
      ).

  Definition univalent_karoubi_split_idempotent_object
    : univalent_karoubi_cat C.
  Show proof.
    exists univalent_karoubi_split_idempotent_presheaf.
    refine (hinhfun _ (pr2 X)).
    intro HX.
    exists (pr1 HX).
    exact (compose_retraction
      univalent_karoubi_split_idempotent_presheaf_retraction
      (pr2 HX)).

  Definition univalent_karoubi_split_idempotent
    : is_split_idempotent f.
  Show proof.
    use make_is_split_idempotent.
    - exact univalent_karoubi_split_idempotent_object.
    - apply (fully_faithful_functor_reflects_retraction _ (full_subcat_pr1_fully_faithful _ _)).
      exact univalent_karoubi_split_idempotent_presheaf_retraction.
    - abstract (
        apply univalent_karoubi_eq_on_mor;
        exact (!EqualizerCommutes _ _ _ _)
      ).

End SplitIdempotents.

Definition univalent_karoubi_idempotents_split
  (C : category)
  : idempotents_split (univalent_karoubi_cat C).
Show proof.
  intros X f.
  apply hinhpr.
  apply univalent_karoubi_split_idempotent.

1.4. Every object of the karoubi envelope is a retract of an element of C

Definition univalent_karoubi_objects_are_retracts
  (C : category)
  : objects_are_retracts (embedding_into_karoubi C).
Show proof.
  intro X.
  refine (hinhfun _ (pr2 X)).
  intro HX.
  exists (pr1 HX).
  apply (fully_faithful_functor_reflects_retraction _ (full_subcat_pr1_fully_faithful _ _)).
  exact (pr2 HX).

1.5. The bundling of the above into a term of univalent_karoubi_envelope

Definition univalent_karoubi
  (C : category)
  : univalent_karoubi_envelope C.
Show proof.
  use make_univalent_karoubi_envelope.
  - use make_karoubi_envelope.
    + use make_karoubi_envelope_data.
      * exact (univalent_karoubi_cat C).
      * exact (embedding_into_karoubi C).
    + apply make_is_karoubi_envelope.
      * exact (univalent_karoubi_idempotents_split C).
      * exact (embedding_into_karoubi_is_fully_faithful C).
      * exact (univalent_karoubi_objects_are_retracts C).
  - apply (is_univalent_karoubi_cat C).

1.6. Another proof of the splitting

Proposition idempotents_in_karoubi_envelope_split (X : category)
    : idempotents_split (univalent_karoubi_cat X).
Show proof.
  use idempotents_split_in_full_subcat.
  - apply idempotents_split_in_functor_cat.
    + apply is_univalent_HSET.
    + apply idempotents_split_in_set.
  - intros F G r.
    use (factor_through_squash _ _ (pr2 F)).
    { apply isapropishinh. }
    intros [x r'].
    apply hinhpr.
    exists x.
    exact (compose_retraction r r').