open import 1Lab.Prelude

open import Data.List.Membership
open import Data.Id.Properties
open import Data.List.Base
open import Data.Fin.Base
open import Data.Nat.Base as Nat
open import Data.Sum.Base
open import Data.Irr

module Data.List.Sigma where

module _ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} where
  private
    fibre' : {x y : A} (xs : List (B x)) (p : y ≡ᵢ x) → B y → Type _
    fibre' xs p b = Σ[ ix ∈ Fin (length xs) ] substᵢ B (symᵢ p) (xs ! ix) ≡ᵢ b

    pair-mem : (x : A) (xs : List (B x)) (a : A) (b : B a) → Type _
    pair-mem x xs a b = Σ[ p ∈ a ≡ᵢ x ] (fibre' xs p b)

    pair-member
      : (x : A) (xs : List (B x)) (a : A) (b : B a)
      → (a , b) ∈ₗ map (x ,_) xs
      → pair-mem x xs a b
    pair-member x (y ∷ ys) a b (here p) = apᵢ fst p , fzero , substᵢ (λ e → transportᵢ e y ≡ᵢ b)
      (symᵢ (apᵢ-apᵢ B fst (symᵢ p)) ∙ᵢ (apᵢ (apᵢ B) (apᵢ-symᵢ fst p))) (apdᵢ snd (symᵢ p))
    pair-member x (y ∷ ys) a b (there p) with pair-member x ys a b p
    ... | (p , ix , q) = p , fsuc ix , q

    member-pair
      : (x : A) (xs : List (B x)) (a : A) (b : B a)
      → pair-mem x xs a b
      → (a , b) ∈ₗ map (x ,_) xs
    member-pair x (y ∷ ys) a b (p , i , q) with fin-view i
    ... | zero  = here (Σ-id p (symPᵢ⁻ p q))
    ... | suc i = there (member-pair x ys a b (p , i , q))

    member-pair-inv
      : (x : A) (xs : List (B x)) (a : A) (b : B a) (it : (a , b) ∈ₗ map (x ,_) xs)
      → member-pair x xs a b (pair-member x xs a b it) ≡ it
    member-pair-inv x (y ∷ ys) a b (here reflᵢ) = refl
    member-pair-inv x (y ∷ ys) a b (there it)   = ap there (member-pair-inv x ys a b it)

    rem₀
      : ∀ {x a} (ys : ∀ a → List (B a)) (b : B a) (p : a ≡ᵢ x) ix .{q} .{q'}
      → (Id-over B (symᵢ p) (ys x ! fin ix ⦃ forget q ⦄) b) ≃ (ys a ! fin ix ⦃ forget q' ⦄ ≡ᵢ b)
    rem₀ {x = x} {a} ys b p ix {q} {q'} = Jᵢ'
      (λ a x p → ∀ b .q .q' → Id-over B (symᵢ p) (ys x ! fin ix ⦃ forget q ⦄) b ≃ (ys a ! fin ix ⦃ forget q' ⦄ ≡ᵢ b))
      (λ b q q' → id , id-equiv)
      p b q q'

    rem₁ : ∀ {x a} (ys : ∀ a → List (B a)) (b : B _) (p : a ≡ᵢ x) → fibre' (ys x) p b → fibreᵢ (ys a !_) b
    rem₁ {x = x} {a} ys b p (fin ix ⦃ forget q ⦄ , r) = fin ix ⦃ q' ⦄ , Equiv.to (rem₀ ys b p ix) r where
      q' = forget (transport (λ i → suc ix Nat.≤ length (ys (Id≃path.to p (~ i)))) q)

    rem₂ : ∀ {x a} (ys : ∀ a → List (B a)) (b : B _) (p : a ≡ᵢ x) → fibreᵢ (ys a !_) b → fibre' (ys x) p b
    rem₂ {x = x} {a} ys b p (fin ix ⦃ forget q ⦄ , r) = fin ix ⦃ q' ⦄ , Equiv.from (rem₀ ys b p ix) r where
      q' = forget (transport (λ i → suc ix Nat.≤ length (ys (Id≃path.to p i))) q)

  sigma-member : ∀ {a b xs ys} → a ∈ₗ xs → b ∈ₗ ys a → (a , b) ∈ₗ sigma xs ys
  sigma-member {a = a} {b = b} {xs = x ∷ xs} {ys = ys} (here {x' = x'} p) q =
    ++-memberₗ $ member-pair x (ys x) a b (p , rem₂ ys b p (member→lookup q))
  sigma-member (there p) q = ++-memberᵣ (sigma-member p q)

  private
    split : ∀ {a b} xs ys → (a , b) ∈ₗ sigma xs ys → Type _
    split {a = a} {b} xs ys top = Σ[ p ∈ a ∈ₗ xs ] Σ[ q ∈ b ∈ₗ ys a ] (sigma-member p q ≡ top)

    here-sigma
      : ∀ (a : A) b xs ys {x : A} (q : (a , b) ∈ₗ map (x ,_) (ys x))
      → split (x ∷ xs) ys (++-memberₗ q)
    here-sigma a b xs ys {x} p with inspect (pair-member x (ys x) a b p)
    ... | (p' , fin ix ⦃ forget q ⦄ , r) , prf = here p' , elt , coh where
      q' = forget (transport (λ i → suc ix Nat.≤ length (ys (Id≃path.to p' (~ i)))) q)

      elt = lookup→member (rem₁ ys b p' (fin ix ⦃ forget q ⦄ , r))

      abstract
        coh : sigma-member {xs = x ∷ xs} (here p') elt ≡ ++-memberₗ p
        coh = ap ++-memberₗ
          (ap (member-pair x (ys x) a b)
            ( Σ-pathp refl (ap (rem₂ ys b p') (Equiv.ε member≃lookup _)
            ∙ Σ-pathp refl (Equiv.η (rem₀ ys b p' ix) _))
            ∙ sym prf)
          ∙ member-pair-inv x (ys x) a b p)

    member-sigma : ∀ a b xs ys (top : (a , b) ∈ₗ sigma xs ys) → split xs ys top
    member-sigma a b (x ∷ xs) ys top with member-++-view (map (x ,_) (ys x)) _ top
    ... | inl (q , prf) =
      let (a , b , it) = here-sigma a b xs ys q
      in a , b , it ∙ prf
    ... | inr (q , prf) =
      let (a , b , it) = member-sigma a b xs ys q
      in there a , b , ap ++-memberᵣ it ∙ prf

  member-sigmaₗ : ∀ {a b} xs ys → (a , b) ∈ₗ sigma xs ys → a ∈ₗ xs
  member-sigmaₗ _ _ p = member-sigma _ _ _ _ p .fst

  member-sigmaᵣ : ∀ {a b} xs ys → (a , b) ∈ₗ sigma xs ys → b ∈ₗ ys a
  member-sigmaᵣ xs ys p = member-sigma _ _ xs ys p .snd .fst

  sigma-member' : ∀ {a b xs ys} → a ∈ₗ xs × b ∈ₗ ys a → (a , b) ∈ₗ sigma xs ys
  sigma-member' (p , q) = sigma-member p q

  member-sigma-view : ∀ {a b} xs ys (p : (a , b) ∈ₗ sigma xs ys) → fibre sigma-member' p
  member-sigma-view xs ys p = record
    { fst = member-sigmaₗ xs ys p , member-sigmaᵣ xs ys p
    ; snd = member-sigma _ _ xs ys p .snd .snd
    }