Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Last active March 22, 2024 10:00
Show Gist options
  • Save Lysxia/c33a3757f4184e993610d73cff757265 to your computer and use it in GitHub Desktop.
Save Lysxia/c33a3757f4184e993610d73cff757265 to your computer and use it in GitHub Desktop.
(* https://proofassistants.stackexchange.com/questions/3841/assistance-using-destruct-on-an-equality-proof-for-functors/3843 *)
(* Proof of associativity of functor composition without UIP *)
(* 1. Intuition: treat equality as a proper algebraic structure:
think of it as a category (aka. the discrete category), not an equivalence relation. *)
(* 1a. An equality between morphisms, f = g, becomes the existence of a morphism between f and g. *)
(* 1b. In the definition of a category, homsets are thus categories.
The resulting structure is known as a 2-category. https://ncatlab.org/nlab/show/2-category
You can kepp applying the same generalization to the morphism category, resulting
in the concepts of n-category and infinity-category. https://ncatlab.org/nlab/show/infinity-category *)
(* 2. In the definition of Functor_Composition, we need to prove
AF G (AF F (o f g)) = o (AF G (AF F f)) (AF G (AF F g)).
Reinterpret that as constructing a "=-morphism" (morphism in the discrete category)
between those two "B-morphisms" (where B is the category containing f and g). *)
(* 2a. Instead of "rewrite", use categorical constructs in the "=" category:
- eq_trans : x = y -> y = z -> x = z (composition of morphisms, aka. transitivity)
- f_equal : forall (f : A -> B) (x y : A), x = y -> f x = f y (functions are endofunctors in "=")
especially the specialization to the functor mapping
f_equal (AF F) : f = g -> AF F f = AF F g
(also of course, eq_refl : x = x)
Their equations can be found via "Search eq_trans" and "Search f_equal".
*)
(* 3. In the proof of associativity of Functor_Composition, equalities between equalities can now
be reasoned about as equalities between morphism.
It's just category theory in the discrete category. *)
Definition Function_Extensionality := forall (A:Type) (B: A -> Type) (f g: (forall (a:A),B a)), (forall a: A, f a = g a) -> f = g.
Record Category_By_Hom_Types := {
object_type : Type;
morphism_type : object_type -> object_type -> Type;
identity_morphism : forall (A: object_type), (morphism_type A A);
morphism_composition : forall (X Y Z: object_type) (g : (morphism_type Y Z)) (f : (morphism_type X Y)), (morphism_type X Z);
composition_associator : forall (W X Y Z: object_type) (h : (morphism_type Y Z)) (g : (morphism_type X Y)) (f : (morphism_type W X)), morphism_composition _ _ _ h (morphism_composition _ _ _ g f) = (morphism_composition _ _ _ (morphism_composition _ _ _ h g) f);
identity_morphism_left_unitor : forall (X Y: object_type) (f: (morphism_type X Y)), morphism_composition _ _ _ (identity_morphism Y) f = f;
identity_morphism_right_unitor : forall (X Y: object_type) (f: (morphism_type X Y)), morphism_composition _ _ _ f (identity_morphism X) = f;
}.
(* Shorthands for Categories *)
Notation CHT := Category_By_Hom_Types.
Notation O := object_type.
Notation A := morphism_type.
Notation o := ( morphism_composition _ _ _ _ ).
Notation i := identity_morphism.
Notation i_left_unit := (identity_morphism_left_unitor).
Notation i_right_unit := (identity_morphism_right_unitor).
Notation o_assoc := composition_associator.
Record Functor_By_Hom_Types (C D : Category_By_Hom_Types) := {
map_of_objects : O C -> O D;
map_of_morphisms : forall (X Y: O C), (A C X Y) -> (A D ( map_of_objects X) (map_of_objects Y));
functor_commutes_with_composition : forall (X Y Z: O C) (g: (A C Y Z)) (f: (A C X Y)), map_of_morphisms _ _ (o g f) = o (map_of_morphisms _ _ g) (map_of_morphisms _ _ f);
functor_commutes_with_identity : forall (X: O C), map_of_morphisms _ _ (i C X) = (i D (map_of_objects X));
}.
(* Shorthands for Functors *)
Notation FHT := Functor_By_Hom_Types.
Notation OF := (map_of_objects _ _).
Notation AF F := (map_of_morphisms _ _ F _ _).
Notation comm_F := (functor_commutes_with_composition _ _).
Notation unit_F := (functor_commutes_with_identity _ _).
Lemma Functor_Composition : forall (B C D : CHT) (G: (FHT C D)) (F: (FHT B C)) ,(FHT B D).
Proof.
intros B C D G F.
unshelve econstructor.
- exact (fun X => OF G (OF F X)).
- exact (fun X Y f => AF G (AF F f)).
- cbn. intros.
transitivity (AF G (o (AF F g) (AF F f))).
+ apply (f_equal (AF G)). apply (comm_F F).
+ apply (comm_F G).
- cbn. intros.
transitivity (AF G (i C (OF F X))).
+ apply (f_equal (AF G)). apply (unit_F F).
+ apply (unit_F G).
Defined.
Notation oFunctor := (Functor_Composition _ _ _).
Parameter function_extensionality : Function_Extensionality.
Lemma Functor_Composition_Assoc : forall (B C D E : CHT) (H : FHT D E) (G : FHT C D) (F : FHT B C),
oFunctor H (oFunctor G F) = oFunctor (oFunctor H G) F.
Proof.
intros. unfold oFunctor; cbn. f_equal.
- do 5 (apply function_extensionality; intros).
(* With some simplified notations, this is an equality between morphisms (in the discrete category):
o (EF H (o (EF G (comm_F F)) (comm_F G))) (comm_F H)
= o (EF (oFunctor H G) (comm_F F)) (o (EF G (comm_F F)) (comm_F H))
where o = eq_trans, EF K = f_equal (AF K)
Proof by functoriality of EF ("eq_trans_map_distr")
and associativity of o ("eq_trans_assoc").
*)
apply (eq_trans (f_equal (fun e => eq_trans e _) (eq_trans_map_distr (AF H) _ _))).
apply (eq_trans (eq_sym (eq_trans_assoc _ _ _))).
f_equal. apply f_equal_compose.
- apply function_extensionality; intros.
(* same as above, with unit_F instead of comm_F *)
apply (eq_trans (f_equal (fun e => eq_trans e _) (eq_trans_map_distr (AF H) _ _))).
apply (eq_trans (eq_sym (eq_trans_assoc _ _ _))).
f_equal. apply f_equal_compose.
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment