⊆

集合の包含関係なんですが、Agda で、

　　_⊆_ :　( A B : OD　 ) → ∀{ x : OD　} →　Set n
　　_⊆_ A B {x} = A ∋ x →　B ∋ x

を使ってたんですが、変数 x がうっとうしい。省略可能にしてるんだけど消せないんだよな。

プロシンの発表資料書かないといけないので、twitter でぶつぶついいながらやってたら、record にすれば良いってのが降ってきました。

　　record _⊆_ ( A B : OD ) : Set (suc n) where
　　　field
　　　　 incl : { x : OD } → A ∋ x →　B ∋ x

なるほどね。∀を隠すのはこうするのか。

　 ⊆-trans :　{a b c x : OD}　→　_⊆_ a b {x}　→　 _⊆_ b c {x}　→　 _⊆_ a c {x}　　
　 ⊆-trans a⊆b b⊆c a∋x　= b⊆c (a⊆b a∋x)

が、

　 ⊆-trans :　{a b c : OD}　→　a ⊆ b　→　 b ⊆ c　→ a ⊆ c　　
　 ⊆-trans a⊆b b⊆c = record { incl = λ a∋x →　incl b⊆c (incl a⊆b a∋x) }

おお、まとも。この手の「二項関係を data や record で表す」ってのは面白い。