{-# OPTIONS --safe #-}

module Problem2 (T : Set) where
open import Data.List
open import Data.Nat
open import Data.Product

Relation = T → T → Set

Commutes : Relation → Relation → Set
Commutes R1 R2 = ∀{x y z} → R1 x y →  R2 x z → ∃[ t ] (R2 y t × R1 z t)

Diamond : Relation → Set
Diamond R = Commutes R R

data Star (R : Relation) : Relation where
  rule  : ∀{x y} → R x y → Star R x y
  refl  : ∀{x} → Star R x x
  trans : ∀{x y z} → Star R x y → Star R y z → Star R x z

-- We prove by induction on the transitive closure proof rs. The three cases
-- are given diagrammatically:
--
-- rs = rule r′
-- We have the following diagram by assumption.
-- x - r′ → y
-- |        |
-- r        s
-- ↓        ↓
-- z - s′ → t
--
-- rs = refl
-- The diagram commutes.
-- x == x
-- |    |
-- r    r
-- ↓    ↓
-- z == z
--
-- rs = trans rs₁ rs₂
-- The diagram commutes, with each square derived by induction.
-- x - rs₁ → y₁ - rs₂ → y₂
-- |         |          |
-- r         s₁         s₂
-- ↓         ↓          ↓
-- z - ss₁ → t₁ - ss₂ → t₂
strip : ∀{R} → Diamond R → Commutes (Star R) R
strip commutes (rule r′) r =
  let (t , s , s′) = commutes r′ r in
  t , s , rule s′
strip commutes refl r = -, r , refl
strip commutes (trans rs₁ rs₂) r =
  let (t₁ , s₁ , ss₁) = strip commutes rs₁ r in
  let (t₂ , s₂ , ss₂) = strip commutes rs₂ s₁ in
  t₂ , s₂ , trans ss₁ ss₂