Library UniMath.CategoryTheory.Presheaf

****************************************************************************
Theory about set-valued presheaves. We write PreShv C for C^op,HSET.
Contents:
Written by: Anders Mörtberg, 2017-2019

Require Import UniMath.MoreFoundations.All.

Require Import UniMath.Algebra.Monoids.
Require Import UniMath.OrderTheory.Lattice.Lattice.
Require Import UniMath.OrderTheory.Lattice.Bounded.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.LatticeObject.

Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.Limits.
Require Import UniMath.CategoryTheory.categories.HSET.Colimits.
Require Import UniMath.CategoryTheory.categories.HSET.Structures.

Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.products.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.limits.coproducts.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.pullbacks.

Local Open Scope cat.

Notation "'PreShv' C" := [C^op, HSET] (at level 4) : cat.

Section basics.

Lemma transportf_PreShv {C : category} (F : PreShv C) {x y z : C}
  (e : x = y) (f : Cx,z) (u : ((F : functor _ _) z : hSet)) :
  transportf (λ x, pr1 (pr1 F x)) e (# (pr1 F) f u) =
  # (pr1 F) (transportf (@precategory_morphisms C^op z) e f) u.
Show proof.
now induction e.

End basics.

Various limits and colimits in PreShv C

Define some standard presheaves

Section presheaves.

Context {C : category}.

Definition constant_PreShv (A : HSET) : PreShv C.
Show proof.
use make_functor.
+ use tpair.
  - intros _; apply A.
  - cbn. intros a b f. apply idfun.
+ now split.

Definition empty_PreShv : PreShv C := constant_PreShv emptyHSET.

End presheaves.

Definition of the subobject classifier in a presheaf.

See: "Sheaves in Geometry and Logic" by Mac Lane and Moerdijk (page 37)
Section Ω_PreShv.

Context {C : category}.

Definition sieve_def (c : C) : UU.
Show proof.
use total2.
- apply (hsubtype ( (x : C),Cx,c)).
- intros S.
  apply ( (s1 : (x : C),Cx,c), S s1
          y (f : Cy,pr1 s1), S (y,, f · pr2 s1)).

Lemma isaset_sieve (c : C) : isaset (sieve_def c).
Show proof.
use isaset_total2.
- apply isasethsubtype.
- intros S; repeat (apply impred_isaset; intro); apply isasetaprop, propproperty.

Definition sieve (c : C) : hSet := (sieve_def c,,isaset_sieve c).

Definition pr1sieve {c : C} : sieve_def c hsubtype _ := @pr1 _ _.
Coercion pr1sieve : sieve_def >-> hsubtype.

Lemma sieve_eq (c : C) (s t : sieve c) (H : pr1 s = pr1 t) : s = t.
Show proof.
apply subtypePath; [|apply H].
now intros x; repeat (apply impred; intros); apply propproperty.

Definition maximal_sieve (c : C) : sieve c.
Show proof.
use tpair.
- intro S; apply htrue.
- cbn. intros; apply tt.

Definition empty_sieve (c : C) : sieve c.
Show proof.
use tpair.
- intros S; apply hfalse.
- intros f S y g; apply S.

Definition intersection_sieve (c : C) : binop (sieve c).
Show proof.
simpl; intros S1 S2.
use tpair.
- intros f.
  apply (S1 f S2 f).
- simpl; intros f S f'.
  split.
  + apply (pr2 S1 _ (pr1 S)).
  + apply (pr2 S2 _ (pr2 S)).

Definition union_sieve (c : C) : binop (sieve c).
Show proof.
simpl; intros S1 S2.
use tpair.
- intros f.
  apply (S1 f S2 f).
- intros f S y f'; simpl in S; apply S; clear S; intro S.
  apply hinhpr.
  induction S as [S|S].
  + apply ii1, (pr2 S1 _ S).
  + apply ii2, (pr2 S2 _ S).

Definition sieve_lattice (c : C) : lattice (sieve c).
Show proof.
use make_lattice.
- apply intersection_sieve.
- apply union_sieve.
- repeat split; intros S1; intros;
  apply sieve_eq, funextsec; intro f; simpl.
  + apply (isassoc_Lmin hProp_lattice).
  + apply (iscomm_Lmin hProp_lattice).
  + apply (isassoc_Lmax hProp_lattice).
  + apply (iscomm_Lmax hProp_lattice).
  + apply (Lmin_absorb hProp_lattice).
  + apply (Lmax_absorb hProp_lattice).

Definition sieve_bounded_lattice (c : C) : bounded_lattice (sieve c).
Show proof.
use make_bounded_lattice.
- apply sieve_lattice.
- apply empty_sieve.
- apply maximal_sieve.
- split; intros S; apply sieve_eq, funextsec; intro f; simpl.
  + apply (islunit_Lmax_Lbot hProp_bounded_lattice).
  + apply (islunit_Lmin_Ltop hProp_bounded_lattice).

Definition sieve_mor a b (f : Cb,a) : sieve a sieve b.
Show proof.
simpl; intros S.
use tpair.
- intros g.
  apply (S (pr1 g,,pr2 g · f)).
- abstract (intros g H y h; simpl; rewrite <- assoc; apply (pr2 S (pr1 g,,pr2 g · f)), H).

Local Definition Ω_PreShv_data : functor_data C^op HSET := (sieve,,sieve_mor).

Local Lemma is_functor_Ω_PreShv_data : is_functor Ω_PreShv_data.
Show proof.
split.
- intros x; apply funextfun; intros [S hS]; simpl.
  apply subtypePath; simpl.
  + intros X; repeat (apply impred; intro); apply propproperty.
  + now apply funextsec; intro; rewrite id_right.
- intros x y z f g; apply funextfun; intros [S hS]; simpl.
  apply subtypePath; simpl.
  + intros X; repeat (apply impred; intro); apply propproperty.
  + now repeat (apply funextsec; intro); rewrite <- assoc.

Definition Ω_PreShv : PreShv C := (Ω_PreShv_data,,is_functor_Ω_PreShv_data).

Definition Ω_mor : (PreShv C)⟦Terminal_PreShv,Ω_PreShv.
Show proof.
use make_nat_trans.
- red; simpl; apply (λ c _, maximal_sieve c).
- intros x y f; simpl in *; apply funextfun; cbn; intros _.
  apply sieve_eq; simpl.
  now repeat (apply funextsec; intros).

Lemma isMonic_Ω_mor : isMonic Ω_mor.
Show proof.

Local Notation "c ⊗ d" := (BinProductObject _ (BinProducts_PreShv c d)) : cat.

Definition Ω_PreShv_meet : PreShv(C)Ω_PreShv Ω_PreShv,Ω_PreShv.
Show proof.
use make_nat_trans.
+ intros c S1S2.
  apply (intersection_sieve c (pr1 S1S2) (pr2 S1S2)).
+ intros x y f.
  apply funextsec; cbn; intros [S1 S2].
  now apply sieve_eq.

Definition Ω_PreShv_join : PreShv(C)Ω_PreShv Ω_PreShv,Ω_PreShv.
Show proof.
use make_nat_trans.
+ intros c S1S2.
  apply (union_sieve c (pr1 S1S2) (pr2 S1S2)).
+ intros x y f.
  apply funextsec; cbn; intros [S1 S2].
  now apply sieve_eq.

Definition Ω_PreShv_lattice : latticeob BinProducts_PreShv Ω_PreShv.
Show proof.
use make_latticeob.
+ apply Ω_PreShv_meet.
+ apply Ω_PreShv_join.
+ repeat split; apply (nat_trans_eq has_homsets_HSET); intro c;
                apply funextsec; intros S; simpl.
  - apply (isassoc_Lmin (sieve_lattice c)).
  - apply (iscomm_Lmin (sieve_lattice c)).
  - apply (isassoc_Lmax (sieve_lattice c)).
  - apply (iscomm_Lmax (sieve_lattice c)).
  - apply (Lmin_absorb (sieve_lattice c)).
  - apply (Lmax_absorb (sieve_lattice c)).

Definition Ω_PreShv_bottom : PreShv(C)Terminal_PreShv,Ω_PreShv.
Show proof.
use make_nat_trans.
+ intros c _; apply empty_sieve.
+ now intros x y f; apply funextsec; intros []; apply sieve_eq.

Definition Ω_PreShv_top : PreShv(C)Terminal_PreShv,Ω_PreShv.
Show proof.
use make_nat_trans.
+ intros c _; apply maximal_sieve.
+ now intros x y f; apply funextsec; intros []; apply sieve_eq.

Definition Ω_PreShv_bounded_lattice :
  bounded_latticeob BinProducts_PreShv Terminal_PreShv Ω_PreShv.
Show proof.
use make_bounded_latticeob.
- exact Ω_PreShv_lattice.
- exact Ω_PreShv_bottom.
- exact Ω_PreShv_top.
- split; apply (nat_trans_eq has_homsets_HSET); intro c;
         apply funextsec; cbn; intros S.
  + apply (islunit_Lmax_Lbot (sieve_bounded_lattice c)).
  + apply (islunit_Lmin_Ltop (sieve_bounded_lattice c)).

End Ω_PreShv.

Construction of isomorphisms of functors between presheaf categories
Section iso_presheaf.

Context {C : category}.

Local Definition make_PreShv_functor_z_iso_helper (F G : functor (PreShv C) (PreShv C))
      (set_iso : X c, z_iso (pr1 (F X) c) (pr1 (G X) c))
      (nat_in_c : X, is_nat_trans _ _ (λ c, set_iso X c))
      (nat_in_X : is_nat_trans F G (λ X, make_nat_trans _ _ _ (nat_in_c X))) :
      [PreShv C, PreShv C] F, G .
Show proof.
  use make_nat_trans.
    + intros X.
      use make_nat_trans.
      * intros c.
        exact (set_iso X c).
      * use nat_in_c.
    + exact nat_in_X.

Lemma make_PreShv_functor_z_iso (F G : functor (PreShv C) (PreShv C))
      (set_iso : X c, z_iso (pr1 (F X) c) (pr1 (G X) c))
      (nat_in_c : X, is_nat_trans _ _ (λ c, set_iso X c))
      (nat_in_X : is_nat_trans F G (λ X, make_nat_trans _ _ _ (nat_in_c X))) :
      @z_iso [PreShv C, PreShv C] F G.
Show proof.
  exists (make_PreShv_functor_z_iso_helper F G set_iso nat_in_c nat_in_X).
  use make_is_z_isomorphism.
  + use make_PreShv_functor_z_iso_helper.
      * intros X c.
        exact (z_iso_inv_from_z_iso (set_iso X c)).
      * abstract (intros X c y f;
                  apply pathsinv0, z_iso_inv_on_left; rewrite <- assoc;
                  now apply pathsinv0, z_iso_inv_on_right, (nat_in_c X)).
      * abstract (intros X Y α;
                  apply nat_trans_eq; [ apply homset_property|];
                  intro x; simpl;
                  apply pathsinv0, (z_iso_inv_on_left _ _ _ _ (set_iso Y x));
                  rewrite <- assoc; apply pathsinv0, (z_iso_inv_on_right (C:=HSET));
                  exact (eqtohomot (maponpaths pr1 (nat_in_X X Y α)) x)).
    + abstract (use make_is_inverse_in_precat;
                [ apply nat_trans_eq; [ apply homset_property |]; intro X;
                  apply nat_trans_eq; [ apply homset_property |]; intro x;
                  exact (z_iso_inv_after_z_iso (set_iso X x))
                | apply nat_trans_eq; [ apply homset_property |]; intro X;
                  apply nat_trans_eq; [ apply homset_property |]; intro x;
                  apply funextsec; intros y;
                  exact (eqtohomot (z_iso_after_z_iso_inv (set_iso X x)) y) ]).

End iso_presheaf.