open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality

postulate
  cheat : {A : Set} → A

record DCat : Set₁ where -- Direct category
  field
    Obj : ℕ → Set
  ObjN : Set
  ObjN = Σ ℕ Obj
  ob : {n : ℕ} → Obj n → ObjN 
  ob {n} I = (n , I)
  field
    Hom : ObjN → ObjN → Set
    -- Hom (m , I) (n , J) => m < n
    comp : {I J K : ObjN} → Hom J K → Hom I J → Hom I K

open DCat

shift : (C : DCat)(X : Obj C 0 → Set) → DCat
Obj (shift C X) n = Σ (Obj C (suc n))
                      λ J → {I : Obj C 0} →
                            Hom C (ob C I) (ob C J) → X I 
Hom (shift C X) (_ , (J , x)) (_ , (K , y)) =
           Σ (Hom C (ob C J) (ob C K))
             λ f → {I : Obj C 0} →
                    (g : Hom C (ob C I) (ob C J))
                    → x g ≡ y (comp C f g)
comp (shift D C) = cheat -- needs assoc

record ReedyFib (C : DCat) : Set₁ where
  coinductive
  field
    hd : Obj C 0 → Set
    tl : ReedyFib (shift C hd)

open ReedyFib

record PSh (C : DCat) : Set₁ where
    constructor _,_
    field
      Fobj : ObjN C → Set
      Fhom : {I J : ObjN C} → Hom C I J → Fobj J → Fobj I

open PSh

rfib→fobj : {C : DCat} → ReedyFib C
            → {n : ℕ} → Obj C n → Set

rfib→fobj {C} Xs {zero} I = hd Xs I
rfib→fobj {C} Xs {suc n} J =
          Σ ({I : Obj C 0} (f : Hom C (ob C I) (ob C J)) → hd Xs I)
            (λ x → rfib→fobj (tl Xs) (J , x))

rfib→fhom : {C : DCat}(Xs : ReedyFib C)
            → {n : ℕ}(I : Obj C n)
            → {m : ℕ}(J : Obj C m) -- n < m
            → Hom C (ob C I) (ob C J)
            → rfib→fobj Xs J → rfib→fobj Xs I
rfib→fhom {C} Xs {n} I {zero} J f x = cheat -- impossible
rfib→fhom {C} Xs {zero} I {suc m} J f (x , _)
  = x {I} f 
rfib→fhom {C} Xs {suc n} I {suc m} J f (x , xs)
  = (λ {K} g → x (comp C f g))
    , rfib→fhom (tl Xs) (I , λ {K} g → x (comp C f g))
                         (J , x) (f , cheat) xs -- assoc ?

rfib→psh : {C : DCat} → ReedyFib C → PSh C
Fobj (rfib→psh {C} Xs) (n , I) = rfib→fobj Xs {n} I
Fhom (rfib→psh {C} Xs) {n , J} {m , I} = rfib→fhom {C} Xs {n} J {m} I

Fzero : {C : DCat} → PSh C → Obj C 0 → Set
Fzero F I = Fobj F (0 , I)

shiftPSh : {C : DCat}(F : PSh C) → PSh (shift C (Fzero F))
Fobj (shiftPSh {C} (Fobj , Fhom)) (n , I , x)
  = Σ (Fobj (suc n , I))
      (λ z → {J : Obj C 0}(f : Hom C (ob C J) (ob C I))
                 → x f ≡ Fhom f z) 
Fhom (shiftPSh {C} (Fobj , Fhom)) { n , (I , x) } {m , ( J , y)} (f , p) (z , g)
  = (Fhom f z) , (λ {K} h → trans (p h)
                          (trans (g (comp C f h)) cheat)) -- functor law


{-
shiftPSh : {C : DCat}(X : Obj C 0 → Set) → PSh C → PSh (shift C X)
Fobj (shiftPSh {C} X (Fobj , Fhom)) (n , I , x)
  = Σ (Fobj (suc n , I)) (λ z → {!(J : Obj C 0)(f : Hom (ob J) I) → !}) -- Fobj (suc n , I)
Fhom (shiftPSh X (Fobj , Fhom)) { n , (I , x) } {m , ( J , y)} (f , p) z
  = {!!}
  -- Fhom f z
-}



--{-# TERMINATING #-}
psh→rfib : {C : DCat} → PSh C → ReedyFib C
hd (psh→rfib {C} F) = Fzero F
tl (psh→rfib {C} F) = psh→rfib (shiftPSh F)

{- simple example -}
record Πℕ (A : ℕ → Set) : Set where
  coinductive
  field
    hd : A 0
    tl : Πℕ (λ n → A (suc n))

open Πℕ

mkΠℕ : {A : ℕ → Set} → ((n : ℕ) → A n) → Πℕ A
hd (mkΠℕ {A} f) = f 0
tl (mkΠℕ {A} f) = mkΠℕ (λ n → f (suc n)) 

{- negative example -}

record Πℕ2 (A : ℕ → Set) : Set₁ where
  coinductive
  field
    hd : A 0 → Set
    tl : Πℕ2 (λ n → A (suc n))

open Πℕ2

mkΠℕ2 : {A : ℕ → Set} → ((n : ℕ) → A n → Set) → Πℕ2 A
hd (mkΠℕ2 {A} f) = f 0
tl (mkΠℕ2 {A} f) = mkΠℕ2 (λ n → f (suc n)) 

-- Id

open import delta-i
open import Data.Unit

Δi-icat : DCat
Obj Δi-icat = λ _ → ⊤
Hom Δi-icat (n , _) (m , _) = Δi n m
comp Δi-icat f g = f ∘ g

constPSh : (A : Set) → PSh Δi-icat
Fobj (constPSh A) _ = A
Fhom (constPSh A) f x = x

constFib : (A : Set) → ReedyFib Δi-icat
constFib A = psh→rfib (constPSh A)

eqPSh : (A : Set) → PSh Δi-icat
eqPSh A = rfib→psh (constFib A)

module _ (A : Set) where

  e : PSh Δi-icat
  e = eqPSh A

  x = Fobj e (1 , _)
  -- Σ ({I : ⊤} → Δi 0 1 → A) (λ x₁ → A)
  -- Σ ({I : ⊤} → Δi 0 1 → A)
  --   (λ x₁ → Σ A (λ z₁ → (J : ⊤) (f : Δi 0 1) → x₁ f ≡ z₁))