# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1557663518 -32400
# Node ID 5ed16e2d8eb763f04fcee22fb430eb93e45a3f95
# Parent  cb014a103467f896522b42194b0d3b78624da80d
try to fix axiom of replacement

diff -r cb014a103467 -r 5ed16e2d8eb7 zf.agda
--- a/zf.agda	Sun May 12 11:08:17 2019 +0900
+++ b/zf.agda	Sun May 12 21:18:38 2019 +0900
@@ -30,15 +30,24 @@
 infixr  140 _∨_
 infixr  150 _⇔_
 
+record Func {n m : Level } (ZFSet : Set n) (_≈_ : Rel ZFSet m) : Set (n ⊔ suc m) where
+  field
+     Restrict : ZFSet 
+     rel : Rel ZFSet m
+     dom : ( y : ZFSet ) → ∀ { x : ZFSet } → rel x y
+     fun-eq : { x y z : ZFSet } →  ( rel  x  y  ∧ rel  x  z  ) → y ≈ z 
+
+open Func
+
+
 record IsZF {n m : Level }
      (ZFSet : Set n)
      (_∋_ : ( A x : ZFSet  ) → Set m)
-     (_≈_ : ( A B : ZFSet  ) → Set m)
+     (_≈_ : Rel ZFSet m)
      (∅  : ZFSet)
      (_×_ : ( A B : ZFSet  ) → ZFSet)
      (Union : ( A : ZFSet  ) → ZFSet)
      (Power : ( A : ZFSet  ) → ZFSet)
-     (Restrict : ( ZFSet → Set m ) → ZFSet)
      (infinite : ZFSet)
        : Set (suc (n ⊔ m)) where
   field
@@ -52,10 +61,12 @@
   A ∈ B = B ∋ A
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } → ∀{ A∋x : Set m } → Set m
   _⊆_ A B {x} {A∋x} = B ∋ x
+  Repl : ( ψ : ZFSet → Set m ) → Func ZFSet _≈_ 
+  Repl ψ = record { Restrict = {!!} ; rel = {!!} ; dom = {!!} ; fun-eq = {!!} }
   _∩_ : ( A B : ZFSet  ) → ZFSet
-  A ∩ B = Restrict ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
+  A ∩ B = Restrict ( Repl ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) )
   _∪_ : ( A B : ZFSet  ) → ZFSet
-  A ∪ B = Restrict ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) )
+  A ∪ B = Restrict ( Repl ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) )
   infixr  200 _∈_
   infixr  230 _∩_ _∪_
   infixr  220 _⊆_ 
@@ -71,10 +82,10 @@
      regularity : ∀( x : ZFSet  ) → ¬ (x ≈ ∅) → (  smaller x ∈ x ∧  ( smaller x  ∩ x  ≈ ∅ ) )
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
-     infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ Restrict ( λ y → x ≈ y )) ∈ infinite 
+     infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ Restrict ( Repl ( λ y → x ≈ y ))) ∈ infinite 
      -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
      -- this form looks like specification
-     replacement : ( ψ :  ZFSet → Set m ) → ( x : ZFSet  ) →  x  ∈  Restrict ψ  → ψ x
+     replacement : ( ψ : Func ZFSet _≈_ ) → ∀ ( y : ZFSet  ) →  ( y  ∈  Restrict ψ )  → {!!} -- dom ψ y 
 
 record ZF {n m : Level } : Set (suc (n ⊔ m)) where
   infixr  210 _×_
@@ -89,9 +100,8 @@
      _×_ : ( A B : ZFSet  ) → ZFSet
      Union : ( A : ZFSet  ) → ZFSet
      Power : ( A : ZFSet  ) → ZFSet
-     Restrict : ( ZFSet → Set m ) → ZFSet
      infinite : ZFSet
-     isZF : IsZF ZFSet _∋_ _≈_ ∅ _×_ Union Power Restrict infinite 
+     isZF : IsZF ZFSet _∋_ _≈_ ∅ _×_ Union Power infinite 
 
 module reguraliry-m {n m : Level } ( zf : ZF {m} {n} ) where
 
@@ -101,16 +111,15 @@
 
    _≈_ =  ZF._≈_ zf
    ZFSet =  ZF.ZFSet 
-   Restrict =  ZF.Restrict  zf
    ∅ =  ZF.∅ zf
    _∩_ =  ( IsZF._∩_  ) (ZF.isZF zf)
    _∋_ =   ZF._∋_  zf
    replacement =   IsZF.replacement  ( ZF.isZF zf )
 
-   russel : ( x : ZFSet zf ) → x ≈ Restrict ( λ x → ¬ ( x ∋ x ) ) → ⊥
-   russel x eq with  x ∋ x 
-   ... | x∋x  with replacement ( λ x → ¬ ( x ∋ x )) x {!!}
-   ... | r1 = {!!}
+--   russel : ( x : ZFSet zf ) → x ≈ Restrict ( λ x → ¬ ( x ∋ x ) ) → ⊥
+--   russel x eq with  x ∋ x 
+--   ... | x∋x  with replacement ( λ x → ¬ ( x ∋ x )) x {!!}
+--   ... | r1 = {!!}