open import 1Lab.Prelude

open import Data.List.Membership
open import Data.Fin.Product
open import Data.List.Sigma
open import Data.List.Base
open import Data.Fin.Base

module Data.List.Pi where

private variable
  ℓ ℓ' : Level
  A B C : Type ℓ
  P Q : A → Type ℓ

Pi : (xs : List A) → (A → Type ℓ') → Type _
Pi {ℓ' = ℓ'} xs P = Πᶠ {length xs} {λ _ → ℓ'} (λ i → P (xs ! i))

pi : (xs : List A) (ys : ∀ a → List (P a)) → List (Pi xs P)
pi [] ys = tt ∷ []
pi (x ∷ xs) ys = sigma (ys x) (λ _ → pi xs ys)

Pi' : (xs : List A) → (A → Type ℓ') → Type _
Pi' xs P = ∀ a → a ∈ₗ xs → P a

module _ {A : Type ℓ} (P : A → Type ℓ') where
  to-pi' : ∀ {xs} → Pi xs P → Pi' xs P
  to-pi' (x , xs) a (here p) = substᵢ P (symᵢ p) x
  to-pi' (x , xs) a (there h) = to-pi' xs a h

  from-pi' : ∀ {xs} → Pi' xs P → Pi xs P
  from-pi' {[]} x = tt
  from-pi' {x₁ ∷ xs} x = x _ (here reflᵢ) , from-pi' {xs} (λ _ h → x _ (there h))

  to-from-pi' : ∀ {xs} (p : Pi xs P) → from-pi' (to-pi' p) ≡ p
  to-from-pi' {[]} p = refl
  to-from-pi' {x ∷ xs} p = refl ,ₚ to-from-pi' {xs} (p .snd)

  from-to-pi' : ∀ {xs} (p : Pi' xs P) → to-pi' (from-pi' p) ≡ p
  from-to-pi' p i a (here reflᵢ) = p a (here reflᵢ)
  from-to-pi' p i a (there x) = from-to-pi' (λ a h → p a (there h)) i a x

  pi-member'
    : {A : Type ℓ} {P : A → Type ℓ'} (xs : List A) (ys : ∀ a → List (P a)) {e : Pi xs P}
    → (∀ h → indexₚ e h ∈ₗ ys (xs ! h)) → e ∈ₗ pi xs ys
  pi-member' [] ys {tt} p = here reflᵢ
  pi-member' (x ∷ xs) ys {p , ps} q = sigma-member {xs = ys x} {ys = λ _ → pi xs ys} (q fzero) (pi-member' xs ys (q ∘ fsuc))

  member-pi'
    : {A : Type ℓ} {P : A → Type ℓ'} (xs : List A) (ys : ∀ a → List (P a)) {e : Pi xs P}
    → (α : e ∈ₗ pi xs ys) → fibre (pi-member' xs ys) α
  member-pi' [] ys (here p) = (λ h → absurd (Fin-absurd h)) , ap here (is-set→is-setᵢ (hlevel ) _ _ reflᵢ p)
  member-pi' (x ∷ xs) ys elt =
    let
      α = member-sigmaₗ (ys x) (λ _ → pi xs ys) elt
      β = member-sigmaᵣ (ys x) (λ _ → pi xs ys) elt

      (f , coh) = member-pi' xs ys β

      g = Fin-cases α λ h → member-pi' xs ys β .fst h
    in g , ap (sigma-member α) coh ∙ member-sigma-view (ys x) (λ _ → pi xs ys) elt .snd