Library HoTT.Categories.Grothendieck.ToSet.Core
Require Import Category.Core Functor.Core.
Require Import SetCategory.Core.
Require Import Basics.Trunc Types.Sigma.
Require Import Basics.Tactics.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Local Open Scope morphism_scope.
Section Grothendieck.
Context `{Funext}.
Require Import SetCategory.Core.
Require Import Basics.Trunc Types.Sigma.
Require Import Basics.Tactics.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
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
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.
F : C → Set
Variable C : PreCategory.
Variable F : Functor C set_cat.
Record Pair :=
{
c : C;
x : F c
}.
Definition issig_pair : { c : C | F c } <~> Pair.
Proof.
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).
Proof.
etransitivity; [ | exact (m1.2) ].
etransitivity; [ | apply ap; exact (m2.2) ].
match goal with
| [ |- ?f ?x = ?g (?h ?x) ] ⇒ change (f x = (g o h) x)
end.
match goal with
| [ |- ?f ?x = ?g ?x ] ⇒ apply (@apD10 _ _ f g)
end.
apply (composition_of F).
Defined.
Definition compose s d d'
(m1 : morphism d d')
(m2 : morphism s d)
: morphism s d'.
Proof.
∃ (m1.1 o m2.1).
apply compose_H.
Defined.
Definition identity_H s
:= apD10 (identity_of F s.(c)) s.(x).
Definition identity s : morphism s s.
Proof.
∃ 1.
apply identity_H.
Defined.
Global Arguments compose_H : simpl never.
Global Arguments identity_H : simpl never.
Global Arguments identity _ / .
Global Arguments compose _ _ _ _ _ / .
Definition category : PreCategory.
Proof.
refine (@Build_PreCategory
Pair
(fun s d ⇒ morphism s d)
identity
compose
_
_
_
_);
abstract (
repeat intro;
apply path_sigma_uncurried; simpl;
((∃ (associativity _ _ _ _ _ _ _ _))
|| (∃ (left_identity _ _ _ _))
|| (∃ (right_identity _ _ _ _)));
exact (center _)
).
Defined.
Proof.
refine (@Build_PreCategory
Pair
(fun s d ⇒ morphism s d)
identity
compose
_
_
_
_);
abstract (
repeat intro;
apply path_sigma_uncurried; simpl;
((∃ (associativity _ _ _ _ _ _ _ _))
|| (∃ (left_identity _ _ _ _))
|| (∃ (right_identity _ _ _ _)));
exact (center _)
).
Defined.