# Pastebin yxATxzvR
{-# OPTIONS --cubical --rewriting #-}

module Cubical.Examples.CircleHomog where

open import Cubical.FromStdLib
open import Cubical.PathPrelude
open import Cubical.Rewrite
open import Cubical.GradLemma

open import Cubical.Examples.Circle


Set* = Σ Set (λ X → X)

-- from cubicaltt prelude.ctt
constSquare : ∀ {i} {A : Set i} {x : A} (p : x ≡ x)
  → PathP (λ i → Path (p i) (p i)) p p
constSquare {A = A} {x = x} p i j =
  primComp (λ _ → A) (i ∨ ~ i ∨ j ∨ ~ j)
    (λ { k (i = i0) → p (j ∨ ~ k)
       ; k (i = i1) → p (j ∧ k)
       ; k (j = i0) → p (i ∨ ~ k)
       ; k (j = i1) → p (i ∧ k)})
    x

loops : (x : S¹) → x ≡ x
loops = S¹-elim loop (constSquare loop)

loopsLoop : Path {A = S¹ ≃ S¹} idEquiv idEquiv
loopsLoop i =
  ( (λ x → loops x i)
  , lemPropF propIsEquiv (λ i x → loops x i) {snd idEquiv} {snd idEquiv} i
  )

homog : (x : S¹) → Path {A = Set*} (S¹ , base) (S¹ , x)
homog = S¹-elim refl
  (λ i j →
     ( Glue S¹ (i ∨ j ∨ ~ i ∨ ~ j)
         (λ _ → S¹)
         (λ { (i = i0) → idEquiv
            ; (i = i1) → idEquiv
            ; (j = i0) → loopsLoop i
            ; (j = i1) → idEquiv
            })
     , glue
         (λ { (i = i0) → base
            ; (i = i1) → base
            ; (j = i0) → base
            ; (j = i1) → loop i
            })
         (loop i)
     ))

corollary : (x : S¹) → (base ≡ base) ≃ (x ≡ x)
corollary x = transp (λ i → (base ≡ base) ≃ (snd (homog x i) ≡ snd (homog x i))) idEquiv