\lambda\delta home page

home	news	documentation	specification		implementation
foreword	milestones	version 2	version 2	(background - core - applications)	library	(static LDDL directory)
citations	visibility	version 1	version 1	(static HELM directory)	helena

Informal description: ""

{λ[sigma:Set] . λ[tau:Set] . λ[f:Π[x:sigma] . tau] . λ[i:{(f) . (tau) . (sigma)} . injective ] . λ[ta:tau] . λ[ja:{(ta) . (f) . (tau) . (sigma)} . image ] . λ[tb:tau] . λ[jb:{(tb) . (f) . (tau) . (sigma)} . image ] . λ[j:{({(jb) . (tb) . (i) . (f) . (tau) . (sigma)} . soft ) . ({(ja) . (ta) . (i) . (f) . (tau) . (sigma)} . soft ) . (sigma)} . is ]} . <{(tb) . (ta) . (tau)} . is > . {({(jb) . (tb) . (i) . (f) . (tau) . (sigma)} . ists2 ) . ({(j) . ({(jb) . (tb) . (i) . (f) . (tau) . (sigma)} . soft ) . ({(ja) . (ta) . (i) . (f) . (tau) . (sigma)} . soft ) . (f) . (tau) . (sigma)} . isf ) . ({(ja) . (ta) . (i) . (f) . (tau) . (sigma)} . ists1 ) . (tb) . ({({(jb) . (tb) . (i) . (f) . (tau) . (sigma)} . soft ) . (f) . (tau) . (sigma)} . tofs ) . ({({(ja) . (ta) . (i) . (f) . (tau) . (sigma)} . soft ) . (f) . (tau) . (sigma)} . tofs ) . (ta) . (tau)} . tr3is

Validation parameters: sort hierarchy = "Z2", kernel options = ""