\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] . λ[b:{(f) . (tau) . (sigma)} . bijective ] . λ[s:sigma]} . <{(((s) . f) . {(b) . (f) . (tau) . (sigma)} . invf ) . (s) . (sigma)} . is > . {({({({(s) . (f) . (tau) . (sigma)} . tofs ) . (tau)} . refis ) . (({(s) . (f) . (tau) . (sigma)} . tofs ) . {(b) . (f) . (tau) . (sigma)} . t3 ) . ({(s) . (f) . (tau) . (sigma)} . tofs ) . ({(s) . (f) . (tau) . (sigma)} . imagei ) . ({(s) . (f) . (tau) . (sigma)} . tofs ) . ({(b) . (f) . (tau) . (sigma)} . t2 ) . (f) . (tau) . (sigma)} . isinv ) . ({(s) . ({(b) . (f) . (tau) . (sigma)} . t2 ) . (f) . (tau) . (sigma)} . isst1 ) . (((s) . f) . {(b) . (f) . (tau) . (sigma)} . invf ) . ({({(s) . (f) . (tau) . (sigma)} . imagei ) . ({(s) . (f) . (tau) . (sigma)} . tofs ) . ({(b) . (f) . (tau) . (sigma)} . t2 ) . (f) . (tau) . (sigma)} . soft ) . (s) . (sigma)} . tris

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