avigad

universes u v
variables {ι : Type u} {α : Type v}

/- the usual definitions of indexed union and intersection -/

def Union (s : ι → set α) : set α := { a | ∃ i, a ∈ s i }
def Inter (s : ι → set α) : set α := { a | ∀ i, a ∈ s i }
notation `⋃` binders `, ` r:(scoped f, Union f) := r
notation `⋂` binders `, ` r:(scoped f, Inter f) := r

avigad

open tactic
open smt_tactic

meta def blast : tactic unit := using_smt $ intros >> try simp >> try eblast

notation `♮` := by abstract { blast }

universe variables u v

structure Category :=