{-# OPTIONS --rewriting #-}

open import Agda.Primitive using (Level;lsuc;_⊔_;lzero)
open import Lib
open import Interval
open import Proposition
open import Cofibs

-- the lsuc lzero is avoidable, because we could define codes for cofibs in universe 0

module Kan where 

  ⇐ : ∀ {l} {I : Set} (A : I → Set l) {r r' : I} → A r' → (p : r == r') → A r
  ⇐ A x id = x

  ⇒ : ∀ {l} {I : Set} {A : I → Set l} {r r' : I} → A r → (p : r == r') → A r'
  ⇒ {A = A} x p = transport A p x

  k : ∀ {l1 l2} {A : Set l1} {B : Set l2} → A → B → A
  k x y = x

  hasCom : ∀ {l} → (I → Set l) → Set (lsuc lzero ⊔ l)
  hasCom A = (r r' : I) (α : Set) {{_ : Cofib α}} 
           → (t : (z : I) → α → A z) 
           → (b : A r [ α ↦ t r ]) 
           → A r' [ α ↦ t r' , (r == r') ↦ ⇒ (fst b) ]

  relCom : ∀ {l1 l2} {Γ : Set l1} (A : Γ → Set l2)
         -> Set (lsuc lzero ⊔ l1 ⊔ l2)
  relCom {Γ = Γ} A = (p : I → Γ) → hasCom (A o p)

  comPre : ∀ {l1 l2 l3} {Δ : Set l1} {Γ : Set l2} (θ : Δ → Γ) (A : Γ → Set l3) → relCom A → relCom (A o θ)
  comPre θ _ comA p = comA (θ o p)

  comPre-o : {l1 l2 l3 l4 : Level} {Γ1 : Set l1} {Γ2 : Set l2} {Γ3 : Set l3} {A : Γ3 → Set l4}
           → (g : Γ2 → Γ3) (f : Γ1 → Γ2) (comA : relCom A)
           → comPre f (A o g) (comPre g A comA) == comPre (g o f) A comA
  comPre-o g f comA = id

  Fib : ∀ (l : Level) {l1 : Level} (Γ : Set l1) → Set (l1 ⊔ lsuc l)
  Fib l Γ = Σ \ (A : Γ → Set l) → relCom A

  reindex-Fib : {l : Level} {l1 l2 : Level} {Γ : Set l1} {Δ : Set l2} (θ : Γ → Δ) → Fib l Δ → Fib l Γ
  reindex-Fib θ (A , comA) = (A o θ) , comPre θ A comA

  -- ----------------------------------------------------------------------
  -- specialized notions and interderivabilities

  hasHCom : {l : Level} → Set l → Set (lsuc lzero ⊔ l)
  hasHCom A = (r r' : I) (α : Set) {{_ : Cofib α}} 
            → (t : (z : I) → α → A) 
            → (b : A [ α ↦ t r ]) 
            → A [ α ↦ t r' , (r == r') ↦ k (fst b) ]

  hasCoe : {l : Level} → (I → Set l) → Set l
  hasCoe A = (r r' : I) 
           → (b : A r) 
           → A r' [ (r == r') ↦ ⇒ b ]

  hasWCoe : {l : Level} → (I → Set l) → Set l
  hasWCoe A = (r r' : I) →  
    Σ \ (f : A r → A r') → 
        ((e : r == r') → (b : A r) → Σ \ (p : (x : I) → A r') → (p `0 == f b) × (p `1 == ⇒ b e))

  relCoe : ∀ {l1 l2} {Γ : Set l1} (A : Γ → Set l2) -> Set (l1 ⊔ l2)
  relCoe {_} {_} {Γ} A = (p : I → Γ) → hasCoe (A o p)

  coePre : ∀ {l1 l2 l3} {Δ : Set l1} {Γ : Set l2} (θ : Δ → Γ) (A : Γ → Set l3) → relCoe A → relCoe (A o θ)
  coePre θ _ r p = r (θ o p)

  relWCoe : ∀ {l1 l2} {Γ : Set l1} (A : Γ → Set l2) -> Set (l1 ⊔ l2)
  relWCoe {_} {_} {Γ} A = (p : I → Γ) → hasWCoe (A o p)

  wcoePre : ∀ {l1 l2 l3} {Δ : Set l1} {Γ : Set l2} (θ : Δ → Γ) (A : Γ → Set l3) → relWCoe A → relWCoe (A o θ)
  wcoePre θ _ r p = r (θ o p)

  decompose-hasCom : ∀ {l2} (A : I → Set l2) → 
                  ((x : I) → hasHCom (A x)) 
                  → hasCoe A 
                  → hasCom A
  decompose-hasCom A hcomA coeA r r' α t b = 
    (fst h) , 
    (\ u → fst (snd h) u ∘ snd (coeA r' r' (t r' u)) id) , 
           (\ { id → snd (snd h) id ∘ snd (coeA r r (fst b)) id}) where
    h = ((hcomA r') r r' 
                α (\ z u → fst (coeA z r' (t z u)))
                (fst (coeA r r' (fst b)) , (\ u → ap (\ h → fst (coeA r r' h)) (snd b u))))

  decompose-com : ∀ {l1 l2} {Γ : Set l1} (A : Γ → Set l2) → 
                  ((x : Γ) → hasHCom (A x)) 
                  → relCoe A 
                  → relCom A
  decompose-com A hcomA coeA p = decompose-hasCom (A o p) (\ x → hcomA (p x)) (coeA p) 

  relCom-hasHCom : ∀ {l1 l2} {Γ : Set l1} (A : Γ → Set l2) -> 
                   relCom A 
                 → (x : Γ) → hasHCom (A x)
  relCom-hasHCom A rA x r r' α t b = fst user , fst (snd user) , (\ r=r' → snd (snd user) r=r' ∘ ! (ap= (transport-constant r=r'))) where
    user = rA (\ _ → x) r r' α t b

  relCom-relCoe : ∀ {l1 l2} {Γ : Set l1} (A : Γ → Set l2) -> 
                   relCom A 
                 → relCoe A
  relCom-relCoe A comA p r r' b = fst com , (\ r=r' → snd (snd com) r=r') where
    com = comA p r r' ⊥ (\ x → abort) (b , \ x → abort x)

  hasCoe-from-hasWCoe : ∀ {l2} (A : I → Set l2) 
                 → ((x : I) → hasHCom (A x))
                 → hasWCoe A
                 → hasCoe A
  hasCoe-from-hasWCoe A hcomA wcoeA s s' b = fst fix , (\ s=s' → fst (snd fix) s=s' ∘ ! (snd (snd (snd (wcoeA s s') s=s' b)))) where
    fix = hcomA (s') `0 `1 (s == s') 
                             (\ x → \ s=s' → fst ((snd (wcoeA s s') s=s') b) x)
                             ((fst (wcoeA s s') b) , 
                              (\ s=s' →  fst (snd ((snd (wcoeA s s') s=s' b))) ))

  coe-from-wcoe : ∀ {l1 l2} {Γ : Set l1} (A : Γ → Set l2) 
                 → ((x : Γ) → hasHCom (A x))
                 → relWCoe A
                 → relCoe A
  coe-from-wcoe A hcomA wcoeA p = hasCoe-from-hasWCoe (A o p) (\ x → hcomA (p x)) (wcoeA p) 

  relCom-constant : ∀ {l1 l2} {Γ : Set l1} (A : Set l2) -> 
                  hasHCom A
                  → relCom {Γ = Γ} (\ _ → A )
  relCom-constant A hcomA p r r' α t b = 
    (fst (hcomA r r' α t b)) , ((\ pα → fst (snd (hcomA r r' α t b)) pα) , (\ {id → snd (snd (hcomA r r' α t b)) id}))

  hcomDec : ∀ {l : Level} {A : Set l} 
          → ((x y : A) → (x == y) ∨ ((x == y) → ⊥{l}))
          → hasHCom A
  hcomDec {A = A} dec r r' α t (b , p) = 
    b , (\ pα → p pα ∘ ! (constant (\ x → t x pα) r r')) , (λ { id → id }) where

    constant : ∀ (t : I → A) (r r' : I) → t r == t r'
    constant t r r' = 
      case (\ f → f r')
           (\ f → abort (f r id))
           (\ _ _ → uip)
           (iconnected (\ i → (t r == t i , (\ _ _ → uip))) (\ i →  dec (t r) (t i) ))

  -- useful macro
  hasCom-hasCom2 : ∀ {l} → (A : I → Set l) → hasCom A
               → (r r' : I) (α : Set) {{cα : Cofib α}} 
               → (t : (z : I) → α → A z)
               → (α' : Set)  {{cα' : Cofib α'}} 
               → (t' : (z : I) → α' → A z)
               → (compat : (x : I) (p : α) (q : α') → t x p == t' x q)
               → (b : A r [ (α ∨ α') ↦ case (t r) (t' r) (compat r) ]) 
               → A r' [ (α ∨ α') ↦ case (t r') (t' r') (compat r') , (r == r') ↦ ⇒ (fst b) ]
  hasCom-hasCom2 A hcomA r r' α {{cα}} t α' {{cα'}} t' compat b =
    hcomA r r' (α ∨ α') (\ x → case (t x) (t' x) (compat x)) b 


  Strictly-Preserves-HCom : {l1 l2 : Level} (A : Set l1) (C : A → Set l2)
                          → (hcomA : hasHCom A)
                          → (comC : relCom C)
                          → (f : (x : A) → C x) → Set _
  Strictly-Preserves-HCom A C hcomA comC f = 
    (r r' : I) (α : Set) {{_ : Cofib α}} 
           → (t : (z : I) → α → A) 
           → (b : A [ α ↦ t r ]) 
           → f (fst (hcomA r r' α t b)) == 
             (fst (comC (\ x → (fst (hcomA r x α t b))) r r' α 
                        (\z pα → transport C (fst (snd (hcomA r z α t b)) pα) (f (t z pα)))
                        (transport C (snd (snd (hcomA r r α t b)) id) (f (fst b)) , 
                         (\ pα → (! (apd f (snd (snd (hcomA r r α t b)) id))) 
                                   ∘ apd f (fst (snd (hcomA r r α t b)) pα)))))


  ContractibleFill : {l : Level} (A : Set l) → Set (ℓ₁ ⊔ l)
  ContractibleFill A = (α : Set) {{cα : Cofib α}} → (t : α → A) → A [ α ↦ t ]

  -- ----------------------------------------------------------------------
  -- equality lemmas

  relCom= : ∀ {l1 l2} {Γ : Set l1} (A : Γ → Set l2) 
           (r1 r2 : relCom A) → 
           ((p : I → Γ) (r r' : I) (α : Set) {{_ : Cofib α}} (t : _) (b : _) → fst (r1 p r r' α t b) == fst (r2 p r r' α t b))
           → r1 == r2
  relCom= A r1 r2 h = λ= \ p → λ= \ s → λ= \ s' → λ= \ α → λ=inf \ cα → λ= \ t → λ= \ b → pair= (h p s s' α {{ cα }} t b) (pair= (λ= \ _ → uip) ((λ= \ _ → uip)))   

  com=tb : ∀ {l1 l2} {Γ : Set l1} (A : Γ → Set l2) 
           (comA : relCom A) →
           (p : I → Γ)
           (r r' : I) (α : Set) {{_ : Cofib α}}
           (t t' : _) → t == t' → 
           (b : _) (b' : _) → fst b == fst b'
           → fst (comA p r r' α t b) == fst (comA p r r' α t' b')
  com=tb A comA p r r' α t t' id b b' id = ap (\ h → fst (comA p r r' α t (fst b' , h))) (λ= \ _ → uip) 

  hCom= : ∀ {l2} {A : Set l2}
           (hcom1 hcom2 : hasHCom A) → 
           ((r r' : I) (α : Set) {{_ : Cofib α}} (t : _) (b : _) → fst (hcom1 r r' α t b) == fst (hcom2 r r' α t b))
           → hcom1 == hcom2
  hCom= r1 r2 h = λ= \ s → λ= \ s' → λ= \ α → λ=inf \ cα → λ= \ t → λ= \ b → pair= (h s s' α {{ cα }} t b) (pair= (λ= \ _ → uip) ((λ= \ _ → uip)))   

  hCom=h : ∀ {l2} {A A' : Set l2}
           → (p : A == A')
           (hcom1 : hasHCom A) (hcom2 : hasHCom A') → 
           ((r r' : I) (α : Set) {{_ : Cofib α}} {t : _} {t' : _} → (t =h t') → {b : _} {b' : _} → b =h b' → fst (hcom1 r r' α t b) =h (fst (hcom2 r r' α t' b')))
           → hcom1 =h  hcom2
  hCom=h id hcom1 hcom2 h = hom-to-het (hCom= hcom1 hcom2 ((\ r r' α {{ cα }} t b → het-to-hom (h r r' α {{ cα }} {t} {t} hid {b} {b} hid))))