main :: IO ()
main = return ()

---- Rig category of types ----

data (⊥)
data (⊤) = TT

infix 7 ×
infix 6 ∐
infix 4 ≡

data (∐) a b where
  Inl :: a -> a ∐ b
  Inr :: b -> a ∐ b

data (×) a b where
  Pair :: a -> b -> a × b

data (≡) a b where
  Equiv :: (a -> b) -> (b -> a) -> a ≡ b

--- Equivalence relation ---

equiv_refl :: forall a. a -> a ≡ a
equiv_refl _ = Equiv id id

equiv_sym_sub1 :: forall a b. a ≡ b -> b ≡ a
equiv_sym_sub1 (Equiv a_to_b b_to_a) = Equiv b_to_a a_to_b

equiv_sym_sub2 :: forall a b. b ≡ a -> a ≡ b
equiv_sym_sub2 (Equiv b_to_a a_to_b) = Equiv a_to_b b_to_a

equiv_sym :: forall a b. (a ≡ b) ≡ (b ≡ a)
equiv_sym = Equiv equiv_sym_sub1 equiv_sym_sub2

equiv_trans :: forall a b c. a ≡ b -> b ≡ c -> a ≡ c
equiv_trans (Equiv a_to_b b_to_a) (Equiv b_to_c c_to_b) = Equiv (b_to_c . a_to_b) (b_to_a . c_to_b)

--- Additive monoid ---

-- Identity --

-- Auxiliary lemmas
coproduct_idl_sub1 :: forall a. a ∐ (⊥) -> a
coproduct_idl_sub1 (Inl a) = a

coproduct_idl_sub2 :: forall a. a -> a ∐ (⊥)
coproduct_idl_sub2 a = Inl a

coproduct_idr_sub1 :: forall a. (⊥) ∐ a -> a
coproduct_idr_sub1 (Inr a) = a

coproduct_idr_sub2 :: forall a. a -> (⊥) ∐ a
coproduct_idr_sub2 a = Inr a

-- Theorems
coproduct_idl :: forall a. a ∐ (⊥) ≡ a
coproduct_idl = Equiv coproduct_idl_sub1 coproduct_idl_sub2

coproduct_idr :: forall a. (⊥) ∐ a ≡ a
coproduct_idr = Equiv coproduct_idr_sub1 coproduct_idr_sub2

-- Associativity

-- Auxiliary lemmas
coproduct_assocl :: forall a b c. (a ∐ b) ∐ c -> a ∐ (b ∐ c)
coproduct_assocl (Inl (Inl a)) = Inl a
coproduct_assocl (Inl (Inr b)) = Inr (Inl b)
coproduct_assocl (Inr c) = Inr (Inr c)

coproduct_assocr :: forall a b c. a ∐ (b ∐ c) -> (a ∐ b) ∐ c
coproduct_assocr (Inl a) = Inl (Inl a)
coproduct_assocr (Inr (Inl b)) = Inl (Inr b)
coproduct_assocr (Inr (Inr c)) = Inr c

-- Theorem
coproduct_assoc :: forall a b c. (a ∐ b) ∐ c ≡ a ∐ (b ∐ c)
coproduct_assoc = Equiv coproduct_assocl coproduct_assocr

--- Multiplicative monoid ---

-- Identity --

-- Auxiliary lemmas
product_idl_sub1 :: forall a. a × (⊤) -> a
product_idl_sub1 (Pair a TT) = a

product_idl_sub2 :: forall a. a -> a × (⊤)
product_idl_sub2 a = Pair a TT

product_idr_sub1 :: forall a. (⊤) × a -> a
product_idr_sub1 (Pair TT a) = a

product_idr_sub2 :: forall a. a -> (⊤) × a
product_idr_sub2 a = Pair TT a

-- Theorems
product_idl :: forall a. a × (⊤) ≡ a
product_idl = Equiv product_idl_sub1 product_idl_sub2

product_idr :: forall a. (⊤) × a ≡ a
product_idr = Equiv product_idr_sub1 product_idr_sub2

-- Associativity --

-- Auxiliary lemmas
product_assocl :: forall a b c. (a × b) × c -> a × (b × c)
product_assocl (Pair (Pair a b) c) = Pair a (Pair b c)

product_assocr :: forall a b c. a × (b × c) -> (a × b) × c
product_assocr (Pair a (Pair b c)) = Pair (Pair a b) c

-- Theorem
product_assoc :: forall a b c. (a × b) × c ≡ a × (b × c)
product_assoc = Equiv product_assocl product_assocr

--- Absorption (Annihilation) ---

-- Auxiliary lemmas

product_absorpl_sub1 :: forall a. (⊥) × a -> (⊥)
product_absorpl_sub1 (Pair false _) = false

product_absorpl_sub2 :: forall a. (⊥) -> (⊥) × a
product_absorpl_sub2 false = case false of {}

product_absorpr_sub1 :: forall a. a × (⊥) -> (⊥)
product_absorpr_sub1 (Pair _ false) = false

product_absorpr_sub2 :: forall a. (⊥) -> a × (⊥)
product_absorpr_sub2 false = case false of {}

-- Theorems

product_absorpl :: forall a. (⊥) × a ≡ (⊥)
product_absorpl = Equiv product_absorpl_sub1 product_absorpl_sub2

product_absorpr :: forall a. a × (⊥) ≡ (⊥)
product_absorpr = Equiv product_absorpr_sub1 product_absorpr_sub2

--- Distributity ---

-- Auxiliary lemmas

distrib_product_over_coproductl_sub1 :: forall a b c. a × (b ∐ c) -> a × b ∐ a × c
distrib_product_over_coproductl_sub1 (Pair a (Inl b)) = Inl (Pair a b)
distrib_product_over_coproductl_sub1 (Pair a (Inr c)) = Inr (Pair a c)

distrib_product_over_coproductl_sub2 :: forall a b c. a × b ∐ a × c -> a × (b ∐ c)
distrib_product_over_coproductl_sub2 (Inl (Pair a b)) = Pair a (Inl b)
distrib_product_over_coproductl_sub2 (Inr (Pair a c)) = Pair a (Inr c)

distrib_product_over_coproductr_sub1 :: forall a b c. (a ∐ b) × c -> a × c ∐ b × c
distrib_product_over_coproductr_sub1 (Pair (Inl a) c) = Inl (Pair a c)
distrib_product_over_coproductr_sub1 (Pair (Inr b) c) = Inr (Pair b c)

distrib_product_over_coproductr_sub2 :: forall a b c. a × c ∐ b × c -> (a ∐ b) × c
distrib_product_over_coproductr_sub2 (Inl (Pair a c)) = Pair (Inl a) c
distrib_product_over_coproductr_sub2 (Inr (Pair b c)) = Pair (Inr b) c

-- Theorems

distrib_product_over_coproductl :: forall a b c. a × (b ∐ c) ≡ a × b ∐ a × c
distrib_product_over_coproductl = Equiv distrib_product_over_coproductl_sub1 distrib_product_over_coproductl_sub2

distrib_product_over_coproductr :: forall a b c. (a ∐ b) × c ≡ a × c ∐ b × c
distrib_product_over_coproductr = Equiv distrib_product_over_coproductr_sub1 distrib_product_over_coproductr_sub2