/-! ファミリーと多項式 -/
/- →《《《《《《《《《《《《《《《《《《《《 → -/
namespace My
/- 型コンストラクタ Fam -/
def Fam (X : Type) := X → Type
abbrev FamOver := Fam
variable (I : Type) (i j : I)
variable (F G : FamOver I)
def Sigm {X: Type} (F : Fam X) : Type :=
Σ(x:X),(F x)
def π {X: Type} (F : Fam X) : (Sigm F) → X :=
λ(x : Sigm F)=>
match x with
| ⟨a, _⟩ => a
structure Sect {E B : Type} (f: E → B) where
map : B → E
cond : f ∘ map = λ(b:B)=>b
def Pi {X: Type} (F : Fam X) : Type :=
Sect (π F)
abbrev TyCon := Type → Type
def Poly {I : Type} (F: Fam I) : TyCon :=
λ(X : Type)=> Σ(i: I), (F i → X)
end My
/- ← 》》》》》》》》》》》》》》》》》》》》← -/
