Last active
June 13, 2016 00:03
-
-
Save mietek/4b7b83068f3d7b59e0410b444b4b4ae5 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# OPTIONS --type-in-type #-} | |
module HoTTAczel where | |
open import Data.Bool using (Bool ; true ; false) | |
open import Data.Empty using (⊥ ; ⊥-elim) | |
open import Data.Product using (Σ ; _×_ ; _,_) renaming (proj₁ to π₁ ; proj₂ to π₂) | |
open import Data.Sum using (_⊎_) renaming (inj₁ to ι₁ ; inj₂ to ι₂) | |
open import Data.Unit using (⊤ ; tt) | |
open import Function using (id ; _∘_) | |
open import Level using (zero ; suc) | |
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) | |
open import Relation.Nullary using (¬_ ; Dec ; yes ; no) | |
open import Relation.Nullary.Negation using (contradiction) | |
-- Sets of Aczel’s constructive set theory. | |
-- “Menge” means “set” in German. | |
-- We use: | |
-- * uppercase Latin for types (A , B , C) | |
-- * lowercase Latin for inhabitants of types (x , y, z) | |
-- * lowercase Latin for functions from types to sets (f , g , h) | |
-- * lowercase Greek for sets (α , β , γ) | |
data Menge : Set₁ where | |
sup : (A : Set) (f : A → Menge) → Menge | |
-- Equality of α and β. | |
infix 5 _⫗_ | |
_⫗_ : (α β : Menge) → Set | |
(sup A f) ⫗ (sup B g) = (∀ (x : A) → Σ B (λ y → f x ⫗ g y)) × | |
(∀ (y : B) → Σ A (λ x → g y ⫗ f x)) | |
infix 5 _⫘_ | |
_⫘_ : (α β : Menge) → Set | |
α ⫘ β = ¬ α ⫗ β | |
⫗-refl : ∀ {α} → α ⫗ α | |
π₁ (⫗-refl {sup A f}) x = x , ⫗-refl | |
π₂ (⫗-refl {sup A f}) x = x , ⫗-refl | |
⫗-sym : ∀ {α β} → α ⫗ β → β ⫗ α | |
π₁ (⫗-sym {sup A f} {sup B g} (α▹β , β▹α)) y with β▹α y | |
… | x , gy⫗fx = x , gy⫗fx | |
π₂ (⫗-sym {sup A f} {sup B g} (α▹β , β▹α)) x with α▹β x | |
… | y , fx⫗gy = y , fx⫗gy | |
⫗-trans : ∀ {α β γ} → α ⫗ β → β ⫗ γ → α ⫗ γ | |
π₁ (⫗-trans {sup A f} {sup B g} {sup C h} (α▹β , β▹α) (β▹γ , γ▹β)) x with α▹β x | |
… | y , fx⫗gy with β▹γ y | |
… | z , gy⫗hz = z , ⫗-trans fx⫗gy gy⫗hz | |
π₂ (⫗-trans {sup A f} {sup B g} {sup C h} (α▹β , β▹α) (β▹γ , γ▹β)) z with γ▹β z | |
… | y , hz⫗gy with β▹α y | |
… | x , gy⫗fx = x , ⫗-trans hz⫗gy gy⫗fx | |
-- Membership of α in β. | |
infix 6 _∈_ | |
_∈_ : (α β : Menge) → Set | |
α ∈ sup B g = Σ B (λ y → α ⫗ g y) | |
infix 6 _∉_ | |
_∉_ : (α β : Menge) → Set | |
α ∉ β = ¬ α ∈ β | |
-- Inclusion of α in β. | |
infix 5 _⊆_ | |
_⊆_ : (α β : Menge) → Set₁ | |
α ⊆ β = ∀ {ξ : Menge} → ξ ∈ α → ξ ∈ β | |
infix 5 _⊇_ | |
_⊇_ : (α β : Menge) → Set₁ | |
α ⊇ β = β ⊆ α | |
⊆-refl : ∀ {α} → α ⊆ α | |
⊆-refl = id | |
⊆-trans : ∀ {α β γ} → α ⊆ β → β ⊆ γ → α ⊆ γ | |
⊆-trans α⊆β β⊆γ = β⊆γ ∘ α⊆β | |
⊆-antisym₁ : ∀ {α β} → α ⊆ β × β ⊆ α → α ⫗ β | |
π₁ (⊆-antisym₁ {sup A f} {sup B g} (α⊆β , β⊆α)) x = α⊆β (x , ⫗-refl) | |
π₂ (⊆-antisym₁ {sup A f} {sup B g} (α⊆β , β⊆α)) y = β⊆α (y , ⫗-refl) | |
⊆-antisym₂ : ∀ {α β} → α ⫗ β → α ⊆ β × β ⊆ α | |
π₁ (⊆-antisym₂ {sup A f} {sup B g} (α▹β , β▹α)) (x , ξ⫗fx) with α▹β x | |
… | y , fx⫗gy = y , ⫗-trans ξ⫗fx fx⫗gy | |
π₂ (⊆-antisym₂ {sup A f} {sup B g} (α▹β , β▹α)) (y , ξ⫗gy) with β▹α y | |
… | x , gy⫗fx = x , ⫗-trans ξ⫗gy gy⫗fx | |
-- The empty set. | |
∅ : Menge | |
∅ = sup ⊥ ⊥-elim | |
⊆-bot : ∀ {α} → ∅ ⊆ α | |
⊆-bot {sup A f} (() , ξ⫗↯) | |
-- A universal set would be inconsistent. | |
𝕌 : Menge | |
𝕌 = sup Menge id | |
⊆-top : ∀ {α} → α ⊆ 𝕌 | |
⊆-top {sup A f} {ξ} (x , ξ⫗fx) = ξ , ⫗-refl | |
-- Singleton sets. | |
⟨_⟩ : (α : Menge) → Menge | |
⟨ α ⟩ = sup ⊤ (λ { tt → α }) | |
-- Absolute complement of α. | |
∁_ : (α : Menge) → Menge | |
∁ (sup A f) = sup (Σ Menge (λ β → ∀ {x : A} → f x ⫘ β)) (λ { (β , fx⫘β) → β }) | |
∁-invol : ∀ {α} → ∁ ∁ α ⊇ α | |
∁-invol {sup A f} {sup B g} (x , β⫗fx) = | |
(sup B g , (λ { {sup C h , fx⫘γ} (γ▹β , β▹γ) → | |
let fx⫗β = ⫗-sym β⫗fx | |
in contradiction {!!} fx⫘γ })) , | |
(λ y → y , ⫗-refl) , | |
(λ y → y , ⫗-refl) | |
-- TODO | |
∁-invol′ : ∀ {α} → ∁ ∁ α ⊆ α | |
∁-invol′ {sup A f} {sup B g} ((sup C h , proj₂) , proj₃) = {!!} | |
∅-compl : ∁ ∅ ⫗ 𝕌 | |
∅-compl = {!!} | |
𝕌-compl : ∁ 𝕌 ⫗ ∅ | |
𝕌-compl = {!!} | |
-- TODO: Correct notation below. | |
-- Union of A and B. | |
infixl 7 _∪_ | |
_∪_ : (α β : Menge) → Menge | |
(sup A f) ∪ (sup B g) = sup (A ⊎ B) (λ { (ι₁ x) → f x ; (ι₂ y) → g y }) | |
∪-comm : ∀ {A B} → A ∪ B ⫗ B ∪ A | |
π₁ (∪-comm {sup A f} {sup B g}) (ι₁ x) = ι₂ x , ⫗-refl | |
π₁ (∪-comm {sup A f} {sup B g}) (ι₂ y) = ι₁ y , ⫗-refl | |
π₂ (∪-comm {sup A f} {sup B g}) (ι₁ y) = ι₂ y , ⫗-refl | |
π₂ (∪-comm {sup A f} {sup B g}) (ι₂ x) = ι₁ x , ⫗-refl | |
∪-assoc : ∀ {A B C} → (A ∪ B) ∪ C ⫗ A ∪ (B ∪ C) | |
π₁ (∪-assoc {sup A f} {sup B g} {sup C h}) (ι₁ (ι₁ x)) = ι₁ x , ⫗-refl | |
π₁ (∪-assoc {sup A f} {sup B g} {sup C h}) (ι₁ (ι₂ y)) = ι₂ (ι₁ y) , ⫗-refl | |
π₁ (∪-assoc {sup A f} {sup B g} {sup C h}) (ι₂ z) = ι₂ (ι₂ z) , ⫗-refl | |
π₂ (∪-assoc {sup A f} {sup B g} {sup C h}) (ι₁ x) = ι₁ (ι₁ x) , ⫗-refl | |
π₂ (∪-assoc {sup A f} {sup B g} {sup C h}) (ι₂ (ι₁ y)) = ι₁ (ι₂ y) , ⫗-refl | |
π₂ (∪-assoc {sup A f} {sup B g} {sup C h}) (ι₂ (ι₂ z)) = ι₂ z , ⫗-refl | |
∪-id₁ : ∀ {A} → A ∪ ∅ ⫗ A | |
π₁ (∪-id₁ {sup A f}) (ι₁ x) = x , ⫗-refl | |
π₁ (∪-id₁ {sup A f}) (ι₂ ()) | |
π₂ (∪-id₁ {sup A f}) x = ι₁ x , ⫗-refl | |
∪-id₂ : ∀ {A} → ∅ ∪ A ⫗ A | |
π₁ (∪-id₂ {sup A f}) (ι₁ ()) | |
π₁ (∪-id₂ {sup A f}) (ι₂ x) = x , ⫗-refl | |
π₂ (∪-id₂ {sup A f}) x = ι₂ x , ⫗-refl | |
-- ∪-compl : ∀ {A} → A ∪ ∁ A ⊆ 𝕌 | |
-- ∪-compl = {!!} | |
∪-idem : ∀ {A} → A ∪ A ⫗ A | |
π₁ (∪-idem {sup A f}) (ι₁ x) = x , ⫗-refl | |
π₁ (∪-idem {sup A f}) (ι₂ x) = x , ⫗-refl | |
π₂ (∪-idem {sup A f}) x = ι₁ x , ⫗-refl | |
-- ∪-dom : ∀ {A} → A ∪ 𝕌 ⫗ 𝕌 | |
-- ∪-dom = {!!} | |
∪-join-id : ∀ {A B} → A ⊆ A ∪ B | |
∪-join-id {sup A f} {sup B g} (x , ξ⫗fx) = ι₁ x , ξ⫗fx | |
∪-join-∘ : ∀ {A B C} → A ⊆ C → B ⊆ C → A ∪ B ⊆ C | |
∪-join-∘ {sup A f} {sup B g} {sup C h} A⊆C B⊆C (ι₁ x , ξ⫗fx) = A⊆C (x , ξ⫗fx) | |
∪-join-∘ {sup A f} {sup B g} {sup C h} A⊆C B⊆C (ι₂ y , ξ⫗gy) = B⊆C (y , ξ⫗gy) | |
-- Intersection of A and B. | |
infixl 7 _∩_ | |
_∩_ : (α β : Menge) → Menge | |
(sup A f) ∩ (sup B g) = sup (Σ A (λ x → Σ B (λ y → f x ⫗ g y))) | |
(λ { (x , y , fx⫗gy) → f x }) | |
--(sup A f) ∩ (sup B g) = sup (Σ (A × B) (λ { (x , y) → f x ⫗ g y })) | |
-- (λ { ((x , y) , fx⫗gy) → f x }) | |
∩-comm : ∀ {A B} → A ∩ B ⫗ B ∩ A | |
π₁ (∩-comm {sup A f} {sup B g}) (x , y , fx⫗gy) = (y , x , ⫗-sym fx⫗gy) , fx⫗gy | |
π₂ (∩-comm {sup A f} {sup B g}) (y , x , gy⫗fx) = (x , y , ⫗-sym gy⫗fx) , gy⫗fx | |
∩-assoc : ∀ {A B C} → (A ∩ B) ∩ C ⫗ A ∩ (B ∩ C) | |
π₁ (∩-assoc {sup A f} {sup B g} {sup C h}) ((x , y , fx⫗gy) , z , fx⫗hz) = {!!} , {!!} | |
π₂ (∩-assoc {sup A f} {sup B g} {sup C h}) (x , (y , z , gy⫗hz) , fx⫗**) = {!!} | |
-- π₁ (∩-assoc {sup A f} {sup B g} {sup C h}) ((x , y , fx⊆gy , gy⊆fx) , z , fx⊆hz , hz⊆fx) = {!!} | |
-- π₂ (∩-assoc {sup A f} {sup B g} {sup C h}) (x , (y , z , gy⊆hz , hz⊆gy) , fx⊆xxx , gy⊆fx) = {!!} | |
-- -- ∩-id₁ : ∀ {A} → A ∩ 𝕌 ⫗ A | |
-- -- ∩-id₁ = {!!} | |
-- -- ∩-id₂ : ∀ {A} → 𝕌 ∩ A ⫗ A | |
-- -- ∩-id₂ = {!!} | |
-- ∩-compl : ∀ {A} → A ∩ ∁ A ⫗ ∅ | |
-- ∩-compl = {!!} | |
-- ∩-idem : ∀ {A} → A ∩ A ⫗ A | |
-- ∩-idem = {!!} | |
-- ∩-dom : ∀ {A} → A ∩ ∅ ⫗ ∅ | |
-- ∩-dom = {!!} | |
-- ∩-meet-id : ∀ {A B} → A ∩ B ⊆ A | |
-- ∩-meet-id = {!!} | |
-- ∩-meet-∘ : ∀ {A B C} → A ⊇ C → B ⊇ C → A ∩ B ⊇ C | |
-- ∩-meet-∘ = {!!} | |
-- -- Additional union and intersection laws. | |
-- ∪-dist-∩ : ∀ {A B C} → A ∪ (B ∩ C) ⫗ (A ∪ B) ∩ (A ∪ C) | |
-- ∪-dist-∩ = {!!} | |
-- ∩-dist-∪ : ∀ {A B C} → A ∩ (B ∪ C) ⫗ (A ∩ B) ∪ (A ∩ C) | |
-- ∩-dist-∪ = {!!} | |
-- ∪-absorb-∩ : ∀ {A B} → A ∪ (A ∩ B) ⫗ A | |
-- ∪-absorb-∩ = {!!} | |
-- ∩-absorb-∪ : ∀ {A B} → A ∩ (A ∪ B) ⫗ A | |
-- ∩-absorb-∪ = {!!} | |
-- -- Additional union, intersection, and complement laws. | |
-- ∪-de-morgan : ∀ {A B} → ∁ (A ∪ B) ⫗ ∁ A ∩ ∁ B | |
-- ∪-de-morgan = {!!} | |
-- ∩-de-morgan : ∀ {A B} → ∁ (A ∩ B) ⊇ ∁ A ∪ ∁ B | |
-- ∩-de-morgan = {!!} | |
-- -- TODO | |
-- ∩-de-morgan′ : ∀ {A B} → ∁ (A ∩ B) ⊆ ∁ A ∪ ∁ B | |
-- ∩-de-morgan′ = {!!} | |
-- -- ∁-uniq : ∀ {A B} → A ∪ B ⫗ 𝕌 → A ∩ B ⫗ ∅ → B ⫗ ∁ A | |
-- -- ∁-uniq = {!!} | |
-- -- Relative complement of A in B, or set-theoretic difference of B and A. | |
-- infixl 7 _∖_ | |
-- _∖_ : V → V → V | |
-- A ∖ B = A ∩ ∁ B | |
-- open import Data.Nat | |
-- open import Agda.Builtin.FromNat | |
-- num : ℕ → V | |
-- num ℕ.zero = ∅ | |
-- num (ℕ.suc n) = num n ∪ ⟨ num n ⟩ | |
-- record ⊤' : Set₁ where | |
-- instance | |
-- V-number : Number V | |
-- V-number = record | |
-- { Constraint = λ _ → ⊤' | |
-- ; fromNat = λ n → num n | |
-- } | |
-- ⟦0,2⟧ : V | |
-- ⟦0,2⟧ = ⟨ 0 ⟩ ∪ ⟨ 2 ⟩ | |
-- ⟦0,1⟧ : V | |
-- ⟦0,1⟧ = ⟨ 0 ⟩ ∪ ⟨ 1 ⟩ | |
-- ⟦2,3⟧ : V | |
-- ⟦2,3⟧ = ⟨ 2 ⟩ ∪ ⟨ 3 ⟩ | |
-- ⟦⟦0,1⟧,⟦2,3⟧⟧ : V | |
-- ⟦⟦0,1⟧,⟦2,3⟧⟧ = ⟨ ⟦0,1⟧ ⟩ ∪ ⟨ ⟦2,3⟧ ⟩ | |
-- bad : ⟦0,2⟧ ⊆ ⟦⟦0,1⟧,⟦2,3⟧⟧ | |
-- bad (ι₁ tt) = (ι₁ tt , (λ())) | |
-- bad (ι₂ tt) = (ι₂ tt , (λ { (ι₁ (ι₁ ())) | |
-- ; (ι₁ (ι₂ tt)) → (ι₁ tt , λ()) | |
-- ; (ι₂ tt) → (ι₁ tt , (λ { (ι₁ ()) | |
-- ; (ι₂ tt) → ι₁ (ι₂ tt) , (λ()) | |
-- })) | |
-- })) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment