Return to Answer

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\} $$

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\} $$

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: \mbox{dom}((pr_1 \circ f)\restriction i)=\mbox{dom}((pr_1 \circ g) \restriction i) \longrightarrow f \restriction i = g \restriction i\} $$

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\} $$

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))).

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 factorize it somehow...

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: \mbox{dom}((pr_1 \circ f)\restriction i)=\mbox{dom}((pr_1 \circ g) \restriction i) \longrightarrow f \restriction i = g \restriction i\} $$