minor

src/Monad/Instance/K/EquationalLifting.lagda.md

@@ -32,6 +32,7 @@ open kleisliK using (extend)
 open monadK using (μ)
 open FreeObject using (*-uniq)
 open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
+open strongK using (strengthen)
 
 -- some helper definitions to make our life easier
 private
@@ -93,14 +94,21 @@ From this we can follow that the kleisli category of **K** is a *restriction cat
 ```agda
 kleisli-restriction' : Restriction (Kleisli monadK)
 kleisli-restriction' = record
-  { _↓ = λ f → K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩
+  { _↓ = _↓
   ; pidʳ = λ {A} {B} {f} → begin 
-    (μ.η _ ∘ K.₁ f) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC {A} , f ⟩ ≈⟨ {!   !} ⟩ 
+    (μ.η _ ∘ K.₁ f) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC {A} , f ⟩ ≈⟨ pullʳ (sym-assoc ○ pullˡ ((sym K.homomorphism) ⟩∘⟨refl)) ⟩ 
-    (μ.η _ ∘ K.₁ f) ∘ K.₁ π₁ ∘ τ _ ∘ (idC ⁂ f) ∘ ⟨ idC , idC ⟩ ≈⟨ {!   !} ⟩ 
+    μ.η _ ∘ (K.₁ (f ∘ π₁) ∘ τ _) ∘ ⟨ idC , f ⟩ ≈˘⟨ refl⟩∘⟨ ((K.F-resp-≈ π₁∘⁂) ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
-    (μ.η B ∘ K.₁ f) ∘ K.₁ π₁ ∘ τ _ ∘ (idC ⁂ f) ∘ ⟨ idC , idC ⟩ ≈⟨ {!   !} ⟩ 
+    μ.η _ ∘ (K.₁ (π₁ ∘ (f ⁂ idC)) ∘ τ _) ∘ ⟨ idC , f ⟩ ≈˘⟨ refl⟩∘⟨ (pullˡ (pullˡ (sym K.homomorphism))) ⟩ 
-    {!   !} ≈⟨ {!   !} ⟩ 
+    μ.η _ ∘ K.₁ π₁ ∘ (K.₁ (f ⁂ idC) ∘ τ _) ∘ ⟨ idC , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (sym (strengthen.commute _) ○ refl⟩∘⟨ ⁂-cong₂ refl K.identity)) ⟩ 
-    {!   !} ≈⟨ {!   !} ⟩ 
+    μ.η _ ∘ K.₁ π₁ ∘ τ _ ∘ (f ⁂ idC) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ 
-    (μ.η B ∘ K.₁ f) ∘ η A ≈⟨ {!   !} ⟩ 
+    μ.η _ ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ f , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ Δ∘ ⟩ 
+    μ.η _ ∘ K.₁ π₁ ∘ (τ _ ∘ Δ) ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ equationalLifting ⟩∘⟨refl ⟩ 
+    μ.η _ ∘ K.₁ π₁ ∘ (K.₁ ⟨ η _ , idC ⟩) ∘ f ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym K.homomorphism ○ K.F-resp-≈ ⁂∘Δ) ⟩
+    μ.η _ ∘ K.₁ π₁ ∘ K.₁ (η _ ⁂ idC) ∘ K.₁ Δ ∘ f ≈⟨ refl⟩∘⟨ (pullˡ (sym K.homomorphism)) ⟩ 
+    μ.η _ ∘ K.₁ (π₁ ∘ (η _ ⁂ idC)) ∘ K.₁ Δ ∘ f ≈⟨ refl⟩∘⟨ ((K.F-resp-≈ π₁∘⁂) ⟩∘⟨refl) ⟩ 
+    μ.η _ ∘ K.₁ (η _ ∘ π₁) ∘ K.₁ Δ ∘ f ≈˘⟨ refl⟩∘⟨ (pullˡ (sym K.homomorphism)) ⟩ 
+    μ.η _ ∘ K.₁ (η _) ∘ K.₁ π₁ ∘ K.₁ Δ ∘ f ≈⟨ cancelˡ monadK.identityˡ ⟩ 
+    K.₁ π₁ ∘ K.₁ Δ ∘ f ≈⟨ cancelˡ (sym K.homomorphism ○ K.F-resp-≈ project₁ ○ K.identity) ⟩ 
     f ∎
   ; ↓-comm = λ {A} {B} {D} {f} {g} → begin 
     (μ.η _ ∘ K.₁ (K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩)) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩ ≈⟨ pullˡ (pullʳ (sym K.homomorphism)) ⟩ 
@@ -115,4 +123,23 @@ kleisli-restriction' = record
   ; ↓-skew-comm = {!   !}
   ; ↓-cong = λ eq → refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl eq
   }
+  where
+    _↓ : ∀ {A B : Obj} → A ⇒ K.₀ B → A ⇒ K.₀ A
+    f ↓ = K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩
+    ↓-comm' : ∀ {A B C : Obj} {f : A ⇒ K.₀ B} {g : A ⇒ K.₀ C} → extend (f ↓) ∘ g ↓ ≈ extend (g ↓) ∘ f ↓
+    ↓-comm' {A} {B} {C} {f} {g} = begin 
+      (μ.η _ ∘ K.₁ (K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩)) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩ ≈⟨ {!   !} ⟩ 
+      {!   !} ≈⟨ {!   !} ⟩ 
+      {!   !} ≈⟨ {!   !} ⟩ 
+      {!   !} ≈⟨ {!   !} ⟩ 
+      (μ.η _ ∘ K.₁ (K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩)) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ∎
+      where
+        f-helper : μ.η _ ∘ K.₁ (K.₁ π₁) ∘ K.₁ (τ _) ∘ K.₁ ⟨ idC , f ⟩ ≈ μ.η _ ∘ K.₁ π₁ ∘ τ _ ∘ Δ
+        f-helper = sym (begin 
+          μ.η _ ∘ K.₁ π₁ ∘ τ _ ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ equationalLifting ⟩ 
+          μ.η A ∘ K.₁ π₁ ∘ K.₁ ⟨ η A , idC ⟩ ≈⟨ refl⟩∘⟨ sym K.homomorphism ⟩ 
+          μ.η A ∘ K.₁ (π₁ ∘ ⟨ η A , idC ⟩) ≈⟨ {!   !} ⟩ 
+          μ.η A ∘ K.₁ (η A) ≈⟨ {!   !} ⟩ 
+          {!   !} ≈⟨ {!   !} ⟩ 
+          μ.η _ ∘ K.₁ (K.₁ π₁) ∘ K.₁ (τ _) ∘ K.₁ ⟨ idC , f ⟩ ∎)
 ```

src/Monad/Instance/K/PreElgot.lagda.md

@@ -33,7 +33,9 @@ module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK
 
   open HomReasoning
   open Equiv
+  open M C
   open MR C
+  open import Categories.Morphism.Properties C
   open kleisliK using (extend)
   open monadK using (η; μ)
   open strongK using (strengthen)
@@ -202,6 +204,20 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
     (g ⇂ f) ∘ h ≈⟨ ⇂∘ ⟩ 
     ((g ∘ h) ⇂ (f ∘ h)) ∎
 
+  ⊑-monoʳ : ∀ {A X Y} {f g : X ⇒ K.₀ Y} {h : A ⇒ K.₀ X} → f ⊑ g → (extend f ∘ h) ⊑ (extend g ∘ h)
+  ⊑-monoʳ {A} {X} {Y} {f} {g} {h} leq = sym (begin 
+    ((extend g ∘ h) ⇂ (extend f ∘ h)) ≈⟨ restrict-law (extend g ∘ h) (extend f ∘ h) ⟩ 
+    extend (extend g ∘ h) ∘ (extend f ∘ h)↓ ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩ 
+    extend g ∘ extend h ∘ (extend f ∘ h) ↓ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ↓-cong (sym (pullˡ (kleisliK.sym-assoc ○ kleisliK.extend-≈ leq'))) ⟩ 
+    extend g ∘ extend h ∘ (extend g ∘ extend (f ↓) ∘ h) ↓ ≈⟨ refl⟩∘⟨ {!   !} ⟩ -- RST₄ + kleisliK.sym-assoc inside 
+    extend g ∘ extend ((extend g ∘ (f ↓)) ↓) ∘ h ≈⟨ {!   !} ⟩ -- RST₃
+    extend g ∘ extend (g ↓) ∘ extend (f ↓) ∘ h ≈⟨ {!   !} ⟩ -- RST₁
+    extend g ∘ extend (f ↓) ∘ h ≈⟨ pullˡ (kleisliK.sym-assoc ○ kleisliK.extend-≈ leq') ⟩ 
+    extend f ∘ h ∎)
+    where
+      leq' : extend g ∘ f ↓ ≈ f
+      leq' = sym (restrict-law g f) ○ sym leq
+
   extend-⊑ : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ⊑ g → extend f ⊑ extend g
   extend-⊑ {X} {Y} {f} {g} fg = begin 
     extend f ≈⟨ kleisliK.extend-≈ fg ⟩ 
@@ -392,81 +408,74 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
         extend π₁ ∘ (K.₁ (g ⁂ idC) ∘ τ (X , N)) ∘ ⟨ idC , (h #) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ pullˡ (pullˡ (extend∘F₁ monadK π₁ (g ⁂ idC))) ⟩ 
         (extend (π₁ ∘ (g ⁂ idC)) ∘ τ _) ∘ ⟨ idC , (h #) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ assoc ○ (kleisliK.extend-≈ π₁∘⁂) ⟩∘⟨refl ⟩ 
         extend (g ∘ π₁) ∘ τ (X , N) ∘ ⟨ idC , (h #) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ∎)
-      -- to show eq₁ we strengthen the goal:
+
-      w-fact : w ∘ (idC ⁂ s) ≈ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w
+      case'_inl_inr_ : ∀ {X Y Z U} → X ⇒ Y + Z → Y ⇒ U → Z ⇒ U → X ⇒ U
-      w-fact = begin 
+      case' f inl g inr h = [ g , h ] ∘ f
-        w ∘ (idC ⁂ s)                                                                    ≈⟨ p-rec-IS _ _ ⟩ 
+
-        ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _                          ≈⟨ pullʳ (pullʳ ⟨⟩∘) ⟩
+      case_inl_inr_ : ∀ {X Y Z U} → X ⇒ Y + Z → X × Y ⇒ U → X × Z ⇒ U → X ⇒ U
-        [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ π₁) ∘ φ' _ _ , ((f ∘ π₁) ∘ π₂) ∘ φ' _ _ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (assoc ○ identityˡ) (assoc ○ pullʳ (π₁∘π₂∘φ' _ _)) ⟩ 
+      case f inl g inr h = [ g , h ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩
-        [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩                                     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (p-induction ⟨ idC , f ⟩ {!   !} ⟨ w , f ∘ π₁ ⟩ (sym (⟨⟩∘ ○ ⟨⟩-cong₂ (p-rec-IB idC _) (cancelʳ project₁))) (sym {!   !})) ⟩ 
+
-        [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ p-rec ⟨ idC , f ⟩ {!   !}                                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ p-induction ⟨ idC , f ⟩ {!   !} ⟨ w , f ∘ w ⟩ (sym (⟨⟩∘ ○ ⟨⟩-cong₂ (p-rec-IB idC _) (cancelʳ (p-rec-IB idC _)))) (sym {!   !}) ⟩ 
+      casecase' : ∀ {X Y Z U} (f : X ⇒ Y + Z) (g : Y ⇒ U) (h : Z ⇒ U) → case f inl (g ∘ π₂) inr (h ∘ π₂) ≈ case' f inl g inr h
-        [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ w ⟩                                      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ refl) ⟩ 
+      casecase' f g h = begin 
-        [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w                                    ∎
+        [ g ∘ π₂ , h ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ sym (pullˡ []∘+₁) ⟩
+        [ g , h ] ∘ (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ pullˡ distribute₂ ⟩ 
+        [ g , h ] ∘ π₂ ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ project₂ ⟩ 
+        [ g , h ] ∘ f ∎
+      
+      case-id : ∀ {X Y Z} (f : X ⇒ Y + Z) → case f inl (i₁ ∘ π₂) inr (i₂ ∘ π₂) ≈ f
+      case-id f = begin 
+        (case f inl i₁ ∘ π₂ inr (i₂ ∘ π₂)) ≈⟨ casecase' f i₁ i₂ ⟩ 
+        (case' f inl i₁ inr i₂) ≈⟨ elimˡ +-η ⟩ 
+        f ∎
+
+      case_inl$l->_$l&inr$r->_$r : ∀ {X Y Z U} → X ⇒ Y + Z → X × Y ⇒ U → X × Z ⇒ U → X ⇒ U
+      case f inl$l-> g $l&inr$r-> h $r = [ g , h ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩
+
+      case∘ˡ : ∀ {X Y Z U V} (f : X ⇒ Y + Z) (g : X × Y ⇒ U) (h : X × Z ⇒ U) (l : U ⇒ V) → l ∘ (case f inl g inr h) ≈ case f inl (l ∘ g) inr (l ∘ h)
+      case∘ˡ f g h l = pullˡ ∘[]
+
+      case∘ʳ : ∀ {X Y Z U V} (f : X ⇒ Y + Z) (g : X × Y ⇒ U) (h : X × Z ⇒ U) (r : V ⇒ X) → (case f inl g inr h) ∘ r ≈ case f ∘ r inl (g ∘ (r ⁂ idC)) inr (h ∘ (r ⁂ idC))
+      case∘ʳ f g h r = begin 
+        (case f inl g inr h) ∘ r ≈⟨ pullʳ (pullʳ ⟨⟩∘) ⟩ 
+        [ g , h ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ r , f ∘ r ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ id-comm identityˡ) ⟩ 
+        [ g , h ] ∘ distributeˡ⁻¹ ∘ (r ⁂ idC) ∘ ⟨ idC , f ∘ r ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (refl⟩∘⟨ (⁂-cong₂ refl (sym ([]-unique id-comm-sym id-comm-sym))) ○ sym (distribute₁ r idC idC))) ⟩ 
+        [ g , h ] ∘ (((r ⁂ idC) +₁ (r ⁂ idC)) ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ r ⟩ ≈⟨ pullˡ (pullˡ []∘+₁) ○ assoc ⟩ 
+        (case f ∘ r inl (g ∘ (r ⁂ idC)) inr (h ∘ (r ⁂ idC))) ∎
+
+      case⟩_⟨inl⟩_⟨inr⟩_ : ∀ {X Y Z U} {f f' : X ⇒ Y + Z} {g g' : X × Y ⇒ U} {h h' : X × Z ⇒ U} → f ≈ f' → g ≈ g' → h ≈ h' → case f inl g inr h ≈ case f' inl g' inr h'
+      case⟩ f≈f' ⟨inl⟩ g≈g' ⟨inr⟩ h≈h' = []-cong₂ g≈g' h≈h' ⟩∘⟨ refl ⟩∘⟨ ⟨⟩-cong₂ refl f≈f'
+
+      case-nested : ∀ {X Y Z U} (f : X ⇒ Y + Z) (g : X × Y ⇒ U) (g' : X × Y ⇒ U) (h : X × Z ⇒ U) → case f inl g inr ((case f inl g' inr h) ∘ π₁) ≈ case f inl g inr h
+      case-nested f g g' h = begin 
+        [ g , (case f inl g' inr h) ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ refl ⟩ 
+        [ g , ([ g' , h ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩) ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈˘⟨ ([]-cong₂ (elimʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ (cancelˡ project₁) (cancelˡ identity²) ○ ⁂-η)) (sym (pullʳ (pullʳ (sym π₁∘⁂))))) ⟩∘⟨refl ⟩
+        [ g ∘ (π₁ ⁂ idC) ∘ (⟨ idC , f ⟩ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ∘ (⟨ idC , f ⟩ ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ assoc assoc²') ⟩
+        [ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ]  ∘ ((⟨ idC , f ⟩ ⁂ idC) +₁ (⟨ idC , f ⟩ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ pullˡ (distribute₁ ⟨ idC , f ⟩ idC idC ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym)) ⟩
+        [ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ (distributeˡ⁻¹ ∘ (⟨ idC , f ⟩ ⁂ idC)) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ (pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ)) ⟩
+        [ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ ⟨ idC , f ⟩ , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl project₂ ⟩
+        [ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ ⟨ idC , f ⟩ , π₂ ∘ ⟨ idC , f ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩∘ ○ refl⟩∘⟨ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) ⟩
+        [ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩ ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ pullˡ helper ⟩
+        [ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ ((⟨ (idC ⁂ i₁) , π₂ ⟩ +₁ ⟨ (idC ⁂ i₂) , π₂ ⟩) ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ assoc ○ pullˡ ([]∘+₁ ○ []-cong₂ assoc assoc²') ⟩
+        [ g ∘ (π₁ ⁂ idC) ∘ ⟨ (idC ⁂ i₁) , π₂ ⟩ , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ∘ ⟨ (idC ⁂ i₂) , π₂ ⟩ ] ∘  distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ ([]-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ refl⟩∘⟨ project₁)) ⟩∘⟨refl ⟩
+        [ g ∘ ⟨ π₁ ∘ (idC ⁂ i₁) , idC ∘ π₂ ⟩ , [ g' , h ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂) ] ∘  distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ ([]-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ π₁∘⁂ refl)) (refl⟩∘⟨ dstr-law₂)) ⟩∘⟨refl ⟩
+        [ g ∘ ⟨ idC ∘ π₁ , idC ∘ π₂ ⟩ , [ g' , h ] ∘ i₂ ] ∘  distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ []-cong₂ (elimʳ (⟨⟩-cong₂ identityˡ identityˡ ○ ⁂-η)) inject₂ ⟩∘⟨refl ⟩
+        [ g , h ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∎
         where
-          -- TODO this just wont work... maybe w-fact' is wrong, maybe im just missing the link in between
+          helper : distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩ ≈ (⟨ (idC ⁂ i₁) , π₂ ⟩ +₁ ⟨ (idC ⁂ i₂) , π₂ ⟩) ∘ distributeˡ⁻¹
-          -- maybe step: ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f ∘ π₁)
+          helper = Iso⇒Epi (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩) ((⟨ idC ⁂ i₁ , π₂ ⟩ +₁ ⟨ idC ⁂ i₂ , π₂ ⟩) ∘ distributeˡ⁻¹) (begin 
-          ind-base : w ∘ (idC ⁂ s) ∘ ⟨ idC , z ∘ ! ⟩ ≈ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w) ∘ ⟨ idC , z ∘ ! ⟩
+            (distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩) ∘ distributeˡ ≈⟨ ∘[] ⟩ 
-          ind-base = begin 
+            [ ((distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩) ∘ (idC ⁂ i₁)) , ((distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩) ∘ (idC ⁂ i₂)) ] ≈⟨ []-cong₂ (pullʳ ⟨⟩∘) (pullʳ ⟨⟩∘) ⟩ 
-            w ∘ (idC ⁂ s) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ pullˡ (p-rec-IS _ _) ⟩ 
+            [ (distributeˡ⁻¹ ∘ ⟨ idC ∘ (idC ⁂ i₁) , π₂ ∘ (idC ⁂ i₁) ⟩) , (distributeˡ⁻¹ ∘ ⟨ idC ∘ (idC ⁂ i₂) , π₂ ∘ (idC ⁂ i₂) ⟩) ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ π₂∘⁂)) (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ π₂∘⁂)) ⟩ 
-            (([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ pullʳ (sym commute₁) ⟩ 
+            [ distributeˡ⁻¹ ∘ ⟨ (idC ⁂ i₁) , i₁ ∘ π₂ ⟩ , distributeˡ⁻¹ ∘ ⟨ (idC ⁂ i₂) , i₂ ∘ π₂ ⟩ ] ≈˘⟨ []-cong₂ (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)) (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)) ⟩ 
-            ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ idC , ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ pullʳ (pullʳ ⁂∘⟨⟩) ⟩ 
+            [ distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ (idC ⁂ i₁) , π₂ ⟩ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ (idC ⁂ i₂) , π₂ ⟩ ] ≈⟨ []-cong₂ (pullˡ dstr-law₁) (pullˡ dstr-law₂) ⟩
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ idC , (f ∘ π₁) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identity² (cancelʳ project₁) ⟩ 
+            [ i₁ ∘ ⟨ (idC ⁂ i₁) , π₂ ⟩ , i₂ ∘ ⟨ (idC ⁂ i₂) , π₂ ⟩ ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩ 
+            ((⟨ (idC ⁂ i₁) , π₂ ⟩ +₁ ⟨ (idC ⁂ i₂) , π₂ ⟩) ∘ distributeˡ⁻¹) ∘ distributeˡ ∎)
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ idC ≈˘⟨ pullʳ (pullʳ (pullʳ (p-rec-IB _ _))) ⟩ 
+
-            ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w) ∘ ⟨ idC , z ∘ ! ⟩ ∎
+      -- to show eq₁ we strengthen the goal:
-          ind-step : w ∘ (idC ⁂ s) ∘ (idC ⁂ s) ≈ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w ∘ (idC ⁂ s)
+      w' : X × N ⇒ X
-          ind-step = begin 
+      w' = p-rec idC {! case ? inl ? inr ?  !} -- ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) 
-            w ∘ (idC ⁂ s) ∘ (idC ⁂ s) ≈⟨ pullˡ (p-rec-IS _ _) ⟩ 
+      w : X × N ⇒ X
-            (([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _) ∘ (idC ⁂ s) ≈⟨ pullʳ (sym commute₂) ⟩ 
+      w = universal idC (case f inl π₁ inr π₂) --([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩)
-            ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁) , ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ⟩ ∘ φ' _ _ ≈⟨ pullʳ (pullʳ (pullˡ ⁂∘⟨⟩)) ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁) , (f ∘ π₁) ∘ ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ⟩ ∘ φ' _ _ ≈⟨ {!   !} ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , ((f ∘ π₁) ∘ ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩) ∘ φ' _ _ ⟩ ≈⟨ {!   !} ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , (f ∘ π₁ ∘ π₂) ∘ φ' _ _ ⟩ ≈⟨ {!   !} ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
-            {!   !} ≈⟨ {!   !} ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ [ π₁ ∘ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ [ π₁ , π₂ ] ∘ ((π₁ ⁂ idC) +₁ (π₁ ⁂ idC)) ∘  distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (π₁ ⁂ idC) ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩ ⟩ ≈˘⟨ {!   !} ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ π₁) ∘ φ' _ _ , ((f ∘ π₁) ∘ π₂) ∘ φ' _ _ ⟩ ⟩ ≈˘⟨ {!   !} ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , (f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ ⟩ ≈˘⟨ {!   !} ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁) , f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁) ⟩ ∘ φ' _ _ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ ⟨⟩∘ ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ p-rec-IS _ _ ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w ∘ (idC ⁂ s) ∎
-          help : π₁ ≈ [ π₁ ∘ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩
-          help = begin 
-            π₁ ≈⟨ {!   !} ⟩ 
-            {!   !} ≈⟨ {!   !} ⟩ 
-            [ w ∘ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
-            π₁ ∘ [ φ' _ _ ∘ π₁ , ⟨ π₂ , {!   !} ∘ (φ' _ _ ⁂ idC) ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
-            π₁ ∘ [ φ' _ _ ∘ π₁ , ⟨ π₂ ∘ (φ' _ _ ⁂ idC) , {!   !} ∘ (φ' _ _ ⁂ idC) ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
-            π₁ ∘ [ π₁ ∘ (φ' _ _ ⁂ idC) , ⟨ π₂ , {!   !} ⟩ ∘ (φ' _ _ ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
-            π₁ ∘ [ π₁ , ⟨ π₂ , {!   !} ⟩ ] ∘ ((φ' _ _ ⁂ idC) +₁ (φ' _ _ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
-            π₁ ∘ [ π₁ , ⟨ π₂ , {!   !} ⟩ ] ∘ distributeˡ⁻¹ ∘ (φ' _ _ ⁂ idC) ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
-            π₁ ∘ [ π₁ , ⟨ π₂ , {!   !} ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
-            [ π₁ ∘ π₁ , π₁ ∘ ⟨ π₂ , {!   !} ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
-            [ π₁ ∘ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ∎
-          helper : (idC ⁂ f ∘ π₁) ∘ φ' _ _ ≈ ⟨ w , f ∘ π₁ ⟩
-          helper = begin {!   !} ≈⟨ {!   !} ⟩ {!   !} ∎
-          IS₁ : ⟨ w , f ∘ π₁ ⟩ ∘ (idC ⁂ s) ≈ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f ∘ π₁) ∘ ⟨ ⟨ w , f ∘ π₁ ⟩ , idC ⟩
-          IS₁ = begin 
-            ⟨ w , f ∘ π₁ ⟩ ∘ (idC ⁂ s) ≈⟨ ⟨⟩∘ ⟩ 
-            ⟨ w ∘ (idC ⁂ s) , (f ∘ π₁) ∘ (idC ⁂ s) ⟩ ≈⟨ ⟨⟩-cong₂ (p-rec-IS idC _) (pullʳ π₁∘⁂) ⟩ 
-            ⟨ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ idC ∘ π₁ ⟩ ≈⟨ ⟨⟩-cong₂ (pullʳ (pullʳ ⟨⟩∘)) (refl⟩∘⟨ identityˡ) ⟩ 
-            ⟨ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ π₁) ∘ φ' _ _ , ((f ∘ π₁) ∘ π₂) ∘ φ' _ _ ⟩ , f ∘ π₁ ⟩ ≈⟨ ⟨⟩-cong₂ (refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (assoc ○ identityˡ) (assoc ○ pullʳ (π₁∘π₂∘φ' _ _))) refl ⟩ 
-            ⟨ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩ , f ∘ π₁ ⟩ ≈˘⟨ ⁂∘⟨⟩ ○ ⟨⟩-cong₂ assoc identityʳ ⟩ 
-            ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f ∘ π₁) ∘ ⟨ ⟨ w , f ∘ π₁ ⟩ , idC ⟩ ∎
-          IS₂ : ⟨ w , f ∘ w ⟩ ∘ (idC ⁂ s) ≈ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f ∘ π₁) ∘ ⟨ ⟨ w , f ∘ w ⟩ , idC ⟩
-          IS₂ = begin 
-            ⟨ w , f ∘ w ⟩ ∘ (idC ⁂ s) ≈⟨ ⟨⟩∘ ⟩ 
-            ⟨ w ∘ (idC ⁂ s) , (f ∘ w) ∘ (idC ⁂ s) ⟩ ≈⟨ ⟨⟩-cong₂ (p-rec-IS _ _) (pullʳ (p-rec-IS _ _)) ⟩ 
-            ⟨ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ ⟩ ≈⟨ ⟨⟩-cong₂ (pullʳ (pullʳ helper)) (refl⟩∘⟨ pullʳ (pullʳ helper)) ⟩ 
-            ⟨ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩ , f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
-            ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f) ∘ ⟨ ⟨ w , f ∘ π₁ ⟩ , [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
-            {!   !} ≈⟨ {!   !} ⟩ 
-            {!   !} ≈⟨ {!   !} ⟩ 
-            ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f) ∘ ⟨ ⟨ w , f ∘ w ⟩ , π₁ ⟩ ≈⟨ {!   !} ⟩ 
-            ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f ∘ π₁) ∘ ⟨ ⟨ w , f ∘ w ⟩ , idC ⟩ ∎ 
         
       -- TODO this depends on (8) and (9)
       stronger : ((extend [ i₂ # , f ]#⟩ ∘ τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩ ≈ f # ∘ w
@@ -475,9 +484,38 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
         ((π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ )# ≈⟨ #-Uniformity (algebras _) by-uni₂ ⟩ 
         f # ∘ w ∎
         where
+          f#⟩-fact : [ i₂ # , f ]#⟩ ∘ (idC ⁂ s) ≈ case (f ∘ w) inl π₂ inr (i₂ #)
+          f#⟩-fact = begin 
+            [ i₂ # , f ]#⟩ ∘ (idC ⁂ s) ≈⟨ {!   !} ⟩
+            universal (case f inl (π₂) inr (i₂ #)) {!  case f inl ? inr ? !} ≈⟨ sym (unique (sym IB₁) (sym IS₁)) ⟩
+            (case (f ∘ w) inl π₂ inr (i₂ #)) ∎
+            where
+              IB₁ : (case f ∘ w inl π₂ inr (i₂ #)) ∘ ⟨ idC , z ∘ ! ⟩ ≈ case f inl (π₂) inr (i₂ #)
+              IB₁ = begin 
+                (case f ∘ w inl π₂ inr (i₂ #)) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ case∘ʳ (f ∘ w) π₂ (i₂ #) ⟨ idC , z ∘ ! ⟩ ⟩ 
+                (case (f ∘ w) ∘ ⟨ idC , z ∘ ! ⟩ inl (π₂ ∘ (⟨ idC , z ∘ ! ⟩ ⁂ idC)) inr (i₂ # ∘ (⟨ idC , z ∘ ! ⟩ ⁂ idC))) ≈⟨ (case⟩ (cancelʳ (sym commute₁)) ⟨inl⟩ (π₂∘⁂ ○ identityˡ) ⟨inr⟩ {!   !}) ⟩ 
+                (case f inl (π₂) inr (i₂ #)) ∎
+              IS₁ : (case f ∘ w inl π₂ inr (i₂ #)) ∘ (idC ⁂ s) ≈ {!  (case f inl π₂ inr (i₂ #)) ∘ w !} ∘ (case f ∘ w inl π₂ inr (i₂ #))
+              IS₁ = begin 
+                (case f ∘ w inl π₂ inr (i₂ #)) ∘ (idC ⁂ s) ≈⟨ case∘ʳ (f ∘ w) π₂ (i₂ #) (idC ⁂ s) ⟩ 
+                (case ((f ∘ w) ∘ (idC ⁂ s)) inl (π₂ ∘ ((idC ⁂ s) ⁂ idC)) inr ((i₂ #) ∘ ((idC ⁂ s) ⁂ idC))) ≈⟨ (case⟩ (pullʳ (sym commute₂)) ⟨inl⟩ (π₂∘⁂ ○ identityˡ) ⟨inr⟩ {!   !}) ⟩ 
+                (case (f ∘ (case f inl π₁ inr π₂) ∘ w) inl (π₂) inr (i₂ #)) ≈⟨ {!   !} ⟩ 
+                {!   !} ≈⟨ {!   !} ⟩ 
+                {!   !} ≈⟨ {!   !} ⟩ 
+                {!   !} ∎
           by-uni₁ : (idC +₁ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ ≈ ((extend [ i₂ # , f ]#⟩ ∘ τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩
           by-uni₁ = {!   !}
           by-uni₂ : (idC +₁ w) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ ≈ f ∘ w
-          by-uni₂ = {!   !}
+          by-uni₂ = begin 
-
+            (idC +₁ w) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ 
+            (idC +₁ w) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ s) ⁂ idC) ∘ ⟨ idC , f ∘ w ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (sym (distribute₁ (idC ⁂ s) idC idC ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym))) ○ assoc) ⟩
+            (idC +₁ w) ∘ (π₂ +₁ π₁) ∘ ((idC ⁂ s) ⁂ idC +₁ (idC ⁂ s) ⁂ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ w ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (π₂∘⁂ ○ identityˡ) π₁∘⁂)) ⟩ 
+            (idC +₁ w) ∘ (π₂ +₁ (idC ⁂ s) ∘ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ w ⟩ ≈⟨ refl ⟩ 
+            (idC +₁ w) ∘ (case f ∘ w inl (i₁ ∘ π₂) inr (i₂ ∘ (idC ⁂ s) ∘ π₁)) ≈⟨ case∘ˡ (f ∘ w) (i₁ ∘ π₂) (i₂ ∘ (idC ⁂ s) ∘ π₁) (idC +₁ w)  ○ (case⟩ refl ⟨inl⟩ (pullˡ (+₁∘i₁ ○ identityʳ)) ⟨inr⟩ (pullˡ +₁∘i₂ ○ assoc)) ⟩
+            case (f ∘ w) inl (i₁ ∘ π₂) inr (i₂ ∘ w ∘ (idC ⁂ s) ∘ π₁) ≈⟨ (case⟩ refl ⟨inl⟩ refl ⟨inr⟩ (refl⟩∘⟨ (pullˡ (sym commute₂) ○ assoc))) ⟩
+            case (f ∘ w) inl (i₁ ∘ π₂) inr (i₂ ∘ (case f inl π₁ inr π₂) ∘ w ∘ π₁) ≈⟨ (case⟩ refl ⟨inl⟩ refl ⟨inr⟩ (refl⟩∘⟨ (pullˡ (case∘ʳ f π₁ π₂ w)))) ⟩ 
+            (case (f ∘ w) inl (i₁ ∘ π₂) inr (i₂ ∘ (case f ∘ w inl (π₁ ∘ (w ⁂ idC)) inr (π₂ ∘ (w ⁂ idC))) ∘ π₁)) ≈⟨ (case⟩ refl ⟨inl⟩ refl ⟨inr⟩ (pullˡ (case∘ˡ (f ∘ w) (π₁ ∘ (w ⁂ idC)) (π₂ ∘ (w ⁂ idC)) i₂))) ⟩ 
+            (case (f ∘ w) inl (i₁ ∘ π₂) inr ((case f ∘ w inl (i₂ ∘ π₁ ∘ (w ⁂ idC)) inr (i₂ ∘ π₂ ∘ (w ⁂ idC))) ∘ π₁)) ≈⟨ case-nested (f ∘ w) (i₁ ∘ π₂) (i₂ ∘ π₁ ∘ (w ⁂ idC)) (i₂ ∘ π₂ ∘ (w ⁂ idC)) ⟩ 
+            (case f ∘ w inl i₁ ∘ π₂ inr (i₂ ∘ π₂ ∘ (w ⁂ idC))) ≈⟨ (case⟩ refl ⟨inl⟩ refl ⟨inr⟩ (refl⟩∘⟨ (π₂∘⁂ ○ identityˡ))) ○ case-id (f ∘ w) ⟩ 
+            f ∘ w ∎
 ```