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

module homotopy.3x3.Common where

open import HoTT public hiding (↓-='-in; ↓-='-out; ↓-=-in; ↓-=-out; ↓-∘=idf-in)

!-∘-ap-inv : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : B → C) (g : A → B) {a b : A}
  (p : a == b)
  → ap-∘ f g p == ! (∘-ap f g p)
!-∘-ap-inv f g idp = idp

!-ap-∘-inv : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : B → C) (g : A → B) {a b : A}
  (p : a == b)
  → ∘-ap f g p == ! (ap-∘ f g p)
!-ap-∘-inv f g idp = idp

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

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

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

  _,_=□_,_ : {a b b' c : A} (p : a == b) (q : b == c)
             (r : a == b') (s : b' == c) → Type i
  (idp , q =□ r , idp) = (q == r)

  idp□ : {a b : A} {p : a == b} → idp , p =□ idp , p
  idp□ {p = idp} = idp

  idp□-i : {a b : A} {p : a == b} → p , idp =□ idp , p
  idp□-i {p = idp} = idp

  idp,=□idp,-in : {a b : A} {p q : a == b}
                → p == q → idp , p =□ idp , q
  idp,=□idp,-in {q = idp} α = α

  idp,=□idp,-out : {a b : A} {p q : a == b}
                 → idp , p =□ idp , q → p == q
  idp,=□idp,-out {q = idp} α = α

  idp,=□idp,-β : {a b : A} {p q : a == b}
                 (α : p == q) → idp,=□idp,-out (idp,=□idp,-in α) == α
  idp,=□idp,-β {q = idp} α = idp

  idp,=□idp,-η : {a b : A} {p q : a == b}
                  (α : idp , p =□ idp , q) → idp,=□idp,-in (idp,=□idp,-out α) == α
  idp,=□idp,-η {q = idp} α = idp

  ,idp=□,idp-in : {a b : A} {p q : a == b}
                → p == q → p , idp =□ q , idp
  ,idp=□,idp-in {p = idp} α = α

  ,idp=□,idp-out : {a b : A} {p q : a == b}
                 → p , idp =□ q , idp → p == q
  ,idp=□,idp-out {p = idp} α = α

  ,idp=□,idp-β : {a b : A} {p q : a == b}
                 (α : p == q) → ,idp=□,idp-out (,idp=□,idp-in α) == α
  ,idp=□,idp-β {p = idp} α = idp

  ,idp=□,idp-η : {a b : A} {p q : a == b}
                 (α : p , idp =□ q , idp) → ,idp=□,idp-in (,idp=□,idp-out α) == α
  ,idp=□,idp-η {p = idp} α = idp

  ,idp=□idp,-in : {a b : A} {p q : a == b}
                → p == q → p , idp =□ idp , q
  ,idp=□idp,-in {p = idp} = idp,=□idp,-in

  ,idp=□idp,-out : {a b : A} {p q : a == b}
                 → p , idp =□ idp , q → p == q
  ,idp=□idp,-out {p = idp} {q} α = idp,=□idp,-out α

  ,idp=□idp,-β : {a b : A} {p q : a == b}
                 (α : p == q) → ,idp=□idp,-out (,idp=□idp,-in α) == α
  ,idp=□idp,-β {p = idp} α = idp,=□idp,-β α

  ,idp=□idp,-η : {a b : A} {p q : a == b}
                 (α : p , idp =□ idp , q) → ,idp=□idp,-in (,idp=□idp,-out α) == α
  ,idp=□idp,-η {p = idp} α = idp,=□idp,-η α

  _∙□-i/_/_/ : {a b b' c : A} {p : a == b} {q q' : b == c}
         {r r' : a == b'} {s : b' == c}
         → (p , q =□ r , s) → (q' == q) → (r == r')
         → (p , q' =□ r' , s)
  α ∙□-i/ idp / idp / = α

  _∙□-o/_/_/ : {a b b' c : A} {p p' : a == b} {q : b == c}
         {r : a == b'} {s s' : b' == c}
         → (p , q =□ r , s) → (p' == p) → (s == s')
         → (p' , q =□ r , s')
  α ∙□-o/ idp / idp / = α

  _∙□h_ : {a b b' c c' d : A} {p : a == b} {q : b == c} {r : a == b'}
    {s : b' == c} {t : c == d} {u : b' == c'} {v : c' == d}
    → (p , q =□ r , s) → (s , t =□ u , v) → (p , q ∙ t =□ r ∙ u , v)
  _∙□h_ {p = idp} {s = idp} {v = idp} idp idp = idp

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

  ap□ : {a b b' c : A} {p : a == b} {q : b == c} {r : a == b'} {s : b' == c}
    → (p , q =□ r , s) → (ap f p , ap f q =□ ap f r , ap f s)
  ap□ {p = idp} {s = idp} α = ap (ap f) α

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

  ap□-,idp=□idp,-in :  {a b : A} {p q : a == b}
                (α : p == q) → ap□ f (,idp=□idp,-in α) == ,idp=□idp,-in (ap (ap f) α)
  ap□-,idp=□idp,-in {p = idp} idp = idp

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

  _,_=□d-i_,_ : {a b : A} {p : a == b} {u v : B a} {w x : B b}
           → (u == v) → (v == w [ B ↓ p ])
           → (u == x [ B ↓ p ]) → (x == w)
           → Type j
  _,_=□d-i_,_ idp α β idp = (α == β)
  -- _,_=□d-i_,_ {p = idp} = _,_=□_,_

  idp,=□d-iidp,-out : {a : A} {u w : B a} {α β : u == w}
    → (idp , α =□d-i idp , β) → α == β
  idp,=□d-iidp,-out {β = idp} x = x

  ,idp=□d-iidp,-out : {a : A} {u w : B a} {α β : u == w}
    → (α , idp =□d-i idp , β) → α == β
  ,idp=□d-iidp,-out {α = idp} x = idp,=□d-iidp,-out x

  idp,=□d-iidp,-in : {a : A} {u w : B a} {α β : u == w}
    → α == β → (idp , α =□d-i idp , β)
  idp,=□d-iidp,-in {β = idp} x = x

  ,idp=□d-iidp,-in : {a : A} {u w : B a} {α β : u == w}
    → α == β → (α , idp =□d-i idp , β)
  ,idp=□d-iidp,-in {α = idp} x = idp,=□d-iidp,-in x

  _◃/_/_/ : {a b : A} {p : a == b} {u v : B a} {w x : B b}
          → (v == w [ B ↓ p ]) → (u == v) → (w == x)
          → (u == x [ B ↓ p ])
  α ◃/ idp / idp / = α

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

  _,_,_=□□_,_,_ : {a0 b0 b'0 c0 a1 b1 b'1 c1 : A}
    {p0 : a0 == b0} {q0 : b0 == c0} {r0 : a0 == b'0} {s0 : b'0 == c0}
    {p1 : a1 == b1} {q1 : b1 == c1} {r1 : a1 == b'1} {s1 : b'1 == c1}
    {a* : a0 == a1} {b* : b0 == b1} {b'* : b'0 == b'1} {c* : c0 == c1}
    → (p0 , q0 =□ r0 , s0) → (s0 , c* =□ b'* , s1) → (r0 , b'* =□ a* , r1)
    → (q0 , c* =□ b* , q1) → (p0 , b* =□ a* , p1) → (p1 , q1 =□ r1 , s1)
    → Type i
  _,_,_=□□_,_,_ {p0 = idp} {s0 = idp} {p1 = idp} {s1 = idp} idp idp β γ idp idp = β == γ

{- Nondependent identity type -}

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

  ↓-='-in : {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
    → (u , ap g p =□ ap f p , v)
    → (u == v [ (λ x → f x == g x) ↓ p ])
  ↓-='-in {p = idp} α = ,idp=□idp,-out α

  ↓-='-out : {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
    → (u == v [ (λ x → f x == g x) ↓ p ])
    → (u , ap g p =□ ap f p , v)
  ↓-='-out {p = idp} α = ,idp=□idp,-in α

↓-='-β : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
  {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
  (α : (u , ap g p =□ ap f p , v))
  → ↓-='-out (↓-='-in α) == α
↓-='-β {p = idp} α = ,idp=□idp,-η α

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

  lemma-a : {x y : A} (p : x == y) {u : g (f x) == h (f x)} {v : g (f y) == h (f y)} {q : f x == f y} (r : ap f p == q)
    (α : u == v [ (λ z → g z == h z) ↓ q ])
    → ↓-='-out (↓-ap-out= (λ z → g z == h z) f p r α) == ↓-='-out α ∙□-i/ ap-∘ h f p ∙ ap (ap h) r / ! (ap (ap g) r) ∙ ∘-ap g f p /
  lemma-a idp idp idp = idp

{- Dependent identity type -}

↓-=-in : ∀ {i j} {A : Type i} {B : A → Type j} {f g : Π A B}
  {x y : A} {p : x == y} {u : g x == f x} {v : g y == f y}
  → (u , apd f p =□d-i apd g p , v)
  → (u == v [ (λ x → g x == f x) ↓ p ])
↓-=-in {B = B} {p = idp} {u} {v} α = ,idp=□d-iidp,-out α

↓-=-out : ∀ {i j} {A : Type i} {B : A → Type j} {f g : Π A B}
  {x y : A} {p : x == y} {u : g x == f x} {v : g y == f y}
  → (u == v [ (λ x → g x == f x) ↓ p ])
  → (u , apd f p =□d-i apd g p , v)
↓-=-out {B = B} {p = idp} {u} {v} α = ,idp=□d-iidp,-in α

↓-=□-in : ∀ {i j} {A : Type i} {B : Type j} {f g g' h : A → B}
  {x y : A} {α : x == y} {p : (x : A) → f x == g x} {q : (x : A) → g x == h x}
  {r : (x : A) → f x == g' x} {s : (x : A) → g' x == h x}
  {u : (p x , q x =□ r x , s x)} {v : (p y , q y =□ r y , s y)}
  → (u , ↓-='-out (apd s α) , ↓-='-out (apd r α) =□□ ↓-='-out (apd q α) , ↓-='-out (apd p α) , v)
  → (u == v [ (λ x → (p x , q x =□ r x , s x)) ↓ α ])
↓-=□-in {α = idp} = ch _ _ where

  ch : ∀ {j} {B : Type j} {f g g' h : B} {p : f == g} {q : g == h}
       {r : f == g'} {s : g' == h} (u v : p , q =□ r , s)
       → u , ,idp=□idp,-in idp , ,idp=□idp,-in idp =□□ ,idp=□idp,-in idp , ,idp=□idp,-in idp , v
       → u == v
  ch {p = idp} {s = idp} u v = ,idp=□idp,-out ∘ ch2 u idp idp v   where

    ch2 : ∀ {i} {A : Type i} {a b : A}
          {q q' r r' : a == b}
          (p : q == r) (p' : r == r')
          (s' : q == q') (s : q' == r')
          → (p , idp , ,idp=□idp,-in p' =□□ ,idp=□idp,-in s' , idp , s) → (p , p' =□ s' , s)
    ch2 idp p' s' idp α = ! (,idp=□idp,-β p') ∙ ap ,idp=□idp,-out α ∙ ,idp=□idp,-β s'

-- Dependent path in a type of the form [λ x → x ≡ g (f x)]
module _ {i j} {A : Type i} {B : Type j} (g : B → A) (f : A → B) where
  ↓-idf=∘-in : {x y : A} {p : x == y} {u : x == g (f x)} {v : y == g (f y)}
    → (u , ap g (ap f p) =□ p , v)
    → (u == v [ (λ x → x == g (f x)) ↓ p ])
  ↓-idf=∘-in {p = idp} q = ,idp=□idp,-out q

  ↓-∘=idf-in : {x y : A} {p : x == y} {u : g (f x) == x} {v : g (f y) == y}
    → (u , p =□ ap g (ap f p) , v)
    → (u == v [ (λ x → g (f x) == x) ↓ p ])
  ↓-∘=idf-in {p = idp} q = ,idp=□idp,-out q

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

  ap-∙∙`∘`∘ : {a b : A} {c d : A'} (p : a == b) (q : g b == h c) (r : c == d)
    → ap f (ap g p ∙ q ∙ ap h r) == ap (f ∘ g) p ∙ ap f q ∙ ap (f ∘ h) r
  ap-∙∙`∘`∘ idp q idp = ap-∙ f q idp

  ap-∙∙!`∘`∘ : {a b : A} {c d : A'} (p : a == b) (q : g b == h c) (r : d == c)
    → ap f (ap g p ∙ q ∙ ap h (! r)) == ap (f ∘ g) p ∙ ap f q ∙ ! (ap (f ∘ h) r)
  ap-∙∙!`∘`∘ idp q idp = ap-∙ f q idp

  ap-∙∙!'`∘`∘ : {a b : A} {c d : A'} (p : a == b) (q : g b == h c) (r : d == c)
    → ap f (ap g p ∙ q ∙ ! (ap h r)) == ap (f ∘ g) p ∙ ap f q ∙ ! (ap (f ∘ h) r)
  ap-∙∙!'`∘`∘ idp q idp = ap-∙ f q idp

  ap-!∙∙`∘`∘ : {a b : A} {c d : A'} (p : b == a) (q : g b == h c) (r : c == d)
    → ap f (ap g (! p) ∙ q ∙ ap h r) == ! (ap (f ∘ g) p) ∙ ap f q ∙ ap (f ∘ h) r
  ap-!∙∙`∘`∘ idp q idp = ap-∙ f q idp

  ap-!'∙∙`∘`∘ : {a b : A} {c d : A'} (p : b == a) (q : g b == h c) (r : c == d)
    → ap f (! (ap g p) ∙ q ∙ ap h r) == ! (ap (f ∘ g) p) ∙ ap f q ∙ ap (f ∘ h) r
  ap-!'∙∙`∘`∘ idp q idp = ap-∙ f q idp

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

  apd-∙∙`∘`∘ : {a b : A} {c d : A'} (p : a == b) (q : g b == h c) (r : c == d)
    → apd f (ap g p ∙ q ∙ ap h r) == ↓-ap-in _ _ (apd (f ∘ g) p) ∙ᵈ apd f q ∙ᵈ ↓-ap-in _ _ (apd (f ∘ h) r)
  apd-∙∙`∘`∘ idp q idp = ch q  where

    ch : {a b : B} (q : a == b)
         → apd f (q ∙ idp) == idp ∙ᵈ apd f q ∙ᵈ idp
    ch idp = idp

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

  lemma-b : {x y : A} {z t : A'} {p : x == y} {q : z == t} (r : f y == f' z)
    {a : g (f x) == h (f x)} {b : g (f y) == h (f y)}
    {c : g (f' z) == h (f' z)} {d : g (f' t) == h (f' t)}
    (u : a == b [ (λ x → g (f x) == h (f x)) ↓ p ]) (v : (b , ap h r =□ ap g r , c))
    (w : c == d [ (λ x → g (f' x) == h (f' x)) ↓ q ])
    → ↓-='-out (↓-ap-in _ f u ∙ᵈ ↓-='-in v ∙ᵈ ↓-ap-in _ f' w) == (↓-='-out u ∙□h (v ∙□h ↓-='-out w))  ∙□-i/ ap-∙∙`∘`∘ h f f' p r q / ! (ap-∙∙`∘`∘ g f f' p r q) /
  lemma-b {p = idp} {q = idp} r idp v idp = ch r v  where

    ch : ∀ {a b : B} (r : a == b) {p : g a == h a} {q : g b == h b} (v : (p , ap h r =□ ap g r , q))
         → ↓-='-out (idp ∙ᵈ ↓-='-in v ∙ᵈ idp)
           == (,idp=□idp,-in idp ∙□h (v ∙□h ,idp=□idp,-in idp))
              ∙□-i/ ap-∙ h r idp / ! (ap-∙ g r idp) /
    ch idp v = ch2 (,idp=□idp,-out v) ∙ (,idp=□idp,-η v |in-ctx (λ u → ,idp=□idp,-in idp ∙□h (u ∙□h ,idp=□idp,-in idp)))  where

      ch2 : ∀ {i} {A : Type i} {a b : A} {p q : a == b} (v' : p == q)
            → ,idp=□idp,-in (v' ∙ idp) == ,idp=□idp,-in idp ∙□h (,idp=□idp,-in v' ∙□h ,idp=□idp,-in idp)
      ch2 {p = idp} v' = ch3 v'  where

        ch3 : ∀ {i} {A : Type i} {a : A} {q : a == a} (v' : idp == q)
              → idp,=□idp,-in (v' ∙ idp) == (,idp=□idp,-in idp ∙□h (idp,=□idp,-in v' ∙□h ,idp=□idp,-in idp))
        ch3 idp = idp

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

  pp-coh : {a b b' c c' d d' e : A}
           {p : a == b}  {q : b == c}   {r : c == d}   {s : e == d}
           {t : b' == a} {u : b' == c'} {v : c' == d'} {w : d' == e}
    → (p , (q ∙ r ∙ (! s)) =□ (! t ∙ u ∙ v) , w) → (u , (v ∙ w ∙ s) =□ (t ∙ p ∙ q) , r)
  pp-coh {p = idp} {q} {idp} {idp} {idp} {idp} {idp} {idp} α = (! α) ∙ (∙-unit-r q)

  pp-coh! : {a b b' c c' d d' e : A}
            {u : b' == c'} {v : c' == d'} {w : d' == e} {s : e == d}
            {t : b' == a}  {p : a == b}   {q : b == c}  {r : c == d}
    → (u , (v ∙ w ∙ s) =□ (t ∙ p ∙ q) , r) → (p , (q ∙ r ∙ (! s)) =□ ((! t) ∙ u ∙ v) , w)
  pp-coh! {u = idp} {idp} {idp} {idp} {idp} {idp} {q} {idp} α = ∙-unit-r q ∙ (! α)

  pp-coh-β : {a b b' c c' d d' e : A}
             {u : b' == c'} {v : c' == d'} {w : d' == e} {s : e == d}
             {t : b' == a}  {p : a == b}   {q : b == c}  {r : c == d}
             (α : (u , (v ∙ w ∙ s) =□ (t ∙ p ∙ q) , r))
             → pp-coh {p = p} {q = q} {r = r} {s = s} {t = t} {u = u} {v = v} {w = w}
               (pp-coh! {u = u} {v = v} {w = w} {s = s} {t = t} {p = p} {q = q} {r = r} α) == α
  pp-coh-β {u = idp} {idp} {idp} {idp} {idp} {idp} {.idp} {idp} idp = idp

  pp-coh!-β : {a b b' c c' d d' e : A}
              {p : a == b}  {q : b == c}   {r : c == d}   {s : e == d}
              {t : b' == a} {u : b' == c'} {v : c' == d'} {w : d' == e}
              (α : (p , (q ∙ r ∙ (! s)) =□ (! t ∙ u ∙ v) , w))
              → pp-coh! {u = u} {v} {w} {s} {t} {p} {q} {r}
                (pp-coh {p = p} {q} {r} {s} {t} {u} {v} {w} α) == α
  pp-coh!-β {p = idp} {idp} {idp} {idp} {idp} {idp} {.idp} {idp} idp = idp

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

  ap-∙∙ : (f : A → B) {x y z t : A} (p : x == y) (q : y == z) (r : z == t) → ap f (p ∙ q ∙ r) == ap f p ∙ ap f q ∙ ap f r
  ap-∙∙ f idp q idp = ap-∙ f q idp

  ap-∙∙! : (f : A → B) {x y z t : A} (p : x == y) (q : y == z) (r : t == z) → ap f (p ∙ q ∙ ! r) == ap f p ∙ ap f q ∙ ! (ap f r)
  ap-∙∙! f idp q idp = ap-∙ f q idp

  ap-!∙∙ : (f : A → B) {x y z t : A} (p : y == x) (q : y == z) (r : z == t) → ap f (! p ∙ q ∙ r) == ! (ap f p) ∙ ap f q ∙ ap f r
  ap-!∙∙ f idp q idp = ap-∙ f q idp

module _ {i j k} {A : Type i} {B : Type j} {C₁ C₂ C₃ C₄ : Type k} {g₁ : C₁ → A} {g₂ : C₂ → A} {g₃ : C₃ → A} {g₄ : C₄ → A} (f : A → B) where

  ap□-pp-coh : {a b b' c c' d d' e : A}
               {p : a == b}  {q : b == c}   {r : c == d}   {s : e == d}
               {t : b' == a} {u : b' == c'} {v : c' == d'} {w : d' == e}
               (α : (p , (q ∙ r ∙ (! s)) =□ (! t ∙ u ∙ v) , w))
               → ap□ f (pp-coh {p = p} {q} {r} {s} {t} {u} {v} {w} α) ==
                 pp-coh {p = ap f p} {ap f q} {ap f r} {ap f s} {ap f t} {ap f u} {ap f v} {ap f w}
                   (ap□ f α ∙□-i/ ! (ap-∙∙! f q r s) / ap-!∙∙ f t u v /)
                 ∙□-i/ ap-∙∙ f v w s / ! (ap-∙∙ f t p q) /
  ap□-pp-coh {p = idp} {q} {idp} {idp} {idp} {idp} {idp} {idp} α = c q idp α  where

    c : {a b : A} (q q' : a == b) (α : q ∙ idp == q')
        → ap (ap f) (! α ∙ ∙-unit-r q) ==
          (! (ap (ap f) α ∙□-i/ ! (ap-∙∙! f q idp idp) / idp /) ∙
          ∙-unit-r (ap f q))
          ∙□-i/ idp / ! (ap-∙∙ f idp idp q) /
    c idp q' α = d α  where

      d : {a b : A} {q q' : a == b} (α : q == q')
          → ap (ap f) (! α ∙ idp) == ! (ap (ap f) α) ∙ idp
      d idp = idp

  ap□-coh : {a₁ b₁ : C₁} {a₂ b₂ : C₂} {a₃ b₃ : C₃} {a₄ b₄ : C₄}
               {p : g₃ b₃ == g₁ a₁} {q : a₁ == b₁}       {r : g₁ b₁ == g₂ b₂} {s : a₂ == b₂}
               {t : a₃ == b₃}       {u : g₃ a₃ == g₄ a₄} {v : a₄ == b₄}       {w : g₄ b₄ == g₂ a₂}
               (α : (p , (ap g₁ q ∙ r ∙ (! (ap g₂ s))) =□ (! (ap g₃ t) ∙ u ∙ ap g₄ v) , w))
               → ap□ f (pp-coh {p = p} {ap g₁ q} {r} {ap g₂ s} {ap g₃ t} {u} {ap g₄ v} {w} α) ==
                 pp-coh {p = ap f p} {ap (f ∘ g₁) q} {ap f r} {ap (f ∘ g₂) s} {ap (f ∘ g₃) t} {ap f u} {ap (f ∘ g₄) v} {ap f w}
                   (ap□ f α ∙□-i/ ! (ap-∙∙!'`∘`∘ f g₁ g₂ q r s) / ap-!'∙∙`∘`∘ f g₃ g₄ t u v /)
                 ∙□-i/ ap-∙∙`∘`∘ f g₄ g₂ v w s / ! (ap-∙∙`∘`∘ f g₃ g₁ t p q) /
  ap□-coh {p = p} {idp} {r} {idp} {idp} {u} {idp} {w} α = ap□-pp-coh {p = p} {idp} {r} {idp} {idp} {u} {idp} {w} α

module _ {i j k} {A : Type i} {B : Type j} {C₁ C₂ C₃ C₄ : Type k} {g₁ : C₁ → A} {g₂ : C₂ → A} {g₃ : C₃ → A} {g₄ : C₄ → A} (f : A → B) where

  ap□-pp-coh! : {a b b' c c' d d' e : A}
               {u : b' == c'} {v : c' == d'} {w : d' == e} {s : e == d}
               {t : b' == a}  {p : a == b}   {q : b == c}  {r : c == d}
               (α : (u , (v ∙ w ∙ s) =□ (t ∙ p ∙ q) , r))
               → ap□ f (pp-coh! {u = u} {v} {w} {s} {t} {p} {q} {r} α) ==
                 pp-coh! {u = ap f u} {ap f v} {ap f w} {ap f s} {ap f t} {ap f p} {ap f q} {ap f r}
                   (ap□ f α ∙□-i/ ! (ap-∙∙ f v w s) / ap-∙∙ f t p q /)
                 ∙□-i/ ap-∙∙! f q r s / ! (ap-!∙∙ f t u v) /
  ap□-pp-coh! {u = idp} {idp} {idp} {idp} {idp} {idp} {.idp} {idp} idp = idp

  ap□-coh! : {a₁ b₁ : C₁} {a₂ b₂ : C₂} {a₃ b₃ : C₃} {a₄ b₄ : C₄}
               {u : g₃ a₃ == g₄ a₄} {v : a₄ == b₄}       {w : g₄ b₄ == g₂ a₂} {s : a₂ == b₂}
               {t : a₃ == b₃}       {p : g₃ b₃ == g₁ a₁} {q : a₁ == b₁}       {r : g₁ b₁ == g₂ b₂}
               (α : (u , (ap g₄ v ∙ w ∙ ap g₂ s) =□ (ap g₃ t ∙ p ∙ ap g₁ q) , r))
               → ap□ f (pp-coh! {u = u} {ap g₄ v} {w} {ap g₂ s} {ap g₃ t} {p} {ap g₁ q} {r} α) ==
                 pp-coh! {u = ap f u} {ap (f ∘ g₄) v} {ap f w} {ap (f ∘ g₂) s} {ap (f ∘ g₃) t} {ap f p} {ap (f ∘ g₁) q} {ap f r}
                   (ap□ f α ∙□-i/ ! (ap-∙∙`∘`∘ f g₄ g₂ v w s) / ap-∙∙`∘`∘ f g₃ g₁ t p q /)
                 ∙□-i/ ap-∙∙!'`∘`∘ f g₁ g₂ q r s / ! (ap-!'∙∙`∘`∘ f g₃ g₄ t u v) /
  ap□-coh! {u = u} {idp} {w} {idp} {idp} {p} {idp} {r} α = ap□-pp-coh! {u = u} {idp} {w} {idp} {idp} {p} {idp} {r} α

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

  lemma : {a b b' c c' d d' e : A}
          {u u' : b' == c'} {v : c' == d'} {w w' : d' == e} {s : e == d}
          {t : b' == a}  {p p' : a == b}   {q : b == c}  {r r' : c == d}
          (β : u' == u) (γ : w' == w) (δ : p' == p) (ε : r' == r)
          (α : (u , (v ∙ w ∙ s) =□ (t ∙ p ∙ q) , r))
          → pp-coh {p = p'} {q} {r'} {s} {t} {u'} {v} {w'}
             (pp-coh! {u = u} {v} {w} {s} {t} {p} {q} {r} α
              ∙□-o/ δ / ! γ /
              ∙□-i/ ε |in-ctx (λ x → q ∙ x ∙ ! s) / (! β) |in-ctx (λ x → ! t ∙ x ∙ v) /) == α ∙□-o/ β / ! ε / ∙□-i/ γ |in-ctx (λ x → v ∙ x ∙ s) / (! δ) |in-ctx (λ x → t ∙ x ∙ q) /
  lemma {u = u} {v = v} {w = w} {s = s} {t = t} {p = p} {q = q} {r = r} idp idp idp idp α = pp-coh-β {u = u} {v = v} {w = w} {s = s} {t = t} {p = p} {q = q} {r = r} α

  lemma! : {a b b' c c' d d' e : A}
           {p p' : a == b} {q : b == c}      {r r' : c == d} {s : e == d}
           {t : b' == a}   {u u' : b' == c'} {v : c' == d'}  {w w' : d' == e}
           (β : p' == p) (γ : r' == r) (δ : u' == u) (ε : w' == w)
           (α : (p , (q ∙ r ∙ (! s)) =□ (! t ∙ u ∙ v) , w))
           → pp-coh! {u = u'} {v} {w'} {s} {t} {p'} {q} {r'}
               (pp-coh {p = p} {q} {r} {s} {t} {u} {v} {w} α
                ∙□-o/ δ / ! γ /
                ∙□-i/ ε |in-ctx (λ w → v ∙ w ∙ s) / (! β) |in-ctx (λ p → t ∙ p ∙ q) /) == α ∙□-o/ β / ! ε / ∙□-i/ γ |in-ctx (λ r → q ∙ r ∙ ! s) / (! δ) |in-ctx (λ u → ! t ∙ u ∙ v) /
  lemma! {p = p} {q = q} {r = r} {s = s} {t = t} {u = u} {v = v} {w = w} idp idp idp idp α = pp-coh!-β {p = p} {q} {r} {s} {t} {u} {v} {w} α

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

  coh1 : {a b : A} {α : a == b} {u v : B a} {w x : B b}
         {p : u == w [ B ↓ α ]} {q : w == x} {r : u == v} {s : v == x [ B ↓ α ]}
         → (r , s =□d-i p , q) → p == s ◃/ r / ! q /
  coh1 {α = idp} {p = idp} {idp} {idp} {s} β = ! β

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

  ap↓-↓-='-in-β : {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
    (α : (u , ap g p =□ ap f p , v))
    → ap↓ (ap h) {p = p} {u = u} {v = v} (↓-='-in {p = p} α)
    == ↓-='-in ((ap□ h α) ∙□-i/ (ap-∘ h g p) / (∘-ap h f p) /)
  ap↓-↓-='-in-β {p = idp} = t  where

    t : {x y : B} {u v : x == y} (α : (u , idp =□ idp , v))
        → ap (ap h) (,idp=□idp,-out α) == ,idp=□idp,-out (ap□ h α)
    t {u = idp} {v} = t'  where

      t' : {x y : B} {u v : x == y} (α : (idp , u =□ idp , v))
         → ap (ap h) (idp,=□idp,-out α) == idp,=□idp,-out (ap□ h α)
      t' {u} {v = idp} α = idp

  ap□-↓-='-out-β : {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
    (α : u == v [ (λ x → f x == g x) ↓ p ])
    → ap□ h (↓-='-out α) == ↓-='-out (ap↓ (ap h) α) ∙□-i/ ∘-ap h g p / ap-∘ h f p /
  ap□-↓-='-out-β {p = idp} idp = ap□-,idp=□idp,-in h idp

thing : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
        {x y : A} {p : x == y} {u u' : f x == g x} {v v' : f y == g y}
        (α : (u , ap g p =□ ap f p , v)) (r : u' == u) (s : v == v')
        → ↓-='-out (↓-='-in α ◃/ r / s /) == α ∙□-o/ r / s /
thing α idp idp = ↓-='-β α

ap↓-∘ : ∀ {i j k l} {A : Type i} {B : A → Type j} {C : A → Type k} {D : A → Type l}
  (f : {a : A} → C a → D a) (g : {a : A} → B a → C a)
  {x y : A} {p : x == y} {u : B x} {v : B y} (q : u == v [ B ↓ p ])
  → ap↓ (f ∘ g) q == ap↓ f (ap↓ g q)
ap↓-∘ f g {p = idp} idp = idp

ap↓-◃/ : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  (f : {a : A} → B a → C a) {x y : A} {p : x == y} {u u' : B x} {v v' : B y}
  (q : u == v [ B ↓ p ]) (r : u' == u) (s : v == v')
  → ap↓ f (q ◃/ r / s /) == ap↓ f q ◃/ ap f r / ap f s /
ap↓-◃/ f {p = idp} idp idp idp = idp

ap□-∙□-i/ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  {a b b' c : A} {p : a == b} {q q' : b == c} {r r' : a == b'} {s : b' == c}
  (α : (p , q =□ r , s)) (t : q' == q) (u : r == r')
  → ap□ f (α ∙□-i/ t / u /) == ap□ f α ∙□-i/ ap (ap f) t / ap (ap f) u /
ap□-∙□-i/ f {p = idp} {s = idp} idp idp idp = idp

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

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

ap-∘-ap-coh : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  (g : B → C) (f : A → B) {a b : A} {p q : a == b} (α : p == q)
  → ap (ap g) (! α |in-ctx (ap f)) ∙ ∘-ap g f p ∙ (α |in-ctx (ap (g ∘ f)))
  == ∘-ap g f q
ap-∘-ap-coh g f idp = ∙-unit-r _

ap-∘-ap-coh' : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  (g : B → C) (f : A → B) {a b : A} {p q : a == b} (α : p == q)
  → (! α |in-ctx (ap (g ∘ f))) ∙ ap-∘ g f p ∙ ap (ap g) (α |in-ctx (ap f))
  == ap-∘ g f q
ap-∘-ap-coh' g f idp = ∙-unit-r _

ap-∘-ap-coh'2 : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  (g : B → C) (f : A → B) {a b : A} {p q : a == b} (α : p == q)
  → (! (α |in-ctx (ap (g ∘ f)))) ∙ ap-∘ g f p ∙ ap (ap g) (α |in-ctx (ap f))
  == ap-∘ g f q
ap-∘-ap-coh'2 g f {p = idp} idp = idp

module _ {i i' j k l} {A : Type i} {A' : Type i'} {B : Type j} {C : Type k} {D : Type l}
  (f2 : C → D) (f1 : B → C) (g : A → B) (h : A' → B) where

  ap-∘-ap-∙∙!`∘`∘-coh : {a b : A} {c d : A'} (p : a == b) (q : g b == h c) (r : d == c)
    → ! (ap-∙∙!'`∘`∘ f2 (f1 ∘ g) (f1 ∘ h) p (ap f1 q) r)
      ∙ ap (ap f2) (! (ap-∙∙!`∘`∘ f1 g h p q r))
      ∙ ∘-ap f2 f1 (ap g p ∙ q ∙ ap h (! r))
      ∙ ap-∙∙!`∘`∘ (f2 ∘ f1) g h p q r
      == ((∘-ap f2 f1 q) |in-ctx (λ u → ap (f2 ∘ f1 ∘ g) p ∙ u ∙ ! (ap (f2 ∘ f1 ∘ h) r)))
  ap-∘-ap-∙∙!`∘`∘-coh idp q idp = coh q  where

    coh : {a b : B} (q : a == b) →
          ! (ap-∙ f2 (ap f1 q) idp)
          ∙ ap (ap f2) (! (ap-∙ f1 q idp))
          ∙ ∘-ap f2 f1 (q ∙ idp)
          ∙ ap-∙ (f2 ∘ f1) q idp
          == ap (λ u → u ∙ idp) (∘-ap f2 f1 q)
    coh idp = idp

  ap-∘-ap-!∙∙`∘`∘-coh : {a b : A} {c d : A'} (p : a == b) (q : g a == h c) (r : c == d)
    → ! (ap-!∙∙`∘`∘ (f2 ∘ f1) g h p q r)
      ∙ ap-∘ f2 f1 (ap g (! p) ∙ q ∙ ap h r)
      ∙ ap (ap f2) (ap-!∙∙`∘`∘ f1 g h p q r)
      ∙ ap-!'∙∙`∘`∘ f2 (f1 ∘ g) (f1 ∘ h) p (ap f1 q) r
      == ((ap-∘ f2 f1 q) |in-ctx (λ u → ! (ap (f2 ∘ f1 ∘ g) p) ∙ u ∙ ap (f2 ∘ f1 ∘ h) r))
  ap-∘-ap-!∙∙`∘`∘-coh idp q idp = coh q where

    coh : {a b : B} (q : a == b)
          → ! (ap-∙ (f2 ∘ f1) q idp) ∙ ap-∘ f2 f1 (q ∙ idp) ∙ ap (ap f2) (ap-∙ f1 q idp) ∙ ap-∙ f2 (ap f1 q) idp
          == ap (λ u → u ∙ idp) (ap-∘ f2 f1 q)
    coh idp = idp

  ap-∘-ap-∙∙2`∘`∘-coh : {a b : A} {c d : A'} (p : a == b) (q : g b == h c) (r : c == d)
    → ! (ap-∙∙`∘`∘ (f2 ∘ f1) g h p q r)
      ∙ ap-∘ f2 f1 (ap g p ∙ q ∙ ap h r)
      ∙ ap (ap f2) (ap-∙∙`∘`∘ f1 g h p q r)
      ∙ ap-∙∙`∘`∘ f2 (f1 ∘ g) (f1 ∘ h) p (ap f1 q) r
      == ((ap-∘ f2 f1 q) |in-ctx (λ u → ap (f2 ∘ f1 ∘ g) p ∙ u ∙ ap (f2 ∘ f1 ∘ h) r))
  ap-∘-ap-∙∙2`∘`∘-coh idp q idp = coh q where

    coh : {a b : B} (q : a == b)
          → ! (ap-∙ (f2 ∘ f1) q idp) ∙ ap-∘ f2 f1 (q ∙ idp) ∙ ap (ap f2) (ap-∙ f1 q idp) ∙ ap-∙ f2 (ap f1 q) idp
          == ap (λ u → u ∙ idp) (ap-∘ f2 f1 q)
    coh idp = idp

  ap-∘-ap-∙∙3`∘`∘-coh : {a b : A} {c d : A'} (p : a == b) (q : g b == h c) (r : c == d)
    → ! (ap-∙∙`∘`∘ f2 (f1 ∘ g) (f1 ∘ h) p (ap f1 q) r)
      ∙ ap (ap f2) (! (ap-∙∙`∘`∘ f1 g h p q r))
      ∙ ∘-ap f2 f1 (ap g p ∙ q ∙ ap h r)
      ∙ ap-∙∙`∘`∘ (f2 ∘ f1) g h p q r
      == ((∘-ap f2 f1 q) |in-ctx (λ u → ap (f2 ∘ f1 ∘ g) p ∙ u ∙ ap (f2 ∘ f1 ∘ h) r))
  ap-∘-ap-∙∙3`∘`∘-coh idp q idp = coh q  where

    coh : {a b : B} (q : a == b) →
          ! (ap-∙ f2 (ap f1 q) idp)
          ∙ ap (ap f2) (! (ap-∙ f1 q idp))
          ∙ ∘-ap f2 f1 (q ∙ idp)
          ∙ ap-∙ (f2 ∘ f1) q idp
          == ap (λ u → u ∙ idp) (∘-ap f2 f1 q)
    coh idp = idp

  ap-∘-ap-∙∙4`∘`∘-coh : {a b : A} {c d : A'} (p : a == b) {q : g b == h c} {q' : f1 (g b) == f1 (h c)} (α : ap f1 q == q') (r : c == d)
    → ap-∘ f2 f1 (ap g p ∙ q ∙ ap h r)
      ∙ ap (ap f2) (ap-∙∙`∘`∘ f1 g h p q r)
      ∙ ap (ap f2) (α |in-ctx (λ u → ap (f1 ∘ g) p ∙ u ∙ ap (f1 ∘ h) r))
      ∙ ap-∙∙`∘`∘ f2 (f1 ∘ g) (f1 ∘ h) p q' r
      ==
      ap-∙∙`∘`∘ (f2 ∘ f1) g h p q r
      ∙ (ap-∘ f2 f1 q |in-ctx (λ u → ap (f2 ∘ f1 ∘ g) p ∙ u ∙ ap (f2 ∘ f1 ∘ h) r))
      ∙ (ap (ap f2) α |in-ctx (λ u → ap (f2 ∘ f1 ∘ g) p ∙ u ∙ ap (f2 ∘ f1 ∘ h) r))
  ap-∘-ap-∙∙4`∘`∘-coh idp {q = q} idp idp = coh q  where

    coh : {a b : B} (q : a == b)
          → ap-∘ f2 f1 (q ∙ idp) ∙ ap (ap f2) (ap-∙ f1 q idp) ∙ ap-∙ f2 (ap f1 q) idp
          == ap-∙ (f2 ∘ f1) q idp ∙ ap (λ u → u ∙ idp) (ap-∘ f2 f1 q) ∙ idp
    coh idp = idp

  ap-∘-ap-∙∙5`∘`∘-coh : {a b : A} {c d : A'} (p : a == b) {q : g a == h c} {q' : f1 (g a) == f1 (h c)} (α : ap f1 q == q') (r : c == d)
    → ap-∘ f2 f1 (ap g (! p) ∙ q ∙ ap h r)
      ∙ ap (ap f2) (ap-!∙∙`∘`∘ f1 g h p q r)
      ∙ ap (ap f2) (α |in-ctx (λ u → ! (ap (f1 ∘ g) p) ∙ u ∙ ap (f1 ∘ h) r))
      ∙ ap-!'∙∙`∘`∘ f2 (f1 ∘ g) (f1 ∘ h) p q' r
      ==
      ap-∙∙`∘`∘ (f2 ∘ f1) g h (! p) q r
      ∙ (ap-∘ f2 f1 q |in-ctx (λ u → ap (f2 ∘ f1 ∘ g) (! p) ∙ u ∙ ap (f2 ∘ f1 ∘ h) r))
      ∙ (ap (ap f2) α |in-ctx (λ u → ap (f2 ∘ f1 ∘ g) (! p) ∙ u ∙ ap (f2 ∘ f1 ∘ h) r))
      ∙ (ap-! (f2 ∘ f1 ∘ g) p |in-ctx (λ u → u ∙ ap f2 q' ∙ ap (f2 ∘ f1 ∘ h) r))
  ap-∘-ap-∙∙5`∘`∘-coh idp {q = q} idp idp = coh q  where

    coh : {a b : B} (q : a == b)
          → ap-∘ f2 f1 (q ∙ idp) ∙ ap (ap f2) (ap-∙ f1 q idp) ∙ ap-∙ f2 (ap f1 q) idp
          == ap-∙ (f2 ∘ f1) q idp ∙ ap (λ u → u ∙ idp) (ap-∘ f2 f1 q) ∙ idp
    coh idp = idp

  ap-∘-ap-∙∙`∘`∘-coh : {a b : A} {c d : A'} (p : a == b) {q : g b == h c} {q' : f1 (g b) == f1 (h c)} (α : ap f1 q == q') (r : c == d)
    → ap (ap f2) (ap-∙∙`∘`∘ f1 g h p q r)
      ∙ ap (ap f2) (α |in-ctx (λ u → ap (f1 ∘ g) p ∙ u ∙ ap (f1 ∘ h) r))
      ∙ ap-∙∙`∘`∘ f2 (f1 ∘ g) (f1 ∘ h) p q' r
      ==
      ∘-ap f2 f1 (ap g p ∙ q ∙ ap h r)
      ∙ ap-∙∙`∘`∘ (f2 ∘ f1) g h p q r
      ∙ (ap-∘ f2 f1 q |in-ctx (λ u → ap (f2 ∘ f1 ∘ g) p ∙ u ∙ ap (f2 ∘ f1 ∘ h) r))
      ∙ (ap (ap f2) α |in-ctx (λ u → ap (f2 ∘ f1 ∘ g) p ∙ u ∙ ap (f2 ∘ f1 ∘ h) r))
  ap-∘-ap-∙∙`∘`∘-coh idp {q = q} idp idp = coh q  where

    coh : {a b : B} (q : a == b)
          → ap (ap f2) (ap-∙ f1 q idp) ∙ ap-∙ f2 (ap f1 q) idp
          == ∘-ap f2 f1 (q ∙ idp) ∙ ap-∙ (f2 ∘ f1) q idp ∙ ap (λ u → u ∙ idp) (ap-∘ f2 f1 q) ∙ idp
    coh idp = idp

  ap-∘-ap-∙∙!'`∘`∘-coh : {a b : A} {c d : A'} (p : a == b) {q : g b == h c} {q' : f1 (g b) == f1 (h c)} (α : ap f1 q == q') (r : d == c)
    → ap (ap f2) (ap-∙∙!`∘`∘ f1 g h p q r)
      ∙ ap (ap f2) (α |in-ctx (λ u → ap (f1 ∘ g) p ∙ u ∙ ! (ap (f1 ∘ h) r)))
      ∙ ap-∙∙!'`∘`∘ f2 (f1 ∘ g) (f1 ∘ h) p q' r
      ==
      ∘-ap f2 f1 (ap g p ∙ q ∙ ap h (! r))
      ∙ ap-∙∙!`∘`∘ (f2 ∘ f1) g h p q r
      ∙ (ap-∘ f2 f1 q |in-ctx (λ u → ap (f2 ∘ f1 ∘ g) p ∙ u ∙ ! (ap (f2 ∘ f1 ∘ h) r)))
      ∙ (ap (ap f2) α |in-ctx (λ u → ap (f2 ∘ f1 ∘ g) p ∙ u ∙ ! (ap (f2 ∘ f1 ∘ h) r)))
  ap-∘-ap-∙∙!'`∘`∘-coh idp {q = q} idp idp = coh q  where

    coh : {a b : B} (q : a == b)
          → ap (ap f2) (ap-∙ f1 q idp) ∙ ap-∙ f2 (ap f1 q) idp
          == ∘-ap f2 f1 (q ∙ idp) ∙ ap-∙ (f2 ∘ f1) q idp ∙ ap (λ u → u ∙ idp) (ap-∘ f2 f1 q) ∙ idp
    coh idp = idp

  ap-∘-ap-∙∙!'2`∘`∘-coh : {a b : A} {c d : A'} (p : a == b) {q : g b == h c} {q' : f1 (g b) == f1 (h c)} (α : ap f1 q == q') (r : d == c)
    → ap (ap f2) (ap-∙∙!`∘`∘ f1 g h p q r)
      ∙ ap (ap f2) (α |in-ctx (λ u → ap (f1 ∘ g) p ∙ u ∙ ! (ap (f1 ∘ h) r)))
      ∙ ap-∙∙!'`∘`∘ f2 (f1 ∘ g) (f1 ∘ h) p q' r
      ==
      ap (ap f2) (ap-∙∙`∘`∘ f1 g h p q (! r))
      ∙ ap (ap f2) (α |in-ctx (λ u → ap (f1 ∘ g) p ∙ u ∙ ap (f1 ∘ h) (! r)))
      ∙ ap-∙∙!`∘`∘ f2 (f1 ∘ g) (f1 ∘ h) p q' r
  ap-∘-ap-∙∙!'2`∘`∘-coh idp {q = q} idp idp = idp

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

  ap-!∙∙`∘`∘-coh : {a b : A} {c d : A'} (p : b == a) {q : g b == h c} {q' : f (g b) == f (h c)} (α : ap f q == q') (r : c == d)
    → ap-!∙∙`∘`∘ f g h p q r
      ∙ ap (λ u → ! (ap (f ∘ g) p) ∙ u ∙ ap (f ∘ h) r) α
      ∙ ! (ap-! (f ∘ g) p |in-ctx (λ u → u ∙ q' ∙ ap (f ∘ h) r))
      ==
      ap-∙∙`∘`∘ f g h (! p) q r
      ∙' ap (λ u → ap (f ∘ g) (! p) ∙ u ∙ ap (f ∘ h) r) α
  ap-!∙∙`∘`∘-coh idp {q = q} idp idp = ∙-unit-r (ap-∙ f q idp)

  ap-∙∙!`∘`∘-coh1 : {a b : A} {c d : A'} (p : a == b) {q : g b == h c} {q' : f (g b) == f (h c)} (α : ap f q == q') (r : d == c)
    → ap-∙∙!`∘`∘ f g h p q r
      ∙ ap (λ u → ap (f ∘ g) p ∙ u ∙ ! (ap (f ∘ h) r)) α
      ==
      ap-∙∙`∘`∘ f g h p q (! r)
      ∙ ap (λ u → ap (f ∘ g) p ∙ u ∙ ap (f ∘ h) (! r)) α
      ∙ (ap-! (f ∘ h) r |in-ctx (λ u → ap (f ∘ g) p ∙ q' ∙ u))
  ap-∙∙!`∘`∘-coh1 idp {q = q} idp idp = idp

  ap-∙∙!`∘`∘-coh2 : {a b : A} {c d : A'} (p : a == b) {q : g b == h c} (r : d == c)
      → (ap-! (f ∘ h) r |in-ctx (λ u → ap (f ∘ g) p ∙ ap f q ∙ u))
        ∙ ! (ap-∙∙!`∘`∘ f g h p q r)
        ==
        ! (ap-∙∙`∘`∘ f g h p q (! r))
  ap-∙∙!`∘`∘-coh2 idp {q} idp = idp

ap-∘-coh : ∀ {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) {p' : h a == h b} (α : ap h p == p')
  → ap-∘ f (g ∘ h) p ∙ ap (ap f) (ap-∘ g h p) ∙ ap (ap f) (α |in-ctx (ap g)) ∙ ∘-ap f g p'
    == ap-∘ (f ∘ g) h p ∙ ap (ap (f ∘ g)) α
ap-∘-coh f g h idp idp = idp

ap-∘-coh2 : ∀ {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) {p' : h a == h b} (α : ap h p == p')
  → ap-∘ f (g ∘ h) p ∙ ap (ap f) (ap-∘ g h p) ∙ ap (ap f) (α |in-ctx (ap g))
    == ap-∘ (f ∘ g) h p ∙ ap (ap (f ∘ g)) α ∙ ap-∘ f g p'
ap-∘-coh2 f g h idp idp = idp

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

∙□-i/-rewrite : ∀ {i} {A : Type i} {a b b' c : A} {p : a == b} {q q' : b == c}
  {r r' : a == b'} {s : b' == c}
  (α : (p , q =□ r , s)) {β β' : q' == q} (eqβ : β == β') {γ γ' : r == r'}
  (eqγ : γ == γ')
  → (α ∙□-i/ β / γ / == α ∙□-i/ β' / γ' /)
∙□-i/-rewrite α idp idp = idp

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
------------------------------------------------------------------------
-- Monotone functions
------------------------------------------------------------------------

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

module Partiality-algebra.Monotone where

open import Equality.Propositional.Cubical
open import Prelude hiding (⊥)

open import Bijection equality-with-J using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level.Closure equality-with-J

open import Partiality-algebra as PA hiding (id; _∘_)
import Partiality-algebra.Properties as PAP

-- Definition of monotone functions.

record [_⟶_]⊑
         {a₁ p₁ q₁} {A₁ : Type a₁} (P₁ : Partiality-algebra p₁ q₁ A₁)
         {a₂ p₂ q₂} {A₂ : Type a₂} (P₂ : Partiality-algebra p₂ q₂ A₂) :
         Type (p₁ ⊔ p₂ ⊔ q₁ ⊔ q₂) where
  private
    module P₁ = Partiality-algebra P₁
    module P₂ = Partiality-algebra P₂

  field
    function : P₁.T → P₂.T
    monotone : ∀ {x y} → x P₁.⊑ y → function x P₂.⊑ function y

open [_⟶_]⊑

-- Identity.

id⊑ : ∀ {a p q} {A : Type a} {P : Partiality-algebra p q A} →
      [ P ⟶ P ]⊑
function id⊑ = id
monotone id⊑ = id

-- Composition.

infixr 40 _∘⊑_

_∘⊑_ :
  ∀ {a₁ p₁ q₁} {A₁ : Type a₁} {P₁ : Partiality-algebra p₁ q₁ A₁}
    {a₂ p₂ q₂} {A₂ : Type a₂} {P₂ : Partiality-algebra p₂ q₂ A₂}
    {a₃ p₃ q₃} {A₃ : Type a₃} {P₃ : Partiality-algebra p₃ q₃ A₃} →
  [ P₂ ⟶ P₃ ]⊑ → [ P₁ ⟶ P₂ ]⊑ → [ P₁ ⟶ P₃ ]⊑
function (f ∘⊑ g) = function f ∘ function g
monotone (f ∘⊑ g) = monotone f ∘ monotone g

-- Equality characterisation lemma for monotone functions.

equality-characterisation-monotone :
  ∀ {a₁ p₁ q₁} {A₁ : Type a₁} {P₁ : Partiality-algebra p₁ q₁ A₁}
    {a₂ p₂ q₂} {A₂ : Type a₂} {P₂ : Partiality-algebra p₂ q₂ A₂}
    {f g : [ P₁ ⟶ P₂ ]⊑} →
  (∀ x → function f x ≡ function g x) ↔ f ≡ g
equality-characterisation-monotone {P₁ = P₁} {P₂ = P₂} {f} {g} =
  (∀ x → function f x ≡ function g x)                                   ↔⟨ Eq.extensionality-isomorphism ext ⟩

  function f ≡ function g                                               ↝⟨ ignore-propositional-component
                                                                             (implicit-Π-closure ext 1 λ _ →
                                                                              implicit-Π-closure ext 1 λ _ →
                                                                              Π-closure          ext 1 λ _ →
                                                                              P₂.⊑-propositional) ⟩
  _↔_.to rearrange f ≡ _↔_.to rearrange g                               ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ rearrange) ⟩□

  f ≡ g                                                                 □
  where
  module P₁ = Partiality-algebra P₁
  module P₂ = Partiality-algebra P₂

  rearrange :
    [ P₁ ⟶ P₂ ]⊑
      ↔
    ∃ λ (h : P₁.T → P₂.T) →
      ∀ {x y} → x P₁.⊑ y → h x P₂.⊑ h y
  rearrange = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ f → function f , monotone f
        ; from = uncurry λ f m → record { function = f; monotone = m }
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    }
    where
    open Partiality-algebra

-- Composition is associative.

∘⊑-assoc :
  ∀ {a₁ p₁ q₁} {A₁ : Type a₁} {P₁ : Partiality-algebra p₁ q₁ A₁}
    {a₂ p₂ q₂} {A₂ : Type a₂} {P₂ : Partiality-algebra p₂ q₂ A₂}
    {a₃ p₃ q₃} {A₃ : Type a₃} {P₃ : Partiality-algebra p₃ q₃ A₃}
    {a₄ p₄ q₄} {A₄ : Type a₄} {P₄ : Partiality-algebra p₄ q₄ A₄}
  (f : [ P₃ ⟶ P₄ ]⊑) (g : [ P₂ ⟶ P₃ ]⊑) {h : [ P₁ ⟶ P₂ ]⊑} →
  f ∘⊑ (g ∘⊑ h) ≡ (f ∘⊑ g) ∘⊑ h
∘⊑-assoc _ _ =
  _↔_.to equality-characterisation-monotone λ _ → refl

module _
  {a₁ p₁ q₁} {A₁ : Type a₁} {P₁ : Partiality-algebra p₁ q₁ A₁}
  {a₂ p₂ q₂} {A₂ : Type a₂} {P₂ : Partiality-algebra p₂ q₂ A₂} where

  private
    module P₁   = Partiality-algebra P₁
    module P₂   = Partiality-algebra P₂
    module PAP₁ = PAP P₁
    module PAP₂ = PAP P₂

  -- If a monotone function is applied to an increasing sequence,
  -- then the result is another increasing sequence.

  [_$_]-inc :
    [ P₁ ⟶ P₂ ]⊑ → P₁.Increasing-sequence → P₂.Increasing-sequence
  [ f $ s ]-inc = (λ n → function f (s P₁.[ n ]))
                , (λ n → monotone f (P₁.increasing s n))

  -- A lemma relating monotone functions and least upper bounds.

  ⨆$⊑$⨆ : (f : [ P₁ ⟶ P₂ ]⊑) →
          ∀ s → P₂.⨆ [ f $ s ]-inc P₂.⊑ function f (P₁.⨆ s)
  ⨆$⊑$⨆ f s = P₂.least-upper-bound _ _ λ n →

    [ f $ s ]-inc P₂.[ n ]  PAP₂.⊑⟨ monotone f (

        s P₁.[ n ]                    PAP₁.⊑⟨ P₁.upper-bound _ _ ⟩■
        P₁.⨆ s                        ■) ⟩■

    function f (P₁.⨆ s)     ■

ext: agda

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
-- Exercises for session 3
--
-- If unsure which exercises to do start with those marked with *
--
{-# OPTIONS --cubical --allow-unsolved-metas #-}
module ExerciseSession3 where

open import Part1
open import Part2
open import Part3
open import Part4
open import ExerciseSession1 hiding (B)

open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Nat
open import Cubical.Data.Int hiding (neg)

-- Exercise* 1: prove associativity of _++_ for FMSet.
-- (hint: mimic the proof of unitr-++)

-- Exercise 2: define the integers as a HIT with a pos and neg
-- constructor each taking a natural number as well as a path
-- constructor equating pos 0 and neg 0.

-- Exercise 3 (a little longer, but not very hard): prove that the
-- above definition of the integers is equal to the ones in
-- Cubical.Data.Int. Deduce that they form a set.

-- Exercise* 4: we can define the notion of a surjection as:
isSurjection : (A → B) → Type _
isSurjection {A = A} {B = B} f = (b : B) → ∃ A (λ a → f a ≡ b)

-- The exercise is now to:
--
-- a) prove that being a surjection is a proposition
--
-- b) prove that the inclusion ∣_∣ : A → ∥ A ∥ is surjective
--    (hint: use rec for ∥_∥)

-- Exercise* 5: define

intLoop : Int → ΩS¹
intLoop = {!!}

-- which given +n return loop^n and given -n returns loop^-n. Then
-- prove that:

windingIntLoop : (n : Int) → winding (intLoop n) ≡ n
windingIntLoop = {!!}

-- (The other direction is much more difficult and relies on the
-- encode-decode method. See Egbert's course on Friday!)

-- Exercise 6 (harder): the suspension of a type can be defined as

data Susp (A : Type ℓ) : Type ℓ where
  north : Susp A
  south : Susp A
  merid : (a : A) → north ≡ south

-- Prove that the circle is equal to the suspension of Bool
S¹≡SuspBool : S¹ ≡ Susp Bool
S¹≡SuspBool = {!!}

-- Hint: define maps back and forth and prove that they cancel.


text:
------------------------------------------------------------------------------
-- In the Agda standard library zero divides zero
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.FOTC.Data.Nat.Divisibility.ZeroDividesZero where

open import Data.Nat.Divisibility
open import Relation.Binary.PropositionalEquality

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

0∣0 : 0 ∣ 0
0∣0 = divides 0 refl

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Inductive.Examples.BinTree where

open import Inductive
open import Tuple

open import Data.Fin
open import Data.Product hiding (map)
open import Data.List hiding (map)
open import Data.Vec hiding (map)

BinTree : Set → Set
BinTree A = Inductive (([] , []) ∷ (((A ∷ []) , ([] ∷ ([] ∷ []))) ∷ []))

leaf : {A : Set} → BinTree A
leaf = construct zero [] []

node : {A : Set} → A → BinTree A → BinTree A → BinTree A
node a lt rt = construct (suc zero) (a ∷ []) ((λ _ → lt) ∷ ((λ _ → rt) ∷ []))

map : {A B : Set} → (A → B) → BinTree A → BinTree B
map f = rec (leaf ∷ ((λ a lt rlt rt rrt → node (f a) rlt rrt) ∷ []))

import Inductive.Examples.List as List

dfs : {A : Set} → BinTree A → List.List A
dfs = rec ( List.nil
          ∷ (λ a lt rlt rt rrt → List.cons a (rlt List.++ rrt))
          ∷ [])

max_stars_repo_name: mr-ohman/general-induction

max_issues_repo_name: mr-ohman/general-induction

max_forks_repo_name: mr-ohman/general-induction


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax Group | G

type
  * : 0-ary

term
  unit : * | ε
  add  : *  *  ->  * | _⊕_ l20
  neg  : *  ->  * | ⊖_ r40

theory
  (εU⊕ᴸ) a |> add (unit, a) = a
  (εU⊕ᴿ) a |> add (a, unit) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊖N⊕ᴸ) a |> add (neg (a), a) = unit
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = unit
-}

module Group.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import Group.Signature
open import Group.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution G:Syn
open import SOAS.Metatheory.SecondOrder.Equality G:Syn

private
  variable
    α β γ τ : *T
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ G) α Γ → (𝔐 ▷ G) α Γ → Set where
  εU⊕ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢       ε ⊕ 𝔞 ≋ₐ 𝔞
  εU⊕ᴿ : ⁅ * ⁆̣             ▹ ∅ ⊢       𝔞 ⊕ ε ≋ₐ 𝔞
  ⊕A   : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ⊕ 𝔟) ⊕ 𝔠 ≋ₐ 𝔞 ⊕ (𝔟 ⊕ 𝔠)
  ⊖N⊕ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢   (⊖ 𝔞) ⊕ 𝔞 ≋ₐ ε
  ⊖N⊕ᴿ : ⁅ * ⁆̣             ▹ ∅ ⊢   𝔞 ⊕ (⊖ 𝔞) ≋ₐ ε

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Issue561.Core where

postulate
  Char : Set

{-# BUILTIN CHAR Char #-}

open import Agda.Builtin.IO public

postulate
  return  : ∀ {a} {A : Set a} → A → IO A

{-# COMPILE GHC return = \_ _ -> return #-}
{-# COMPILE UHC return = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
{-# COMPILE JS return =
    function(u0) { return function(u1) { return function(x) { return function(cb) { cb(x); }; }; }; } #-}
{-# FOREIGN OCaml
  let ioReturn _ _ x world = Lwt.return x
  let ioBind _ _ _ _ x f world = Lwt.bind (x world) (fun x -> f x world)
#-}

{-# COMPILE OCaml return = ioReturn #-}

max_stars_repo_name: xekoukou/agda-ocaml

max_issues_repo_name: xekoukou/agda-ocaml

max_forks_repo_name: xekoukou/agda-ocaml


text:
module Logic.Base where

infix 60 ¬_
infix 30 _/\_
infix 20 _\/_

data True : Set where
  tt : True

data False : Set where

elim-False : {A : Set} -> False -> A
elim-False ()

data _/\_ (P Q : Set) : Set where
  /\-I : P -> Q -> P /\ Q

data _\/_ (P Q : Set) : Set where
  \/-IL : P -> P \/ Q
  \/-IR : Q -> P \/ Q

elimD-\/ : {P Q : Set}(C : P \/ Q -> Set) ->
	   ((p : P) -> C (\/-IL p)) ->
	   ((q : Q) -> C (\/-IR q)) ->
	   (pq : P \/ Q) -> C pq
elimD-\/ C left right (\/-IL p) = left p
elimD-\/ C left right (\/-IR q) = right q

elim-\/ : {P Q R : Set} -> (P -> R) -> (Q -> R) -> P \/ Q -> R
elim-\/ = elimD-\/ (\_ -> _)

¬_ : Set -> Set
¬ P = P -> False

data ∃ {A : Set}(P : A -> Set) : Set where
  ∃-I : (w : A) -> P w -> ∃ P

∏ : {A : Set}(P : A -> Set) -> Set
∏ {A} P = (x : A) -> P x

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Classes where

open import Cubical.Core.Everything

------------------------------------------------------------------------
-- Conversion typeclasses

-- | A typeclass to coerce values of A to some other type. The coercion used is
-- | only dependent on the input type, so the output type does not need to be inferable.
-- |
-- | Coersion should mainly be used for any case where there is only one
-- | unambiguous possible conversion that can happen to some object, such as
-- | the coersions of algebras to their carrier types.
record Coerce {a} (A : Type a) : Typeω where
  field
    b : Level
    Target : Type b
    coerce : A → Target

open Coerce {{...}} using (coerce)

-- | An operator synonym for the typeclass method `coerce`.
⟨_⟩ = coerce

instance
  -- Used for any case where sigma types are used to encode types with structure
  ΣCoerce : ∀ {ℓ ℓ′} {A : Type ℓ} {P : A → Type ℓ′} → Coerce (Σ A P)
  ΣCoerce = record { coerce = fst }

-- | A typeclass used to cast values of A to values of B. The cast performed is
-- | based on both the input and output types, so both need to be inferable.
record Cast {a b} (A : Type a) (B : Type b) : Type (ℓ-max a b) where
  field
    cast : A → B

open Cast {{...}}

-- | An operator synonym for the typeclass method `coerce`.
[_] = cast

------------------------------------------------------------------------
-- Homomorphism typeclasses

-- | A typeclass for function/equivalence types that respect
-- | some structure. The input types are different to allow for
-- | universe polymorphism.
record HomOperators {a b} (A : Type a) (B : Type b) ℓ
          : Type (ℓ-max (ℓ-max a b) (ℓ-suc ℓ)) where
  field
    _⟶ᴴ_ : A → B → Type ℓ
    _≃ᴴ_ : A → B → Type ℓ

open HomOperators {{...}} public


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.LawvereTheories where

-- Category of Lawvere Theories

open import Level

open import Categories.Category
open import Categories.Functor.Cartesian.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.Theory.Lawvere

LawvereTheories : (o ℓ e : Level) → Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
LawvereTheories o ℓ e = record
  { Obj = FiniteProduct o ℓ e
  ; _⇒_ = LT-Hom
  ; _≈_ = λ H₁ H₂ → F H₁ ≃ F H₂
  ; id = LT-id
  ; _∘_ = LT-∘
  ; assoc = λ { {f = f} {g} {h} → associator (F f) (F g) (F h)}
  ; sym-assoc = λ { {f = f} {g} {h} → sym-associator (F f) (F g) (F h)}
  ; identityˡ = unitorˡ
  ; identityʳ = unitorʳ
  ; identity² = unitor²
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = _ⓘₕ_
  }
  where open LT-Hom


text:
{-# OPTIONS --cubical --safe #-}

module Data.Bits.Order where

open import Data.Bits
open import Data.Bool
open import Level

infix 4 _≤ᴮ_ _<ᴮ_
_≤ᴮ_ _<ᴮ_ : Bits → Bits → Bool
[]    ≤ᴮ ys    = true
0∷ xs ≤ᴮ []    = false
0∷ xs ≤ᴮ 0∷ ys = xs ≤ᴮ ys
0∷ xs ≤ᴮ 1∷ ys = true
1∷ xs ≤ᴮ []    = false
1∷ xs ≤ᴮ 0∷ ys = false
1∷ xs ≤ᴮ 1∷ ys = xs ≤ᴮ ys

xs    <ᴮ []    = false
[]    <ᴮ 0∷ ys = true
0∷ xs <ᴮ 0∷ ys = xs <ᴮ ys
1∷ xs <ᴮ 0∷ ys = false
[]    <ᴮ 1∷ ys = true
0∷ xs <ᴮ 1∷ ys = true
1∷ xs <ᴮ 1∷ ys = xs <ᴮ ys

infix 4 _≤_ _<_
_≤_ _<_ : Bits → Bits → Type
xs ≤ ys = T (xs ≤ᴮ ys)
xs < ys = T (xs <ᴮ ys)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Empty.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Empty.Base

isProp⊥ : isProp ⊥
isProp⊥ ()

isContr⊥→A : ∀ {ℓ} {A : Type ℓ} → isContr (⊥ → A)
fst isContr⊥→A ()
snd isContr⊥→A f i ()

uninhabEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → (A → ⊥) → (B → ⊥) → A ≃ B
uninhabEquiv ¬a ¬b = isoToEquiv isom
  where
  open Iso
  isom : Iso _ _
  isom .fun a = rec (¬a a)
  isom .inv b = rec (¬b b)
  isom .rightInv b = rec (¬b b)
  isom .leftInv a = rec (¬a a)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import Base
open import Homotopy.PullbackDef

{- In this file we prove that if two diagrams are equivalent (there are
   equivalences between the types and the squares are commutative), then the
   natural map between the pullbacks is also an equivalence -}

module Homotopy.PullbackInvariantEquiv {i}
    (d d' : pullback-diag i) where

private
  pullback-to-pullback : ∀ {i} {A A' : Set i} (p : A ≡ A')
    {B B' : Set i} (q : B ≡ B') {C C' : Set i} (r : C ≡ C')
    {f : A → C} {f' : A' → C'}
    (s : (a : A) → f' ((transport _ p) a) ≡ transport _ r (f a))
    {g : B → C} {g' : B' → C'}
    (t : (b : B) → transport _ r (g b) ≡ g' ((transport _ q) b))
    → pullback (diag A , B , C , f , g) → pullback (diag A' , B' , C' , f' , g')
  pullback-to-pullback p q r s t (a , b , e) =
    (transport _ p a , transport _ q b , (s a ∘ (ap (transport _ r) e ∘ t b)))

  transport-pullback : ∀ {i} {A A' : Set i} (p : A ≡ A')
    {B B' : Set i} (q : B ≡ B') {C C' : Set i} (r : C ≡ C')
    {f : A → C} {f' : A' → C'} (s : f' ◯ (transport _ p) ≡ transport _ r ◯ f)
    {g : B → C} {g' : B' → C'} (t : transport _ r ◯ g ≡ g' ◯ (transport _ q))
    → transport pullback (pullback-diag-raw-eq p q r {f' = f'} s {g' = g'} t)
      ≡ pullback-to-pullback p q r (happly s) (happly t)
  transport-pullback refl refl refl refl refl =
    funext (λ r → ap (λ u → _ , _ , u)
                  (! (ap-id _) ∘ ! (refl-right-unit _)))

  transport-pullback-funext : ∀ {i} {A A' : Set i} (p : A ≡ A')
    {B B' : Set i} (q : B ≡ B') {C C' : Set i} (r : C ≡ C')
    {f : A → C} {f' : A' → C'}
    (s : (a : A) → f' ((transport _ p) a) ≡ transport _ r (f a))
    {g : B → C} {g' : B' → C'}
    (t : (b : B) → transport _ r (g b) ≡ g' ((transport _ q) b))
    → transport pullback (pullback-diag-raw-eq p q r {f' = f'} (funext s)
                                                     {g' = g'} (funext t))
      ≡ pullback-to-pullback p q r s t
  transport-pullback-funext p q r s t =
    transport-pullback p q r (funext s) (funext t)
    ∘ (ap (λ u → pullback-to-pullback p q r u (happly (funext t)))
           (happly-funext s)
    ∘ ap (λ u → pullback-to-pullback p q r s u) (happly-funext t))

  path-to-eq-ap : ∀ {i j} {A : Set i} (P : A → Set j) {x y : A} (p : x ≡ y)
    → π₁ (path-to-eq (ap P p)) ≡ transport P p
  path-to-eq-ap P refl = refl

open pullback-diag d
open pullback-diag d' renaming (A to A'; B to B'; C to C'; f to f'; g to g')

module PullbackInvariantEquiv (eqA : A ≃ A') (eqB : B ≃ B') (eqC : C ≃ C')
           (p : (a : A) → f' (eqA ☆ a) ≡ eqC ☆ (f a))
           (q : (b : B) → eqC ☆ (g b) ≡ g' (eqB ☆ b)) where

  private
    d≡d' : d ≡ d'
    d≡d' = pullback-diag-eq eqA eqB eqC p q

    pullback-equiv-pullback : pullback d ≃ pullback d'
    pullback-equiv-pullback = path-to-eq (ap pullback d≡d')

    h : (a : A) → f' ((transport (λ v → v) (eq-to-path eqA) a))
                  ≡ transport (λ v → v) (eq-to-path eqC) (f a)
    h a = ap f' (trans-id-eq-to-path eqA a)
          ∘ (p a ∘ (! (trans-id-eq-to-path eqC (f a))))

    h' : (b : B) → transport (λ v → v) (eq-to-path eqC) (g b)
                   ≡ g' ((transport (λ v → v) (eq-to-path eqB) b))
    h' b = trans-id-eq-to-path eqC (g b)
           ∘ (q b ∘ ap g' (! (trans-id-eq-to-path eqB b)))

  pullback-to-equiv-pullback : pullback d → pullback d'
  pullback-to-equiv-pullback (a , b , e) =
    ((eqA ☆ a) , (eqB ☆ b) , (p a ∘ (ap (π₁ eqC) e ∘ q b)))

  private
    pb-to-pb-equal-pb-to-equiv-pb : (x : pullback d)
      → pullback-to-pullback (eq-to-path eqA) (eq-to-path eqB) (eq-to-path eqC)
                             h h' x
        ≡ pullback-to-equiv-pullback x
    pb-to-pb-equal-pb-to-equiv-pb (a , b , h) =
      pullback-eq d' (trans-id-eq-to-path eqA a)
        (trans-id-eq-to-path eqB b)
        (concat-assoc (ap f' (trans-id (eq-to-path eqA) a ∘ _) ∘ _) _ _
         ∘ (concat-assoc (ap f' (trans-id (eq-to-path eqA) a ∘ _)) _ _
         ∘ whisker-left (ap f' (trans-id (eq-to-path eqA) a ∘ _))
        (concat-assoc (p a) _ _
         ∘ whisker-left (p a)
        (whisker-left (! (trans-id (eq-to-path eqC) (f a) ∘ _))
          (concat-assoc (ap (transport (λ v → v) (eq-to-path eqC)) h) _ _
           ∘ whisker-left (ap (transport (λ v → v) (eq-to-path eqC)) h)
          (concat-assoc (trans-id (eq-to-path eqC) (g b) ∘ _) _ _
           ∘ whisker-left (trans-id (eq-to-path eqC) (g b) ∘ _)
          (concat-assoc (q b) _ _
           ∘ (whisker-left (q b)
          (concat-ap g' (! (trans-id (eq-to-path eqB) b ∘ _)) _
           ∘ ap (ap g')
             (opposite-left-inverse (trans-id (eq-to-path eqB) b ∘ _)))
           ∘ refl-right-unit (q b)))))
         ∘ move!-right-on-left (trans-id (eq-to-path eqC) (f a) ∘ _) _ _
         (! (concat-assoc (ap (transport (λ v → v) (eq-to-path eqC)) h)
                (trans-id (eq-to-path eqC) (g b) ∘ _) _)
         ∘ ((whisker-right (q b)
              (homotopy-naturality (transport (λ v → v) (eq-to-path eqC))
                 (π₁ eqC)
                 (λ t → trans-id (eq-to-path eqC) t
                        ∘ ap (λ u → π₁ u t) (eq-to-path-right-inverse eqC))
                 h))
           ∘ concat-assoc (trans-id (eq-to-path eqC) (f a) ∘ _) (ap (π₁ eqC) h)
               (q b)))))))

    pb-equiv-pb-equal-pb-to-equiv-pb
      : π₁ pullback-equiv-pullback ≡ pullback-to-equiv-pullback
    pb-equiv-pb-equal-pb-to-equiv-pb =
        path-to-eq-ap pullback d≡d'
        ∘ (transport-pullback-funext (eq-to-path eqA) (eq-to-path eqB)
                                     (eq-to-path eqC) h h'
        ∘ funext pb-to-pb-equal-pb-to-equiv-pb)

  abstract
    pullback-invariant-is-equiv : is-equiv pullback-to-equiv-pullback
    pullback-invariant-is-equiv =
      transport is-equiv pb-equiv-pb-equal-pb-to-equiv-pb
                (π₂ pullback-equiv-pullback)

  pullback-invariant-equiv : pullback d ≃ pullback d'
  pullback-invariant-equiv =
    (pullback-to-equiv-pullback , pullback-invariant-is-equiv)

open PullbackInvariantEquiv public

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Formalization.FunctionML where

import      Lvl
open import Numeral.Finite
open import Numeral.Natural
open import Type{Lvl.𝟎}

data Value : ℕ → Type
data Expression : ℕ → Type

data Value where
  const : ∀{n} → ℕ → Value n
  var : ∀{n} → 𝕟(n) → Value n
  y-combinator : ∀{n} → Value n
  func : ∀{n} → Value(𝐒 n) → Value n

data Expression where
  val : ∀{n} → Value n → Expression n
  apply : ∀{n} → Expression n → Expression n

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Containers core
------------------------------------------------------------------------

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

module Data.Container.Core where

open import Level
open import Data.Product as Prod using (Σ-syntax)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (_↔_; module Inverse)
open import Relation.Unary using (Pred; _⊆_)

-- Definition of Containers

infix 5 _▷_
record Container (s p : Level) : Set (suc (s ⊔ p)) where
  constructor _▷_
  field
    Shape    : Set s
    Position : Shape → Set p
open Container public

-- The semantics ("extension") of a container.

⟦_⟧ : ∀ {s p ℓ} → Container s p → Set ℓ → Set (s ⊔ p ⊔ ℓ)
⟦ S ▷ P ⟧ X = Σ[ s ∈ S ] (P s → X)

-- The extension is a functor

map : ∀ {s p x y} {C : Container s p} {X : Set x} {Y : Set y} →
      (X → Y) → ⟦ C ⟧ X → ⟦ C ⟧ Y
map f = Prod.map₂ (f ∘_)

-- Representation of container morphisms.

record _⇒_ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂)
           : Set (s₁ ⊔ s₂ ⊔ p₁ ⊔ p₂) where
  constructor _▷_
  field
    shape    : Shape C₁ → Shape C₂
    position : ∀ {s} → Position C₂ (shape s) → Position C₁ s

  ⟪_⟫ : ∀ {x} {X : Set x} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X
  ⟪_⟫ = Prod.map shape (_∘′ position)

open _⇒_ public

-- Linear container morphisms

record _⊸_ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂)
  : Set (s₁ ⊔ s₂ ⊔ p₁ ⊔ p₂) where
  field
    shape⊸    : Shape C₁ → Shape C₂
    position⊸ : ∀ {s} → Position C₂ (shape⊸ s) ↔ Position C₁ s

  morphism : C₁ ⇒ C₂
  morphism = record
    { shape    = shape⊸
    ; position = _⟨$⟩_ (Inverse.to position⊸)
    }

  ⟪_⟫⊸ : ∀ {x} {X : Set x} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X
  ⟪_⟫⊸ = ⟪ morphism ⟫

open _⊸_ public using (shape⊸; position⊸; ⟪_⟫⊸)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of N-ary products
------------------------------------------------------------------------

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

module Data.Product.N-ary.Categorical where

open import Agda.Builtin.Nat
open import Data.Product hiding (map)
open import Data.Product.N-ary
open import Function

open import Category.Functor
open import Category.Applicative
open import Category.Monad

------------------------------------------------------------------------
-- Functor and applicative

functor : ∀ {ℓ} n → RawFunctor {ℓ} (_^ n)
functor n = record { _<$>_ = λ f → map f n }

applicative : ∀ {ℓ} n → RawApplicative {ℓ} (_^ n)
applicative n = record
  { pure = replicate n
  ; _⊛_  = ap n
  }

------------------------------------------------------------------------
-- Get access to other monadic functions

module _ {f F} (App : RawApplicative {f} F) where

  open RawApplicative App

  sequenceA : ∀ {n A} → F A ^ n → F (A ^ n)
  sequenceA {0}    _          = pure _
  sequenceA {1}    fa         = fa
  sequenceA {2+ n} (fa , fas) = _,_ <$> fa ⊛ sequenceA fas

  mapA : ∀ {n a} {A : Set a} {B} → (A → F B) → A ^ n → F (B ^ n)
  mapA f = sequenceA ∘ map f _

  forA : ∀ {n a} {A : Set a} {B} → A ^ n → (A → F B) → F (B ^ n)
  forA = flip mapA

module _ {m M} (Mon : RawMonad {m} M) where

  private App = RawMonad.rawIApplicative Mon

  sequenceM : ∀ {n A} → M A ^ n → M (A ^ n)
  sequenceM = sequenceA App

  mapM : ∀ {n a} {A : Set a} {B} → (A → M B) → A ^ n → M (B ^ n)
  mapM = mapA App

  forM : ∀ {n a} {A : Set a} {B} → A ^ n → (A → M B) → M (B ^ n)
  forM = forA App


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

open import Base
open import Homotopy.Connected

module Homotopy.Extensions.ProductPushoutToProductToConnected
  {i j} {A A′ B B′ : Set i} (f : A → A′) (g : B → B′) (P : A′ → B′ → Set j)
  {n₁ n₂} ⦃ P-is-trunc : ∀ a′ b′ → is-truncated (n₁ +2+ n₂) (P a′ b′) ⦄
  (f-is-conn : has-connected-fibers n₁ f)
  (g-is-conn : has-connected-fibers n₂ g)
  (left* :  ∀ a′ b → P a′ (g b))
  (right* : ∀ a b′ → P (f a) b′)
  (glue* :  ∀ a b → left* (f a) b ≡ right* a (g b))
  where

  open import Homotopy.Truncation
  open import Homotopy.Extensions.ProductPushoutToProductToConnected.Magic

  {-
    -- The pushout diagram you should have in your mind.

    connected-extend-diag : pushout-diag i
    connected-extend-diag = record
      { A = A′ × B
      ; B = A × B′
      ; C = A × B
      ; f = λ{(a , b) → f a , b}
      ; g = λ{(a , b) → a , g b}
      }
  -}

  private
    -- The first part: The extension for a fixed [a] is n₁-truncated.
    extension₁ : ∀ a′ → Set (max i j)
    extension₁ a′ = extension g (P a′) (left* a′)

    extend-magic₁ : ∀ a′ → is-truncated n₁ (extension₁ a′)
    extend-magic₁ a′ = extension-is-truncated
      g g-is-conn (P a′) ⦃ P-is-trunc a′ ⦄ (left* a′)

    -- The second part: The extension of extensions is contractible.
    extension₂ : Set (max i j)
    extension₂ = extension f extension₁ (λ a → right* a , glue* a)

    abstract
      extend-magic₂ : is-truncated ⟨-2⟩ extension₂
      extend-magic₂ = extension-is-truncated
        f f-is-conn extension₁ ⦃ extend-magic₁ ⦄ (λ a → right* a , glue* a)

      extend-magic₃ : extension₂
      extend-magic₃ = π₁ extend-magic₂

  abstract
    -- Get the buried function.
    connected-extend : ∀ a′ b′ → P a′ b′
    connected-extend a′ b′ = π₁ (π₁ extend-magic₃ a′) b′

    -- β rules
    connected-extend-β-left : ∀ a′ b → connected-extend a′ (g b) ≡ left* a′ b
    connected-extend-β-left a′ b = ! $ π₂ (π₁ extend-magic₃ a′) b

    connected-extend-β-right : ∀ a b′ → connected-extend (f a) b′ ≡ right* a b′
    connected-extend-β-right a b′ = ! $ happly (base-path (π₂ extend-magic₃ a)) b′

    private
      -- This is a combination of 2~3 basic rules.
      lemma₁ : ∀ a (k : ∀ b → P (f a) (g b))
        {l₁ l₂ : ∀ b′ → P (f a) b′} (p : l₁ ≡ l₂) (q : ∀ b → k b ≡ l₁ (g b)) c
        → transport (λ l → ∀ b → k b ≡ l (g b)) p q c
        ≡ q c ∘ happly p (g c)
      lemma₁ a k refl q c = ! $ refl-right-unit _

    connected-extend-triangle : ∀ a b
      → connected-extend-β-left (f a) b ∘ glue* a b
      ≡ connected-extend-β-right a (g b)
    connected-extend-triangle a b =
      ! (π₂ (π₁ extend-magic₃ (f a)) b) ∘ glue* a b
        ≡⟨ ap (λ p → ! p ∘ glue* a b) $ ! $ happly (fiber-path (π₂ extend-magic₃ a)) b ⟩
      ! (transport (λ l → ∀ b → left* (f a) b ≡ l (g b)) (base-path (π₂ extend-magic₃ a)) (glue* a) b) ∘ glue* a b
        ≡⟨ ap (λ p → ! p ∘ glue* a b)
              $ lemma₁ a (left* (f a)) (base-path (π₂ extend-magic₃ a)) (glue* a) b ⟩
      ! (glue* a b ∘ happly (base-path (π₂ extend-magic₃ a)) (g b)) ∘ glue* a b
        ≡⟨ ap (λ p → p ∘ glue* a b) $ opposite-concat (glue* a b) (happly (base-path (π₂ extend-magic₃ a)) (g b)) ⟩
      (connected-extend-β-right a (g b) ∘ ! (glue* a b)) ∘ glue* a b
        ≡⟨ concat-assoc (connected-extend-β-right a (g b)) (! (glue* a b)) (glue* a b) ⟩
      connected-extend-β-right a (g b) ∘ ! (glue* a b) ∘ glue* a b
        ≡⟨ ap (λ p → connected-extend-β-right a (g b) ∘ p) $ opposite-left-inverse (glue* a b) ⟩
      connected-extend-β-right a (g b) ∘ refl
        ≡⟨ refl-right-unit _ ⟩∎
      connected-extend-β-right a (g b)
        ∎


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Tarski-style semantics with contexts as concrete worlds, and glueing for □ only.
-- Gentzen-style syntax.

module BasicIS4.Semantics.TarskiGluedGentzen where

open import BasicIS4.Syntax.Common public
open import Common.Semantics public

-- Intuitionistic Tarski models.

record Model : Set₁ where
  infix 3 _⊩ᵅ_ _[⊢]_ _[⊢⋆]_
  field
    -- Forcing for atomic propositions; monotonic.
    _⊩ᵅ_   : Cx Ty → Atom → Set
    mono⊩ᵅ : ∀ {P Γ Γ′} → Γ ⊆ Γ′ → Γ ⊩ᵅ P → Γ′ ⊩ᵅ P

    -- Gentzen-style syntax representation; monotonic.
    _[⊢]_     : Cx Ty → Ty → Set
    _[⊢⋆]_    : Cx Ty → Cx Ty → Set
    mono[⊢]   : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ [⊢] A → Γ′ [⊢] A
    [var]      : ∀ {A Γ}    → A ∈ Γ → Γ [⊢] A
    [lam]      : ∀ {A B Γ}  → Γ , A [⊢] B → Γ [⊢] A ▻ B
    [app]      : ∀ {A B Γ}  → Γ [⊢] A ▻ B → Γ [⊢] A → Γ [⊢] B
    [multibox] : ∀ {A Δ Γ}  → Γ [⊢⋆] □⋆ Δ → □⋆ Δ [⊢] A → Γ [⊢] □ A
    [down]     : ∀ {A Γ}    → Γ [⊢] □ A → Γ [⊢] A
    [pair]     : ∀ {A B Γ}  → Γ [⊢] A → Γ [⊢] B → Γ [⊢] A ∧ B
    [fst]      : ∀ {A B Γ}  → Γ [⊢] A ∧ B → Γ [⊢] A
    [snd]      : ∀ {A B Γ}  → Γ [⊢] A ∧ B → Γ [⊢] B
    [unit]     : ∀ {Γ}      → Γ [⊢] ⊤

    -- TODO: Workarounds for Agda bug #2143.
    top[⊢⋆] : ∀ {Γ}     → (Γ [⊢⋆] ∅) ≡ 𝟙
    pop[⊢⋆] : ∀ {Ξ A Γ} → (Γ [⊢⋆] Ξ , A) ≡ (Γ [⊢⋆] Ξ × Γ [⊢] A)

  infix 3 _[⊢]⋆_
  _[⊢]⋆_ : Cx Ty → Cx Ty → Set
  Γ [⊢]⋆ ∅     = 𝟙
  Γ [⊢]⋆ Ξ , A = Γ [⊢]⋆ Ξ × Γ [⊢] A

  [⊢⋆]→[⊢]⋆ : ∀ {Ξ Γ} → Γ [⊢⋆] Ξ → Γ [⊢]⋆ Ξ
  [⊢⋆]→[⊢]⋆ {∅}     {Γ} ts = ∙
  [⊢⋆]→[⊢]⋆ {Ξ , A} {Γ} ts rewrite pop[⊢⋆] {Ξ} {A} {Γ} = [⊢⋆]→[⊢]⋆ (π₁ ts) , π₂ ts

  [⊢]⋆→[⊢⋆] : ∀ {Ξ Γ} → Γ [⊢]⋆ Ξ → Γ [⊢⋆] Ξ
  [⊢]⋆→[⊢⋆] {∅}     {Γ} ∙        rewrite top[⊢⋆] {Γ}         = ∙
  [⊢]⋆→[⊢⋆] {Ξ , A} {Γ} (ts , t) rewrite pop[⊢⋆] {Ξ} {A} {Γ} = [⊢]⋆→[⊢⋆] ts , t

open Model {{…}} public

-- Forcing in a particular model.

module _ {{_ : Model}} where
  infix 3 _⊩_
  _⊩_ : Cx Ty → Ty → Set
  Γ ⊩ α P   = Γ ⊩ᵅ P
  Γ ⊩ A ▻ B = ∀ {Γ′} → Γ ⊆ Γ′ → Γ′ ⊩ A → Γ′ ⊩ B
  Γ ⊩ □ A   = ∀ {Γ′} → Γ ⊆ Γ′ → Glue (Γ′ [⊢] □ A) (Γ′ ⊩ A)
  Γ ⊩ A ∧ B = Γ ⊩ A × Γ ⊩ B
  Γ ⊩ ⊤    = 𝟙

  infix 3 _⊩⋆_
  _⊩⋆_ : Cx Ty → Cx Ty → Set
  Γ ⊩⋆ ∅     = 𝟙
  Γ ⊩⋆ Ξ , A = Γ ⊩⋆ Ξ × Γ ⊩ A

-- Monotonicity with respect to context inclusion.

module _ {{_ : Model}} where
  mono⊩ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊩ A → Γ′ ⊩ A
  mono⊩ {α P}   η s = mono⊩ᵅ η s
  mono⊩ {A ▻ B} η s = λ η′ → s (trans⊆ η η′)
  mono⊩ {□ A}   η s = λ η′ → s (trans⊆ η η′)
  mono⊩ {A ∧ B} η s = mono⊩ {A} η (π₁ s) , mono⊩ {B} η (π₂ s)
  mono⊩ {⊤}    η s = ∙

  mono⊩⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊩⋆ Ξ → Γ′ ⊩⋆ Ξ
  mono⊩⋆ {∅}     η ∙        = ∙
  mono⊩⋆ {Ξ , A} η (ts , t) = mono⊩⋆ {Ξ} η ts , mono⊩ {A} η t

-- Shorthand for variables.

module _ {{_ : Model}} where
  [v₀] : ∀ {A Γ} → Γ , A [⊢] A
  [v₀] = [var] i₀

  [v₁] : ∀ {A B Γ} → Γ , A , B [⊢] A
  [v₁] = [var] i₁

  [v₂] : ∀ {A B C Γ} → Γ , A , B , C [⊢] A
  [v₂] = [var] i₂

-- Useful theorems in functional form.

module _ {{_ : Model}} where
  [multicut] : ∀ {Ξ A Γ} → Γ [⊢]⋆ Ξ → Ξ [⊢] A → Γ [⊢] A
  [multicut] {∅}     ∙        u = mono[⊢] bot⊆ u
  [multicut] {Ξ , B} (ts , t) u = [app] ([multicut] ts ([lam] u)) t

  [dist] : ∀ {A B Γ} → Γ [⊢] □ (A ▻ B) → Γ [⊢] □ A → Γ [⊢] □ B
  [dist] t u = [multibox] ([⊢]⋆→[⊢⋆] ((∙ , t) , u)) ([app] ([down] [v₁]) ([down] [v₀]))

  [up] : ∀ {A Γ} → Γ [⊢] □ A → Γ [⊢] □ □ A
  [up] t = [multibox] ([⊢]⋆→[⊢⋆] ((∙ , t))) [v₀]

-- Additional useful equipment.

module _ {{_ : Model}} where

  _⟪$⟫_ : ∀ {A B Γ} → Γ ⊩ A ▻ B → Γ ⊩ A → Γ ⊩ B
  s ⟪$⟫ a = s refl⊆ a

  ⟪K⟫ : ∀ {A B Γ} → Γ ⊩ A → Γ ⊩ B ▻ A
  ⟪K⟫ {A} a η = K (mono⊩ {A} η a)

  ⟪S⟫ : ∀ {A B C Γ} → Γ ⊩ A ▻ B ▻ C → Γ ⊩ A ▻ B → Γ ⊩ A → Γ ⊩ C
  ⟪S⟫ {A} {B} {C} s₁ s₂ a = _⟪$⟫_ {B} {C} (_⟪$⟫_ {A} {B ▻ C} s₁ a) (_⟪$⟫_ {A} {B} s₂ a)

  ⟪S⟫′ : ∀ {A B C Γ} → Γ ⊩ A ▻ B ▻ C → Γ ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ {A} {B} {C} s₁ η s₂ η′ a = let s₁′ = mono⊩ {A ▻ B ▻ C} (trans⊆ η η′) s₁
                                      s₂′ = mono⊩ {A ▻ B} η′ s₂
                                  in  ⟪S⟫ {A} {B} {C} s₁′ s₂′ a

  _⟪D⟫_ : ∀ {A B Γ} → Γ ⊩ □ (A ▻ B) → Γ ⊩ □ A → Γ ⊩ □ B
  _⟪D⟫_ {A} {B} s₁ s₂ η = let t ⅋ s₁′ = s₁ η
                              u ⅋ a   = s₂ η
                          in  [dist] t u ⅋ _⟪$⟫_ {A} {B} s₁′ a

  _⟪D⟫′_ : ∀ {A B Γ} → Γ ⊩ □ (A ▻ B) → Γ ⊩ □ A ▻ □ B
  _⟪D⟫′_ {A} {B} s₁ η = _⟪D⟫_ (mono⊩ {□ (A ▻ B)} η s₁)

  ⟪↑⟫ : ∀ {A Γ} → Γ ⊩ □ A → Γ ⊩ □ □ A
  ⟪↑⟫ s η = [up] (syn (s η)) ⅋ λ η′ → s (trans⊆ η η′)

  ⟪↓⟫ : ∀ {A Γ} → Γ ⊩ □ A → Γ ⊩ A
  ⟪↓⟫ s = sem (s refl⊆)

  _⟪,⟫′_ : ∀ {A B Γ} → Γ ⊩ A → Γ ⊩ B ▻ A ∧ B
  _⟪,⟫′_ {A} {B} a η = _,_ (mono⊩ {A} η a)

-- Forcing in a particular world of a particular model, for sequents.

module _ {{_ : Model}} where
  infix 3 _⊩_⇒_
  _⊩_⇒_ : Cx Ty → Cx Ty → Ty → Set
  w ⊩ Γ ⇒ A = w ⊩⋆ Γ → w ⊩ A

  infix 3 _⊩_⇒⋆_
  _⊩_⇒⋆_ : Cx Ty → Cx Ty → Cx Ty → Set
  w ⊩ Γ ⇒⋆ Ξ = w ⊩⋆ Γ → w ⊩⋆ Ξ

-- Entailment, or forcing in all models, for sequents.

infix 3 _⊨_
_⊨_ : Cx Ty → Ty → Set₁
Γ ⊨ A = ∀ {{_ : Model}} {w : Cx Ty} → w ⊩ Γ ⇒ A

infix 3 _⊨⋆_
_⊨⋆_ : Cx Ty → Cx Ty → Set₁
Γ ⊨⋆ Ξ = ∀ {{_ : Model}} {w : Cx Ty} → w ⊩ Γ ⇒⋆ Ξ

-- Additional useful equipment, for sequents.

module _ {{_ : Model}} where
  lookup : ∀ {A Γ w} → A ∈ Γ → w ⊩ Γ ⇒ A
  lookup top     (γ , a) = a
  lookup (pop i) (γ , b) = lookup i γ

  _⟦$⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B
  _⟦$⟧_ {A} {B} s₁ s₂ γ = _⟪$⟫_ {A} {B} (s₁ γ) (s₂ γ)

  ⟦K⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B ▻ A
  ⟦K⟧ {A} {B} a γ = ⟪K⟫ {A} {B} (a γ)

  ⟦S⟧ : ∀ {A B C Γ w} → w ⊩ Γ ⇒ A ▻ B ▻ C → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ C
  ⟦S⟧ {A} {B} {C} s₁ s₂ a γ = ⟪S⟫ {A} {B} {C} (s₁ γ) (s₂ γ) (a γ)

  _⟦D⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ □ (A ▻ B) → w ⊩ Γ ⇒ □ A → w ⊩ Γ ⇒ □ B
  (s₁ ⟦D⟧ s₂) γ = (s₁ γ) ⟪D⟫ (s₂ γ)

  ⟦↑⟧ : ∀ {A Γ w} → w ⊩ Γ ⇒ □ A → w ⊩ Γ ⇒ □ □ A
  ⟦↑⟧ s γ = ⟪↑⟫ (s γ)

  ⟦↓⟧ : ∀ {A Γ w} → w ⊩ Γ ⇒ □ A → w ⊩ Γ ⇒ A
  ⟦↓⟧ s γ = ⟪↓⟫ (s γ)

  _⟦,⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B → w ⊩ Γ ⇒ A ∧ B
  (a ⟦,⟧ b) γ = a γ , b γ

  ⟦π₁⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ A
  ⟦π₁⟧ s γ = π₁ (s γ)

  ⟦π₂⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ B
  ⟦π₂⟧ s γ = π₂ (s γ)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Category where

open import Prelude

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

record Category {ℓ ℓ′}
                (𝒪 : Set ℓ) (_▹_ : 𝒪 → 𝒪 → Set ℓ′)
              : Set (ℓ ⊔ ℓ′) where
  field
    idₓ    : ∀ {x} → x ▹ x

    _⋄_    : ∀ {x y z} → y ▹ x → z ▹ y → z ▹ x

    lid⋄   : ∀ {x y} → (f : y ▹ x)
                     → idₓ ⋄ f ≡ f

    rid⋄   : ∀ {x y} → (f : y ▹ x)
                     → f ⋄ idₓ ≡ f

    assoc⋄ : ∀ {x y z a} → (h : a ▹ z) (g : z ▹ y) (f : y ▹ x)
                         → (f ⋄ g) ⋄ h ≡ f ⋄ (g ⋄ h)

𝗦𝗲𝘁 : (ℓ : Level) → Category (Set ℓ) Π
𝗦𝗲𝘁 ℓ =
  record
    { idₓ    = id
    ; _⋄_    = _∘_
    ; lid⋄   = λ f → refl
    ; rid⋄   = λ f → refl
    ; assoc⋄ = λ h g f → refl
    }

𝗦𝗲𝘁₀ : Category (Set ℓ₀) Π
𝗦𝗲𝘁₀ = 𝗦𝗲𝘁 ℓ₀

record Functor {ℓ₁ ℓ₁′ ℓ₂ ℓ₂′}
               {𝒪₁ : Set ℓ₁} {_▹₁_ : 𝒪₁ → 𝒪₁ → Set ℓ₁′}
               {𝒪₂ : Set ℓ₂} {_▹₂_ : 𝒪₂ → 𝒪₂ → Set ℓ₂′}
               (𝗖 : Category 𝒪₁ _▹₁_) (𝗗 : Category 𝒪₂ _▹₂_)
             : Set (ℓ₁ ⊔ ℓ₁′ ⊔ ℓ₂ ⊔ ℓ₂′) where
  private
    module C = Category 𝗖
    module D = Category 𝗗

  field
    Fₓ  : 𝒪₁ → 𝒪₂

    F   : ∀ {x y} → y ▹₁ x → Fₓ y ▹₂ Fₓ x

    idF : ∀ {x} → F (C.idₓ {x = x}) ≡ D.idₓ

    F⋄  : ∀ {x y z} → (g : z ▹₁ y) (f : y ▹₁ x)
                    → F (f C.⋄ g) ≡ F f D.⋄ F g

record NaturalTransformation {ℓ₁ ℓ₁′ ℓ₂ ℓ₂′}
                             {𝒪₁ : Set ℓ₁} {_▹₁_ : 𝒪₁ → 𝒪₁ → Set ℓ₁′}
                             {𝒪₂ : Set ℓ₂} {_▹₂_ : 𝒪₂ → 𝒪₂ → Set ℓ₂′}
                             {𝗖 : Category 𝒪₁ _▹₁_} {𝗗 : Category 𝒪₂ _▹₂_}
                             (𝗙 𝗚 : Functor 𝗖 𝗗)
                           : Set (ℓ₁ ⊔ ℓ₁′ ⊔ ℓ₂ ⊔ ℓ₂′) where
  private
    open module D = Category 𝗗 using (_⋄_)
    open module F = Functor 𝗙 using (Fₓ ; F)
    open module G = Functor 𝗚 using () renaming (Fₓ to Gₓ ; F to G)

  field
    N    : ∀ {x} → Fₓ x ▹₂ Gₓ x

    natN : ∀ {x y} → (f : y ▹₁ x)
                   → (N ⋄ F f) ≡ (G f ⋄ N)

Opposite : ∀ {ℓ ℓ′} → {𝒪 : Set ℓ} {_▹_ : 𝒪 → 𝒪 → Set ℓ′}
                    → Category 𝒪 _▹_
                    → Category 𝒪 (flip _▹_)
Opposite 𝗖 =
  record
    { idₓ    = C.idₓ
    ; _⋄_    = flip C._⋄_
    ; lid⋄   = C.rid⋄
    ; rid⋄   = C.lid⋄
    ; assoc⋄ = λ f g h → C.assoc⋄ h g f ⁻¹
    }
  where
    module C = Category 𝗖

Presheaf : ∀ ℓ {ℓ′ ℓ″} → {𝒪 : Set ℓ′} {_▹_ : 𝒪 → 𝒪 → Set ℓ″}
                       → (𝗖 : Category 𝒪 _▹_)
                       → Set _
Presheaf ℓ 𝗖 = Functor (Opposite 𝗖) (𝗦𝗲𝘁 ℓ)

Presheaf₀ : ∀ {ℓ ℓ′} → {𝒪 : Set ℓ} {_▹_ : 𝒪 → 𝒪 → Set ℓ′}
                     → (𝗖 : Category 𝒪 _▹_)
                     → Set _
Presheaf₀ 𝗖 = Presheaf ℓ₀ 𝗖

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
------------------------------------------------------------------------
-- Utility methods
------------------------------------------------------------------------
-- Should be pushed to the standard library

{-# OPTIONS --allow-exec #-}

open import Algebra.Core using (Op₂)
open import Level using (Level)
open import Data.Bool.Base using (T; Bool; if_then_else_; not; _∨_)
open import Data.Char.Properties using (_≟_)
open import Data.String using (String; _++_; lines; toList)
open import Data.Nat.Base using (ℕ; suc)
open import Data.Vec.Base using (Vec; []; _∷_)
open import Data.Vec.Functional using (Vector)
open import Data.Vec.Recursive using (_^_; toVec)
open import Data.Product using (_,_)
open import Data.Float.Base using (Float; _≤ᵇ_)
open import Data.List.Base using ([]; _∷_)
open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties using (infix?)
open import Data.Unit.Base using (⊤; tt)
open import Relation.Nullary using (does)
open import Relation.Binary.Core using (Rel)

module Vehicle.Utils where

_⇒_ : Op₂ Bool
x ⇒ y = not x ∨ y

_≤_ :  Rel Float _
x ≤ y = T (x ≤ᵇ y)

_⊆_ : String → String → Bool
s ⊆ t = does (infix? _≟_ (toList s) (toList t))

max_stars_repo_name: wenkokke/vehicle

max_issues_repo_name: wenkokke/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Word.Properties where

open import Agda.Builtin.Word
open import Agda.Builtin.Equality

primitive

  primWord64ToNatInjective : ∀ a b → primWord64ToNat a ≡ primWord64ToNat b → a ≡ b

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
{-

This file contains:

- Definition of set quotients

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.SetQuotients.Base where

open import Cubical.Core.Primitives

-- Set quotients as a higher inductive type:
data _/_ {ℓ ℓ'} (A : Type ℓ) (R : A → A → Type ℓ') : Type (ℓ-max ℓ ℓ') where
  [_] : (a : A) → A / R
  eq/ : (a b : A) → (r : R a b) → [ a ] ≡ [ b ]
  squash/ : (x y : A / R) → (p q : x ≡ y) → p ≡ q


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution {{eqrel : EqRelSet}} where

open import Definition.Untyped hiding (_∷_)
open import Definition.Typed
open import Definition.LogicalRelation

open import Tools.Nat
open import Tools.Product
open import Tools.Unit

private
  variable
    k ℓ m n l : Nat
    Γ : Con Term n

-- The validity judgements:
-- We consider expressions that satisfy these judgments valid

mutual
  -- Validity of contexts
  data ⊩ᵛ_ : Con Term n → Set where
    ε : ⊩ᵛ ε
    _∙_ : ∀ {A l} ([Γ] : ⊩ᵛ Γ) → Γ ⊩ᵛ⟨ l ⟩ A / [Γ]
        → ⊩ᵛ Γ ∙ A

  -- Validity of types
  _⊩ᵛ⟨_⟩_/_ : {n : Nat} (Γ : Con Term n) (l : TypeLevel) (A : Term n) → ⊩ᵛ Γ → Set
  _⊩ᵛ⟨_⟩_/_ {n} Γ l A [Γ] =
    ∀ {k : Nat} {Δ : Con Term k} {σ : Subst k n} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
    → Σ (Δ ⊩⟨ l ⟩ subst σ A) (λ [Aσ]
      → ∀ {σ′} ([σ′] : Δ ⊩ˢ σ′ ∷ Γ / [Γ] / ⊢Δ)
        ([σ≡σ′] : Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ])
      → Δ ⊩⟨ l ⟩ subst σ A ≡ subst σ′ A / [Aσ])

  -- Logical relation for substitutions from a valid context
  _⊩ˢ_∷_/_/_ : (Δ : Con Term n) (σ : Subst n m) (Γ : Con Term m) ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
             → Set
  Δ ⊩ˢ σ ∷ .ε        / ε  / ⊢Δ                = ⊤
  Δ ⊩ˢ σ ∷ .(Γ ∙ A) / (_∙_ {Γ = Γ} {A} {l} [Γ] [A]) / ⊢Δ =
    Σ (Δ ⊩ˢ tail σ ∷ Γ / [Γ] / ⊢Δ) λ [tailσ] →
      (Δ ⊩⟨ l ⟩ head σ ∷ subst (tail σ) A / proj₁ ([A] ⊢Δ [tailσ]))

  -- Logical relation for equality of substitutions from a valid context
  _⊩ˢ_≡_∷_/_/_/_ : (Δ : Con Term n) (σ σ′ : Subst n m) (Γ : Con Term m) ([Γ] : ⊩ᵛ Γ)
                    (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ) → Set
  --Δ ⊩ˢ σ ≡ σ′ ∷ Γ / x / y / z = {!   !}
  Δ ⊩ˢ σ ≡ σ′ ∷ .ε       / ε       / ⊢Δ              / [σ] = ⊤
  Δ ⊩ˢ σ ≡ σ′ ∷ .(Γ ∙ A) / (_∙_ {Γ = Γ} {A} {l} [Γ] [A]) / ⊢Δ / [σ] =
    (Δ ⊩ˢ tail σ ≡ tail σ′ ∷ Γ / [Γ] / ⊢Δ / proj₁ [σ]) ×
    (Δ ⊩⟨ l ⟩ head σ ≡ head σ′ ∷ subst (tail σ) A / proj₁ ([A] ⊢Δ (proj₁ [σ])))

-- Validity of terms
_⊩ᵛ⟨_⟩_∷_/_/_ : (Γ : Con Term n) (l : TypeLevel) (t A : Term n) ([Γ] : ⊩ᵛ Γ)
                 ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ]) → Set
Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A] =
  ∀ {k} {Δ : Con Term k} {σ} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ) →
  Σ (Δ ⊩⟨ l ⟩ subst σ t ∷ subst σ A / proj₁ ([A] ⊢Δ [σ])) λ [tσ] →
  ∀ {σ′} → Δ ⊩ˢ σ′ ∷ Γ / [Γ] / ⊢Δ → Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ]
    → Δ ⊩⟨ l ⟩ subst σ t ≡ subst σ′ t ∷ subst σ A / proj₁ ([A] ⊢Δ [σ])

-- Validity of type equality
_⊩ᵛ⟨_⟩_≡_/_/_ : (Γ : Con Term n) (l : TypeLevel) (A B : Term n) ([Γ] : ⊩ᵛ Γ)
                ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ]) → Set
Γ ⊩ᵛ⟨ l ⟩ A ≡ B / [Γ] / [A] =
  ∀ {k} {Δ : Con Term k} {σ} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
  → Δ ⊩⟨ l ⟩ subst σ A ≡ subst σ B / proj₁ ([A] ⊢Δ [σ])

-- Validity of term equality
_⊩ᵛ⟨_⟩_≡_∷_/_/_ : (Γ : Con Term n) (l : TypeLevel) (t u A : Term n) ([Γ] : ⊩ᵛ Γ)
                    ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ]) → Set
Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A / [Γ] / [A] =
  ∀ {k} {Δ : Con Term k} {σ} → (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
          → Δ ⊩⟨ l ⟩ subst σ t ≡ subst σ u ∷ subst σ A / proj₁ ([A] ⊢Δ [σ])

-- Valid term equality with validity of its type and terms
record [_⊩ᵛ⟨_⟩_≡_∷_/_] (Γ : Con Term n) (l : TypeLevel)
                       (t u A : Term n) ([Γ] : ⊩ᵛ Γ) : Set where
  constructor modelsTermEq
  field
    [A]   : Γ ⊩ᵛ⟨ l ⟩ A / [Γ]
    [t]   : Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A]
    [u]   : Γ ⊩ᵛ⟨ l ⟩ u ∷ A / [Γ] / [A]
    [t≡u] : Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A / [Γ] / [A]

-- Validity of reduction of terms
_⊩ᵛ_⇒_∷_/_ : (Γ : Con Term n) (t u A : Term n) ([Γ] : ⊩ᵛ Γ) → Set
Γ ⊩ᵛ t ⇒ u ∷ A / [Γ] = ∀ {k} {Δ : Con Term k} {σ} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
                       → Δ ⊢ subst σ t ⇒ subst σ u ∷ subst σ A

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
module Extra where

open import Prelude

fromTo : Nat -> List Nat
fromTo n = f n
  where
    f : Nat -> List Nat
    f 0 = []
    f (suc i) = n - i ∷ f i

downFrom : Nat -> List Nat
downFrom 0 = []
downFrom (suc n) = (suc n) ∷ downFrom n

fromTo' : Nat -> List Nat
fromTo' = f []
  where
    f : List Nat -> Nat -> List Nat
    f xs 0 = xs
    f xs (suc x) = seq xs (f ( suc x ∷ xs ) x)

downFrom' : Nat -> List Nat
downFrom' n = f [] n
  where
    f : List Nat -> Nat -> List Nat
    f xs 0 = xs
    f xs (suc x) = seq xs (f ((n - x) ∷ xs) x)

blumblumshub : Nat -> (m : Nat) -> {{ nz : NonZero m }} -> Nat
blumblumshub xn M = natMod M (xn ^ 2)

downFromBbs' : Nat -> Nat -> List Nat
downFromBbs' seed = f seed []
  where
  f : Nat -> List Nat -> Nat -> List Nat
  f _ acc 0       = acc
  f x acc (suc l) = seq acc $ f (blumblumshub x M) ( x ∷ acc ) l
    where
      M M17 M31 : Nat
      M           = M17 * M31
      M17         = 2971
      M31         = 4111

fromToBbs : Nat -> Nat -> List Nat
fromToBbs _ 0 = []
fromToBbs xi (suc n) = xi ∷ fromToBbs (blumblumshub xi m) n
  where
    p = 2971
    q = 4111
    m = p * q

max_stars_repo_name: agda/agda-ocaml


text:
open import Data.Product using ( ∃ ; _×_ )
open import FRP.LTL.RSet.Core using ( RSet )
open import FRP.LTL.Time using ( _≤_ )

module FRP.LTL.RSet.Future where

◇ : RSet → RSet
◇ A t = ∃ λ u → (t ≤ u) × A u

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
{-# OPTIONS --sized-types #-}
module SList.Order.Properties {A  : Set}(_≤_ : A → A → Set) where

open import List.Sorted _≤_
open import Size
open import SList
open import SList.Order _≤_

lemma-slist-sorted : {ι : Size}{x : A}{xs : SList A {ι}} → x *≤ xs → Sorted (unsize A xs) → Sorted (unsize A (x ∙ xs))
lemma-slist-sorted {x = x} genx nils = singls x
lemma-slist-sorted (gecx x≤y genx) (singls y) = conss x≤y (singls y)
lemma-slist-sorted (gecx x≤y x*≤zys ) syzys = conss x≤y syzys

lemma-sorted⊕ : {ι : Size}{x : A}{xs : SList A {ι}} → xs ≤* x → Sorted (unsize A xs) → Sorted (unsize A (_⊕_ A xs (x ∙ snil)))
lemma-sorted⊕ {x = x} {xs = snil} _ nils = singls x
lemma-sorted⊕ {x = x} {xs = y ∙ snil} (lecx y≤x _) (singls .y)  = conss y≤x (singls x)
lemma-sorted⊕ {xs = y ∙ (z ∙ ys)} (lecx y≤x zys≤*x) (conss y≤z szys) = conss y≤z (lemma-sorted⊕ zys≤*x szys)

lemma-⊕≤* : {ι : Size}{x t : A}{xs : SList A {ι}} → x ≤ t → xs ≤* t → (_⊕_ A xs (x ∙ snil)) ≤* t
lemma-⊕≤* x≤t lenx = lecx x≤t lenx
lemma-⊕≤* x≤t (lecx y≤t ys≤*t) = lecx y≤t (lemma-⊕≤* x≤t ys≤*t)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Andreas, 2016-06-17, issue #2018 reported by Nisse

-- Shadowing a module parameter with a record parameter
-- caused the record parameter to be renamed

-- {-# OPTIONS -v tc.rec:20 #-}

module _ {A : Set} where

data D {A : Set} : Set where
  c : D

record R {A : Set} : Set where
  constructor rc

postulate
  B : Set

test-c : (B : Set) → D {A = B}
test-c B = c {A = B}

test-rc : (B : Set) → R {A = B}
test-rc B = rc {A = B}

-- Error WAS:
-- Function does not accept argument {A = _}
-- when checking that {A = B} is a valid argument to a function of
-- type {A₁ : Set} → Set

-- Should work now.

max_forks_repo_name: Agda-zh/agda


text:
module Cats.Category.Constructions.CCC where

open import Level

open import Cats.Category.Base
open import Cats.Category.Constructions.Exponential using
  (HasExponentials)
open import Cats.Category.Constructions.Product using
  (HasFiniteProducts)

record IsCCC {lo la l≈} (Cat : Category lo la l≈)
  : Set (lo ⊔ la ⊔ l≈) where
  field
    {{hasFiniteProducts}} : HasFiniteProducts Cat
    {{hasExponentials}} : HasExponentials Cat

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module PLRTree.Heap.Correctness {A : Set}(_≤_ : A → A → Set) where

open import BTree.Heap _≤_
open import PLRTree {A}
open import PLRTree.Heap _≤_ renaming (Heap to Heap')

lemma-heap'-heap : {t : PLRTree} → Heap' t → Heap (forget t)
lemma-heap'-heap leaf = leaf
lemma-heap'-heap (node {t} {x} (lf≤* .x) (lf≤* .x) _ _) = single x
lemma-heap'-heap (node {t} {x} (lf≤* .x) (nd≤* x≤y  _ _) _ h'r) = right x≤y (lemma-heap'-heap h'r)
lemma-heap'-heap (node {t} {x} (nd≤* x≤y _ _) (lf≤* .x) h'l _) = left x≤y (lemma-heap'-heap h'l)
lemma-heap'-heap (node (nd≤* x≤y _ _) (nd≤* x≤y' _ _) h'l h'r) = both x≤y x≤y' (lemma-heap'-heap h'l) (lemma-heap'-heap h'r)


text:
-- Andreas, 2018-10-16, runtime erasure
--
-- Should not be able to extract erased constructor field.

open import Agda.Builtin.Nat

data Vec (A : Set) : Nat → Set where
  [] : Vec A zero
  _∷_ : {@0 n : Nat} (x : A) (xs : Vec A n) → Vec A (suc n)

length : ∀{A} {@0 n} (x : Vec A n) → Nat
length [] = zero
length (_∷_ {n} _ _) = suc n

-- Expected error:
--
-- Variable n is declared erased, so it cannot be used here
-- when checking that the expression n has type Nat

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT
open import cohomology.FunctionOver

{- The cofiber space of [winl : X → X ∨ Y] is equivalent to [Y],
 - and the cofiber space of [winr : Y → X ∨ Y] is equivalent to [X]. -}

module cohomology.WedgeCofiber where

module WedgeCofiber {i} (X Y : Ptd i) where

  module CofWinl where

    module Into = CofiberRec {f = winl} (snd Y) (projr X Y) (λ _ → idp)

    into = Into.f

    out : fst Y → Cofiber (winl {X = X} {Y = Y})
    out = cfcod ∘ winr

    out-into : (κ : Cofiber (winl {X = X} {Y = Y})) → out (into κ) == κ
    out-into = Cofiber-elim
      (! (cfglue (snd X) ∙ ap cfcod wglue))
      (Wedge-elim
        (λ x → ! (cfglue (snd X) ∙ ap cfcod wglue) ∙ cfglue x)
        (λ y → idp)
        (↓-='-from-square $
          (lemma (cfglue (snd X)) (ap cfcod wglue)
           ∙h⊡ (ap-∘ out (projr X Y) wglue ∙ ap (ap out) (Projr.glue-β X Y))
                ∙v⊡ bl-square (ap cfcod wglue))))
      (λ x → ↓-∘=idf-from-square out into $
        ! (∙-unit-r _) ∙h⊡
          ap (ap out) (Into.glue-β x) ∙v⊡
           hid-square {p = (! (cfglue' winl (snd X) ∙ ap cfcod wglue))}
           ⊡v connection {q = cfglue x})
      where
      lemma : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : y == z)
        → ! (p ∙ q) ∙ p == ! q
      lemma idp idp = idp

    ⊙path : ⊙Cof (⊙winl {X = X} {Y = Y}) == Y
    ⊙path = ⊙ua (⊙≃-in (equiv into out (λ _ → idp) out-into) idp)

    cfcod-over : ⊙cfcod' ⊙winl == ⊙projr X Y
                 [ (λ U → fst (X ⊙∨ Y ⊙→ U)) ↓ ⊙path ]
    cfcod-over = codomain-over-⊙equiv (⊙cfcod' ⊙winl) _
                 ▹ pair= idp (∙-unit-r _ ∙ ap-! into (cfglue (snd X))
                              ∙ ap ! (Into.glue-β (snd X)))

  module CofWinr where

    module Into = CofiberRec {f = winr} (snd X) (projl X Y) (λ _ → idp)

    into = Into.f

    out : fst X → Cofiber (winr {X = X} {Y = Y})
    out = cfcod ∘ winl

    out-into : ∀ κ → out (into κ) == κ
    out-into = Cofiber-elim
      (ap cfcod wglue ∙ ! (cfglue (snd Y)))
      (Wedge-elim
        (λ x → idp)
        (λ y → (ap cfcod wglue ∙ ! (cfglue (snd Y))) ∙ cfglue y)
        (↓-='-from-square $
          (ap-∘ out (projl X Y) wglue ∙ ap (ap out) (Projl.glue-β X Y)) ∙v⊡
             connection
           ⊡h∙ ! (lemma (ap (cfcod' winr) wglue) (cfglue (snd Y)))))
      (λ y → ↓-∘=idf-from-square out into $
        ! (∙-unit-r _) ∙h⊡
          ap (ap out) (Into.glue-β y) ∙v⊡
            hid-square {p = (ap (cfcod' winr) wglue ∙ ! (cfglue (snd Y)))}
            ⊡v connection {q = cfglue y})
      where
      lemma : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : z == y)
        → (p ∙ ! q) ∙ q == p
      lemma idp idp = idp

    ⊙path : ⊙Cof ⊙winr == X
    ⊙path = ⊙ua (⊙≃-in (equiv into out (λ _ → idp) out-into) idp)

    cfcod-over : ⊙cfcod' ⊙winr == ⊙projl X Y
                 [ (λ U → fst (X ⊙∨ Y ⊙→ U)) ↓ ⊙path ]
    cfcod-over = codomain-over-⊙equiv (⊙cfcod' ⊙winr) _
                 ▹ pair= idp lemma
      where
      lemma : ap into (ap cfcod (! (! wglue)) ∙ ! (cfglue (snd Y))) ∙ idp
           == idp
      lemma =
        ap into (ap cfcod (! (! wglue)) ∙ ! (cfglue (snd Y))) ∙ idp
          =⟨ ∙-unit-r _ ⟩
        ap into (ap cfcod (! (! wglue)) ∙ ! (cfglue (snd Y)))
          =⟨ !-! wglue
             |in-ctx (λ w → ap into (ap cfcod w ∙ ! (cfglue (snd Y)))) ⟩
        ap into (ap cfcod wglue ∙ ! (cfglue (snd Y)))
          =⟨ ap-∙ into (ap cfcod wglue) (! (cfglue (snd Y))) ⟩
        ap into (ap cfcod wglue) ∙ ap into (! (cfglue (snd Y)))
          =⟨ ∘-ap into cfcod wglue
             |in-ctx (_∙ ap into (! (cfglue (snd Y)))) ⟩
        ap (projl X Y) wglue ∙ ap into (! (cfglue (snd Y)))
          =⟨ Projl.glue-β X Y
             |in-ctx (_∙ ap into (! (cfglue (snd Y)))) ⟩
        ap into (! (cfglue (snd Y)))
          =⟨ ap-! into (cfglue (snd Y)) ⟩
        ! (ap into (cfglue (snd Y)))
          =⟨ ap ! (Into.glue-β (snd Y)) ⟩
        idp ∎

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda