{-# OPTIONS --without-K #-}

open import lib.Basics
open import lib.types.Paths

module lib.types.Pi where

Π-level :  {i j} {A : Type i} {B : A  Type j} {n : ℕ₋₂}
(((x : A)  has-level n (B x))  has-level n (Π A B))
Π-level {n = ⟨-2⟩} p =
((λ x  fst (p x)) ,  f  λ=  x  snd (p x) (f x))))
Π-level {n = S n} p = λ f g
equiv-preserves-level λ=-equiv
(Π-level  x  p x (f x) (g x)))

module _ {i j} {A : Type i} {B : A  Type j} where
abstract
Π-is-prop : ((x : A)  is-prop (B x))  is-prop (Π A B)
Π-is-prop = Π-level

Π-is-set : ((x : A)  is-set (B x))  is-set (Π A B)
Π-is-set = Π-level

module _ {i j} {A : Type i} {B : Type j} where
abstract
→-level : {n : ℕ₋₂}  (has-level n B  has-level n (A  B))
→-level p = Π-level  _  p)

→-is-set : is-set B  is-set (A  B)
→-is-set = →-level

→-is-prop : is-prop B  is-prop (A  B)
→-is-prop = →-level

{- Equivalences in a Π-type -}
equiv-Π-l :  {i j k} {A : Type i} {B : Type j} (P : B  Type k) {h : A  B}
is-equiv h  Π A (P  h)  Π B P
equiv-Π-l {A = A} {B = B} P {h = h} e = equiv f g f-g g-f where
w : A  B
w = (h , e)

f : Π A (P  h)  Π B P
f u b = transport P (<–-inv-r w b) (u (<– w b))

g : Π B P  Π A (P  h)
g v a = v (–> w a)

f-g :  v  f (g v) == v
f-g v = λ= λ b  to-transp (apd v (<–-inv-r w b))

g-f :  u  g (f u) == u
g-f u = λ= λ a  to-transp \$ transport  p  u _ == _ [ P  p ])
(↓-ap-in P (–> w)
(apd u \$ <–-inv-l w a))

equiv-Π-r :  {i j k} {A : Type i} {B : A  Type j} {C : A  Type k}
(∀ x  B x  C x)  Π A B  Π A C
equiv-Π-r {A = A} {B = B} {C = C} k = equiv f g f-g g-f
where f : Π A B  Π A C
f c x = –> (k x) (c x)

g : Π A C  Π A B
g d x = <– (k x) (d x)

f-g :  d  f (g d) == d
f-g d = λ=  x   <–-inv-r (k x) (d x))

g-f :  c  g (f c) == c
g-f c = λ=  x  <–-inv-l (k x) (c x))

module _ {i₀ i₁ j₀ j₁} {A₀ : Type i₀} {A₁ : Type i₁}
{B₀ : A₀  Type j₀} {B₁ : A₁  Type j₁} where
equiv-Π : (u : A₀  A₁) (v :  a  B₀ (<– u a)  B₁ a)  Π A₀ B₀  Π A₁ B₁
equiv-Π u v = Π A₀ B₀           ≃⟨ equiv-Π-l _ (snd (u ⁻¹)) ⁻¹
Π A₁ (B₀  <– u)  ≃⟨ equiv-Π-r v
Π A₁ B₁           ≃∎

equiv-Π' : (u : A₀  A₁) (v :  a  B₀ a  B₁ (–> u a))  Π A₀ B₀  Π A₁ B₁
equiv-Π' u v = Π A₀ B₀           ≃⟨ equiv-Π-r v
Π A₀ (B₁  –> u)  ≃⟨ equiv-Π-l _ (snd u)
Π A₁ B₁           ≃∎

{- Dependent paths in a Π-type -}
module _ {i j k} {A : Type i} {B : A  Type j} {C : (a : A)  B a  Type k}
where

↓-Π-in : {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
({t : B x} {t' : B x'} (q : t == t' [ B  p ])
u t == u' t' [ uncurry C  pair= p q ])
(u == u' [  x  Π (B x) (C x))  p ])
↓-Π-in {p = idp} f = λ=  x  f (idp {a = x}))

↓-Π-out : {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
(u == u' [  x  Π (B x) (C x))  p ])
({t : B x} {t' : B x'} (q : t == t' [ B  p ])
u t == u' t' [ uncurry C  pair= p q ])
↓-Π-out {p = idp} q idp = app= q _

↓-Π-β : {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
(f : {t : B x} {t' : B x'} (q : t == t' [ B  p ])
u t == u' t' [ uncurry C  pair= p q ])
{t : B x} {t' : B x'} (q : t == t' [ B  p ])
↓-Π-out (↓-Π-in f) q == f q
↓-Π-β {p = idp} f idp = app=-β  x  f (idp {a = x})) _

{- Dependent paths in a Π-type where the codomain is not dependent on anything

Right now, this is defined in terms of the previous one. Maybe it’s a good idea,
maybe not.
-}
module _ {i j k} {A : Type i} {B : A  Type j} {C : Type k} {x x' : A}
{p : x == x'} {u : B x  C} {u' : B x'  C} where

↓-app→cst-in :
({t : B x} {t' : B x'} (q : t == t' [ B  p ])
u t == u' t')
(u == u' [  x  B x  C)  p ])
↓-app→cst-in f = ↓-Π-in  q  ↓-cst-in (f q))

↓-app→cst-out :
(u == u' [  x  B x  C)  p ])
({t : B x} {t' : B x'} (q : t == t' [ B  p ])
u t == u' t')
↓-app→cst-out r q = ↓-cst-out (↓-Π-out r q)

↓-app→cst-β :
(f : ({t : B x} {t' : B x'} (q : t == t' [ B  p ])
u t == u' t'))
{t : B x} {t' : B x'} (q : t == t' [ B  p ])
↓-app→cst-out (↓-app→cst-in f) q == f q
↓-app→cst-β f q =
↓-app→cst-out (↓-app→cst-in f) q
=⟨ idp
↓-cst-out (↓-Π-out (↓-Π-in  qq  ↓-cst-in (f qq))) q)
=⟨ ↓-Π-β  qq  ↓-cst-in (f qq)) q |in-ctx
↓-cst-out
↓-cst-out (↓-cst-in {p = pair= p q} (f q))
=⟨ ↓-cst-β (pair= p q) (f q)
f q

{- Dependent paths in an arrow type -}
module _ {i j k} {A : Type i} {B : A  Type j} {C : A  Type k}
{x x' : A} {p : x == x'} {u : B x  C x} {u' : B x'  C x'} where

↓-→-in :
({t : B x} {t' : B x'} (q : t == t' [ B  p ])
u t == u' t' [ C  p ])
(u == u' [  x  B x  C x)  p ])
↓-→-in f = ↓-Π-in  q  ↓-cst2-in p q (f q))

↓-→-out :
(u == u' [  x  B x  C x)  p ])
({t : B x} {t' : B x'} (q : t == t' [ B  p ])
u t == u' t' [ C  p ])
↓-→-out r q = ↓-cst2-out p q (↓-Π-out r q)

-- Dependent paths in a Π-type where the domain is constant
module _ {i j k} {A : Type i} {B : Type j} {C : A  B  Type k} where

↓-cst→app-in : {x x' : A} {p : x == x'}
{u : (b : B)  C x b} {u' : (b : B)  C x' b}
((b : B)  u b == u' b [  x  C x b)  p ])
(u == u' [  x  (b : B)  C x b)  p ])
↓-cst→app-in {p = idp} f = λ= f

↓-cst→app-out : {x x' : A} {p : x == x'}
{u : (b : B)  C x b} {u' : (b : B)  C x' b}
(u == u' [  x  (b : B)  C x b)  p ])
((b : B)  u b == u' b [  x  C x b)  p ])
↓-cst→app-out {p = idp} q = app= q

split-ap2 :  {i j k} {A : Type i} {B : A  Type j} {C : Type k} (f : Σ A B  C)
{x y : A} (p : x == y)
{u : B x} {v : B y} (q : u == v [ B  p ])
ap f (pair= p q) == ↓-app→cst-out (apd (curry f) p) q
split-ap2 f idp idp = idp

{-
Interaction of [apd] with function composition.
The basic idea is that [apd (g ∘ f) p == apd g (apd f p)] but the version here
is well-typed. Note that we assume a propositional equality [r] between
[apd f p] and [q].
-}
apd-∘ :  {i j k} {A : Type i} {B : A  Type j} {C : (a : A)  B a  Type k}
(g : {a : A}  Π (B a) (C a)) (f : Π A B) {x y : A} (p : x == y)
{q : f x == f y [ B  p ]} (r : apd f p == q)
apd (g  f) p == ↓-apd-out C r (apd↓ g q)
apd-∘ g f idp idp = idp

{- When [g] is nondependent, it’s much simpler -}
apd-∘' :  {i j k} {A : Type i} {B : A  Type j} {C : A  Type k}
(g : {a : A}  B a  C a) (f : Π A B) {x y : A} (p : x == y)
apd (g  f) p == ap↓ g (apd f p)
apd-∘' g f idp = idp

∘'-apd :  {i j k} {A : Type i} {B : A  Type j} {C : A  Type k}
(g : {a : A}  B a  C a) (f : Π A B) {x y : A} (p : x == y)
ap↓ g (apd f p) == apd (g  f) p
∘'-apd g f idp = idp

{- 2-dimensional coherence conditions -}

-- postulate
--  lhs :
--   ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} {f g : Π A B}
--   {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
--   (k : (u ◃ apd g p) == (apd f p ▹ v))
--   (h : {a : A} → B a → C a)
--   → ap h u ◃ apd (h ∘ g) p == ap↓ h (u ◃ apd g p)

--  rhs :
--   ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} {f g : Π A B}
--   {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
--   (k : (u ◃ apd g p) == (apd f p ▹ v))
--   (h : {a : A} → B a → C a)
--   → ap↓ h (apd f p ▹ v) == apd (h ∘ f) p ▹ ap h v

-- ap↓-↓-=-in :
--  ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} {f g : Π A B}
--  {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
--  (k : (u ◃ apd g p) == (apd f p ▹ v))
--  (h : {a : A} → B a → C a)
--  → ap↓ (λ {a} → ap (h {a = a})) (↓-=-in {p = p} {u = u} {v = v} k)
--  == ↓-=-in (lhs {f = f} {g = g} k h ∙ ap (ap↓ (λ {a} → h {a = a})) k
--                                     ∙ rhs {f = f} {g = g} k h)

{-
Commutation of [ap↓ (ap h)] and [↓-swap!]. This is "just" J, but it’s not as
easy as it seems.
-}

module Ap↓-swap! {i j k } {A : Type i} {B : Type j} {C : Type k}
{D : Type } (h : C  D) (f : A  C) (g : B  C)
{a a' : A} {p : a == a'} {b b' : B} {q : b == b'}
(r : f a == g b') (s : f a' == g b)
(t : r == s  ap g q  [  x  f x == g b')  p ])
where

lhs : ap h (ap f p ∙' s) == ap (h  f) p ∙' ap h s
lhs = ap-∙' h (ap f p) s  (ap  u  u ∙' ap h s) (∘-ap h f p))

rhs : ap h (s  ap g q) == ap h s  ap (h  g) q
rhs = ap-∙ h s (ap g q)  (ap  u  ap h s  u) (∘-ap h g q))

β : ap↓ (ap h) (↓-swap! f g r s t) ==
lhs  ↓-swap! (h  f) (h  g) (ap h r) (ap h s) (ap↓ (ap h) t  rhs)
β with a | a' | p | b | b' | q | r | s | t
β | a | .a | idp | b | .b | idp | r | s | t = coh r s t  where

T : {x x' : C} (r s : x == x') (t : r == s  idp)  Type _
T r s t =
ap (ap h) (∙'-unit-l s  ! (∙-unit-r s)  ! t) ==
(ap-∙' h idp s  idp)

(∙'-unit-l (ap h s)
! (∙-unit-r (ap h s))
!
(ap (ap h) t ∙'
(ap-∙ h s idp  idp)))

coh' : {x x' : C} {r s : x == x'} (t : r == s)  T r s (t  ! (∙-unit-r s))
coh' {r = idp} {s = .idp} idp = idp

coh : {x x' : C} (r s : x == x') (t : r == s  idp)  T r s t
coh r s t = transport  t  T r s t) (coh2 t (∙-unit-r s)) (coh' (t  ∙-unit-r s))  where

coh2 :  {i} {A : Type i} {x y z : A} (p : x == y) (q : y == z)  (p  q)  ! q == p
coh2 idp idp = idp

-- module _ {i j k} {A : Type i} {B B' : Type j} {C : Type k} (f : A → C) (g' : B' → B) (g : B → C) where

--   abc : {a a' : A} {p : a == a'} {c c' : B'} {q' : c == c'} {q : g' c == g' c'}
--     (r : f a == g (g' c')) (s : f a' == g (g' c))
--     (t : q == ap g' q')
--     (α : r == s ∙ ap g q [ (λ x → f x == g (g' c')) ↓ p ])
--     → {!(↓-swap! f g r s α ▹ ?) ∙'2ᵈ ?!} == ↓-swap! f (g ∘ g') {p = p} {q = q'} r s (α ▹ ap (λ u → s ∙ u) (ap (ap g) t ∙ ∘-ap g g' q'))
--   abc = {!!}

{- Functoriality of application and function extensionality -}

∙-app= :  {i j} {A : Type i} {B : A  Type j} {f g h : Π A B}
(α : f == g) (β : g == h)
α  β == λ=  x  app= α x  app= β x)
∙-app= idp β = λ=-η β

∙-λ= :  {i j} {A : Type i} {B : A  Type j} {f g h : Π A B}
(α : (x : A)  f x == g x) (β : (x : A)  g x == h x)
λ= α  λ= β == λ=  x  α x  β x)
∙-λ= α β = ∙-app= (λ= α) (λ= β)
ap λ= (λ=  x  ap  w  w  app= (λ= β) x) (app=-β α x)
ap  w  α x  w) (app=-β β x)))