From e0f02bdb0f995df59a169aec8b924b2098c1cfbb Mon Sep 17 00:00:00 2001 From: Sergey Goncharov Date: Tue, 27 Jun 2023 14:55:46 +0000 Subject: [PATCH] Elgot iteration formalization --- ElgotIteration.agda | 355 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 355 insertions(+) create mode 100644 ElgotIteration.agda diff --git a/ElgotIteration.agda b/ElgotIteration.agda new file mode 100644 index 0000000..bd8288b --- /dev/null +++ b/ElgotIteration.agda @@ -0,0 +1,355 @@ +{-# OPTIONS --cubical --safe #-} + +open import Level using (Level) renaming (suc to ℓ-suc) +open import Function using (id; _∘_; _$_) +open import Data.Product using (_×_; Σ; _,_; ∃-syntax; proj₁; proj₂) + +open import CubicalIdentity using (_≡_; sym; trans; refl; cong; cong2; subst; subst-app) +open CubicalIdentity.≡-Reasoning + +open import Category +open import Co-Cartesian +open import Functor + +--* +{- + This module introduces the notion of Elgot iteration in a category. +-} +--* + +module ElgotIteration {ℓ : Level} {Ob : Set (ℓ-suc ℓ)} {C : Category Ob} (CoC : Co-Cartesian C) where + +open Co-Cartesian.Co-Cartesian CoC renaming (_⊎_ to _+_) + +module †-axioms (_† : ∀ {X Y : Obj} → (X ➔ Y + X) → (X ➔ Y)) where + + -- Fixpoint + Fix : Set (ℓ-suc ℓ) + Fix = ∀ {X Y : Obj} {f : X ➔ Y + X} + → [ idm , f † ] ⊚ f ≡ f † + + -- Naturality + Nat : Set (ℓ-suc ℓ) + Nat = ∀ {X Y Z : Obj} {f : X ➔ Y + X} {g : Y ➔ Z} + → ((g ⊕ idm) ⊚ f) † ≡ g ⊚ f † + + -- Dinaturality + Din : Set (ℓ-suc ℓ) + Din = ∀ {X Y Z : Obj} {g : X ➔ Y + Z} {h : Z ➔ Y + X} + → ([ inl , h ] ⊚ g) † ≡ [ idm , ([ inl , g ] ⊚ h) † ] ⊚ g + + -- Codiagonal + Cod : Set (ℓ-suc ℓ) + Cod = ∀ {X Y : Obj} {f : X ➔ (Y + X) + X} + → ([ idm , inr ] ⊚ f) † ≡ f † † + + module _ {D : Category Ob} {CoC-D : Co-Cartesian D} + {F : Functor D C id} (J : CoC-Functor CoC-D CoC F) where + + open Co-Cartesian.Co-Cartesian CoC-D + using () renaming (_➔_ to _➔′_; idm to idm′; _⊕_ to _⊕′_) + open Functor.CoC-Functor J + + Uni : Set (ℓ-suc ℓ) + Uni = ∀ {X Y Z : Obj} {f : X ➔ Y + X} {g : Z ➔ Y + Z} {h : Z ➔′ X} + → f ⊚ (fmap h) ≡ (idm ⊕ fmap h) ⊚ g → f † ⊚ (fmap h) ≡ g † + +open †-axioms + +record ElgotIteration : Set (ℓ-suc ℓ) where + + field + _† : ∀ {X Y : Obj} → (X ➔ Y + X) → (X ➔ Y) + fix : Fix _† + +record ConwayIteration (It : ElgotIteration) : Set (ℓ-suc ℓ) where + open ElgotIteration It public + + field + -- Naturality + nat : Nat _† + + -- Dinaturality + din : Din _† + + -- Codiagonal + cod : Cod _† + +record TotalUniConway (It : ElgotIteration) {D : Category Ob} {CoC-D : Co-Cartesian D} + {F : Functor D C id} (J : CoC-Functor CoC-D CoC F) : Set (ℓ-suc ℓ) where + + -- added uniformity, removed dinaturality; + -- the latter is derivable, which is shown below + open ElgotIteration It public + + field + -- Naturality + nat : Nat _† + + -- Codiagonal + cod : Cod _† + + -- Uniformity + uni : Uni _† J + + open Co-Cartesian.Co-Cartesian CoC-D + using () renaming (inl to inl′; inr to inr′ + ; _⊚_ to _⊚′_; idm to idm′; _➔_ to _➔′_ + ; _⊎_ to _+′_ ; _⊕_ to _⊕′_; [_,_] to [_,_]′) + + open CoC-Functor J + + -- some coherence properties of injections, + -- using the fact that J is identical on objects + fmap-⊎F-inl : ∀ {X Y : Obj} → fmap (⊎F→ {X} {Y} (X ➔′_) inl′) ≡ inl + fmap-⊎F-inl{X}{Y} = trans (sym $ subst-app (X ➔′_) {B₂ = X ➔_} (λ _ → fmap) ⊎F) $ sym inlF + + fmap-⊎F-inr : ∀ {X Y : Obj} → fmap (⊎F→ {X} {Y} (Y ➔′_) inr′) ≡ inr + fmap-⊎F-inr{X}{Y} = trans (sym $ subst-app (Y ➔′_) {B₂ = Y ➔_} (λ _ → fmap) ⊎F) $ sym inrF + + -- an instance of uniformity for inl + †-inl : ∀ {X Y Z : Obj} {f : (X + Z) ➔ Y + (X + Z)} {g : X ➔ Y + X} + → f ⊚ inl ≡ (idm ⊕ inl) ⊚ g → f † ⊚ inl ≡ g † + †-inl {X} {Y} {Z} {f = f} {g = g} p = + begin + f † ⊚ inl + ≡˘⟨ cong (_⊚_ (f †)) fmap-⊎F-inl ⟩ + f † ⊚ fmap (⊎F→ (X ➔′_) inl′) + ≡⟨ uni p′ ⟩ + g † + ∎ + where + p′ : f ⊚ fmap (⊎F→ (X ➔′_) inl′) ≡ (idm ⊕ fmap (⊎F→ (X ➔′_) inl′)) ⊚ g + p′ = trans (cong (_⊚_ f) fmap-⊎F-inl) (trans p (cong (λ w → (idm ⊕ w) ⊚ g) $ sym fmap-⊎F-inl)) + + -- an instance of uniformity for inr + †-inr : ∀ {X Y Z : Obj} {f : (Z + X) ➔ Y + (Z + X)} {g : X ➔ Y + X} + → f ⊚ inr ≡ (idm ⊕ inr) ⊚ g → f † ⊚ inr ≡ g † + †-inr {X} {Y} {Z} {f = f} {g = g} p = + begin + f † ⊚ inr + ≡˘⟨ cong (_⊚_ (f †)) fmap-⊎F-inr ⟩ + f † ⊚ fmap (⊎F→ (X ➔′_) inr′) + ≡⟨ uni p′ ⟩ + g † + ∎ + where + p′ : f ⊚ fmap (⊎F→ (X ➔′_) inr′) ≡ (idm ⊕ fmap (⊎F→ (X ➔′_) inr′)) ⊚ g + p′ = trans (cong (_⊚_ f) fmap-⊎F-inr) $ trans p (cong (λ w → (idm ⊕ w) ⊚ g) (sym fmap-⊎F-inr)) + + -- an instance of uniformity for swap + †-swap : ∀ {X Y Z : Obj} {f : (X + Y) ➔ Z + (X + Y)} + → f † ⊚ swap ≡ ((idm ⊕ swap) ⊚ (f ⊚ swap)) † + + †-swap {X} {Y} {Z} {f = f} = + begin + f † ⊚ swap + ≡˘⟨ ⊚-cong₂ fmap-swap′ ⟩ + f † ⊚ (fmap swap′) + ≡⟨ + uni (trans (sym ⊚-unitˡ) $ trans + (⊚-cong₁ $ trans (trans (sym [inl,inr]) $ + ([]-destruct + (trans (sym ⊚-unitʳ) $ ⊚-cong₂ $ sym ⊚-unitˡ) + (trans (sym ⊚-unitʳ) $ ⊚-cong₂ $ trans (sym swap-swap) $ + ⊚-cong (sym fmap-swap′) (sym fmap-swap′)) + )) + (sym ⊕-⊕)) $ sym ⊚-assoc) + ⟩ + ((idm ⊕ fmap swap′) ⊚ (f ⊚ fmap swap′)) † + ≡⟨ cong2 (λ w w′ → ((idm ⊕ w) ⊚ (f ⊚ w′)) †) fmap-swap′ fmap-swap′ ⟩ + ((idm ⊕ swap) ⊚ (f ⊚ swap)) † + ∎ + where + swap′ : ∀ {X Y : Obj} → X + Y ➔′ Y + X + swap′ {X} {Y} = ⊎F→ ((X + Y) ➔′_) (⊎F→ (_➔′ Y +′ X) [ inr′ , inl′ ]′) + + fmap-swap′ : ∀ {X Y : Obj} → fmap (swap′{X}{Y}) ≡ swap{X}{Y} + fmap-swap′{X}{Y} = + begin + fmap (swap′{X}{Y}) + ≡˘⟨ subst-app ((X + Y) ➔′_) {B₂ = (X + Y) ➔_} (λ _ → fmap) ⊎F ⟩ + ⊎F→ (X + Y ➔_) (fmap (⊎F→ (_➔′ Y +′ X) [ inr′ , inl′ ]′)) + ≡˘⟨ cong (⊎F→ (X + Y ➔_)) (subst-app (_➔′ Y +′ X) {B₂ = _➔ Y +′ X} (λ _ → fmap) ⊎F) ⟩ + ⊎F→ (X + Y ➔_) (⊎F→ (_➔ Y +′ X) (fmap [ inr′ , inl′ ]′)) + ≡˘⟨ cong (⊎F→ (X + Y ➔_)) []F ⟩ + ⊎F→ (X + Y ➔_) ([ fmap inr′ , fmap inl′ ]) + ≡˘⟨ ⊎-destruct (trans []-inl (⊎F→⊚ h inl)) (trans []-inr (⊎F→⊚ h inr)) ⟩ + [ ⊎F→ (_➔_ X) (h ⊚ inl) , ⊎F→ (_➔_ Y) (h ⊚ inr) ] + ≡⟨ + []-destruct + (trans (cong (⊎F→ (_➔_ X)) []-inl) $ sym inrF) + (trans (cong (⊎F→ (_➔_ Y)) []-inr) $ sym inlF) + ⟩ + [ inr , inl ] + ∎ + where h = [ fmap inr′ , fmap inl′ ] + + bekić : ∀ {X Y Z : Obj} {f : X ➔ (Y + X) + Z} {g : Z ➔ (Y + X) + Z} + → [([ idm , g † ] ⊚ f)† , [ idm , ([ idm , g † ] ⊚ f)† ] ⊚ g † ] + ≡ ([ idm ⊕ inl , inr ⊚ inr ] ⊚ [ f , g ]) † + + bekić {f = f} {g = g} = + begin + [ ([ idm , g † ] ⊚ f) † , [ idm , ([ idm , g † ] ⊚ f) † ] ⊚ g † ] + -- using bekić₁ + ≡⟨ bekić₁ ⟩ + ([ (idm ⊕ inl) ⊚ ([ idm , g † ] ⊚ f) , (idm ⊕ inl) ⊚ g † ] †) + ≡⟨ cong _† $ []-cong₁ ⊚-assoc ⟩ + ([ ((idm ⊕ inl) ⊚ [ idm , g † ]) ⊚ f , (idm ⊕ inl) ⊚ g † ] †) + ≡⟨ cong _† $ []-cong₁ $ trans (⊚-cong₁ ⊚-distrib-[]) $ ⊚-cong₁ $ []-cong₁ ⊚-unitʳ ⟩ + [ [ idm ⊕ inl , (idm ⊕ inl) ⊚ g † ] ⊚ f , (idm ⊕ inl) ⊚ g † ] † + ≡˘⟨ cong _† $ []-cong₁ $ ⊚-cong₁ $ trans []-⊕ ([]-destruct ⊚-unitˡ ⊚-unitʳ) ⟩ + [ ([ idm , (idm ⊕ inl) ⊚ g † ] ⊚ ((idm ⊕ inl) ⊕ idm)) ⊚ f , (idm ⊕ inl) ⊚ g † ] † + ≡˘⟨ cong _† $ []-cong₁ $ ⊚-assoc ⟩ + [ [ idm , (idm ⊕ inl) ⊚ g † ] ⊚ (((idm ⊕ inl) ⊕ idm) ⊚ f) , (idm ⊕ inl) ⊚ g † ] † + -- using naturality + ≡⟨ cong _† $ []-destruct (⊚-cong₁ $ []-cong₂ $ sym nat) (sym nat) ⟩ + [ [ idm , (((idm ⊕ inl) ⊕ idm) ⊚ g) † ] ⊚ (((idm ⊕ inl) ⊕ idm) ⊚ f) , (((idm ⊕ inl) ⊕ idm) ⊚ g) † ] † + -- using bekić₂ + ≡⟨ cong _† $ trans bekić₂ $ cong _† $ sym ⊚-distrib-[] ⟩ + ((idm ⊕ inr) ⊚ [ ((idm ⊕ inl) ⊕ idm) ⊚ f , ((idm ⊕ inl) ⊕ idm) ⊚ g ]) † † + ≡⟨ cong (_† ∘ _†) $ ⊚-cong₂ $ sym ⊚-distrib-[] ⟩ + ((idm ⊕ inr) ⊚ (((idm ⊕ inl) ⊕ idm) ⊚ [ f , g ])) † † + ≡⟨ cong (_† ∘ _†) $ trans ⊚-assoc $ ⊚-cong₁ $ trans ⊕-⊕ $ + []-destruct (⊚-cong₂ ⊚-unitˡ) (⊚-cong₂ ⊚-unitʳ) ⟩ + (((idm ⊕ inl) ⊕ inr) ⊚ [ f , g ]) † † + -- using codiagonal + ≡˘⟨ cod ⟩ + ([ idm , inr ] ⊚ (((idm ⊕ inl) ⊕ inr) ⊚ [ f , g ])) † + ≡⟨ cong _† ⊚-assoc ⟩ + (([ idm , inr ] ⊚ ((idm ⊕ inl) ⊕ inr)) ⊚ [ f , g ]) † + ≡⟨ cong _† $ ⊚-cong₁ $ trans []-⊕ $ []-cong₁ ⊚-unitˡ ⟩ + ([(idm ⊕ inl) , inr ⊚ inr ] ⊚ [ f , g ]) † + ∎ + + where + + -- one instance of the Bekić law + bekić₁ : ∀ {X Y Z : Obj} {f : X ➔ Y + X}{g : Z ➔ Y + X} + → [ f † , [ idm , f † ] ⊚ g ] ≡ [ (idm ⊕ inl) ⊚ f , (idm ⊕ inl) ⊚ g ] † + + bekić₁ {f = f} {g = g} = + begin + [ f † , [ idm , f † ] ⊚ g ] + ≡˘⟨ []-destruct (†-inl []-inl) $ ⊚-cong₁ $ []-cong₂ $ †-inl []-inl ⟩ + [ h † ⊚ inl , [ idm , h † ⊚ inl ] ⊚ g ] + ≡˘⟨ []-cong₂ $ ⊚-cong₁ $ []-cong₁ $ ⊚-unitʳ ⟩ + [ h † ⊚ inl , [ idm ⊚ idm , h † ⊚ inl ] ⊚ g ] + ≡˘⟨ []-cong₂ $ ⊚-cong₁ $ []-⊕ ⟩ + [ h † ⊚ inl , ([ idm , h † ] ⊚ (idm ⊕ inl)) ⊚ g ] + ≡˘⟨ []-cong₂ $ ⊚-assoc ⟩ + [ h † ⊚ inl , [ idm , h † ] ⊚ ((idm ⊕ inl) ⊚ g) ] + ≡˘⟨ []-cong₂ $ ⊚-cong₂ $ []-inr ⟩ + [ h † ⊚ inl , [ idm , h † ] ⊚ (h ⊚ inr) ] + ≡⟨ []-cong₂ $ ⊚-assoc ⟩ + [ h † ⊚ inl , ([ idm , h † ] ⊚ h) ⊚ inr ] + ≡⟨ []-cong₂ $ ⊚-cong₁ $ fix ⟩ + [ h † ⊚ inl , h † ⊚ inr ] + ≡˘⟨ ⊚-distrib-[] ⟩ + h † ⊚ [ inl , inr ] + ≡⟨ ⊚-cong₂ [inl,inr] ⟩ + h † ⊚ idm + ≡⟨ ⊚-unitʳ ⟩ + h † + ∎ + where h = [ (idm ⊕ inl) ⊚ f , (idm ⊕ inl) ⊚ g ] + + -- another instance of the Bekić law + bekić₂ : ∀ {X Y Z : Obj} {f : X ➔ Y + X} {g : Z ➔ Y + X} + → [ [ idm , f † ] ⊚ g , f † ] ≡ [ (idm ⊕ inr) ⊚ g , (idm ⊕ inr) ⊚ f ] † + bekić₂ {f = f} {g = g} = + begin + [ [ idm , f † ] ⊚ g , f † ] + ≡˘⟨ []-destruct (⊚-cong₁ $ []-cong₂ $ †-inr []-inr) (†-inr []-inr) ⟩ + [ [ idm , h † ⊚ inr ] ⊚ g , h † ⊚ inr ] + ≡˘⟨ []-cong₁ $ ⊚-cong₁ $ []-cong₁ $ ⊚-unitʳ ⟩ + [ [ idm ⊚ idm , h † ⊚ inr ] ⊚ g , h † ⊚ inr ] + ≡˘⟨ []-cong₁ $ ⊚-cong₁ $ []-⊕ ⟩ + [ ([ idm , h † ] ⊚ (idm ⊕ inr)) ⊚ g , h † ⊚ inr ] + ≡˘⟨ []-cong₁ $ ⊚-assoc ⟩ + [ [ idm , h † ] ⊚ ((idm ⊕ inr) ⊚ g) , h † ⊚ inr ] + ≡˘⟨ []-cong₁ $ ⊚-cong₂ $ []-inl ⟩ + [ [ idm , h † ] ⊚ (h ⊚ inl) , h † ⊚ inr ] + ≡⟨ []-cong₁ $ ⊚-assoc ⟩ + [ ([ idm , h † ] ⊚ h) ⊚ inl , h † ⊚ inr ] + ≡⟨ []-cong₁ $ ⊚-cong₁ $ fix ⟩ + [ h † ⊚ inl , h † ⊚ inr ] + ≡˘⟨ ⊚-distrib-[] ⟩ + h † ⊚ [ inl , inr ] + ≡⟨ ⊚-cong₂ [inl,inr] ⟩ + h † ⊚ idm + ≡⟨ ⊚-unitʳ ⟩ + h † + ∎ + where h = [ (idm ⊕ inr) ⊚ g , (idm ⊕ inr) ⊚ f ] + + -- Dinaturality + din : Din _† + din {g = g} {h = h} = + begin + ([ inl , h ] ⊚ g) † + ≡˘⟨ []-inl ⟩ + [([ inl , h ] ⊚ g) † , [ idm , ([ inl , h ] ⊚ g) † ] ⊚ h ] ⊚ inl + ≡˘⟨ ⊚-cong₁ helper₁ ⟩ + [ (idm ⊕ inr) ⊚ g , (idm ⊕ inl) ⊚ h ] † ⊚ inl + ≡⟨ trans (⊚-cong₁ (sym helper₂)) (trans (sym ⊚-assoc) (⊚-cong₂ []-inl)) ⟩ + [ (idm ⊕ inr) ⊚ h , (idm ⊕ inl) ⊚ g ] † ⊚ inr + -- using fix + ≡⟨ trans (⊚-cong₁ (sym fix)) (trans (sym ⊚-assoc) (trans (⊚-cong₂ []-inr) ⊚-assoc)) ⟩ + ([ idm , [ (idm ⊕ inr) ⊚ h , (idm ⊕ inl) ⊚ g ] † ] ⊚ (idm ⊕ inl)) ⊚ g + ≡⟨ ⊚-cong₁ (trans []-⊕ ([]-cong₁ ⊚-unitˡ)) ⟩ + [ idm , [ (idm ⊕ inr) ⊚ h , (idm ⊕ inl) ⊚ g ] † ⊚ inl ] ⊚ g + ≡⟨ trans (cong (λ w → [ idm , w ⊚ inl ] ⊚ g) helper₁) (cong (λ w → [ idm , w ] ⊚ g) []-inl) ⟩ + [ idm , ([ inl , g ] ⊚ h) † ] ⊚ g + ∎ + where + helper₁ : ∀ {X Y Z : Obj} {g : X ➔ Y + Z} {h : Z ➔ Y + X} → + [ (idm ⊕ inr) ⊚ g , (idm ⊕ inl) ⊚ h ] † ≡ [([ inl , h ] ⊚ g) † , [ idm , ([ inl , h ] ⊚ g) † ] ⊚ h ] + helper₁{X}{Y}{Z}{g = g}{h = h} = + begin + [ (idm ⊕ inr) ⊚ g , (idm ⊕ inl) ⊚ h ] † + ≡˘⟨ cong _† $ []-cong₁ $ ⊚-cong₁ $ []-destruct []-inl ⊚-unitʳ ⟩ + ([ [ (idm ⊕ inl) ⊚ inl , (inr ⊚ inr) ⊚ idm ] ⊚ g , (idm ⊕ inl) ⊚ h ] †) + ≡˘⟨ cong _† $ trans ⊚-distrib-[] $ + []-destruct + (trans ⊚-assoc $ ⊚-cong₁ []-⊕) + (trans ⊚-assoc $ ⊚-cong₁ []-inl) ⟩ + (([ idm ⊕ inl , inr ⊚ inr ] ⊚ [ (inl ⊕ idm) ⊚ g , inl ⊚ h ]) †) + ≡˘⟨ bekić{f = (inl ⊕ idm) ⊚ g}{g = inl ⊚ h} ⟩ + [ ([ idm , (inl ⊚ h) † ] ⊚ ((inl ⊕ idm) ⊚ g))† , + [ idm , ([ idm , (inl ⊚ h) † ] ⊚ ((inl ⊕ idm) ⊚ g))† ] ⊚ ((inl ⊚ h) †) ] + ≡⟨ cong2 (λ w₁ w₂ → [ w₁ † , [ idm , w₂ † ] ⊚ ((inl ⊚ h) †) ]) + (trans ⊚-assoc $ cong (_⊚ g) $ trans []-⊕ $ []-destruct ⊚-unitˡ ⊚-unitʳ) + (trans ⊚-assoc $ cong (_⊚ g) $ trans []-⊕ $ []-destruct ⊚-unitˡ ⊚-unitʳ) ⟩ + [ ([ inl , (inl ⊚ h) † ] ⊚ g) † , [ idm , ([ inl , (inl ⊚ h) † ] ⊚ g) † ] ⊚ ((inl ⊚ h) †) ] + ≡⟨ []-destruct + (cong _† $ ⊚-cong₁ $ []-cong₂ inl-h†) + (cong2 (λ w₁ w₂ → [ idm , ([ inl , w₁ ] ⊚ g) † ] ⊚ w₂) inl-h† inl-h†) ⟩ + [([ inl , h ] ⊚ g) † , [ idm , ([ inl , h ] ⊚ g)† ] ⊚ h ] + ∎ + where + inl-h† : (inl ⊚ h) † ≡ h + inl-h† = trans (sym fix) $ trans ⊚-assoc $ trans (⊚-cong₁ []-inl) ⊚-unitˡ + + helper₂ : ∀ {X Y Z : Obj} {g : X ➔ Y + Z} {h : Z ➔ Y + X} → + [ (idm ⊕ inr) ⊚ g , (idm ⊕ inl) ⊚ h ] † ⊚ swap ≡ [ (idm ⊕ inr) ⊚ h , (idm ⊕ inl) ⊚ g ] † + helper₂ = trans †-swap $ + cong _† $ trans (⊚-cong₂ []-swap) (trans ⊚-distrib-[] $ []-destruct + (trans ⊚-assoc $ ⊚-cong₁ $ trans ⊕-⊕ $ []-destruct (⊚-cong₂ ⊚-unitˡ) $ ⊚-cong₂ []-inl) + (trans ⊚-assoc $ ⊚-cong₁ $ trans ⊕-⊕ $ []-destruct (⊚-cong₂ ⊚-unitˡ) $ ⊚-cong₂ []-inr)) + + +module _ (It : ElgotIteration) {D : Category Ob} {CoC-D : Co-Cartesian D} + {F : Functor D C id} (J : CoC-Functor CoC-D CoC F) where + + TotalUniConway→ConwayIteration : TotalUniConway It J → ConwayIteration It + TotalUniConway→ConwayIteration TC = + record { + nat = nat ; + din = din ; + cod = cod + } + + where + open TotalUniConway TC