Skip to content

Instantly share code, notes, and snippets.

@mietek
Last active June 13, 2016 00:03
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mietek/4b7b83068f3d7b59e0410b444b4b4ae5 to your computer and use it in GitHub Desktop.
Save mietek/4b7b83068f3d7b59e0410b444b4b4ae5 to your computer and use it in GitHub Desktop.
{-# 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