[Replaced the syntax Σ[ x ∶ A ] B with Σ[ x ∈ A ] B. Nils Anders Danielsson **20120506171416 Ignore-this: de9703959a0f42cf81466c21c4a22a9 ] hunk ./src/Data/AVL/IndexedMap.agda 37 - fromKV : KV → Σ[ ik ∶ ∃ Key ] Value (proj₁ ik) + fromKV : KV → Σ[ ik ∈ ∃ Key ] Value (proj₁ ik) hunk ./src/Data/AVL/IndexedMap.agda 40 - toKV : Σ[ ik ∶ ∃ Key ] Value (proj₁ ik) → KV + toKV : Σ[ ik ∈ ∃ Key ] Value (proj₁ ik) → KV hunk ./src/Data/Container.agda 40 -⟦ C ⟧ X = Σ[ s ∶ Shape C ] (Position C s → X) +⟦ C ⟧ X = Σ[ s ∈ Shape C ] (Position C s → X) hunk ./src/Data/Container.agda 47 - Σ[ eq ∶ s ≡ s′ ] (∀ p → f p ≈ f′ (P.subst (Position C) eq p)) + Σ[ eq ∈ s ≡ s′ ] (∀ p → f p ≈ f′ (P.subst (Position C) eq p)) hunk ./src/Data/Product.agda 28 -syntax Σ A (λ x → B) = Σ[ x ∶ A ] B +syntax Σ A (λ x → B) = Σ[ x ∈ A ] B hunk ./src/Data/Product.agda 41 -A × B = Σ[ x ∶ A ] B +A × B = Σ[ x ∈ A ] B hunk ./src/Relation/Nullary/Negation.agda 141 - Q → (P → Σ Q R) → ¬ ¬ (Σ[ x ∶ Q ] (P → R x)) + Q → (P → Σ Q R) → ¬ ¬ (Σ[ x ∈ Q ] (P → R x))