Library UniMath.CategoryTheory.DisplayedCats.Constructions.FullSubcategory

Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Univalence.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.

Local Open Scope cat.

1. The construction of the full subcategory as a displayed category

Definition disp_full_sub_ob_mor (C : precategory_ob_mor) (P : C → UU)
  : disp_cat_ob_mor C
  := (P ,, (λ a b aa bb f , unit )).

Definition disp_full_sub_id_comp (C : precategory_data) (P : C → UU)
  : disp_cat_id_comp C (disp_full_sub_ob_mor C P).
Show proof.

split; intros; apply tt.

Definition disp_full_sub_data (C : precategory_data) (P : C → UU)
  : disp_cat_data C
  := disp_full_sub_ob_mor C P ,, disp_full_sub_id_comp C P.

Lemma disp_full_sub_locally_prop (C : category) (P : C → UU) :
  locally_propositional (disp_full_sub_data C P).
Show proof.

intro; intros; apply isapropunit.

Definition disp_full_sub (C : category) (P : C → UU)
: disp_cat C.
Show proof.

  use make_disp_cat_locally_prop.
  - exact (disp_full_sub_data C P).
  - apply disp_full_sub_locally_prop.

2. Univalence

Lemma disp_full_sub_univalent (C : category) (P : C → UU) :
(∏ x : C , isaprop (P x)) →
is_univalent_disp (disp_full_sub C P).
Show proof.

  intro HP.
  apply is_univalent_disp_from_fibers.
  intros x xx xx'. cbn in *.
  apply isweqcontrprop. apply HP.
  apply isofhleveltotal2.
  - apply isapropunit.
  - intro. apply (@isaprop_is_z_iso_disp _ (disp_full_sub C P)).

3. Shortcuts for just the resulting total category

Definition full_subcat (C : category) (P : C → UU) : category := total_category (disp_full_sub C P).

Definition is_univalent_full_subcat (C : category) (univC : is_univalent C) (P : C → UU) :
(∏ x : C , isaprop (P x)) → is_univalent (full_subcat C P).
Show proof.

  intro H.
  apply is_univalent_total_category.
  - exact univC.
  - exact (disp_full_sub_univalent _ _ H).