• API
• FAQ
• Tools
• Archive
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.

Top