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