(** * Grothendieck Construction of a functor to Set *)
Require Import Category.Core Functor.Core.
Require Import SetCategory.Core.
Require Import Basics.Trunc Types.Sigma.
Require Import Basics.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope morphism_scope.

Section Grothendieck.
  Context `{Funext}.

  (**
     Quoting Wikipedia:

     The Grothendieck construction is an auxiliary construction used
     in the mathematical field of category theory.

     Let

<<
     F : C → Set
>>

     be a functor from any small category to the category of sets.
     The Grothendieck construct for [F] is the category [Γ F] whose
     objects are pairs [(c, x)], where [c : C] is an object and [x : F
     c] is an element, and for which the set [Hom (Γ F) (c1, x1) (c2,
     x2)] is the set of morphisms [f : c1 → c2] in [C] such that
     [F₁ f x1 = x2].  *)

  Variable C : PreCategory.
  Variable F : Functor C set_cat.

  Record Pair :=
    {
      c : C;
      x : F c
    }.

  Definition issig_pair : { c : C | F c } <~> Pair.
H: Funext
C: PreCategory
F: Functor C set_cat
{c0 : C & (F _0 c0)%object} <~> Pair
  Proof.
H: Funext
C: PreCategory
F: Functor C set_cat
{c0 : C & (F _0 c0)%object} <~> Pair
    issig.
  Defined.

  Local Notation morphism s d :=
    { f : morphism C s.(c) d.(c)
    | F _1 f s.(x) = d.(x) }.

  Definition compose_H s d d'
             (m1 : morphism d d')
             (m2 : morphism s d)
  : (F _1 (m1 .1 o m2 .1)) s.(x) = d'.(x).
H: Funext
C: PreCategory
F: Functor C set_cat
s, d, d': Pair
m1: morphism d d'
m2: morphism s d
(F _1 (m1.1 o m2.1)) (x s) = x d'
  Proof.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d, d': Pair
m1: morphism d d'
m2: morphism s d
(F _1 (m1.1 o m2.1)) (x s) = x d'
    etransitivity; [ | exact (m1.2) ].
H: Funext
C: PreCategory
F: Functor C set_cat
s, d, d': Pair
m1: morphism d d'
m2: morphism s d
(F _1 (m1.1 o m2.1)) (x s) = (F _1 m1.1) (x d)
    etransitivity; [ | apply ap; exact (m2.2) ].
H: Funext
C: PreCategory
F: Functor C set_cat
s, d, d': Pair
m1: morphism d d'
m2: morphism s d
(F _1 (m1.1 o m2.1)) (x s) = (F _1 m1.1) ((F _1 m2.1) (x s))
    match goal with
      | [ |- ?f ?x = ?g (?h ?x) ] => change (f x = (g o h) x)
    end.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d, d': Pair
m1: morphism d d'
m2: morphism s d
(F _1 (m1.1 o m2.1)) (x s) = (F _1 m1.1 o F _1 m2.1) (x s)
    match goal with
      | [ |- ?f ?x = ?g ?x ] => apply (@apD10 _ _ f g)
    end.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d, d': Pair
m1: morphism d d'
m2: morphism s d
F _1 (m1.1 o m2.1) = F _1 m1.1 o F _1 m2.1
    apply (composition_of F).
  Defined.

  Definition compose s d d'
             (m1 : morphism d d')
             (m2 : morphism s d)
  : morphism s d'.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d, d': Pair
m1: morphism d d'
m2: morphism s d
morphism s d'
  Proof.
H: Funext
C: PreCategory
F: Functor C set_cat
s, d, d': Pair
m1: morphism d d'
m2: morphism s d
morphism s d'
    exists (m1.1 o m2.1).
H: Funext
C: PreCategory
F: Functor C set_cat
s, d, d': Pair
m1: morphism d d'
m2: morphism s d
(F _1 (m1.1 o m2.1)) (x s) = x d'
    apply compose_H.
  Defined.

  Definition identity_H s
    := apD10 (identity_of F s.(c)) s.(x).

  Definition identity s : morphism s s.
H: Funext
C: PreCategory
F: Functor C set_cat
s: Pair
morphism s s
  Proof.
H: Funext
C: PreCategory
F: Functor C set_cat
s: Pair
morphism s s
    exists 1.
H: Funext
C: PreCategory
F: Functor C set_cat
s: Pair
(F _1 1) (x s) = x s
    apply identity_H.
  Defined.

  Global Arguments compose_H : simpl never.
  Global Arguments identity_H : simpl never.
  Global Arguments identity _ / .
  Global Arguments compose _ _ _ _ _ / .

  (** ** Category of elements *)
  Definition category : PreCategory.
H: Funext
C: PreCategory
F: Functor C set_cat
PreCategory
  Proof.
H: Funext
C: PreCategory
F: Functor C set_cat
PreCategory
    refine (@Build_PreCategory
              Pair
              (fun s d => morphism s d)
              identity
              compose
              _
              _
              _
              _);
    abstract (
        repeat intro;
        apply path_sigma_uncurried; simpl;
        ((exists (associativity _ _ _ _ _ _ _ _))
           || (exists (left_identity _ _ _ _))
           || (exists (right_identity _ _ _ _)));
        exact (center _)
      ).
  Defined.

  (** ** First projection functor *)
  Definition pr1 : Functor category C
    := Build_Functor
         category C
         c
         (fun s d => @pr1 _ _)
         (fun _ _ _ _ _ => idpath)
         (fun _ => idpath).
End Grothendieck.