290 lines
9.4 KiB
Coq
290 lines
9.4 KiB
Coq
(* Exercises on Category Theory in UniMath *)
|
||
(* for lecture by Peter LeFanu Lumsdaine, Thu 2017-12-14 *)
|
||
(* School and Workshop on Univalent Maths, Birmingham 2017 *)
|
||
(* https://unimath.github.io/bham2017/ *)
|
||
|
||
Require Import UniMath.MoreFoundations.All.
|
||
Require Import UniMath.CategoryTheory.Core.Prelude.
|
||
Require Import UniMath.CategoryTheory.Core.Setcategories.
|
||
Require Import UniMath.CategoryTheory.Categories.HSET.All.
|
||
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
|
||
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
|
||
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
|
||
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
|
||
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
|
||
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
|
||
Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
|
||
Require Import UniMath.CategoryTheory.Limits.Terminal.
|
||
Require Import UniMath.CategoryTheory.Limits.Initial.
|
||
Require Import UniMath.CategoryTheory.Limits.FinOrdProducts.
|
||
Require Import UniMath.CategoryTheory.Limits.Equalizers.
|
||
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
|
||
Require Import UniMath.CategoryTheory.Adjunctions.Core.
|
||
Require Import UniMath.CategoryTheory.Monads.Monads.
|
||
Require Import UniMath.Combinatorics.StandardFiniteSets.
|
||
Require Import UniMath.CategoryTheory.Limits.BinProducts.
|
||
|
||
Local Open Scope cat.
|
||
|
||
(* NOTE: some of these exercises (or parts of them) are straightforward, while other parts are intended to be quite difficult. So I don’t recomment aiming to complete them in order — if stuck on a difficult part, move on and come back for another attempt later!
|
||
|
||
Skeleton solutions and hints are provided, to exhibit good tools and techniques for working with categories. However, you may well want to add extra definitions/lemmas besides the ones suggested in the skeleton. *)
|
||
|
||
Section Exercise_0.
|
||
(** Univalent categories
|
||
|
||
Show that in any univalent category, the type of objects has h-level 3 *)
|
||
|
||
Proposition isofhlevel3_ob_of_univalent_cat (C : category) (H : is_univalent C)
|
||
: isofhlevel 3 (ob C).
|
||
Proof.
|
||
unfold isofhlevel. intros x y.
|
||
unfold is_univalent in H.
|
||
induction C as [PC HS]. unfold has_homsets in HS.
|
||
enough (H2 : isaset (x = y)). apply H2.
|
||
set (eq := idtoiso ,, H x y).
|
||
apply (isofhlevelweqb 2 eq).
|
||
apply isofhleveltotal2.
|
||
{ apply HS. }
|
||
{ intros f. apply isofhleveltotal2.
|
||
{ apply HS. }
|
||
{ intros g. apply isofhleveltotal2.
|
||
{ apply isasetaprop. apply HS. }
|
||
{ intros p. apply isasetaprop. apply HS. }
|
||
}
|
||
}
|
||
Defined.
|
||
|
||
End Exercise_0.
|
||
|
||
Section Exercise_1.
|
||
(** Non-univalent categories
|
||
|
||
Problem: Construct the category with objects the natural numbers, and with maps m->n all functions {1,…,m}->{1,…,n}. Show that this is a set-category, and that it is NOT univalent.
|
||
|
||
Hint: for defining categories (and other large multi-component structures), it’s usually better to define them a few components at a time, following the structure of the definition, as the following skeleton suggests.
|
||
|
||
An alternative approach is to go directly for the total structure [Definition nat_category : category], then begin with [use makecategory.] and construct the whole thing in a single interactive proof. This approach can be good for first finding a proof/construction; but it often causes speed issues down the line, because the resulting term is very large. *)
|
||
|
||
Definition nat_category_ob_mor : precategory_ob_mor.
|
||
Proof.
|
||
unfold precategory_ob_mor. use tpair.
|
||
{ exact nat. }
|
||
{ simpl. intros x y. exact (stn x -> stn y). }
|
||
Defined.
|
||
|
||
Definition nat_category_data : precategory_data.
|
||
Proof.
|
||
unfold precategory_data. use tpair.
|
||
{ unfold precategory_ob_mor. use tpair.
|
||
{ exact nat. }
|
||
{ simpl. intros x y. exact (stn x -> stn y). }
|
||
}
|
||
{ simpl. unfold precategory_id_comp. use tpair.
|
||
{ intros. }
|
||
}
|
||
Admitted.
|
||
|
||
Definition nat_category_is_precategory : is_precategory nat_category_data.
|
||
Proof.
|
||
Admitted.
|
||
|
||
Definition nat_category : category.
|
||
Proof.
|
||
Admitted.
|
||
|
||
Definition nat_setcategory : setcategory.
|
||
Proof.
|
||
Admitted.
|
||
|
||
Proposition nat_category_not_univalent : ¬ (is_univalent nat_category).
|
||
Proof.
|
||
Admitted.
|
||
|
||
End Exercise_1.
|
||
|
||
Section Exercise_2.
|
||
(* Exercise 2.1: Define `pointed_disp_cat` with `disp_struct`. *)
|
||
Definition pointed_disp_cat
|
||
: disp_cat SET.
|
||
Proof.
|
||
Admitted.
|
||
|
||
(* Exercise 2.2: Define a displayed category on sets of a binary operation on them.
|
||
The displayed objects over `X` are maps `X × X → X` and the displayed morphisms over `f` are proofs that `f` preserves the operation.
|
||
*)
|
||
Definition operation_disp_cat
|
||
: disp_cat SET.
|
||
Proof.
|
||
Admitted.
|
||
|
||
(* Using the product of displayed categories, we now define *)
|
||
Definition pointed_operation_disp_cat
|
||
: disp_cat SET.
|
||
Proof.
|
||
use dirprod_disp_cat.
|
||
- exact pointed_disp_cat.
|
||
- exact operation_disp_cat.
|
||
Defined.
|
||
|
||
(* This gives rise to a total category *)
|
||
Definition pointed_operation_set
|
||
: category
|
||
:= total_category pointed_operation_disp_cat.
|
||
|
||
(* For convenience, we define some projection to access the structure *)
|
||
Definition carrier
|
||
(X : pointed_operation_set)
|
||
: hSet
|
||
:= pr1 X.
|
||
|
||
Definition unit_el
|
||
(X : pointed_operation_set)
|
||
: carrier X.
|
||
Proof.
|
||
Admitted.
|
||
(* Once defined, the following should type check. *)
|
||
(* := pr12 X. *)
|
||
|
||
Definition mul
|
||
(X : pointed_operation_set)
|
||
: carrier X → carrier X → carrier X.
|
||
Admitted.
|
||
(* Once defined, the following should type check. *)
|
||
(* := λ x y, pr22 X (x ,, y). *)
|
||
|
||
(* Exercise 2.3: Define the category of monoid displayed category.
|
||
Hint: use `disp_full_sub`.
|
||
*)
|
||
Definition monoid_laws_disp_cat
|
||
: disp_cat pointed_operation_set.
|
||
Proof.
|
||
Admitted.
|
||
|
||
Definition monoids
|
||
: category
|
||
:= total_category monoid_laws_disp_cat.
|
||
|
||
(* During the lecture, we already showed that pointed sets are univalent as follows *)
|
||
Definition pointed_is_univalent_disp
|
||
: is_univalent_disp pointed_disp_cat.
|
||
Proof.
|
||
Admitted.
|
||
(* Once everything is in place, the following proof should work. *)
|
||
(*
|
||
apply is_univalent_disp_from_fibers.
|
||
intros X x₁ x₂.
|
||
use isweqimplimpl.
|
||
- intros f.
|
||
apply f.
|
||
- apply X.
|
||
- apply isaproptotal2.
|
||
+ intro.
|
||
apply isaprop_is_iso_disp.
|
||
+ intros p q r₁ r₂.
|
||
apply X.
|
||
Defined.
|
||
*)
|
||
|
||
(* Exercise 2.4: Show that each part gives rise to a displayed univalent category and conclude that the total category is univalent.
|
||
Hint: adapt the proof from the lecture notes.
|
||
*)
|
||
Definition operation_is_univalent_disp
|
||
: is_univalent_disp operation_disp_cat.
|
||
Proof.
|
||
apply is_univalent_disp_from_fibers.
|
||
Admitted.
|
||
|
||
(* Now we conclude *)
|
||
Definition pointed_operation_is_univalent_disp
|
||
: is_univalent_disp pointed_operation_disp_cat.
|
||
Proof.
|
||
use dirprod_disp_cat_is_univalent.
|
||
- exact pointed_is_univalent_disp.
|
||
- exact operation_is_univalent_disp.
|
||
Defined.
|
||
|
||
Definition pointed_operation_is_univalent
|
||
: is_univalent pointed_operation_set.
|
||
Proof.
|
||
apply is_univalent_total_category.
|
||
- exact is_univalent_HSET.
|
||
- exact pointed_operation_is_univalent_disp.
|
||
Defined.
|
||
|
||
(* Exercise 2.5: conclude that the category of monoids is univalent. *)
|
||
Definition monoid_is_univalent_disp
|
||
: is_univalent_disp monoid_laws_disp_cat.
|
||
Proof.
|
||
Admitted.
|
||
|
||
Definition monoids_is_univalent
|
||
: is_univalent monoids.
|
||
Proof.
|
||
apply is_univalent_total_category.
|
||
- exact pointed_operation_is_univalent.
|
||
- exact monoid_is_univalent_disp.
|
||
Defined.
|
||
End Exercise_2.
|
||
|
||
|
||
Section Exercise_3.
|
||
(** Limits and colimits.
|
||
|
||
1. Define the empty graph and empty diagram, and show that any limit of the empty diagram is a terminal object in the directly-defined sense.
|
||
*)
|
||
|
||
Definition empty_graph : graph.
|
||
Proof.
|
||
Admitted.
|
||
|
||
Definition empty_diagram (C : category) : diagram empty_graph C.
|
||
Proof.
|
||
Admitted.
|
||
|
||
Definition isTerminal_limit_of_empty_diagram
|
||
{C} (L : LimCone (empty_diagram C))
|
||
: isTerminal _ (lim L).
|
||
Proof.
|
||
Admitted.
|
||
|
||
(* 2. Show that for a univalent category, “having an initial object” is a property. *)
|
||
Definition isaprop_initial_obs_of_univalent_category
|
||
{C : univalent_category}
|
||
: isaprop (Initial C).
|
||
Proof.
|
||
Admitted.
|
||
|
||
(* 3. Show that if a category has equalisers and finite products, then it has pullbacks *)
|
||
Definition pullbacks_from_equalizers_and_products {C : category}
|
||
: Equalizers C -> BinProducts C -> Pullbacks C.
|
||
Proof.
|
||
Admitted.
|
||
|
||
End Exercise_3.
|
||
|
||
Section Exercise_4.
|
||
(** Functors and natural transformations / monads and adjunctions
|
||
|
||
Prove that an adjunction induces a monad. Construct the Kleisli category of a monad. Show that the Kleisli construction does not preserve univalence: that is, give an example of a monad on a univalent category whose Kleisli category is not univalent. *)
|
||
|
||
(* Hint: as usual, it may be helpful to break out parts of these multi-component structures as separate definitions. *)
|
||
|
||
Definition monad_from_adjunction {C D : category}
|
||
(F : functor C D) (G : functor D C) (A : are_adjoints F G)
|
||
: Monad C.
|
||
Proof.
|
||
Admitted.
|
||
|
||
Definition kleisli_cat {C : category} (T : Monad C) : category.
|
||
Proof.
|
||
(* see <https://en.wikipedia.org/wiki/Kleisli_category> *)
|
||
Admitted.
|
||
|
||
Theorem kleisli_breaks_univalence
|
||
: ∑ (C : univalent_category) (T : Monad C), ¬ is_univalent (kleisli_cat T).
|
||
Proof.
|
||
Admitted.
|
||
|
||
End Exercise_4.
|