mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-10-12 15:18:40 +00:00
Some basic sets (#94)
This commit is contained in:
Patrick Stevens
GitHub
@@ -84,6 +84,9 @@ open import Setoids.Lists
|
||||
open import Setoids.Orders
|
||||
open import Setoids.Functions.Definition
|
||||
open import Setoids.Functions.Extension
|
||||
open import Setoids.Algebra.Lemmas
|
||||
open import Setoids.Intersection.Lemmas
|
||||
open import Setoids.Union.Lemmas
|
||||
|
||||
open import Sets.Cardinality.Infinite.Examples
|
||||
open import Sets.Cardinality.Infinite.Lemmas
|
||||
|
||||
143
Functions.agda
143
Functions.agda
@@ -5,95 +5,96 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
open import LogicalFormulae
|
||||
|
||||
module Functions where
|
||||
Rel : {a b : _} → Set a → Set (a ⊔ lsuc b)
|
||||
Rel {a} {b} A = A → A → Set b
|
||||
|
||||
_∘_ : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (f : B → C) → (g : A → B) → (A → C)
|
||||
g ∘ f = λ a → g (f a)
|
||||
Rel : {a b : _} → Set a → Set (a ⊔ lsuc b)
|
||||
Rel {a} {b} A = A → A → Set b
|
||||
|
||||
Injection : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set (a ⊔ b)
|
||||
Injection {A = A} f = {x y : A} → (f x ≡ f y) → x ≡ y
|
||||
_∘_ : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (f : B → C) → (g : A → B) → (A → C)
|
||||
g ∘ f = λ a → g (f a)
|
||||
|
||||
Surjection : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set (a ⊔ b)
|
||||
Surjection {A = A} {B = B} f = (b : B) → Sg A (λ a → f a ≡ b)
|
||||
Injection : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set (a ⊔ b)
|
||||
Injection {A = A} f = {x y : A} → (f x ≡ f y) → x ≡ y
|
||||
|
||||
record Bijection {a b : _} {A : Set a} {B : Set b} (f : A → B) : Set (a ⊔ b) where
|
||||
field
|
||||
inj : Injection f
|
||||
surj : Surjection f
|
||||
Surjection : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set (a ⊔ b)
|
||||
Surjection {A = A} {B = B} f = (b : B) → Sg A (λ a → f a ≡ b)
|
||||
|
||||
record Invertible {a b : _} {A : Set a} {B : Set b} (f : A → B) : Set (a ⊔ b) where
|
||||
field
|
||||
inverse : B → A
|
||||
isLeft : (b : B) → f (inverse b) ≡ b
|
||||
isRight : (a : A) → inverse (f a) ≡ a
|
||||
record Bijection {a b : _} {A : Set a} {B : Set b} (f : A → B) : Set (a ⊔ b) where
|
||||
field
|
||||
inj : Injection f
|
||||
surj : Surjection f
|
||||
|
||||
invertibleImpliesBijection : {a b : _} {A : Set a} {B : Set b} {f : A → B} → Invertible f → Bijection f
|
||||
Bijection.inj (invertibleImpliesBijection {a} {b} {A} {B} {f} record { inverse = inverse ; isLeft = isLeft ; isRight = isRight }) {x} {y} fx=fy = ans
|
||||
where
|
||||
bl : inverse (f x) ≡ inverse (f y)
|
||||
bl = applyEquality inverse fx=fy
|
||||
ans : x ≡ y
|
||||
ans rewrite equalityCommutative (isRight x) | equalityCommutative (isRight y) = bl
|
||||
Bijection.surj (invertibleImpliesBijection {a} {b} {A} {B} {f} record { inverse = inverse ; isLeft = isLeft ; isRight = isRight }) y = (inverse y , isLeft y)
|
||||
record Invertible {a b : _} {A : Set a} {B : Set b} (f : A → B) : Set (a ⊔ b) where
|
||||
field
|
||||
inverse : B → A
|
||||
isLeft : (b : B) → f (inverse b) ≡ b
|
||||
isRight : (a : A) → inverse (f a) ≡ a
|
||||
|
||||
bijectionImpliesInvertible : {a b : _} {A : Set a} {B : Set b} {f : A → B} → Bijection f → Invertible f
|
||||
Invertible.inverse (bijectionImpliesInvertible record { inj = inj ; surj = surj }) b = underlying (surj b)
|
||||
Invertible.isLeft (bijectionImpliesInvertible {f = f} record { inj = inj ; surj = surj }) b with surj b
|
||||
Invertible.isLeft (bijectionImpliesInvertible {f = f} record { inj = inj ; surj = surj }) b | a , prop = prop
|
||||
Invertible.isRight (bijectionImpliesInvertible {f = f} record { inj = inj ; surj = surj }) a with surj (f a)
|
||||
Invertible.isRight (bijectionImpliesInvertible {f = f} record { inj = property ; surj = surj }) a | a₁ , b = property b
|
||||
invertibleImpliesBijection : {a b : _} {A : Set a} {B : Set b} {f : A → B} → Invertible f → Bijection f
|
||||
Bijection.inj (invertibleImpliesBijection {a} {b} {A} {B} {f} record { inverse = inverse ; isLeft = isLeft ; isRight = isRight }) {x} {y} fx=fy = ans
|
||||
where
|
||||
bl : inverse (f x) ≡ inverse (f y)
|
||||
bl = applyEquality inverse fx=fy
|
||||
ans : x ≡ y
|
||||
ans rewrite equalityCommutative (isRight x) | equalityCommutative (isRight y) = bl
|
||||
Bijection.surj (invertibleImpliesBijection {a} {b} {A} {B} {f} record { inverse = inverse ; isLeft = isLeft ; isRight = isRight }) y = (inverse y , isLeft y)
|
||||
|
||||
injComp : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Injection f → Injection g → Injection (g ∘ f)
|
||||
injComp {f = f} {g} propF propG pr = propF (propG pr)
|
||||
bijectionImpliesInvertible : {a b : _} {A : Set a} {B : Set b} {f : A → B} → Bijection f → Invertible f
|
||||
Invertible.inverse (bijectionImpliesInvertible record { inj = inj ; surj = surj }) b = underlying (surj b)
|
||||
Invertible.isLeft (bijectionImpliesInvertible {f = f} record { inj = inj ; surj = surj }) b with surj b
|
||||
Invertible.isLeft (bijectionImpliesInvertible {f = f} record { inj = inj ; surj = surj }) b | a , prop = prop
|
||||
Invertible.isRight (bijectionImpliesInvertible {f = f} record { inj = inj ; surj = surj }) a with surj (f a)
|
||||
Invertible.isRight (bijectionImpliesInvertible {f = f} record { inj = property ; surj = surj }) a | a₁ , b = property b
|
||||
|
||||
surjComp : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Surjection f → Surjection g → Surjection (g ∘ f)
|
||||
surjComp {f = f} {g} propF propG c with propG c
|
||||
surjComp {f = f} {g} propF propG c | b , pr with propF b
|
||||
surjComp {f = f} {g} propF propG c | b , pr | a , pr2 = a , pr'
|
||||
where
|
||||
pr' : g (f a) ≡ c
|
||||
pr' rewrite pr2 = pr
|
||||
injComp : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Injection f → Injection g → Injection (g ∘ f)
|
||||
injComp {f = f} {g} propF propG pr = propF (propG pr)
|
||||
|
||||
bijectionComp : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Bijection f → Bijection g → Bijection (g ∘ f)
|
||||
Bijection.inj (bijectionComp bijF bijG) = injComp (Bijection.inj bijF) (Bijection.inj bijG)
|
||||
Bijection.surj (bijectionComp bijF bijG) = surjComp (Bijection.surj bijF) (Bijection.surj bijG)
|
||||
surjComp : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Surjection f → Surjection g → Surjection (g ∘ f)
|
||||
surjComp {f = f} {g} propF propG c with propG c
|
||||
surjComp {f = f} {g} propF propG c | b , pr with propF b
|
||||
surjComp {f = f} {g} propF propG c | b , pr | a , pr2 = a , pr'
|
||||
where
|
||||
pr' : g (f a) ≡ c
|
||||
pr' rewrite pr2 = pr
|
||||
|
||||
compInjRightInj : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Injection (g ∘ f) → Injection f
|
||||
compInjRightInj {f = f} {g} property {x} {y} fx=fy = property (applyEquality g fx=fy)
|
||||
bijectionComp : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Bijection f → Bijection g → Bijection (g ∘ f)
|
||||
Bijection.inj (bijectionComp bijF bijG) = injComp (Bijection.inj bijF) (Bijection.inj bijG)
|
||||
Bijection.surj (bijectionComp bijF bijG) = surjComp (Bijection.surj bijF) (Bijection.surj bijG)
|
||||
|
||||
compSurjLeftSurj : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Surjection (g ∘ f) → Surjection g
|
||||
compSurjLeftSurj {f = f} {g} property b with property b
|
||||
compSurjLeftSurj {f = f} {g} property b | a , b1 = f a , b1
|
||||
compInjRightInj : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Injection (g ∘ f) → Injection f
|
||||
compInjRightInj {f = f} {g} property {x} {y} fx=fy = property (applyEquality g fx=fy)
|
||||
|
||||
injectionPreservedUnderExtensionalEq : {a b : _} {A : Set a} {B : Set b} {f g : A → B} → Injection f → ({x : A} → f x ≡ g x) → Injection g
|
||||
injectionPreservedUnderExtensionalEq {A = A} {B} {f} {g} property prop {x} {y} gx=gy = property (transitivity (prop {x}) (transitivity gx=gy (equalityCommutative (prop {y}))))
|
||||
compSurjLeftSurj : {a b c : _} {A : Set a} {B : Set b} {C : Set c} {f : A → B} {g : B → C} → Surjection (g ∘ f) → Surjection g
|
||||
compSurjLeftSurj {f = f} {g} property b with property b
|
||||
compSurjLeftSurj {f = f} {g} property b | a , b1 = f a , b1
|
||||
|
||||
surjectionPreservedUnderExtensionalEq : {a b : _} {A : Set a} {B : Set b} {f g : A → B} → Surjection f → ({x : A} → f x ≡ g x) → Surjection g
|
||||
surjectionPreservedUnderExtensionalEq {f = f} {g} surj ext b with surj b
|
||||
surjectionPreservedUnderExtensionalEq {f = f} {g} surj ext b | a , pr = a , transitivity (equalityCommutative ext) pr
|
||||
injectionPreservedUnderExtensionalEq : {a b : _} {A : Set a} {B : Set b} {f g : A → B} → Injection f → ({x : A} → f x ≡ g x) → Injection g
|
||||
injectionPreservedUnderExtensionalEq {A = A} {B} {f} {g} property prop {x} {y} gx=gy = property (transitivity (prop {x}) (transitivity gx=gy (equalityCommutative (prop {y}))))
|
||||
|
||||
bijectionPreservedUnderExtensionalEq : {a b : _} {A : Set a} {B : Set b} {f g : A → B} → Bijection f → ({x : A} → f x ≡ g x) → Bijection g
|
||||
Bijection.inj (bijectionPreservedUnderExtensionalEq record { inj = inj ; surj = surj } ext) = injectionPreservedUnderExtensionalEq inj ext
|
||||
Bijection.surj (bijectionPreservedUnderExtensionalEq record { inj = inj ; surj = surj } ext) = surjectionPreservedUnderExtensionalEq surj ext
|
||||
surjectionPreservedUnderExtensionalEq : {a b : _} {A : Set a} {B : Set b} {f g : A → B} → Surjection f → ({x : A} → f x ≡ g x) → Surjection g
|
||||
surjectionPreservedUnderExtensionalEq {f = f} {g} surj ext b with surj b
|
||||
surjectionPreservedUnderExtensionalEq {f = f} {g} surj ext b | a , pr = a , transitivity (equalityCommutative ext) pr
|
||||
|
||||
inverseIsInvertible : {a b : _} {A : Set a} {B : Set b} {f : A → B} → (inv : Invertible f) → Invertible (Invertible.inverse inv)
|
||||
Invertible.inverse (inverseIsInvertible {f = f} inv) = f
|
||||
Invertible.isLeft (inverseIsInvertible {f = f} inv) b = Invertible.isRight inv b
|
||||
Invertible.isRight (inverseIsInvertible {f = f} inv) a = Invertible.isLeft inv a
|
||||
bijectionPreservedUnderExtensionalEq : {a b : _} {A : Set a} {B : Set b} {f g : A → B} → Bijection f → ({x : A} → f x ≡ g x) → Bijection g
|
||||
Bijection.inj (bijectionPreservedUnderExtensionalEq record { inj = inj ; surj = surj } ext) = injectionPreservedUnderExtensionalEq inj ext
|
||||
Bijection.surj (bijectionPreservedUnderExtensionalEq record { inj = inj ; surj = surj } ext) = surjectionPreservedUnderExtensionalEq surj ext
|
||||
|
||||
id : {a : _} {A : Set a} → (A → A)
|
||||
id a = a
|
||||
inverseIsInvertible : {a b : _} {A : Set a} {B : Set b} {f : A → B} → (inv : Invertible f) → Invertible (Invertible.inverse inv)
|
||||
Invertible.inverse (inverseIsInvertible {f = f} inv) = f
|
||||
Invertible.isLeft (inverseIsInvertible {f = f} inv) b = Invertible.isRight inv b
|
||||
Invertible.isRight (inverseIsInvertible {f = f} inv) a = Invertible.isLeft inv a
|
||||
|
||||
idIsBijective : {a : _} {A : Set a} → Bijection (id {a} {A})
|
||||
Bijection.inj idIsBijective pr = pr
|
||||
Bijection.surj idIsBijective b = b , refl
|
||||
id : {a : _} {A : Set a} → (A → A)
|
||||
id a = a
|
||||
|
||||
functionCompositionExtensionallyAssociative : {a b c d : _} {A : Set a} {B : Set b} {C : Set c} {D : Set d} → (f : A → B) → (g : B → C) → (h : C → D) → (x : A) → (h ∘ (g ∘ f)) x ≡ ((h ∘ g) ∘ f) x
|
||||
functionCompositionExtensionallyAssociative f g h x = refl
|
||||
idIsBijective : {a : _} {A : Set a} → Bijection (id {a} {A})
|
||||
Bijection.inj idIsBijective pr = pr
|
||||
Bijection.surj idIsBijective b = b , refl
|
||||
|
||||
dom : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set a
|
||||
dom {A = A} f = A
|
||||
functionCompositionExtensionallyAssociative : {a b c d : _} {A : Set a} {B : Set b} {C : Set c} {D : Set d} → (f : A → B) → (g : B → C) → (h : C → D) → (x : A) → (h ∘ (g ∘ f)) x ≡ ((h ∘ g) ∘ f) x
|
||||
functionCompositionExtensionallyAssociative f g h x = refl
|
||||
|
||||
codom : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set b
|
||||
codom {B = B} f = B
|
||||
dom : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set a
|
||||
dom {A = A} f = A
|
||||
|
||||
codom : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set b
|
||||
codom {B = B} f = B
|
||||
|
||||
25
Setoids/Algebra/Lemmas.agda
Normal file
25
Setoids/Algebra/Lemmas.agda
Normal file
@@ -0,0 +1,25 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
open import LogicalFormulae
|
||||
open import Sets.EquivalenceRelations
|
||||
open import Setoids.Setoids
|
||||
|
||||
module Setoids.Algebra.Lemmas {a b : _} {A : Set a} (S : Setoid {a} {b} A) where
|
||||
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
open import Setoids.Subset S
|
||||
open import Setoids.Equality S
|
||||
open import Setoids.Intersection.Definition S
|
||||
open import Setoids.Union.Definition S
|
||||
|
||||
intersectionAndUnion : {c d e : _} {pred1 : A → Set c} {pred2 : A → Set d} {pred3 : A → Set e} → (s1 : subset pred1) (s2 : subset pred2) (s3 : subset pred3) → intersection s1 (union s2 s3) =S union (intersection s1 s2) (intersection s1 s3)
|
||||
intersectionAndUnion s1 s2 s3 x = ans1 ,, ans2
|
||||
where
|
||||
ans1 : _
|
||||
ans1 (fst ,, inl x) = inl (fst ,, x)
|
||||
ans1 (fst ,, inr x) = inr (fst ,, x)
|
||||
ans2 : _
|
||||
ans2 (inl x) = _&&_.fst x ,, inl (_&&_.snd x)
|
||||
ans2 (inr x) = _&&_.fst x ,, inr (_&&_.snd x)
|
||||
24
Setoids/Equality.agda
Normal file
24
Setoids/Equality.agda
Normal file
@@ -0,0 +1,24 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
open import LogicalFormulae
|
||||
open import Sets.EquivalenceRelations
|
||||
open import Setoids.Setoids
|
||||
|
||||
module Setoids.Equality {a b : _} {A : Set a} (S : Setoid {a} {b} A) where
|
||||
|
||||
open import Setoids.Subset S
|
||||
|
||||
_=S_ : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset pred1) (s2 : subset pred2) → Set _
|
||||
_=S_ {pred1 = pred1} {pred2} s1 s2 = (x : A) → (pred1 x → pred2 x) && (pred2 x → pred1 x)
|
||||
|
||||
setoidEqualitySymmetric : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} → (s1 : subset pred1) (s2 : subset pred2) → s1 =S s2 → s2 =S s1
|
||||
setoidEqualitySymmetric s1 s2 s1=s2 x = _&&_.snd (s1=s2 x) ,, _&&_.fst (s1=s2 x)
|
||||
|
||||
setoidEqualityTransitive : {c d e : _} {pred1 : A → Set c} {pred2 : A → Set d} {pred3 : A → Set e} (s1 : subset pred1) (s2 : subset pred2) (s3 : subset pred3) → s1 =S s2 → s2 =S s3 → s1 =S s3
|
||||
setoidEqualityTransitive s1 s2 s3 s1=s2 s2=s3 x with s1=s2 x
|
||||
setoidEqualityTransitive s1 s2 s3 s1=s2 s2=s3 x | p1top2 ,, p1top2' with s2=s3 x
|
||||
setoidEqualityTransitive s1 s2 s3 s1=s2 s2=s3 x | p1top2 ,, p1top2' | fst ,, snd = (λ i → fst (p1top2 i)) ,, λ i → p1top2' (snd i)
|
||||
|
||||
setoidEqualityReflexive : {c : _} {pred : A → Set c} (s : subset pred) → s =S s
|
||||
setoidEqualityReflexive s x = (λ x → x) ,, λ x → x
|
||||
18
Setoids/Intersection/Definition.agda
Normal file
18
Setoids/Intersection/Definition.agda
Normal file
@@ -0,0 +1,18 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
open import LogicalFormulae
|
||||
open import Sets.EquivalenceRelations
|
||||
open import Setoids.Setoids
|
||||
|
||||
module Setoids.Intersection.Definition {a b : _} {A : Set a} (S : Setoid {a} {b} A) where
|
||||
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
open import Setoids.Subset S
|
||||
|
||||
intersectionPredicate : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset pred1) (s2 : subset pred2) → A → Set (c ⊔ d)
|
||||
intersectionPredicate {pred1 = pred1} {pred2} s1 s2 a = pred1 a && pred2 a
|
||||
|
||||
intersection : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset pred1) (s2 : subset pred2) → subset (intersectionPredicate s1 s2)
|
||||
intersection s1 s2 {x1} {x2} x1=x2 (inS1 ,, inS2) = s1 x1=x2 inS1 ,, s2 x1=x2 inS2
|
||||
18
Setoids/Intersection/Lemmas.agda
Normal file
18
Setoids/Intersection/Lemmas.agda
Normal file
@@ -0,0 +1,18 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
open import LogicalFormulae
|
||||
open import Sets.EquivalenceRelations
|
||||
open import Setoids.Setoids
|
||||
open import Setoids.Subset
|
||||
|
||||
module Setoids.Intersection.Lemmas {a b : _} {A : Set a} (S : Setoid {a} {b} A) {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset S pred1) (s2 : subset S pred2) where
|
||||
|
||||
open import Setoids.Intersection.Definition S
|
||||
open import Setoids.Equality S
|
||||
|
||||
intersectionCommutative : intersection s1 s2 =S intersection s2 s1
|
||||
intersectionCommutative i = (λ t → _&&_.snd t ,, _&&_.fst t) ,, λ t → _&&_.snd t ,, _&&_.fst t
|
||||
|
||||
intersectionAssociative : {e : _} {pred3 : A → Set e} (s3 : subset S pred3) → intersection (intersection s1 s2) s3 =S intersection s1 (intersection s2 s3)
|
||||
intersectionAssociative s3 x = (λ pr → _&&_.fst (_&&_.fst pr) ,, (_&&_.snd (_&&_.fst pr) ,, _&&_.snd pr)) ,, λ z → (_&&_.fst z ,, _&&_.fst (_&&_.snd z)) ,, _&&_.snd (_&&_.snd z)
|
||||
19
Setoids/Union/Definition.agda
Normal file
19
Setoids/Union/Definition.agda
Normal file
@@ -0,0 +1,19 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
open import LogicalFormulae
|
||||
open import Sets.EquivalenceRelations
|
||||
open import Setoids.Setoids
|
||||
|
||||
module Setoids.Union.Definition {a b : _} {A : Set a} (S : Setoid {a} {b} A) where
|
||||
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
open import Setoids.Subset S
|
||||
|
||||
unionPredicate : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset pred1) (s2 : subset pred2) → A → Set (c ⊔ d)
|
||||
unionPredicate {pred1 = pred1} {pred2} s1 s2 a = pred1 a || pred2 a
|
||||
|
||||
union : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset pred1) (s2 : subset pred2) → subset (unionPredicate s1 s2)
|
||||
union s1 s2 {x1} {x2} x1=x2 (inl x) = inl (s1 x1=x2 x)
|
||||
union s1 s2 {x1} {x2} x1=x2 (inr x) = inr (s2 x1=x2 x)
|
||||
34
Setoids/Union/Lemmas.agda
Normal file
34
Setoids/Union/Lemmas.agda
Normal file
@@ -0,0 +1,34 @@
|
||||
{-# OPTIONS --safe --warning=error --without-K #-}
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
open import LogicalFormulae
|
||||
open import Sets.EquivalenceRelations
|
||||
open import Setoids.Setoids
|
||||
open import Setoids.Subset
|
||||
|
||||
module Setoids.Union.Lemmas {a b : _} {A : Set a} (S : Setoid {a} {b} A) {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset S pred1) (s2 : subset S pred2) where
|
||||
|
||||
open import Setoids.Union.Definition S
|
||||
open import Setoids.Equality S
|
||||
|
||||
unionCommutative : union s1 s2 =S union s2 s1
|
||||
unionCommutative i = ans1 ,, ans2
|
||||
where
|
||||
ans1 : unionPredicate s1 s2 i → unionPredicate s2 s1 i
|
||||
ans1 (inl x) = inr x
|
||||
ans1 (inr x) = inl x
|
||||
ans2 : unionPredicate s2 s1 i → unionPredicate s1 s2 i
|
||||
ans2 (inl x) = inr x
|
||||
ans2 (inr x) = inl x
|
||||
|
||||
unionAssociative : {e : _} {pred3 : A → Set e} (s3 : subset S pred3) → union (union s1 s2) s3 =S union s1 (union s2 s3)
|
||||
unionAssociative s3 x = ans1 ,, ans2
|
||||
where
|
||||
ans1 : unionPredicate (union s1 s2) s3 x → unionPredicate s1 (union s2 s3) x
|
||||
ans1 (inl (inl x)) = inl x
|
||||
ans1 (inl (inr x)) = inr (inl x)
|
||||
ans1 (inr x) = inr (inr x)
|
||||
ans2 : _
|
||||
ans2 (inl x) = inl (inl x)
|
||||
ans2 (inr (inl x)) = inl (inr x)
|
||||
ans2 (inr (inr x)) = inr x
|
||||
Reference in New Issue
Block a user