Theory coalgAxioms

[oracles: ] [axioms: mapID] [] ⊢ mapF (λx. x) = (λa. a)

[oracles: ] [axioms: mapO] [] ⊢ mapF f ∘ mapF g = mapF (f ∘ g)

[oracles: ] [axioms: map_CONG] []
⊢ ∀f g y. (∀x. x ∈ setF y ⇒ f x = g x) ⇒ mapF f y = mapF g y

[oracles: ] [axioms: relO] [] ⊢ relF R ∘ᵣ relF S ⊆ᵣ relF (R ∘ᵣ S)

[oracles: ] [axioms: set_map] [] ⊢ setF ∘ mapF f = IMAGE f ∘ setF

⊢ ∀A. Fset A = {af | setF af ⊆ A}

⊢ ∀R A af B bf.
    bisim R (A,af) (B,bf) ⇔
    system (A,af) ∧ system (B,bf) ∧
    ∀a b. R a b ⇒ a ∈ A ∧ b ∈ B ∧ relF R (af a) (bf b)

⊢ ∀As Bs. bisimilar As Bs ⇔ ∃R. bisim R As Bs

⊢ ∀A af R.
    bquot (A,af) R =
    (partition R A,(λap. mapF (eps R A) (af (CHOICE ap)))⟨partition R A⟩)

⊢ ∀A af x y. gbisim (A,af) x y ⇔ ∃R. bisim R (A,af) (A,af) ∧ R x y

⊢ ∀As X. genS As X = BIGINTER {V | subsystem V As ∧ X ⊆ V}

⊢ ∀h A af B bf.
    hom h (A,af) (B,bf) ⇔
    system (A,af) ∧ system (B,bf) ∧
    (∀a. a ∈ A ⇒ h a ∈ B ∧ bf (h a) = mapF h (af a)) ∧
    ∀a. a ∉ A ⇒ h a = ARB

⊢ ∀A af B bf.
    iso (A,af) (B,bf) ⇔
    ∃f g.
      hom f (A,af) (B,bf) ∧ hom g (B,bf) (A,af) ∧
      (∀a. a ∈ A ⇒ g (f a) = a) ∧ ∀b. b ∈ B ⇒ f (g b) = b

⊢ ∀R x y. relF R x y ⇔ ∃z. setF z ⊆ Rᴾ ∧ mapF FST z = x ∧ mapF SND z = y

⊢ ∀A. simple A ⇔ ∀R. bisim R A A ⇒ ∀x y. R x y ⇒ x = y

⊢ ∀V A af.
    subsystem V (A,af) ⇔
    system (A,af) ∧ V ⊆ A ∧ ∃vf. hom (λx. x)⟨V⟩ (V,vf) (A,af)

⊢ ∀A af.
    system (A,af) ⇔ (∀a. a ∈ A ⇒ af a ∈ Fset A) ∧ ∀a. a ∉ A ⇒ af a = ARB

[oracles: DISK_THM] [axioms: mapO, mapID, map_CONG] []
⊢ hom f (A,af) (B,bf) ∧ BIJ f A B ⇒ iso (A,af) (B,bf)

⊢ Fpushout (A,af) (B,bf) (C',cf) f g ((P,pf),i1,i2) (:δ) ⇔
  hom f (A,af) (B,bf) ∧ hom g (A,af) (C',cf) ∧ hom i1 (B,bf) (P,pf) ∧
  hom i2 (C',cf) (P,pf) ∧ (i1 ∘ f)⟨A⟩ = (i2 ∘ g)⟨A⟩ ∧
  ∀Q qf j1 j2.
    hom j1 (B,bf) (Q,qf) ∧ hom j2 (C',cf) (Q,qf) ∧
    (j1 ∘ f)⟨A⟩ = (j2 ∘ g)⟨A⟩ ⇒
    ∃!u. hom u (P,pf) (Q,qf) ∧ (u ∘ i1)⟨B⟩ = j1 ∧ (u ∘ i2)⟨C'⟩ = j2

⊢ ∀P'.
    (∀A af B bf C cf f g P pf i1 i2.
       P' (A,af) (B,bf) (C,cf) f g ((P,pf),i1,i2) (:δ)) ⇒
    ∀v v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12.
      P' (v,v1) (v2,v3) (v4,v5) v6 v7 ((v8,v9),v10,v11) v12

⊢ hom f (A,af) (B,bf) ∧ INJ f A B ⇒
  ∀C cf g h.
    hom g (C,cf) (A,af) ∧ hom h (C,cf) (A,af) ∧ f ∘ g = f ∘ h ⇒ g = h

⊢ hom f (A,af) (B,bf) ∧ SURJ f A B ⇒ epi f (A,af) (B,bf) (:γ)

⊢ system (𝕌(:α),af)

⊢ bisim R1 As Bs ∧ bisim R2 As Bs ⇒ bisim (R1 ∪ᵣ R2) As Bs

⊢ system (A,af) ⇒ bisim (gbisim (A,af)) (A,af) (A,af)

⊢ bisim R As Bs ⇒ system As ∧ system Bs

[oracles: DISK_THM] [axioms: mapID, relO, mapO, set_map, map_CONG] []
⊢ bisimilar equiv_on system

[oracles: DISK_THM] [axioms: relO, mapO, set_map, map_CONG] []
⊢ bisim R (A,af) (B,bf) ∧ bisim Q (B,bf) (C,cf) ⇒
  bisim (Q ∘ᵣ R) (A,af) (C,cf)

⊢ bounded (:α) (:β) ⇔
  ∀a A af. system (A,af) ∧ a ∈ A ⇒ ∃f V. INJ f (genS (A,af) {a}) V

⊢ ∀P. P (:α) (:β) ⇒ ∀v v1. P v v1

[oracles: DISK_THM] [axioms: mapO, set_map, map_CONG] []
⊢ system (A,af) ∧ bisim R (A,af) (A,af) ∧ R equiv_on A ⇒
  ∃Rf.
    coequalizer (Rᴾ,Rf) (A,af) FST⟨Rᴾ⟩ SND⟨Rᴾ⟩ (bquot (A,af) R,eps R A)
      (:δ)

[oracles: DISK_THM] [axioms: set_map, mapO, map_CONG] []
⊢ system (A,af) ∧ bisim R (A,af) (A,af) ∧ R equiv_on A ⇒
  system (bquot (A,af) R) ∧ hom (eps R A) (A,af) (bquot (A,af) R)

⊢ coequalizer (A,af) (B,bf) f1 f2 ((C',cf),g) (:δ) ⇔
  hom f1 (A,af) (B,bf) ∧ hom f2 (A,af) (B,bf) ∧ hom g (B,bf) (C',cf) ∧
  (g ∘ f1)⟨A⟩ = (g ∘ f2)⟨A⟩ ∧
  ∀h D df.
    hom h (B,bf) (D,df) ∧ (h ∘ f1)⟨A⟩ = (h ∘ f2)⟨A⟩ ⇒
    ∃!u. hom u (C',cf) (D,df) ∧ h = (u ∘ g)⟨B⟩

⊢ ∀P. (∀A af B bf f1 f2 C cf g. P (A,af) (B,bf) f1 f2 ((C,cf),g) (:δ)) ⇒
      ∀v v1 v2 v3 v4 v5 v6 v7 v8 v9. P (v,v1) (v2,v3) v4 v5 ((v6,v7),v8) v9

⊢ coequalizer (A,af) (B,bf) f1 f2 (Cs,g) (:δ) ⇔
  hom f1 (A,af) (B,bf) ∧ hom f2 (A,af) (B,bf) ∧ hom g (B,bf) Cs ∧
  (g ∘ f1)⟨A⟩ = (g ∘ f2)⟨A⟩ ∧
  ∀h D df.
    hom h (B,bf) (D,df) ∧ (h ∘ f1)⟨A⟩ = (h ∘ f2)⟨A⟩ ⇒
    ∃!u. hom u Cs (D,df) ∧ h = (u ∘ g)⟨B⟩

[oracles: DISK_THM] [axioms: mapID, map_CONG] []
⊢ epi f (A,af) (B,bf) (:γ) ⇔
  Fpushout (A,af) (B,bf) (B,bf) f f ((B,bf),(λx. x)⟨B⟩,(λx. x)⟨B⟩) (:γ)

⊢ epi f (A,af) (B,bf) (:γ) ⇔
  hom f (A,af) (B,bf) ∧
  ∀C cf g h.
    hom g (B,bf) (C,cf) ∧ hom h (B,bf) (C,cf) ∧ (g ∘ f)⟨A⟩ = (h ∘ f)⟨A⟩ ⇒
    g = h

⊢ ∀P. (∀f A af B bf. P f (A,af) (B,bf) (:γ)) ⇒
      ∀v v1 v2 v3 v4 v5. P v (v1,v2) (v3,v4) v5

[oracles: DISK_THM] [axioms: mapID, relO, mapO, set_map, map_CONG] []
⊢ system (A,af) ⇒ gbisim (A,af) equiv_on A

[oracles: DISK_THM] [axioms: set_map, mapO, mapID, map_CONG] []
⊢ system (A,af) ∧ X ⊆ A ⇒ subsystem (genS (A,af) X) (A,af)

[oracles: DISK_THM] [axioms: mapID, map_CONG] []
⊢ system (A,af) ⇒ hom (λx. x)⟨A⟩ (A,af) (A,af)

⊢ hom f (A,af) Bs ⇒ f⟨A⟩ = f

⊢ hom f (A,af) (B,bf) ⇒ shom f A B

[oracles: DISK_THM] [axioms: mapO, map_CONG] []
⊢ hom f As Bs ∧ hom g Bs Cs ⇒ hom (g ∘ f)⟨FST As⟩ As Cs

⊢ iso As Bs ⇔ iso Bs As

[oracles: DISK_THM] [axioms: mapO, map_CONG] []
⊢ iso (A,af) (B,bf) ∧ hom h (A,af) (C,cf) ∧ INJ h A C ⇒
  ∃j. hom j (B,bf) (C,cf) ∧ INJ j B C

[oracles: DISK_THM] [axioms: mapO] []
⊢ hom (h ∘ g) (A,af) (C,cf) ∧ hom g (A,af) (B,bf) ∧ SURJ g A B ∧
  (∀b. b ∉ B ⇒ h b = ARB) ⇒
  hom h (B,bf) (C,cf)

[oracles: DISK_THM] [axioms: set_map, map_CONG, mapID, mapO] []
⊢ hom (h ∘ g) (A,af) (C,cf) ∧ hom h (B,bf) (C,cf) ∧ (∀a. a ∈ A ⇒ g a ∈ B) ∧
  (∀a. a ∉ A ⇒ g a = ARB) ∧ INJ h B C ⇒
  hom g (A,af) (B,bf)

[oracles: DISK_THM] [axioms: set_map, mapO] []
⊢ hom f (A,af) (B,bf) ∧ hom g (A,af) (C,cf) ⇒
  bisim (span A f g) (B,bf) (C,cf)

[oracles: DISK_THM] [axioms: mapO] []
⊢ ∀x. mapF f (mapF g x) = mapF (f ∘ g) x

[oracles: DISK_THM] [axioms: set_map, map_CONG, mapID, mapO] []
⊢ INJ f A B ⇒ INJ (mapF f) (Fset A) (Fset B)

[oracles: DISK_THM] [axioms: set_map] []
⊢ (∀a. a ∈ A ⇒ f a ∈ B) ⇒ ∀af. af ∈ Fset A ⇒ mapF f af ∈ Fset B

[oracles: DISK_THM] [axioms: mapO, set_map, mapID, map_CONG] []
⊢ system (A,af) ⇒ bisim (Δ A) (A,af) (A,af)

[oracles: DISK_THM] [axioms: relO, set_map, mapID, mapO, map_CONG] []
⊢ hom f (A,af) (B,bf) ⇒
  bisim (kernel A f) (A,af) (A,af) ∧ kernel A f equiv_on A

[oracles: DISK_THM] [axioms: set_map, mapO, map_CONG] []
⊢ system (A,af) ∧ bisim R (A,af) (A,af) ∧ R equiv_on A ⇒
  system (bquot (A,af) R) ∧ hom (eps R A) (A,af) (bquot (A,af) R)

[oracles: DISK_THM] [axioms: mapID, relO, mapO, set_map, map_CONG] []
⊢ hom f⟨A⟩ (A,af) (B,bf) ∧ bisim R (A,af) (A,af) ⇒
  bisim (RIMAGE f A R) (B,bf) (B,bf)

[oracles: DISK_THM] [axioms: mapID, relO, mapO, set_map, map_CONG] []
⊢ hom f⟨A⟩ (A,af) (B,bf) ∧ bisim Q (B,bf) (B,bf) ⇒
  bisim (RINV_IMAGE f A Q) (A,af) (A,af)

[oracles: DISK_THM] [axioms: mapID, map_CONG] []
⊢ V ⊆ A ∧ hom (λx. x)⟨V⟩ (V,kf) (A,af) ∧ hom (λx. x)⟨V⟩ (V,lf) (A,af) ⇒
  kf = lf

[oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
⊢ system (A,af) ⇒ (subsystem V (A,af) ⇔ V ⊆ A ∧ bisim (Δ V) (A,af) (A,af))

[oracles: DISK_THM] [axioms: map_CONG, set_map, mapO, mapID] []
⊢ relF $= = $=

[oracles: DISK_THM] [axioms: mapO, set_map, map_CONG] []
⊢ relF Rᵀ x y ⇔ relF R y x

[oracles: DISK_THM] [axioms: relO, mapO, set_map, map_CONG] []
⊢ relF R ∘ᵣ relF S = relF (R ∘ᵣ S)

⊢ (∀a b. R a b ⇒ S a b) ⇒ ∀A B. relF R A B ⇒ relF S A B

[oracles: DISK_THM] [axioms: map_CONG] []
⊢ bisim R (A,af) (B,bf) ⇔
  ∃Rf. hom FST⟨Rᴾ⟩ (Rᴾ,Rf) (A,af) ∧ hom SND⟨Rᴾ⟩ (Rᴾ,Rf) (B,bf)

[oracles: DISK_THM] [axioms: set_map] []
⊢ ∀x x'. x' ∈ setF (mapF f x) ⇔ ∃x''. x' = f x'' ∧ x'' ∈ setF x

[oracles: DISK_THM] [axioms: mapID, relO, mapO, set_map, map_CONG] []
⊢ simple As ⇔ ∀R. bisim R As As ∧ R equiv_on FST As ⇒ R = Δ (FST As)

[oracles: DISK_THM] [axioms: set_map, mapO] []
⊢ simple As ⇒ ∀Bs f g. hom f Bs As ∧ hom g Bs As ⇒ f = g

[oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
⊢ subsystem V (A,af) ⇔
  V ⊆ A ∧ system (A,af) ∧ hom (λx. x)⟨V⟩ (V,af⟨V⟩) (A,af)

[oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
⊢ system (A,af) ∧ (∀V. V ∈ VS ⇒ subsystem V (A,af)) ∧ VS ≠ ∅ ⇒
  subsystem (BIGINTER VS) (A,af)

[oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
⊢ system (A,af) ∧ subsystem V1 (A,af) ∧ subsystem V2 (A,af) ⇒
  subsystem (V1 ∩ V2) (A,af)

[oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
⊢ system (A,af) ∧ (∀V. V ∈ VS ⇒ subsystem V (A,af)) ⇒
  subsystem (BIGUNION VS) (A,af)

[oracles: DISK_THM] [axioms: mapID, map_CONG] []
⊢ system (A,af) ⇒ subsystem A (A,af)

[oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
⊢ subsystem V (A,af) ⇒ system (V,af⟨V⟩)

⊢ system (A,af) ⇒ ∀a b. a ∈ A ∧ b ∈ setF (af a) ⇒ b ∈ A

[oracles: DISK_THM] [axioms: set_map, mapID, mapO, map_CONG] []
⊢ hom h (A,af) (B,bf) ⇔
  (∀a. a ∈ A ⇒ h a ∈ B) ∧ (∀a. a ∉ A ⇒ h a = ARB) ∧
  bisim (Gr h A) (A,af) (B,bf)

[oracles: DISK_THM] [axioms: mapO, set_map, map_CONG] []
⊢ bisim Rᵀ Bs As ⇔ bisim R As Bs

[oracles: DISK_THM] [axioms: relO, mapO, set_map, map_CONG] []
⊢ bisim R (A,af) (B,bf) ∧ bisim Q (B,bf) (C,cf) ⇒
  bisim (Q ∘ᵣ R) (A,af) (C,cf)

⊢ (∀R. R ∈ Rs ⇒ bisim R As Bs) ∧ system As ∧ system Bs ⇒
  bisim (λa b. ∃R. R ∈ Rs ∧ R a b) As Bs

[oracles: DISK_THM] [axioms: relO, mapO, map_CONG, mapID, set_map] []
⊢ hom f (A,af) (B,bf) ∧ subsystem V (A,af) ⇒ subsystem (IMAGE f V) (B,bf)

[oracles: DISK_THM] [axioms: mapO, map_CONG, mapID, set_map] []
⊢ hom f (A,af) (B,bf) ∧ subsystem W (B,bf) ⇒
  subsystem (PREIMAGE f W ∩ A) (A,af)

[oracles: DISK_THM] [axioms: relO, mapO, map_CONG, mapID, set_map] []
⊢ hom f (A,af) (B,bf) ⇒
  hom f (A,af) (IMAGE f A,bf⟨IMAGE f A⟩) ∧
  (∀g h C cf.
     hom g (IMAGE f A,bf⟨IMAGE f A⟩) (C,cf) ∧
     hom h (IMAGE f A,bf⟨IMAGE f A⟩) (C,cf) ∧ (h ∘ f)⟨A⟩ = (g ∘ f)⟨A⟩ ⇒
     h = g) ∧ hom (eps (kernel A f) A) (A,af) (bquot (A,af) (kernel A f)) ∧
  hom (λx. x)⟨IMAGE f A⟩ (IMAGE f A,bf⟨IMAGE f A⟩) (B,bf) ∧
  iso (IMAGE f A,bf⟨IMAGE f A⟩) (bquot (A,af) (kernel A f)) ∧
  ∃mu.
    hom mu (bquot (A,af) (kernel A f)) (B,bf) ∧
    INJ mu (FST (bquot (A,af) (kernel A f))) B

[oracles: DISK_THM] [axioms: mapO, set_map, map_CONG] []
⊢ hom f (A,af) (B,bf) ∧ bisim R (A,af) (A,af) ∧ R ⊆ᵣ kernel A f ∧
  R equiv_on A ⇒
  ∃!fbar. hom fbar (bquot (A,af) R) (B,bf) ∧ f = (fbar ∘ eps R A)⟨A⟩

[oracles: DISK_THM] [axioms: relO, set_map, mapID, mapO, map_CONG] []
⊢ system (A,af) ∧ subsystem B (A,af) ∧ bisim R (A,af) (A,af) ∧
  R equiv_on A ∧ Abbrev (TR = {a | a ∈ A ∧ ∃b. b ∈ B ∧ R a b}) ⇒
  subsystem TR (A,af) ∧
  (let
     Q = CURRY (Rᴾ ∩ B × B)
   in
     bisim Q (B,af⟨B⟩) (B,af⟨B⟩) ∧ Q equiv_on B ∧
     iso (bquot (B,af⟨B⟩) Q) (bquot (TR,af⟨TR⟩) R))