From 8c6f68e5421425b3f4546b44468ef2eadc52f211 Mon Sep 17 00:00:00 2001
From: KANG Rongji <smallpigkang@gmail.com>
Date: Mon, 8 Aug 2022 23:36:42 +0800
Subject: [PATCH] done

---
 Cubical/Foundations/CartesianKanOps.agda | 35 ++++++++++++++++++++++--
 1 file changed, 33 insertions(+), 2 deletions(-)

diff --git a/Cubical/Foundations/CartesianKanOps.agda b/Cubical/Foundations/CartesianKanOps.agda
index 6aa33b8701..5d00cec502 100644
--- a/Cubical/Foundations/CartesianKanOps.agda
+++ b/Cubical/Foundations/CartesianKanOps.agda
@@ -3,6 +3,8 @@
 module Cubical.Foundations.CartesianKanOps where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Transport
 
 coe0→1 : ∀ {ℓ} (A : I → Type ℓ) → A i0 → A i1
 coe0→1 A a = transp (\ i → A i) i0 a
@@ -79,9 +81,38 @@ coei→i1 A i a = refl
 coei1→i : ∀ {ℓ} (A : I → Type ℓ) (i : I) (a : A i1) → coei→j A i1 i a ≡ coe1→i A i a
 coei1→i A i a = refl
 
--- only non-definitional equation
+-- only non-definitional equation, but definitional at the ends
 coei→i : ∀ {ℓ} (A : I → Type ℓ) (i : I) (a : A i) → coei→j A i i a ≡ a
-coei→i A i = coe0→i (λ i → (a : A i) → coei→j A i i a ≡ a) i (λ _ → refl)
+coei→i A i a j =
+  comp (λ k → A (i ∧ (j ∨ k)))
+  (λ k → λ
+    { (i = i0) → a
+    ; (i = i1) → coe1→i A (j ∨ k) a
+    ; (j = i1) → a })
+  (transpFill {A = A i0} (~ i) (λ t → inS (A (i ∧ ~ t))) a (~ j))
+
+coe0→0 : ∀ {ℓ} (A : I → Type ℓ) (a : A i0) → coei→i A i0 a ≡ refl
+coe0→0 A a = refl
+
+coe1→1 : ∀ {ℓ} (A : I → Type ℓ) (a : A i1) → coei→i A i1 a ≡ refl
+coe1→1 A a = refl
+
+-- coercion when there already exists a path
+coePath : ∀ {ℓ} (A : I → Type ℓ) (p : (i : I) → A i) → (i j : I) → coei→j A i j (p i) ≡ p j
+coePath A p i j =
+  hcomp (λ k → λ
+    { (i = i0)(j = i0) → rUnit refl (~ k)
+    ; (i = i1)(j = i1) → rUnit refl (~ k) })
+  (diag ∙ coei→i A j (p j))
+  where
+  diag : coei→j A i j (p i) ≡ coei→j A j j (p j)
+  diag k = coei→j A _ j (p ((j ∨ (i ∧ ~ k)) ∧ (i ∨ (j ∧ k))))
+
+coePathi0 : ∀ {ℓ} (A : I → Type ℓ) (p : (i : I) → A i) → coePath A p i0 i0 ≡ refl
+coePathi0 A p = refl
+
+coePathi1 : ∀ {ℓ} (A : I → Type ℓ) (p : (i : I) → A i) → coePath A p i1 i1 ≡ refl
+coePathi1 A p = refl
 
 -- do the same for fill