Theory "simpleSetCat"

Parents cardinal

Signature

Constant	Type
Delta	:(α -> bool) -> α -> α -> bool
Gr	:(α -> β) -> (α -> bool) -> α -> β -> bool
RIMAGE	:(α -> β) -> (α -> bool) -> (α -> α -> bool) -> β -> β -> bool
RINV_IMAGE	:(α -> β) -> (α -> bool) -> (β -> β -> bool) -> α -> α -> bool
SPO	:(γ -> bool) -> (α -> bool) -> (β -> bool) -> (γ -> α) -> (γ -> β) -> ((α + β -> bool) -> bool) # (α -> α + β -> bool) # (β -> α + β -> bool)
SPO_pimg	:(α -> bool) -> (α -> β) -> (α -> γ) -> β + γ -> α -> bool
SPOr	:(γ -> bool) -> (γ -> α) -> (γ -> β) -> α + β -> α + β -> bool
Spushout	:(α -> bool) -> (β -> bool) -> (γ -> bool) -> (α -> β) -> (α -> γ) -> (π -> bool) # (β -> π) # (γ -> π) -> δ itself -> bool
cardgt	:α itself -> num -> bool
eps	:(α -> α -> bool) -> (α -> bool) -> α -> α -> bool
kernel	:(α -> bool) -> (α -> β) -> α -> α -> bool
restr	:(α -> β) -> (α -> bool) -> α -> β
shom	:(α -> β) -> (α -> bool) -> (β -> bool) -> bool
span	:(α -> bool) -> (α -> β) -> (α -> γ) -> β -> γ -> bool

Definitions

Delta_def

⊢ ∀V a b. Δ V a b ⇔ (a = b) ∧ a ∈ V

Gr_def

⊢ ∀h A a b. Gr h A a b ⇔ a ∈ A ∧ (b = h a)

RIMAGE_def

⊢ ∀f A R x y.
    RIMAGE f A R x y ⇔
    ∃x0 y0. (x = f x0) ∧ (y = f y0) ∧ R x0 y0 ∧ x0 ∈ A ∧ y0 ∈ A

RINV_IMAGE_def

⊢ ∀f A R x y. RINV_IMAGE f A R x y ⇔ x ∈ A ∧ y ∈ A ∧ R (f x) (f y)

SPO_def

⊢ ∀A B C f g.
    SPO A B C f g =
    (partition (SPOr A f g) (B ⊔ C),
     (λb. {a | a ∈ B ⊔ C ∧ SPOr A f g (INL b) a})⟨B⟩,
     (λc. {a | a ∈ B ⊔ C ∧ SPOr A f g (INR c) a})⟨C⟩)

SPO_pimg_def

⊢ (∀A f g x. SPO_pimg A f g (INL x) = PREIMAGE f {x} ∩ A) ∧
  ∀A f g y. SPO_pimg A f g (INR y) = PREIMAGE g {y} ∩ A

SPOr_def

⊢ ∀A f g.
    SPOr A f g =
    (λx y. (∃a. a ∈ A ∧ (x = INL (f a)) ∧ (y = INR (g a))) ∨ (x = y))^=

cardgt_def

⊢ ∀n. cardgt (:α) n ⇔ FINITE 𝕌(:α) ⇒ n < CARD 𝕌(:α)

eps_def

⊢ ∀R A a. eps R A a = if a ∈ A then {b | R a b ∧ b ∈ A} else ARB

kernel_def

⊢ ∀A f x y. kernel A f x y ⇔ x ∈ A ∧ y ∈ A ∧ (f x = f y)

restr_def

⊢ ∀f s. f⟨s⟩ = (λx. if x ∈ s then f x else ARB)

shom_def

⊢ ∀f A B. shom f A B ⇔ (∀a. a ∈ A ⇒ f a ∈ B) ∧ ∀a. a ∉ A ⇒ (f a = ARB)

span_def

⊢ ∀A f g b d. span A f g b d ⇔ ∃a. a ∈ A ∧ (b = f a) ∧ (d = g a)

Theorems

Delta_IMAGE

⊢ Δ (IMAGE f A) = RIMAGE f A (Δ A)

Delta_INTER

⊢ Δ (s ∩ t) = Δ s ∩ᵣ Δ t

Gr_Id

⊢ Gr (λx. x) A = Δ A

Gr_restr

⊢ Gr f⟨A⟩ A = Gr f A

IN_UNCURRY

⊢ (a,b) ∈ Rᴾ ⇔ R a b

RIMAGE_Gr

⊢ RIMAGE f A R = Gr f A ∘ᵣ R ∘ᵣ (Gr f A)ᵀ

RINV_IMAGE_Gr

⊢ RINV_IMAGE f A R = (Gr f A)ᵀ ∘ᵣ R ∘ᵣ Gr f A

SPOr_REFL

⊢ SPOr A f g x x

SPOr_lemma

⊢ ((j1 ∘ f)⟨A⟩ = (j2 ∘ g)⟨A⟩) ⇒
  (∀b1 b2. SPOr A f g (INL b1) (INL b2) ⇒ (j1 b1 = j1 b2)) ∧
  (∀b c. SPOr A f g (INL b) (INR c) ⇒ (j1 b = j2 c)) ∧
  (∀b' c'. SPOr A f g (INR c') (INL b') ⇒ (j1 b' = j2 c')) ∧
  ∀c1 c2. SPOr A f g (INR c1) (INR c2) ⇒ (j2 c1 = j2 c2)

Spushout_def

⊢ Spushout A B C' f g (P,i1,i2) (:δ) ⇔
  shom f A B ∧ shom g A C' ∧ shom i1 B P ∧ shom i2 C' P ∧
  ((i1 ∘ f)⟨A⟩ = (i2 ∘ g)⟨A⟩) ∧
  ∀Q j1 j2.
    shom j1 B Q ∧ shom j2 C' Q ∧ ((j1 ∘ f)⟨A⟩ = (j2 ∘ g)⟨A⟩) ⇒
    ∃!u. shom u P Q ∧ ((u ∘ i1)⟨B⟩ = j1) ∧ ((u ∘ i2)⟨C'⟩ = j2)

Spushout_ind

⊢ ∀P'.
    (∀A B C f g P i1 i2. P' A B C f g (P,i1,i2) (:δ)) ⇒
    ∀v v1 v2 v3 v4 v5 v6 v7 v8. P' v v1 v2 v3 v4 (v5,v6,v7) v8

Spushout_quotient

⊢ shom f A B ∧ shom g A C ⇒ Spushout A B C f g (SPO A B C f g) (:δ)

Spushout_sym

⊢ Spushout A B C f g (P,p1,p2) (:δ) ⇒ Spushout A C B g f (P,p2,p1) (:δ)

Spushout_transfer

⊢ Spushout A B C f g (P,i1,i2) (:δ) ∧ INJ h 𝕌(:ε) 𝕌(:δ) ⇒
  Spushout A B C f g (P,i1,i2) (:ε)

Spushouts_iso

⊢ Spushout A B C f g (P,i1,i2) (:ε) ∧ Spushout A B C f g (Q,j1,j2) (:δ) ∧
  cardgt (:δ) 1 ∧ cardgt (:ε) 1 ⇒
  ∃H. BIJ H P Q ∧ ((H ∘ i1)⟨B⟩ = j1) ∧ ((H ∘ i2)⟨C⟩ = j2)

cardgt0

⊢ cardgt (:α) 0

cardgt1_INJ_bool

⊢ cardgt (:α) 1 ⇔ ∃bf. INJ bf {T; F} 𝕌(:α)

eps_partition

⊢ a ∈ A ⇒ eps R A a ∈ partition R A

kernel_graph

⊢ kernel A f = (Gr f A)ᵀ ∘ᵣ Gr f A

oID

⊢ (f ∘ (λx. x) = f) ∧ ((λx. x) ∘ f = f)

restr_EMPTY

⊢ f⟨∅⟩ = K ARB

restr_applies

⊢ x ∈ A ⇒ (f⟨A⟩ x = f x)

restr_cases

⊢ (f⟨A⟩ x = g x) ⇔ x ∈ A ∧ (f x = g x) ∨ x ∉ A ∧ (g x = ARB)

restr_restr_o

⊢ (f ∘ g⟨A⟩)⟨A⟩ = (f ∘ g)⟨A⟩

shom_into_EMPTY

⊢ shom f A ∅ ⇔ (A = ∅) ∧ (f = K ARB)

shom_outof_EMPTY

⊢ shom f ∅ A ⇔ (f = K ARB)

shoms_exist

⊢ ∀A B. B ≠ ∅ ⇒ ∃h. shom h A B

symmetric_SPOr

⊢ symmetric (SPOr A f g)

transitive_SPOr

⊢ transitive (SPOr A f g)

unit_pushout

⊢ shom f A B ∧ shom g A C ∧ A ≠ ∅ ⇒
  Spushout A B C f g ({()},(K ())⟨B⟩,(K ())⟨C⟩) (:unit)