Skip to content

Commit

Permalink
Merge pull request #1778 from Alizter/ps/branch/wildcat__show_univers…
Browse files Browse the repository at this point in the history
…e_is_a_2_cat
  • Loading branch information
Alizter authored Oct 17, 2023
2 parents aa5b8d5 + 21209e7 commit 9922cad
Showing 1 changed file with 65 additions and 4 deletions.
69 changes: 65 additions & 4 deletions theories/WildCat/Universe.v
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
Require Import Basics.Overture Basics.Tactics Basics.Equivalences Types.Equiv.
Require Import WildCat.Core.
Require Import WildCat.Equiv.
Require Import Basics.Overture Basics.Tactics Basics.Equivalences Basics.PathGroupoids.
Require Import Types.Equiv.
Require Import WildCat.Core WildCat.Equiv WildCat.NatTrans WildCat.TwoOneCat.

(** ** The category of types *)
(** ** The (1-)category of types *)

Global Instance isgraph_type@{u v} : IsGraph@{v u} Type@{u}
:= Build_IsGraph Type@{u} (fun a b => a -> b).
Expand Down Expand Up @@ -112,3 +112,64 @@ Proof.
intros f x.
by destruct (f x).
Defined.

(** ** The 2-category of types *)

Global Instance is3graph_type : Is3Graph Type.
Proof.
intros A B f g.
apply Build_IsGraph.
intros p q.
exact (p == q).
Defined.

Global Instance is1cat_type_hom A B : Is1Cat (A $-> B).
Proof.
repeat unshelve esplit.
- intros f g h p q x.
exact (q x @ p x).
- intros; by symmetry.
- intros f h p x.
exact (p x @@ 1).
- intros g h p x.
exact (1 @@ p x).
- intros ? ? ? ? ? ? ? ?; apply concat_p_pp.
- intros ? ? ? ?. apply concat_p1.
- intros ? ? ? ?. apply concat_1p.
Defined.

Global Instance is1gpd_type_hom (A B : Type) : Is1Gpd (A $-> B).
Proof.
repeat unshelve esplit.
- intros ? ? ? ?; apply concat_pV.
- intros ? ? ? ?; apply concat_Vp.
Defined.

Global Instance is1functor_cat_postcomp {A B C : Type} (g : B $-> C)
: Is1Functor (cat_postcomp A g).
Proof.
repeat unshelve esplit.
- intros ? ? ? ? p ?; exact (ap _ (p _)).
- intros ? ? ? ? ? ?; cbn; apply ap_pp.
Defined.

Global Instance is1functor_cat_precomp {A B C : Type} (f : A $-> B)
: Is1Functor (cat_precomp C f).
Proof.
repeat unshelve esplit.
intros ? ? ? ? p ?; exact (p _).
Defined.

Global Instance is21cat_type : Is21Cat Type.
Proof.
snrapply Build_Is21Cat.
1-6: exact _.
- intros a b c d f g h i p x; cbn.
exact (concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^).
- intros a b f g p x; cbn.
exact (concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
- intros a b f g p x; cbn.
exact (concat_p1 _ @ (concat_1p _)^).
- reflexivity.
- reflexivity.
Defined.

0 comments on commit 9922cad

Please sign in to comment.