[Agda] taking limit of a cumulative predicate

[Carette, Jacques]

ℕ is well-ordered, so you may as well take the smallest i, not just ‘some’ i.  If you further make your P i’s contractible (so as to be proof-irrelevant), then you’re closer to the classical case.

In general, you might want to read everything under Relation.Binary.Indexed in the standard library. I much prefer the Homogeneous case, the Heterogeneous version is weird in MLTT. [It’s not weird in other type theories.]

Jacques

From: Agda <agda-bounces at lists.chalmers.se> On Behalf Of Jason Hu
Sent: November 12, 2021 9:49 AM
To: agda at lists.chalmers.se
Subject: [Agda] taking limit of a cumulative predicate

Hi all,

I bumped into a difference between type theory and set theory that I am somewhat struggling with in Agda.

Consider a type D and its predicate indexed by natural number:

P : ℕ → D → Set

where for x : D, P i x means x is in the subset of D described by P i.

Now imagine P is cumulative, namely

cumu : ∀ {i a} → P i a → P (suc i) a

then sometimes, in set theory, we would conveniently take this index i to be \infty or omega and claim that such a subset is well-defined.

As you might have already noticed, this notion of taking a limit is difficult to formalize in a type theory. I can think of two tentative solutions:


  1.  using Sigma type
  2.
  3.  P∞ x = ∃ λ i → P i x
  4.
  5.  This seems plausible, especially when we see this notion captures the fact that the set theoretic counterpart does implies for every P∞ x some index i exists. However, a problem arises when we encounter two instances of P∞ x. Then to use them, we must unpack them, and now we have two distinct indices with no explicit relation. Meanwhile in set theory, we actually disregard the difference of indices, because we are talking about infinity.

  1.  another tentative solution is to redefine P such that it takes Maybe ℕ and the nothing case represents infinity. But this solution has a big problem. There could be an x : D such that only (P nothing x) holds. In other words, P becomes larger than the limit of its set theoretic counterpart.
Is there any solution to this problem which encodes the set theoretic notion more faithfully?

Thanks,
Jason Hu
https://hustmphrrr.github.io/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211112/aba44548/attachment-0001.html>