Merge tag 'upstream/0.17'

Upstream version 0.17

# gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST
# gpg:                using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240
# gpg:                issuer "spwhitton@spwhitton.name"
# gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate]
# Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4  753F 0F56 D055 3B6D 411B
#      Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC  248B 695B 7AE4 BF06 6240

9 files changed, 108 insertions, 185 deletions

diff --git a/src/Data/Star/BoundedVec.agda b/src/Data/Star/BoundedVec.agda
index cef4e6c..376fe14 100644
--- a/src/Data/Star/BoundedVec.agda
+++ b/src/Data/Star/BoundedVec.agda
@@ -8,16 +8,16 @@
 
 module Data.Star.BoundedVec where
 
-open import Data.Star
+import Data.Maybe.Base as Maybe
 open import Data.Star.Nat
 open import Data.Star.Decoration
 open import Data.Star.Pointer
 open import Data.Star.List using (List)
 open import Data.Unit
 open import Function
-import Data.Maybe.Base as Maybe
 open import Relation.Binary
 open import Relation.Binary.Consequences
+open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 
 ------------------------------------------------------------------------
 -- The type
diff --git a/src/Data/Star/Decoration.agda b/src/Data/Star/Decoration.agda
index 0e954cc..fb98b19 100644
--- a/src/Data/Star/Decoration.agda
+++ b/src/Data/Star/Decoration.agda
@@ -6,49 +6,50 @@
 
 module Data.Star.Decoration where
 
-open import Data.Star
-open import Relation.Binary
-open import Function
 open import Data.Unit
+open import Function
 open import Level
+open import Relation.Binary
+open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 
 -- A predicate on relation "edges" (think of the relation as a graph).
 
-EdgePred : {I : Set} → Rel I zero → Set₁
-EdgePred T = ∀ {i j} → T i j → Set
+EdgePred : {ℓ r : Level} (p : Level) {I : Set ℓ} → Rel I r → Set (suc p ⊔ ℓ ⊔ r)
+EdgePred p T = ∀ {i j} → T i j → Set p
+
 
-data NonEmptyEdgePred {I : Set}
-                      (T : Rel I zero) (P : EdgePred T) : Set where
+data NonEmptyEdgePred {ℓ r p : Level} {I : Set ℓ} (T : Rel I r)
+                      (P : EdgePred p T) : Set (ℓ ⊔ r ⊔ p) where
   nonEmptyEdgePred : ∀ {i j} {x : T i j}
                      (p : P x) → NonEmptyEdgePred T P
 
 -- Decorating an edge with more information.
 
-data DecoratedWith {I : Set} {T : Rel I zero} (P : EdgePred T)
-       : Rel (NonEmpty (Star T)) zero where
+data DecoratedWith {ℓ r p : Level} {I : Set ℓ} {T : Rel I r} (P : EdgePred p T)
+       : Rel (NonEmpty (Star T)) p where
   ↦ : ∀ {i j k} {x : T i j} {xs : Star T j k}
       (p : P x) → DecoratedWith P (nonEmpty (x ◅ xs)) (nonEmpty xs)
 
-edge : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} →
-       DecoratedWith {T = T} P i j → NonEmpty T
-edge (↦ {x = x} p) = nonEmpty x
+module _ {ℓ r p : Level} {I : Set ℓ} {T : Rel I r} {P : EdgePred p T} where
+
+  edge : ∀ {i j} → DecoratedWith {T = T} P i j → NonEmpty T
+  edge (↦ {x = x} p) = nonEmpty x
 
-decoration : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} →
-             (d : DecoratedWith {T = T} P i j) →
-             P (NonEmpty.proof (edge d))
-decoration (↦ p) = p
+  decoration : ∀ {i j} → (d : DecoratedWith {T = T} P i j) →
+               P (NonEmpty.proof (edge d))
+  decoration (↦ p) = p
 
 -- Star-lists decorated with extra information. All P xs means that
 -- all edges in xs satisfy P.
 
-All : ∀ {I} {T : Rel I zero} → EdgePred T → EdgePred (Star T)
+All : ∀ {ℓ r p} {I : Set ℓ} {T : Rel I r} → EdgePred p T → EdgePred (ℓ ⊔ (r ⊔ p)) (Star T)
 All P {j = j} xs =
   Star (DecoratedWith P) (nonEmpty xs) (nonEmpty {y = j} ε)
 
 -- We can map over decorated vectors.
 
-gmapAll : ∀ {I} {T : Rel I zero} {P : EdgePred T}
-                {J} {U : Rel J zero} {Q : EdgePred U}
+gmapAll : ∀ {ℓ ℓ′ r p q} {I : Set ℓ} {T : Rel I r} {P : EdgePred p T}
+                {J : Set ℓ′} {U : Rel J r} {Q : EdgePred q U}
                 {i j} {xs : Star T i j}
           (f : I → J) (g : T =[ f ]⇒ U) →
           (∀ {i j} {x : T i j} → P x → Q (g x)) →
@@ -59,7 +60,8 @@ gmapAll f g h (↦ x ◅ xs) = ↦ (h x) ◅ gmapAll f g h xs
 -- Since we don't automatically have gmap id id xs ≡ xs it is easier
 -- to implement mapAll in terms of map than in terms of gmapAll.
 
-mapAll : ∀ {I} {T : Rel I zero} {P Q : EdgePred T} {i j} {xs : Star T i j} →
+mapAll : ∀ {ℓ r p q} {I : Set ℓ} {T : Rel I r}
+         {P : EdgePred p T} {Q : EdgePred q T} {i j} {xs : Star T i j} →
          (∀ {i j} {x : T i j} → P x → Q x) →
          All P xs → All Q xs
 mapAll {P = P} {Q} f ps = map F ps
@@ -69,7 +71,7 @@ mapAll {P = P} {Q} f ps = map F ps
 
 -- We can decorate star-lists with universally true predicates.
 
-decorate : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} →
+decorate : ∀ {ℓ r p} {I : Set ℓ} {T : Rel I r} {P : EdgePred p T} {i j} →
            (∀ {i j} (x : T i j) → P x) →
            (xs : Star T i j) → All P xs
 decorate f ε        = ε
@@ -79,13 +81,13 @@ decorate f (x ◅ xs) = ↦ (f x) ◅ decorate f xs
 
 infixr 5 _◅◅◅_ _▻▻▻_
 
-_◅◅◅_ : ∀ {I} {T : Rel I zero} {P : EdgePred T}
+_◅◅◅_ : ∀ {ℓ r p} {I : Set ℓ} {T : Rel I r} {P : EdgePred p T}
               {i j k} {xs : Star T i j} {ys : Star T j k} →
         All P xs → All P ys → All P (xs ◅◅ ys)
 ε          ◅◅◅ ys = ys
 (↦ x ◅ xs) ◅◅◅ ys = ↦ x ◅ xs ◅◅◅ ys
 
-_▻▻▻_ : ∀ {I} {T : Rel I zero} {P : EdgePred T}
+_▻▻▻_ : ∀ {ℓ r p} {I : Set ℓ} {T : Rel I r} {P : EdgePred p T}
               {i j k} {xs : Star T j k} {ys : Star T i j} →
         All P xs → All P ys → All P (xs ▻▻ ys)
 _▻▻▻_ = flip _◅◅◅_
diff --git a/src/Data/Star/Environment.agda b/src/Data/Star/Environment.agda
index 826d8e7..fe906f0 100644
--- a/src/Data/Star/Environment.agda
+++ b/src/Data/Star/Environment.agda
@@ -4,36 +4,38 @@
 -- Environments (heterogeneous collections)
 ------------------------------------------------------------------------
 
-module Data.Star.Environment (Ty : Set) where
+module Data.Star.Environment {ℓ} (Ty : Set ℓ) where
 
-open import Data.Star
+open import Level
 open import Data.Star.List
 open import Data.Star.Decoration
 open import Data.Star.Pointer as Pointer hiding (lookup)
 open import Data.Unit
+open import Function hiding (_∋_)
 open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 
 -- Contexts, listing the types of all the elements in an environment.
 
-Ctxt : Set
+Ctxt : Set ℓ
 Ctxt = List Ty
 
 -- Variables (de Bruijn indices); pointers into environments.
 
 infix 4 _∋_
 
-_∋_ : Ctxt → Ty → Set
-Γ ∋ σ = Any (λ _ → ⊤) (_≡_ σ) Γ
+_∋_ : Ctxt → Ty → Set ℓ
+Γ ∋ σ = Any (const (Lift ℓ ⊤)) (σ ≡_) Γ
 
 vz : ∀ {Γ σ} → Γ ▻ σ ∋ σ
 vz = this refl
 
 vs : ∀ {Γ σ τ} → Γ ∋ τ → Γ ▻ σ ∋ τ
-vs = that tt
+vs = that _
 
 -- Environments. The T function maps types to element types.
 
-Env : (Ty → Set) → Ctxt → Set
+Env : ∀ {e} → (Ty → Set e) → (Ctxt → Set (ℓ ⊔ e))
 Env T Γ = All T Γ
 
 -- A safe lookup function for environments.
diff --git a/src/Data/Star/Fin.agda b/src/Data/Star/Fin.agda
index add8e50..e20fc41 100644
--- a/src/Data/Star/Fin.agda
+++ b/src/Data/Star/Fin.agda
@@ -1,12 +1,11 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Finite sets defined in terms of Data.Star
+-- Finite sets defined using the reflexive-transitive closure, Star
 ------------------------------------------------------------------------
 
 module Data.Star.Fin where
 
-open import Data.Star
 open import Data.Star.Nat as ℕ using (ℕ)
 open import Data.Star.Pointer
 open import Data.Unit
diff --git a/src/Data/Star/List.agda b/src/Data/Star/List.agda
index 54aeb1a..9365f86 100644
--- a/src/Data/Star/List.agda
+++ b/src/Data/Star/List.agda
@@ -1,29 +1,30 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Lists defined in terms of Data.Star
+-- Lists defined in terms of the reflexive-transitive closure, Star
 ------------------------------------------------------------------------
 
 module Data.Star.List where
 
-open import Data.Star
-open import Data.Unit
-open import Relation.Binary.Simple
 open import Data.Star.Nat
+open import Data.Unit
+open import Relation.Binary.Construct.Always using (Always)
+open import Relation.Binary.Construct.Constant using (Const)
+open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 
 -- Lists.
 
-List : Set → Set
-List a = Star (Const a) tt tt
+List : ∀ {a} → Set a → Set a
+List A = Star (Const A) tt tt
 
 -- Nil and cons.
 
-[] : ∀ {a} → List a
+[] : ∀ {a} {A : Set a} → List A
 [] = ε
 
 infixr 5 _∷_
 
-_∷_ : ∀ {a} → a → List a → List a
+_∷_ : ∀ {a} {A : Set a} → A → List A → List A
 _∷_ = _◅_
 
 -- The sum of the elements in a list containing natural numbers.
diff --git a/src/Data/Star/Nat.agda b/src/Data/Star/Nat.agda
index a54a465..7597032 100644
--- a/src/Data/Star/Nat.agda
+++ b/src/Data/Star/Nat.agda
@@ -1,16 +1,16 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Natural numbers defined in terms of Data.Star
+-- Natural numbers defined using the reflexive-transitive closure, Star
 ------------------------------------------------------------------------
 
 module Data.Star.Nat where
 
-open import Data.Star
 open import Data.Unit
 open import Function
 open import Relation.Binary
-open import Relation.Binary.Simple
+open import Relation.Binary.Construct.Closure.ReflexiveTransitive
+open import Relation.Binary.Construct.Always using (Always)
 
 -- Natural numbers.
 
diff --git a/src/Data/Star/Pointer.agda b/src/Data/Star/Pointer.agda
index 52d9737..83983c6 100644
--- a/src/Data/Star/Pointer.agda
+++ b/src/Data/Star/Pointer.agda
@@ -4,21 +4,22 @@
 -- Pointers into star-lists
 ------------------------------------------------------------------------
 
-module Data.Star.Pointer where
+module Data.Star.Pointer {ℓ} {I : Set ℓ} where
 
-open import Data.Star
-open import Data.Star.Decoration
-open import Relation.Binary
 open import Data.Maybe.Base using (Maybe; nothing; just)
+open import Data.Star.Decoration
 open import Data.Unit
 open import Function
 open import Level
+open import Relation.Binary
+open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 
 -- Pointers into star-lists. The edge pointed to is decorated with Q,
 -- while other edges are decorated with P.
 
-data Pointer {I : Set} {T : Rel I zero} (P Q : EdgePred T)
-       : Rel (Maybe (NonEmpty (Star T))) zero where
+data Pointer {r p q} {T : Rel I r}
+             (P : EdgePred p T) (Q : EdgePred q T)
+             : Rel (Maybe (NonEmpty (Star T))) (p ⊔ q) where
   step : ∀ {i j k} {x : T i j} {xs : Star T j k}
          (p : P x) → Pointer P Q (just (nonEmpty (x ◅ xs)))
                                  (just (nonEmpty xs))
@@ -30,61 +31,60 @@ data Pointer {I : Set} {T : Rel I zero} (P Q : EdgePred T)
 -- is basically a prefix of xs; the existence of such a prefix
 -- guarantees that xs is non-empty.
 
-Any : ∀ {I} {T : Rel I zero} (P Q : EdgePred T) → EdgePred (Star T)
+Any : ∀ {r p q} {T : Rel I r} (P : EdgePred p T) (Q : EdgePred q T) →
+      EdgePred (ℓ ⊔ (r ⊔ (p ⊔ q))) (Star T)
 Any P Q xs = Star (Pointer P Q) (just (nonEmpty xs)) nothing
 
-this : ∀ {I} {T : Rel I zero} {P Q : EdgePred T}
-             {i j k} {x : T i j} {xs : Star T j k} →
-       Q x → Any P Q (x ◅ xs)
-this q = done q ◅ ε
+module _ {r p q} {T : Rel I r} {P : EdgePred p T} {Q : EdgePred q T} where
+
+  this : ∀ {i j k} {x : T i j} {xs : Star T j k} →
+         Q x → Any P Q (x ◅ xs)
+  this q = done q ◅ ε
 
-that : ∀ {I} {T : Rel I zero} {P Q : EdgePred T}
-       {i j k} {x : T i j} {xs : Star T j k} →
-       P x → Any P Q xs → Any P Q (x ◅ xs)
-that p = _◅_ (step p)
+  that : ∀ {i j k} {x : T i j} {xs : Star T j k} →
+         P x → Any P Q xs → Any P Q (x ◅ xs)
+  that p = _◅_ (step p)
 
 -- Safe lookup.
 
-data Result {I : Set} (T : Rel I zero) (P Q : EdgePred T) : Set where
-  result : ∀ {i j} {x : T i j}
-           (p : P x) (q : Q x) → Result T P Q
+data Result {r p q} (T : Rel I r)
+            (P : EdgePred p T) (Q : EdgePred q T) : Set (ℓ ⊔ r ⊔ p ⊔ q) where
+  result : ∀ {i j} {x : T i j} (p : P x) (q : Q x) → Result T P Q
 
 -- The first argument points out which edge to extract. The edge is
 -- returned, together with proofs that it satisfies Q and R.
 
-lookup : ∀ {I} {T : Rel I zero} {P Q R : EdgePred T}
-               {i j} {xs : Star T i j} →
-         Any P Q xs → All R xs → Result T Q R
-lookup (done q ◅ ε)      (↦ r ◅ _)  = result q r
-lookup (step p ◅ ps)     (↦ r ◅ rs) = lookup ps rs
-lookup (done _ ◅ () ◅ _) _
+module _ {t p q} {T : Rel I t} {P : EdgePred p T} {Q : EdgePred q T} where
+
+  lookup : ∀ {r} {R : EdgePred r T} {i j} {xs : Star T i j} →
+           Any P Q xs → All R xs → Result T Q R
+  lookup (done q ◅ ε)      (↦ r ◅ _)  = result q r
+  lookup (step p ◅ ps)     (↦ r ◅ rs) = lookup ps rs
+  lookup (done _ ◅ () ◅ _) _
 
 -- We can define something resembling init.
 
-prefixIndex : ∀ {I} {T : Rel I zero} {P Q : EdgePred T}
-                    {i j} {xs : Star T i j} →
-              Any P Q xs → I
-prefixIndex (done {i = i} q ◅ _)  = i
-prefixIndex (step p         ◅ ps) = prefixIndex ps
+  prefixIndex : ∀ {i j} {xs : Star T i j} → Any P Q xs → I
+  prefixIndex (done {i = i} q ◅ _)  = i
+  prefixIndex (step p         ◅ ps) = prefixIndex ps
 
-prefix : ∀ {I} {T : Rel I zero} {P Q : EdgePred T} {i j} {xs : Star T i j} →
-         (ps : Any P Q xs) → Star T i (prefixIndex ps)
-prefix (done q         ◅ _)  = ε
-prefix (step {x = x} p ◅ ps) = x ◅ prefix ps
+  prefix : ∀ {i j} {xs : Star T i j} →
+           (ps : Any P Q xs) → Star T i (prefixIndex ps)
+  prefix (done q         ◅ _)  = ε
+  prefix (step {x = x} p ◅ ps) = x ◅ prefix ps
 
 -- Here we are taking the initial segment of ps (all elements but the
 -- last, i.e. all edges satisfying P).
 
-init : ∀ {I} {T : Rel I zero} {P Q : EdgePred T} {i j} {xs : Star T i j} →
-       (ps : Any P Q xs) → All P (prefix ps)
-init (done q ◅ _)  = ε
-init (step p ◅ ps) = ↦ p ◅ init ps
+  init : ∀ {i j} {xs : Star T i j} →
+        (ps : Any P Q xs) → All P (prefix ps)
+  init (done q ◅ _)  = ε
+  init (step p ◅ ps) = ↦ p ◅ init ps
 
 -- One can simplify the implementation by not carrying around the
 -- indices in the type:
 
-last : ∀ {I} {T : Rel I zero} {P Q : EdgePred T}
-             {i j} {xs : Star T i j} →
-       Any P Q xs → NonEmptyEdgePred T Q
-last ps with lookup ps (decorate (const tt) _)
-... | result q _ = nonEmptyEdgePred q
+  last : ∀ {i j} {xs : Star T i j} →
+         Any P Q xs → NonEmptyEdgePred T Q
+  last ps with lookup {r = p} ps (decorate (const (lift tt)) _)
+  ... | result q _ = nonEmptyEdgePred q
diff --git a/src/Data/Star/Properties.agda b/src/Data/Star/Properties.agda
index a5d88bf..e3672bb 100644
--- a/src/Data/Star/Properties.agda
+++ b/src/Data/Star/Properties.agda
@@ -2,94 +2,13 @@
 -- The Agda standard library
 --
 -- Some properties related to Data.Star
+--
+-- This module is DEPRECATED. Please use the
+-- Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
+-- module directly.
 ------------------------------------------------------------------------
 
 module Data.Star.Properties where
 
-open import Data.Star
-open import Function
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as PropEq
-  using (_≡_; refl; sym; cong; cong₂)
-import Relation.Binary.PreorderReasoning as PreR
-
-◅◅-assoc : ∀ {i t} {I : Set i} {T : Rel I t} {i j k l}
-           (xs : Star T i j) (ys : Star T j k)
-           (zs : Star T k l) →
-           (xs ◅◅ ys) ◅◅ zs ≡ xs ◅◅ (ys ◅◅ zs)
-◅◅-assoc ε        ys zs = refl
-◅◅-assoc (x ◅ xs) ys zs = cong (_◅_ x) (◅◅-assoc xs ys zs)
-
-gmap-id : ∀ {i t} {I : Set i} {T : Rel I t} {i j} (xs : Star T i j) →
-          gmap id id xs ≡ xs
-gmap-id ε        = refl
-gmap-id (x ◅ xs) = cong (_◅_ x) (gmap-id xs)
-
-gmap-∘ : ∀ {i t} {I : Set i} {T : Rel I t}
-           {j u} {J : Set j} {U : Rel J u}
-           {k v} {K : Set k} {V : Rel K v}
-         (f  : J → K) (g  : U =[ f  ]⇒ V)
-         (f′ : I → J) (g′ : T =[ f′ ]⇒ U)
-         {i j} (xs : Star T i j) →
-         (gmap {U = V} f g ∘ gmap f′ g′) xs ≡ gmap (f ∘ f′) (g ∘ g′) xs
-gmap-∘ f g f′ g′ ε        = refl
-gmap-∘ f g f′ g′ (x ◅ xs) = cong (_◅_ (g (g′ x))) (gmap-∘ f g f′ g′ xs)
-
-gmap-◅◅ : ∀ {i t j u}
-            {I : Set i} {T : Rel I t} {J : Set j} {U : Rel J u}
-          (f : I → J) (g : T =[ f ]⇒ U)
-          {i j k} (xs : Star T i j) (ys : Star T j k) →
-          gmap {U = U} f g (xs ◅◅ ys) ≡ gmap f g xs ◅◅ gmap f g ys
-gmap-◅◅ f g ε        ys = refl
-gmap-◅◅ f g (x ◅ xs) ys = cong (_◅_ (g x)) (gmap-◅◅ f g xs ys)
-
-gmap-cong : ∀ {i t j u}
-              {I : Set i} {T : Rel I t} {J : Set j} {U : Rel J u}
-            (f : I → J) (g : T =[ f ]⇒ U) (g′ : T =[ f ]⇒ U) →
-            (∀ {i j} (x : T i j) → g x ≡ g′ x) →
-            ∀ {i j} (xs : Star T i j) →
-            gmap {U = U} f g xs ≡ gmap f g′ xs
-gmap-cong f g g′ eq ε        = refl
-gmap-cong f g g′ eq (x ◅ xs) = cong₂ _◅_ (eq x) (gmap-cong f g g′ eq xs)
-
-fold-◅◅ : ∀ {i p} {I : Set i}
-          (P : Rel I p) (_⊕_ : Transitive P) (∅ : Reflexive P) →
-          (∀ {i j} (x : P i j) → (∅ ⊕ x) ≡ x) →
-          (∀ {i j k l} (x : P i j) (y : P j k) (z : P k l) →
-             ((x ⊕ y) ⊕ z) ≡ (x ⊕ (y ⊕ z))) →
-          ∀ {i j k} (xs : Star P i j) (ys : Star P j k) →
-          fold P _⊕_ ∅ (xs ◅◅ ys) ≡ (fold P _⊕_ ∅ xs ⊕ fold P _⊕_ ∅ ys)
-fold-◅◅ P _⊕_ ∅ left-unit assoc ε        ys = sym (left-unit _)
-fold-◅◅ P _⊕_ ∅ left-unit assoc (x ◅ xs) ys = begin
-  (x ⊕  fold P _⊕_ ∅ (xs ◅◅ ys))              ≡⟨ cong (_⊕_ x) $
-                                                   fold-◅◅ P _⊕_ ∅ left-unit assoc xs ys ⟩
-  (x ⊕ (fold P _⊕_ ∅ xs  ⊕ fold P _⊕_ ∅ ys))  ≡⟨ sym (assoc x _ _) ⟩
-  ((x ⊕ fold P _⊕_ ∅ xs) ⊕ fold P _⊕_ ∅ ys)   ∎
-  where open PropEq.≡-Reasoning
-
--- Reflexive transitive closures are preorders.
-
-preorder : ∀ {i t} {I : Set i} (T : Rel I t) → Preorder _ _ _
-preorder T = record
-  { _≈_        = _≡_
-  ; _∼_        = Star T
-  ; isPreorder = record
-    { isEquivalence = PropEq.isEquivalence
-    ; reflexive     = reflexive
-    ; trans         = _◅◅_
-    }
-  }
-  where
-  reflexive : _≡_ ⇒ Star T
-  reflexive refl = ε
-
--- Preorder reasoning for Star.
-
-module StarReasoning {i t} {I : Set i} (T : Rel I t) where
-  open PreR (preorder T) public
-    renaming (_∼⟨_⟩_ to _⟶⋆⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_)
-
-  infixr 2 _⟶⟨_⟩_
-
-  _⟶⟨_⟩_ : ∀ x {y z} → T x y → y IsRelatedTo z → x IsRelatedTo z
-  x ⟶⟨ x⟶y ⟩ y⟶⋆z = x ⟶⋆⟨ x⟶y ◅ ε ⟩ y⟶⋆z
+open import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
+  public
diff --git a/src/Data/Star/Vec.agda b/src/Data/Star/Vec.agda
index e7e0a53..e10b941 100644
--- a/src/Data/Star/Vec.agda
+++ b/src/Data/Star/Vec.agda
@@ -1,12 +1,11 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Vectors defined in terms of Data.Star
+-- Vectors defined in terms of the reflexive-transitive closure, Star
 ------------------------------------------------------------------------
 
 module Data.Star.Vec where
 
-open import Data.Star
 open import Data.Star.Nat
 open import Data.Star.Fin using (Fin)
 open import Data.Star.Decoration
@@ -14,6 +13,7 @@ open import Data.Star.Pointer as Pointer hiding (lookup)
 open import Data.Star.List using (List)
 open import Relation.Binary
 open import Relation.Binary.Consequences
+open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 open import Function
 open import Data.Unit
 
@@ -21,45 +21,45 @@ open import Data.Unit
 -- information (i.e. elements).
 
 Vec : Set → ℕ → Set
-Vec a = All (λ _ → a)
+Vec A = All (λ _ → A)
 
 -- Nil and cons.
 
-[] : ∀ {a} → Vec a zero
+[] : ∀ {A} → Vec A zero
 [] = ε
 
 infixr 5 _∷_
 
-_∷_ : ∀ {a n} → a → Vec a n → Vec a (suc n)
+_∷_ : ∀ {A n} → A → Vec A n → Vec A (suc n)
 x ∷ xs = ↦ x ◅ xs
 
 -- Projections.
 
-head : ∀ {a n} → Vec a (1# + n) → a
+head : ∀ {A n} → Vec A (1# + n) → A
 head (↦ x ◅ _) = x
 
-tail : ∀ {a n} → Vec a (1# + n) → Vec a n
+tail : ∀ {A n} → Vec A (1# + n) → Vec A n
 tail (↦ _ ◅ xs) = xs
 
 -- Append.
 
 infixr 5 _++_
 
-_++_ : ∀ {a m n} → Vec a m → Vec a n → Vec a (m + n)
+_++_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m + n)
 _++_ = _◅◅◅_
 
 -- Safe lookup.
 
-lookup : ∀ {a n} → Fin n → Vec a n → a
+lookup : ∀ {A n} → Fin n → Vec A n → A
 lookup i xs with Pointer.lookup i xs
 ... | result _ x = x
 
 ------------------------------------------------------------------------
 -- Conversions
 
-fromList : ∀ {a} → (xs : List a) → Vec a (length xs)
+fromList : ∀ {A} → (xs : List A) → Vec A (length xs)
 fromList ε        = []
 fromList (x ◅ xs) = x ∷ fromList xs
 
-toList : ∀ {a n} → Vec a n → List a
+toList : ∀ {A n} → Vec A n → List A
 toList = gmap (const tt) decoration