2
$\begingroup$

It is relatively easy to construct an object in set/class theory which has properties of any of the following: dependent sum, dependent product, W-types.

E.g. Dependent sum of a family F is just the composition $(E^{-1}\ $o$\ F)$. (it depends slightly on definitions, but this is the idea)

Fix some family B. (let's say it is a class-function, or even just function) But how to obtain an object which will represent M(x:A)B(x)? (i.e. I am trying to implement coinductive types)

It was easy to implement inductive types, W(x:A)B(x) with a recursive definition of "stages" followed by set-theoretic union. But how to implement coinductive types M(x:A)B(x) ? How to mathematically define an object which will be a set-theoretic semantic of "M(x:A)B(x)"?

(related to this question : Definition of M-type in type theory )

very related to https://math.stackexchange.com/questions/4919803/way-of-defining-families-of-proper-classes-in-class-theory

enter image description here

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ What do you mean by "object" and "represent"? If you are talking about underlying realizers (in some computational model), you could look at the proof that realizability models interpret $M$-types as final coalgebras for polynomial functors. I can't tell whether you'd like to see how $M$-types are constructed in set theory, or implemented as datastructures. $\endgroup$
    – Andrej Bauer
    Commented May 29 at 13:15
  • $\begingroup$ Would it suffice to answer the question with: the $W$-type for a family $B : A \to \mathsf{Type}$ consists of well-founded trees with $A$-labeled nodes and branching types~$B$, while the corresponding $M$-type consists of all such trees (not necessarily well-founded)? $\endgroup$
    – Andrej Bauer
    Commented May 29 at 13:21
  • $\begingroup$ @AndrejBauer I understand how it should look like, but defining it is a bit elusive. How to define a class of such structures as a term anywhere in ZFC/NBG/MK ? For me answer is anything "It is a class of .... . (R is infinite tree) :<-> (... forall p in R: ...) . " $\endgroup$
    – g_d
    Commented May 29 at 14:31
  • $\begingroup$ @AndrejBauer I have posted an implementation in Coq as an answer to this question. I think I understand that element of w type is just arbitrary collection of branches = functions to sigma type with at most countable domains, just want to double-check that understanding is correct. $\endgroup$
    – g_d
    Commented May 29 at 15:18

1 Answer 1

Reset to default
0
$\begingroup$

This is my attempt to define M-types in Coq.

Inductive sigma (A:Type) (F:A->Type) : Type :=
 sigma_intro : forall (a : A), (F a) -> (sigma A F)  
.

Require Import List.


(* countable collection of something *)
Inductive Cou (X:Type) : Type :=
  fin : (list X) -> Cou X
| inf : (nat -> X) -> Cou X.

Definition M (A:Type) (F:A->Type) : Type 
  := sigma Type (fun Q => sigma Q (fun _ => Cou (sigma A F))).

(* It may not be enough: requires equal beginnings *)

Set-theoretically it will be something like $$ MF := \mathcal{P}\{f:D \to\Sigma F| (D\in\omega)\lor(D=\omega)\} $$ $$ = \mathcal{P}\{f|\exists D: (f:D \to \Sigma F) \land ( (D\in\omega)\lor(D=\omega))\} $$

(D is a variable bound by notation for class-collection)

Or should the values of the initial segments of the branches with equal initial labels coincide? Then it is necessary to require coinciding initial labels to have coinciding initial values $$ MF := \{Q\in\mathcal{P}\{f:D \to\Sigma F| (D\in\omega)\lor(D=\omega)\} | \forall f,g\in Q: \forall \mbox{i initial segment of }\omega: ((pr_1 \circ f)\restriction i)=((pr_1 \circ g) \restriction i) \longrightarrow f \restriction i = g \restriction i\} $$

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.