open import 1Lab.Prelude

open import Data.Bool

module wip.test6 where

module _ {P : Type} (isp : is-prop P) where
  -- data ΣP : Type where
  --   N S : ΣP
  --   merid : P → N ≡ S

  -- Σ-elim : ∀ {ℓ} {B : ΣP → Type ℓ} (n : B N) (s : B S)
  --        → (∀ x → PathP (λ i → B (merid x i)) n s) → ∀ x → B x
  -- Σ-elim n s p N = n
  -- Σ-elim n s p S = s
  -- Σ-elim n s p (merid x i) = p x i

  -- Σ-rec : ∀ {ℓ} {B : Type ℓ} (n s : B) → (P → n ≡ s) → ΣP → B
  -- Σ-rec = Σ-elim

  -- ⊤* : Prop lzero
  -- ⊤* = ⊤ , λ _ _ _ → tt

  -- P* : Prop lzero
  -- P* = P , isp

  -- p→p≡t : P → ⊤* ≡ P*
  -- p→p≡t x = n-ua (prop-ext (λ _ _ _ → tt) isp (λ _ → x) λ _ → tt)

  -- Code : ΣP → ΣP → Prop lzero
  -- Code = Σ-rec (Σ-rec ⊤* P* p→p≡t) (Σ-rec P* ⊤* (sym ∘ p→p≡t))
  --   λ p → funext (Σ-elim (p→p≡t p) (sym (p→p≡t p))
  --     (λ x → is-set→squarep (λ _ _ → n-Type-is-hlevel 1) _ _ _ _))

  -- decode : ∀ y → ∣ Code N y ∣ → N ≡ y
  -- decode = Σ-elim (λ _ → refl) merid λ x → funext-dep λ {y z} p → transport (sym Square≡··) (
  --   refl ·· refl ·· merid _ ≡⟨ ··≡twice∙ _ _ _ ⟩
  --   refl ∙ refl ∙ merid _   ≡⟨ ∙-assoc _ _ _ ⟩
  --   (refl ∙ refl) ∙ merid _ ≡⟨ ap₂ _∙_ (∙-id-l refl) refl ·· ∙-id-l (merid _) ·· ap merid (isp x z) ⟩
  --   merid _                 ∎
  --   )

  -- encode : ∀ y → N ≡ y → ∣ Code N y ∣
  -- encode y = J (λ y _ → ∣ Code N y ∣) tt

  -- encode-decode : ∀ {y} p → decode y (encode y p) ≡ p
  -- encode-decode = J (λ y p → decode y (encode y p) ≡ p) refl

  -- decode-encode : ∀ {y} p → encode y (decode y p) ≡ p
  -- decode-encode {y} = Σ-elim {B = λ y → ∀ p → encode y (decode y p) ≡ p} (λ _ → refl) (λ _ → isp _ _)
  --   (λ x → funext-dep λ p → is-set→squarep (λ i j → is-prop→is-set (p→p≡t x i .is-tr))
  --     _ _ _ _) y

  -- result : P ≃ (N ≡ S)
  -- result = Iso→Equiv
  --   (decode S , iso (encode S) encode-decode (decode-encode {y = S}))

  -- data RP2 : Type where
  --   base : RP2
  --   one : base ≡ base
  --   negate : sym one ≡ one
  --   add-square : Square (sym one) one refl refl

  -- add : one ∙ one ≡ refl
  -- add = ap fst
  --   (··-unique one one refl (one ∙ one , ∙-filler' one one) (refl , add-square))

  -- RP2-elim : ∀ {ℓ} {B : RP2 → Type ℓ}
  --            (b : B base) (o : PathP (λ i → B (one i)) b b)
  --          → SquareP (λ i j → B (negate i j)) refl (λ i → o (~ i)) o refl
  --          → SquareP (λ i j → B (add-square i j)) (λ i → o (~ i)) o refl refl
  --          → ∀ x → B x
  -- RP2-elim b l m a base = b
  -- RP2-elim b l m a (one i) = l i
  -- RP2-elim b l m a (negate i j) = m i j
  -- RP2-elim b l m a (add-square i j) = a i j

  -- rot : Bool ≡ Bool
  -- rot = ua (_ , not-is-equiv)

  -- negate-rot : sym rot ≡ rot
  -- negate-rot =
  --   sym (ua (_ , not-is-equiv))         ≡⟨ sym-ua _ ⟩
  --   ua (equiv→inverse not-is-equiv , _) ≡⟨ ap ua (Σ-prop-path is-equiv-is-prop refl) ⟩
  --   ua (_ , not-is-equiv)               ∎

  -- Code : RP2 → Type
  -- Code = RP2-elim Bool
  --   (ua (_ , not-is-equiv))
  --   negate-rot
  --   (transport (sym Square≡··) (
  --        ··≡twice∙ rot rot _
  --     ·· ap (rot ∙_) (∙-id-r _)
  --     ·· sym ua∙
  --     ·· ap ua (Σ-prop-path is-equiv-is-prop (funext not-involutive))
  --     ·· ua-id-equiv))

  -- encode : ∀ {b} → base ≡ b → Code b
  -- encode = J (λ y _ → Code y) true

  -- dec : Bool → base ≡ base
  -- dec false = one
  -- dec true = refl

  -- flip : ∀ c → dec c ≡ dec (not c)
  -- flip false = {!   !}
  -- flip true = {!   !}

  -- decode : ∀ b → Code b → base ≡ b
  -- decode base = dec
  -- decode (one i) c =
  --   hcomp (λ { j (i = i0) → flip c (~ j) ; j (i = i1) → flip c (~ j) })
  --     (p1 (unglue (i ∨ ~ i) c) i)
  --   where
  --     p1 : ∀ x → Square refl (dec x) (dec (not x)) one
  --     p1 false = transport (sym Square≡··) (··≡twice∙ refl one one ·· ∙-id-l _ ·· add)
  --     p1 true = transport (sym Square≡··) (··≡twice∙ refl refl one ·· ∙-id-l _ ·· ∙-id-l _)

  -- decode (negate i i₁) c = {!   !}
  -- decode (add-square i i₁) c = {!   !}
  -- -- decode = RP2-elim dec
  --   -- (funext-dep (λ p → transport (sym Square≡··) (··≡twice∙ refl _ one ∙ ∙-id-l _ ∙ p1 _ _ (ua-pathp→path _ p))))
  --   -- {!  !} {!   !}
  --   -- where

  BAut : Type → Type₁
  BAut T = Σ[ B ∈ Type ] ∥ T ≃ B ∥

  base : ∀ {T} → BAut T
  base {T} = T , inc (id , id-equiv)

  connected : ∀ {T} b → ∥ b ≡ base {T} ∥
  connected (b , x) =
    ∥-∥-elim {P = λ x → ∥ (b , x) ≡ base ∥} (λ _ → squash) (λ e → inc (p _ _)) x
    where
      p : ∀ b e → (b , inc e) ≡ base
      p _ = EquivJ (λ B e → (B , inc e) ≡ base) refl

  Code : ∀ {T} (b : BAut T) → Type
  Code {T} b = (b .fst ≃ T)

  encode : ∀ {T} (b : BAut T) → b ≡ base → Code b
  encode {T} x = J (λ b p → b .fst ≃ T) (id , id-equiv) ∘ sym

  decode : ∀ {T} (b : BAut T) → Code b → b ≡ base
  decode (b , eqv) rot = Σ-pathp (ua rot) (is-prop→pathp (λ _ → squash) _ _)

  isom : ∀ {T} (b : BAut T) → is-iso (encode b)
  isom {T} b = iso (decode b) (linv {b = b}) (rinv ∘ sym) where
    rinv : ∀ {b : BAut T} (p : base ≡ b) → decode b (encode b (sym p)) ≡ sym p
    rinv = J (λ b p → decode b (encode b (sym p)) ≡ sym p)
      (Σ-prop-square (λ _ → squash)
        (transport (sym Square≡··)
          (  ··≡twice∙ refl _ _
          ·· ∙-id-l _ ·· ∙-id-r _
          ·· ap (ap fst ∘ decode base) (transport-refl _) ·· ua-id-equiv)))

    linv : ∀ {b : BAut T} (p : b .fst ≃ T) → encode b (decode b p) ≡ p
    linv p = Σ-prop-path is-equiv-is-prop q where
      q : subst (λ e → e → T) (sym (ua p)) id ≡ p .fst
      q =
        subst (λ e → e → T) (sym (ua p)) id                          ≡⟨ refl ⟩
        (λ x → transport (λ i → T) (transport (sym (sym (ua p))) x)) ≡⟨ funext (λ x → transport-refl _) ⟩
        (λ x → transport (ua p) x)                                   ≡⟨ funext (uaβ p) ⟩
        p .fst                                                       ∎

  result : ∀ {T} → (base {T} ≡ base) ≃ (T ≃ T)
  result = _ , is-iso→is-equiv (isom _)

  RP² : Type₁
  RP² = BAut Bool