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 }