We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent b865c6f commit 7e13086Copy full SHA for 7e13086
Cubical/Data/Sigma/Base.agda
@@ -54,5 +54,5 @@ syntax ∃!-syntax A (λ x → B) = ∃![ x ∈ A ] B
54
-- Instance
55
56
instance
57
- Σ-instance : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} ⦃ x : A ⦄ ⦃ B x ⦄ → Σ A B
+ Σ-instance : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} ⦃ x : A ⦄ ⦃ _ : B x ⦄ → Σ A B
58
Σ-instance ⦃ x ⦄ ⦃ y ⦄ = (x , y)
0 commit comments