Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Inductive False : Prop :=.
- Inductive True : Prop := I.
- Inductive eq {T : Type} (x : T) : T -> Prop := refl : eq x x.
- Inductive and (X Y : Type) : Type :=
- | both : X -> Y -> and X Y.
- Inductive or (X Y : Type) : Type :=
- | inleft : X -> or X Y
- | inright : Y -> or X Y.
- Inductive Sigma (T : Type) (P : T -> Type) : Type :=
- | witnessS : forall t : T, P t -> Sigma T P.
- Inductive Exists (T : Type) (P : T -> Prop) : Prop :=
- | witnessE : forall t : T, P t -> Exists T P.
- Definition pi1 {T} {P} (S : Sigma T P) : T :=
- match S with
- | witnessS t _ => t
- end.
- Theorem symm (T : Type) (x y : T) : eq x y -> eq y x.
- intro E; elim E; apply refl.
- Defined.
- Theorem trans (T : Type) (x y z : T) : eq x y -> eq y z -> eq x z.
- intro E; elim E.
- intro E'; elim E'.
- apply refl.
- Defined.
- Definition Relation (T : Type) := T -> T -> Prop.
- Record Equivalence {T : Type} (R : Relation T) :=
- { equivalence_reflexivity : forall x, R x x
- ; equivalence_symmetry : forall x y, R x y -> R y x
- ; equivalence_transitivity : forall x y z, R x y -> R y z -> R x z
- }.
- Theorem eq_Equivalence (T : Type) : Equivalence (@eq T).
- apply Build_Equivalence.
- intros x; apply refl.
- intros x y; apply symm.
- intros x y z; apply trans.
- Defined.
- Theorem eq_f_Equivalence (X T : Type) (f : X -> T) : Equivalence (fun x x' => @eq T (f x) (f x')).
- apply Build_Equivalence.
- intros x; apply refl.
- intros x y; apply symm.
- intros x y z; apply trans.
- Defined.
- Definition Respectful
- {A : Type} (R : Relation A)
- {B : Type} (S : Relation B)
- (f : A -> B) : Prop :=
- forall a a', R a a' -> S (f a) (f a').
- Record Category
- (Ob : Type) (Hom : Ob -> Ob -> Type)
- (ObEq : Relation Ob) (HomEq : forall X Y, Relation (Hom X Y)) :=
- { identity : forall {X}, Hom X X
- ; compose : forall {X Y Z}, Hom X Y -> Hom Y Z -> Hom X Z
- ; compose_respectful_left : forall {X Y Z} (f : Hom X Y),
- Respectful (HomEq Y Z) (HomEq X Z) (fun g => compose f g)
- ; compose_respectful_right : forall {X Y Z} (g : Hom Y Z),
- Respectful (HomEq X Y) (HomEq X Z) (fun f => compose f g)
- ; category_ObEq_equivalence : Equivalence ObEq
- ; category_HomEq_equivalence : forall X Y, Equivalence (HomEq X Y)
- ; category_associativity : forall X Y Z W,
- forall (f : Hom X Y) (g : Hom Y Z) (h : Hom Z W),
- HomEq _ _ (compose (compose f g) h) (compose f (compose g h))
- ; category_left_identity : forall X Y,
- forall (f : Hom X Y),
- HomEq _ _ (compose identity f) f
- ; category_right_identity : forall X Y,
- forall (f : Hom X Y),
- HomEq _ _ (compose f identity) f
- }.
- Section Setoids.
- Record Setoid :=
- { carrier : Type
- ; relation : Relation carrier
- ; setoid_relation_eq : Equivalence relation
- }.
- Definition Morphism (X Y : Setoid) :=
- Sigma (carrier X -> carrier Y) (fun f => Respectful (relation X) (relation Y) f).
- Definition Morphism_Identity (X : Setoid) : Morphism X X.
- apply (witnessS (carrier X -> carrier X) _ (fun x => x)).
- unfold Respectful; intros; assumption.
- Defined.
- Definition Morphism_Compose (X Y Z : Setoid) (f : Morphism X Y) (g : Morphism Y Z) : Morphism X Z.
- apply (witnessS (carrier X -> carrier Z) _ (fun x => pi1 g (pi1 f x))).
- destruct f; destruct g.
- unfold Respectful in *; simpl; intros.
- apply r0.
- apply r.
- assumption.
- Defined.
- Definition Morphism_equality (X Y : Setoid) (m m' : Morphism X Y) :=
- forall x : carrier X,
- relation Y (pi1 m x) (pi1 m' x).
- Definition Setoid_Isomorphism (S T : Setoid) : Prop :=
- Exists (and (Morphism S T) (Morphism T S)) (fun fg =>
- match fg with
- | both f g => and
- (Morphism_equality _ _ (Morphism_Compose _ _ _ f g)
- (Morphism_Identity _))
- (Morphism_equality _ _ (Morphism_Compose _ _ _ g f)
- (Morphism_Identity _))
- end).
- Theorem Equivalence_Setoid_Isomorphism : Equivalence (fun X Y : Setoid => Setoid_Isomorphism X Y).
- apply Build_Equivalence; unfold Setoid_Isomorphism.
- intro; apply (witnessE _ _ (both _ _ (Morphism_Identity _) (Morphism_Identity _))).
- assert (Morphism_equality x x
- (Morphism_Compose x x x (Morphism_Identity x) (Morphism_Identity x))
- (Morphism_Identity x));
- unfold Morphism_equality; unfold Morphism_Compose; simpl.
- intros; apply (setoid_relation_eq x).
- constructor.
- apply H.
- apply H.
- intros x y [[l r] [l' r']].
- apply (witnessE _ _ (both _ _ r l)).
- apply (both _ _ r' l').
- intros x y z [[l r] [l' r']] [[r'' h] [r''' h']].
- pose (Morphism_Compose _ _ _ l r'') as m.
- pose (Morphism_Compose _ _ _ h r) as m'.
- apply (witnessE _ _ (both _ _ m m')).
- constructor;
- unfold Morphism_equality in *; unfold Morphism_Compose in *; simpl in *; clear m; clear m';
- intros.
- eapply equivalence_transitivity.
- apply (setoid_relation_eq x).
- Focus 2.
- apply l'.
- assert (relation y (pi1 h (pi1 r'' (pi1 l x0))) (pi1 l x0)).
- apply r'''.
- unfold Morphism in r.
- destruct r.
- simpl.
- apply r.
- assumption.
- eapply equivalence_transitivity.
- apply (setoid_relation_eq z).
- Focus 2.
- apply h'.
- assert (relation y (pi1 l (pi1 r (pi1 h x0))) (pi1 h x0)).
- apply r'.
- unfold Morphism in r'.
- destruct r''.
- simpl.
- apply r0.
- assumption.
- Defined.
- End Setoids.
- Section SET.
- Definition SET : Category
- Setoid (fun X Y => Morphism X Y)
- (fun X Y => Setoid_Isomorphism X Y) (fun X Y f g => Morphism_equality X Y f g).
- Print Build_Category.
- apply (Build_Category
- Setoid (fun X Y => Morphism X Y)
- (fun X Y => Setoid_Isomorphism X Y) (fun X Y f g => Morphism_equality X Y f g)
- (fun X => Morphism_Identity X)
- (fun X Y Z f g => Morphism_Compose X Y Z f g));
- unfold Respectful in *;
- unfold Morphism_equality in *;
- unfold Morphism_Compose in *;
- simpl in *; intros.
- apply H.
- pose (H x).
- destruct g; simpl in *.
- unfold Respectful in *.
- apply r0.
- apply r.
- apply Equivalence_Setoid_Isomorphism.
- apply Build_Equivalence.
- intros; apply equivalence_reflexivity.
- apply (setoid_relation_eq Y).
- intros; apply equivalence_symmetry.
- apply (setoid_relation_eq Y).
- apply H.
- intros; eapply equivalence_transitivity.
- apply (setoid_relation_eq Y).
- apply H.
- apply H0.
- apply equivalence_reflexivity.
- apply (setoid_relation_eq W).
- apply equivalence_reflexivity.
- apply (setoid_relation_eq Y).
- apply equivalence_reflexivity.
- apply (setoid_relation_eq Y).
- Defined.
- End SET.
- (*
- Definition SET : Category Set (fun X Y => X -> Y) (eq) (fun _ _ f g => forall x, eq (f x) (g x)).
- apply (Build_Category
- Set (fun X Y => X -> Y) (eq) (fun _ _ f g => forall x, eq (f x) (g x))
- (fun X x => x)
- (fun X Y Z f g x => g (f x))).
- unfold Respectful; intros.
- apply H.
- unfold Respectful; intros.
- elim (H x).
- apply refl.
- apply eq_Equivalence.
- intros; apply Build_Equivalence.
- intros; apply refl.
- intros; apply symm.
- apply H.
- intros; eapply trans.
- apply H.
- apply H0.
- intros; apply refl.
- intros; apply refl.
- intros; apply refl.
- Defined.
- *)
- Record Functor
- {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq)
- {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq') :=
- { MapOb : Ob -> Ob'
- ; MapHom : forall X Y : Ob, Hom X Y -> Hom' (MapOb X) (MapOb Y)
- ; functor_respectful : forall X Y : Ob,
- Respectful (@HomEq X Y) (@HomEq' (MapOb X) (MapOb Y)) (MapHom X Y)
- ; functor_identity : forall X,
- HomEq' _ _ (identity _ _ _ _ D) (MapHom X X (identity _ _ _ _ C))
- ; functor_compose : forall X Y Z,
- forall (f : Hom X Y) (g : Hom Y Z),
- HomEq' _ _ (MapHom _ _ (compose _ _ _ _ C f g))
- (compose _ _ _ _ D (MapHom _ _ f) (MapHom _ _ g))
- }.
- Section Opposite.
- Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
- Definition Op : Category Ob (fun Y X => Hom X Y) ObEq (fun X Y f g => HomEq Y X f g).
- apply (Build_Category
- Ob (fun Y X => Hom X Y) ObEq (fun X Y f g => HomEq Y X f g)
- (fun X => identity _ _ _ _ C)
- (fun X Y Z f g => compose _ _ _ _ C g f)).
- unfold Respectful; intros.
- apply compose_respectful_right.
- assumption.
- unfold Respectful; intros.
- apply compose_respectful_left.
- assumption.
- apply (category_ObEq_equivalence _ _ _ _ C).
- intros X Y; pose (category_HomEq_equivalence _ _ _ _ C) as E.
- destruct (E Y X) as [axR axS axT].
- apply Build_Equivalence; assumption.
- intros.
- apply equivalence_symmetry.
- apply (category_HomEq_equivalence _ _ _ _ C).
- apply category_associativity.
- intros.
- apply category_right_identity.
- intros.
- apply category_left_identity.
- Defined.
- End Opposite.
- Section Functors.
- Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
- Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').
- Context {Ob'' Hom'' ObEq'' HomEq''} (E : Category Ob'' Hom'' ObEq'' HomEq'').
- Definition Functor_equality (F G : Functor C D) : Prop :=
- and (forall X, ObEq' (MapOb C D F X) (MapOb C D F X))
- (forall X Y (f : Hom X Y), HomEq' _ _ (MapHom C D F X Y f) (MapHom C D G X Y f)).
- Definition Identity_Functor : Functor C C.
- apply (Build_Functor
- _ _ _ _ C
- _ _ _ _ C
- (fun X => X)
- (fun X Y f => f)
- ).
- unfold Respectful; intros; assumption.
- intros; apply equivalence_reflexivity.
- apply (category_HomEq_equivalence _ _ _ _ C X X).
- intros; apply equivalence_reflexivity.
- apply (category_HomEq_equivalence _ _ _ _ C X Z).
- Defined.
- Definition Compose_Functors (F : Functor C D) (G : Functor D E) : Functor C E.
- apply (Build_Functor
- _ _ _ _ C
- _ _ _ _ E
- (fun X => MapOb _ _ G (MapOb _ _ F X))
- (fun X Y f => MapHom _ _ G _ _ (MapHom _ _ F _ _ f))
- ).
- unfold Respectful; intros.
- apply functor_respectful.
- apply functor_respectful.
- assumption.
- intros.
- apply equivalence_transitivity with
- (y := MapHom D E G (MapOb C D F X) (MapOb C D F X)
- (identity Ob' Hom' ObEq' HomEq' D)).
- apply (category_HomEq_equivalence _ _ _ _ E _ _).
- apply functor_identity.
- apply functor_respectful.
- apply functor_identity.
- intros.
- assert (
- HomEq' _ _
- (MapHom C D F X Z (compose Ob Hom ObEq HomEq C f g))
- (compose _ _ _ _ D
- (MapHom C D F X Y f)
- (MapHom C D F Y Z g))) as lemma by apply functor_compose.
- Print functor_respectful.
- pose (functor_respectful D E G _ _ _ _ lemma) as lemma'.
- eapply equivalence_transitivity.
- apply (category_HomEq_equivalence _ _ _ _ E _ _).
- apply lemma'.
- apply (functor_compose D E G).
- Defined.
- End Functors.
- Section Isomorphism.
- Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
- Record Isomorphism {X Y : Ob} (iso : Hom X Y) :=
- { inverse : Hom Y X
- ; isomorphism_left_inverse : HomEq _ _ (compose _ _ _ _ C inverse iso) (identity _ _ _ _ C)
- ; isomorphism_right_inverse : HomEq _ _ (compose _ _ _ _ C iso inverse) (identity _ _ _ _ C)
- }.
- End Isomorphism.
- Section Terminal.
- Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
- Record Terminal :=
- { terminal_object : Ob
- ; terminal_morphism : forall X, Hom X terminal_object
- ; terminal_morphism_unique : forall X (f : Hom X terminal_object),
- HomEq _ _ f (terminal_morphism X)
- }.
- Theorem Terminal_Isomorphism (terminal : Terminal) :
- Isomorphism C (terminal_morphism terminal (terminal_object terminal)).
- apply (Build_Isomorphism
- C _ _ _
- (terminal_morphism terminal (terminal_object terminal))).
- apply equivalence_transitivity with (y := terminal_morphism terminal (terminal_object terminal)).
- apply (category_HomEq_equivalence _ _ _ _ C _ _).
- apply terminal_morphism_unique.
- apply equivalence_symmetry.
- apply (category_HomEq_equivalence _ _ _ _ C _ _).
- apply terminal_morphism_unique.
- apply equivalence_transitivity with (y := terminal_morphism terminal (terminal_object terminal)).
- apply (category_HomEq_equivalence _ _ _ _ C _ _).
- apply terminal_morphism_unique.
- apply equivalence_symmetry.
- apply (category_HomEq_equivalence _ _ _ _ C _ _).
- apply terminal_morphism_unique.
- Defined.
- End Terminal.
- Section Initial.
- Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
- Definition Initial := @Terminal Ob (fun Y X => Hom X Y) (fun X Y f g => HomEq Y X f g).
- Definition initial_object (i : Initial) := terminal_object i.
- Definition initial_morphism (i : Initial) : forall X, Hom (initial_object i) X.
- destruct i as [termOb termMor termUniq].
- simpl.
- intro; apply termMor.
- Defined.
- Definition initial_morphism_unique (i : Initial) : forall X (f : Hom (initial_object i) X), HomEq _ _ f (initial_morphism i X).
- destruct i as [termOb termMor termUniq]; simpl.
- intros.
- apply termUniq.
- Defined.
- Theorem Initial_Isomorphism (i : Initial) :
- Isomorphism C (initial_morphism i (initial_object i)).
- pose (@Terminal_Isomorphism _ _ _ _ (Op C) i) as t.
- destruct t as [tInv tInvL tInvR]; simpl in *.
- destruct i as [iObj iMor iUniq]; simpl in *.
- apply Build_Isomorphism with (inverse := tInv).
- apply tInvR.
- apply tInvL.
- Defined.
- End Initial.
- Section NaturalTransform.
- Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
- Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').
- Context (F : Functor C D) (G : Functor C D).
- Record NaturalTransform :=
- { eta_ : forall X, Hom' (MapOb _ _ F X) (MapOb _ _ G X)
- ; naturality : forall X Y,
- forall f : Hom X Y,
- HomEq' _ _ (compose _ _ _ _ D (MapHom _ _ F _ _ f) (eta_ Y))
- (compose _ _ _ _ D (eta_ X) (MapHom _ _ G _ _ f))
- }.
- End NaturalTransform.
- Section CategoryOfSmallCats.
- Record SmallCategory :=
- { S : Set
- ; R : Relation S
- ; Hom : S -> S -> Set
- ; HomR : forall X Y, Relation (Hom X Y)
- ; smallCategory_carrier : Category S Hom R HomR
- }.
- Definition SmallCategory_Isomorphism : Relation SmallCategory.
- unfold Relation.
- intros [S_C R_C Hom_C HomR_C C] [S_D R_D Hom_D HomR_D D].
- Admitted.
- Definition SmallFunctor (C : SmallCategory) (D : SmallCategory) := Functor (smallCategory_carrier C) (smallCategory_carrier D).
- Axiom SmallFunctor_Isomorphism : forall C D, Relation (SmallFunctor C D).
- Definition CAT : Category SmallCategory SmallFunctor SmallCategory_Isomorphism SmallFunctor_Isomorphism.
- Print Build_Category.
- apply (Build_Category
- SmallCategory SmallFunctor SmallCategory_Isomorphism SmallFunctor_Isomorphism
- (fun X =>
- Identity_Functor (smallCategory_carrier X))
- (fun X Y Z f g =>
- Compose_Functors (smallCategory_carrier X)
- (smallCategory_carrier Y)
- (smallCategory_carrier Z)
- f g)).
- Admitted.
- End CategoryOfSmallCats.
- Section NaturalTransforms.
- Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
- Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').
- Context (F : Functor C D) (G : Functor C D) (H : Functor C D).
- Context (eta : NaturalTransform C D F G).
- Context (nu : NaturalTransform C D G H).
- Definition Identity_NaturalTransform'' : NaturalTransform C C (Identity_Functor C) (Identity_Functor C).
- Print Build_NaturalTransform.
- apply (Build_NaturalTransform
- C C (Identity_Functor C) (Identity_Functor C)
- (fun X => identity _ _ _ _ C)).
- simpl; intros.
- eapply equivalence_transitivity.
- apply (category_HomEq_equivalence _ _ _ _ C).
- apply category_right_identity.
- apply equivalence_symmetry.
- apply (category_HomEq_equivalence _ _ _ _ C).
- apply category_left_identity.
- Defined.
- Definition Identity_NaturalTransform : NaturalTransform C D F F.
- Print Build_NaturalTransform.
- apply (Build_NaturalTransform
- C D F F
- (fun X => identity _ _ _ _ D)).
- simpl; intros.
- eapply equivalence_transitivity.
- apply (category_HomEq_equivalence _ _ _ _ D).
- apply category_right_identity.
- apply equivalence_symmetry.
- apply (category_HomEq_equivalence _ _ _ _ D).
- apply category_left_identity.
- Defined.
- Definition Compose_NaturalTransformations : NaturalTransform C D F H.
- Print Build_NaturalTransform.
- Print eta_.
- apply (Build_NaturalTransform
- C D F H
- (fun X => compose _ _ _ _ D (eta_ C D F G eta X) (eta_ C D G H nu X))).
- intros.
- apply equivalence_transitivity with
- (y := compose _ _ _ _ D
- (compose Ob' Hom' ObEq' HomEq' D (MapHom C D F X Y f)
- (eta_ C D F G eta Y))
- (eta_ C D G H nu Y)).
- apply (category_HomEq_equivalence _ _ _ _ D).
- eapply equivalence_symmetry.
- apply (category_HomEq_equivalence _ _ _ _ D).
- apply (category_associativity).
- apply equivalence_transitivity with
- (y := compose _ _ _ _ D (eta_ C D F G eta _)
- (compose _ _ _ _ D (MapHom C D G _ _ f)
- (eta_ C D G H nu Y))).
- apply (category_HomEq_equivalence _ _ _ _ D).
- eapply equivalence_symmetry.
- apply (category_HomEq_equivalence _ _ _ _ D).
- eapply equivalence_transitivity with
- (y := compose Ob' Hom' ObEq' HomEq' D
- (compose Ob' Hom' ObEq' HomEq' D (eta_ C D F G eta _)
- (MapHom C D G X Y f)) (eta_ C D G H nu Y)).
- apply (category_HomEq_equivalence _ _ _ _ D).
- eapply equivalence_symmetry.
- apply (category_HomEq_equivalence _ _ _ _ D).
- apply category_associativity.
- apply compose_respectful_right.
- eapply equivalence_symmetry.
- apply (category_HomEq_equivalence _ _ _ _ D).
- apply naturality.
- eapply equivalence_symmetry.
- apply (category_HomEq_equivalence _ _ _ _ D).
- eapply equivalence_transitivity with
- (y := compose Ob' Hom' ObEq' HomEq' D (eta_ C D F G eta X)
- (compose Ob' Hom' ObEq' HomEq' D
- (eta_ C D G H nu X) (MapHom C D H X Y f))).
- apply (category_HomEq_equivalence _ _ _ _ D).
- apply category_associativity.
- apply compose_respectful_left.
- eapply equivalence_symmetry.
- apply (category_HomEq_equivalence _ _ _ _ D).
- apply naturality.
- Defined.
- End NaturalTransforms.
- Section FunctorCategory.
- Context {Ob Hom ObEq HomEq} (C : Category Ob Hom ObEq HomEq).
- Context {Ob' Hom' ObEq' HomEq'} (D : Category Ob' Hom' ObEq' HomEq').
- Definition FunctorCategory : Category
- (Functor C D) (NaturalTransform C D)
- (fun F G => forall c, F c = G c) (fun _ _ _ _ => True).
- Print Identity_NaturalTransform.
- apply (Build_Category
- (Functor C D) (NaturalTransform C D)
- (fun F G => _) (fun _ _ _ _ => True)
- (fun F => Identity_NaturalTransform C D F)
- (fun F G H eta nu => Compose_NaturalTransformations C D F G H eta nu)).
- (*
- *** Local Variables: ***
- *** coq-prog-args: ("-emacs-U" "-nois") ***
- *** End: ***
- *)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement