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))
                    || (progress destruct_head_hnf @EOpenSet)
                    || (apply f_equal)
                    || (apply ProofIrrelevance.proof_irrelevance)
                    || (apply proof_irrelevance_JMeq)
                    || (apply Functor_Eq)
                )).
  Defined.

End Exercise_4_2_3_2.
Module Exercise_4_2_3_2_continuity_bad.
  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 ×
                 | _progress destruct_head_hnf @ex
                 | _progress destruct_head_hnf @and
                 | _progress intuition subst
               end
      ).
  Qed.
End Exercise_4_2_3_2_continuity_bad.