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

module PathInduction where

open import Base public

-- The rewriting relation
{-<rewrite>-}
postulate
  _↦_ : ∀ {i} {A : Type i} → A → A → Type i

{-# BUILTIN REWRITE _↦_ #-}
{-</>-}

-- We redefine concatenation of paths to use induction on both paths, in order
-- to make unification more powerful
infixr 80 _∙_
_∙_ : ∀ {i} {A : Type i} {a b c : A} (p : a == b) (q : b == c) → a == c
idp ∙ idp = idp

record Coh {i} (A : Type i) : Type i where
  field
    & : A
open Coh public

instance
  J→ : ∀ {i j k} {A : Type i} {B : A → Type j} {f : (a : A) → B a} {P : {g : (a : A) → B a} (h : (a : A) → f a == g a) → Type k}
    → Coh (P (λ a → idp)) → Coh ({g : (a : A) → B a} → (h : (a : A) → f a == g a) → P h)
  & (J→ {A = A} {B} {f} {P = P} d) h = transport P (λ= (app=-β h)) (J-aux (λ= h)) where

    J-aux : {g : (a : A) → B a} (h : f == g) → P (app= h)
    J-aux idp = & d

  J→! : ∀ {i j k} {A : Type i} {B : A → Type j} {f : (a : A) → B a} {P : {g : (a : A) → B a} (h : (a : A) → g a == f a) → Type k}
    → Coh (P (λ a → idp)) → Coh ({g : (a : A) → B a} → (h : (a : A) → g a == f a) → P h)
  & (J→! {A = A} {B} {f} {P = P} d) h = transport P (λ= (app=-β h)) (J-aux (λ= h)) where

    J-aux : {g : (a : A) → B a} (h : g == f) → P (app= h)
    J-aux idp = & d

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

 instance

  J- : {B : (a' : A) → a == a' → Type j}
    → Coh (B a idp) → Coh ({a' : A} (p : a == a') → B a' p)
  & (J- d) idp = & d

  J! : {B : (a' : A) → a' == a → Type j}
    → Coh (B a idp) → Coh ({a' : A} (p : a' == a) → B a' p)
  & (J! d) idp = & d

  J□ : {B : {b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} → Square p q r s → Type j}
    → Coh (B ids) → Coh ({b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} (sq : Square p q r s) → B sq)
  & (J□ {B = B} d) ids = & d

  J□i : {B : {b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} → Square p q r s → Type j}
    → Coh (B ids) → Coh ({b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} {sq : Square p q r s} → B sq)
  & (J□i {B = B} d) {sq = ids} = & d

  J□1 : {B : (p : a == a) → Square p idp idp idp → Type j}
    → Coh (B idp ids) → Coh ({p : a == a} (sq : Square p idp idp idp) → B p sq)
  & (J□1 {B = B} d) c = aux B (& d) c  where

    e : {a b c d : A} (q : a == c) (r : b == d) (s : c == d) → Square (q ∙ s ∙ ! r) q r s
    e idp idp idp = ids

    aux : {a b c d : A} {q : a == c} {r : b == d} {s : c == d} (B : (p : a == b) → Square p q r s → Type j)
       → B (q ∙ s ∙ ! r) (e q r s) → {p : a == b} (sq : Square p q r s) → B p sq
    aux B d ids = d

  J□2 : {B : (p : a == a) → Square idp p idp idp → Type j}
    → Coh (B idp ids) → Coh ({p : a == a} (sq : Square idp p idp idp) → B p sq)
  & (J□2 {B = B} d) c = aux B (& d) c  where

    e : {a b c d : A} (p : a == b) (r : b == d) (s : c == d) → Square p (p ∙ r ∙ ! s) r s
    e idp idp idp = ids

    aux : {a b c d : A} {p : a == b} {r : b == d} {s : c == d} (B : (q : a == c) → Square p q r s → Type j)
       → B (p ∙ r ∙ ! s) (e p r s) → {q : a == c} (sq : Square p q r s) → B q sq
    aux B d ids = d

  J□3 : {B : (p : a == a) → Square idp idp p idp → Type j}
    → Coh (B idp ids) → Coh ({p : a == a} (sq : Square idp idp p idp) → B p sq)
  & (J□3 {B = B} d) c = aux B (& d) c  where

    e : {a b c d : A} (p : a == b) (q : a == c) (s : c == d) → Square p q (! p ∙ q ∙ s) s
    e idp idp idp = ids

    aux : {a b c d : A} {p : a == b} {q : a == c} {s : c == d} (B : (r : b == d) → Square p q r s → Type j)
       → B (! p ∙ q ∙ s) (e p q s) → {r : b == d} (sq : Square p q r s) → B r sq
    aux B d ids = d

  J□4 : {B : (p : a == a) → Square idp idp idp p → Type j}
    → Coh (B idp ids) → Coh ({p : a == a} (sq : Square idp idp idp p) → B p sq)
  & (J□4 {B = B} d) c = aux B (& d) c  where

    e : {a b c d : A} (p : a == b) (q : a == c) (r : b == d) → Square p q r (! q ∙ p ∙ r)
    e idp idp idp = ids

    aux : {a b c d : A} {p : a == b} {q : a == c} {r : b == d} (B : (s : c == d) → Square p q r s → Type j)
       → B (! q ∙ p ∙ r) (e p q r) → {s : c == d} (sq : Square p q r s) → B s sq
    aux B d ids = d

instance
  idp-Coh : ∀ {i} {A : Type i} {a : A} → Coh (a == a)
  & idp-Coh = idp

  ids-Coh : ∀ {i} {A : Type i} {a : A} → Coh (Square {a₀₀ = a} idp idp idp idp)
  & ids-Coh = ids

  idc-Coh : ∀ {i} {A : Type i} {a : A} → Coh (Cube {a₀₀₀ = a} ids ids ids ids ids ids)
  & idc-Coh = idc

  -- Allows us to put the initial [a] in the [Coh]
  strip-a : ∀ {i j} {A : Type i} {P : A → A → Type j} → ((a : A) → Coh ({b : A} → P a b)) → Coh ({a b : A} → P a b)
  & (strip-a z) = & (z _)

  -- Allows us to put the initial [A] in the [Coh]
  strip-A : ∀ {i j} {P : Type i → Type j} → ((A : Type i) → Coh (P A)) → Coh ({A : Type i} → P A)
  & (strip-A z) = & (z _)

  -- Allows us to have implicit arguments
  implicit : ∀ {i j k} {A : Type i} {B : A → Type j} {C : (a : A) → B a → Type k} → Coh ({a : A} (b : B a) → C a b) → Coh ({a : A} {b : B a} → C a b)
  & (implicit d) = & d _

path-induction : ∀ {i} {A : Type i} {{a : A}} → A
path-induction {{a}} = a

-- Rules for cubes

instance
  idsidc1-Coh : ∀ {i} {A : Type i} {a : A} → Coh (Σ (Square (idp {a = a}) idp idp idp) (λ left → Cube left ids ids ids ids ids))
  & idsidc1-Coh = (ids , idc)

  idsidc2-Coh : ∀ {i} {A : Type i} {a : A} → Coh (Σ (Square (idp {a = a}) idp idp idp) (λ right → Cube ids right ids ids ids ids))
  & idsidc2-Coh = (ids , idc)

  idsidc6-Coh : ∀ {i} {A : Type i} {a : A} → Coh (Σ (Square (idp {a = a}) idp idp idp) (λ front → Cube ids ids ids ids ids front))
  & idsidc6-Coh = (ids , idc)

module _ {i j} {A : Type i} {a : A} where
 instance

  JCube1 : {B : (p : Square {a₀₀ = a} idp idp idp idp) → Cube p ids ids ids ids ids → Type j}
    → Coh (B ids idc) → Coh ({p : Square {a₀₀ = a} idp idp idp idp} (cube : Cube p ids ids ids ids ids) → B p cube)
  & (JCube1 {B = B} d) c = aux B (& d) c  where

    comp : Coh ({a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
           {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
           {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
           (right : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁)

           {a₀₀₀ : A} {p₀₀₋ : a₀₀₀ == a₀₀₁}
           {a₀₁₀ : A} {p₀₁₋ : a₀₁₀ == a₀₁₁}
           {a₁₀₀ : A} {p₁₀₋ : a₁₀₀ == a₁₀₁}
           {a₁₁₀ : A} {p₁₁₋ : a₁₁₀ == a₁₁₁}

           {p₀₋₀ : a₀₀₀ == a₀₁₀}
           (back : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁)
           {p₋₀₀ : a₀₀₀ == a₁₀₀}
           (top : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁)
           {p₋₁₀ : a₀₁₀ == a₁₁₀}
           (bottom : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁)
           {p₁₋₀ : a₁₀₀ == a₁₁₀}
           (front : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁)
           → Σ (Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀) (λ left → Cube left right back top bottom front))
    comp = path-induction

    aux :  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
           {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
           {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
           -- missing left

           {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
           {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
           {right : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁}

           {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
           {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
           {back : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁}
           {top : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁}
           {bottom : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁}
           {front : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁}
           → (B : (left : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀) → Cube left right back top bottom front → Type j)
           → uncurry B (& comp right back top bottom front)
           → ({left : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} (cube : Cube left right back top bottom front) → B left cube)
    aux B d idc = d

  JCube2 : {B : (p : Square {a₀₀ = a} idp idp idp idp) → Cube ids p ids ids ids ids → Type j}
    → Coh (B ids idc) → Coh ({p : Square {a₀₀ = a} idp idp idp idp} (cube : Cube ids p ids ids ids ids) → B p cube)
  & (JCube2 {B = B} d) c = aux B (& d) c  where

    comp : Coh ({a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ : A}
           {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
           {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
           (left : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀)

           {a₀₀₁ : A} {p₀₀₋ : a₀₀₀ == a₀₀₁}
           {a₀₁₁ : A} {p₀₁₋ : a₀₁₀ == a₀₁₁}
           {a₁₀₁ : A} {p₁₀₋ : a₁₀₀ == a₁₀₁}
           {a₁₁₁ : A} {p₁₁₋ : a₁₁₀ == a₁₁₁}

           {p₀₋₁ : a₀₀₁ == a₀₁₁}
           (back : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁)
           {p₋₀₁ : a₀₀₁ == a₁₀₁}
           (top : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁)
           {p₋₁₁ : a₀₁₁ == a₁₁₁}
           (bottom : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁)
           {p₁₋₁ : a₁₀₁ == a₁₁₁}
           (front : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁)
           → Σ (Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁) (λ right → Cube left right back top bottom front))
    comp = path-induction

    aux :  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
           {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
           {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
           {left : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀}

           {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
           {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}

           {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
           {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
           {back : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁}
           {top : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁}
           {bottom : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁}
           {front : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁}
           → (B : (right : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁) → Cube left right back top bottom front → Type j)
           → uncurry B (& comp left back top bottom front)
           → ({right : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} (cube : Cube left right back top bottom front) → B right cube)
    aux B d idc = d

  JCube6 : {B : (p : Square {a₀₀ = a} idp idp idp idp) → Cube ids ids ids ids ids p → Type j}
    → Coh (B ids idc) → Coh ({p : Square {a₀₀ = a} idp idp idp idp} (cube : Cube ids ids ids ids ids p) → B p cube)
  & (JCube6 {B = B} d) c = aux B (& d) c  where

    comp : Coh ({a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ : A}
           {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
           {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
           (left : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀)

           {a₀₀₁ : A} {p₀₀₋ : a₀₀₀ == a₀₀₁}
           {a₀₁₁ : A} {p₀₁₋ : a₀₁₀ == a₀₁₁}
           {a₁₀₁ : A} {p₁₀₋ : a₁₀₀ == a₁₀₁}
           {a₁₁₁ : A} {p₁₁₋ : a₁₁₀ == a₁₁₁}

           {p₀₋₁ : a₀₀₁ == a₀₁₁}
           (back : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁)
           {p₋₀₁ : a₀₀₁ == a₁₀₁}
           (top : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁)
           {p₋₁₁ : a₀₁₁ == a₁₁₁}
           (bottom : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁)
           {p₁₋₁ : a₁₀₁ == a₁₁₁}
           (right : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁)
           → Σ (Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁) (λ front → Cube left right back top bottom front))
    comp = path-induction

    aux :  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
           {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
           {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
           {left : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀}

           {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
           {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
           {right : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁}

           {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
           {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
           {back : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁}
           {top : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁}
           {bottom : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁}
           → (B : (front : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁) → Cube left right back top bottom front → Type j)
           → uncurry B (& comp left back top bottom right)
           → ({front : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} (cube : Cube left right back top bottom front) → B front cube)
    aux B d idc = d

-- Flat cubes (cubes where the four lateral faces are actually only 2-dimensional paths
data FlatCube {i} {A : Type i} {a : A} :
  {b c d : A} {p p' : a == b} {q q' : a == c} {r r' : b == d} {s s' : c == d}
  → Square p q r s → Square p' q' r' s' → p == p' → q == q' → r == r' → s == s' → Type i where
  idfc : FlatCube ids ids idp idp idp idp

instance
  idfc-Coh : ∀ {i} {A : Type i} {a : A} → Coh (FlatCube {a = a} ids ids idp idp idp idp)
  & idfc-Coh = idfc

  JFlatCube1 : ∀ {i j} {A : Type i} {a : A} {B : (p : Square {a₀₀ = a} idp idp idp idp) → FlatCube p ids idp idp idp idp → Type j}
    → Coh (B ids idfc) → Coh ({p : Square {a₀₀ = a} idp idp idp idp} (cube : FlatCube p ids idp idp idp idp) → B p cube)
  & (JFlatCube1 {i} {j} {B = B} d) c = aux B (& d) c  where

    comp : {A : Type i} {a b c d : A} {p' : a == b} {q' : a == c} {r' : b == d} {s' : c == d} (sq' : Square p' q' r' s')
           {p : a == b} (p= : p == p') {q : a == c} (q= : q == q') {r : b == d} (r= : r == r') {s : c == d} (s= : s == s')
         → Square p q r s
    comp ids idp idp idp idp = ids

    fill : {A : Type i} {a b c d : A} {p' : a == b} {q' : a == c} {r' : b == d} {s' : c == d} (sq' : Square p' q' r' s')
           {p : a == b} (p= : p == p') {q : a == c} (q= : q == q') {r : b == d} (r= : r == r') {s : c == d} (s= : s == s')
         → FlatCube (comp sq' p= q= r= s=) sq' p= q= r= s=
    fill ids idp idp idp idp = idfc

    aux : {A : Type i} {a b c d : A} {p' : a == b} {q' : a == c} {r' : b == d} {s' : c == d} {sq' : Square p' q' r' s'}
          {p : a == b} {p= : p == p'} {q : a == c} {q= : q == q'} {r : b == d} {r= : r == r'} {s : c == d} {s= : s == s'}
         (B : (sq : Square p q r s) (fil : FlatCube sq sq' p= q= r= s=) → Type j)
          → B (comp sq' p= q= r= s=) (fill sq' p= q= r= s=)
          → {sq : Square p q r s} (fil : FlatCube sq sq' p= q= r= s=) → B sq fil
    aux B d idfc = d

  JFlatCube2 : ∀ {i j} {A : Type i} {a : A} {B : (p : Square {a₀₀ = a} idp idp idp idp) → FlatCube ids p idp idp idp idp → Type j}
    → Coh (B ids idfc) → Coh ({p : Square {a₀₀ = a} idp idp idp idp} (cube : FlatCube ids p idp idp idp idp) → B p cube)
  & (JFlatCube2 d) idfc = & d

ap-∙ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a b c : A} (p : a == b) (q : b == c) → ap f (p ∙ q) == ap f p ∙ ap f q
ap-∙ f idp idp = idp

ap-∙! : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a b : A} (p : a == b) {c : A} (q : c == b) → ap f (p ∙ ! q) == ap f p ∙ ! (ap f q)
ap-∙! f idp idp = idp

ap-shape-∙! : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a b c : A} {p : a == b} {q : a == c} {r : b == c}
  → p == q ∙ ! r → ap f p == ap f q ∙ ! (ap f r)
ap-shape-∙! f {q = idp} {r = idp} idp = idp

ap-!∙ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a b : A} (p : b == a) {c : A} (q : b == c) → ap f (! p ∙ q) == ! (ap f p) ∙ ap f q
ap-!∙ f idp idp = idp

∘-ap : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B)
  {x y : A} (p : x == y) → ap g (ap f p) == ap (g ∘ f) p
∘-ap f g p = ! (ap-∘ f g p)

∙idp : ∀ {i} {A : Type i} {a b : A} {p : a == b} → p ∙ idp == p
∙idp {p = idp} = idp

idp∙ : ∀ {i} {A : Type i} {a a' : A} {p : a == a'} → idp ∙ p == p
idp∙ {p = idp} = idp

!-inv-r : ∀ {i} {A : Type i} {a b : A} {p : a == b} → p ∙ ! p == idp
!-inv-r {p = idp} = idp

!-inv-l : ∀ {i} {A : Type i} {a b : A} {p : a == b} → ! p ∙ p == idp
!-inv-l {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 idp = hid-square

  vert-degen-square : {a a' : A} {p q : a == a'}
    → p == q → Square idp p q idp
  vert-degen-square idp = vid-square

  horiz-degen-path : {a a' : A} {p q : a == a'}
    → Square p idp idp q → p == q
  horiz-degen-path {p = idp} ids = idp

  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

  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 = ids} = idp

  horiz-degen-square-η : {a a' : A} {p q : a == a'} {r : p == q} → horiz-degen-path (horiz-degen-square r) == r
  horiz-degen-square-η {p = idp} {r = idp} = idp

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

  natural-square : (h : (a : A) → f a == g a)
    {x y : A} (p : x == y)
    → {fp : f x == f y} (fp= : ap f p == fp)
    → {gp : g x == g y} (gp= : ap g p == gp)
    → Square (h x) fp gp (h y)
  natural-square h idp idp idp = hid-square

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

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

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

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

  ↓-ap-in2 : {x y : A} {p : x == y} {u : C (f x)} {v : C (f y)}
    {fp : f x == f y} (fp= : ap f p == fp)
    → u == v [ C ∘ f ↓ p ]
    → u == v [ C ↓ fp ]
  ↓-ap-in2 {p = idp} idp idp = idp

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

  ↓-ap-in-coh : {X : Type i} {g : X → A} {x y : X} {p : x == y} {gp : g x == g y} {p-β : ap g p == gp} (h : (a : A) → C (f a))
    → ↓-ap-in C f (apd h gp) == ↓-ap-in2 C (f ∘ g) (ap-∘ f g p ∙ ap (ap f) p-β) (apd (h ∘ g) p)
  ↓-ap-in-coh {p = idp} {p-β = idp} h = idp

↓-PathOver-from-square : ∀ {i j} {A X : Type i} {P : A → Type j} {a b : X → A}
  {q : (x : X) → a x == b x} {f : (x : X) → P (a x)} {g : (x : X) → P (b x)}
  {x y : X} {p : x == y} {u : PathOver P (q x) (f x) (g x)} {v : PathOver P (q y) (f y) (g y)}
  {a-p : a x == a y} {ap= : ap a p == a-p}
  {b-p : b x == b y} {bp= : ap b p == b-p}
  → SquareOver P (natural-square q p ap= bp=) u (↓-ap-in2 P a {p = p} ap= (apd f p)) (↓-ap-in2 P b bp= (apd g p)) v
  → u == v [ (λ z → f z == g z [ P ↓ q z ]) ↓ p ]
↓-PathOver-from-square {p = idp} {ap= = idp} {bp= = idp} pq = coh pq  where

  coh : ∀ {i j} {A : Type i} {P : A → Type j} {a b : A} {q : a == b} {f : P a} {g : P b} {u v : f == g [ P ↓ q ]}
      → SquareOver P hid-square u idp idp v → u == v
  coh {q = idp} {u = idp} ids = idp

adapt-SquareOver : ∀ {i j} {A : Type i} {P : A → Type j} {a b c d : A}
  {p : a == b} {q : a == c} {r : b == d} {s : c == d} {sq : Square p q r s}
  {a' : P a} {b' : P b} {c' : P c} {d' : P d}
  {p' : a' == b' [ P ↓ p ]} {q' q'2 : a' == c' [ P ↓ q ]}
  {r' r'2 : b' == d' [ P ↓ r ]} {s' : c' == d' [ P ↓ s ]}
  (q'= : q' == q'2) (r'= : r' == r'2)
  → SquareOver P sq p' q' r' s'
  → SquareOver P sq p' q'2 r'2 s'
adapt-SquareOver {sq = ids} idp idp ids = ids

ap-square-natural-square : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : B → C) →
  Coh ({a b : A} (p : a == b) {u v : A → B} (g : (x : A) → u x == v x)
      {up : u a == u b} {up= : ap u p == up}
      {vp : v a == v b} {vp= : ap v p == vp}
      {fup : ap (λ z → f (u z)) p == ap f up} (fup= : ap-∘ f u p ∙ ap (ap f) up= == fup)
      {fvp : ap (λ z → f (v z)) p == ap f vp} (fvp= : ap-∘ f v p ∙ ap (ap f) vp= == fvp)
    → ap-square f (natural-square g p up= vp=) == natural-square (ap f ∘ g) p fup fvp)
ap-square-natural-square {i} {j} {k} f = path-induction

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

adapt-square : ∀ {i} {A : Type i} {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} (sq : Square p q r s)
               {q' : a == c} (q= : q == q') {r' : b == d} (r= : r == r')
             → Square p q' r' s
adapt-square ids idp idp = ids

ap2-idf : ∀ {i} → Coh ({A : Type i} {x y : A} {p q : x == y} {r : p == q} → Square (ap (ap (λ z → z)) r) (ap-idf _) (ap-idf _) r)
ap2-idf = path-induction

ap-∘3 : ∀ {i j k l} {A : Type i} {B : Type j} {C : Type k} {D : Type l}
        (f : C → D) (g : B → C) (h : A → B) {a b : A} (p : a == b)
      → Square (ap-∘ f (g ∘ h) p) (ap-∘ (f ∘ g) h p) (ap (ap f) (ap-∘ g h p)) (ap-∘ f g (ap h p))
ap-∘3 f g h idp = ids

_∙□_ : ∀ {i} {A : Type i} {a b c d e f : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} {t : c == e} {u : d == f} {v : e == f}
         (sq1 : Square p q r s) (sq2 : Square s t u v)
       → Square p (q ∙ t) (r ∙ u) v
ids ∙□ ids = ids

_|∙_ : ∀ {i} {A : Type i} {a b c d : A} {p p' : a == b} {q : a == c} {r : b == d} {s : c == d}
         (p= : p == p') (sq1 : Square p' q r s)
       → Square p q r s
idp |∙ ids = ids

_∙|_ : ∀ {i} {A : Type i} {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s s' : c == d}
         (sq1 : Square p q r s) (s= : s == s')
       → Square p q r s'
ids ∙| idp = ids

infixr 80 _∙□_ _|∙_ _∙|_

_∙³x_ : ∀ {i} {A : Type i}
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ a₀₀₂ a₀₁₂ a₁₀₂ a₁₁₂ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- middle

  {p₀₋₂ : a₀₀₂ == a₀₁₂} {p₋₀₂ : a₀₀₂ == a₁₀₂}
  {p₋₁₂ : a₀₁₂ == a₁₁₂} {p₁₋₂ : a₁₀₂ == a₁₁₂}
  {sq₋₋₂ : Square p₀₋₂ p₋₀₂ p₋₁₂ p₁₋₂} -- right

  {p₀₀l : a₀₀₀ == a₀₀₁} {p₀₁l : a₀₁₀ == a₀₁₁}
  {p₁₀l : a₁₀₀ == a₁₀₁} {p₁₁l : a₁₁₀ == a₁₁₁}
  {sq₀₋l : Square p₀₋₀ p₀₀l p₀₁l p₀₋₁} -- backl
  {sq₋₀l : Square p₋₀₀ p₀₀l p₁₀l p₋₀₁} -- topl
  {sq₋₁l : Square p₋₁₀ p₀₁l p₁₁l p₋₁₁} -- bottoml
  {sq₁₋l : Square p₁₋₀ p₁₀l p₁₁l p₁₋₁} -- frontl

  {p₀₀r : a₀₀₁ == a₀₀₂} {p₀₁r : a₀₁₁ == a₀₁₂}
  {p₁₀r : a₁₀₁ == a₁₀₂} {p₁₁r : a₁₁₁ == a₁₁₂}
  {sq₀₋r : Square p₀₋₁ p₀₀r p₀₁r p₀₋₂} -- backr
  {sq₋₀r : Square p₋₀₁ p₀₀r p₁₀r p₋₀₂} -- topr
  {sq₋₁r : Square p₋₁₁ p₀₁r p₁₁r p₋₁₂} -- bottomr
  {sq₁₋r : Square p₁₋₁ p₁₀r p₁₁r p₁₋₂} -- frontr

  → Cube sq₋₋₀ sq₋₋₁ sq₀₋l sq₋₀l sq₋₁l sq₁₋l
  → Cube sq₋₋₁ sq₋₋₂ sq₀₋r sq₋₀r sq₋₁r sq₁₋r
  → Cube sq₋₋₀ sq₋₋₂ (sq₀₋l ∙□ sq₀₋r) (sq₋₀l ∙□ sq₋₀r)
         (sq₋₁l ∙□ sq₋₁r) (sq₁₋l ∙□ sq₁₋r)
idc ∙³x idc = idc

infixr 80 _∙³x_

x-degen-cube : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {sq₋₋₀ sq₋₋₁ : Square p₀₋ p₋₀ p₋₁ p₁₋}
  → sq₋₋₀ == sq₋₋₁
  → Cube sq₋₋₀ sq₋₋₁ hid-square hid-square hid-square hid-square
x-degen-cube {sq₋₋₀ = ids} idp = idc

natural-cube-η∞ : ∀ {i j} {A : Type i} {B : Type j}
  {u : A → B}
  {r : (a : A) → u a == u a}
  (p : ∀ a → r a == idp)
  {x y : A} (q : x == y)
  {uq : u x == u y} {uq= : ap u q == uq}
  → Cube (horiz-degen-square (p x)) (horiz-degen-square (p y))
         (natural-square r q uq= uq=) vid-square vid-square vid-square
natural-cube-η∞ p idp {uq= = idp} = x-degen-cube idp

natural-square-∘ : ∀ {i} {A B C : Type i} {a b : C} (p : a == b) (k : C → A) →
         Coh ({f g : A → B} (h : (a : A) → f a == g a)
              {fkp : _} {fkp= : ap (f ∘ k) p == fkp}
              {gkp : _} {gkp= : ap (g ∘ k) p == gkp}
              {fkp2 : _} (fkp2= : ∘-ap f k p ∙ fkp= == fkp2)
              {gkp2 : _} (gkp2= : ∘-ap g k p ∙ gkp= == gkp2)
         → natural-square (h ∘ k) p fkp= gkp= == natural-square h (ap k p) fkp2 gkp2)
natural-square-∘ idp = path-induction

_-∙³_ : ∀ {i} {A : Type i}
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ sq₋₋₀' : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀ : a₀₀₀ == a₀₀₁} {p₀₁ : a₀₁₀ == a₀₁₁}
  {p₁₀ : a₁₀₀ == a₁₀₁} {p₁₁ : a₁₁₀ == a₁₁₁}
  {sq₀₋ : Square p₀₋₀ p₀₀ p₀₁ p₀₋₁} -- back
  {sq₋₀ : Square p₋₀₀ p₀₀ p₁₀ p₋₀₁} -- top
  {sq₋₁ : Square p₋₁₀ p₀₁ p₁₁ p₋₁₁} -- bottom
  {sq₁₋ : Square p₁₋₀ p₁₀ p₁₁ p₁₋₁} -- front

  → (sq₋₋₀ == sq₋₋₀')
  → Cube sq₋₋₀' sq₋₋₁ sq₀₋ sq₋₀ sq₋₁ sq₁₋
  → Cube sq₋₋₀  sq₋₋₁ sq₀₋ sq₋₀ sq₋₁ sq₁₋
idp -∙³ idc = idc

_-|∙³_ : ∀ {i} {A : Type i} → {a₀₀₀ a₀₁₀ : A}
  {a b p₀₋₀ p₁₋₀ : a₀₀₀ == a₀₁₀}
  {p : a == b} {q : a == p₀₋₀} {r : b == p₁₋₀}
  {sq₋₋₀ : p₀₋₀ == p₁₋₀} -- left

  (α : Square p q r sq₋₋₀)

  {a₀₀₁ : A} {p₀₀₋ : a₀₀₀ == a₀₀₁}
  {a₀₁₁ : A} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {a₁₀₁ : A} {p₁₀₋ : a₀₀₀ == a₁₀₁}
  {a₁₁₁ : A} {p₁₁₋ : a₀₁₀ == a₁₁₁}

  {p₀₋₁ : a₀₀₁ == a₀₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {sq₋₀₋ : Square idp p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {p₋₁₁ : a₀₁₁ == a₁₁₁}
  {sq₋₁₋ : Square idp p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front

  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right
    → Cube (horiz-degen-square sq₋₋₀) sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
    → Cube (horiz-degen-square p) sq₋₋₁ (q |∙ sq₀₋₋ ) sq₋₀₋ sq₋₁₋ (r |∙ sq₁₋₋)
ids -|∙³ idc = idc

infixr 80 _-|∙³_

adapt-cube : ∀ {i} {A : Type i} {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  (cube : Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋ )

  {p₀₀₋' : a₀₀₀ == a₀₀₁} (p₀₀₋= : p₀₀₋ == p₀₀₋') {p₀₁₋' : a₀₁₀ == a₀₁₁} (p₀₁₋= : p₀₁₋ == p₀₁₋')
  {p₁₀₋' : a₁₀₀ == a₁₀₁} (p₁₀₋= : p₁₀₋ == p₁₀₋') {p₁₁₋' : a₁₁₀ == a₁₁₁} (p₁₁₋= : p₁₁₋ == p₁₁₋')
  {sq₀₋₋' : Square p₀₋₀ p₀₀₋' p₀₁₋' p₀₋₁} (sq₀₋₋= : adapt-square sq₀₋₋ p₀₀₋= p₀₁₋= == sq₀₋₋') -- back
  {sq₋₀₋' : Square p₋₀₀ p₀₀₋' p₁₀₋' p₋₀₁} (sq₋₀₋= : adapt-square sq₋₀₋ p₀₀₋= p₁₀₋= == sq₋₀₋') -- top
  {sq₋₁₋' : Square p₋₁₀ p₀₁₋' p₁₁₋' p₋₁₁} (sq₋₁₋= : adapt-square sq₋₁₋ p₀₁₋= p₁₁₋= == sq₋₁₋') -- bottom
  {sq₁₋₋' : Square p₁₋₀ p₁₀₋' p₁₁₋' p₁₋₁} (sq₁₋₋= : adapt-square sq₁₋₋ p₁₀₋= p₁₁₋= == sq₁₋₋') -- front

  → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋' sq₋₀₋' sq₋₁₋' sq₁₋₋'
adapt-cube idc idp idp idp idp idp idp idp idp = idc

adapt-cube-idp : ∀ {i} {A : Type i} {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  (cube : Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋ )

  {sq₀₋₋' : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} (sq₀₋₋= : sq₀₋₋ == sq₀₋₋') -- back
  {sq₋₀₋' : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} (sq₋₀₋= : sq₋₀₋ == sq₋₀₋') -- top
  {sq₋₁₋' : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} (sq₋₁₋= : sq₋₁₋ == sq₋₁₋') -- bottom
  {sq₁₋₋' : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} (sq₁₋₋= : sq₁₋₋ == sq₁₋₋') -- front

  → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋' sq₋₀₋' sq₋₁₋' sq₁₋₋'
adapt-cube-idp idc idp idp idp idp = idc

{- A SquareOver between paths can be represented as a cube -}
module _ {i j} {A : Type i} {B : Type j} {f g : A → B}
  where

  cube-to-↓-square : {a : A} {a= : f a == g a}
    {b : A} {p : a == b} {c : A} {q : a == c} {d : A} {r : b == d} {s : c == d}
    {sq : Square p q r s}
    {fp : _} {fp= : ap f p == fp}
    {fq : _} {fq= : ap f q == fq}
    {fr : _} {fr= : ap f r == fr}
    {fs : _} {fs= : ap f s == fs}
    {b= : f b == g b}
    (p= : Square fp a= b= (ap g p))
    {c= : f c == g c}
    {q= : Square fq a= c= (ap g q)}
    {q□ : PathOver (λ z → f z == g z) q a= c=}
    (q□= : q□ == ↓-='-from-square fq= idp (square-symmetry q=))
    {d= : f d == g d}
    {r= : Square b= fr (ap g r) d=}
    {r□ : PathOver (λ z → f z == g z) r b= d=}
    (r□= : r□ == ↓-='-from-square fr= idp r=)
    (s= : Square fs c= d= (ap g s))
    → Cube (ap-square f sq) (ap-square g sq) (fp= |∙ p=) (fq= |∙ q=) (fr= |∙ square-symmetry r=) (fs= |∙ s=)
    → SquareOver (λ z → f z == g z) sq (↓-='-from-square fp= idp (square-symmetry p=))
                                       q□
                                       r□
                                       (↓-='-from-square fs= idp (square-symmetry s=))
  cube-to-↓-square {sq = ids} {fp= = idp} {fq= = idp} {fr= = idp} {fs= = idp} p= idp idp s= cube = & coh cube (& coh2)  where

    coh : Coh ({A : Type j} {x y : A} {a= b= : x == y} {p= : Square idp a= b= idp} {c= : x == y} {q= : Square idp a= c= idp} {d= : x == y} {r= : Square b= idp idp d=} {s=' : Square idp c= d= idp}
        → Cube ids ids (idp |∙ p=) (idp |∙ q=) (idp |∙ square-symmetry r=) s='
        → {s= : Square idp c= d= idp} (s== : s= == s=')
        → Square (horiz-degen-path (square-symmetry p=))
                 (horiz-degen-path (square-symmetry q=))
                 (horiz-degen-path r=)
                 (horiz-degen-path (square-symmetry s=)))
    coh = path-induction

    coh2 : Coh ({A : Type j} {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} {sq : Square p q r s} → sq == idp |∙ sq)
    coh2 = path-induction

x-degen-cube-in : ∀ {i} → Coh ({A : Type i} {a b c d : A}
  {p : a == b} {q : a == c}
  {r : b == d} {s : c == d}
  {sq sq' : Square p q r s}
  → sq == sq'
  → Cube sq sq' hid-square hid-square hid-square hid-square)
x-degen-cube-in = path-induction

x-degen-cube-out : ∀ {i} → Coh ({A : Type i} {a b c d : A}
  {p : a == b} {q : a == c}
  {r : b == d} {s : c == d}
  {sq sq' : Square p q r s}
  → Cube sq sq' hid-square hid-square hid-square hid-square
  → sq == sq')
x-degen-cube-out = path-induction

{- A pathover between squares can be represented as a cube -}
module _ {i j} {A : Type i} {B : Type j} {b₀₀ b₀₁ b₁₀ b₁₁ : A → B}
  {p₀₋ : (a : A) → b₀₀ a == b₀₁ a} {p₋₀ : (a : A) → b₀₀ a == b₁₀ a}
  {p₋₁ : (a : A) → b₀₁ a == b₁₁ a} {p₁₋ : (a : A) → b₁₀ a == b₁₁ a}
  where

  cube-to-↓-path : {x y : A} {q : x == y}
    {sqx : Square (p₀₋ x) (p₋₀ x) (p₋₁ x) (p₁₋ x)}
    {sqy : Square (p₀₋ y) (p₋₀ y) (p₋₁ y) (p₁₋ y)}
    {b₀₀q : b₀₀ x == b₀₀ y} (b₀₀q= : ap b₀₀ q == b₀₀q)
    {b₀₁q : b₀₁ x == b₀₁ y} (b₀₁q= : ap b₀₁ q == b₀₁q)
    {b₁₀q : b₁₀ x == b₁₀ y} (b₁₀q= : ap b₁₀ q == b₁₀q)
    {b₁₁q : b₁₁ x == b₁₁ y} (b₁₁q= : ap b₁₁ q == b₁₁q)
    → Cube sqx sqy
           (natural-square p₀₋ q b₀₀q= b₀₁q=) (natural-square p₋₀ q b₀₀q= b₁₀q=)
           (natural-square p₋₁ q b₀₁q= b₁₁q=) (natural-square p₁₋ q b₁₀q= b₁₁q=)
    → sqx == sqy [ (λ z → Square (p₀₋ z) (p₋₀ z) (p₋₁ z) (p₁₋ z)) ↓ q ]
  cube-to-↓-path {q = idp} idp idp idp idp cu = & x-degen-cube-out cu

_|∙³_ : ∀ {i} {A : Type i}
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ p₀₋₀' : a₀₀₀ == a₀₁₀} {p₋₀₀ p₋₀₀' : a₀₀₀ == a₁₀₀}
  {p₋₁₀ p₋₁₀' : a₀₁₀ == a₁₁₀} {p₁₋₀ p₁₋₀' : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₀= : p₀₋₀ == p₀₋₀'} {p₋₀₀= : p₋₀₀ == p₋₀₀'}
  {p₋₁₀= : p₋₁₀ == p₋₁₀'} {p₁₋₀= : p₁₋₀ == p₁₋₀'}
  {sq₋₋₀' : Square p₀₋₀' p₋₀₀' p₋₁₀' p₁₋₀'} -- middle

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀' p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀' p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀' p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀' p₁₀₋ p₁₁₋ p₁₋₁} -- front

  → FlatCube sq₋₋₀ sq₋₋₀' p₀₋₀= p₋₀₀= p₋₁₀= p₁₋₀=
  → Cube sq₋₋₀' sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  → Cube sq₋₋₀ sq₋₋₁ (p₀₋₀= |∙ sq₀₋₋) (p₋₀₀= |∙ sq₋₀₋) (p₋₁₀= |∙ sq₋₁₋) (p₁₋₀= |∙ sq₁₋₋)
idfc |∙³ idc = idc

_/∙³_ : ∀ {i} {A : Type i} {a b c d : A} {p p' : a == b} {q q' : a == c} {r r' : b == d} {s s' : c == d}
  {sq sq2 : Square p q r s} (sq= : sq == sq2)
  {sq' : Square p' q' r' s'} {p= : p == p'} {q= : q == q'} {r= : r == r'} {s= : s == s'}
  → FlatCube sq2 sq' p= q= r= s=
  → FlatCube sq sq' p= q= r= s=
idp /∙³ idfc = idfc

_∙³/_ : ∀ {i} {A : Type i} {a b c d : A} {p p' : a == b} {q q' : a == c} {r r' : b == d} {s s' : c == d}
  {sq : Square p q r s}
  {sq' : Square p' q' r' s'} {p= : p == p'} {q= : q == q'} {r= : r == r'} {s= : s == s'}
  → FlatCube sq sq' p= q= r= s=
  → {sq'2 : Square p' q' r' s'} → sq' == sq'2
  → FlatCube sq sq'2 p= q= r= s=
idfc ∙³/ idp = idfc

_∙fc_ : ∀ {i} {A : Type i} {a b c d : A} {p p' p'' : a == b} {q q' q'' : a == c} {r r' r'' : b == d} {s s' s'' : c == d}
  {sq : Square p q r s} {sq' : Square p' q' r' s'} {sq'' : Square p'' q'' r'' s''}
  {p= : p == p'} {q= : q == q'} {r= : r == r'} {s= : s == s'}
  {p=' : p' == p''} {q=' : q' == q''} {r=' : r' == r''} {s=' : s' == s''}
  → FlatCube sq  sq'  p=  q=  r=  s=
  → FlatCube sq' sq'' p=' q=' r=' s='
  → FlatCube sq  sq'' (p= ∙ p=') (q= ∙ q=') (r= ∙ r=') (s= ∙ s=')
idfc ∙fc idfc = idfc

infixr 80 _|∙³_ _-∙³_ _/∙³_ _∙fc_ _∙³/_

adapt-flatcube : ∀ {i} {A : Type i} {a b c d : A} {p p' : a == b} {q q' : a == c} {r r' : b == d} {s s' : c == d}
  {p= p=' : p == p'} (p== : p= == p=')
  {q= q=' : q == q'} (q== : q= == q=')
  {r= r=' : r == r'} (r== : r= == r=')
  {s= s=' : s == s'} (s== : s= == s=')
  {sq : Square p q r s} {sq' : Square p' q' r' s'}
  → FlatCube sq sq' p= q= r= s=
  → FlatCube sq sq' p=' q=' r=' s='
adapt-flatcube idp idp idp idp idfc = idfc

!² : ∀ {i} {A : Type i} {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d}
  → Square p q r s → Square s (! q) (! r) p
!² ids = ids

!³ : ∀ {i} {A : Type i}
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀ : a₀₀₀ == a₀₀₁} {p₀₁ : a₀₁₀ == a₀₁₁}
  {p₁₀ : a₁₀₀ == a₁₀₁} {p₁₁ : a₁₁₀ == a₁₁₁}
  {sq₀₋ : Square p₀₋₀ p₀₀ p₀₁ p₀₋₁} -- back
  {sq₋₀ : Square p₋₀₀ p₀₀ p₁₀ p₋₀₁} -- top
  {sq₋₁ : Square p₋₁₀ p₀₁ p₁₁ p₋₁₁} -- bottom
  {sq₁₋ : Square p₁₋₀ p₁₀ p₁₁ p₁₋₁} -- front
  → Cube sq₋₋₀ sq₋₋₁ sq₀₋ sq₋₀ sq₋₁ sq₁₋
  → Cube sq₋₋₁ sq₋₋₀ (!² sq₀₋) (!² sq₋₀) (!² sq₋₁) (!² sq₁₋)
!³ idc = idc

natural-square-homotopy : ∀ {i j} {A : Type i} {B : Type j} {a : A}
  → Coh ({u v : A → B} {f g : (x : A) → u x == v x} (h : (x : A) → f x == g x)
      {b : A} (p : a == b)
      {up : u a == u b} {up= : ap u p == up}
      {vp : v a == v b} {vp= : ap v p == vp}
      → FlatCube (natural-square f p up= vp=) (natural-square g p up= vp=) (h a) idp idp (h b))
natural-square-homotopy = path-induction

natural-cube2 : ∀ {i j} {A : Type i} {B : Type j} {a : A} →
  Coh ({f g : A → B} (h : (a : A) → f a == g a) {b : A} {p : a == b} {c : A} {q : a == c} {d : A} {r : b == d}
  {s : c == d} (sq : Square p q r s)
  {fp : f a == f b} {fp= : ap f p == fp} {gp : g a == g b} {gp= : ap g p == gp}
  {fq : f a == f c} {fq= : ap f q == fq} {gq : g a == g c} {gq= : ap g q == gq}
  {fr : f b == f d} {fr= : ap f r == fr} {gr : g b == g d} {gr= : ap g r == gr}
  {fs : f c == f d} {fs= : ap f s == fs} {gs : g c == g d} {gs= : ap g s == gs}
  {fsq : Square fp fq fr fs} (fsq= : FlatCube (ap-square f sq) fsq fp= fq= fr= fs=)
  {gsq : Square gp gq gr gs} (gsq= : FlatCube (ap-square g sq) gsq gp= gq= gr= gs=)
  → Cube (natural-square h p fp= gp=) (natural-square h s fs= gs=) (natural-square h q fq= gq=) fsq gsq (natural-square h r fr= gr=))
natural-cube2 = path-induction

ap-square-idf : ∀ {i} {A : Type i} {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d}
  (sq : Square p q r s)
  → FlatCube (ap-square (λ z → z) sq) sq (ap-idf p) (ap-idf q) (ap-idf r) (ap-idf s)
ap-square-idf ids = idfc

hid-flatcube : ∀ {i} {A : Type i} {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} (sq : Square p q r s)
  → FlatCube sq sq idp idp idp idp
hid-flatcube ids = idfc

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

  natural-square= : Coh ({f g : A → B} (h : (a : A) → f a == g a)
          {x y : A} {p p' : x == y} (p= : p == p')
          → {fp : f x == f y} {fp= : ap f p == fp} {fp' : f x == f y} {fp=' : ap f p' == fp'}
          → {gp : g x == g y} {gp= : ap g p == gp} {gp' : g x == g y} {gp=' : ap g p' == gp'}
          → {fp=fp' : fp == fp'} (fp=fp'= : Square (ap (ap f) p=) fp= fp=' fp=fp')
          → {gp=gp' : gp == gp'} (gp=gp'= : Square (ap (ap g) p=) gp= gp=' gp=gp')
          → FlatCube (natural-square h p fp= gp=) (natural-square h p' fp=' gp=') idp fp=fp' gp=gp' idp)
  natural-square= = path-induction

  -- More or less a special case of the previous one
  natural-square== : Coh ({f g : A → B} (h : (a : A) → f a == g a)
          {x y : A} (p : x == y)
          → {fp : f x == f y} {fp= : ap f p == fp} {fp' : f x == f y} {fp=' : ap f p == fp'}
          → {gp : g x == g y} {gp= : ap g p == gp} {gp' : g x == g y} {gp=' : ap g p == gp'}
          → {fpp' : fp == fp'} (fpp'= : ! fp= ∙ fp=' == fpp')
          → {gpp' : gp == gp'} (gpp'= : ! gp= ∙ gp=' == gpp')
          → FlatCube (natural-square h p fp= gp=) (natural-square h p fp=' gp=') idp fpp' gpp' idp)
  natural-square== = path-induction

∘-ap-square : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B)
  {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} (sq : Square p q r s)
  → FlatCube (ap-square g (ap-square f sq)) (ap-square (g ∘ f) sq) (∘-ap g f p) (∘-ap g f q) (∘-ap g f r) (∘-ap g f s)
∘-ap-square g f ids = idfc

ap-square-∘ : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B)
  {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} (sq : Square p q r s)
  → FlatCube (ap-square (g ∘ f) sq) (ap-square g (ap-square f sq)) (ap-∘ g f p) (ap-∘ g f q) (ap-∘ g f r) (ap-∘ g f s)
ap-square-∘ g f ids = idfc

-- Similar to [ap-square-natural-square]
natural-square-ap : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : B → C) →
  Coh ({a b : A} (p : a == b) {u v : A → B} (g : (x : A) → u x == v x)
      {fup : _} {fup= : ap (f ∘ u) p == fup}
      {fvp : _} {fvp= : ap (f ∘ v) p == fvp}
      {up : _} {up= : ap u p == up}
      {vp : _} {vp= : ap v p == vp}
      {apfup : ap f up == fup} (apfup= : Square (∘-ap f u p) (ap (ap f) up=) fup= apfup)
      {apfvp : ap f vp == fvp} (apfvp= : Square (∘-ap f v p) (ap (ap f) vp=) fvp= apfvp)
    → natural-square (ap f ∘ g) p fup= fvp= == adapt-square (ap-square f (natural-square g p up= vp=)) apfup apfvp)
natural-square-ap f = path-induction

cube-rotate : ∀ {i} {A : Type i}
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  → Cube sq₀₋₋ sq₁₋₋ sq₋₋₀ (square-symmetry sq₋₀₋) (square-symmetry sq₋₁₋) sq₋₋₁
cube-rotate idc = idc

horiz-degen-path-hid-square : ∀ {i} → Coh ({A : Type i} {x y : A} {p : x == y} → idp == horiz-degen-path (horiz-degen-square (idp {a = p})))
horiz-degen-path-hid-square = path-induction

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

  ↓-ap-in-=' : {x y : A} {p : x == y} (k : (x : A) → g (f x) == h (f x))
               {gfp : g (f x) == g (f y)} {gfp= : ap g (ap f p) == gfp}
    → ↓-ap-in (λ z → g z == h z) f (apd k p) == ↓-='-from-square gfp= idp (natural-square k p (ap-∘ g f p ∙ gfp=) (ap-∘ h f p))
  ↓-ap-in-=' {p = idp} k {gfp= = idp} = & horiz-degen-path-hid-square

module _ {i j} {A : Type i} {a : A} where
 instance
  JCubehorizdegensquare : {B : (p : idp {a = a} == idp) → Cube ids (horiz-degen-square p) ids ids ids ids → Type j}
    → Coh (B idp idc) → Coh ({p : idp == idp} (cube : Cube ids (horiz-degen-square p) ids ids ids ids) → B p cube)
  & (JCubehorizdegensquare {B} d) cube = B= (! horiz-degen-square-η) (! horiz-degen-square-β) horiz-degen-square-◂ cube (& (JCube2 {B = B'} d) cube) where

    B' : (p : Square {a₀₀ = a} idp idp idp idp) → Cube ids p ids ids ids ids → Type j
    B' p c = B (horiz-degen-path p) (c ∙³x & x-degen-cube-in (! horiz-degen-square-β))

    horiz-degen-square-◂ : ∀ {i} {A : Type i} {a a' : A} {p q : a == a'} {r : p == q} → ap horiz-degen-square (! (horiz-degen-square-η {r = r})) == ! horiz-degen-square-β
    horiz-degen-square-◂ {p = idp} {r = idp} = idp

    B= : {p' p : idp == idp} (p= : p == p') (p=' : horiz-degen-square p == horiz-degen-square p') (p== : ap horiz-degen-square p= == p=')
         (c : Cube ids (horiz-degen-square p) ids ids ids ids)
         → B p' (c ∙³x & x-degen-cube-in p=') → B p c
    B= idp _ idp c = transport (B _) (& eq c)  where

      eq : Coh ({sq : Square (idp {a = a}) idp idp idp} (c : Cube ids sq ids ids ids ids) → c ∙³x & x-degen-cube-in idp == c)
      eq = path-induction

max_stars_repo_name: guillaumebrunerie/JamesConstruction

max_issues_repo_name: guillaumebrunerie/JamesConstruction

max_forks_repo_name: guillaumebrunerie/JamesConstruction


text:
module lib where

open import datatypes public
open import logic public
open import thms public
open import termination public
open import error public
open import io public

ext: agda

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --without-K --safe #-}
-- Take a relation that is already reflexive and transitive
-- and make it symmetric.
--   (Borrowed from Categories/Support/ZigZag from copumpkin's Categories library

module Relation.Binary.Construct.Symmetrize where

open import Level
open import Relation.Binary
open import Relation.Binary.Construct.On using () renaming (isEquivalence to on-preserves-equivalence)

data Direction : Set where
  ↘ ↗ : Direction

rotate : Direction → Direction
rotate ↘ = ↗
rotate ↗ = ↘

private
  variable
    c ℓ₁ ℓ₂ : Level
    Carrier : Set c

data ZigZag′ (_∼_ : Rel Carrier ℓ₂) : (x y : Carrier) (begin end : Direction) → Set (levelOfTerm x ⊔ ℓ₂) where
  zig : ∀ {x y z e} (first : x ∼ y) (rest : ZigZag′ _∼_ y z ↗ e) → ZigZag′ _∼_ x z ↘ e
  zag : ∀ {x y z e} (first : y ∼ x) (rest : ZigZag′ _∼_ y z ↘ e) → ZigZag′ _∼_ x z ↗ e
  slish : ∀ {x y} (last : x ∼ y) → ZigZag′ _∼_ x y ↘ ↘
  slash : ∀ {x y} (last : y ∼ x) → ZigZag′ _∼_ x y ↗ ↗

data Alternating′ (_∼_ : Carrier -> Carrier -> Set ℓ₂) (x y : Carrier) : Set (levelOfTerm x ⊔ ℓ₂) where
  disorient : ∀ {begin end} (zz : ZigZag′ _∼_ x y begin end) → Alternating′ _∼_ x y

module _ (Base : Preorder c ℓ₁ ℓ₂) where

  ZigZag : (x y : Preorder.Carrier Base) (begin end : Direction) → Set (c ⊔ ℓ₂)
  ZigZag = ZigZag′ (Preorder._∼_ Base)

  private
    sym′ : {x y z : Preorder.Carrier Base} {begin middle end : Direction} → ZigZag y z middle end →
           ZigZag y x middle begin → ZigZag z x (rotate end) begin
    sym′ (zig first rest) accum = sym′ rest (zag first accum)
    sym′ (zag first rest) accum = sym′ rest (zig first accum)
    sym′ (slish last) accum     = zag last accum
    sym′ (slash last) accum     = zig last accum

  sym : ∀ {x y begin end} → ZigZag x y begin end → ZigZag y x (rotate end) (rotate begin)
  sym (zig first rest) = sym′ rest (slash first)
  sym (zag first rest) = sym′ rest (slish first)
  sym (slish last)     = slash last
  sym (slash last)     = slish last

  trans : ∀ {x y z begin end begin′ end′} → ZigZag x y begin end → ZigZag y z begin′ end′ → ZigZag x z begin end′
  trans (zig first rest) yz = zig first (trans rest yz)
  trans (zag first rest) yz = zag first (trans rest yz)
  trans (slish last) (zig first rest) = zig (Preorder.trans Base last first) rest
  trans (slish last) (zag first rest) = zig last (zag first rest)
  trans (slish last) (slish only) = slish (Preorder.trans Base last only)
  trans (slish last) (slash only) = zig last (slash only)
  trans (slash last) (zig first rest) = zag last (zig first rest)
  trans (slash last) (zag first rest) = zag (Preorder.trans Base first last) rest
  trans (slash last) (slish only) = zag last (slish only)
  trans (slash last) (slash only) = slash (Preorder.trans Base only last)

  Alternating : (x y : Preorder.Carrier Base) → Set (c ⊔ ℓ₂)
  Alternating = Alternating′ (Preorder._∼_ Base)

  private
    is-equivalence : IsEquivalence Alternating
    is-equivalence = record
      { refl = disorient (slash (Preorder.refl Base))
      ; sym = λ where (disorient zz) → disorient (sym zz)
      ; trans = λ where (disorient ij) (disorient jk) → disorient (trans ij jk)
      }

  setoid : Setoid c (c ⊔ ℓ₂)
  setoid = record
    { Carrier = Preorder.Carrier Base
    ; _≈_ = Alternating
    ; isEquivalence = is-equivalence
    }

  -- the main eliminators for Alternating -- they prove that any equivalence that
  -- respects the base preorder also respects its Alternating completion.
  locally-minimal : ∀ {ℓ′} {_≈_ : Rel (Preorder.Carrier Base) ℓ′} (≈-isEquivalence : IsEquivalence _≈_) →
    (Preorder._∼_ Base ⇒ _≈_) → (Alternating ⇒ _≈_)
  locally-minimal {_} {_≋_} isEq inj (disorient zz) = impl zz
    where
    open IsEquivalence isEq renaming (sym to >sym; trans to _>trans>_)

    impl : {i j : Preorder.Carrier Base} {b e : Direction} → ZigZag i j b e → i ≋ j
    impl (zig first rest) = inj first >trans> impl rest
    impl (zag first rest) = >sym (inj first) >trans> impl rest
    impl (slish last) = inj last
    impl (slash last) = >sym (inj last)

  minimal : ∀ {c′ ℓ′} (Dest : Setoid c′ ℓ′) (f : Preorder.Carrier Base → Setoid.Carrier Dest) →
            (Preorder._∼_ Base =[ f ]⇒ Setoid._≈_ Dest) → (Alternating =[ f ]⇒ Setoid._≈_ Dest)
  minimal Dest f inj = locally-minimal (on-preserves-equivalence f (Setoid.isEquivalence Dest)) inj

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
open import Prelude

module Implicits.Resolution.Ambiguous.Resolution where

open import Data.Fin.Substitution
open import Data.List
open import Data.List.Any
open Membership-≡

open import Implicits.Syntax
open import Implicits.Substitutions

data _⊢ᵣ_ {ν} (Δ : ICtx ν) : Type ν → Set where
  r-tabs : ∀ {r} → ictx-weaken Δ ⊢ᵣ r → Δ ⊢ᵣ ∀' r
  r-tapp : ∀ {r} a → Δ ⊢ᵣ ∀' r → Δ ⊢ᵣ (r tp[/tp a ])
  r-ivar : ∀ {r} → r ∈ Δ → Δ ⊢ᵣ r
  r-iabs : ∀ {a b} → (a ∷ Δ) ⊢ᵣ b → Δ ⊢ᵣ (a ⇒ b)
  r-iapp : ∀ {a b} → Δ ⊢ᵣ (a ⇒ b) → Δ ⊢ᵣ a → Δ ⊢ᵣ b


text:
-- Andreas, 2015-07-20, record patterns

open import Common.Prelude

postulate A : Set

record R : Set where
  field f : A

T : Bool → Set
T true  = R
T false = A

test : ∀{b} → T b → A
test record{f = a} = a

-- Could succeed by some magic.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module AnnotatedTypes where

{-

-- ATypes are stratified such that that dynamically bound
-- functions can only have dynamically bound parameters.

-- TODO: why exactly is that necessary?

-- Think about the example of the evaluation of a dynamic function with
-- static components

-- The following well-formedness relation as an alternative representation
-- for this constraint:
module AType-WF where
  open import Relation.Binary.PropositionalEquality
  -- Static and dynamic binding times
  data BT : Set where
    stat : BT
    dyn : BT

  -- Ordering on binding times: dynamic binding time subsumes static
  -- binding time.
  data _≤-bt_ : BT → BT → Set where
    bt≤bt : ∀ bt → bt ≤-bt bt
    stat≤bt : ∀ bt → stat ≤-bt bt

  module WF (ATy : Set) (typeof : ATy → Type) (btof : ATy → BT) where
    data wf : ATy → Set where
      wf-int : ∀ α → typeof α ≡ Int → wf α
      wf-fun : ∀ α α₁ α₂ →
               typeof α ≡ Fun (typeof α₁) (typeof α₂) →
               --btof α ≤-bt btof α₁ →
               --btof α ≤-bt btof α₂ →
               wf α₁ → wf α₂ →
               wf α
      -- Note that in [wf-fun],we can omit the checking of the label of
      -- the arguments against that of the function and [_≤-bt_] is
      -- unnecessary
      wf-pair : ∀ α α₁ α₂ →
               typeof α ≡ typeof α₁ • typeof α₂ →
               wf α₁ → wf α₂ →
               wf α
      wf-sum  : ∀ α α₁ α₂ →
               typeof α ≡ typeof α₁ ⊎ typeof α₂ →
               wf α₁ → wf α₂ →
               wf α

  -- It is easy to check that the stratification respects the
  -- well-formedness, given the intended mapping from ATypes to
  -- binding times expained above:
  btof : AType → BT
  btof AInt = stat
  btof (AFun aty aty₁) = stat
  btof (D x) = dyn
  btof (aty • aty₁) = stat
  btof (aty ⊎ aty₁) = stat

  ---------------------
  -- Alternative [btof]
  ---------------------
  btof' : AType → BT
  btof' AInt = stat
  btof' (AFun aty aty₁) = stat
  btof' (D x) = dyn
  btof' (aty • aty₁) = dyn
  btof' (aty ⊎ aty₁) = dyn

  open WF AType typeof btof using (wf-fun; wf-int) renaming (wf to wf-AType)
  lem-wf-AType : ∀ α → wf-AType α
  lem-wf-AType AInt = WF.wf-int AInt refl
  lem-wf-AType (AFun α₁ α₂) = WF.wf-fun (AFun α₁ α₂) α₁ α₂ refl (lem-wf-AType α₁)
                                (lem-wf-AType α₂)
  lem-wf-AType (D Int) = WF.wf-int (D Int) refl
  lem-wf-AType (D (Fun x x₁)) = WF.wf-fun (D (Fun x x₁)) (D x) (D x₁) refl (lem-wf-AType (D x))
                                  (lem-wf-AType (D x₁))
  lem-wf-AType (D (x • x₁)) = WF.wf-pair (D (x • x₁)) (D x) (D x₁) refl (lem-wf-AType (D x))
                                (lem-wf-AType (D x₁))
  lem-wf-AType (D (x ⊎ x₁)) = WF.wf-sum (D (x ⊎ x₁)) (D x) (D x₁) refl (lem-wf-AType (D x))
                                (lem-wf-AType (D x₁))
  lem-wf-AType (α₁ • α₂) = WF.wf-pair (α₁ • α₂) α₁ α₂ refl (lem-wf-AType α₁) (lem-wf-AType α₂)
  lem-wf-AType (α₁ ⊎ α₂) = WF.wf-sum (α₁ ⊎ α₂) α₁ α₂ refl (lem-wf-AType α₁) (lem-wf-AType α₂)
  --lem-wf-AType AInt = WF.wf-int AInt refl
  --lem-wf-AType (AFun α α₁) = WF.wf-fun (AFun α α₁) α α₁ refl (stat≤bt (btof α))
  --                           (stat≤bt (btof α₁))
  --                          (lem-wf-AType α)
  --                           (lem-wf-AType α₁)
  --lem-wf-AType (D Int) = WF.wf-int (D Int) refl
  --lem-wf-AType (D (Fun x x₁)) = WF.wf-fun (D (Fun x x₁))
  --                                        (D x) (D x₁)
  --                                        refl (bt≤bt dyn) (bt≤bt dyn)
  --                                        (lem-wf-AType (D x))
  --                                        (lem-wf-AType (D x₁))

  -----------------------------------------
  -- Note that [lem-wf-AType] is based upon
  -- a modified [wf]
  -----------------------------------------

-}

max_stars_repo_name: luminousfennell/polybta

max_issues_repo_name: luminousfennell/polybta

max_forks_repo_name: luminousfennell/polybta


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category
open import Categories.Functor hiding (id)

-- Cocone over a Functor F (from shape category J into category C)

module Categories.Diagram.Cocone
  {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where

open Category C
open Functor F

open import Level

record Coapex (N : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′) where
  field
    ψ       : (X : Category.Obj J) → F₀ X ⇒ N
    commute : ∀ {X Y} (f : J [ X , Y ]) → ψ Y ∘ F₁ f ≈ ψ X

record Cocone : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′) where
  field
    {N}    : Obj
    coapex : Coapex N

  open Coapex coapex public

open Coapex
open Cocone

record Cocone⇒ (c c′ : Cocone) : Set (ℓ ⊔ e ⊔ o′) where
  field
    arr     : N c ⇒ N c′
    commute : ∀ {X} → arr ∘ ψ c X ≈ ψ c′ X

open Cocone⇒

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module CompilingCoinduction where

open import Common.Coinduction
open import Common.Char
open import Common.String

data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () () #-}

postulate
  IO : Set → Set

{-# COMPILED_TYPE IO IO #-}
{-# BUILTIN IO IO #-}

{-# IMPORT Data.Text.IO #-}

postulate
  putStrLn : ∞ String → IO Unit

{-# COMPILED putStrLn Data.Text.IO.putStrLn #-}
{-# COMPILED_UHC putStrLn (UHC.Agda.Builtins.primPutStrLn) #-}
{-# COMPILED_JS putStrLn function(x) { return function(cb) { process.stdout.write(x(0) + "\n"); cb(0); }; } #-}

main = putStrLn (♯ "a")

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Core lemmas for division and modulus operations
------------------------------------------------------------------------

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

module Data.Nat.DivMod.Core where

open import Agda.Builtin.Nat using ()
  renaming (div-helper to divₕ; mod-helper to modₕ)

open import Data.Nat.Base
open import Data.Nat.Properties
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (contradiction)

open ≤-Reasoning

-------------------------------------------------------------------------
-- Helper lemmas that have no interpretation for _%_, only for modₕ

private

  mod-cong₃ : ∀ {c n a₁ a₂ b} → a₁ ≡ a₂ → modₕ c n a₁ b ≡ modₕ c n a₂ b
  mod-cong₃ refl = refl

  modₕ-skipTo0 : ∀ acc n a b → modₕ acc n (b + a) a ≡ modₕ (a + acc) n b 0
  modₕ-skipTo0 acc n zero    b = cong (λ v → modₕ acc n v 0) (+-identityʳ b)
  modₕ-skipTo0 acc n (suc a) b = begin-equality
    modₕ acc n (b + suc a) (suc a) ≡⟨ mod-cong₃ (+-suc b a) ⟩
    modₕ acc n (suc b + a) (suc a) ≡⟨⟩
    modₕ (suc acc) n (b + a) a     ≡⟨ modₕ-skipTo0 (suc acc) n a b ⟩
    modₕ (a + suc acc) n b 0       ≡⟨ cong (λ v → modₕ v n b 0) (+-suc a acc) ⟩
    modₕ (suc a + acc) n b 0       ∎

-------------------------------------------------------------------------
-- Lemmas for modₕ that also have an interpretation for _%_

a[modₕ]1≡0 : ∀ a → modₕ 0 0 a 0 ≡ 0
a[modₕ]1≡0 zero    = refl
a[modₕ]1≡0 (suc a) = a[modₕ]1≡0 a

n[modₕ]n≡0 : ∀ acc v → modₕ acc (acc + v) (suc v) v ≡ 0
n[modₕ]n≡0 acc v = modₕ-skipTo0 acc (acc + v) v 1

a[modₕ]n<n : ∀ acc d n → modₕ acc (acc + n) d n ≤ acc + n
a[modₕ]n<n acc zero    n       = m≤m+n acc n
a[modₕ]n<n acc (suc d) zero    = a[modₕ]n<n zero d (acc + 0)
a[modₕ]n<n acc (suc d) (suc n) rewrite +-suc acc n = a[modₕ]n<n (suc acc) d n

a[modₕ]n≤a : ∀ acc a n → modₕ acc (acc + n) a n ≤ acc + a
a[modₕ]n≤a acc zero    n       = ≤-reflexive (sym (+-identityʳ acc))
a[modₕ]n≤a acc (suc a) (suc n) = begin
  modₕ acc (acc + suc n) (suc a) (suc n) ≡⟨ cong (λ v → modₕ acc v (suc a) (suc n)) (+-suc acc n) ⟩
  modₕ acc (suc acc + n) (suc a) (suc n) ≤⟨ a[modₕ]n≤a (suc acc) a n ⟩
  suc acc + a                            ≡⟨ sym (+-suc acc a) ⟩
  acc + suc a                            ∎
a[modₕ]n≤a acc (suc a) zero    = begin
  modₕ acc (acc + 0) (suc a) 0 ≡⟨ cong (λ v → modₕ acc v (suc a) 0) (+-identityʳ acc) ⟩
  modₕ acc acc (suc a) 0       ≤⟨ a[modₕ]n≤a 0 a acc ⟩
  a                            ≤⟨ n≤1+n a ⟩
  suc a                        ≤⟨ m≤n+m (suc a) acc ⟩
  acc + suc a                  ∎

a≤n⇒a[modₕ]n≡a : ∀ acc n a b → modₕ acc n a (a + b) ≡ acc + a
a≤n⇒a[modₕ]n≡a acc n zero    b = sym (+-identityʳ acc)
a≤n⇒a[modₕ]n≡a acc n (suc a) b = begin-equality
  modₕ (suc acc) n a (a + b) ≡⟨ a≤n⇒a[modₕ]n≡a (suc acc) n a b ⟩
  suc acc + a                ≡⟨ sym (+-suc acc a) ⟩
  acc + suc a                ∎

modₕ-idem : ∀ acc a n → modₕ 0 (acc + n) (modₕ acc (acc + n) a n) (acc + n) ≡ modₕ acc (acc + n) a n
modₕ-idem acc zero    n       = a≤n⇒a[modₕ]n≡a 0 (acc + n) acc n
modₕ-idem acc (suc a) zero    rewrite +-identityʳ acc = modₕ-idem 0 a acc
modₕ-idem acc (suc a) (suc n) rewrite +-suc acc n = modₕ-idem (suc acc) a n

a+1[modₕ]n≡0⇒a[modₕ]n≡n-1 : ∀ acc l n → modₕ acc (acc + l) (suc n) l ≡ 0 → modₕ acc (acc + l) n l ≡ acc + l
a+1[modₕ]n≡0⇒a[modₕ]n≡n-1 acc zero    zero    eq rewrite +-identityʳ acc = refl
a+1[modₕ]n≡0⇒a[modₕ]n≡n-1 acc zero    (suc n) eq rewrite +-identityʳ acc = a+1[modₕ]n≡0⇒a[modₕ]n≡n-1 0 acc n eq
a+1[modₕ]n≡0⇒a[modₕ]n≡n-1 acc (suc l) (suc n) eq rewrite +-suc acc l     = a+1[modₕ]n≡0⇒a[modₕ]n≡n-1 (suc acc) l n eq

k<1+a[modₕ]n⇒k≤a[modₕ]n  : ∀ acc k n l → suc k ≤ modₕ acc (acc + l) (suc n) l → k ≤ modₕ acc (acc + l) n l
k<1+a[modₕ]n⇒k≤a[modₕ]n acc k zero    (suc l) (s≤s leq) = leq
k<1+a[modₕ]n⇒k≤a[modₕ]n acc k (suc n) zero    leq rewrite +-identityʳ acc = k<1+a[modₕ]n⇒k≤a[modₕ]n 0 k n acc leq
k<1+a[modₕ]n⇒k≤a[modₕ]n acc k (suc n) (suc l) leq rewrite +-suc acc l     = k<1+a[modₕ]n⇒k≤a[modₕ]n (suc acc) k n l leq

1+a[modₕ]n≤1+k⇒a[modₕ]n≤k : ∀ acc k n l → 0 < modₕ acc (acc + l) (suc n) l →
                            modₕ acc (acc + l) (suc n) l ≤ suc k → modₕ acc (acc + l) n l ≤ k
1+a[modₕ]n≤1+k⇒a[modₕ]n≤k acc k zero    (suc l) 0<mod (s≤s leq) = leq
1+a[modₕ]n≤1+k⇒a[modₕ]n≤k acc k (suc n) zero    0<mod leq rewrite +-identityʳ acc = 1+a[modₕ]n≤1+k⇒a[modₕ]n≤k 0 k n acc 0<mod leq
1+a[modₕ]n≤1+k⇒a[modₕ]n≤k acc k (suc n) (suc l) 0<mod leq rewrite +-suc acc l = 1+a[modₕ]n≤1+k⇒a[modₕ]n≤k (suc acc) k n l 0<mod leq

a+n[modₕ]n≡a[modₕ]n : ∀ acc a n → modₕ acc (acc + n) (acc + a + suc n) n ≡ modₕ acc (acc + n) a n
a+n[modₕ]n≡a[modₕ]n acc zero n rewrite +-identityʳ acc = begin-equality
  modₕ acc (acc + n) (acc + suc n) n   ≡⟨ mod-cong₃ (+-suc acc n) ⟩
  modₕ acc (acc + n) (suc acc + n) n   ≡⟨ modₕ-skipTo0 acc (acc + n) n (suc acc) ⟩
  modₕ (acc + n) (acc + n) (suc acc) 0 ≡⟨⟩
  modₕ 0 (acc + n) acc (acc + n)       ≡⟨ a≤n⇒a[modₕ]n≡a 0 (acc + n) acc n ⟩
  acc                                  ∎
a+n[modₕ]n≡a[modₕ]n acc (suc a) zero rewrite +-identityʳ acc = begin-equality
  modₕ acc acc (acc + suc a + 1)   0   ≡⟨ mod-cong₃ (+-comm (acc + suc a) 1) ⟩
  modₕ acc acc (1 + (acc + suc a)) 0   ≡⟨⟩
  modₕ 0   acc (acc + suc a)       acc ≡⟨ mod-cong₃ (+-comm acc (suc a)) ⟩
  modₕ 0   acc (suc a + acc)       acc ≡⟨ mod-cong₃ (sym (+-suc a acc)) ⟩
  modₕ 0   acc (a + suc acc)       acc ≡⟨ a+n[modₕ]n≡a[modₕ]n 0 a acc ⟩
  modₕ 0   acc a                   acc ∎
a+n[modₕ]n≡a[modₕ]n acc (suc a) (suc n) rewrite +-suc acc n = begin-equality
  mod₁ (acc + suc a + (2 + n)) (suc n) ≡⟨ cong (λ v → mod₁ (v + suc (suc n)) (suc n)) (+-suc acc a) ⟩
  mod₁ (suc acc + a + (2 + n)) (suc n) ≡⟨⟩
  mod₂ (acc + a + (2 + n))     n       ≡⟨ mod-cong₃ (sym (+-assoc (acc + a) 1 (suc n))) ⟩
  mod₂ (acc + a + 1 + suc n)   n       ≡⟨ mod-cong₃ (cong (_+ suc n) (+-comm (acc + a) 1)) ⟩
  mod₂ (suc acc + a + suc n)   n       ≡⟨ a+n[modₕ]n≡a[modₕ]n (suc acc) a n ⟩
  mod₂ a                       n       ∎
  where
  mod₁ = modₕ acc       (suc acc + n)
  mod₂ = modₕ (suc acc) (suc acc + n)

-------------------------------------------------------------------------
-- Helper lemmas that have no interpretation for `_/_`, only for `divₕ`

private

  div-cong₃ : ∀ {c n a₁ a₂ b} → a₁ ≡ a₂ → divₕ c n a₁ b ≡ divₕ c n a₂ b
  div-cong₃ refl = refl

  divₕ-restart : ∀ {acc} d n j → j < n → divₕ acc d n j ≡ divₕ (suc acc) d (n ∸ suc j) d
  divₕ-restart d (suc n) zero    j<n       = refl
  divₕ-restart d (suc n) (suc j) (s≤s j<n) = divₕ-restart d n j j<n

  divₕ-finish : ∀ {acc} d n j → j ≥ n → divₕ acc d n j ≡ acc
  divₕ-finish d zero    j       j≥n       = refl
  divₕ-finish d (suc n) (suc j) (s≤s j≥n) = divₕ-finish d n j j≥n

  acc≤divₕ[acc] : ∀ {acc} d n j → acc ≤ divₕ acc d n j
  acc≤divₕ[acc] {acc} d zero    j       = ≤-refl
  acc≤divₕ[acc] {acc} d (suc n) zero    = ≤-trans (n≤1+n acc) (acc≤divₕ[acc] d n d)
  acc≤divₕ[acc] {acc} d (suc n) (suc j) = acc≤divₕ[acc] d n j

  divₕ-extractAcc : ∀ acc d n j → divₕ acc d n j ≡ acc + divₕ 0 d n j
  divₕ-extractAcc acc d zero j          = sym (+-identityʳ acc)
  divₕ-extractAcc acc d (suc n) (suc j) = divₕ-extractAcc acc d n j
  divₕ-extractAcc acc d (suc n) zero = begin-equality
    divₕ (suc acc)    d n d  ≡⟨ divₕ-extractAcc (suc acc) d n d ⟩
    suc acc +  divₕ 0 d n d  ≡⟨ sym (+-suc acc _) ⟩
    acc + suc (divₕ 0 d n d) ≡⟨ cong (acc +_) (sym (divₕ-extractAcc 1 d n d)) ⟩
    acc +      divₕ 1 d n d  ∎

  pattern inj₂′ x = inj₂ (inj₁ x)
  pattern inj₃  x = inj₂ (inj₂ x)

  -- This hideous lemma details the conditions needed for two divisions to
  -- be equal when the two offsets (i.e. the 4ᵗʰ parameters) are different.
  -- It may be that this triple sum has an elegant simplification to a
  -- set of inequalities involving the modulus but I can't find it.
  divₕ-offsetEq : ∀ {acc₁ acc₂} d n j k → j ≤ d → k ≤ d →
                  (acc₁ ≡ acc₂     × j ≤ k × k < modₕ 0 d n d) ⊎
                  (acc₁ ≡ acc₂     × modₕ 0 d n d ≤ j × j ≤ k) ⊎
                  (acc₁ ≡ suc acc₂ × k < modₕ 0 d n d × modₕ 0 d n d ≤ j) →
                  divₕ acc₁ d n j ≡ divₕ acc₂ d n k
  divₕ-offsetEq d zero    j       k       j≤d k≤d (inj₁  (refl , _)) = refl
  divₕ-offsetEq d zero    j       k       j≤d k≤d (inj₂′ (refl , _)) = refl
  divₕ-offsetEq d zero    j       k       j≤d k≤d (inj₃ (eq , () , _))
  -- (0 , 0) cases
  divₕ-offsetEq d (suc n) zero    zero    j≤d k≤d (inj₁ (refl , _)) =
    divₕ-offsetEq d n d d ≤-refl ≤-refl (inj₂′ (refl , a[modₕ]n<n 0 n d , ≤-refl))
  divₕ-offsetEq d (suc n) zero    zero    j≤d k≤d (inj₂′ (refl , _)) =
    divₕ-offsetEq d n d d ≤-refl ≤-refl (inj₂′ (refl , a[modₕ]n<n 0 n d , ≤-refl))
  divₕ-offsetEq d (suc n) zero    zero    j≤d k≤d (inj₃ (_ , 0<mod , mod≤0)) =
    contradiction (<-transˡ 0<mod mod≤0) λ()
  -- (0 , suc) cases
  divₕ-offsetEq d (suc n) zero (suc k)    j≤d k≤d (inj₁  (refl , _ , 1+k<mod)) =
    divₕ-offsetEq d n d k ≤-refl (<⇒≤ k≤d) (inj₃ (refl , k<1+a[modₕ]n⇒k≤a[modₕ]n 0 (suc k) n d 1+k<mod , a[modₕ]n<n 0 n d))
  divₕ-offsetEq d (suc n) zero (suc k)    j≤d k≤d (inj₂′ (refl , mod≤0 , _)) =
    divₕ-offsetEq d n d k ≤-refl (<⇒≤ k≤d) (inj₃ (refl , subst (k <_) (sym (a+1[modₕ]n≡0⇒a[modₕ]n≡n-1 0 d n (n≤0⇒n≡0 mod≤0))) k≤d , a[modₕ]n<n 0 n d))
  divₕ-offsetEq d (suc n) zero (suc k)    j≤d k≤d (inj₃  (_ , 1+k<mod , mod≤0)) =
    contradiction (<-transˡ 1+k<mod mod≤0) λ()
  -- (suc , 0) cases
  divₕ-offsetEq d (suc n) (suc j) zero j≤d k≤d (inj₁  (_ , () , _))
  divₕ-offsetEq d (suc n) (suc j) zero j≤d k≤d (inj₂′ (_ , _ , ()))
  divₕ-offsetEq d (suc n) (suc j) zero j≤d k≤d (inj₃  (eq , 0<mod , mod≤1+j)) =
    divₕ-offsetEq d n j d (<⇒≤ j≤d) ≤-refl (inj₂′ (eq , 1+a[modₕ]n≤1+k⇒a[modₕ]n≤k 0 j n d 0<mod mod≤1+j , <⇒≤ j≤d))
  -- (suc , suc) cases
  divₕ-offsetEq d (suc n) (suc j) (suc k) j≤d k≤d (inj₁ (eq , s≤s j≤k , 1+k<mod)) =
    divₕ-offsetEq d n j k (<⇒≤ j≤d) (<⇒≤ k≤d) (inj₁ (eq , j≤k , k<1+a[modₕ]n⇒k≤a[modₕ]n 0 (suc k) n d 1+k<mod))
  divₕ-offsetEq d (suc n) (suc j) (suc k) j≤d k≤d (inj₂′ (eq , mod≤1+j , (s≤s j≤k))) with modₕ 0 d (suc n) d ≟ 0
  ... | yes mod≡0 = divₕ-offsetEq d n j k (<⇒≤ j≤d) (<⇒≤ k≤d) (inj₁ (eq , j≤k , subst (k <_) (sym (a+1[modₕ]n≡0⇒a[modₕ]n≡n-1 0 d n mod≡0)) k≤d))
  ... | no  mod≢0 = divₕ-offsetEq d n j k (<⇒≤ j≤d) (<⇒≤ k≤d) (inj₂′ (eq , 1+a[modₕ]n≤1+k⇒a[modₕ]n≤k 0 j n d (n≢0⇒n>0 mod≢0) mod≤1+j , j≤k))
  divₕ-offsetEq d (suc n) (suc j) (suc k) j≤d k≤d (inj₃  (eq , k<mod , mod≤1+j)) =
    divₕ-offsetEq d n j k (<⇒≤ j≤d) (<⇒≤ k≤d) (inj₃ (eq , k<1+a[modₕ]n⇒k≤a[modₕ]n 0 (suc k) n d k<mod , 1+a[modₕ]n≤1+k⇒a[modₕ]n≤k 0 j n d (<-transʳ z≤n k<mod) mod≤1+j))

-------------------------------------------------------------------------
-- Lemmas for divₕ that also have an interpretation for _/_

-- The quotient and remainder are related to the dividend and
-- divisor in the right way.

div-mod-lemma : ∀ accᵐ accᵈ d n →
    accᵐ + accᵈ * suc (accᵐ + n) + d ≡
    modₕ accᵐ (accᵐ + n) d n + divₕ accᵈ (accᵐ + n) d n * suc (accᵐ + n)
div-mod-lemma accᵐ accᵈ zero    n    = +-identityʳ _
div-mod-lemma accᵐ accᵈ (suc d) zero rewrite +-identityʳ accᵐ = begin-equality
  accᵐ + accᵈ * suc accᵐ + suc d          ≡⟨ +-suc _ d ⟩
  suc accᵈ * suc accᵐ + d                 ≡⟨ div-mod-lemma zero (suc accᵈ) d accᵐ ⟩
  modₕ 0          accᵐ d accᵐ +
  divₕ (suc accᵈ) accᵐ d accᵐ * suc accᵐ  ≡⟨⟩
  modₕ accᵐ accᵐ (suc d) 0 +
  divₕ accᵈ accᵐ (suc d) 0 * suc accᵐ     ∎
div-mod-lemma accᵐ accᵈ (suc d) (suc n) rewrite +-suc accᵐ n = begin-equality
  accᵐ + accᵈ * m + suc d             ≡⟨ +-suc _ d ⟩
  suc (accᵐ + accᵈ * m + d)           ≡⟨ div-mod-lemma (suc accᵐ) accᵈ d n ⟩
  modₕ _ _ d n + divₕ accᵈ _ d n * m  ∎
  where
  m = 2 + accᵐ + n

n[divₕ]n≡1 : ∀ n m → divₕ 0 n (suc m) m ≡ 1
n[divₕ]n≡1 n zero    = refl
n[divₕ]n≡1 n (suc m) = n[divₕ]n≡1 n m

a[divₕ]1≡a : ∀ acc a → divₕ acc 0 a 0 ≡ acc + a
a[divₕ]1≡a acc zero    = sym (+-identityʳ acc)
a[divₕ]1≡a acc (suc a) = trans (a[divₕ]1≡a (suc acc) a) (sym (+-suc acc a))

a*n[divₕ]n≡a : ∀ acc a n → divₕ acc n (a * suc n) n ≡ acc + a
a*n[divₕ]n≡a acc zero    n = sym (+-identityʳ acc)
a*n[divₕ]n≡a acc (suc a) n = begin-equality
  divₕ acc       n (suc a * suc n)             n ≡⟨ divₕ-restart n (suc a * suc n) n (m≤m+n (suc n) _) ⟩
  divₕ (suc acc) n (suc a * suc n ∸ suc n)     n ≡⟨⟩
  divₕ (suc acc) n (suc n + a * suc n ∸ suc n) n ≡⟨ div-cong₃ (m+n∸m≡n (suc n) (a * suc n)) ⟩
  divₕ (suc acc) n (a * suc n)                 n ≡⟨ a*n[divₕ]n≡a (suc acc) a n ⟩
  suc acc + a                                    ≡⟨ sym (+-suc acc a) ⟩
  acc + suc a                                    ∎

+-distrib-divₕ : ∀ acc k m n j → modₕ k (k + j) m j + modₕ 0 (k + j) n (k + j) < suc (k + j) →
                 divₕ acc (k + j) (m + n) j ≡ divₕ acc (k + j) m j + divₕ 0 (k + j) n (k + j)
+-distrib-divₕ acc k (suc m) n zero leq rewrite +-identityʳ k = +-distrib-divₕ (suc acc) 0 m n k leq
+-distrib-divₕ acc k (suc m) n (suc j) leq rewrite +-suc k j = +-distrib-divₕ acc (suc k) m n j leq
+-distrib-divₕ acc k zero n j leq = begin-equality
  divₕ acc (k + j) n j           ≡⟨ divₕ-extractAcc acc (k + j) n j ⟩
  acc + divₕ 0 (k + j) n j       ≡⟨ cong (acc +_) (divₕ-offsetEq _ n j _ (m≤n+m j k) ≤-refl case) ⟩
  acc + divₕ 0 (k + j) n (k + j) ∎
  where
  case = inj₂′ (refl , +-cancelˡ-≤ (suc k) leq , m≤n+m j k)

divₕ-mono-≤ : ∀ {acc} k {m n o p} → m ≤ n → p ≤ o → divₕ acc (k + o) m o ≤ divₕ acc (k + p) n p
divₕ-mono-≤ {acc} k {0} {n} {_} {p} z≤n p≤o = acc≤divₕ[acc] (k + p) n p
divₕ-mono-≤ {acc} k {_} {_} {suc o} {suc p} (s≤s m≤n) (s≤s p≤o)
  rewrite +-suc k o | +-suc k p = divₕ-mono-≤ (suc k) m≤n p≤o
divₕ-mono-≤ {acc} k {suc m} {suc n} {o} {0}      (s≤s m≤n) z≤n with o <? suc m
... | no  o≮1+m rewrite +-identityʳ k = begin
  divₕ acc (k + o) (suc m) o ≡⟨ divₕ-finish (k + o) (suc m) o (≮⇒≥ o≮1+m) ⟩
  acc                        ≤⟨ n≤1+n acc ⟩
  suc acc                    ≤⟨ acc≤divₕ[acc] k n k ⟩
  divₕ (suc acc) k n k       ∎
... | yes o<1+m rewrite +-identityʳ k = begin
  divₕ acc       (k + o) (suc m) o       ≡⟨ divₕ-restart (k + o) (suc m) o o<1+m ⟩
  divₕ (suc acc) (k + o) (m ∸ o) (k + o) ≤⟨ divₕ-mono-≤ 0 (≤-trans (m∸n≤m m o) m≤n) (m≤m+n k o) ⟩
  divₕ (suc acc) k       n       k       ∎


text:
module HostRequirements where

open import Agda.Builtin.Unit
open import Data.String as String using (String)
open import Category.Applicative
open import Category.Monad
open import Category.Monad.State

data Path : Set where
  MkPath : String -> Path

data Value : Set where
  MkValue : String -> Value

data Identifier : Set where
  MkIdentifier : String -> Identifier

separator : String
separator = "/"

data Env : Set where
  MkEnv : Env

{-
get : Path -> State Env Value
get path = return (MkValue "")

set : Path -> Value -> State Env ⊤
set path value = return ⊤

delete : Path -> State Env ⊤
delete path = return ⊤

getConsensusState : State Env ConsensusState
getConsensusState = ?

getCallingModule : State Env Identifier
getCallingModule = return (MkIdentifier "")
-}

max_stars_repo_name: dogemos/ics

max_issues_repo_name: dogemos/ics

max_forks_repo_name: dogemos/ics


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.DirectProd where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.DirectProd
open import Cubical.Algebra.CommRing.Base

private
  variable
    ℓ ℓ' : Level

module _
  (A'@(A , Ar) : CommRing ℓ)
  (B'@(B , Br) : CommRing ℓ')
  where

  AB = DirectProd-Ring (CommRing→Ring A') (CommRing→Ring B')

  open RingStr (snd AB) using ()
    renaming
    ( 0r        to 0AB
    ; 1r        to 1AB
    ; _+_       to _+AB_
    ; -_        to -AB_
    ; _·_       to _·AB_
    ; +Assoc    to +ABAssoc
    ; +IdL      to +ABIdL
    ; +IdR      to +ABIdR
    ; +InvL     to +ABInvL
    ; +InvR     to +ABInvR
    ; +Comm     to +ABComm
    ; ·Assoc    to ·ABAssoc
    ; ·IdR      to ·ABIdR
    ; ·IdL      to ·ABIdL
    ; ·DistR+   to ·ABDistR+
    ; ·DistL+   to ·ABDistL+
    ; is-set    to isSetAB     )

  DirectProd-CommRing : CommRing (ℓ-max ℓ ℓ')
  fst DirectProd-CommRing = A × B
  CommRingStr.0r (snd DirectProd-CommRing) = 0AB
  CommRingStr.1r (snd DirectProd-CommRing) = 1AB
  CommRingStr._+_ (snd DirectProd-CommRing) = _+AB_
  CommRingStr._·_ (snd DirectProd-CommRing) = _·AB_
  CommRingStr.- snd DirectProd-CommRing = -AB_
  CommRingStr.isCommRing (snd DirectProd-CommRing) =
    makeIsCommRing
    isSetAB
    +ABAssoc
    +ABIdR
    +ABInvR
    +ABComm
    ·ABAssoc
    ·ABIdR
    ·ABDistR+
    λ x y i → (CommRingStr.·Comm Ar (fst x) (fst y) i) , (CommRingStr.·Comm Br (snd x) (snd y) i)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Operators for combining and building families
module SOAS.Families.Build {T : Set} where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Sorting {T}
open import SOAS.Families.Core {T}

-- | Metavariable contexts

-- Inductive construction of context- and type-indexed sets
data MCtx : Set where
  ⁅⁆      : MCtx
  ⁅_⊩ₙ_⁆_ : (Π : Ctx {T}) → (τ : T) → MCtx → MCtx
infixr 7 ⁅_⊩ₙ_⁆_

-- Pattern synonym for parameterless elements and final elements
infixr 10 ⁅_⁆̣ ⁅_⊩ₙ_⁆̣
infixr 7 ⁅_⁆_ ⁅_⊩_⁆_ ⁅_·_⊩_⁆_ ⁅_⊩_⁆̣ ⁅_·_⊩_⁆̣ _⁅_⊩ₙ_⁆
pattern ⁅_⁆̣ α = ⁅ ∅ ⊩ₙ α ⁆ ⁅⁆
pattern ⁅_⊩ₙ_⁆̣ Π α = ⁅ Π ⊩ₙ α ⁆ ⁅⁆
pattern ⁅_⁆_ τ 𝔐 = ⁅ ∅ ⊩ₙ τ ⁆ 𝔐
pattern ⁅_⊩_⁆_ τ α 𝔐 = ⁅ ⌊ τ ⌋ ⊩ₙ α ⁆ 𝔐
pattern ⁅_·_⊩_⁆_ τ₁ τ₂ α 𝔐 = ⁅ ⌊ τ₁ ∙ τ₂ ⌋ ⊩ₙ α ⁆ 𝔐
pattern ⁅_⊩_⁆̣ τ α = ⁅ ⌊ τ ⌋ ⊩ₙ α ⁆ ⁅⁆
pattern ⁅_·_⊩_⁆̣ τ₁ τ₂ α = ⁅ ⌊ τ₁ ∙ τ₂ ⌋ ⊩ₙ α ⁆ ⁅⁆

-- Add type-context pair to the end of the metavariable context
_⁅_⊩ₙ_⁆ : MCtx → Ctx {T} → T → MCtx
⁅⁆              ⁅ Γ ⊩ₙ α ⁆ = ⁅ Γ ⊩ₙ α ⁆̣
(⁅ Π ⊩ₙ τ ⁆ 𝔐) ⁅ Γ ⊩ₙ α ⁆ = ⁅ Π ⊩ₙ τ ⁆ (𝔐 ⁅ Γ ⊩ₙ α ⁆)

private
  variable
    Γ Δ Θ Π : Ctx
    α β γ τ : T
    𝔐 : MCtx

-- Membership of metavariable contexts
data _⊩_∈_ : Ctx → T → MCtx → Set where
  ↓ : Π ⊩ τ ∈ (⁅ Π ⊩ₙ τ ⁆ 𝔐)
  ↑_ : Π ⊩ τ ∈ 𝔐 → Π ⊩ τ ∈ (⁅ Γ ⊩ₙ α ⁆ 𝔐)

infixr 220 ↑_

-- Metavariable context can be interpreted as a family via the membership
∥_∥ : MCtx → Familyₛ
∥ 𝔐 ∥ α Γ = Γ ⊩ α ∈ 𝔐
infixr 60 ∥_∥

_▷_ : MCtx → (Familyₛ → Familyₛ) → Familyₛ
𝔐 ▷ 𝒳 = 𝒳 ∥ 𝔐 ∥
infix 4 _▷_

-- Generalised sums and pattern matching
data +₂ (A B : Set) : Set where
  _₁ : A → +₂ A B
  _₂ : B → +₂ A B

data +₃ (A B C : Set) : Set where
  _₁ : A → +₃ A B C
  _₂ : B → +₃ A B C
  _₃ : C → +₃ A B C

data +₄ (A B C D : Set) : Set where
  _₁ : A → +₄ A B C D
  _₂ : B → +₄ A B C D
  _₃ : C → +₄ A B C D
  _₄ : D → +₄ A B C D

infixr 60 _₁
infixr 60 _₂
infixr 60 _₃
infixr 60 _₄

₂| : {A B : Set}{X : Set} → (A → X) → (B → X) → (+₂ A B → X)
₂| f g (a ₁) = f a
₂| f g (b ₂) = g b

₃| : {A B C : Set}{X : Set} → (A → X) → (B → X) → (C → X) → (+₃ A B C → X)
₃| f g h (a ₁) = f a
₃| f g h (b ₂) = g b
₃| f g h (c ₃) = h c

₄| : {A B C D : Set}{X : Set} → (A → X) → (B → X) → (C → X) → (D → X) → (+₄ A B C D → X)
₄| f g h e (a ₁) = f a
₄| f g h e (b ₂) = g b
₄| f g h e (c ₃) = h c
₄| f g h e (d ₄) = e d

pattern _ₛ 𝔪 = 𝔪 ₁
pattern _ₘ 𝔪 = 𝔪 ₂
infixr 60 _ₛ
infixr 60 _ₘ

-- Empty and unit families

data Ø : Familyₛ where

data _⊪_ (Γ : Ctx)(α : T) : Familyₛ where
  ● : (Γ ⊪ α) α Γ

⊪_ : T → Familyₛ
⊪ α = ∅ ⊪ α

infix 20 _⊪_
infix 20 ⊪_

-- Sum of families

infix 10 _⊹_
infix 10 _⊹_⊹_
infix 10 _⊹_⊹_⊹_

_⊹_ : Familyₛ → Familyₛ → Familyₛ
(𝒳 ⊹ 𝒴) α Γ = +₂ (𝒳 α Γ) (𝒴 α Γ)

_⊹₁_ : {𝒳₁ 𝒳₂ 𝒴₁ 𝒴₂ : Familyₛ} → (𝒳₁ ⇾̣ 𝒳₂) → (𝒴₁ ⇾̣ 𝒴₂)
     → (𝒳₁ ⊹ 𝒴₁) ⇾̣ (𝒳₂ ⊹ 𝒴₂)
(f ⊹₁ g) (x ₁) = (f x) ₁
(f ⊹₁ g) (y ₂) = (g y) ₂

_⊹_⊹_ : Familyₛ → Familyₛ → Familyₛ → Familyₛ
(𝒳 ⊹ 𝒴 ⊹ 𝒵) α Γ = +₃ (𝒳 α Γ) (𝒴 α Γ) (𝒵 α Γ)

_⊹_⊹_⊹_ : Familyₛ → Familyₛ → Familyₛ → Familyₛ → Familyₛ
(𝒳 ⊹ 𝒴 ⊹ 𝒵 ⊹ 𝒲) α Γ = +₄ (𝒳 α Γ) (𝒴 α Γ) (𝒵 α Γ) (𝒲 α Γ)


text:
module Data.Num.Properties where

open import Data.Num
open import Data.Num.Core
open import Data.Num.Next
open import Data.Num.Continuous

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra
open import Data.Fin.Properties hiding (setoid; _≟_)
open import Data.Nat.DM
open import Data.Fin as Fin
    using (Fin; #_; fromℕ≤; inject≤)
    renaming (zero to z; suc to s)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥)
open import Function
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)

open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

-- start
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- □

-- begin
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ∎

-- toℕ-⊹-ℤₙ-homo : ∀ {o}
--     → (xs ys : Numeral 1 1 o)
--     → ⟦ ⊹-ℤₙ xs ys ⟧ ≡ ⟦ xs ⟧ + ⟦ ys ⟧
-- toℕ-⊹-ℤₙ-homo {o} (x ∙) ys =
--     begin
--         Digit-toℕ x o + ⟦ ys ⟧ * 1
--     ≡⟨ cong (_+_ (Digit-toℕ x o)) (*-right-identity ⟦ ys ⟧) ⟩
--         Digit-toℕ x o + ⟦ ys ⟧
--     ∎
-- toℕ-⊹-ℤₙ-homo {o} (x ∷ xs) ys =
--     begin
--         Digit-toℕ x o + ⟦ ⊹-ℤₙ xs ys ⟧ * 1
--     ≡⟨ cong (λ w → Digit-toℕ x o + w * 1) (toℕ-⊹-ℤₙ-homo xs ys) ⟩
--         Digit-toℕ x o + (⟦ xs ⟧ + ⟦ ys ⟧) * 1
--     ≡⟨ cong (_+_ (Digit-toℕ x o)) (distribʳ-*-+ 1 ⟦ xs ⟧ ⟦ ys ⟧) ⟩
--         Digit-toℕ x o + (⟦ xs ⟧ * 1 + ⟦ ys ⟧ * 1)
--     ≡⟨ cong (λ w → Digit-toℕ x o + (⟦ xs ⟧ * 1 + w)) (*-right-identity ⟦ ys ⟧) ⟩
--         Digit-toℕ x o + (⟦ xs ⟧ * 1 + ⟦ ys ⟧)
--     ≡⟨ sym (+-assoc (Digit-toℕ x o) (⟦ xs ⟧ * 1) ⟦ ys ⟧) ⟩
--         Digit-toℕ x o + ⟦ xs ⟧ * 1 + ⟦ ys ⟧
--     ∎

toℕ-⊹-Proper-homo : ∀ {b d o}
    → (¬gapped : ¬ (Gapped#0 b d o))
    → (proper : suc d + o ≥ 2)
    → (xs ys : Numeral (suc b) (suc d) o)
    →  ⟦ ⊹-Proper ¬gapped proper xs ys ⟧ ≡ ⟦ xs ⟧ + ⟦ ys ⟧
toℕ-⊹-Proper-homo {b} {d} {o} ¬gapped proper (x ∙) ys = n+-Proper-toℕ ¬gapped proper x ys
toℕ-⊹-Proper-homo {b} {d} {o} ¬gapped proper (x ∷ xs) (y ∙) =
    begin
        ⟦ n+-Proper ¬gapped proper y (x ∷ xs) ⟧
    ≡⟨ n+-Proper-toℕ ¬gapped proper y (x ∷ xs) ⟩
        Digit-toℕ y o + (Digit-toℕ x o + ⟦ xs ⟧ * suc b)
    ≡⟨ +-comm (Digit-toℕ y o) (Digit-toℕ x o + ⟦ xs ⟧ * suc b) ⟩
        Digit-toℕ x o + ⟦ xs ⟧ * suc b + Digit-toℕ y o
    ∎
toℕ-⊹-Proper-homo {b} {d} {o} ¬gapped proper (x ∷ xs) (y ∷ ys) with sumView b d o ¬gapped proper x y
toℕ-⊹-Proper-homo {b} {d} {o} ¬gapped proper (x ∷ xs) (y ∷ ys) | NoCarry leftover property =
    begin
        Digit-toℕ leftover o + ⟦ ⊹-Proper ¬gapped proper xs ys ⟧ * suc b
    ≡⟨ cong (λ w → Digit-toℕ leftover o + w * suc b) (toℕ-⊹-Proper-homo ¬gapped proper xs ys) ⟩
        Digit-toℕ leftover o + (⟦ xs ⟧ + ⟦ ys ⟧) * suc b
    ≡⟨ cong (λ w → w + (⟦ xs ⟧ + ⟦ ys ⟧) * suc b) property ⟩
        Digit-toℕ x o + (Digit-toℕ y o) + (⟦ xs ⟧ + ⟦ ys ⟧) * suc b
    ≡⟨ cong (λ w → Digit-toℕ x o + (Digit-toℕ y o) + w) (distribʳ-*-+ (suc b) ⟦ xs ⟧ ⟦ ys ⟧) ⟩
        (Digit-toℕ x o) + (Digit-toℕ y o) + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b)
    ≡⟨ +-assoc (Digit-toℕ x o) (Digit-toℕ y o) (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b) ⟩
        Digit-toℕ x o + (Digit-toℕ y o + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b))
    ≡⟨ cong (λ w → Digit-toℕ x o + w) (a+[b+c]≡b+[a+c] (Digit-toℕ y o) (⟦ xs ⟧ * suc b) (⟦ ys ⟧ * suc b)) ⟩
        Digit-toℕ x o + (⟦ xs ⟧ * suc b + (Digit-toℕ y o + ⟦ ys ⟧ * suc b))
    ≡⟨ sym (+-assoc (Digit-toℕ x o) (⟦ xs ⟧ * suc b) (Digit-toℕ y o + ⟦ ys ⟧ * suc b)) ⟩
        Digit-toℕ x o + ⟦ xs ⟧ * suc b + (Digit-toℕ y o + ⟦ ys ⟧ * suc b)
    ∎
toℕ-⊹-Proper-homo {b} {d} {o} ¬gapped proper (x ∷ xs) (y ∷ ys) | Fixed leftover carry property =
    begin
        Digit-toℕ leftover o + ⟦ n+-Proper ¬gapped proper carry (⊹-Proper ¬gapped proper xs ys) ⟧ * suc b
    ≡⟨ cong (λ w → Digit-toℕ leftover o + w * suc b) (n+-Proper-toℕ ¬gapped proper carry (⊹-Proper ¬gapped proper xs ys))   ⟩
        Digit-toℕ leftover o + (Digit-toℕ carry o + ⟦ ⊹-Proper ¬gapped proper xs ys ⟧) * suc b
    ≡⟨ cong (λ w → Digit-toℕ leftover o + (Digit-toℕ carry o + w) * suc b) (toℕ-⊹-Proper-homo ¬gapped proper xs ys) ⟩
        Digit-toℕ leftover o + (Digit-toℕ carry o + (⟦ xs ⟧ + ⟦ ys ⟧)) * suc b
    ≡⟨ cong (λ w → Digit-toℕ leftover o + w) (distribʳ-*-+ (suc b) (Digit-toℕ carry o) (⟦ xs ⟧ + ⟦ ys ⟧)) ⟩
        Digit-toℕ leftover o + ((Digit-toℕ carry o) * suc b + (⟦ xs ⟧ + ⟦ ys ⟧) * suc b)
    ≡⟨ cong (λ w → Digit-toℕ leftover o + ((Digit-toℕ carry o) * suc b + w)) (distribʳ-*-+ (suc b) ⟦ xs ⟧ ⟦ ys ⟧) ⟩
        Digit-toℕ leftover o + ((Digit-toℕ carry o) * suc b + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b))
    ≡⟨ sym (+-assoc (Digit-toℕ leftover o) ((Digit-toℕ carry o) * suc b) (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b)) ⟩
        Digit-toℕ leftover o + (Digit-toℕ carry o) * suc b + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b)
    ≡⟨ cong (λ w → w + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b)) property ⟩
        (Digit-toℕ x o) + (Digit-toℕ y o) + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b)
    ≡⟨ +-assoc (Digit-toℕ x o) (Digit-toℕ y o) (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b) ⟩
        Digit-toℕ x o + (Digit-toℕ y o + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b))
    ≡⟨ cong (λ w → Digit-toℕ x o + w) (a+[b+c]≡b+[a+c] (Digit-toℕ y o) (⟦ xs ⟧ * suc b) (⟦ ys ⟧ * suc b)) ⟩
        Digit-toℕ x o + (⟦ xs ⟧ * suc b + (Digit-toℕ y o + ⟦ ys ⟧ * suc b))
    ≡⟨ sym (+-assoc (Digit-toℕ x o) (⟦ xs ⟧ * suc b) (Digit-toℕ y o + ⟦ ys ⟧ * suc b)) ⟩
        Digit-toℕ x o + ⟦ xs ⟧ * suc b + (Digit-toℕ y o + ⟦ ys ⟧ * suc b)
    ∎
toℕ-⊹-Proper-homo {b} {d} {o} ¬gapped proper (x ∷ xs) (y ∷ ys) | Floating leftover carry property =
    begin
        Digit-toℕ leftover o + ⟦ n+-Proper ¬gapped proper carry (⊹-Proper ¬gapped proper xs ys) ⟧ * suc b
    ≡⟨ cong (λ w → Digit-toℕ leftover o + w * suc b) (n+-Proper-toℕ ¬gapped proper carry (⊹-Proper ¬gapped proper xs ys))   ⟩
        Digit-toℕ leftover o + (Digit-toℕ carry o + ⟦ ⊹-Proper ¬gapped proper xs ys ⟧) * suc b
    ≡⟨ cong (λ w → Digit-toℕ leftover o + (Digit-toℕ carry o + w) * suc b) (toℕ-⊹-Proper-homo ¬gapped proper xs ys) ⟩
        Digit-toℕ leftover o + (Digit-toℕ carry o + (⟦ xs ⟧ + ⟦ ys ⟧)) * suc b
    ≡⟨ cong (λ w → Digit-toℕ leftover o + w) (distribʳ-*-+ (suc b) (Digit-toℕ carry o) (⟦ xs ⟧ + ⟦ ys ⟧)) ⟩
        Digit-toℕ leftover o + ((Digit-toℕ carry o) * suc b + (⟦ xs ⟧ + ⟦ ys ⟧) * suc b)
    ≡⟨ cong (λ w → Digit-toℕ leftover o + ((Digit-toℕ carry o) * suc b + w)) (distribʳ-*-+ (suc b) ⟦ xs ⟧ ⟦ ys ⟧) ⟩
        Digit-toℕ leftover o + ((Digit-toℕ carry o) * suc b + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b))
    ≡⟨ sym (+-assoc (Digit-toℕ leftover o) ((Digit-toℕ carry o) * suc b) (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b)) ⟩
        Digit-toℕ leftover o + (Digit-toℕ carry o) * suc b + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b)
    ≡⟨ cong (λ w → w + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b)) property ⟩
        (Digit-toℕ x o) + (Digit-toℕ y o) + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b)
    ≡⟨ +-assoc (Digit-toℕ x o) (Digit-toℕ y o) (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b) ⟩
        Digit-toℕ x o + (Digit-toℕ y o + (⟦ xs ⟧ * suc b + ⟦ ys ⟧ * suc b))
    ≡⟨ cong (λ w → Digit-toℕ x o + w) (a+[b+c]≡b+[a+c] (Digit-toℕ y o) (⟦ xs ⟧ * suc b) (⟦ ys ⟧ * suc b)) ⟩
        Digit-toℕ x o + (⟦ xs ⟧ * suc b + (Digit-toℕ y o + ⟦ ys ⟧ * suc b))
    ≡⟨ sym (+-assoc (Digit-toℕ x o) (⟦ xs ⟧ * suc b) (Digit-toℕ y o + ⟦ ys ⟧ * suc b)) ⟩
        Digit-toℕ x o + ⟦ xs ⟧ * suc b + (Digit-toℕ y o + ⟦ ys ⟧ * suc b)
    ∎

-- _⊹_ : ∀ {b d o}
--     → {cond : N+Closed b d o}
--     → (xs ys : Numeral b d o)
--     → Numeral b d o
-- _⊹_ {b} {d} {o} {IsContinuous cont} xs ys with numView b d o
-- _⊹_ {cond = IsContinuous ()} xs ys | NullBase d o
-- _⊹_ {cond = IsContinuous cont} xs ys | NoDigits b o = NoDigits-explode xs
-- _⊹_ {cond = IsContinuous ()} xs ys | AllZeros b
-- _⊹_ {cond = IsContinuous cont} xs ys | Proper b d o proper with Gapped#0? b d o
-- _⊹_ {cond = IsContinuous ()} xs ys | Proper b d o proper | yes ¬gapped#0
-- _⊹_ {cond = IsContinuous cont} xs ys | Proper b d o proper | no ¬gapped#0 = ⊹-Proper (≤-pred (≰⇒> ¬gapped#0)) proper xs ys
-- _⊹_ {cond = ℤₙ} xs ys = ⊹-ℤₙ xs ys

toℕ-⊹-homo : ∀ {b d o}
    → (cont : True (Continuous? b d o))
    → (xs ys : Numeral b d o)
    → ⟦ _⊹_ {cont = cont} xs ys ⟧ ≡ ⟦ xs ⟧ + ⟦ ys ⟧
toℕ-⊹-homo {b} {d} {o} cont xs ys with numView b d o
toℕ-⊹-homo ()   xs ys | NullBase d o
toℕ-⊹-homo cont xs ys | NoDigits b o = NoDigits-explode xs
toℕ-⊹-homo ()   xs ys | AllZeros b
toℕ-⊹-homo cont xs ys | Proper b d o proper with Gapped#0? b d o
toℕ-⊹-homo ()   xs ys | Proper b d o proper | yes gapped#0
toℕ-⊹-homo cont xs ys | Proper b d o proper | no ¬gapped#0 = toℕ-⊹-Proper-homo ¬gapped#0 proper xs ys

-- toℕ-≋-ℕ⇒Num-lemma-1 : ∀ m n → m * suc n ≡ 0 → m ≡ 0
-- toℕ-≋-ℕ⇒Num-lemma-1 zero n p = refl
-- toℕ-≋-ℕ⇒Num-lemma-1 (suc m) n ()
--
--
-- toℕ-≋-ℕ⇒Num-lemma-2 : ∀ m n → m ≢ 0 → m + n ≢ 0
-- toℕ-≋-ℕ⇒Num-lemma-2 zero    n p = contradiction refl p
-- toℕ-≋-ℕ⇒Num-lemma-2 (suc m) n p ()
--
-- toℕ-≋-ℕ⇒Numeral : ∀ {b d o}
--     → (xs ys : Numeral b d o)
--     → toℕ xs ≡ toℕ ys
--     → xs ≋ ys
-- toℕ-≋-ℕ⇒Numeral ∙ ∙        ⟦xs⟧≡⟦ys⟧ = tt
-- toℕ-≋-ℕ⇒Numeral {b} {zero} ∙ (() ∷ ys) ⟦∙⟧≡⟦y∷ys⟧
-- toℕ-≋-ℕ⇒Numeral {b} {suc d} {o} ∙ (y ∷ ys) ⟦∙⟧≡⟦y∷ys⟧ with Digit-toℕ y o ≟ 0
-- toℕ-≋-ℕ⇒Numeral {zero} {suc d} ∙ (y ∷ ys) ⟦∙⟧≡⟦y∷ys⟧ | yes p = tt
-- toℕ-≋-ℕ⇒Numeral {suc b} {suc d} {o} ∙ (y ∷ ys) ⟦∙⟧≡⟦y∷ys⟧ | yes p =
--     let ⟦ys⟧≡0 : toℕ ys * suc b ≡ 0
--         ⟦ys⟧≡0 =
--             begin
--                 toℕ ys * suc b
--             ≡⟨ cong (λ w → w + toℕ ys * suc b) (sym p) ⟩
--                 o + Fin.toℕ y + toℕ ys * suc b
--             ≡⟨ sym ⟦∙⟧≡⟦y∷ys⟧ ⟩
--                 zero
--             ∎
--     in
--     toℕ-≋-ℕ⇒Numeral ∙ ys (sym (toℕ-≋-ℕ⇒Num-lemma-1 (toℕ ys) b ⟦ys⟧≡0))
-- toℕ-≋-ℕ⇒Numeral {b} {suc d} {o} ∙ (y ∷ ys) ⟦∙⟧≡⟦y∷ys⟧ | no ¬p = toℕ-≋-ℕ⇒Num-lemma-2 (Digit-toℕ y o) (toℕ ys * b) ¬p (sym ⟦∙⟧≡⟦y∷ys⟧)
-- toℕ-≋-ℕ⇒Numeral {b} {zero} (() ∷ xs) ∙ ⟦x∷xs⟧≡⟦∙⟧
-- toℕ-≋-ℕ⇒Numeral {b} {suc d} {o} (x ∷ xs) ∙ ⟦x∷xs⟧≡⟦∙⟧ with Digit-toℕ x o ≟ 0
-- toℕ-≋-ℕ⇒Numeral {zero} {suc d} (x ∷ xs) ∙ ⟦x∷xs⟧≡⟦∙⟧ | yes p = tt
-- toℕ-≋-ℕ⇒Numeral {suc b} {suc d} (x ∷ xs) ∙ ⟦x∷xs⟧≡⟦∙⟧ | yes p = {!   !}
-- toℕ-≋-ℕ⇒Numeral {b} {suc d} (x ∷ xs) ∙ ⟦x∷xs⟧≡⟦∙⟧ | no ¬p = {!   !}
-- toℕ-≋-ℕ⇒Numeral (x ∷ xs) (x₁ ∷ ys) ⟦xs⟧≡⟦ys⟧ = {!   !}

-- begin
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ∎
-- start
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- □

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
-- Andreas, 2022-03-25, issue #5838, inconsistency in Cubical Agda.
-- Reported by Tom Jack: variant of test/Fail/Issue5838.agda.

{-# OPTIONS --safe --cubical #-}

open import Agda.Builtin.Bool
open import Agda.Builtin.Sigma

open import Agda.Primitive.Cubical
open import Agda.Primitive.Cubical public
  renaming ( primIMin       to _∧_  -- I → I → I
           ; primIMax       to _∨_  -- I → I → I
           ; primINeg       to ~_   -- I → I
           ; isOneEmpty     to empty
           ; primComp       to comp
           ; primHComp      to hcomp
           ; primTransp     to transp
           ; itIsOne        to 1=1 )

open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Glue; open Helpers public
open import Agda.Builtin.Cubical.Sub public
  renaming ( inc to inS
           ; primSubOut to outS
           )

---------------------------------------------------------------------------
-- Foundations

Type = Set

Path : (A : Type) → A → A → Type
Path A a b = PathP (λ _ → A) a b

isProp : Type → Type
isProp A = (x y : A) → x ≡ y

toPathP : {A : I → Type} {x : A i0} {y : A i1} → transp (λ i → A i) i0 x ≡ y → PathP A x y
toPathP {A = A} {x = x} p i =
  hcomp (λ j → λ { (i = i0) → x
                 ; (i = i1) → p j })
    (transp (λ j → A (i ∧ j)) (~ i) x)

isProp→PathP : ∀ {B : I → Type} → ((i : I) → isProp (B i))
               → (b0 : B i0) (b1 : B i1)
               → PathP (λ i → B i) b0 b1
isProp→PathP hB b0 b1 = toPathP (hB _ _ _)

---------------------------------------------------------------------------
-- Equivalence

-- The identity equivalence
idIsEquiv : (A : Type) → isEquiv (λ (x : A) → x)
idIsEquiv A .equiv-proof y =
  (y , refl) , λ z i → z .snd (~ i) , λ j → z .snd (~ i ∨ j)

idEquiv : (A : Type) → A ≃ A
idEquiv A .fst = λ x → x
idEquiv A .snd = idIsEquiv A

isPropIsEquiv : {A B : Type} (f : A → B) → isProp (isEquiv f)
isPropIsEquiv f p q i .equiv-proof y =
  let p2 = p .equiv-proof y .snd
      q2 = q .equiv-proof y .snd
  in p2 (q .equiv-proof y .fst) i
   , λ w j → hcomp (λ k → λ { (i = i0) → p2 w j
                            ; (i = i1) → q2 w (j ∨ ~ k)
                            ; (j = i0) → p2 (q2 w (~ k)) i
                            ; (j = i1) → w })
                   (p2 w (i ∨ j))

equivEq : {A B : Type} {e f : A ≃ B} → (h : e .fst ≡ f .fst) → e ≡ f
equivEq {e = e} {f = f} h i =
  h i , isProp→PathP (λ i → isPropIsEquiv (h i)) (e .snd) (f .snd) i

---------------------------------------------------------------------------
-- Univalence

Glue : (A : Type) {φ : I}
       → (Te : Partial φ (Σ Type λ T → T ≃ A))
       → Type
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)

ua : ∀ {A B : Type} → A ≃ B → A ≡ B
ua {A = A} {B = B} e i = Glue B (λ { (i = i0) → (A , e)
                                   ; (i = i1) → (B , idEquiv B) })

---------------------------------------------------------------------------
-- Isomorphisms

record Iso (A B : Type) : Type where
  no-eta-equality
  constructor iso
  field
    fun : A → B
    inv : B → A
    rightInv : ∀ b → fun (inv b) ≡ b
    leftInv  : ∀ a → inv (fun a) ≡ a

-- Any iso is an equivalence
module _ {A B : Type} (i : Iso A B) where
  open Iso i renaming ( fun to f
                      ; inv to g
                      ; rightInv to s
                      ; leftInv to t)

  private
    module _ (y : B) (x0 x1 : A) (p0 : f x0 ≡ y) (p1 : f x1 ≡ y) where
      fill0 : I → I → A
      fill0 i = hfill (λ k → λ { (i = i1) → t x0 k
                               ; (i = i0) → g y })
                      (inS (g (p0 (~ i))))

      fill1 : I → I → A
      fill1 i = hfill (λ k → λ { (i = i1) → t x1 k
                               ; (i = i0) → g y })
                      (inS (g (p1 (~ i))))

      fill2 : I → I → A
      fill2 i = hfill (λ k → λ { (i = i1) → fill1 k i1
                               ; (i = i0) → fill0 k i1 })
                      (inS (g y))

      p : x0 ≡ x1
      p i = fill2 i i1

      sq : I → I → A
      sq i j = hcomp (λ k → λ { (i = i1) → fill1 j (~ k)
                              ; (i = i0) → fill0 j (~ k)
                              ; (j = i1) → t (fill2 i i1) (~ k)
                              ; (j = i0) → g y })
                     (fill2 i j)

      sq1 : I → I → B
      sq1 i j = hcomp (λ k → λ { (i = i1) → s (p1 (~ j)) k
                               ; (i = i0) → s (p0 (~ j)) k
                               ; (j = i1) → s (f (p i)) k
                               ; (j = i0) → s y k })
                      (f (sq i j))

      lemIso : (x0 , p0) ≡ (x1 , p1)
      lemIso i .fst = p i
      lemIso i .snd = λ j → sq1 i (~ j)

  isoToIsEquiv : isEquiv f
  isoToIsEquiv .equiv-proof y .fst .fst = g y
  isoToIsEquiv .equiv-proof y .fst .snd = s y
  isoToIsEquiv .equiv-proof y .snd z = lemIso y (g y) (fst z) (s y) (snd z)

  isoToEquiv : A ≃ B
  isoToEquiv .fst = _
  isoToEquiv .snd = isoToIsEquiv

---------------------------------------------------------------------------
-- Booleans

notEquiv : Bool ≃ Bool
notEquiv = isoToEquiv (iso not not notnot notnot)
  where
  not : Bool → Bool
  not true = false
  not false = true

  notnot : ∀ x → not (not x) ≡ x
  notnot true  = refl
  notnot false = refl

---------------------------------------------------------------------------
-- Circle

data S¹ : Type where
  base : S¹
  loop : base ≡ base

-- rot, used in the Hopf fibration
-- we will denote rotation by _·_
-- it is called μ in the HoTT-book in "8.5.2 The Hopf construction"

rotLoop : (a : S¹) → a ≡ a
rotLoop base       = loop
rotLoop (loop i) j =
  hcomp (λ k → λ { (i = i0) → loop (j ∨ ~ k)
                 ; (i = i1) → loop (j ∧ k)
                 ; (j = i0) → loop (i ∨ ~ k)
                 ; (j = i1) → loop (i ∧ k)}) base

---------------------------------------------------------------------------
-- Inconsistency distilled from #5838

-- twisted-square : Path (Path Type S¹ S¹) refl refl  -- needs Path in Type₁
twisted-square : (i j : I) → Type  -- SLOW
twisted-square i j = Glue S¹ λ
  { (i = i0) → S¹ , equivEq {e = idEquiv S¹} {f = idEquiv S¹} (λ k x → rotLoop x k) j
  ; (i = i1) → S¹ , idEquiv S¹
  ; (j = i0) → S¹ , idEquiv S¹
  ; (j = i1) → S¹ , idEquiv S¹
  }

DoubleCover : S¹ → Type
DoubleCover base     = Bool
DoubleCover (loop i) = ua notEquiv i

-- @tomjack writes (2022-03-24):
-- Here is an addendum to Issue5838.agda which shows (I think?)
-- that compHCompU DoTransp also needs to be fixed:

twisted-square' : (i j : I) → Type
twisted-square' i j =
  hcomp (λ k → λ { (i = i0) → twisted-square k j
                 ; (i = i1) → S¹
                 ; (j = i0) → S¹
                 ; (j = i1) → S¹
                 })
        S¹

-- Exploit an invalid reduction of transp on composition for the universe.

bad' : true ≡ false
bad' k = transp (λ i → DoubleCover (transp (λ j → twisted-square' i j) (k ∧ (i ∨ ~ i)) base)) i0 false

-- Expected:
-- false != true of type Bool
-- when checking the definition of bad'

-- This is test/Fail/Issue5838:
-- Exploit an invalid reduction of transp on Glue.

bad : true ≡ false
bad k = transp (λ i → DoubleCover (transp (λ j → twisted-square i j) (k ∧ (i ∨ ~ i)) base)) i0 false

-- Expected:
-- false != true of type Bool
-- when checking the definition of bad


text:
open import Agda.Builtin.Equality

-- Case splitting should not remove implicit arguments
record ⊤ : Set where constructor tt

test₁ : {A : Set} → ⊤ → ⊤
test₁ {A} x = {!x!}

-- Case splitting on an implicit argument should make it visible
test₂ : {x : ⊤} → ⊤
test₂ = {!.x!}

-- Implicit variables in dot patterns should be replaced by _
postulate
  A B : Set
  f : A → B

test₃ : {x : A} (y : B) → f x ≡ y → B
test₃ y e = {!e!}

-- .. but not if they are bound inside the dot pattern
test₄ : (f : A → A) → f ≡ (λ x → x) → Set
test₄ f e = {!e!}


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

module UpperNaturals where

  open import Basics
  open import lib.Basics
  open import lib.NType2

  open import lib.types.Pi
  open import lib.types.Nat
  open import lib.types.Truncation

  ≤-antisymmetry : {n m : ℕ} (_ : n ≤ m) (_ : m ≤ n) → n == m
  ≤-antisymmetry {_} {_} (inl p) _ = p
  ≤-antisymmetry {_} {_} _ (inl p) = ! p
  ≤-antisymmetry {_} {_} (inr p) q = quodlibet (<-to-≱ p q)

  -- A propositional version of _≤_
  _≤p_ : ℕ → ℕ → PropT₀
  n ≤p m = (n ≤ m) , (≤-is-prop {n} {m})

  _is-upward-closed : (N : ℕ → PropT₀) → Type _
  N is-upward-closed = (n m : ℕ) → n ≤ m → (N n) holds → (N m) holds

  upward-closed-is-a-prop : (N : ℕ → PropT₀) → (N is-upward-closed) is-a-prop
  upward-closed-is-a-prop N = mp (λ _ → mp (λ m → mp (λ _ → mp (λ _ → (N m) holds-is-a-prop))))
    where
      mp = mapping-into-prop-is-a-prop

  ℕ→PropT₀-is-a-set : (ℕ → PropT₀) is-a-set
  ℕ→PropT₀-is-a-set = Π-level {_}{_}{ℕ}{λ _ → PropT₀}{0} (λ _ → hProp-is-set _)

  ℕ↑-prop : SubtypeProp (ℕ → PropT₀) _
  ℕ↑-prop = _is-upward-closed , upward-closed-is-a-prop

  {- The Upper Naturals
     An upper natural is an upward closed proposition concerning natural numbers.

     The interpretation is that an upper natural is a natural ``defined by its upper bounds'', in the
     sense that for the proposition N holding of a natural n means that n is an upper bound of N.

     The important bit about upper naturals is that they satisfy the well-ordering principle,
     constructively.
  -}
  ℕ↑ : Type₁
  ℕ↑ = Subtype ℕ↑-prop
   -- Σ (ℕ → PropT₀) _is-upward-closed

  ℕ↑-is-a-set : ℕ↑ is-a-set
  ℕ↑-is-a-set = Subtype-level ℕ↑-prop

  _is-an-upper-bound-of_ : ℕ → ℕ↑ → Type _
  n is-an-upper-bound-of M = ((fst M) n) holds

  _≤:↑_ : ℕ↑ → ℕ → Type _
  M ≤:↑ n = n is-an-upper-bound-of M

  ≤:↑-is-a-prop : {M : ℕ↑} {n : ℕ} → (M ≤:↑ n) is-a-prop
  ≤:↑-is-a-prop {M} {n} = ((fst M) n) holds-is-a-prop

  ≤p-is-upward-closed : {n : ℕ} → (n ≤p_) is-upward-closed
  ≤p-is-upward-closed = λ n m z z₁ → ≤-trans z₁ z

  _^↑ : ℕ → ℕ↑
  n ^↑ = (n ≤p_) , ≤p-is-upward-closed

  -- 0 is bounded above by every number.
  O↑ : ℕ↑
  O↑ = O ^↑

  -- Infinity is defined to be the number with no upper bounds.
  ∞↑ : ℕ↑
  ∞↑ = (λ _ → False) , proof
    where proof : (λ _ → False) is-upward-closed
          proof = λ n m _ z → z

  ∞↑-has-no-upper-bounds : (n : ℕ) → ¬ (∞↑ ≤:↑ n)
  ∞↑-has-no-upper-bounds n = λ z → z

  ≤:↑-refl : {n : ℕ} → n is-an-upper-bound-of (n ^↑)
  ≤:↑-refl = ≤-refl

  -- The ordering on the upper naturals is defined by saying that
  -- N is at most M if every upper bound of M is an upper bound of N.
  _≤↑_ : ℕ↑ → ℕ↑ → Type _
  N ≤↑ M = (n : ℕ) → M ≤:↑ n → N ≤:↑ n

  ≤↑-is-a-prop : {N M : ℕ↑} → (N ≤↑ M) is-a-prop
  ≤↑-is-a-prop {N} {M} = mp (λ n → mp (λ _ → ≤:↑-is-a-prop {N} {n}))
    where mp = mapping-into-prop-is-a-prop

  ≤↑-refl : {N : ℕ↑} → N ≤↑ N
  ≤↑-refl = λ n z → z

  ≤↑-trans : {N M P : ℕ↑} → N ≤↑ M → M ≤↑ P → N ≤↑ P
  ≤↑-trans = λ z z₁ n z₂ → z n (z₁ n z₂)

  ^↑-is-monotone : {n m : ℕ} → n ≤ m → (n ^↑) ≤↑ (m ^↑)
  ^↑-is-monotone = λ x k x₁ → ≤-trans x x₁

  ^↑-yoneda : {n : ℕ} {M : ℕ↑} → M ≤↑ (n ^↑) → M ≤:↑ n
  ^↑-yoneda {n} {M} = λ x → x n ≤:↑-refl

  ^↑-is-full : {n m : ℕ} → (n ^↑) ≤↑ (m ^↑) → n ≤ m
  ^↑-is-full {n} {m} = λ z → z m (inl idp)

  ^↑-is-ff : {n m : ℕ} → (n ≤ m) ≃ ((n ^↑) ≤↑ (m ^↑))
  ^↑-is-ff {n} {m} = equiv ^↑-is-monotone ^↑-is-full
    (λ b → prop-path (≤↑-is-a-prop {(n ^↑)} {(m ^↑)}) (λ _ → ≤-trans (b m (inl idp))) b)
    (λ a → prop-path ≤-is-prop (≤-trans a (inl idp)) a)

  =-to-≤↑ : {N M : ℕ↑} → N == M → N ≤↑ M
  =-to-≤↑ idp = λ n z → z

  ^↑-is-injective : {n m : ℕ} → (n ^↑) == (m ^↑) → n == m
  ^↑-is-injective {n} {m}  =
    λ x → ≤-antisymmetry (^↑-is-full (=-to-≤↑ x)) (^↑-is-full ((=-to-≤↑ (! x))))

  O↑≤↑ : (N : ℕ↑) → O↑ ≤↑ N
  O↑≤↑ N = λ n x → ^↑-is-monotone (O≤ n) n ≤:↑-refl

  _≤↑∞↑ : (N : ℕ↑) → N ≤↑ ∞↑
  N ≤↑∞↑ = λ n x → quodlibet (∞↑-has-no-upper-bounds n x)

  minℕ : (P : ℕ → Type₀) → ℕ↑
  minℕ P =
    (λ n → min-pred n) ,
      (λ n m x → Trunc-rec (implication n m x))
    where
      min-pred : (n : ℕ) → PropT₀
      min-pred n = ∃ (λ k → (P k) And (k ≤ n))

      implication : (n m : ℕ) (x : n ≤ m)
                    → Σ ℕ (λ k → (P k) And (k ≤ n))
                    → min-pred m holds
      implication n m x = λ {(k , p) → [ k , fst p , ≤-trans (snd p) x ] }

  {- Probably requires propositional resizing
  minℕ↑ : (P : ℕ↑ → Type₀) → ℕ↑
  minℕ↑ P =
    (λ n → min-pred n) ,
      (λ n m x → Trunc-rec (implication n m x))
    where
      min-pred : (n : ℕ) → PropT₀
      min-pred n = ∃ (λ K → (P K) And (K ≤:↑ n))

      implication : (n m : ℕ) (x : n ≤ m)
                    → Σ ℕ↑ (λ K → (P K) And (K ≤:↑ n))
                    → min-pred m holds
      implication n m x = λ {(k , p) → [ k , fst p , ≤-trans (snd p) x ] }
  -}

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
-- Agda program using the Iowa Agda library

open import bool

module TO-PROVE-evendoublecoin
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
  where

open import eq
open import nat
open import list
open import maybe

---------------------------------------------------------------------------
-- Translated Curry operations:

add : ℕ → ℕ → ℕ
add zero x = x
add (suc y) z = suc (add y z)

coin : Choice → ℕ → ℕ
coin c1 x = if choose c1 then x else suc x

double : ℕ → ℕ
double x = add x x

even : ℕ → 𝔹
even zero = tt
even (suc zero) = ff
even (suc (suc x)) = even x

---------------------------------------------------------------------------

evendoublecoin : (c1 : Choice) → (x : ℕ) → (even (double (coin c1 x))) ≡ tt
evendoublecoin c1 x = ?

---------------------------------------------------------------------------


text:
-- Andreas, 2013-10-22
-- Fixed by checking with-function-types in internal syntax!
module Issue893 where

  postulate
    S : Set

  data Dec (Px : Set) (q : Px → S) : Set where
    tt : Dec Px q

  -- record parameter is essential to reproduce error message
  record Rec (P : S → Set) : Set where
    field
      prop : {x : S} → P x → S

    bla : (x : S) → Dec (P x) prop
    bla x with x
    bla x | _ = tt