Skip to content

Commit b865c6f

Browse files
authored
Update Base.agda
1 parent 36f8b9f commit b865c6f

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Cubical/Data/Sigma/Base.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,5 +54,5 @@ syntax ∃!-syntax A (λ x → B) = ∃![ x ∈ A ] B
5454
-- Instance
5555

5656
instance
57-
Σ-instance : {ℓ ℓ'} {A : Type ℓ} {B : A Type ℓ'} {{ x : A }} {{ B x }} Σ A B
58-
Σ-instance {{ x }} {{ y }} = (x , y)
57+
Σ-instance : {ℓ ℓ'} {A : Type ℓ} {B : A Type ℓ'} x : A ⦄ ⦃ B x Σ A B
58+
Σ-instance x ⦄ ⦃ y = (x , y)

0 commit comments

Comments
 (0)