Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison cardinal.agda @ 272:985a1af11bce

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate ordered pair and Boolean Algebra
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 31 Dec 2019 11:22:52 +0900
parents 63df67b6281c
children 29a85a427ed2
comparison
equal deleted inserted replaced
271:2169d948159b 272:985a1af11bce
96 onto-iso : {y : Ordinal } → (lty : def Y y ) → 96 onto-iso : {y : Ordinal } → (lty : def Y y ) →
97 func-1 ( od→func {X} {Y} {xmap} xfunc ) ( func-1 (od→func yfunc) y ) ≡ y 97 func-1 ( od→func {X} {Y} {xmap} xfunc ) ( func-1 (od→func yfunc) y ) ≡ y
98 98
99 open Onto 99 open Onto
100 100
101 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z 101 onto-restrict : {X Y Z : OD} → Onto X Y → Z ⊆ Y → Onto X Z
102 onto-restrict {X} {Y} {Z} onto Z⊆Y = record { 102 onto-restrict {X} {Y} {Z} onto Z⊆Y = record {
103 xmap = xmap1 103 xmap = xmap1
104 ; ymap = zmap 104 ; ymap = zmap
105 ; xfunc = xfunc1 105 ; xfunc = xfunc1
106 ; yfunc = zfunc 106 ; yfunc = zfunc