{-# OPTIONS --no-positivity-check --no-termination-check #-}

module Hyper.Base where

open import Prelude hiding (_∘_)

infixr -1 _↬_
record _↬_ (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
  inductive; constructor hyp
  field ι : (B ↬ A) → B
open _↬_ public

hyp-ind : {x y : A ↬ B}
        → (∀ z → ι z x ≡ ι z y → ι x z ≡ ι y z)
        → x ≡ y
ι (hyp-ind {x = x} {y} prf i) z =
  prf z (cong (ι z) (hyp-ind prf)) i

cong-ι : {p q : A ↬ B} → (∀ h → ι p h ≡ ι q h) → p ≡ q
ι (cong-ι p i) h = p h i

private module CompTyImpl where
  _∘_ : (B ↬ C) → (A ↬ B) → (A ↬ C)

  ι (f ∘ g) k = ι f (g ∘ k)

private module CompImpl where
  _∘_  :  (B ↬ C) → (A ↬ B) →  (A ↬ C)
  ι (f ∘ g) k = ι f (g ∘ k)

open import Prelude using (_∘_)

infixr 8 _#_
_#_ : (B ↬ C) → (A ↬ B) → A ↬ C
ι (f # g) k = ι f (g # k)

infixr 5 _◃_
_◃_ : (A → B) → (A ↬ B) →  (A ↬ B)
ι (f ◃ h) k = f (ι k h)

[_] : (A → B) → A ↬ B
[ f ] = f ◃ [ f ]

𝕀 : A ↬ A
ι 𝕀 x = ι x 𝕀

Prod : Type a → Type b → Type _
Prod A B = (A → B) ↬ B

Cons : Type a → Type b → Type _
Cons A B = B ↬ (A → B)

cons : A → Prod A B → Prod A B
ι (cons x k₁) k₂ = (ι k₂ k₁) x

prod : (A → B → B) → Cons A B → Cons A B
(ι (prod f k₁) k₂) x = f x (ι k₂ k₁)

cata : (((C → A) → B) → C) → A ↬ B → C
cata ϕ h = ϕ λ k → ι h (hyp (k ∘ cata ϕ))

ana : (C → (C → A) → B) → C → A ↬ B
ι (ana ψ r) x = ψ r λ y → ι x (ana ψ y)

𝕂 : A → B ↬ A
ι (𝕂 x) _ = x


private module _ (_⊕_ : A → A → A) where
  _∥_ : A ↬ A → A ↬ A → A ↬ A

  ι (f ∥ g) h = (ι f (g ∥ h)) ⊕ (ι g (f ∥ h))



-- module _ {A : Type a} {B : Type b} {C : Type c} where
--   ℂ : (A ↬ B ↬ C) → B ↬ A ↬ C
--   ℂ ι f x · y = ι f (hyp λ r → {!𝕂 · y!} · r) · hyp λ r → x · 𝕂 # r

  -- ℂ : (A ↬ B ↬ C) → B ↬ A ↬ C
  -- ℂ = cata alg
  --   where
  --   alg : ((B ↬ A ↬ C → A) → B ↬ C) → B ↬ A ↬ C
  --   alg k · x · y = k (λ bac → y · (bac · x)) · hyp λ r → x · {!!}

-- 𝔹 : (B ↬ C) ↬ (A ↬ B) ↬ A ↬ C
-- 𝔹 · ι f g · x = let h = f # {!g!} in {!!}

-- 𝕊 : (A ↬ B ↬ C) ↬ (A ↬ B) ↬ A ↬ C
-- 𝕊 · ι f g · x =
--   let h₁ = ι f 𝕊
--       h₂ = g · {!!}
--   in {!!}

mutual
  rmap : (A → B) → B ↬ C → A ↬ C
  ι (rmap f h) k = ι h (lmap f k)

  lmap : (B → C) → A ↬ B → A ↬ C
  ι (lmap f h) k = f (ι h (rmap f k))

dimap : ∀ {a′ b′} {A′ : Type a′} {B′ : Type b′} → (B → B′) → (A′ → A) → A ↬ B → A′ ↬ B′
ι (dimap f g h) r = f (ι h (hyp λ r′ → g (ι r (dimap f g r′))))

run : A ↬ A → A
run h = ι h (hyp run)

fold : (A → B → C) → C → List A → B ↬ C
ι (fold f b [])        k = b
ι (fold f b (x ∷ xs))  k = f x (ι k (fold f b xs))