-- Replaces the value mapped at i₀ with t₀.
substitute : {{_ : Eq I}} → (I → T) → I → T → I → T
substitute f i₀ t₀ i with i₀ == i
...                     | yes _ = t₀
...                     | no _  = f i

-- Whether two terms of possibly-distinct types satisfy some property.
-- TODO: this feels vaguely like a functor, except that it uses the equality
--       proof to rewrite types. Could probably be abstracted?
somehowCompare : (T → T → Type) → T → U → Dec (T ≡ U) → Type
somehowCompare _≟_ t u (yes eq) rewrite eq = t ≟ u
somehowCompare _ _ _ (no ¬eq) = ⊤


-- Defines a candidate for dep rel using a type alias of nested sums.
DepRelAlias : {{_ : Eq I}} → (op : (c : I → T) → J c → U) (c : I → T) → I → J c → Type₁
DepRelAlias {T = T} op c i j = Σ[ t ∈ T ]
    ∃ (somehowCompare (λ d₁ d₂ → d₁ j ≢ d₂ j) (op c) (op (substitute c i t)))

-- Does the same thing with a record type.
record DepRelRecord {{_ : Eq I}} (op : (c : I → T) → J c → U) (c : I → T) (i : I) (j : J c) : Type₁ where
  field
    t-sub : T
  c-sub = substitute c i t-sub
  field
    J-equal : Dec ((J c → U) ≡ (J c-sub → U)) -- TODO: only require equality between J c and J c-sub
    Depend? : somehowCompare (λ d₁ d₂ → d₁ j ≢ d₂ j) (op c) (op c-sub) J-equal


-- A version using a mapping function to convert between J c and J c-sub
DepRelMapped : {{_ : Eq I}} → (op : (c : I → T) → J c → U) (c : I → T) → I → J c → Type
DepRelMapped {T = T} {J = J} op c i j =
    Σ[ t ∈ T ] Σ[ mapⱼ ∈ (J c → J (substitute c i t))]
        op c j ≢ op (substitute c i t) (mapⱼ j)