Andrej Bauer: Instance reducibility and containers

This is joint work with Danel Ahman.

Abstract: Instance reducibility is a notion of reducibility between predicates that captures a common proof-method: in order to show that ∀ b ∈ B . ψ(b) implies ∀ a ∈ A . φ(a), it suffices to establish ∀ a ∈ A ∃ b ∈ B . ψ(b) ⇒ φ(a). When this is the case, we say that φ is instance reducible to ψ, because every φ-instance a ∈ A follows from some ψ-instance b ∈ B. There is a strong similarity with container morphisms, which we get when the quantifiers ∀ and ∃ are replaced with their type-theoretic counterparts Π and Σ, and the predicates with type families. In the talk we shall make these observations mathematically precise.