Braids1.agda

Braids1.agda

{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Prelude
open import Cubical.HITs.S1

module Braids1 where

{-

 Conjecture:

 Assuming internalized parametricity, the type

   (X : Set) (η : S¹ → X) → (h : X → X) × (h ∘ η ≡ η)

 is contractible. Its unique inhabitant is λ X η → ⟨ λx → x, refl ⟩.

 The reason I think this is true is that the only "sensible" way I can
 think of to map a set to itself preserving a specified circle is the
 identity.

 A reason I worry it's not true is that maybe "the only parametric map
 X → X is the identity" and "the circle is preserved" are together
 "redundant information", and homotopical data about precisely how h ∘
 η ≡ η is achieved "leaks into" the above type making it not
 contractible. Compare this to how in the circle, we have

    (a) (s : S¹) × s ≡ base            (contractible)
    (b) (s : S¹) × s ≡ base × s ≡ base (not contractible)

 So a situation like (b) is what I'm suggesting with the phrase "redundant information".

 The reason I want it to be true is it would validate the
 trivial n=1 case of a more general conjecture that braid groups arise
 as exactly the parametric self-maps of certain pushouts of a type
 with a specified circle. In those terms, the above conjecture says
 "there exists exactly one braid on one strand".

 An equivalent statement of the conjecture, merely pulling apart the Σ-types, is:

 If we had parametric

   h : (X : Set) (η : X → X) (x : X) → X
   p : (X : Set) (η : X → X) (s : S¹) → h (η s) ≡ η s

 Then we could prove

  h! : h X η ≡ id
  p! : p X η s ≡ refl (in a suitable fashion over the path h!)

 My intended meaning of "h is parametric" is h* below and "p is parametric" is p* below.

-}

postulate
 h : {X : Set} (η : S¹ → X) (x : X) → X
 p : {X : Set} (η : S¹ → X) (s : S¹) → h η (η s) ≡ η s
 h* : {X₁ X₂ : Set} (R : X₁ → X₂ → Set)
       (η₁ : S¹ → X₁) (η₂ : S¹ → X₂) (η* : (s : S¹) → R (η₁ s) (η₂ s))
       (x₁ : X₁) (x₂ : X₂) → R x₁ x₂ → R (h η₁ x₁) (h η₂ x₂)

-- Transport a relation across some equalities on its indices, used to
-- assert parametricity for a type yielding an equality (i.e. the type
-- of p)
reltrans : (X₁ X₂ : Set) (R : X₁ → X₂ → Set) (x₁ y₁ : X₁) (x₂ y₂ : X₂)
           → R x₁ x₂ → x₁ ≡ y₁ → x₂ ≡ y₂ → R y₁ y₂
reltrans X₁ X₂ R x₁ y₁ x₂ y₂ r p q = transport (λ i → R (p i) (q i)) r

postulate
 p* :
    (X₁ X₂ : Set) (R : X₁ → X₂ → Set)
    (η₁ : S¹ → X₁) (η₂ : S¹ → X₂) (η* : (s : S¹) → R (η₁ s) (η₂ s))
    (s : S¹)
    → reltrans X₁ X₂ R (h η₁ (η₁ s)) (η₁ s) (h η₂ (η₂ s)) (η₂ s)
       (h* R η₁ η₂ η* (η₁ s) (η₂ s) (η* s)) (p η₁ s) (p η₂ s) ≡ η* s

-- Diagram for p*: https://q.uiver.app/#q=WzAsNCxbMCwwLCJoXFwgKFxcZXRhXzFcXCBzKSJdLFsxLDAsImhcXCAoXFxldGFfMlxcIHMpIl0sWzAsMSwiXFxldGFfMVxcIHMiXSxbMSwxLCJcXGV0YV8yXFwgcyJdLFswLDEsImhfXFxzdGFyXFwgKFxcZXRhX1xcc3RhclxcIHMpIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoic3F1aWdnbHkifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsyLDMsIlxcZXRhX1xcc3RhclxcIHMiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJzcXVpZ2dseSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzAsMiwicFxcIFxcZXRhXzFcXCBzIiwyLHsibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMSwzLCJwXFwgXFxldGFfMlxcIHMiLDAseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dXQ==

-- Goal:
h! : {X : Set} (η : S¹ → X) (x : X) → h η x ≡ x
h! η x = {!!}

p! : {X : Set} (η : S¹ → X) (s : S¹) → Square (h! η (η s)) refl (p η s) refl
p! {X} η s = {!!}

-- Diagram for p!: https://q.uiver.app/#q=WzAsNCxbMCwwLCJoXFwgKFxcZXRhXFwgcykiXSxbMSwwLCJcXGV0YVxcIHMiXSxbMCwxLCJcXGV0YVxcIHMiXSxbMSwxLCJcXGV0YVxcIHMiXSxbMCwxLCJwXFwgXFxldGFcXCBzIiwwLHsibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMiwzLCJcXG1hdGhzZntyZWZsfSIsMix7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzAsMiwiaF8hXFwgKFxcZXRhXFwgcykiLDIseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFsxLDMsIlxcbWF0aHNme3JlZmx9IiwwLHsibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XV0=