------------------------------------------------------------------------
-- The "circle"
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

-- Partly following the HoTT book.

open import Equality

module Circle
  {reflexive} (eq :  {a p}  Equality-with-J a p reflexive) where

open import Logical-equivalence using (module _⇔_)
open import Prelude

open Derived-definitions-and-properties eq hiding (elim)
open import Equality.Groupoid eq as EG
open import Function-universe eq hiding (_∘_)
open import Groupoid eq
open import H-level eq
open import H-level.Truncation eq hiding (rec)
open import Nat eq
open import Univalence-axiom eq

-- Circle p is an axiomatisation of the circle, eliminating into
-- Set p.

Circle : (p : Level)  Set (lsuc p)
Circle p =
   λ ( : Set) 
   λ (base : ) 
   λ (loop : base  base) 
    (P :   Set p)
    (b : P base)
    ( : subst P loop b  b) 
     λ (f :  x  P x) 
     λ (f-base : f base  b) 
      subst  b  subst P loop b  b)
            f-base
            (dependent-cong f loop) 
      

module Circle {p} (C : Circle p) where

  -- The circle.

   : Set
   = proj₁ C

  base : 
  base = proj₁ (proj₂ C)

  loop : base  base
  loop = proj₁ (proj₂ (proj₂ C))

  -- Dependent eliminator.

  elim :
    (P :   Set p)
    (b : P base)
    ( : subst P loop b  b) 
     λ (f :  x  P x) 
     λ (f-base : f base  b) 
      subst  b  subst P loop b  b)
            f-base
            (dependent-cong f loop) 
      
  elim = proj₂ (proj₂ (proj₂ C))

  -- Non-dependent eliminator.

  rec :
    (P : Set p)
    (b : P)
    ( : b  b) 
     λ (f :   P) 
     λ (f-base : f base  b) 
      subst  b  b  b) f-base (cong f loop)  
  rec P b  =
    let f , f-base , f-loop =
          elim (const P) b (subst (const P) loop b  ≡⟨ subst-const loop 
                            b                       ≡⟨  ⟩∎
                            b                       )

        lemma₁ =
          trans (subst-const loop)
                (subst  b  b  b) (refl _) (cong f loop))  ≡⟨ cong (trans _) $ subst-refl _ _ 

          trans (subst-const loop) (cong f loop)              ≡⟨ sym $ subst-refl _ _ ⟩∎

          subst  b  subst (const P) loop b  b)
                (refl _)
                (trans (subst-const loop) (cong f loop))      

        lemma₂ =
          trans (subst-const loop)
                (subst  b  b  b) f-base (cong f loop))  ≡⟨ elim¹  eq  trans (subst-const loop)
                                                                                   (subst  b  b  b) eq (cong f loop))
                                                                               
                                                                             subst  b  subst (const P) loop b  b)
                                                                                   eq
                                                                                   (trans (subst-const loop) (cong f loop)))
                                                                      lemma₁
                                                                      f-base  
          subst  b  subst (const P) loop b  b)
                f-base
                (trans (subst-const loop) (cong f loop))    ≡⟨ cong (subst _ _) $ sym $ dependent-cong-subst-const-cong _ _ 

          subst  b  subst (const P) loop b  b)
                f-base
                (dependent-cong f loop)                     ≡⟨ f-loop ⟩∎

          trans (subst-const loop)                         

    in
    f , f-base , (
      subst  b  b  b) f-base (cong f loop)  ≡⟨ Groupoid.right-cancellative (EG.groupoid _) lemma₂ ⟩∎
                                               )

-- For circles that eliminate into universes with positive universe
-- levels loop is not equal to refl base (assuming univalence).

loop≢refl :
   {p} 
  Univalence p 
  (C : Circle (lsuc p)) 
  let open Circle C in
  loop  refl base
loop≢refl {p} univ C loop≡refl = ¬-Set-set-↑ univ Set-set
  where
  open Circle C

  refl≡ : (A : Set p) (A≡A : A  A)  refl A  A≡A
  refl≡ A A≡A =
    let
      (f , f-base , f-loop) = rec (Set p) A A≡A

      lemma =
        trans (refl (f base)) f-base  ≡⟨ trans-reflˡ _ 
        f-base                        ≡⟨ sym $ trans-reflʳ _ ⟩∎
        trans f-base (refl A)         
    in
    refl A                                           ≡⟨ sym $ ≡⇒→ (sym [subst≡]≡[trans≡trans]) lemma 
    subst  b  b  b) f-base (refl (f base))       ≡⟨ cong (subst  b  b  b) f-base) $ sym $ cong-refl _ 
    subst  b  b  b) f-base (cong f (refl base))  ≡⟨ cong (subst  b  b  b) f-base  cong f) $ sym loop≡refl 
    subst  b  b  b) f-base (cong f loop)         ≡⟨ f-loop ⟩∎
    A≡A                                              

  Set-set : Is-set (Set p)
  Set-set A B = _⇔_.from propositional⇔irrelevant
    (elim¹  p   q  p  q)
           (refl≡ A))

-- Thus circles that eliminate into universes with positive universe
-- levels are not sets (assuming univalence).

¬-S¹-set :
   {p} 
  Univalence p 
  (C : Circle (lsuc p)) 
  let open Circle C in
  ¬ Is-set 
¬-S¹-set univ C =
  Is-set                      ↝⟨  h  h _ _) 
  Is-proposition (base  base)  ↝⟨  h  _⇔_.to propositional⇔irrelevant h _ _) 
  loop  refl base              ↝⟨ loop≢refl univ C ⟩□
                               
  where
  open Circle C

-- Every element of a circle that eliminates into a universe with a
-- positive universe level is /merely/ equal to the base point
-- (assuming extensionality).
--
-- This lemma (more or less) was mentioned by Mike Shulman in a blog
-- post (http://homotopytypetheory.org/2013/07/24/cohomology/).

all-points-on-the-circle-are-merely-equal :
   {} 
  Extensionality (lsuc )  
  (C : Circle (lsuc )) 
  let open Circle C in
  (x : )   x  base  1 
all-points-on-the-circle-are-merely-equal ext C =
  proj₁ $
  elim _  refl base 
       (_⇔_.to propositional⇔irrelevant
          (truncation-has-correct-h-level 1 ext)
          _ _)
  where
  open Circle C

-- However, it is not the case that every point on a circle that
-- eliminates into a universe with a positive universe level is
-- /equal/ to the base point (assuming univalence).

¬-all-points-on-the-circle-are-equal :
   {} 
  Univalence  
  (C : Circle (lsuc )) 
  let open Circle C in
  ¬ ((x : )  x  base)
¬-all-points-on-the-circle-are-equal univ C =
  ((x : )  x  base)  ↝⟨  hyp x y  x     ≡⟨ hyp x 
                                         base  ≡⟨ sym (hyp y) ⟩∎
                                         y     ) 
  Proof-irrelevant     ↝⟨ _⇔_.from propositional⇔irrelevant 
  Is-proposition       ↝⟨ mono₁ 1 
  Is-set               ↝⟨ ¬-S¹-set univ C ⟩□
                        
  where
  open Circle C

-- H-level.Closure.proj₁-closure cannot be generalised by replacing
-- the assumption ∀ a → B a with ∀ a → ∥ B a ∥ 1 (# 0) (assuming
-- extensionality, univalence and the presence of a certain kind of
-- circle).
--
-- This observation is due to Andrea Vezzosi.

¬-generalised-proj₁-closure :
  Extensionality (# 1) (# 0) 
  Univalence (# 0) 
  Circle (# 1) 
  ¬ ({A : Set} {B : A  Set} 
     (∀ a   B a  1 (# 0)) 
      n  H-level n (Σ A B)  H-level n A)
¬-generalised-proj₁-closure ext univ C generalised-proj₁-closure =
                                 $⟨ singleton-contractible _ 
  Contractible (Σ  (_≡ base))  ↝⟨ generalised-proj₁-closure
                                      (all-points-on-the-circle-are-merely-equal ext C)
                                      0 
  Contractible                 ↝⟨ mono (zero≤ 2) 
  Is-set                       ↝⟨ ¬-S¹-set univ C ⟩□
                                
  where
  open Circle C