-- 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
  | ()