Skip to content

Commit 438f95a

Browse files
committed
convert Cast's implicit module param to variable
(needed for next commit)
1 parent 9146bee commit 438f95a

File tree

1 file changed

+9
-5
lines changed
  • src/Data/Vec/Relation/Binary/Equality

1 file changed

+9
-5
lines changed

src/Data/Vec/Relation/Binary/Equality/Cast.agda

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,9 @@
1010

1111
{-# OPTIONS --cubical-compatible --safe #-}
1212

13-
module Data.Vec.Relation.Binary.Equality.Cast {a} {A : Set a} where
13+
module Data.Vec.Relation.Binary.Equality.Cast where
1414

15+
open import Level using (Level)
1516
open import Data.Nat.Base using (ℕ; zero; suc)
1617
open import Data.Nat.Properties using (suc-injective)
1718
open import Data.Vec.Base
@@ -24,6 +25,8 @@ open import Relation.Binary.PropositionalEquality.Properties
2425

2526
private
2627
variable
28+
a : Level
29+
A : Set a
2730
l m n o :
2831
xs ys zs : Vec A n
2932

@@ -41,24 +44,25 @@ cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
4144

4245
infix 3 _≈[_]_
4346

44-
_≈[_]_ : {n m} Vec A n .(eq : n ≡ m) Vec A m Set a
47+
_≈[_]_ : {n m} Vec A n .(eq : n ≡ m) Vec A m Set _
4548
xs ≈[ eq ] ys = cast eq xs ≡ ys
4649

4750
------------------------------------------------------------------------
4851
-- _≈[_]_ is ‘reflexive’, ‘symmetric’ and ‘transitive’
4952

50-
≈-reflexive : {n} _≡_ ⇒ (λ xs ys _≈[_]_ {n} xs refl ys)
53+
≈-reflexive : {n} _≡_ ⇒ (λ xs ys _≈[_]_ {A = A} {n} xs refl ys)
5154
≈-reflexive {x = x} eq = trans (cast-is-id refl x) eq
5255

53-
≈-sym : .{m≡n : m ≡ n} Sym _≈[ m≡n ]_ _≈[ sym m≡n ]_
56+
≈-sym : .{m≡n : m ≡ n} Sym {A = Vec A m} _≈[ m≡n ]_ _≈[ sym m≡n ]_
5457
≈-sym {m≡n = m≡n} {xs} {ys} xs≈ys = begin
5558
cast (sym m≡n) ys ≡⟨ cong (cast (sym m≡n)) xs≈ys ⟨
5659
cast (sym m≡n) (cast m≡n xs) ≡⟨ cast-trans m≡n (sym m≡n) xs ⟩
5760
cast (trans m≡n (sym m≡n)) xs ≡⟨ cast-is-id (trans m≡n (sym m≡n)) xs ⟩
5861
xs ∎
5962
where open ≡-Reasoning
6063

61-
≈-trans : .{m≡n : m ≡ n} .{n≡o : n ≡ o} Trans _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_
64+
≈-trans : .{m≡n : m ≡ n} .{n≡o : n ≡ o}
65+
Trans {A = Vec A m} _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_
6266
≈-trans {m≡n = m≡n} {n≡o} {xs} {ys} {zs} xs≈ys ys≈zs = begin
6367
cast (trans m≡n n≡o) xs ≡⟨ cast-trans m≡n n≡o xs ⟨
6468
cast n≡o (cast m≡n xs) ≡⟨ cong (cast n≡o) xs≈ys ⟩

0 commit comments

Comments
 (0)