SHARE
TWEET

Untitled

a guest May 25th, 2019 71 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. -- Replaces the value mapped at i₀ with t₀.
  2. substitute : {{_ : Eq I}} → (I → T) → I → T → I → T
  3. substitute f i₀ t₀ i with i₀ == i
  4. ...                     | yes _ = t₀
  5. ...                     | no _  = f i
  6.  
  7. -- Whether two terms of possibly-distinct types satisfy some property.
  8. -- TODO: this feels vaguely like a functor, except that it uses the equality
  9. --       proof to rewrite types. Could probably be abstracted?
  10. somehowCompare : (T → T → Type) → T → U → Dec (T ≡ U) → Type
  11. somehowCompare _≟_ t u (yes eq) rewrite eq = t ≟ u
  12. somehowCompare _ _ _ (no ¬eq) = ⊤
  13.  
  14.  
  15. -- Defines a candidate for dep rel using a type alias of nested sums.
  16. DepRelAlias : {{_ : Eq I}} → (op : (c : I → T) → J c → U) (c : I → T) → I → J c → Type₁
  17. DepRelAlias {T = T} op c i j = Σ[ t ∈ T ]
  18.     ∃ (somehowCompare (λ d₁ d₂ → d₁ j ≢ d₂ j) (op c) (op (substitute c i t)))
  19.  
  20. -- Does the same thing with a record type.
  21. record DepRelRecord {{_ : Eq I}} (op : (c : I → T) → J c → U) (c : I → T) (i : I) (j : J c) : Type₁ where
  22.   field
  23.     t-sub : T
  24.   c-sub = substitute c i t-sub
  25.   field
  26.     J-equal : Dec ((J c → U) ≡ (J c-sub → U)) -- TODO: only require equality between J c and J c-sub
  27.     Depend? : somehowCompare (λ d₁ d₂ → d₁ j ≢ d₂ j) (op c) (op c-sub) J-equal
  28.    
  29.    
  30. -- A version using a mapping function to convert between J c and J c-sub
  31. DepRelMapped : {{_ : Eq I}} → (op : (c : I → T) → J c → U) (c : I → T) → I → J c → Type
  32. DepRelMapped {T = T} {J = J} op c i j =
  33.     Σ[ t ∈ T ] Σ[ mapⱼ ∈ (J c → J (substitute c i t))]
  34.         op c j ≢ op (substitute c i t) (mapⱼ j)
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top