Conceptual Mathematics, Session 10, exercises

Session10.agda

{- Conceptual Mathematics, Session 10, exercises -}

module Session10 where

open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; _≢_)
open import Data.Product using (∃; _,_; _×_)
open import Relation.Nullary using (¬_)

-- contraposition : ∀ {l} -> ∀ {A B : Set l} -> (A -> B) -> ¬ B -> ¬ A
-- contraposition f nb a = nb (f a)

_∧_ = _×_

infixl 2 _∧_

module Exercises
  {l}
  (_⟿_ : Set l -> Set l -> Set l) {- morphism -}
  (Id : ∀ {a} -> (a ⟿ a))
  (_∘_ : ∀ {a b c} -> (b ⟿ c) -> (a ⟿ b) -> (a ⟿ c))
  (LeftIdLaw : ∀ {a b} -> ∀ (f : a ⟿ b) -> Id ∘ f ≡ f)
  (RightIdLaw : ∀ {a b} -> ∀ (f : a ⟿ b) -> f ∘ Id ≡ f)
  (AssocLaw : ∀ {a b c d} {f : c ⟿ d} {g : b ⟿ c} {h : a ⟿ b} -> (f ∘ g) ∘ h ≡ f ∘ (g ∘ h))
  (Continuous : ∀ {a b} -> ∀ (f : a ⟿ b) -> Set)
  (ContinuousCompose : ∀ {a b c} {f : b ⟿ c} {g : a ⟿ b} -> Continuous f -> Continuous g -> Continuous (f ∘ g))

  (E : Set l)
  (I : Set l)
  (C : Set l)
  (D : Set l)
  (S : Set l)
  (B : Set l)
  where

  module Exercise1
    (f : D ⟿ D)
    (cf : Continuous f)
    (g : D ⟿ D)
    (cg : Continuous g)
    (j : C ⟿ D)
    (gj≡j : g ∘ j ≡ j)
    {- fx≢gx : ∀x -> f(x) ≢ g(x) , r := arrowCrossC fx≢gx -}
    (arrowCrossC : (fx≢gx : ∀ {T : Set l} (x : T ⟿ D) -> f ∘ x ≢ g ∘ x) -> D ⟿ C)
    {- f(x) ≢ g(x) for every point x in the disk D.
       Draw an arrow with its tail at f(x) and its head at g(x),
       This arrow will 'point to' some point r(x). -}
    (accgj≡Id : (fx≢gx : ∀ {T : Set l} (x : T ⟿ D) -> f ∘ x ≢ g ∘ x) -> arrowCrossC fx≢gx ∘ (g ∘ j) ≡ Id)
    {- When g(x) was already a point on the boundary, r(x) is g(x), so that r is a retraction for (g ∘ j) -}
    (cacc : (fx≢gx : ∀ {T : Set l} (x : T ⟿ D) -> f ∘ x ≢ g ∘ x) -> Continuous (arrowCrossC fx≢gx))
    {- r is continuous under continuous f and continuous g -}
    where
      ex1lemma : (fx≢gx : ∀ {T : Set l} (x : T ⟿ D) -> f ∘ x ≢ g ∘ x)
               -> ∃ (λ (r : D ⟿ C) -> r ∘ j ≡ Id ∧ Continuous r)
      ex1lemma fx≢gx rewrite gj≡j = arrowCrossC fx≢gx , accgj≡Id fx≢gx , cacc fx≢gx

      ex1goal : (retractionTheorem : ∀ (r : D ⟿ C) -> r ∘ j ≡ Id -> ¬ Continuous r)
              -> ¬ (∀ {T : Set l} (x : T ⟿ D) -> f ∘ x ≢ g ∘ x)
      ex1goal retractionTheorem fx≢gx with ex1lemma fx≢gx
      ...                                | r , rjId , cr = retractionTheorem r rjId cr

  module Exercise2
    {A : Set l}
    {X : Set l}
    (T : Set l)
    (s : A ⟿ X)
    (r : X ⟿ A)
    (rsId : r ∘ s ≡ Id)
    where
      ex2core : (g : A ⟿ A)
              -> ∃ (λ (x : T ⟿ X) -> ((s ∘ g) ∘ r) ∘ x ≡ x)
              -> ∃ (λ (a : T ⟿ A) -> g ∘ a ≡ a)
      ex2core g (x , sgrx≡x) = (r ∘ x) , ga≡a
        where
          s1 : g ∘ (r ∘ x) ≡ (r ∘ s) ∘ (g ∘ (r ∘ x))
          s1 rewrite rsId rewrite LeftIdLaw (g ∘ (r ∘ x)) = refl
          s2 : (r ∘ s) ∘ (g ∘ (r ∘ x)) ≡ r ∘ (((s ∘ g) ∘ r) ∘ x)
          s2 rewrite  AssocLaw {_} {_} {_} {_} {r} {s} {g ∘ (r ∘ x)}
             rewrite  AssocLaw {_} {_} {_} {_} {s ∘ g} {r} {x}
             rewrite  AssocLaw {_} {_} {_} {_} {s} {g} {r ∘ x}
             = refl
          ga≡a : g ∘ (r ∘ x) ≡ r ∘ x
          ga≡a rewrite s1 rewrite s2 rewrite sgrx≡x = refl

      ex2goal : ( ∀ (f : X ⟿ X) -> ∃ (λ (x : T ⟿ X) -> f ∘ x ≡ x) )
              ->  ∀ (g : A ⟿ A) -> ∃ (λ (a : T ⟿ A) -> g ∘ a ≡ a)
      ex2goal FPPX g =  ex2core g (FPPX ((s ∘ g) ∘ r))

  module Exercise3
    (T : Set l)
    (antipodalE : E ⟿ E)
    (continuousE : Continuous antipodalE)
    (NoFixpointE : (a : T ⟿ E) -> antipodalE ∘ a ≢ a)
    (antipodalC : C ⟿ C)
    (continuousC : Continuous antipodalC)
    (NoFixpointC : (a : T ⟿ C) -> antipodalC ∘ a ≢ a)
    (antipodalS : S ⟿ S)
    (continuousS : Continuous antipodalS)
    (NoFixpointS : (a : T ⟿ S) -> antipodalS ∘ a ≢ a)
    where
      NotContinuousDistR : ∀ {a b c} {f : b ⟿ c} {g : a ⟿ b} -> ¬ Continuous (f ∘ g) -> Continuous f -> ¬ Continuous g
      NotContinuousDistR ncfg cf cg = ncfg (ContinuousCompose cf cg)

      ex2contra :  {A : Set l}
                -> {X : Set l}
                -> (s : A ⟿ X)
                -> (r : X ⟿ A)
                -> (rsId : r ∘ s ≡ Id)
                -> (g : A ⟿ A)
                -> (NoFixpoint : ∀ (a : T ⟿ A) -> g ∘ a ≢ a)
                -> ∀ (x : T ⟿ X) -> ((s ∘ g) ∘ r) ∘ x ≢ x
      ex2contra {A} {X} s r rsId g NoFixpoint x sgrx≡x
                with Exercise2.ex2core T s r rsId g (x , sgrx≡x)
      ...          | a , ga≡a  =  NoFixpoint a ga≡a

      RetractionTheorem :  {A X : Set l}
                           (g : A ⟿ A) (cg : Continuous g)
                           (NoFixpoint : ∀ (a : T ⟿ A) -> g ∘ a ≢ a)
                           (FixpointTheorem : ∀ (f : X ⟿ X) -> Continuous f -> ∃ (λ (x : T ⟿ X) -> f ∘ x ≡ x))
                           (s : A ⟿ X) (cs : Continuous s)
                           (r : X ⟿ A)
                           (rsId : r ∘ s ≡ Id)
                        -> ¬ Continuous r
      RetractionTheorem {_} {X} g cg NoFixpoint FixpointTheorem s cs r rsId =
        NotContinuousDistR (contraFT (ex2contra s r rsId g NoFixpoint)) (ContinuousCompose cs cg)
        where
          contraFT : (∀ (x : T ⟿ X) -> ((s ∘ g) ∘ r) ∘ x ≢ x) -> ¬ Continuous ((s ∘ g) ∘ r)
          contraFT nofix csgr with FixpointTheorem ((s ∘ g) ∘ r) csgr
          ...                    | x , sgrx≡x = nofix x sgrx≡x

      RetractionTheoremI : (FixpointTheoremI : ∀ (f : I ⟿ I) -> Continuous f -> ∃ (λ (x : T ⟿ I) -> f ∘ x ≡ x)) →
                           (j : E ⟿ I) (cj : Continuous j) (r : I ⟿ E) (rsId : r ∘ j ≡ Id) -> ¬ Continuous r
      RetractionTheoremI = RetractionTheorem antipodalE continuousE NoFixpointE

      RetractionTheoremD : (FixpointTheoremD : ∀ (f : D ⟿ D) -> Continuous f -> ∃ (λ (x : T ⟿ D) -> f ∘ x ≡ x)) →
                           (j : C ⟿ D) (cj : Continuous j) (r : D ⟿ C) (rsId : r ∘ j ≡ Id) -> ¬ Continuous r
      RetractionTheoremD = RetractionTheorem antipodalC continuousC NoFixpointC

      RetractionTheoremB : (FixpointTheoremB : ∀ (f : B ⟿ B) -> Continuous f -> ∃ (λ (x : T ⟿ B) -> f ∘ x ≡ x)) →
                           (j : S ⟿ B) (cj : Continuous j) (r : B ⟿ S) (rsId : r ∘ j ≡ Id) -> ¬ Continuous r
      RetractionTheoremB = RetractionTheorem antipodalS continuousS NoFixpointS

Session10.v

Module Exercises.

Polymorphic Parameters morphism : Type -> Type -> Type.
Notation " a '⇀' b " := (morphism a b) (at level 80).

Parameters
  (Id : forall {a}, (a ⇀ a))
  (compose : forall {a b c}, (b ⇀ c) -> (a ⇀ b) -> (a ⇀ c)).
Notation " f '∘' g" := (compose f g) (at level 10).

Parameters
  (LeftIdLaw : forall {a b} (f : a ⇀ b), Id ∘ f = f)
  (RightIdLaw : forall {a b} (f : a ⇀ b), f ∘ Id = f)
  (AssocLaw : forall {a b c d} {f : c ⇀ d} {g : b ⇀ c} {h : a ⇀ b}, (f ∘ g) ∘ h = f ∘ (g ∘ h)).
Parameters
  (Continuous : forall {a b} (f : a ⇀ b), Prop)
  (ContinuousCompose : forall {a b c} {f : b ⇀ c} {g : a ⇀ b}, Continuous f -> Continuous g -> Continuous (f ∘ g)).

Polymorphic Parameters
  (E : Type)
  (I : Type)
  (C : Type)
  (D : Type)
  (S : Type)
  (B : Type).

Parameters
  (FixpointTheoremI : forall {T} (f : I ⇀ I), Continuous f -> exists x : T ⇀ I, f ∘ x = x)
  (FixpointTheoremD : forall {T} (f : D ⇀ D), Continuous f -> exists x : T ⇀ D, f ∘ x = x)
  (FixpointTheoremB : forall {T} (f : B ⇀ B), Continuous f -> exists x : T ⇀ B, f ∘ x = x).

(* Set Printing Universes. *)
(* About compose. *)

Module Exercise1.
  Parameters
    (f : D ⇀ D)
    (cf : Continuous f)
    (g : D ⇀ D)
    (cg : Continuous g).
  Parameters
    (j : C ⇀ D)
    (gj_eq_j : g ∘ j = j).
  Parameters arrowCrossC : (forall {T : Type} (x : T ⇀ D), f ∘ x <> g ∘ x) -> D ⇀ C.
  Parameters accj_eq_id : forall (fx_neq_gx : (forall [T : Type] (x : T ⇀ D), f ∘ x <> g ∘ x)), arrowCrossC fx_neq_gx ∘ (g ∘ j) = Id.
  Parameters cacc : forall (fx_neq_gx : (forall [T : Type] (x : T ⇀ D), f ∘ x <> g ∘ x)), Continuous (arrowCrossC fx_neq_gx).

  Lemma ex1lemma :
    forall (fx_neq_gx : (forall [T : Type] (x : T ⇀ D), f ∘ x <> g ∘ x)),
    exists r : D ⇀ C, r ∘ j = Id /\ Continuous r.
  Proof.
    intro.
    exists (arrowCrossC fx_neq_gx).
    split.
    - rewrite <- (accj_eq_id fx_neq_gx).
      rewrite -> gj_eq_j.
      reflexivity.
    - exact (cacc fx_neq_gx).
  Defined.

  Theorem ex1goal :
    (forall r : D ⇀ C, r ∘ j = Id -> ~ Continuous r) ->
    ~ (forall [T : Type] (x : T ⇀ D), f ∘ x <> g ∘ x).
  Proof.
    unfold not.
    intros rt fx_neq_gx.
    destruct (ex1lemma fx_neq_gx) as [r [rjId cr]].
    exact (rt r rjId cr).
  Defined.
End Exercise1.

Theorem ex2core :
  forall {A X}
     (T : Type)
     (s : A ⇀ X)
     (r : X ⇀ A)
     (rsId : r ∘ s = Id)
     (g : A ⇀ A), (exists x : T ⇀ X, ((s ∘ g) ∘ r) ∘ x = x) -> exists a : T ⇀ A, g ∘ a = a.
Proof.
  intros A X T s r rsId g [x sgrx_eq_x].
  exists (r ∘ x).

  assert (s1 : g ∘ (r ∘ x) = (r ∘ s) ∘ (g ∘ (r ∘ x))).
  rewrite rsId. rewrite LeftIdLaw. reflexivity.

  assert (s2 : (r ∘ s) ∘ (g ∘ (r ∘ x)) = r ∘ (((s ∘ g) ∘ r) ∘ x)).
  rewrite AssocLaw. rewrite AssocLaw. rewrite AssocLaw. reflexivity.

  rewrite s1. rewrite s2. rewrite sgrx_eq_x. reflexivity.
Defined.

Module Type Exercise2.
  Polymorphic Parameters
    (A : Type)
    (X : Type).
  Arguments A : default implicits.
  Arguments X : default implicits.

  Parameters (T : Type).
  Parameters
    (s : A ⇀ X)
    (r : X ⇀ A)
    (rsId : r ∘ s = Id).

  (*
  Theorem ex2core : forall g : A ⇀ A, (exists x : T ⇀ X, ((s ∘ g) ∘ r) ∘ x = x) -> exists a : T ⇀ A, g ∘ a = a.
  Proof.
    intros g [x sgrx_eq_x].
    exists (r ∘ x).

    assert (s1 : g ∘ (r ∘ x) = (r ∘ s) ∘ (g ∘ (r ∘ x))).
    rewrite rsId. rewrite LeftIdLaw. reflexivity.

    assert (s2 : (r ∘ s) ∘ (g ∘ (r ∘ x)) = r ∘ (((s ∘ g) ∘ r) ∘ x)).
    rewrite AssocLaw. rewrite AssocLaw. rewrite AssocLaw. reflexivity.

    rewrite s1. rewrite s2. rewrite sgrx_eq_x. reflexivity.
  Defined.
   *)

  Theorem ex2goal : (forall f : X ⇀ X, exists x : T ⇀ X, f ∘ x = x) ->
                    (forall g : A ⇀ A, exists a : T ⇀ A, g ∘ a = a).
  Proof.
    intros FPPX g.
    exact (ex2core T s r rsId g (FPPX ((s ∘ g) ∘ r))).
  Defined.
End Exercise2.

Module Exercise3.

  Polymorphic Parameters T : Type.
  Parameters
    (antipodalE : E ⇀ E)
    (continuousE : Continuous antipodalE)
    (NoFixpointE : forall a : T ⇀ E, antipodalE ∘ a <> a).
  Parameters
    (antipodalC : C ⇀ C)
    (continuousC : Continuous antipodalC)
    (NoFixpointC : forall a : T ⇀ C, antipodalC ∘ a <> a).
  Parameters
    (antipodalS : S ⇀ S)
    (continuousS : Continuous antipodalS)
    (NoFixpointS : forall a : T ⇀ S, antipodalS ∘ a <> a).

  Lemma NotContinuousDistR : forall {a b c} {f : b ⇀ c} {g : a ⇀ b}, ~ Continuous (f ∘ g) -> Continuous f -> ~ Continuous g.
  Proof.
    intros a b c f g ncfg cf cg.
    exact (ncfg (ContinuousCompose cf cg)).
  Defined.

  Lemma ex2contra :
    forall {A X : Type}
       (s : A ⇀ X) (r : X ⇀ A) (rsId : r ∘ s = Id)
       (g : A ⇀ A) (NoFixpoint : forall a : T ⇀ A, g ∘ a <> a) (x : T ⇀ X),
      ((s ∘ g) ∘ r) ∘ x <> x.
  Proof.
    intros. intro sgrx_eq_x.

    assert (ex_sgrx_eq_x : exists x : T ⇀ X, ((s ∘ g) ∘ r) ∘ x = x).
    exists x. exact sgrx_eq_x.

    destruct (ex2core T s r rsId g ex_sgrx_eq_x) as [a ga_eq_a].
    exact (NoFixpoint a ga_eq_a).
  Defined.

  Theorem RetractionTheorem :
    forall {A X : Type}
       (g : A ⇀ A) (cg : Continuous g)
       (NoFixpoint : forall (a : T ⇀ A), g ∘ a <> a)
       (FixpointTheorem : forall f : X ⇀ X, Continuous f -> exists x : T ⇀ X, f ∘ x = x)
       (s : A ⇀ X) (cs : Continuous s)
       (r : X ⇀ A)
       (rsId : r ∘ s = Id),
      ~ Continuous r.
  Proof.
    intros.

    assert (contraFT : (forall x : T ⇀ X, ((s ∘ g) ∘ r) ∘ x <> x) -> ~ Continuous ((s ∘ g) ∘ r)).
    intros nofix csgr. destruct (FixpointTheorem ((s ∘ g) ∘ r) csgr) as [x sgrx_eq_x]. exact (nofix x sgrx_eq_x).

    exact (NotContinuousDistR (contraFT (ex2contra s r rsId g NoFixpoint)) (ContinuousCompose cs cg)).
  Defined.

  Theorem RetractionTheoremI :
    forall (j : E ⇀ I) (cj : Continuous j) (r : I ⇀ E) (rsId : r ∘ j = Id), ~ Continuous r.
  Proof. exact (RetractionTheorem antipodalE continuousE NoFixpointE FixpointTheoremI). Defined.


  Theorem RetractionTheoremD :
    forall (j : C ⇀ D) (cj : Continuous j) (r : D ⇀ C) (rsId : r ∘ j = Id), ~ Continuous r.
  Proof. exact (RetractionTheorem antipodalC continuousC NoFixpointC FixpointTheoremD). Defined.

  Theorem RetractionTheoremB :
    forall (j : S ⇀ B) (cj : Continuous j) (r : B ⇀ S) (rsId : r ∘ j = Id), ~ Continuous r.
  Proof. exact (RetractionTheorem antipodalS continuousS NoFixpointS FixpointTheoremB). Defined.
End Exercise3.

End Exercises.