{-# OPTIONS --without-K #-}

open import lib.Base
open import lib.PathGroupoid
open import lib.PathOver
open import lib.cubical.Square

module lib.cubical.SquareOver where

SquareOver :  {i j} {A : Type i} (B : A  Type j) {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ : B a₁₀} {b₁₁ : B a₁₁}
  (q₀₋ : b₀₀ == b₀₁ [ B  p₀₋ ]) (q₋₀ : b₀₀ == b₁₀ [ B  p₋₀ ])
  (q₋₁ : b₀₁ == b₁₁ [ B  p₋₁ ]) (q₁₋ : b₁₀ == b₁₁ [ B  p₁₋ ])
   Type j
SquareOver B ids = Square

apd-square :  {i j} {A : Type i} {B : A  Type j} (f : Π A B)
  {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
   SquareOver B sq (apd f p₀₋) (apd f p₋₀) (apd f p₋₁) (apd f p₁₋)
apd-square f ids = ids

↓-=-to-squareover :  {i j} {A : Type i} {B : A  Type j}
  {f g : Π A B} {x y : A} {p : x == y}
  {u : f x == g x} {v : f y == g y}
   u == v [  z  f z == g z)  p ]
   SquareOver B vid-square u (apd f p) (apd g p) v
↓-=-to-squareover {p = idp} idp = hid-square

↓-=-from-squareover :  {i j} {A : Type i} {B : A  Type j}
  {f g : Π A B} {x y : A} {p : x == y}
  {u : f x == g x} {v : f y == g y}
   SquareOver B vid-square u (apd f p) (apd g p) v
   u == v [  z  f z == g z)  p ]
↓-=-from-squareover {p = idp} sq = horiz-degen-path sq

squareover-cst-in :  {i j} {A : Type i} {B : Type j} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {sq : Square p₀₋ p₋₀ p₋₁ p₁₋}
  {b₀₀ b₀₁ b₁₀ b₁₁ : B}
  {q₀₋ : b₀₀ == b₀₁} {q₋₀ : b₀₀ == b₁₀} {q₋₁ : b₀₁ == b₁₁} {q₁₋ : b₁₀ == b₁₁}
  (sq' : Square q₀₋ q₋₀ q₋₁ q₁₋)
   SquareOver  _  B) sq
      (↓-cst-in q₀₋) (↓-cst-in q₋₀) (↓-cst-in q₋₁) (↓-cst-in q₁₋)
squareover-cst-in {sq = ids} sq' = sq'

↓↓-from-squareover :  {i j k} {A : Type i} {B : A  Type j} {C : Type k}
  {x y : C  A} {u : (c : C)  B (x c)} {v : (c : C)  B (y c)}
  {p : (c : C)  x c == y c} {c₁ c₂ : C} {q : c₁ == c₂}
  {α : u c₁ == v c₁ [ B  p c₁ ]} {β : u c₂ == v c₂ [ B  p c₂ ]}
   SquareOver B (natural-square p q)
               α (↓-ap-in _ _ (apd u q)) (↓-ap-in _ _ (apd v q)) β
   α == β [  c  u c == v c [ B  p c ])  q ]
↓↓-from-squareover {q = idp} sq = lemma sq
  where
  lemma :  {i j} {A : Type i} {B : A  Type j}
    {x y : A} {u : B x} {v : B y} {p : x == y}
    {α β : u == v [ B  p ]}
     SquareOver B hid-square α idp idp β
     α == β
  lemma {p = idp} sq = horiz-degen-path sq

↓↓-to-squareover :  {i j k} {A : Type i} {B : A  Type j} {C : Type k}
  {x y : C  A} {u : (c : C)  B (x c)} {v : (c : C)  B (y c)}
  {p : (c : C)  x c == y c} {c₁ c₂ : C} {q : c₁ == c₂}
  {α : u c₁ == v c₁ [ B  p c₁ ]} {β : u c₂ == v c₂ [ B  p c₂ ]}
   α == β [  c  u c == v c [ B  p c ])  q ]
   SquareOver B (natural-square p q)
               α (↓-ap-in _ _ (apd u q)) (↓-ap-in _ _ (apd v q)) β
↓↓-to-squareover {q = idp} r = lemma r
  where
  lemma :  {i j} {A : Type i} {B : A  Type j}
    {x y : A} {u : B x} {v : B y} {p : x == y}
    {α β : u == v [ B  p ]}
     α == β
     SquareOver B hid-square α idp idp β
  lemma {p = idp} r = horiz-degen-square r

infixr 80 _∙v↓⊡_ _∙h↓⊡_ _↓⊡v∙_ _↓⊡h∙_

_∙h↓⊡_ :  {i j} {A : Type i} {B : A  Type j} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {sq : Square p₀₋ p₋₀ p₋₁ p₁₋}
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ : B a₁₀} {b₁₁ : B a₁₁}
  {q₀₋ q₀₋' : b₀₀ == b₀₁ [ B  p₀₋ ]} {q₋₀ : b₀₀ == b₁₀ [ B  p₋₀ ]}
  {q₋₁ : b₀₁ == b₁₁ [ B  p₋₁ ]} {q₁₋ : b₁₀ == b₁₁ [ B  p₁₋ ]}
   q₀₋ == q₀₋'
   SquareOver B sq q₀₋' q₋₀ q₋₁ q₁₋
   SquareOver B sq q₀₋ q₋₀ q₋₁ q₁₋
_∙h↓⊡_ {sq = ids} = _∙h⊡_

_∙v↓⊡_ :  {i j} {A : Type i} {B : A  Type j} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {sq : Square p₀₋ p₋₀ p₋₁ p₁₋}
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ : B a₁₀} {b₁₁ : B a₁₁}
  {q₀₋ : b₀₀ == b₀₁ [ B  p₀₋ ]} {q₋₀ q₋₀' : b₀₀ == b₁₀ [ B  p₋₀ ]}
  {q₋₁ : b₀₁ == b₁₁ [ B  p₋₁ ]} {q₁₋ : b₁₀ == b₁₁ [ B  p₁₋ ]}
   q₋₀ == q₋₀'
   SquareOver B sq q₀₋ q₋₀' q₋₁ q₁₋
   SquareOver B sq q₀₋ q₋₀ q₋₁ q₁₋
_∙v↓⊡_ {sq = ids} = _∙v⊡_

_↓⊡v∙_ :  {i j} {A : Type i} {B : A  Type j} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {sq : Square p₀₋ p₋₀ p₋₁ p₁₋}
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ : B a₁₀} {b₁₁ : B a₁₁}
  {q₀₋ : b₀₀ == b₀₁ [ B  p₀₋ ]} {q₋₀ : b₀₀ == b₁₀ [ B  p₋₀ ]}
  {q₋₁ q₋₁' : b₀₁ == b₁₁ [ B  p₋₁ ]} {q₁₋ : b₁₀ == b₁₁ [ B  p₁₋ ]}
   SquareOver B sq q₀₋ q₋₀ q₋₁ q₁₋
   q₋₁ == q₋₁'
   SquareOver B sq q₀₋ q₋₀ q₋₁' q₁₋
_↓⊡v∙_ {sq = ids} = _⊡v∙_

_↓⊡h∙_ :  {i j} {A : Type i} {B : A  Type j} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {sq : Square p₀₋ p₋₀ p₋₁ p₁₋}
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ : B a₁₀} {b₁₁ : B a₁₁}
  {q₀₋ : b₀₀ == b₀₁ [ B  p₀₋ ]} {q₋₀ : b₀₀ == b₁₀ [ B  p₋₀ ]}
  {q₋₁ : b₀₁ == b₁₁ [ B  p₋₁ ]} {q₁₋ q₁₋' : b₁₀ == b₁₁ [ B  p₁₋ ]}
   SquareOver B sq q₀₋ q₋₀ q₋₁ q₁₋
   q₁₋ == q₁₋'
   SquareOver B sq q₀₋ q₋₀ q₋₁ q₁₋'
_↓⊡h∙_ {sq = ids} = _⊡h∙_