open import 1Lab.Prelude

open import Agda.Builtin.Maybe

open import Data.Set.Coequaliser

module wip.test7 where

-- data T/ (A : Type) (R : A → A → Type) : Type where
--   inc : A → T/ A R
--   quot : ∀ {x y} → R x y → inc x ≡ inc y

-- elim₂
--   : ∀ {ℓ} {A B : Type} {R : A → A → Type} {S : B → B → Type}
--   → (P : T/ A R → T/ B S → Type ℓ)
--   → (pt : ∀ x y → P (inc x) (inc y))
--   → (p : ∀ x y z (r : R x y) → PathP (λ i → P (quot r i) (inc z)) (pt x z) (pt y z))
--   → (q : ∀ x y z (r : S x y) → PathP (λ i → P (inc z) (quot r i)) (pt z x) (pt z y))
--   → ( ∀ w x y z (r : R w x) (s : S y z)
--     → SquareP (λ i j → P (quot r i) (quot s j))
--         (p w x y r) (q y z w s) (q y z x s) (p w x z r))
--   → ∀ x y → P x y
-- elim₂ P pt p q sq (inc x) (inc y) = pt x y
-- elim₂ P pt p q sq (inc x) (quot y i) = q _ _ x y i
-- elim₂ P pt p q sq (quot x i) (inc y) = p _ _ _ x i
-- elim₂ P pt p q sq (quot x i) (quot y j) = sq _ _ _ _ x y i j

just≠nothing : ∀ {A : Type} {x : A} → just x ≡ nothing → ⊥
just≠nothing p = subst (λ { (just x) → ⊤ ; nothing → ⊥ }) p tt

just-injective : ∀ {A : Type} {x y : A} → just x ≡ just y → x ≡ y
just-injective {y = y} = ap λ { (just x) → x
                              ; nothing → y }

absurd-path : ∀ {ℓ} {A : Type ℓ} {y : A} {x : ⊥} → absurd x ≡ y
absurd-path {x = ()}

inj : ∀ {A B : Type} → Maybe A ≡ Maybe B → A ≡ B
inj {A = A} {B} p = ua (Iso→Equiv (a→b , iso b→a b→a→b a→b→a)) where
  ma≃mb : Maybe A ≃ Maybe B
  ma≃mb = path→equiv p

  mb≃ma : Maybe B ≃ Maybe A
  mb≃ma = ma≃mb e⁻¹

  a→b : A → B
  a→b x with inspect (ma≃mb .fst (just x))
  ... | just y , _ = y
  ... | nothing , p with inspect (ma≃mb .fst nothing)
  ... | just y , _ = y
  ... | nothing , q = absurd (just≠nothing (ap fst (is-contr→is-prop (ma≃mb .snd .is-eqv _) (_ , p) (_ , q))))

  b→a : B → A
  b→a x with inspect (mb≃ma .fst (just x))
  ... | just x , _ = x
  ... | nothing , p with inspect (mb≃ma .fst nothing)
  ... | just y , _ = y
  ... | nothing , q = absurd (just≠nothing (ap fst (is-contr→is-prop (mb≃ma .snd .is-eqv _) (_ , p) (_ , q))))

  a→b→a : ∀ a → b→a (a→b a) ≡ a
  a→b→a a with inspect (ma≃mb .fst (just a))
  a→b→a a | just x , p′ with inspect (mb≃ma .fst (just x))
  a→b→a a | just x , p′ | just y , q′ = just-injective (
    just y                                   ≡⟨ sym q′ ⟩
    transport (sym p) (just x)               ≡⟨ ap (transport (sym p)) (sym p′) ⟩
    transport (sym p) (transport p (just a)) ≡⟨ transport⁻transport p _ ⟩
    just a                                   ∎)
  a→b→a a | just x , p′ | nothing , q′ = absurd contra where
    r = ap fst (is-contr→is-prop (ma≃mb .snd .is-eqv _) (_ , p′)
               (_ , transport⁻transport (sym p) _))
    contra = just≠nothing (r ∙ q′)
  a→b→a a | nothing , p′ with inspect (ma≃mb .fst nothing)
  a→b→a a | nothing , p′ | just x , q′ with inspect (mb≃ma .fst (just x))
  a→b→a a | nothing , p′ | just x , q′ | just y , r′ = absurd (just≠nothing (sym r′ ∙ ap (transport (sym p)) (sym q′) ∙ transport⁻transport p _))
  a→b→a a | nothing , p′ | just x , q′ | nothing , r′ with inspect (mb≃ma .fst nothing)
  a→b→a a | nothing , p′ | just x , q′ | nothing , r′ | just z , s = just-injective (sym s ∙ ap (transport (sym p)) (sym p′) ∙ transport⁻transport p _)
  a→b→a a | nothing , p′ | just x , q′ | nothing , r′ | nothing , s = absurd-path
  a→b→a a | nothing , p′ | nothing , q′ = absurd (just≠nothing (ap fst (is-contr→is-prop (ma≃mb .snd .is-eqv _) (_ , p′) (_ , q′))))

  b→a→b : ∀ b → a→b (b→a b) ≡ b
  b→a→b b with inspect (mb≃ma .fst (just b))
  b→a→b b | just x , p′ with inspect (ma≃mb .fst (just x))
  b→a→b b | just x , p′ | just x₁ , q′ = just-injective (sym q′ ∙ ap (transport p) (sym p′) ∙ transport⁻transport (sym p) _)
  b→a→b b | just x , p′ | nothing , q′ = absurd contra where
    r = ap fst (is-contr→is-prop (mb≃ma .snd .is-eqv _) (_ , p′)
               (_ , transport⁻transport p _))
    contra = just≠nothing (r ∙ q′)
  b→a→b b | nothing , p′ with inspect (mb≃ma .fst nothing)
  b→a→b b | nothing , p′ | just x , q′ with inspect (ma≃mb .fst (just x))
  b→a→b b | nothing , p′ | just x , q′ | just y , r′  = absurd (just≠nothing (sym r′ ∙ ap (transport p) (sym q′) ∙ transport⁻transport (sym p) _))
  b→a→b b | nothing , p′ | just x , q′ | nothing , r′ with inspect (ma≃mb .fst nothing)
  b→a→b a | nothing , p′ | just x , q′ | nothing , r′ | just z , s = just-injective (sym s ∙ ap (transport p) (sym p′) ∙ transport⁻transport (sym p) _)
  b→a→b a | nothing , p′ | just x , q′ | nothing , r′ | nothing , s = absurd-path
  b→a→b b | nothing , p′ | nothing , q′ = absurd (just≠nothing (ap fst (is-contr→is-prop (mb≃ma .snd .is-eqv _) (_ , p′) (_ , q′))))

open import 1Lab.HIT.S1

test : Square refl refl loop loop
test i j = loop (i ∧ j)

test3 : Square (sym loop) refl loop refl
test3 i j = loop (~ i ∨ j)

∙-filler''
  : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z)
  → Square refl (sym p) q (p ∙ q)
∙-filler'' {x = x} {y} {z} p q i j =
  hcomp (λ { k (i = i0) → p (~ j)
           ; k (i = i1) → q (k ∧ j)
           ; k (j = i0) → y
           })
    (p (i ∨ ~ j))

{-
composite-square looks like:

    p
  x - y
p |   | q
  y - z
    q
-}

composite-square
  : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z)
  → Square p p q q
composite-square {x = x} p q i j =
  hcomp (λ { k (i = i0) → p j
           ; k (i = i1) → ∙-filler p q j k
           ; k (j = i0) → p (k ∧ i)
           ; k (j = i1) → ∙-filler'' p q k i
           })
    (p (~ i ∧ j))

asdf : (x : S¹) → x ≡ x
asdf base = loop
asdf (loop i) j = composite-square loop loop i j