Library UniMath.CategoryTheory.GrothendieckToposes.Toposes

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

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.Subcategory.Core.
Require Import UniMath.CategoryTheory.CategoryEquality.
Require Import UniMath.CategoryTheory.catiso.

Require Import UniMath.CategoryTheory.GrothendieckToposes.Sheaves.
Require Import UniMath.CategoryTheory.GrothendieckToposes.Sites.

1. The property of being a Grothendieck topos

Definition Grothendieck_topos_structure
  (C : category)
  : UU
  := ∑ (D : site ), adj_equiv C (sheaf_cat D).

Definition Grothendieck_topos_structure_site
  {C : category}
  (G : Grothendieck_topos_structure C)
  : site
  := pr1 G.

Definition Grothendieck_topos_structure_equiv
  {C : category}
  (G : Grothendieck_topos_structure C)
  : adj_equiv C (sheaf_cat (Grothendieck_topos_structure_site G))
  := pr2 G.

Definition is_Grothendieck_topos
  (C : category)
  : hProp
  := ∥ Grothendieck_topos_structure C ∥.

2. Grothendieck toposes

Definition Grothendieck_topos : UU :=
  carrier is_Grothendieck_topos.

Definition make_Grothendieck_topos
  (C : category)
  (G : is_Grothendieck_topos C)
  : Grothendieck_topos
  := C ,, G.

Coercion Grothendieck_topos_category (GT : Grothendieck_topos) : category :=
  pr1 GT.

Definition Grothendieck_topos_is_Grothendieck_topos
  (GT : Grothendieck_topos)
  : is_Grothendieck_topos GT := pr2 GT.

3. The recursion and induction principles

Lemma Grothendieck_topos_rect
  (P : category → UU)
  (HP : ∏ (D : site ), P (sheaf_cat D))
  {C : category}
  (HU : is_univalent C)
  (HT : Grothendieck_topos_structure C)
  : P C.
Show proof.

  refine (transportf P _ (HP (Grothendieck_topos_structure_site HT))).
  apply (invmap (catiso_is_path_cat _ _)).
  use (adj_equivalence_of_cats_to_cat_iso (adj_equivalence_of_cats_inv _ (Grothendieck_topos_structure_equiv HT))).
  - apply sheaf_cat_univalent.
  - apply HU.

Lemma Grothendieck_topos_ind
  (P : category → hProp)
  (HP : ∏ (D : site ), P (sheaf_cat D))
  {C : category}
  (HU : is_univalent C)
  (HT : is_Grothendieck_topos C)
  : P C.
Show proof.

  revert HT.
  apply hinhuniv.
  exact (Grothendieck_topos_rect P HP HU).