# Library Exercise_4_2_3_2

Require Import Utf8.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import Common Notations FEqualDep SetCategory TopologyCategory PreOrderCategory Functor Morphism Duals IndiscreteTopology DiscreteTopology.

Set Implicit Arguments.

Generalizable All Variables.

Local Open Scope topology_scope.

# Exercise 4.2.3.2

Section Exercise_4_2_3_2.
Require Import ClassicalFacts.

## Problem

Explain how "looking at points" gives a functor Top Set. Does "looking at open sets" give a functor Top PrO?

Definition UnderlyingPoints : Functor CategoryOfTopologies CategoryOfTypes.
refine {| ObjectOf := (fun X : CategoryOfTopologies
X : CategoryOfTypes);
MorphismOf := (fun s d (m : Morphism CategoryOfTopologies s d)
proj1_sig m : Morphism CategoryOfTypes _ _) |};
reflexivity.
Defined.

Record > EOpenSet `(Topology X) :=
{
OpenSetSet :> Ensemble X;
OpenSetOpen :> Open OpenSetSet
}.

Lemma OpenSet_eq `(T : Topology X) (A B : EOpenSet T)
: OpenSetSet A = OpenSetSet B
→ A = B.
destruct A, B; simpl; intro; subst;
f_equal; apply ProofIrrelevance.proof_irrelevance.
Qed.

Global Instance opens_ordered_by_inclusion `(Topology X)
: @PreOrder (EOpenSet _) (fun U VU V).
split; firstorder.
Qed.

Definition continuous_induced_functor_object_of
s d (m : Morphism CategoryOfTopologies s d)
: (opens_ordered_by_inclusion d) → (opens_ordered_by_inclusion s).
intro; hnf in ×.
(inverse_image (proj1_sig m) X);
simpl.
abstract (
destruct m as [f c];
apply c;
destruct X;
assumption
).
Defined.

Definition continuous_induced_functor_morphism_of
s d (m : Morphism CategoryOfTopologies s d)
: s' d' (m' : Morphism (PreOrderCategory (opens_ordered_by_inclusion d))
s'
d'),
Morphism (PreOrderCategory (opens_ordered_by_inclusion s))
(continuous_induced_functor_object_of m s')
(continuous_induced_functor_object_of m d').
intros s' d' m' x H.
hnf in m, m'.
simpl in ×.
destruct m as [ f c ]; simpl in ×.
repeat unfold Ensembles.In, inverse_image in ×.
intuition.
Qed.

Definition continuous_induced_functor
s d (m : Morphism CategoryOfTopologies s d)
: Morphism CategoryOfPreOrders
(opens_ordered_by_inclusion d)
(opens_ordered_by_inclusion s).
refine {| ObjectOf := (continuous_induced_functor_object_of m);
MorphismOf := (continuous_induced_functor_morphism_of m) |};
abstract (intros; simpl; apply ProofIrrelevance.proof_irrelevance).
Defined.
Definition PreOrderedSets
: Functor CategoryOfTopologies (OppositeCategory CategoryOfPreOrders).
refine (Build_Functor CategoryOfTopologies
(OppositeCategory CategoryOfPreOrders)
(fun xopens_ordered_by_inclusion x)
continuous_induced_functor
_
_);
abstract (repeat (
reflexivity
|| (progress (simpl; intros; expand))
|| (apply f_equal)
|| (apply ProofIrrelevance.proof_irrelevance)
|| (apply proof_irrelevance_JMeq)
|| (apply Functor_Eq)
)).
Defined.

End Exercise_4_2_3_2.
Inductive Three := A | B | C.

Definition ThreeTopology1 : Topology Three
:= DiscreteTopology _.
Definition ThreeTopology2 : Topology Three
:= IndiscreteTopology _.

Definition f := @id Three.
Definition continuous_function_continuous : continuous ThreeTopology1 ThreeTopology2 f.
repeat intro; constructor.
Defined.

Lemma f_not_preserve_open : S,
@Open _ ThreeTopology1 S
¬@Open _ ThreeTopology2 (image f S).
(fun xmatch x with
| ATrue
| _False
end);
abstract (
simpl; intuition; firstorder subst;
fg_equal;
repeat match goal with
| [ H : _ |- _ ] ⇒ pose proof (H A);
pose proof (H B);
pose proof (H C);
clear H
| [ H : @eq Prop ?a ?b |- _ ]
⇒ let H' := fresh in
assert (H' : a b) by (rewrite H; firstorder);
clear H;
destruct H';
intuition
| [ H : _ : ?T, _ |- _ ]
⇒ match type of T with
| Proplet t := fresh in
assert (t : T) by (repeat esplit;
try reflexivity;
trivial);
specialize (H t)
end
| _progress compute in ×