module CZF.AczelV where open import MLTT.MLTT data _×_ (A B : Set) : Set where _,_ : A → B → A × B V : Set V = W U T -- equality as bisimulation, cf isomorphism _≈_ : V → V → Set sup a v ≈ sup a' v' = ((i : T a) → Σ (T a') (λ i' → v i ≈ v' i')) × ((i' : T a') → Σ (T a) (λ i → v' i' ≈ v i)) -- sup a v = sup a' v' = (f : T a → T a') x (forall i : T a. v i ≈ v' (f i)) x -- (f' : T a' → T a) x (forall i' : T a'. v' i' ≈ v (f' i')) -- extensional membership _∈_ : V → V → Set u ∈ sup a v = Σ (T a) (λ i → u ≈ v i) ≈-refl : (u : V) → u ≈ u ≈-refl (sup a v) = ((λ i → i , ≈-refl (v i)) , (λ i → i , ≈-refl (v i))) ≈-sym : (u v : V) → u ≈ v → v ≈ u ≈-sym (sup a v) (sup a' v') (p , p') = (p' , p) {- Exercise: prove transitivity of ≈! Exercise: prove the axiom of extensionality _iff_ : Set → Set → Set A iff B = (A → B) × (B → A) extL : (x y z : V) → (x ≈ y) iff (z ∈ x → z ∈ y) -} ∅ : V ∅ = sup n₀ R₀ ∅-axiom : (x : V) → x ∈ ∅ → N₀ ∅-axiom c (() , v) _∪_ : V → V → V sup a b ∪ sup a' b' = sup (a ⊕ a') (D b b') -- Exercise: Prove the ∪-axiom: -- ∪-axiom : (a b c : V) → ((c ∈ (a ∪ b)) iff ((c ∈ a) + (c ∈ b))) -- ∪-axiom (sup a b) (sup a₁ b₁) c = ({!!} , {!!}) -- Exercise: prove that ∪ preserves ≈ -- Exercise: define disjoint union -- Exercise (hard): define the function space in V! -- Natural numbers: -- 0 = ∅ -- succ x = x ∪ { x } [_] : V → V [ a ] = sup n₁ (λ x → a) zeroV = ∅ succV : V → V succV x = x ∪ [ x ] oneV = [ zeroV ] ω : V ω = sup n (R ∅ (λ x y → succV y)) -- a bigger ordinal ω+ω : V ω+ω = sup (n ⊕ n) (D (R ∅ (λ x y → succV y)) (R ω (λ x y → succV y))) -- Unordered pairs: n₂ : U n₂ = n₁ ⊕ n₁ pairV : V → V → V -- unordered pair pairV a b = sup n₂ (D (λ _ → a) (λ _ → b))