text:
{-# OPTIONS --without-K --rewriting #-}

open import lib.Base
open import lib.Equivalence
open import lib.NType
open import lib.PathFunctor
open import lib.PathGroupoid
open import lib.PathOver
open import lib.Univalence

module lib.cubical.Square where

{-
  *--1--*
  |     |
  0     3
  |     |
  *--2--*
-}

data Square {i} {A : Type i} {a₀₀ : A} : {a₀₁ a₁₀ a₁₁ : A}
  → a₀₀ == a₀₁ → a₀₀ == a₁₀ → a₀₁ == a₁₁ → a₁₀ == a₁₁ → Type i
  where
  ids : Square idp idp idp idp

hid-square : ∀ {i} {A : Type i} {a₀₀ a₀₁ : A} {p : a₀₀ == a₀₁}
  → Square p idp idp p
hid-square {p = idp} = ids

vid-square : ∀ {i} {A : Type i} {a₀₀ a₁₀ : A} {p : a₀₀ == a₁₀}
  → Square idp p p idp
vid-square {p = idp} = ids

square-to-disc : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → p₀₋ ∙ p₋₁ == p₋₀ ∙ p₁₋
square-to-disc ids = idp

disc-to-square : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → p₀₋ ∙ p₋₁ == p₋₀ ∙ p₁₋
  → Square p₀₋ p₋₀ p₋₁ p₁₋
disc-to-square {p₀₋ = idp} {p₋₀ = idp} {p₋₁ = idp} {p₁₋ = .idp} idp = ids

square-to-disc-β : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (α : p₀₋ ∙ p₋₁ == p₋₀ ∙ p₁₋)
  → square-to-disc (disc-to-square {p₀₋ = p₀₋} {p₋₀ = p₋₀} α) == α
square-to-disc-β {p₀₋ = idp} {p₋₀ = idp} {p₋₁ = idp} {p₁₋ = .idp} idp = idp

disc-to-square-β : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → disc-to-square (square-to-disc sq) == sq
disc-to-square-β ids = idp

square-disc-equiv : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → (Square p₀₋ p₋₀ p₋₁ p₁₋) ≃ (p₀₋ ∙ p₋₁ == p₋₀ ∙ p₁₋)
square-disc-equiv =
  equiv square-to-disc disc-to-square square-to-disc-β disc-to-square-β

Square-level : ∀ {n : ℕ₋₂} {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → has-level (S (S n)) A
  → has-level n (Square p₀₋ p₋₀ p₋₁ p₁₋)
Square-level {n} A-level =
  transport (has-level n) (! (ua square-disc-equiv)) $
  has-level-apply (has-level-apply A-level _ _) _ _

ap-square : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → Square (ap f p₀₋) (ap f p₋₀) (ap f p₋₁) (ap f p₁₋)
ap-square f ids = ids

ap-square-hid : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
  {a₀ a₁ : A} {p : a₀ == a₁}
  → ap-square f (hid-square {p = p}) == hid-square
ap-square-hid {p = idp} = idp

ap-square-vid : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
  {a₀ a₁ : A} {p : a₀ == a₁}
  → ap-square f (vid-square {p = p}) == vid-square
ap-square-vid {p = idp} = idp

module _ {i} {A : Type i} where

  horiz-degen-square : {a a' : A} {p q : a == a'}
    → p == q → Square p idp idp q
  horiz-degen-square {p = idp} α = disc-to-square α

  horiz-degen-path : {a a' : A} {p q : a == a'}
    → Square p idp idp q → p == q
  horiz-degen-path {p = idp} sq = square-to-disc sq

  horiz-degen-path-β : {a a' : A} {p q : a == a'} (α : p == q)
    → horiz-degen-path (horiz-degen-square α) == α
  horiz-degen-path-β {p = idp} α = square-to-disc-β α

  horiz-degen-square-β : {a a' : A} {p q : a == a'} (sq : Square p idp idp q)
    → horiz-degen-square (horiz-degen-path sq) == sq
  horiz-degen-square-β {p = idp} sq = disc-to-square-β sq

  vert-degen-square : {a a' : A} {p q : a == a'}
    → p == q → Square idp p q idp
  vert-degen-square {p = idp} α = disc-to-square (! α)

  vert-degen-path : {a a' : A} {p q : a == a'}
    → Square idp p q idp → p == q
  vert-degen-path {p = idp} sq = ! (square-to-disc sq)

  vert-degen-path-β : {a a' : A} {p q : a == a'} (α : p == q)
    → vert-degen-path (vert-degen-square α) == α
  vert-degen-path-β {p = idp} α = ap ! (square-to-disc-β (! α)) ∙ !-! α

  vert-degen-square-β : {a a' : A} {p q : a == a'} (sq : Square idp p q idp)
    → vert-degen-square (vert-degen-path sq) == sq
  vert-degen-square-β {p = idp} sq =
    ap disc-to-square (!-! (square-to-disc sq)) ∙ disc-to-square-β sq

  horiz-degen-square-idp : {a a' : A} {p : a == a'}
    → horiz-degen-square (idp {a = p}) == hid-square
  horiz-degen-square-idp {p = idp} = idp

  vert-degen-square-idp : {a a' : A} {p : a == a'}
    → vert-degen-square (idp {a = p}) == vid-square
  vert-degen-square-idp {p = idp} = idp

ap-horiz-degen-square : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  {a a' : A} {p q : a == a'} (r : p == q)
  → ap-square f (horiz-degen-square r) == horiz-degen-square (ap (ap f) r)
ap-horiz-degen-square f {p = idp} r@idp = idp

ap-vert-degen-square : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  {a a' : A} {p q : a == a'} (r : p == q)
  → ap-square f (vert-degen-square r) == vert-degen-square (ap (ap f) r)
ap-vert-degen-square f {p = idp} r@idp = idp

{- Flipping squares -}
module _ {i} {A : Type i} where

  square-symmetry : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square p₋₀ p₀₋ p₁₋ p₋₁
  square-symmetry ids = ids

  square-sym-inv : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → square-symmetry (square-symmetry sq) == sq
  square-sym-inv ids = idp

  !□h : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋
    → Square p₁₋ (! p₋₀) (! p₋₁) p₀₋
  !□h ids = ids

  !□v : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋
    → Square (! p₀₋) p₋₁ p₋₀ (! p₁₋)
  !□v ids = ids

  !□v-horiz-degen-square : {a a' : A} {p q : a == a'}
    (r : p == q)
    → !□v (horiz-degen-square r) == horiz-degen-square (ap ! r)
  !□v-horiz-degen-square {p = idp} r@idp = idp

  !□v-vert-degen-square : {a a' : A} {p q : a == a'}
    (r : p == q)
    → !□v (vert-degen-square r) == vert-degen-square (! r)
  !□v-vert-degen-square {p = idp} r@idp = idp

ap-square-symmetry : ∀ {i j} {A : Type i} {B : 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₁₋)
  → ap-square f (square-symmetry sq) == square-symmetry (ap-square f sq)
ap-square-symmetry f ids = idp

horiz-degen-square-symmetry : ∀ {i} {A : Type i}
  {a a' : A} {p q : a == a'} (r : p == q)
  → square-symmetry (horiz-degen-square r) == vert-degen-square r
horiz-degen-square-symmetry {p = idp} α@idp = idp

{- Alternate induction principles -}

square-left-J : ∀ {i j} {A : Type i} {a₀₀ a₀₁ : A} {p₀₋ : a₀₀ == a₀₁}
  (P : {a₁₀ a₁₁ : A} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
       (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
       → Type j)
  (r : P hid-square)
  {a₁₀ a₁₁ : A} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → P sq
square-left-J P r ids = r

square-top-J : ∀ {i j} {A : Type i} {a₀₀ a₁₀ : A} {p₋₀ : a₀₀ == a₁₀}
  (P : {a₀₁ a₁₁ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
       (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
       → Type j)
  (r : P vid-square)
  {a₀₁ a₁₁ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → P sq
square-top-J P r ids = r

square-bot-J : ∀ {i j} {A : Type i} {a₀₁ a₁₁ : A} {p₋₁ : a₀₁ == a₁₁}
  (P : {a₀₀ a₁₀ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₁₋ : a₁₀ == a₁₁}
       (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
       → Type j)
  (r : P vid-square)
  {a₀₀ a₁₀ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → P sq
square-bot-J P r ids = r

square-right-J : ∀ {i j} {A : Type i} {a₁₀ a₁₁ : A} {p₁₋ : a₁₀ == a₁₁}
  (P : {a₀₀ a₀₁ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁}
       (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
       → Type j)
  (r : P hid-square)
  {a₀₀ a₀₁ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → P sq
square-right-J P r ids = r

module _ where
  private
    lemma : ∀ {i j} {A : Type i} {a₀ : A}
      (P : {a₁ : A} {p q : a₀ == a₁} → p == q → Type j)
      (r : P (idp {a = idp}))
      {a₁ : A} {p q : a₀ == a₁} (α : p == q)
      → P α
    lemma P r {p = idp} idp = r

  horiz-degen-J : ∀ {i j} {A : Type i} {a₀ : A}
    (P : {a₁ : A} {p q : a₀ == a₁} → Square p idp idp q → Type j)
    (r : P ids)
    {a₁ : A} {p q : a₀ == a₁} (sq : Square p idp idp q)
    → P sq
  horiz-degen-J P r sq = transport P
    (horiz-degen-square-β sq)
    (lemma (P ∘ horiz-degen-square) r (horiz-degen-path sq))

  vert-degen-J : ∀ {i j} {A : Type i} {a₀ : A}
    (P : {a₁ : A} {p q : a₀ == a₁} → Square idp p q idp → Type j)
    (r : P ids)
    {a₁ : A} {p q : a₀ == a₁} (sq : Square idp p q idp)
    → P sq
  vert-degen-J P r sq = transport P
    (vert-degen-square-β sq)
    (lemma (P ∘ vert-degen-square) r (vert-degen-path sq))

{- Square filling -}
module _ {i} {A : Type i} where
  fill-square-left : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    (p₋₀ : a₀₀ == a₁₀) (p₋₁ : a₀₁ == a₁₁) (p₁₋ : a₁₀ == a₁₁)
    → Σ (a₀₀ == a₀₁) (λ p₀₋ → Square p₀₋ p₋₀ p₋₁ p₁₋)
  fill-square-left idp idp p = (p , hid-square)

  fill-square-top : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    (p₀₋ : a₀₀ == a₀₁) (p₋₁ : a₀₁ == a₁₁) (p₁₋ : a₁₀ == a₁₁)
    → Σ (a₀₀ == a₁₀) (λ p₋₀ → Square p₀₋ p₋₀ p₋₁ p₁₋)
  fill-square-top idp p idp = (p , vid-square)

  fill-square-bot : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    (p₀₋ : a₀₀ == a₀₁) (p₋₀ : a₀₀ == a₁₀) (p₁₋ : a₁₀ == a₁₁)
    → Σ (a₀₁ == a₁₁) (λ p₋₁ → Square p₀₋ p₋₀ p₋₁ p₁₋)
  fill-square-bot idp p idp = (p , vid-square)

  fill-square-right : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    (p₀₋ : a₀₀ == a₀₁) (p₋₀ : a₀₀ == a₁₀) (p₋₁ : a₀₁ == a₁₁)
    → Σ (a₁₀ == a₁₁) (λ p₁₋ → Square p₀₋ p₋₀ p₋₁ p₁₋)
  fill-square-right p idp idp = (p , hid-square)

module _  {i j} {A : Type i} {B : Type j} {f : A → B} {b : B} where

  ↓-cst=app-from-square : {x y : A} {p : x == y}
    {u : b == f x} {v : b == f y}
    → Square u idp (ap f p) v
    → u == v [ (λ z → b == f z) ↓ p ]
  ↓-cst=app-from-square {p = idp} sq = horiz-degen-path sq

  ↓-cst=app-to-square : {x y : A} {p : x == y}
    {u : b == f x} {v : b == f y}
    → u == v [ (λ z → b == f z) ↓ p ]
    → Square u idp (ap f p) v
  ↓-cst=app-to-square {p = idp} α = horiz-degen-square α

  ↓-app=cst-from-square : {x y : A} {p : x == y}
    {u : f x == b} {v : f y == b}
    → Square u (ap f p) idp v
    → u == v [ (λ z → f z == b) ↓ p ]
  ↓-app=cst-from-square {p = idp} sq = horiz-degen-path sq

  ↓-app=cst-to-square : {x y : A} {p : x == y}
    {u : f x == b} {v : f y == b}
    → u == v [ (λ z → f z == b) ↓ p ]
    → Square u (ap f p) idp v
  ↓-app=cst-to-square {p = idp} α = horiz-degen-square α

module _  {i} {A : Type i} {f : A → A} where

  ↓-idf=app-from-square : {x y : A} {p : x == y}
    {u : x == f x} {v : y == f y}
    → Square u p (ap f p) v
    → u == v [ (λ z → z == f z) ↓ p ]
  ↓-idf=app-from-square {p = idp} sq = horiz-degen-path sq

  ↓-idf=app-to-square : {x y : A} {p : x == y}
    {u : x == f x} {v : y == f y}
    → u == v [ (λ z → z == f z) ↓ p ]
    → Square u p (ap f p) v
  ↓-idf=app-to-square {p = idp} α = horiz-degen-square α

  ↓-app=idf-from-square : {x y : A} {p : x == y}
    {u : f x == x} {v : f y == y}
    → Square u (ap f p) p v
    → u == v [ (λ z → f z == z) ↓ p ]
  ↓-app=idf-from-square {p = idp} sq = horiz-degen-path sq

  ↓-app=idf-to-square : {x y : A} {p : x == y}
    {u : f x == x} {v : f y == y}
    → u == v [ (λ z → f z == z) ↓ p ]
    → Square u (ap f p) p v
  ↓-app=idf-to-square {p = idp} α = horiz-degen-square α

module _  {i j} {A : Type i} {B : Type j} (g : B → A) (f : A → B) where

  ↓-∘=idf-from-square : {x y : A} {p : x == y}
    {u : g (f x) == x} {v : g (f y) == y}
    → Square u (ap g (ap f p)) p v
    → (u == v [ (λ z → g (f z) == z) ↓ p ])
  ↓-∘=idf-from-square {p = idp} sq = horiz-degen-path sq

  ↓-∘=idf-to-square : {x y : A} {p : x == y}
    {u : g (f x) == x} {v : g (f y) == y}
    → (u == v [ (λ z → g (f z) == z) ↓ p ])
    → Square u (ap g (ap f p)) p v
  ↓-∘=idf-to-square {p = idp} α = horiz-degen-square α

_⊡v_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ a₀₂ a₁₂ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {q₀₋ : a₀₁ == a₀₂} {q₋₂ : a₀₂ == a₁₂} {q₁₋ : a₁₁ == a₁₂}
  → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square q₀₋ p₋₁ q₋₂ q₁₋
  → Square (p₀₋ ∙ q₀₋) p₋₀ q₋₂ (p₁₋ ∙ q₁₋)
ids ⊡v sq = sq

_⊡v'_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ a₀₂ a₁₂ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {q₀₋ : a₀₁ == a₀₂} {q₋₂ : a₀₂ == a₁₂} {q₁₋ : a₁₁ == a₁₂}
  → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square q₀₋ p₋₁ q₋₂ q₁₋
  → Square (p₀₋ ∙' q₀₋) p₋₀ q₋₂ (p₁₋ ∙' q₁₋)
sq ⊡v' ids = sq

_∙v⊡_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ p₋₀' : a₀₀ == a₁₀}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → p₋₀ == p₋₀'
  → Square p₀₋ p₋₀' p₋₁ p₁₋
  → Square p₀₋ p₋₀ p₋₁ p₁₋
idp ∙v⊡ sq = sq

_⊡v∙_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₋₀ : a₀₀ == a₁₀} {p₀₋ : a₀₀ == a₀₁}
  {p₋₁ p₋₁' : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → p₋₁ == p₋₁'
  → Square p₀₋ p₋₀ p₋₁' p₁₋
sq ⊡v∙ idp = sq

_⊡h_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ a₂₀ a₂₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {q₋₀ : a₁₀ == a₂₀} {q₋₁ : a₁₁ == a₂₁} {q₂₋ : a₂₀ == a₂₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → Square p₁₋ q₋₀ q₋₁ q₂₋
  → Square p₀₋ (p₋₀ ∙ q₋₀) (p₋₁ ∙ q₋₁) q₂₋
ids ⊡h sq = sq

_⊡h'_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ a₂₀ a₂₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {q₋₀ : a₁₀ == a₂₀} {q₋₁ : a₁₁ == a₂₁} {q₂₋ : a₂₀ == a₂₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → Square p₁₋ q₋₀ q₋₁ q₂₋
  → Square p₀₋ (p₋₀ ∙' q₋₀) (p₋₁ ∙' q₋₁) q₂₋
sq ⊡h' ids = sq

_∙h⊡_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ p₀₋' : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → p₀₋ == p₀₋'
  → Square p₀₋' p₋₀ p₋₁ p₁₋
  → Square p₀₋ p₋₀ p₋₁ p₁₋
idp ∙h⊡ sq = sq

_⊡h∙_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ p₁₋' : a₁₀ == a₁₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → p₁₋ == p₁₋'
  → Square p₀₋ p₋₀ p₋₁ p₁₋'
sq ⊡h∙ idp = sq

infixr 80 _⊡v_ _⊡v'_ _⊡h_ _⊡h'_

infixr 80 _∙v⊡_ _∙h⊡_
infixl 85 _⊡v∙_ _⊡h∙_

∙h⊡-hid-square-⊡h∙ : ∀ {i} {A : Type i} {a₀₀ a₀₁ : A} {p p' : a₀₀ == a₀₁}
  (q : p' == p)
  → ! q ∙h⊡ hid-square ⊡h∙ q == hid-square
∙h⊡-hid-square-⊡h∙ q@idp = idp

∙v⊡-assoc : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₋₀ p₋₀' p₋₀'' : a₀₀ == a₁₀} {p₀₋ : a₀₀ == a₀₁}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (q : p₋₀ == p₋₀')
  (r : p₋₀' == p₋₀'')
  (sq : Square p₀₋ p₋₀'' p₋₁ p₁₋)
  → (q ∙ r) ∙v⊡ sq == q ∙v⊡ (r ∙v⊡ sq)
∙v⊡-assoc q@idp r sq = idp

⊡v∙-assoc : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₋₀ : a₀₀ == a₁₀} {p₀₋ : a₀₀ == a₀₁}
  {p₋₁ p₋₁' p₋₁'' : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  (q : p₋₁ == p₋₁')
  (r : p₋₁' == p₋₁'')
  → (sq ⊡v∙ q) ⊡v∙ r == sq ⊡v∙ (q ∙ r)
⊡v∙-assoc sq q@idp r = idp

⊡h∙-assoc : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₋₀ : a₀₀ == a₁₀} {p₀₋ : a₀₀ == a₀₁}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ p₁₋' p₁₋'' : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  (q : p₁₋ == p₁₋')
  (r : p₁₋' == p₁₋'')
  → (sq ⊡h∙ q) ⊡h∙ r == sq ⊡h∙ (q ∙ r)
⊡h∙-assoc sq q@idp r = idp

∙v⊡-⊡h∙-comm : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₋₀ p₋₀' : a₀₀ == a₁₀} {p₀₋ : a₀₀ == a₀₁}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ p₁₋' : a₁₀ == a₁₁}
  (q : p₋₀ == p₋₀')
  (sq : Square p₀₋ p₋₀' p₋₁ p₁₋)
  (r : p₁₋ == p₁₋')
  → (q ∙v⊡ sq) ⊡h∙ r == q ∙v⊡ (sq ⊡h∙ r)
∙v⊡-⊡h∙-comm q@idp sq r = idp

⊡v∙-⊡h∙-comm : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₋₀ : a₀₀ == a₁₀} {p₀₋ : a₀₀ == a₀₁}
  {p₋₁ p₋₁' : a₀₁ == a₁₁} {p₁₋ p₁₋' : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  (q : p₋₁ == p₋₁')
  (r : p₁₋ == p₁₋')
  → (sq ⊡v∙ q) ⊡h∙ r == (sq ⊡h∙ r) ⊡v∙ q
⊡v∙-⊡h∙-comm sq q@idp r = idp

∙v⊡-⊡v∙-comm : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₋₀ p₋₀' : a₀₀ == a₁₀} {p₀₋ : a₀₀ == a₀₁}
  {p₋₁ p₋₁' : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (q : p₋₀ == p₋₀')
  (sq : Square p₀₋ p₋₀' p₋₁ p₁₋)
  (r : p₋₁ == p₋₁')
  → (q ∙v⊡ sq) ⊡v∙ r == q ∙v⊡ (sq ⊡v∙ r)
∙v⊡-⊡v∙-comm q@idp sq r = idp

∙h⊡-⊡h∙-comm : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₋₀ : a₀₀ == a₁₀} {p₀₋ p₀₋' : a₀₀ == a₀₁}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ p₁₋' : a₁₀ == a₁₁}
  (q : p₀₋ == p₀₋')
  (sq : Square p₀₋' p₋₀ p₋₁ p₁₋)
  (r : p₁₋ == p₁₋')
  → (q ∙h⊡ sq) ⊡h∙ r == q ∙h⊡ (sq ⊡h∙ r)
∙h⊡-⊡h∙-comm q@idp sq r = idp

⊡h-⊡v∙-comm : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ a₂₀ a₂₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ p₋₁' : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {q₋₀ : a₁₀ == a₂₀} {q₋₁ q₋₁' : a₁₁ == a₂₁} {q₂₋ : a₂₀ == a₂₁}
  (p-sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  (q-sq : Square p₁₋ q₋₀ q₋₁ q₂₋)
  (r : p₋₁ == p₋₁')
  (s : q₋₁ == q₋₁')
  → (p-sq ⊡h q-sq) ⊡v∙ (ap2 _∙_ r s) == (p-sq ⊡v∙ r) ⊡h (q-sq ⊡v∙ s)
⊡h-⊡v∙-comm p-sq q-sq r@idp s@idp = idp

module _ {i j} {A : Type i} {B : Type j} (f : A → B) where

  ap-square-∙v⊡ : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₋₀ p₋₀' : a₀₀ == a₁₀} {p₀₋ : a₀₀ == a₀₁}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (q : p₋₀ == p₋₀')
    (sq : Square p₀₋ p₋₀' p₋₁ p₁₋)
    → ap (ap f) q ∙v⊡ ap-square f sq == ap-square f (q ∙v⊡ sq)
  ap-square-∙v⊡ q@idp sq = idp

  ap-square-⊡v∙ : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₋₀ : a₀₀ == a₁₀} {p₀₋ : a₀₀ == a₀₁}
    {p₋₁ p₋₁' : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    (q : p₋₁ == p₋₁')
    → ap-square f sq ⊡v∙ ap (ap f) q == ap-square f (sq ⊡v∙ q)
  ap-square-⊡v∙ sq q@idp = idp

module _ {i j} {A : Type i} {B : Type j} {f g : A → B} where

  ↓-='-to-square : {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
    → u == v [ (λ z → f z == g z) ↓ p ]
    → Square u (ap f p) (ap g p) v
  ↓-='-to-square {p = idp} α = horiz-degen-square α

  ↓-='-from-square : {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
    → Square u (ap f p) (ap g p) v
    → u == v [ (λ z → f z == g z) ↓ p ]
  ↓-='-from-square {p = idp} sq = horiz-degen-path sq

  ↓-='-square-comp : {x y z : A} {p : x == y} {q : y == z}
    {u : f x == g x} {v : f y == g y} {w : f z == g z}
    → Square u (ap f p) (ap g p) v
    → Square v (ap f q) (ap g q) w
    → Square u (ap f (p ∙ q)) (ap g (p ∙ q)) w
  ↓-='-square-comp {p = idp} {q = idp} sq₁ sq₂ =
    horiz-degen-square (horiz-degen-path sq₁ ∙ horiz-degen-path sq₂)

  ↓-='-from-square-comp : {x y z : A} {p : x == y} {q : y == z}
    {u : f x == g x} {v : f y == g y} {w : f z == g z}
    (sq₁ : Square u (ap f p) (ap g p) v)
    (sq₂ : Square v (ap f q) (ap g q) w)
    → ↓-='-from-square (↓-='-square-comp sq₁ sq₂) ==
      ↓-='-from-square sq₁ ∙ᵈ ↓-='-from-square sq₂
  ↓-='-from-square-comp {p = idp} {q = idp} sq₁ sq₂ =
    horiz-degen-path-β _

  private
    custom-square-over :
      {x y z : A} {p : x == y} {q : y == z} {r : x == z}
      (comp : r == p ∙ q)
      {u : f x == g x} {v : f y == g y} {w : f z == g z}
      (p-sq : Square u (ap f p) (ap g p) v)
      (q-sq : Square v (ap f q) (ap g q) w)
      (r-sq : Square u (ap f r) (ap g r) w)
      → r-sq ⊡v∙ ap (ap g) comp ==
        ap (ap f) comp ∙v⊡ ↓-='-square-comp p-sq q-sq
      → r-sq == ↓-='-square-comp p-sq q-sq
          [ (λ s → Square u (ap f s) (ap g s) w) ↓ comp ]
    custom-square-over {p = idp} {q = idp} {r = .idp} idp p-sq q-sq r-sq e = e

  ↓-='-from-square-comp-path :
    {x y z : A} {p : x == y} {q : y == z} {r : x == z}
    (comp : r == p ∙ q)
    {u : f x == g x} {v : f y == g y} {w : f z == g z}
    (p-sq : Square u (ap f p) (ap g p) v)
    (q-sq : Square v (ap f q) (ap g q) w)
    (r-sq : Square u (ap f r) (ap g r) w)
    → r-sq ⊡v∙ ap (ap g) comp ==
      ap (ap f) comp ∙v⊡ ↓-='-square-comp p-sq q-sq
    → ↓-='-from-square r-sq == ↓-='-from-square p-sq ∙ᵈ ↓-='-from-square q-sq
        [ (λ p → u == w [ (λ x → f x == g x) ↓ p ]) ↓ comp ]
  ↓-='-from-square-comp-path comp p-sq q-sq r-sq e =
    ap↓ ↓-='-from-square (custom-square-over comp p-sq q-sq r-sq e) ▹
    ↓-='-from-square-comp p-sq q-sq

↓-='-from-square-! : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
  {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
  (sq : Square u (ap f p) (ap g p) v)
  → ap↓ ! (↓-='-from-square sq) == ↓-='-from-square (!□v sq)
↓-='-from-square-! {p = idp} sq =
  ap ! (horiz-degen-path sq)
    =⟨ ! (horiz-degen-path-β (ap ! (horiz-degen-path sq))) ⟩
  horiz-degen-path (horiz-degen-square (ap ! (horiz-degen-path sq)))
    =⟨ ap horiz-degen-path (! (!□v-horiz-degen-square (horiz-degen-path sq))) ⟩
  horiz-degen-path (!□v (horiz-degen-square (horiz-degen-path sq)))
    =⟨ ap (horiz-degen-path ∘ !□v) (horiz-degen-square-β sq) ⟩
  horiz-degen-path (!□v sq) =∎

↓-='-from-square-post-∘ : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  {f g : A → B} {h : B → C}
  {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
  → (sq : Square u (ap f p) (ap g p) v)
  → ap↓ (ap h) (↓-='-from-square sq)
    ==
    ↓-='-from-square (ap-∘ h f p ∙v⊡ ap-square h sq ⊡v∙ ∘-ap h g p)
↓-='-from-square-post-∘ {h = h} {p = idp} sq =
  ap (ap h) (horiz-degen-path sq)
    =⟨ ! (horiz-degen-path-β (ap (ap h) (horiz-degen-path sq))) ⟩
  horiz-degen-path (horiz-degen-square (ap (ap h) (horiz-degen-path sq)))
    =⟨ ap horiz-degen-path (! (ap-horiz-degen-square h (horiz-degen-path sq))) ⟩
  horiz-degen-path (ap-square h (horiz-degen-square (horiz-degen-path sq)))
    =⟨ ap (horiz-degen-path ∘ ap-square h) (horiz-degen-square-β sq) ⟩
  horiz-degen-path (ap-square h sq) =∎

module _ {i j} {A : Type i} {B : Type j} where

  natural-square : {f₁ f₂ : A → B} (h : ∀ a → f₁ a == f₂ a)
    {a₁ a₂ : A} (q : a₁ == a₂)
    → Square (h a₁) (ap f₁ q) (ap f₂ q) (h a₂)
  natural-square h idp = hid-square

  natural-square-path : {f₁ f₂ : A → B} (h h' : ∀ a → f₁ a == f₂ a)
    (H : ∀ a → h' a == h a)
    {a₁ a₂ : A} (q : a₁ == a₂)
    → ! (H a₁) ∙h⊡ natural-square h' q ⊡h∙ H a₂ == natural-square h q
  natural-square-path h h' H {a₁} idp = ∙h⊡-hid-square-⊡h∙ (H a₁)

  natural-square-idp : {f₁ : A → B} {a₁ a₂ : A} (q : a₁ == a₂)
    → natural-square {f₁ = f₁} (λ _ → idp) q == vid-square
  natural-square-idp idp = idp

  natural-square-cst : ∀ (b₁ b₂ : B) (h : A → b₁ == b₂)
    {a₁ a₂ : A} (q : a₁ == a₂)
    → ! (ap-cst b₁ q) ∙v⊡ natural-square {f₁ = λ a → b₁} {f₂ = λ a → b₂} h q ⊡v∙ ap-cst b₂ q
      ==
      horiz-degen-square (ap h q)
  natural-square-cst b₁ b₂ h q@idp = ! horiz-degen-square-idp

  {- Used for getting square equivalents of glue-β terms -}
  natural-square-β : {f₁ f₂ : A → B} (h : (a : A) → f₁ a == f₂ a)
    {x y : A} (q : x == y)
    {sq : Square (h x) (ap f₁ q) (ap f₂ q) (h y)}
    → apd h q == ↓-='-from-square sq
    → natural-square h q == sq
  natural-square-β _ idp α =
    ! horiz-degen-square-idp ∙ ap horiz-degen-square α ∙ horiz-degen-square-β _

module _ {i j k} {A : Type i} {B : Type j} {C : Type k} where

  natural-square-ap : (g : B → C)
    {f₁ f₂ : A → B} (h : ∀ a → f₁ a == f₂ a)
    {a₁ a₂ : A} (q : a₁ == a₂)
    → natural-square (ap g ∘ h) q
      ==
      ap-∘ g f₁ q ∙v⊡
      ap-square g (natural-square h q) ⊡v∙
      ∘-ap g f₂ q
  natural-square-ap g h q@idp = ! ap-square-hid

  natural-square-symmetry : (f : A → B → C)
    {a₁ a₂ : A} (p : a₁ == a₂)
    {b₁ b₂ : B} (q : b₁ == b₂)
    → square-symmetry (natural-square (λ b → ap (λ a → f a b) p) q)
      ==
      natural-square (λ a → ap (f a) q) p
  natural-square-symmetry f p@idp q@idp = idp

module _ {i} {A : Type i} where

  horiz-degen-path-⊡h : {a a' : A} {p q r : a == a'}
    (sq₁ : Square p idp idp q)
    (sq₂ : Square q idp idp r)
    → horiz-degen-path (sq₁ ⊡h sq₂) ==
      horiz-degen-path sq₁ ∙ horiz-degen-path sq₂
  horiz-degen-path-⊡h {p = idp} {q = .idp} ids sq₂ = idp

  vert-degen-square-⊡v∙ : {a a' : A} {p q r : a == a'}
    → (s : p == q) (t : q == r)
    → vert-degen-square s ⊡v∙ t == vert-degen-square (s ∙ t)
  vert-degen-square-⊡v∙ idp idp = idp

  vert-degen-square-∙v⊡ : {a a' : A} {p q r : a == a'}
    → (s : p == q) (t : q == r)
    → s ∙v⊡ vert-degen-square t == vert-degen-square (s ∙ t)
  vert-degen-square-∙v⊡ idp idp = idp

  vert-degen-square-⊡h : {a a' a'' : A}
    {p p' : a == a'} {q q' : a' == a''}
    (s : p == p') (t : q == q')
    → vert-degen-square s ⊡h vert-degen-square t ==
      vert-degen-square (ap2 _∙_ s t)
  vert-degen-square-⊡h {p = idp} idp idp = idp

module _ {i j} {A : Type i} {B : Type j} {f g : A → B} where

  ↓-='-square-comp' : {x y z : A} {p : x == y} {q : y == z}
    {u : f x == g x} {v : f y == g y} {w : f z == g z}
    → Square u (ap f p) (ap g p) v
    → Square v (ap f q) (ap g q) w
    → Square u (ap f (p ∙ q)) (ap g (p ∙ q)) w
  ↓-='-square-comp' {p = p} {q = q} sq₁ sq₂ =
    ap-∙ f p q ∙v⊡ ((sq₁ ⊡h sq₂) ⊡v∙ ∙-ap g p q)

  ↓-='-square-comp'=↓-='-square-comp : {x y z : A} {p : x == y} {q : y == z}
    {u : f x == g x} {v : f y == g y} {w : f z == g z}
    → (sq₁ : Square u (ap f p) (ap g p) v)
    → (sq₂ : Square v (ap f q) (ap g q) w)
    → ↓-='-square-comp' sq₁ sq₂ == ↓-='-square-comp sq₁ sq₂
  ↓-='-square-comp'=↓-='-square-comp {p = idp} {q = idp} sq₁ sq₂ =
    ↓-='-square-comp' sq₁ sq₂
      =⟨ idp ⟩
    sq₁ ⊡h sq₂
      =⟨ ! (horiz-degen-square-β (sq₁ ⊡h sq₂)) ⟩
    horiz-degen-square (horiz-degen-path (sq₁ ⊡h sq₂))
      =⟨ ap horiz-degen-square (horiz-degen-path-⊡h sq₁ sq₂) ⟩
    horiz-degen-square (horiz-degen-path sq₁ ∙ horiz-degen-path sq₂) =∎

module _ {i} {A : Type i} where

  {- TODO rest of these -}

  ⊡h-unit-l : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → hid-square ⊡h sq == sq
  ⊡h-unit-l ids = idp

  ⊡h-unit-r : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → sq ⊡h hid-square == ∙-unit-r _ ∙v⊡ (sq ⊡v∙ ! (∙-unit-r _))
  ⊡h-unit-r ids = idp

  ⊡h'-unit-l : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → hid-square ⊡h' sq == ∙'-unit-l _ ∙v⊡ (sq ⊡v∙ ! (∙'-unit-l _))
  ⊡h'-unit-l ids = idp

  ⊡h-unit-l-unique : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq' : Square p₀₋ idp idp p₀₋) (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → sq' ⊡h sq == sq
    → sq' == hid-square
  ⊡h-unit-l-unique sq' ids p = ! (⊡h-unit-r sq') ∙ p

module _ {i} {A : Type i} where
  !□h-inv-l : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → (!□h sq) ⊡h sq == !-inv-l p₋₀ ∙v⊡ (hid-square ⊡v∙ ! (!-inv-l p₋₁))
  !□h-inv-l ids = idp

  !□h-inv-r : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → sq ⊡h (!□h sq) == !-inv-r p₋₀ ∙v⊡ (hid-square ⊡v∙ ! (!-inv-r p₋₁))
  !□h-inv-r ids = idp

  !□v-inv-l : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → (!□v sq) ⊡v sq == !-inv-l p₀₋ ∙h⊡ (vid-square ⊡h∙ ! (!-inv-l p₁₋))
  !□v-inv-l ids = idp

  !□v-inv-r : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → sq ⊡v (!□v sq) == !-inv-r p₀₋ ∙h⊡ (vid-square ⊡h∙ ! (!-inv-r p₁₋))
  !□v-inv-r ids = idp

module _ {i} {A : Type i} where
  square-left-unique : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ p₀₋' : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square p₀₋' p₋₀ p₋₁ p₁₋
    → p₀₋ == p₀₋'
  square-left-unique {p₋₀ = idp} {p₋₁ = idp} sq₁ sq₂ =
    horiz-degen-path (sq₁ ⊡h (!□h sq₂))

  square-top-unique : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ p₋₀' : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square p₀₋ p₋₀' p₋₁ p₁₋
    → p₋₀ == p₋₀'
  square-top-unique {p₀₋ = idp} {p₁₋ = idp} sq₁ sq₂ =
    vert-degen-path (sq₁ ⊡v (!□v sq₂))

  square-bot-unique : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ p₋₁' : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square p₀₋ p₋₀ p₋₁' p₁₋
    → p₋₁ == p₋₁'
  square-bot-unique {p₀₋ = idp} {p₁₋ = idp} sq₁ sq₂ =
    vert-degen-path ((!□v sq₁) ⊡v sq₂)

  square-right-unique : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ p₁₋' : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square p₀₋ p₋₀ p₋₁ p₁₋'
    → p₁₋ == p₁₋'
  square-right-unique {p₋₀ = idp} {p₋₁ = idp} sq₁ sq₂ =
    horiz-degen-path ((!□h sq₁) ⊡h sq₂)

module _ {i} {A : Type i} where

  {- XXX naminig -}
  connection : {a₀ a₁ : A} {q : a₀ == a₁}
    → Square idp idp q q
  connection {q = idp} = ids

  {- XXX naminig -}
  connection2 : {a₀ a₁ a₂ : A} {p : a₀ == a₁} {q : a₁ == a₂}
    → Square p p q q
  connection2 {p = idp} {q = idp} = ids

  lb-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square p idp (! p) idp
  lb-square idp = ids

  bl-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square (! p) idp p idp
  bl-square idp = ids

  br-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square idp idp p p
  br-square idp = ids

  rb-square = br-square

  rt-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square idp (! p) idp p
  rt-square idp = ids

  tr-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square idp p idp (! p)
  tr-square idp = ids

  lt-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square p p idp idp
  lt-square idp = ids

  tl-square = lt-square

  tr-square-∙v⊡-⊡h∙ : {a₀ a₁ : A} {p p' : a₀ == a₁} (r : p == p')
    → ! r ∙v⊡ tr-square p ⊡h∙ ap ! r == tr-square p'
  tr-square-∙v⊡-⊡h∙ r@idp = idp

  tr-square-! : {a₀ a₁ : A} (p : a₀ == a₁)
    → tr-square (! p) ⊡h∙ !-! p == rt-square p
  tr-square-! p@idp = idp

module _ {i} {j} {A : Type i} {B : Type j} (f : A → B) where

  ap-tr-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → ap-square f (tr-square p) ⊡h∙ ap-! f p == tr-square (ap f p)
  ap-tr-square p@idp = idp

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
------------------------------------------------------------------------
-- Some defined parsers, collected in a library
------------------------------------------------------------------------

-- Recursive parsers cannot be defined simply as functions, but have
-- to be defined in terms of a grammar.

-- Non-recursive parsers can either be defined directly or by using a
-- grammar. The grammar version may be harder to use in some cases,
-- but has the potential advantage of increased sharing/less memory
-- usage.

module RecursiveDescent.Inductive.Lib (tok : Set) where

open import RecursiveDescent.Index
open import RecursiveDescent.Inductive
open import RecursiveDescent.Inductive.SimpleLib
open import Utilities

open import Data.Bool
open import Data.List
open import Data.Nat
open import Data.Product.Record using (_,_)
open import Data.Product renaming (_,_ to pair)

-- The index of atLeast can only be partly inferred.

atLeast-index : Corners -> ℕ -> Index
atLeast-index c zero    = _
atLeast-index c (suc n) = _

private

  -- Note that the parsers are parameterised on other parsers.

  data NT (nt : ParserType₁) : ParserType₁ where
    many     : forall {c r} ->
               Parser tok nt (false , c) r ->
               NT nt _ (List r)
    many₁    : forall {c r} ->
               Parser tok nt (false , c) r ->
               NT nt _ (List r)
    atLeast' : forall {c r} (n : ℕ) ->
               Parser tok nt (false , c) r ->
               NT nt (atLeast-index c n) (List r)
    chain≥'  : forall {c₁ i₂ r} (n : ℕ) ->
               Assoc ->
               Parser tok nt (false , c₁) r ->
               Parser tok nt i₂ (r -> r -> r) ->
               NT nt _ r

Nonterminal : ParserType₁ -> ParserType₁
Nonterminal = NT

module Combinators
         {nt} (lib : forall {i r} -> Nonterminal nt i r -> nt i r)
         where

  infix 55 _⋆ _+

  _⋆ : forall {c r} ->
       Parser tok nt (false , c) r ->
       Parser tok nt _ (List r)
  p ⋆ = ! lib (many p)

  _+ : forall {c r} ->
       Parser tok nt (false , c) r ->
       Parser tok nt _ (List r)
  p + = ! lib (many₁ p)

  -- At least n occurrences of p.

  atLeast : forall {c r} (n : ℕ) ->
            Parser tok nt (false , c) r ->
            Parser tok nt _ (List r)
  atLeast n p = ! lib (atLeast' n p)

  -- Chains at least n occurrences of op, in an a-associative
  -- manner. The ops are surrounded by ps.

  chain≥ : forall {c₁ i₂ r} (n : ℕ) ->
           Assoc ->
           Parser tok nt (false , c₁) r ->
           Parser tok nt i₂ (r -> r -> r) ->
           Parser tok nt _ r
  chain≥ n a p op = ! lib (chain≥' n a p op)

  library : forall {i r} -> Nonterminal nt i r -> Parser tok nt i r
  library (many  p)            = return [] ∣ p +
  library (many₁ p)            = _∷_ <$> p ⊛ p ⋆
  library (atLeast' zero    p) = p ⋆
  library (atLeast' (suc n) p) = _∷_ <$> p ⊛ atLeast n p
  library (chain≥' n a p op)   = chain≥-combine a <$>
                                   p ⊛ atLeast n (op ⊗! p)

ext: agda

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- 2010-11-16
-- compactification of Data.Set.Decoration.gmapAll
--
-- This test case fails if we remove instantiateFull
-- (and with it eta-contraction) from definition bodies in Def.hs
-- see Issue 361

-- {-# OPTIONS -v tc.lhs.unify:25 #-}

module EtaContractionDefBody where

------------------------------------------------------------------------
-- Binary relations

-- Homogeneous binary relations

Rel : Set → Set1
Rel A = A → A → Set

-- Generalised implication. If P ≡ Q it can be read as "f preserves
-- P".

_=[_]⇒_ : {A B : Set} →
          Rel A → (A → B) → Rel B → Set
P =[ f ]⇒ Q = ∀ {x y} → P x y → Q (f x) (f y)

record Σ₂ {A B : Set}
                (T : A → B → Set) : Set  where
  constructor pack₂
  field
    {x}   : A
    {y}   : B
    proof : T x y

-- Data.Star

infixr 5 _◅_

-- Reflexive transitive closure.

data Star {I : Set} (T : Rel I) : Rel I where
  ε   : ∀ {i} → Star T i i
  _◅_ : ∀ {i j k} (x : T i j) (xs : Star T j k) → Star T i k
        -- The type of _◅_ is Trans T (Star T) (Star T); I expanded
        -- the definition in order to be able to name the arguments (x
        -- and xs).

-- A generalised variant of map which allows the index type to change.

gmap : ∀ {I} {T : Rel I} {J} {U : Rel J} →
       (f : I → J) → T =[ f ]⇒ U → Star T =[ f ]⇒ Star U
gmap f g ε        = ε
gmap f g (x ◅ xs) = g x ◅ gmap f g xs

-- Data.Star.Decoration

EdgePred : ∀ {I} → Rel I → Set₁
EdgePred T = ∀ {i j} → T i j → Set

-- Decorating an edge with more information.

data DecoratedWith {I : Set} {T : Rel I} (P : EdgePred T)
       : Rel (Σ₂ (Star T)) where
  ↦ : ∀ {i j k} {x : T i j} {xs : Star T j k}
      (p : P x) → DecoratedWith P (pack₂ (x ◅ xs)) (pack₂ xs)

-- Star-lists decorated with extra information. All P xs means that
-- all edges in xs satisfy P.

All : ∀ {I} {T : Rel I} → EdgePred T → EdgePred (Star T)
All P {j = j} xs =
  Star (DecoratedWith P) (pack₂ xs) (pack₂ {y = j} ε)

-- We can map over decorated vectors.

gmapAll : ∀ {I} {T : Rel I} {P : EdgePred T}
                {J} {U : Rel J} {Q : EdgePred U}
                {i j} {xs : Star T i j}
          (f : I → J) (g : T =[ f ]⇒ U) →
          (∀ {i j} {x : T i j} → P x → Q (g x)) →
          All P xs → All {T = U} Q (gmap f g xs)
gmapAll f g h ε          = ε
gmapAll f g h (↦ x ◅ xs) = ↦ (h x) ◅ gmapAll f g h xs

{- THIS WOULD BE THE ERROR MESSAGE:
/Users/abel/cover/alfa/Agda2/test/succeed/EtaContractionDefBody.agda:76,15-16
xs != ε of type Star (λ .i' .j → T .i' .j) j j
when checking that the pattern ε has type
Star (DecoratedWith (λ {.i} {.j} → P)) (pack₂ xs) (pack₂ ε)
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso