One small theorem, seven formal readings

Open the proof source

-- Modern local reconstruction of the semantic content of PM *54.43.
-- This is not a formalization of PM's ramified type theory or class machinery.
-- Only Lean's implicit Init import; no Mathlib, Classical, choice, or new axioms.
namespace Principia
universe u
variable {X : Type u}

def EqualSets (S T : X → Prop) : Prop := ∀ z, S z ↔ T z
def Singleton (a : X) : X → Prop := fun z => z = a
def One (S : X → Prop) : Prop := ∃ a, EqualSets S (Singleton a)
def Two (S : X → Prop) : Prop :=
  ∃ a b, a ≠ b ∧ ∀ z, S z ↔ (z = a ∨ z = b)
def Union (S T : X → Prop) : X → Prop := fun z => S z ∨ T z
def Disjoint (S T : X → Prop) : Prop := ∀ z, S z → T z → False

-- Semantic analogue of *51.231: singletons are disjoint iff witnesses differ.
theorem singleton_disjoint_iff_distinct (a b : X) :
    Disjoint (Singleton a) (Singleton b) ↔ a ≠ b := by
  constructor
  · intro h hab
    exact h a rfl hab
  · intro hab z hza hzb
    exact hab (hza.symm.trans hzb)

-- Semantic analogue of *54.26: the singleton union has exactly two members
-- iff its displayed witnesses are distinct.
theorem singleton_union_two_iff_distinct (a b : X) :
    Two (Union (Singleton a) (Singleton b)) ↔ a ≠ b := by
  constructor
  · intro h hab
    obtain ⟨c, d, hcd, hmembers⟩ := h
    have hc : c = a := by
      have hc_union := (hmembers c).mpr (Or.inl rfl)
      cases hc_union with
      | inl hca => exact hca
      | inr hcb => exact hcb.trans hab.symm
    have hd : d = a := by
      have hd_union := (hmembers d).mpr (Or.inr rfl)
      cases hd_union with
      | inl hda => exact hda
      | inr hdb => exact hdb.trans hab.symm
    exact hcd (hc.trans hd.symm)
  · intro hab
    exact ⟨a, b, hab, fun _ => Iff.rfl⟩

-- Pointwise equivalence transports disjointness without predicate equality.
theorem disjoint_congr {S T A B : X → Prop}
    (hS : EqualSets S A) (hT : EqualSets T B) :
    Disjoint S T ↔ Disjoint A B := by
  constructor
  · intro h z hA hB
    exact h z ((hS z).mpr hA) ((hT z).mpr hB)
  · intro h z hS' hT'
    exact h z ((hS z).mp hS') ((hT z).mp hT')

theorem union_congr {S T A B : X → Prop}
    (hS : EqualSets S A) (hT : EqualSets T B) :
    EqualSets (Union S T) (Union A B) := by
  intro z
  constructor
  · intro h
    cases h with
    | inl hs => exact Or.inl ((hS z).mp hs)
    | inr ht => exact Or.inr ((hT z).mp ht)
  · intro h
    cases h with
    | inl ha => exact Or.inl ((hS z).mpr ha)
    | inr hb => exact Or.inr ((hT z).mpr hb)

theorem two_congr {S T : X → Prop} (hST : EqualSets S T) :
    Two S ↔ Two T := by
  constructor
  · intro h
    obtain ⟨a, b, hab, hm⟩ := h
    exact ⟨a, b, hab, fun z => (hST z).symm.trans (hm z)⟩
  · intro h
    obtain ⟨a, b, hab, hm⟩ := h
    exact ⟨a, b, hab, fun z => (hST z).trans (hm z)⟩

-- Both input existentials are eliminated locally; no witness choice function.
theorem pm_54_43 (S T : X → Prop) :
    One S → One T → (Disjoint S T ↔ Two (Union S T)) := by
  intro hS hT
  obtain ⟨a, hSa⟩ := hS
  obtain ⟨b, hTb⟩ := hT
  have hd : Disjoint S T ↔ a ≠ b :=
    (disjoint_congr hSa hTb).trans (singleton_disjoint_iff_distinct a b)
  have ht : Two (Union S T) ↔ a ≠ b :=
    (two_congr (union_congr hSa hTb)).trans
      (singleton_union_two_iff_distinct a b)
  exact hd.trans ht.symm

-- Checked negative control: dropping disjointness/distinctness is false,
-- already for one chosen element of any inhabited carrier.
theorem equal_singletons_not_two (a : X) :
    ¬ Two (Union (Singleton a) (Singleton a)) := by
  intro h
  exact ((singleton_union_two_iff_distinct a a).mp h) rfl

#print axioms singleton_disjoint_iff_distinct
#print axioms singleton_union_two_iff_distinct
#print axioms disjoint_congr
#print axioms union_congr
#print axioms two_congr
#print axioms pm_54_43
#print axioms equal_singletons_not_two
end Principia

Open the proof source

(* Modern local reconstruction of the semantic content of PM *54.43.
   This does not formalize PM's ramified type theory or class machinery.
   Only the default Rocq prelude; no imports, Classical, choice, or axioms. *)
Set Implicit Arguments.
Section PrincipiaProof.
Context {X : Type}.

Definition EqualSets (S T : X -> Prop) : Prop := forall z, S z <-> T z.
Definition Singleton (a : X) : X -> Prop := fun z => z = a.
Definition One (S : X -> Prop) : Prop := exists a, EqualSets S (Singleton a).
Definition Two (S : X -> Prop) : Prop :=
  exists a b, a <> b /\ forall z, S z <-> (z = a \/ z = b).
Definition Union (S T : X -> Prop) : X -> Prop := fun z => S z \/ T z.
Definition Disjoint (S T : X -> Prop) : Prop :=
  forall z, S z -> T z -> False.

(* Semantic analogue of *51.231. *)
Theorem singleton_disjoint_iff_distinct (a b : X) :
  Disjoint (Singleton a) (Singleton b) <-> a <> b.
Proof.
  split.
  - intros h hab. exact (h a eq_refl hab).
  - intros hab z hza hzb. apply hab.
    exact (eq_trans (eq_sym hza) hzb).
Qed.

(* Semantic analogue of *54.26. *)
Theorem singleton_union_two_iff_distinct (a b : X) :
  Two (Union (Singleton a) (Singleton b)) <-> a <> b.
Proof.
  split.
  - intros [c [d [hcd hm]]] hab.
    assert (hc : c = a).
    { destruct (proj2 (hm c) (or_introl eq_refl)) as [hca | hcb].
      - exact hca.
      - exact (eq_trans hcb (eq_sym hab)). }
    assert (hd : d = a).
    { destruct (proj2 (hm d) (or_intror eq_refl)) as [hda | hdb].
      - exact hda.
      - exact (eq_trans hdb (eq_sym hab)). }
    exact (hcd (eq_trans hc (eq_sym hd))).
  - intro hab. exists a, b. split.
    + exact hab.
    + intro z. unfold Union, Singleton. split; intro h; exact h.
Qed.

Theorem disjoint_congr (S T A B : X -> Prop)
  (hS : EqualSets S A) (hT : EqualSets T B) :
  Disjoint S T <-> Disjoint A B.
Proof.
  split.
  - intros h z hA hB.
    exact (h z (proj2 (hS z) hA) (proj2 (hT z) hB)).
  - intros h z hS' hT'.
    exact (h z (proj1 (hS z) hS') (proj1 (hT z) hT')).
Qed.

Theorem union_congr (S T A B : X -> Prop)
  (hS : EqualSets S A) (hT : EqualSets T B) :
  EqualSets (Union S T) (Union A B).
Proof.
  intro z. split.
  - intros [h | h].
    + left. exact (proj1 (hS z) h).
    + right. exact (proj1 (hT z) h).
  - intros [h | h].
    + left. exact (proj2 (hS z) h).
    + right. exact (proj2 (hT z) h).
Qed.

Theorem two_congr (S T : X -> Prop) (hST : EqualSets S T) :
  Two S <-> Two T.
Proof.
  split.
  - intros [a [b [hab hm]]]. exists a, b. split.
    + exact hab.
    + intro z. split.
      * intro ht. exact (proj1 (hm z) (proj2 (hST z) ht)).
      * intro hz. exact (proj1 (hST z) (proj2 (hm z) hz)).
  - intros [a [b [hab hm]]]. exists a, b. split.
    + exact hab.
    + intro z. split.
      * intro hs. exact (proj1 (hm z) (proj1 (hST z) hs)).
      * intro hz. exact (proj2 (hST z) (proj2 (hm z) hz)).
Qed.

(* Eliminate the given singleton witnesses within Prop. *)
Theorem pm_54_43 (S T : X -> Prop) :
  One S -> One T -> (Disjoint S T <-> Two (Union S T)).
Proof.
  intros [a hSa] [b hTb].
  pose proof (disjoint_congr hSa hTb) as hd.
  pose proof (two_congr (union_congr hSa hTb)) as ht.
  split.
  - intro h. apply (proj2 ht).
    apply (proj2 (singleton_union_two_iff_distinct a b)).
    apply (proj1 (singleton_disjoint_iff_distinct a b)).
    exact (proj1 hd h).
  - intro h. apply (proj2 hd).
    apply (proj2 (singleton_disjoint_iff_distinct a b)).
    apply (proj1 (singleton_union_two_iff_distinct a b)).
    exact (proj1 ht h).
Qed.

(* Checked negative control: coincident singletons cannot have two members. *)
Theorem equal_singletons_not_two (a : X) :
  ~ Two (Union (Singleton a) (Singleton a)).
Proof.
  intro h.
  exact (proj1 (singleton_union_two_iff_distinct a a) h eq_refl).
Qed.
End PrincipiaProof.

Set Printing All Assumptions.
Print Typing Flags.
Print Assumptions singleton_disjoint_iff_distinct.
Print Assumptions singleton_union_two_iff_distinct.
Print Assumptions disjoint_congr.
Print Assumptions union_congr.
Print Assumptions two_congr.
Print Assumptions pm_54_43.
Print Assumptions equal_singletons_not_two.

Open the proof source

theory Principia
  imports Main
begin

text \<open>Local semantic reconstruction of PM *54.43, not its ramified type theory.\<close>

definition One :: "'a set \<Rightarrow> bool" where
  "One S \<longleftrightarrow> (\<exists>a. S = {a})"
definition Two :: "'a set \<Rightarrow> bool" where
  "Two S \<longleftrightarrow> (\<exists>a b. a \<noteq> b \<and> S = {a,b})"
definition Disjoint :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
  "Disjoint S T \<longleftrightarrow> S \<inter> T = {}"

lemma PM51_231:
  "Disjoint {a} {b} \<longleftrightarrow> a \<noteq> b"
  unfolding Disjoint_def by auto

lemma PM54_26:
  "Two ({a} \<union> {b}) \<longleftrightarrow> a \<noteq> b"
proof
  assume two: "Two ({a} \<union> {b})"
  then obtain c d where distinct: "c \<noteq> d"
    and pair: "{a} \<union> {b} = {c,d}"
    unfolding Two_def by blast
  show "a \<noteq> b"
  proof
    assume "a = b"
    with pair have "c = a" and "d = a" by auto
    with distinct show False by simp
  qed
next
  assume "a \<noteq> b"
  moreover have "{a} \<union> {b} = {a,b}" by auto
  ultimately show "Two ({a} \<union> {b})"
    unfolding Two_def by blast
qed

theorem PM54_43:
  assumes "One S" and "One T"
  shows "Disjoint S T \<longleftrightarrow> Two (S \<union> T)"
proof -
  from assms(1) obtain a where s: "S = {a}"
    unfolding One_def by blast
  from assms(2) obtain b where t: "T = {b}"
    unfolding One_def by blast
  have "Disjoint S T \<longleftrightarrow> a \<noteq> b"
    using PM51_231[of a b] s t by simp
  also have "... \<longleftrightarrow> Two (S \<union> T)"
    using PM54_26[of a b] s t by simp
  finally show ?thesis .
qed

text \<open>Checked negative control: without distinctness, a repeated singleton
satisfies the weakened Two predicate while disjointness fails.\<close>
definition TwoWeak :: "'a set \<Rightarrow> bool" where
  "TwoWeak S \<longleftrightarrow> (\<exists>a b. S = {a,b})"
lemma distinctness_counterexample:
  "One ({()} :: unit set) \<and> TwoWeak ({()} \<union> {()})
   \<and> \<not> Disjoint {()} {()} \<and> \<not> Two ({()} \<union> {()})"
  unfolding One_def TwoWeak_def Two_def Disjoint_def by auto

end

Open the proof source

:: Local semantic reconstruction of PM *54.43 (1910, p. 379).
:: This article uses ordinary Mizar sets, not PM's ramified type theory.
environ
 vocabularies TARSKI, XBOOLE_0;
 notations TARSKI, XBOOLE_0;
 constructors TARSKI, XBOOLE_0;
 registrations XBOOLE_0;
 requirements BOOLE;
 theorems TARSKI, XBOOLE_0;
 definitions TARSKI, XBOOLE_0;

begin

defpred One[set] means ex a being object st $1 = {a};
defpred Two[set] means
  ex a,b being object st a <> b & $1 = {a,b};
defpred Disjoint[set,set] means $1 /\ $2 = {};

PM51231: for a,b being object holds Disjoint[{a},{b}] iff a <> b
proof
 let a,b be object;
 thus Disjoint[{a},{b}] implies a <> b
 proof
  assume A1: {a} /\ {b} = {};
  assume a = b;
  then a in {a} & a in {b} by TARSKI:def 1;
  then a in {} by A1,XBOOLE_0:def 4;
  hence contradiction;
 end;
 assume A2: a <> b;
 for x being object holds not x in {a} /\ {b}
 proof
  let x be object;
  assume x in {a} /\ {b};
  then x in {a} & x in {b} by XBOOLE_0:def 4;
  then x = a & x = b by TARSKI:def 1;
  hence contradiction by A2;
 end;
 hence Disjoint[{a},{b}] by XBOOLE_0:def 1;
end;

SingletonUnion: for a,b being object holds {a} \/ {b} = {a,b}
proof
 let a,b be object;
 now
  let x be object;
  x in {a} \/ {b} iff x in {a} or x in {b} by XBOOLE_0:def 3;
  then x in {a} \/ {b} iff x = a or x = b by TARSKI:def 1;
  hence x in {a} \/ {b} iff x in {a,b} by TARSKI:def 2;
 end;
 hence thesis by TARSKI:2;
end;

PM5426: for a,b being object holds Two[{a} \/ {b}] iff a <> b
proof
 let a,b be object;
 thus Two[{a} \/ {b}] implies a <> b
 proof
  given c,d being object such that
  A1: c <> d and A2: {a} \/ {b} = {c,d};
  assume A3: a = b;
  c in {c,d} & d in {c,d} by TARSKI:def 2;
  then c in {a} & d in {a} by A2,A3;
  then c = a & d = a by TARSKI:def 1;
  hence contradiction by A1;
 end;
 assume A4: a <> b;
 {a} \/ {b} = {a,b} by SingletonUnion;
 hence Two[{a} \/ {b}] by A4;
end;

PM5443: for S,T being set st One[S] & One[T]
 holds Disjoint[S,T] iff Two[S \/ T]
proof
 let S,T be set;
 assume A1: One[S] & One[T];
 consider a being object such that A2: S = {a} by A1;
 consider b being object such that A3: T = {b} by A1;
 Disjoint[S,T] iff a <> b by A2,A3,PM51231;
 hence thesis by A2,A3,PM5426;
end;

:: Checked counterexample after removing distinctness from Two.
defpred TwoWeak[set] means ex a,b being object st $1 = {a,b};

DistinctnessCounterexample:
 One[{{}}] & TwoWeak[{{}} \/ {{}}] &
 not Disjoint[{{}},{{}}] & not Two[{{}} \/ {{}}]
proof
 thus One[{{}}];
 {{}} \/ {{}} = {{},{}} by SingletonUnion;
 hence TwoWeak[{{}} \/ {{}}];
 thus not Disjoint[{{}},{{}}] by PM51231;
 thus not Two[{{}} \/ {{}}] by PM5426;
end;

Open the proof source

{-# OPTIONS --safe --without-K #-}
module Principia where

open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

data Empty : Set where

data _+_ (A B : Set) : Set where
  left : A → A + B
  right : B → A + B

infixr 2 _+_

_×_ : Set → Set → Set
A × B = Σ A (λ _ → B)

_↔_ : Set → Set → Set
A ↔ B = (A → B) × (B → A)

sym : {A : Set} {a b : A} → a ≡ b → b ≡ a
sym refl = refl

trans : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans refl q = q

module Contract (X : Set) where
  Subset = X → Set
  Singleton : X → Subset
  Singleton a z = z ≡ a

  Same : Subset → Subset → Set
  Same S T = (z : X) → (S z → T z) × (T z → S z)

  One : Subset → Set
  One S = Σ X (λ a → Same S (Singleton a))

  Union : Subset → Subset → Subset
  Union S T z = S z + T z

  Disjoint : Subset → Subset → Set
  Disjoint S T = (z : X) → S z → T z → Empty

  Distinct : X → X → Set
  Distinct a b = a ≡ b → Empty

  Two : Subset → Set
  Two S = Σ X (λ a → Σ X (λ b → Distinct a b × Same S (Union (Singleton a) (Singleton b))))

  same_refl : (S : Subset) → Same S S
  same_refl S z = (λ x → x) , (λ x → x)

  same_sym : {S T : Subset} → Same S T → Same T S
  same_sym e z = snd (e z) , fst (e z)

  same_trans : {S T U : Subset} → Same S T → Same T U → Same S U
  same_trans e f z = (λ s → fst (f z) (fst (e z) s)) , (λ u → snd (e z) (snd (f z) u))

  union_map : {S T U V : Subset} → Same S U → Same T V → Same (Union S T) (Union U V)
  union_map {S} {T} {U} {V} e f z = forward , backward
    where
    forward : S z + T z → U z + V z
    forward (left s) = left (fst (e z) s)
    forward (right t) = right (fst (f z) t)
    backward : U z + V z → S z + T z
    backward (left u) = left (snd (e z) u)
    backward (right v) = right (snd (f z) v)

  two_map : {S T : Subset} → Same S T → Two S → Two T
  two_map e (a , (b , (d , f))) = a , (b , (d , same_trans (same_sym e) f))

  disjoint_map : {S T U V : Subset} → Same S U → Same T V → Disjoint S T → Disjoint U V
  disjoint_map e f d z u v = d z (snd (e z) u) (snd (f z) v)

  singleton_disjoint_iff_distinct : (a b : X) → Disjoint (Singleton a) (Singleton b) ↔ Distinct a b
  singleton_disjoint_iff_distinct a b = (λ d p → d a refl p) , (λ d z p q → d (trans (sym p) q))

  collapse : {a b z : X} → a ≡ b → (z ≡ a) + (z ≡ b) → z ≡ a
  collapse p (left q) = q
  collapse p (right q) = trans q (sym p)

  union_two_implies_distinct : {a b : X} → Two (Union (Singleton a) (Singleton b)) → Distinct a b
  union_two_implies_distinct (c , (d , (neq , e))) p = neq (trans ca (sym da))
    where
    ca = collapse p (snd (e c) (left refl))
    da = collapse p (snd (e d) (right refl))

  singleton_union_two_iff_distinct : (a b : X) → Two (Union (Singleton a) (Singleton b)) ↔ Distinct a b
  singleton_union_two_iff_distinct a b = union_two_implies_distinct , (λ d → a , (b , (d , same_refl _)))

  pm54-43 : {S T : Subset} → One S → One T → Disjoint S T ↔ Two (Union S T)
  pm54-43 {S} {T} (a , e) (b , f) = forward , backward
    where
    forward : Disjoint S T → Two (Union S T)
    forward d = two_map (same_sym (union_map e f))
      (snd (singleton_union_two_iff_distinct a b)
        (fst (singleton_disjoint_iff_distinct a b) (disjoint_map e f d)))
    backward : Two (Union S T) → Disjoint S T
    backward t = disjoint_map (same_sym e) (same_sym f)
      (snd (singleton_disjoint_iff_distinct a b)
        (fst (singleton_union_two_iff_distinct a b) (two_map (union_map e f) t)))

  -- The tagged carrier retains the side even when the original points coincide.
  Tagged : Set
  Tagged = X + X
  tagged_left_ne_right : (a b : X) → left a ≡ right b → Empty
  tagged_left_ne_right a b ()



module NegativeControl (X : Set) where
  module C = Contract X
  module T = Contract C.Tagged
  tagged_coproduct_two : (a b : X) → T.Two (T.Union (T.Singleton (left a)) (T.Singleton (right b)))
  tagged_coproduct_two a b = left a , (right b , (C.tagged_left_ne_right a b , T.same_refl _))
  equal_points_still_two : (a : X) → T.Two (T.Union (T.Singleton (left a)) (T.Singleton (right a)))
  equal_points_still_two a = tagged_coproduct_two a a

module EvidenceRelevant (X : Set) where
  open Contract X
  ordinary_equal_not_two : (a : X) → Two (Union (Singleton a) (Singleton a)) → Empty
  ordinary_equal_not_two a t = union_two_implies_distinct t refl

  -- A coincident ordinary union still has two different membership witnesses.
  coincident_membership_tags_distinct : (a : X) →
    left {a ≡ a} {a ≡ a} refl ≡ right refl → Empty
  coincident_membership_tags_distinct a ()

Open the proof source

-- Explicit witnesses; Same and Iff contain maps, not homotopy inverse laws.
\data Empty
\data Sum (A B : \Type0)
  | inl A
  | inr B
\open Sum

\func Product (A B : \Type0) => \Sigma A B
\func Iff (A B : \Type0) => Product (A -> B) (B -> A)

\func transport {A : \Type0} (B : A -> \Type0) {a b : A} (p : a = b) (v : B a) : B b \elim p
  | idp => v
\func sym {A : \Type0} {a b : A} (p : a = b) : b = a
  => transport (\lam z => z = a) p idp
\func trans {A : \Type0} {a b c : A} (p : a = b) (q : b = c) : a = c
  => transport (\lam z => a = z) q p

\func Singleton {X : \Type0} (a z : X) => z = a
\func Same {X : \Type0} (S T : X -> \Type0) => \Pi (z : X) -> Product (S z -> T z) (T z -> S z)
\func One {X : \Type0} (S : X -> \Type0) => \Sigma (a : X) (Same S (Singleton a))
\func Union {X : \Type0} (S T : X -> \Type0) (z : X) => Sum (S z) (T z)
\func Disjoint {X : \Type0} (S T : X -> \Type0) => \Pi (z : X) -> S z -> T z -> Empty
\func Distinct {X : \Type0} (a b : X) => a = b -> Empty
\func Two {X : \Type0} (S : X -> \Type0) => \Sigma (a b : X) (Product (Distinct a b) (Same S (Union (Singleton a) (Singleton b))))

\func same_refl {X : \Type0} (S : X -> \Type0) : Same S S
  => \lam z => (\lam s => s, \lam s => s)
\func same_sym {X : \Type0} {S T : X -> \Type0} (e : Same S T) : Same T S
  => \lam z => ((e z).2, (e z).1)
\func same_trans {X : \Type0} {S T U : X -> \Type0} (e : Same S T) (f : Same T U) : Same S U
  => \lam z => (\lam s => (f z).1 ((e z).1 s), \lam u => (e z).2 ((f z).2 u))
\func sum_map {A B C D : \Type0} (f : A -> C) (g : B -> D) (v : Sum A B) : Sum C D \elim v
  | inl a => inl (f a)
  | inr b => inr (g b)
\func union_map {X : \Type0} {S T U V : X -> \Type0} (e : Same S U) (f : Same T V) : Same (Union S T) (Union U V)
  => \lam z => (sum_map ((e z).1) ((f z).1), sum_map ((e z).2) ((f z).2))
\func two_map {X : \Type0} {S T : X -> \Type0} (e : Same S T) (v : Two S) : Two T
  => (v.1, v.2, (v.3.1, same_trans (same_sym e) v.3.2))
\func disjoint_map {X : \Type0} {S T U V : X -> \Type0} (e : Same S U) (f : Same T V) (d : Disjoint S T) : Disjoint U V
  => \lam z u v => d z ((e z).2 u) ((f z).2 v)

-- PM *51.231 local analogue.
\func singleton_disjoint_iff_distinct {X : \Type0} (a b : X) : Iff (Disjoint (Singleton a) (Singleton b)) (Distinct a b)
  => (\lam d p => d a idp p, \lam d z p q => d (trans (sym p) q))
\func collapse {X : \Type0} {a b z : X} (p : a = b) (v : Sum (z = a) (z = b)) : z = a \elim v
  | inl q => q
  | inr q => trans q (sym p)
\func union_two_implies_distinct {X : \Type0} {a b : X} (v : Two (Union (Singleton a) (Singleton b))) : Distinct a b
  => \lam p => v.3.1 (trans (collapse p ((v.3.2 v.1).2 (inl idp))) (sym (collapse p ((v.3.2 v.2).2 (inr idp)))))
-- PM *54.26 local analogue.
\func singleton_union_two_iff_distinct {X : \Type0} (a b : X) : Iff (Two (Union (Singleton a) (Singleton b))) (Distinct a b)
  => (union_two_implies_distinct, \lam d => (a, b, (d, same_refl (Union (Singleton a) (Singleton b)))))

-- PM *54.43 semantic endpoint, abstract carrier; no set constraint.
\func pm54_43 {X : \Type0} {S T : X -> \Type0} (s : One S) (t : One T) : Iff (Disjoint S T) (Two (Union S T))
  => (\lam d => two_map (same_sym (union_map s.2 t.2))
        ((singleton_union_two_iff_distinct s.1 t.1).2
          ((singleton_disjoint_iff_distinct s.1 t.1).1 (disjoint_map s.2 t.2 d))),
      \lam v => disjoint_map (same_sym s.2) (same_sym t.2)
        ((singleton_disjoint_iff_distinct s.1 t.1).2
          ((singleton_union_two_iff_distinct s.1 t.1).1 (two_map (union_map s.2 t.2) v))))

-- Tags separate elements even when the underlying point is identical.
\func tagged_left_ne_right {X : \Type0} (a b : X) (p : inl {X} {X} a = inr b) : Empty \elim p
  | ()
\func tagged_coproduct_two {X : \Type0} (a b : X) : Two (Union (Singleton (inl {X} {X} a)) (Singleton (inr b)))
  => (inl a, inr b, (tagged_left_ne_right a b, same_refl (Union (Singleton (inl a)) (Singleton (inr b)))))
\func equal_points_still_two {X : \Type0} (a : X) : Two (Union (Singleton (inl {X} {X} a)) (Singleton (inr a)))
  => tagged_coproduct_two a a

\func ordinary_equal_not_two {X : \Type0} (a : X) (v : Two (Union (Singleton a) (Singleton a))) : Empty
  => union_two_implies_distinct v idp
\func coincident_membership_tags_distinct {X : \Type0} (a : X)
  (p : inl {a = a} {a = a} idp = inr idp) : Empty \elim p
  | ()