text:
------------------------------------------------------------------------
-- Lists
------------------------------------------------------------------------

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

open import Equality

module List
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Prelude

open import Bijection eq as Bijection using (_↔_)
open Derived-definitions-and-properties eq
open import Equality.Decision-procedures eq
import Equivalence eq as Eq
open import Function-universe eq hiding (_∘_)
open import H-level eq as H-level
open import H-level.Closure eq
open import Monad eq hiding (map)
open import Nat eq
open import Nat.Solver eq

private
  variable
    a ℓ      : Level
    A B C    : Type a
    x y      : A
    f        : A → B
    n        : ℕ
    xs ys zs : List A
    ns       : List ℕ

------------------------------------------------------------------------
-- Some functions

-- The tail of a list. Returns [] if the list is empty.

tail : List A → List A
tail []       = []
tail (_ ∷ xs) = xs

-- The function take n returns the first n elements of a list (or the
-- entire list, if the list does not contain n elements).

take : ℕ → List A → List A
take zero    xs       = []
take (suc n) (x ∷ xs) = x ∷ take n xs
take (suc n) xs@[]    = xs

-- The function drop n removes the first n elements from a list (or
-- all elements, if the list does not contain n elements).

drop : ℕ → List A → List A
drop zero    xs       = xs
drop (suc n) (x ∷ xs) = drop n xs
drop (suc n) xs@[]    = xs

-- Right fold.

foldr : (A → B → B) → B → List A → B
foldr _⊕_ ε []       = ε
foldr _⊕_ ε (x ∷ xs) = x ⊕ foldr _⊕_ ε xs

-- Left fold.

foldl : (B → A → B) → B → List A → B
foldl _⊕_ ε []       = ε
foldl _⊕_ ε (x ∷ xs) = foldl _⊕_ (ε ⊕ x) xs

-- The length of a list.

length : List A → ℕ
length = foldr (const suc) 0

-- The sum of all the elements in a list of natural numbers.

sum : List ℕ → ℕ
sum = foldr _+_ 0

-- Appends two lists.

infixr 5 _++_

_++_ : List A → List A → List A
xs ++ ys = foldr _∷_ ys xs

-- Maps a function over a list.

map : (A → B) → List A → List B
map f = foldr (λ x ys → f x ∷ ys) []

-- Concatenates a list of lists.

concat : List (List A) → List A
concat = foldr _++_ []

-- "Zips" two lists, using the given function to combine elementsw.

zip-with : (A → B → C) → List A → List B → List C
zip-with f []       _        = []
zip-with f _        []       = []
zip-with f (x ∷ xs) (y ∷ ys) = f x y ∷ zip-with f xs ys

-- "Zips" two lists.

zip : List A → List B → List (A × B)
zip = zip-with _,_

-- Reverses a list.

reverse : List A → List A
reverse = foldl (λ xs x → x ∷ xs) []

-- Replicates the given value the given number of times.

replicate : ℕ → A → List A
replicate zero    x = []
replicate (suc n) x = x ∷ replicate n x

-- A filter function.

filter : (A → Bool) → List A → List A
filter p = foldr (λ x xs → if p x then x ∷ xs else xs) []

-- Finds the element at the given position.

index : (xs : List A) → Fin (length xs) → A
index []       ()
index (x ∷ xs) fzero    = x
index (x ∷ xs) (fsuc i) = index xs i

-- A lookup function.

lookup : (A → A → Bool) → A → List (A × B) → Maybe B
lookup _≟_ x []             = nothing
lookup _≟_ x ((y , z) ∷ ps) =
  if x ≟ y then just z else lookup _≟_ x ps

-- The list nats-< consists of the first n natural numbers in
-- strictly descending order.

nats-< : ℕ → List ℕ
nats-< zero    = []
nats-< (suc n) = n ∷ nats-< n

-- A list that includes every tail of the given list (including the
-- list itself) exactly once. Longer tails precede shorter ones.

tails : List A → List (List A)
tails []           = [] ∷ []
tails xxs@(_ ∷ xs) = xxs ∷ tails xs

------------------------------------------------------------------------
-- Some properties

-- If you take the first n elements from xs and append what you get if
-- you drop the first n elements from xs, then you get xs (even if n
-- is larger than the length of xs).

take++drop : ∀ n → take n xs ++ drop n xs ≡ xs
take++drop               zero    = refl _
take++drop {xs = []}     (suc n) = refl _
take++drop {xs = x ∷ xs} (suc n) = cong (x ∷_) (take++drop n)

-- The map function commutes with take n.

map-take : map f (take n xs) ≡ take n (map f xs)
map-take {n = zero}                = refl _
map-take {n = suc n} {xs = []}     = refl _
map-take {n = suc n} {xs = x ∷ xs} = cong (_ ∷_) map-take

-- The map function commutes with drop n.

map-drop : ∀ n → map f (drop n xs) ≡ drop n (map f xs)
map-drop               zero    = refl _
map-drop {xs = []}     (suc n) = refl _
map-drop {xs = x ∷ xs} (suc n) = map-drop n

-- The function foldr _∷_ [] is pointwise equal to the identity
-- function.

foldr-∷-[] : (xs : List A) → foldr _∷_ [] xs ≡ xs
foldr-∷-[] []       = refl _
foldr-∷-[] (x ∷ xs) = cong (x ∷_) (foldr-∷-[] xs)

-- The empty list is a right identity for the append function.

++-right-identity : (xs : List A) → xs ++ [] ≡ xs
++-right-identity []       = refl _
++-right-identity (x ∷ xs) = cong (x ∷_) (++-right-identity xs)

-- The append function is associative.

++-associative : (xs ys zs : List A) →
                 xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
++-associative []       ys zs = refl _
++-associative (x ∷ xs) ys zs = cong (x ∷_) (++-associative xs ys zs)

-- The map function commutes with _++_.

map-++ : (f : A → B) (xs ys : List A) →
         map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++ f []       ys = refl _
map-++ f (x ∷ xs) ys = cong (f x ∷_) (map-++ f xs ys)

-- The concat function commutes with _++_.

concat-++ : (xss yss : List (List A)) →
            concat (xss ++ yss) ≡ concat xss ++ concat yss
concat-++ []         yss = refl _
concat-++ (xs ∷ xss) yss =
  concat ((xs ∷ xss) ++ yss)        ≡⟨⟩
  xs ++ concat (xss ++ yss)         ≡⟨ cong (xs ++_) (concat-++ xss yss) ⟩
  xs ++ (concat xss ++ concat yss)  ≡⟨ ++-associative xs _ _ ⟩
  (xs ++ concat xss) ++ concat yss  ≡⟨ refl _ ⟩∎
  concat (xs ∷ xss) ++ concat yss   ∎

-- A lemma relating foldr and _++_.

foldr-++ :
  {c : A → B → B} {n : B} →
  ∀ xs → foldr c n (xs ++ ys) ≡ foldr c (foldr c n ys) xs
foldr-++                           []       = refl _
foldr-++ {ys = ys} {c = c} {n = n} (x ∷ xs) =
  foldr c n (x ∷ xs ++ ys)         ≡⟨⟩
  c x (foldr c n (xs ++ ys))       ≡⟨ cong (c x) (foldr-++ xs) ⟩
  c x (foldr c (foldr c n ys) xs)  ≡⟨⟩
  foldr c (foldr c n ys) (x ∷ xs)  ∎

-- A fusion lemma for foldr and map.

foldr∘map :
  (_⊕_ : B → C → C) (ε : C) (f : A → B) (xs : List A) →
  (foldr _⊕_ ε ∘ map f) xs ≡ foldr (_⊕_ ∘ f) ε xs
foldr∘map _⊕_ ε f []       = ε ∎
foldr∘map _⊕_ ε f (x ∷ xs) = cong (f x ⊕_) (foldr∘map _⊕_ ε f xs)

-- A fusion lemma for length and map.

length∘map :
  (f : A → B) (xs : List A) →
  (length ∘ map f) xs ≡ length xs
length∘map = foldr∘map _ _

-- A lemma relating index, map and length∘map.

index∘map :
  ∀ xs {i} →
  index (map f xs) i ≡
  f (index xs (subst Fin (length∘map f xs) i))
index∘map {f = f} (x ∷ xs) {i} =
  index (f x ∷ map f xs) i                                  ≡⟨ lemma i ⟩
  f (index (x ∷ xs) (subst (λ n → ⊤ ⊎ Fin n) p i))          ≡⟨⟩
  f (index (x ∷ xs) (subst (Fin ∘ suc) p i))                ≡⟨ cong (f ∘ index (_ ∷ xs)) (subst-∘ Fin suc _) ⟩
  f (index (x ∷ xs) (subst Fin (cong suc p) i))             ≡⟨⟩
  f (index (x ∷ xs) (subst Fin (length∘map f (x ∷ xs)) i))  ∎
  where
  p = length∘map f xs

  lemma :
    ∀ i →
    index (f x ∷ map f xs) i ≡
    f (index (x ∷ xs) (subst (λ n → ⊤ ⊎ Fin n) p i))
  lemma fzero =
    index (f x ∷ map f xs) fzero                          ≡⟨⟩
    f x                                                   ≡⟨⟩
    f (index (x ∷ xs) fzero)                              ≡⟨⟩
    f (index (x ∷ xs) (inj₁ (subst (λ _ → ⊤) p tt)))      ≡⟨ cong (f ∘ index (_ ∷ xs)) $ sym $ push-subst-inj₁ _ Fin ⟩∎
    f (index (x ∷ xs) (subst (λ n → ⊤ ⊎ Fin n) p fzero))  ∎
  lemma (fsuc i) =
    index (f x ∷ map f xs) (fsuc i)                          ≡⟨⟩
    index (map f xs) i                                       ≡⟨ index∘map xs ⟩
    f (index xs (subst Fin p i))                             ≡⟨⟩
    f (index (x ∷ xs) (fsuc (subst Fin p i)))                ≡⟨ cong (f ∘ index (_ ∷ xs)) $ sym $ push-subst-inj₂ _ Fin ⟩∎
    f (index (x ∷ xs) (subst (λ n → ⊤ ⊎ Fin n) p (fsuc i)))  ∎

-- The length function is homomorphic with respect to _++_/_+_.

length-++ : ∀ xs → length (xs ++ ys) ≡ length xs + length ys
length-++ []       = refl _
length-++ (_ ∷ xs) = cong suc (length-++ xs)

-- The sum function is homomorphic with respect to _++_/_+_.

sum-++ : ∀ ms → sum (ms ++ ns) ≡ sum ms + sum ns
sum-++           []       = refl _
sum-++ {ns = ns} (m ∷ ms) =
  sum (m ∷ ms ++ ns)     ≡⟨⟩
  m + sum (ms ++ ns)     ≡⟨ cong (m +_) $ sum-++ ms ⟩
  m + (sum ms + sum ns)  ≡⟨ +-assoc m ⟩
  (m + sum ms) + sum ns  ≡⟨⟩
  sum (m ∷ ms) + sum ns  ∎

-- Some lemmas related to reverse.

++-reverse : ∀ xs → reverse xs ++ ys ≡ foldl (flip _∷_) ys xs
++-reverse xs = lemma xs
  where
  lemma :
    ∀ xs →
    foldl (flip _∷_) ys xs ++ zs ≡
    foldl (flip _∷_) (ys ++ zs) xs
  lemma                     []       = refl _
  lemma {ys = ys} {zs = zs} (x ∷ xs) =
    foldl (flip _∷_) ys (x ∷ xs) ++ zs    ≡⟨⟩
    foldl (flip _∷_) (x ∷ ys) xs ++ zs    ≡⟨ lemma xs ⟩
    foldl (flip _∷_) (x ∷ ys ++ zs) xs    ≡⟨⟩
    foldl (flip _∷_) (ys ++ zs) (x ∷ xs)  ∎

reverse-∷ : ∀ xs → reverse (x ∷ xs) ≡ reverse xs ++ x ∷ []
reverse-∷ {x = x} xs =
  reverse (x ∷ xs)              ≡⟨⟩
  foldl (flip _∷_) (x ∷ []) xs  ≡⟨ sym $ ++-reverse xs ⟩∎
  reverse xs ++ x ∷ []          ∎

reverse-++ : ∀ xs → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++ {ys = ys} [] =
  reverse ys        ≡⟨ sym $ ++-right-identity _ ⟩∎
  reverse ys ++ []  ∎
reverse-++ {ys = ys} (x ∷ xs) =
  reverse (x ∷ xs ++ ys)                ≡⟨ reverse-∷ (xs ++ _) ⟩
  reverse (xs ++ ys) ++ x ∷ []          ≡⟨ cong (_++ _) $ reverse-++ xs ⟩
  (reverse ys ++ reverse xs) ++ x ∷ []  ≡⟨ sym $ ++-associative (reverse ys) _ _ ⟩
  reverse ys ++ (reverse xs ++ x ∷ [])  ≡⟨ cong (reverse ys ++_) $ sym $ reverse-∷ xs ⟩∎
  reverse ys ++ reverse (x ∷ xs)        ∎

reverse-reverse : (xs : List A) → reverse (reverse xs) ≡ xs
reverse-reverse []       = refl _
reverse-reverse (x ∷ xs) =
  reverse (reverse (x ∷ xs))                ≡⟨ cong reverse (reverse-∷ xs) ⟩
  reverse (reverse xs ++ x ∷ [])            ≡⟨ reverse-++ (reverse xs) ⟩
  reverse (x ∷ []) ++ reverse (reverse xs)  ≡⟨⟩
  x ∷ reverse (reverse xs)                  ≡⟨ cong (x ∷_) (reverse-reverse xs) ⟩∎
  x ∷ xs                                    ∎

map-reverse : ∀ xs → map f (reverse xs) ≡ reverse (map f xs)
map-reverse         []       = refl _
map-reverse {f = f} (x ∷ xs) =
  map f (reverse (x ∷ xs))        ≡⟨ cong (map f) $ reverse-∷ xs ⟩
  map f (reverse xs ++ x ∷ [])    ≡⟨ map-++ _ (reverse xs) _ ⟩
  map f (reverse xs) ++ f x ∷ []  ≡⟨ cong (_++ _) $ map-reverse xs ⟩
  reverse (map f xs) ++ f x ∷ []  ≡⟨ sym $ reverse-∷ (map f xs) ⟩
  reverse (f x ∷ map f xs)        ≡⟨⟩
  reverse (map f (x ∷ xs))        ∎

foldr-reverse :
  {c : A → B → B} {n : B} →
  ∀ xs → foldr c n (reverse xs) ≡ foldl (flip c) n xs
foldr-reverse                 []       = refl _
foldr-reverse {c = c} {n = n} (x ∷ xs) =
  foldr c n (reverse (x ∷ xs))      ≡⟨ cong (foldr c n) (reverse-++ {ys = xs} (x ∷ [])) ⟩
  foldr c n (reverse xs ++ x ∷ [])  ≡⟨ foldr-++ (reverse xs) ⟩
  foldr c (c x n) (reverse xs)      ≡⟨ foldr-reverse xs ⟩
  foldl (flip c) (c x n) xs         ≡⟨⟩
  foldl (flip c) n (x ∷ xs)         ∎

foldl-reverse :
  {c : B → A → B} {n : B} →
  ∀ xs → foldl c n (reverse xs) ≡ foldr (flip c) n xs
foldl-reverse {c = c} {n = n} xs =
  foldl c n (reverse xs)                   ≡⟨ sym (foldr-reverse (reverse xs)) ⟩
  foldr (flip c) n (reverse (reverse xs))  ≡⟨ cong (foldr (flip c) n) (reverse-reverse xs) ⟩∎
  foldr (flip c) n xs                      ∎

length-reverse : (xs : List A) → length (reverse xs) ≡ length xs
length-reverse []       = refl _
length-reverse (x ∷ xs) =
  length (reverse (x ∷ xs))      ≡⟨ cong length (reverse-∷ xs) ⟩
  length (reverse xs ++ x ∷ [])  ≡⟨ length-++ (reverse xs) ⟩
  length (reverse xs) + 1        ≡⟨ cong (_+ 1) (length-reverse xs) ⟩
  length xs + 1                  ≡⟨ +-comm (length xs) ⟩∎
  length (x ∷ xs)                ∎

sum-reverse : ∀ ns → sum (reverse ns) ≡ sum ns
sum-reverse []       = refl _
sum-reverse (n ∷ ns) =
  sum (reverse (n ∷ ns))           ≡⟨ cong sum (reverse-∷ ns) ⟩
  sum (reverse ns ++ n ∷ [])       ≡⟨ sum-++ (reverse ns) ⟩
  sum (reverse ns) + sum (n ∷ [])  ≡⟨ cong₂ _+_ (sum-reverse ns) +-right-identity ⟩
  sum ns + n                       ≡⟨ +-comm (sum ns) ⟩∎
  sum (n ∷ ns)                     ∎

-- The functions filter and map commute (kind of).

filter∘map :
  (p : B → Bool) (f : A → B) (xs : List A) →
  (filter p ∘ map f) xs ≡ (map f ∘ filter (p ∘ f)) xs
filter∘map p f []       = refl _
filter∘map p f (x ∷ xs) with p (f x)
... | true  = cong (_ ∷_) (filter∘map p f xs)
... | false = filter∘map p f xs

-- The length of replicate n x is n.

length-replicate : ∀ n → length (replicate n x) ≡ n
length-replicate         zero    = refl _
length-replicate {x = x} (suc n) =
  length (replicate (suc n) x)  ≡⟨⟩
  suc (length (replicate n x))  ≡⟨ cong suc $ length-replicate n ⟩∎
  suc n                         ∎

-- The sum of replicate m n is m * n.

sum-replicate : ∀ m → sum (replicate m n) ≡ m * n
sum-replicate         zero    = refl _
sum-replicate {n = n} (suc m) =
  sum (replicate (suc m) n)  ≡⟨⟩
  n + sum (replicate m n)    ≡⟨ cong (n +_) $ sum-replicate m ⟩
  n + m * n                  ≡⟨⟩
  suc m * n                  ∎

-- The length of nats-< n is n.

length∘nats-< : ∀ n → length (nats-< n) ≡ n
length∘nats-< zero    = 0 ∎
length∘nats-< (suc n) = cong suc (length∘nats-< n)

-- The sum of nats-< n can be expressed without referring to lists.

sum-nats-< : ∀ n → sum (nats-< n) ≡ ⌊ n * pred n /2⌋
sum-nats-< zero          = refl _
sum-nats-< (suc zero)    = refl _
sum-nats-< (suc (suc n)) =
  sum (suc n ∷ nats-< (suc n))       ≡⟨⟩
  suc n + sum (nats-< (suc n))       ≡⟨ cong (suc n +_) (sum-nats-< (suc n)) ⟩
  suc n + ⌊ suc n * n /2⌋            ≡⟨ sym $ ⌊2*+/2⌋≡ (suc n) ⟩
  ⌊ 2 * suc n + suc n * n /2⌋        ≡⟨ cong ⌊_/2⌋ (solve 1 (λ n → con 2 :* (con 1 :+ n) :+ (con 1 :+ n) :* n :=
                                                                   con 1 :+ n :+ (con 1 :+ n :+ n :* (con 1 :+ n)))
                                                          (refl _) n) ⟩
  ⌊ suc n + (suc n + n * suc n) /2⌋  ≡⟨⟩
  ⌊ suc (suc n) * suc n /2⌋          ∎

-- If xs ++ ys is equal to [], then both lists are.

++≡[]→≡[]×≡[] : ∀ xs → xs ++ ys ≡ [] → xs ≡ [] × ys ≡ []
++≡[]→≡[]×≡[] {ys = []}    []      _    = refl _ , refl _
++≡[]→≡[]×≡[] {ys = _ ∷ _} []      ∷≡[] = ⊥-elim (List.[]≢∷ (sym ∷≡[]))
++≡[]→≡[]×≡[]              (_ ∷ _) ∷≡[] = ⊥-elim (List.[]≢∷ (sym ∷≡[]))

-- Empty lists are not equal to non-empty lists.

[]≢++∷ : ∀ xs → [] ≢ xs ++ y ∷ ys
[]≢++∷ {y = y} {ys = ys} xs =
  [] ≡ xs ++ y ∷ ys  ↝⟨ sym ∘ proj₂ ∘ ++≡[]→≡[]×≡[] xs ∘ sym ⟩
  [] ≡ y ∷ ys        ↝⟨ List.[]≢∷ ⟩□
  ⊥                  □

------------------------------------------------------------------------
-- The list monad

instance

  -- The list monad.

  raw-monad : Raw-monad (List {a = ℓ})
  Raw-monad.return raw-monad x    = x ∷ []
  Raw-monad._>>=_  raw-monad xs f = concat (map f xs)

  monad : Monad (List {a = ℓ})
  Monad.raw-monad      monad     = raw-monad
  Monad.left-identity  monad x f = foldr-∷-[] (f x)
  Monad.right-identity monad xs  = lemma xs
    where
    lemma : ∀ xs → concat (map (_∷ []) xs) ≡ xs
    lemma []       = refl _
    lemma (x ∷ xs) =
      concat (map (_∷ []) (x ∷ xs))  ≡⟨⟩
      x ∷ concat (map (_∷ []) xs)    ≡⟨ cong (x ∷_) (lemma xs) ⟩∎
      x ∷ xs                         ∎
  Monad.associativity monad xs f g = lemma xs
    where
    lemma : ∀ xs → concat (map (concat ∘ map g ∘ f) xs) ≡
                   concat (map g (concat (map f xs)))
    lemma []       = refl _
    lemma (x ∷ xs) =
      concat (map (concat ∘ map g ∘ f) (x ∷ xs))                    ≡⟨⟩
      concat (map g (f x)) ++ concat (map (concat ∘ map g ∘ f) xs)  ≡⟨ cong (concat (map g (f x)) ++_) (lemma xs) ⟩
      concat (map g (f x)) ++ concat (map g (concat (map f xs)))    ≡⟨ sym $ concat-++ (map g (f x)) _ ⟩
      concat (map g (f x) ++ map g (concat (map f xs)))             ≡⟨ cong concat (sym $ map-++ g (f x) _) ⟩
      concat (map g (f x ++ concat (map f xs)))                     ≡⟨ refl _ ⟩∎
      concat (map g (concat (map f (x ∷ xs))))                      ∎

------------------------------------------------------------------------
-- Some isomorphisms

-- An unfolding lemma for List.

List↔Maybe[×List] : List A ↔ Maybe (A × List A)
List↔Maybe[×List] = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { [] → inj₁ tt; (x ∷ xs) → inj₂ (x , xs) }
      ; from = [ (λ _ → []) , uncurry _∷_ ]
      }
    ; right-inverse-of = [ (λ _ → refl _) , (λ _ → refl _) ]
    }
  ; left-inverse-of = λ { [] → refl _; (_ ∷ _) → refl _ }
  }

-- Some isomorphisms related to list equality.

[]≡[]↔⊤ : [] ≡ ([] ⦂ List A) ↔ ⊤
[]≡[]↔⊤ =
  [] ≡ []            ↔⟨ inverse $ Eq.≃-≡ (Eq.↔⇒≃ List↔Maybe[×List]) ⟩
  nothing ≡ nothing  ↝⟨ inverse Bijection.≡↔inj₁≡inj₁ ⟩
  tt ≡ tt            ↝⟨ tt≡tt↔⊤ ⟩□
  ⊤                  □

[]≡∷↔⊥ : [] ≡ x ∷ xs ↔ ⊥ {ℓ = ℓ}
[]≡∷↔⊥ {x = x} {xs = xs} =
  [] ≡ x ∷ xs              ↔⟨ inverse $ Eq.≃-≡ (Eq.↔⇒≃ List↔Maybe[×List]) ⟩
  nothing ≡ just (x , xs)  ↝⟨ Bijection.≡↔⊎ ⟩
  ⊥                        ↝⟨ ⊥↔⊥ ⟩□
  ⊥                        □

∷≡[]↔⊥ : x ∷ xs ≡ [] ↔ ⊥ {ℓ = ℓ}
∷≡[]↔⊥ {x = x} {xs = xs} =
  x ∷ xs ≡ []  ↝⟨ ≡-comm ⟩
  [] ≡ x ∷ xs  ↝⟨ []≡∷↔⊥ ⟩□
  ⊥            □

∷≡∷↔≡×≡ : x ∷ xs ≡ y ∷ ys ↔ x ≡ y × xs ≡ ys
∷≡∷↔≡×≡ {x = x} {xs = xs} {y = y} {ys = ys} =
  x ∷ xs ≡ y ∷ ys                ↔⟨ inverse $ Eq.≃-≡ (Eq.↔⇒≃ List↔Maybe[×List]) ⟩
  just (x , xs) ≡ just (y , ys)  ↝⟨ inverse Bijection.≡↔inj₂≡inj₂ ⟩
  (x , xs) ≡ (y , ys)            ↝⟨ inverse ≡×≡↔≡ ⟩□
  x ≡ y × xs ≡ ys                □

------------------------------------------------------------------------
-- H-levels

-- If A is inhabited, then List A is not a proposition.

¬-List-propositional : A → ¬ Is-proposition (List A)
¬-List-propositional x h = List.[]≢∷ $ h [] (x ∷ [])

-- H-levels greater than or equal to two are closed under List.

H-level-List : ∀ n → H-level (2 + n) A → H-level (2 + n) (List A)
H-level-List n _ {[]} {[]} =
                             $⟨ ⊤-contractible ⟩
  Contractible ⊤             ↝⟨ H-level-cong _ 0 (inverse []≡[]↔⊤) ⟩
  Contractible ([] ≡ [])     ↝⟨ H-level.mono (zero≤ (1 + n)) ⟩□
  H-level (1 + n) ([] ≡ [])  □

H-level-List n h {[]} {y ∷ ys} =
                                 $⟨ ⊥-propositional ⟩
  Is-proposition ⊥₀              ↝⟨ H-level-cong _ 1 (inverse []≡∷↔⊥) ⟩
  Is-proposition ([] ≡ y ∷ ys)   ↝⟨ H-level.mono (suc≤suc (zero≤ n)) ⟩□
  H-level (1 + n) ([] ≡ y ∷ ys)  □

H-level-List n h {x ∷ xs} {[]} =
                                 $⟨ ⊥-propositional ⟩
  Is-proposition ⊥₀              ↝⟨ H-level-cong _ 1 (inverse ∷≡[]↔⊥) ⟩
  Is-proposition (x ∷ xs ≡ [])   ↝⟨ H-level.mono (suc≤suc (zero≤ n)) ⟩□
  H-level (1 + n) (x ∷ xs ≡ [])  □

H-level-List n h {x ∷ xs} {y ∷ ys} =
  H-level-cong _ (1 + n) (inverse ∷≡∷↔≡×≡)
    (×-closure (1 + n) h (H-level-List n h))

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Optics.Prism where
open import Agda.Primitive using (Level; _⊔_; lsuc)
open import Data.Product using (_×_; _,_; ∃-syntax; Σ-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂; fromInj₂)
open import Data.Empty using (⊥-elim)
open import Function.Inverse using (_↔_; inverse)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; module ≡-Reasoning; cong; cong₂; sym)

open import Category.Functor.Arr
open import Category.Functor.Either
open import Category.Profunctor.Star
open import Category.Profunctor.Joker
open import Category.Choice
open import Optics

Prism : ∀ {l} (S T A B : Set l) → Set (lsuc l)
Prism = Optic ChoiceImp

module Prism {l} {S T A B : Set l} (prism : Prism S T A B) where
  matching : S → A ⊎ T
  matching = matchingOptic S T A B (starChoice eitherApplicative) prism
  put : B → T
  put = putOptic S T A B (jokerChoice arrFunctor) prism

record LawfulPrism {l} {S A : Set l} (prism' : Prism S S A A) : Set (lsuc l) where
  open Prism prism' public
  prism : Prism S S A A
  prism = prism'
  field
    matchingput : ∀ (a : A) → matching (put a) ≡ inj₁ a
    putmatching : ∀ (s : S) (a : A) → matching s ≡ inj₁ a → put a ≡ s
    matchingmatching : ∀ (s t : S) → matching s ≡ inj₂ t → matching t ≡ inj₂ s

  matchingWithWitness : (s : S) → (Σ[ a ∈ A ] matching s ≡ inj₁ a) ⊎ (Σ[ t ∈ S ] matching s ≡ inj₂ t)
  matchingWithWitness s with matching s
  ...                      | inj₁ a = inj₁ (a , refl)
  ...                      | inj₂ t = inj₂ (t , refl)

uninjed₁ : ∀ {l₁ l₂} {A : Set l₁} {B : Set l₂} {x x₁ : A} → inj₁ {l₁} {l₂} {A} {B} x ≡ inj₁ {l₁} {l₂} {A} {B} x₁ → x ≡ x₁
uninjed₁ refl = refl

uninjed₂ : ∀ {l₁ l₂} {A : Set l₁} {B : Set l₂} {x x₁ : B} → inj₂ {l₁} {l₂} {A} {B} x ≡ inj₂ {l₁} {l₂} {A} {B} x₁ → x ≡ x₁
uninjed₂ refl = refl

inj₁≢inj₂ : ∀ {l₁ l₂} {A : Set l₁} {B : Set l₂} {x : A} {x₁ : B} → inj₁ x ≢ inj₂ x₁
inj₁≢inj₂ ()

prismIso : ∀ {l} {S A : Set l} {prism : Prism S S A A} → (lawful : LawfulPrism prism) → S ↔ (A ⊎ ∃[ s ] ∃[ t ] (Prism.matching prism s ≡ inj₂ t))
prismIso {_} {S} {A} lawful = inverse to from from∘to to∘from
   where
     open LawfulPrism lawful
     to : S → A ⊎ ∃[ s ] ∃[ t ] (matching s ≡ inj₂ t)
     to s with matchingWithWitness s
     ...     | inj₁ (a , _)          = inj₁ a
     ...     | inj₂ (t , w)          = inj₂ (s , t , w)
     from : A ⊎ ∃[ s ] ∃[ t ] (matching s ≡ inj₂ t) → S
     from (inj₁ x) = put x
     from (inj₂ (s , t , matchs≡injt)) = s
     from∘to : (s : S) → from (to s) ≡ s
     from∘to s with matchingWithWitness s
     ...          | inj₁ (a , w) = putmatching s a w
     ...          | inj₂ (t , _) = refl
     congΣ : ∀ {l₁ l₂} {T : Set l₁} {cmp : Set l₂} (W : T → cmp) (x : cmp) (t t' : T) (w : x ≡ W t) (w' : x ≡ W t') → t ≡ t' → (t , w) ≡ (t' , w')
     congΣ _ _ _ _ refl refl refl = refl
     to∘from : (elem : A ⊎ ∃[ s ] ∃[ t ] (matching s ≡ inj₂ t)) → to (from elem) ≡ elem
     open ≡-Reasoning
     to∘from (inj₁ x) with matchingWithWitness (put x)
     ...                 | inj₁ ( x₁ , w ) = cong inj₁ (uninjed₁ (inj₁ x₁ ≡⟨ sym w ⟩ matching (put x) ≡⟨ matchingput x ⟩ inj₁ x ∎))
     ...                 | inj₂ ( x₁ , w ) = ⊥-elim (inj₁≢inj₂ (inj₁ x ≡⟨ sym (matchingput x) ⟩ matching (put x) ≡⟨ w ⟩ inj₂ x₁ ∎))
     to∘from (inj₂ (s , t , w)) with matchingWithWitness s
     ...                           | inj₂ (t₁ , w₁) = cong inj₂ (cong (s ,_) (congΣ (λ tᵢ → inj₂ tᵢ) (matching s) t₁ t w₁ w (uninjed₂ (inj₂ t₁ ≡⟨ sym w₁ ⟩ matching s ≡⟨ w ⟩ inj₂ t ∎))))
     ...                           | inj₁ (a  , w₁) = ⊥-elim (inj₁≢inj₂ (inj₁ a ≡⟨ sym w₁ ⟩ matching s ≡⟨ w ⟩ inj₂ t ∎))

ext: agda

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


text:
module product-thms where

open import eq
open import level
open import product
open import unit
open import functions

-- this is called the inspect idiom, in the Agda stdlib
keep : ∀{ℓ}{A : Set ℓ} → (x : A) → Σ A (λ y → x ≡ y)
keep x = ( x , refl )

,inj : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}{a a' : A}{b b' : B} →
        (a , b) ≡ (a' , b') → (a ≡ a') ∧ (b ≡ b')
,inj refl = refl , refl

eta-× : ∀{ℓ₁ ℓ₂ ℓ₃}{A : Set ℓ₁}{B : Set ℓ₂}{C : Set ℓ₃}{h : A × B → C}
  → (extensionality {ℓ₁ ⊔ ℓ₂}{ℓ₃})
  → (λ c → h (fst c , snd c)) ≡ h
eta-× {A = A}{B}{C}{h} ext = ext eta-×-aux
 where
   eta-×-aux : ∀{a : Σ A (λ x → B)} → h (fst a , snd a) ≡ h a
   eta-×-aux {(a , b)} = refl

eq-× : ∀{ℓ₁ ℓ₂}{A : Set ℓ₁}{B : Set ℓ₂}{a a' : A}{b b' : B}
  → a ≡ a'
  → b ≡ b'
  → (a , b) ≡ (a' , b')
eq-× refl refl = refl

twist-×-iso : ∀{ℓ : level}{U V : Set ℓ}{a : U × V} → (twist-× ∘ twist-×) a ≡ id a
twist-×-iso {a  = u , v} = refl

-- This module proves typical isomorphisms about ∧.
module ∧-Isos where
  postulate ext-set : ∀{l1 l2 : level} → extensionality {l1} {l2}

  ∧-unit-l : ∀{ℓ}{A : Set ℓ} → A → A ∧ (⊤ {ℓ})
  ∧-unit-l x = x , triv

  ∧-unit-r : ∀{ℓ}{A : Set ℓ} → A → ⊤ ∧ A
  ∧-unit-r x = twist-× (∧-unit-l x)

  ∧-unit-l-iso : ∀{ℓ}{A : Set ℓ} → Iso A (A ∧ ⊤)
  ∧-unit-l-iso {_}{A} = isIso ∧-unit-l fst refl (ext-set aux)
   where
    aux : {a : A ∧ ⊤} → (fst a , triv) ≡ a
    aux {x , triv} = refl

  ∧-unit-r-iso : ∀{ℓ}{A : Set ℓ} → Iso A (⊤ ∧ A)
  ∧-unit-r-iso {_}{A} = isIso ∧-unit-r snd refl (ext-set aux)
   where
    aux : {a : ⊤ ∧ A} → (triv , snd a) ≡ a
    aux {triv , x} = refl

  ∧-assoc₁ : ∀{ℓ}{A B C : Set ℓ} → (A ∧ (B ∧ C)) → ((A ∧ B) ∧ C)
  ∧-assoc₁ (a , b , c) = ((a , b) , c)

  ∧-assoc₂ : ∀{ℓ}{A B C : Set ℓ} → ((A ∧ B) ∧ C) → (A ∧ (B ∧ C))
  ∧-assoc₂ ((a , b) , c) = (a , b , c)

  ∧-assoc-iso : ∀{ℓ}{A B C : Set ℓ} → Iso (A ∧ (B ∧ C)) ((A ∧ B) ∧ C)
  ∧-assoc-iso {_}{A}{B}{C} = isIso ∧-assoc₁ ∧-assoc₂ (ext-set aux₁) (ext-set aux₂)
   where
    aux₁ : {a : A ∧ (B ∧ C)} → ∧-assoc₂ (∧-assoc₁ a) ≡ a
    aux₁ {a , (b , c)} = refl

    aux₂ : {a : (A ∧ B) ∧ C} → ∧-assoc₁ (∧-assoc₂ a) ≡ a
    aux₂ {(a , b) , c} = refl

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


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

open import Algebra
open import Prelude
open import Relation.Binary.Equivalence.PropTruncated

module Algebra.Construct.Cayley.Propositional {a} (mon : Monoid a) where

open Monoid mon

record 𝒞 : Type a where
  constructor cayley
  infixr 7 _⇓_
  field
    _⇓_ : 𝑆 → 𝑆
    small : ∀ x → _⇓_ ε ∙ x ≐ _⇓_ x
open 𝒞 public

⟦_⇓⟧ : 𝒞 → 𝑆
⟦ x ⇓⟧ = x ⇓ ε

⟦_⇑⟧ : 𝑆 → 𝒞
⟦ x ⇑⟧ ⇓ y = x ∙ y
⟦ x ⇑⟧ .small y = ∣ cong (_∙ y) (∙ε x) ∣

ⓔ : 𝒞
ⓔ ⇓ x = x
ⓔ .small x = ∣ ε∙ x ∣

module _ where
  open Reasoning
  _⊙_ : 𝒞 → 𝒞 → 𝒞
  (x ⊙ y) ⇓ z = x ⇓ y ⇓ z
  (x ⊙ y) .small z =
    x ⇓ y ⇓ ε ∙ z       ≐˘⟨ ∙cong (_∙ z) (x .small (y ⇓ ε)) ⟩
    x ⇓ ε ∙ y ⇓ ε ∙ z   ≡⟨ assoc (x ⇓ ε) (y ⇓ ε) z ⟩
    x ⇓ ε ∙ (y ⇓ ε ∙ z) ≐⟨ ∙cong (x ⇓ ε ∙_) (y .small z)  ⟩
    x ⇓ ε ∙ y ⇓ z       ≐⟨ x .small (y ⇓ z) ⟩
    x ⇓ y ⇓ z ∎

⊙-assoc : Associative _⊙_
⊙-assoc x y z = refl

ⓔ⊙ : ∀ x → ⓔ ⊙ x ≡ x
ⓔ⊙ x = refl

⊙ⓔ : ∀ x → x ⊙ ⓔ ≡ x
⊙ⓔ x = refl

cayleyMonoid : Monoid a
Monoid.𝑆 cayleyMonoid = 𝒞
Monoid._∙_ cayleyMonoid = _⊙_
Monoid.ε cayleyMonoid = ⓔ
Monoid.assoc cayleyMonoid = ⊙-assoc
Monoid.ε∙ cayleyMonoid = ⓔ⊙
Monoid.∙ε cayleyMonoid = ⊙ⓔ

open import Data.Sigma.Properties
open import Relation.Nullary.Stable

𝒞≡ : {x y : 𝒞} → (∀ z → x ⇓ z ≡ y ⇓ z) → x ≡ y
𝒞≡ { f } { cayley g q } f≡g =
  subst
    (λ (g′ : 𝑆 → 𝑆) → (q′ : ∀ x → g′ ε ∙ x ≐ g′ x) → f ≡ cayley g′ q′)
    (funExt f≡g)
    (λ _ → refl)
    q

∙-homo : ∀ x y → ⟦ x ∙ y ⇑⟧ ≡ ⟦ x ⇑⟧ ⊙ ⟦ y ⇑⟧
∙-homo x y = 𝒞≡ (assoc x y)

ε-homo : ⟦ ε ⇑⟧ ≡ ⓔ
ε-homo = 𝒞≡ ε∙

homo-to : MonoidHomomorphism mon ⟶ cayleyMonoid
MonoidHomomorphism_⟶_.f homo-to = ⟦_⇑⟧
MonoidHomomorphism_⟶_.∙-homo homo-to = ∙-homo
MonoidHomomorphism_⟶_.ε-homo homo-to = ε-homo

ⓔ-homo : ⟦ ⓔ ⇓⟧ ≡ ε
ⓔ-homo = refl

module _ (sIsStable : ∀ {x y : 𝑆} → Stable (x ≡ y)) where
  ⊙-homo : ∀ x y → ⟦ x ⊙ y ⇓⟧ ≡ ⟦ x ⇓⟧ ∙ ⟦ y ⇓⟧
  ⊙-homo x y = sym (unsquash sIsStable (x .small ⟦ y ⇓⟧))

  𝒞-iso : 𝒞 ⇔ 𝑆
  fun 𝒞-iso = ⟦_⇓⟧
  inv 𝒞-iso = ⟦_⇑⟧
  rightInv 𝒞-iso = ∙ε
  leftInv  𝒞-iso x = 𝒞≡ λ y → unsquash sIsStable (x .small y)

  homo-from : MonoidHomomorphism cayleyMonoid ⟶ mon
  MonoidHomomorphism_⟶_.f homo-from = ⟦_⇓⟧
  MonoidHomomorphism_⟶_.∙-homo homo-from = ⊙-homo
  MonoidHomomorphism_⟶_.ε-homo homo-from = ⓔ-homo

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Boolean algebra expressions
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Properties.BooleanAlgebra.Expression
  {b} (B : BooleanAlgebra b b)
  where

open BooleanAlgebra B

open import Category.Applicative
import Category.Applicative.Indexed as Applicative
open import Category.Monad
open import Data.Fin using (Fin)
open import Data.Nat
open import Data.Product using (_,_; proj₁; proj₂)
open import Data.Vec as Vec using (Vec)
import Data.Vec.Categorical as VecCat
import Function.Identity.Categorical as IdCat
open import Data.Vec.Properties using (lookup-map)
open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW
  using (Pointwise; ext)
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≗_)
import Relation.Binary.Reflection as Reflection

-- Expressions made up of variables and the operations of a boolean
-- algebra.

infixr 7 _and_
infixr 6 _or_

data Expr n : Set b where
  var        : (x : Fin n) → Expr n
  _or_ _and_ : (e₁ e₂ : Expr n) → Expr n
  not        : (e : Expr n) → Expr n
  top bot    : Expr n

-- The semantics of an expression, parametrised by an applicative
-- functor.

module Semantics
  {F : Set b → Set b}
  (A : RawApplicative F)
  where

  open RawApplicative A

  ⟦_⟧ : ∀ {n} → Expr n → Vec (F Carrier) n → F Carrier
  ⟦ var x     ⟧ ρ = Vec.lookup ρ x
  ⟦ e₁ or e₂  ⟧ ρ = pure _∨_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
  ⟦ e₁ and e₂ ⟧ ρ = pure _∧_ ⊛ ⟦ e₁ ⟧ ρ ⊛ ⟦ e₂ ⟧ ρ
  ⟦ not e     ⟧ ρ = pure ¬_ ⊛ ⟦ e ⟧ ρ
  ⟦ top       ⟧ ρ = pure ⊤
  ⟦ bot       ⟧ ρ = pure ⊥

-- flip Semantics.⟦_⟧ e is natural.

module Naturality
  {F₁ F₂ : Set b → Set b}
  {A₁ : RawApplicative F₁}
  {A₂ : RawApplicative F₂}
  (f : Applicative.Morphism A₁ A₂)
  where

  open P.≡-Reasoning
  open Applicative.Morphism f
  open Semantics A₁ renaming (⟦_⟧ to ⟦_⟧₁)
  open Semantics A₂ renaming (⟦_⟧ to ⟦_⟧₂)
  open RawApplicative A₁ renaming (pure to pure₁; _⊛_ to _⊛₁_)
  open RawApplicative A₂ renaming (pure to pure₂; _⊛_ to _⊛₂_)

  natural : ∀ {n} (e : Expr n) → op ∘ ⟦ e ⟧₁ ≗ ⟦ e ⟧₂ ∘ Vec.map op
  natural (var x) ρ = begin
    op (Vec.lookup ρ x)                                            ≡⟨ P.sym $ lookup-map x op ρ ⟩
    Vec.lookup (Vec.map op ρ) x                                    ∎
  natural (e₁ or e₂) ρ = begin
    op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ)                       ≡⟨ op-⊛ _ _ ⟩
    op (pure₁ _∨_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)                  ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩
    op (pure₁ _∨_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)             ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ))
                                                                                (natural e₂ ρ) ⟩
    pure₂ _∨_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ)  ∎
  natural (e₁ and e₂) ρ = begin
    op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ)                       ≡⟨ op-⊛ _ _ ⟩
    op (pure₁ _∧_ ⊛₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)                  ≡⟨ P.cong₂ _⊛₂_ (op-⊛ _ _) P.refl ⟩
    op (pure₁ _∧_) ⊛₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)             ≡⟨ P.cong₂ _⊛₂_ (P.cong₂ _⊛₂_ (op-pure _) (natural e₁ ρ))
                                                                                (natural e₂ ρ) ⟩
    pure₂ _∧_ ⊛₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ)  ∎
  natural (not e) ρ = begin
    op (pure₁ ¬_ ⊛₁ ⟦ e ⟧₁ ρ)                                      ≡⟨ op-⊛ _ _ ⟩
    op (pure₁ ¬_) ⊛₂ op (⟦ e ⟧₁ ρ)                                 ≡⟨ P.cong₂ _⊛₂_ (op-pure _) (natural e ρ) ⟩
    pure₂ ¬_ ⊛₂ ⟦ e ⟧₂ (Vec.map op ρ)                              ∎
  natural top ρ = begin
    op (pure₁ ⊤)                                                   ≡⟨ op-pure _ ⟩
    pure₂ ⊤                                                        ∎
  natural bot ρ = begin
    op (pure₁ ⊥)                                                   ≡⟨ op-pure _ ⟩
    pure₂ ⊥                                                        ∎

-- An example of how naturality can be used: Any boolean algebra can
-- be lifted, in a pointwise manner, to vectors of carrier elements.

lift : ℕ → BooleanAlgebra b b
lift n = record
  { Carrier          = Vec Carrier n
  ; _≈_              = Pointwise _≈_
  ; _∨_              = zipWith _∨_
  ; _∧_              = zipWith _∧_
  ; ¬_               = map ¬_
  ; ⊤                = pure ⊤
  ; ⊥                = pure ⊥
  ; isBooleanAlgebra = record
    { isDistributiveLattice = record
      { isLattice = record
        { isEquivalence = PW.isEquivalence isEquivalence
        ; ∨-comm        = λ _ _ → ext λ i →
                            solve i 2 (λ x y → x or y , y or x)
                                  (∨-comm _ _) _ _
        ; ∨-assoc       = λ _ _ _ → ext λ i →
                            solve i 3
                              (λ x y z → (x or y) or z , x or (y or z))
                              (∨-assoc _ _ _) _ _ _
        ; ∨-cong        = λ xs≈us ys≈vs → ext λ i →
                            solve₁ i 4 (λ x y u v → x or y , u or v)
                                   _ _ _ _
                                   (∨-cong (Pointwise.app xs≈us i)
                                           (Pointwise.app ys≈vs i))
        ; ∧-comm        = λ _ _ → ext λ i →
                            solve i 2 (λ x y → x and y , y and x)
                                  (∧-comm _ _) _ _
        ; ∧-assoc       = λ _ _ _ → ext λ i →
                            solve i 3
                              (λ x y z → (x and y) and z ,
                                         x and (y and z))
                              (∧-assoc _ _ _) _ _ _
        ; ∧-cong        = λ xs≈ys us≈vs → ext λ i →
                            solve₁ i 4 (λ x y u v → x and y , u and v)
                                   _ _ _ _
                                   (∧-cong (Pointwise.app xs≈ys i)
                                           (Pointwise.app us≈vs i))
        ; absorptive    =
          (λ _ _ → ext λ i →
            solve i 2 (λ x y → x or (x and y) , x) (∨-absorbs-∧ _ _) _ _) ,
          (λ _ _ → ext λ i →
            solve i 2 (λ x y → x and (x or y) , x) (∧-absorbs-∨ _ _) _ _)
        }
      ; ∨-∧-distribʳ = λ _ _ _ → ext λ i →
                         solve i 3
                               (λ x y z → (y and z) or x ,
                                          (y or x) and (z or x))
                               (∨-∧-distribʳ _ _ _) _ _ _
      }
    ; ∨-complementʳ = λ _ → ext λ i →
                        solve i 1 (λ x → x or (not x) , top)
                              (∨-complementʳ _) _
    ; ∧-complementʳ = λ _ → ext λ i →
                        solve i 1 (λ x → x and (not x) , bot)
                              (∧-complementʳ _) _
    ; ¬-cong        = λ xs≈ys → ext λ i →
                        solve₁ i 2 (λ x y → not x , not y) _ _
                               (¬-cong (Pointwise.app xs≈ys i))
    }
  }
  where
  open RawApplicative VecCat.applicative
    using (pure; zipWith) renaming (_<$>_ to map)

  ⟦_⟧Id : ∀ {n} → Expr n → Vec Carrier n → Carrier
  ⟦_⟧Id = Semantics.⟦_⟧ IdCat.applicative

  ⟦_⟧Vec : ∀ {m n} → Expr n → Vec (Vec Carrier m) n → Vec Carrier m
  ⟦_⟧Vec = Semantics.⟦_⟧ VecCat.applicative

  open module R {n} (i : Fin n) =
    Reflection setoid var
      (λ e ρ → Vec.lookup (⟦ e ⟧Vec ρ) i)
      (λ e ρ → ⟦ e ⟧Id (Vec.map (flip Vec.lookup i) ρ))
      (λ e ρ → sym $ reflexive $
                 Naturality.natural (VecCat.lookup-morphism i) e ρ)


text:
module Syntax where

open import Agda.Builtin.FromNat public
open import Agda.Builtin.FromNeg public

record plus-syntax (A : Set) (B : A → Set) (C : ∀ x → B x → Set) : Set where
  infixl 6 _+_
  field _+_ : ∀ x (y : B x) → C x y

plus-syntax-simple = λ A B C → plus-syntax A (λ _ → B) (λ _ _ → C)

open plus-syntax {{…}} public

record minus-syntax (A : Set) (B : A → Set) (C : ∀ x → B x → Set) : Set where
  infixl 6 _-_
  field _-_ : ∀ x (y : B x) → C x y

minus-syntax-simple = λ A B C → minus-syntax A (λ _ → B) (λ _ _ → C)

open minus-syntax {{…}} public

record times-syntax (A : Set) (B : A → Set) (C : ∀ x → B x → Set) : Set where
  infixl 7 _*_
  field _*_ : ∀ x (y : B x) → C x y

times-syntax-simple = λ A B C → times-syntax A (λ _ → B) (λ _ _ → C)

open times-syntax {{…}} public

record raise-syntax (A : Set) (B : A → Set) (C : ∀ x → B x → Set) : Set where
  infixl 8 _^_
  field _^_ : ∀ x (y : B x) → C x y

raise-syntax-simple = λ A B C → raise-syntax A (λ _ → B) (λ _ _ → C)

open raise-syntax {{…}} public


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

module Categories.Category.Lift where

open import Level
open import Categories.Category
open import Categories.Functor using (Functor)

liftC : ∀ {o ℓ e} o′ ℓ′ e′ → Category o ℓ e → Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
liftC o′ ℓ′ e′ C = record
  { Obj       = Lift o′ Obj
  ; _⇒_       = λ X Y → Lift ℓ′ (lower X ⇒ lower Y)
  ; _≈_       = λ f g → Lift e′ (lower f ≈ lower g)
  ; id        = lift id
  ; _∘_       = λ f g → lift (lower f ∘ lower g)
  ; assoc     = lift assoc
  ; sym-assoc = lift sym-assoc
  ; identityˡ = lift identityˡ
  ; identityʳ = lift identityʳ
  ; identity² = lift identity²
  ; equiv     = record
    { refl  = lift Equiv.refl
    ; sym   = λ eq → lift (Equiv.sym (lower eq))
    ; trans = λ eq eq′ → lift (Equiv.trans (lower eq) (lower eq′))
    }
  ; ∘-resp-≈  = λ eq eq′ → lift (∘-resp-≈ (lower eq) (lower eq′))
  }
  where open Category C

liftF : ∀ {o ℓ e} o′ ℓ′ e′ (C : Category o ℓ e) → Functor C (liftC o′ ℓ′ e′ C)
liftF  o′ ℓ′ e′ C = record
  { F₀           = lift
  ; F₁           = lift
  ; identity     = lift refl
  ; homomorphism = lift refl
  ; F-resp-≈     = lift
  }
  where open Category C
        open Equiv

unliftF : ∀ {o ℓ e} o′ ℓ′ e′ (C : Category o ℓ e) → Functor (liftC o′ ℓ′ e′ C) C
unliftF o′ ℓ′ e′ C = record
  { F₀           = lower
  ; F₁           = lower
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = lower
  }
  where open Category C
        open Equiv

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 L.Base.Id.Properties where

open import L.Base.Id.Core

sym : ∀{a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym {x = x}{y = y} = λ p → J (λ a b _ → b ≡ a) (λ _ → refl) x y p

tran : ∀{a} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
tran {x = x}{y = y}{z = z} =
     λ p → J (λ a b p → b ≡ z → a ≡ z) (λ a q → q) x y p

ap : ∀{a b} {A : Set a} {B : Set b} {x y : A}
     → (f : A → B) → x ≡ y → (f x) ≡ (f y)
ap {x = x}{y = y} =
   λ f p → J (λ a b p → (f a) ≡ (f b)) (λ u → refl) x y p

transport : ∀{a b} {A : Set a} {x y : A}
            → (B : (x : A) → Set b) → x ≡ y → B x → B y
transport {x = x}{y = y} =
          λ B p → J (λ a b p → B a → B b) (λ a q → q) x y p

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
module BadInductionRecursion1 where

data Unit : Set where
  unit : Unit

mutual
  data D : Set where
    d : forall u -> (D′ u -> D′ u) -> D

  D′ : Unit -> Set
  D′ unit = D

_·_ : D -> D -> D
d unit f · x = f x

ω : D
ω = d unit (\x -> x · x)

Ω : D
Ω = ω · ω

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- The FOTC co-inductive natural numbers type
------------------------------------------------------------------------------

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

-- N.B. This module is re-exported by FOTC.Data.Conat.

-- Adapted from (Sander 1992).

module FOTC.Data.Conat.Type where

open import FOTC.Base

------------------------------------------------------------------------------
-- The FOTC co-inductive natural numbers type (co-inductive predicate
-- for total co-inductive natural)

-- Functional for the NatF predicate.
-- NatF : (D → Set) → D → Set
-- NatF A n = n = zero ∨ (∃[ n' ] n = succ n' ∧ A n')

-- Conat is the greatest fixed-point of NatF (by Conat-out and
-- Conat-coind).

postulate Conat : D → Set

-- Conat is a post-fixed point of NatF, i.e.
--
-- Conat ≤ NatF Conat.
postulate
  Conat-out : ∀ {n} → Conat n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n')
{-# ATP axiom Conat-out #-}

-- Conat is the greatest post-fixed point of NatF, i.e.
--
-- ∀ A. A ≤ NatF A ⇒ A ≤ Conat.
--
-- N.B. This is an axiom schema. Because in the automatic proofs we
-- *must* use an instance, we do not add this postulate as an ATP
-- axiom.
postulate
  Conat-coind :
    (A : D → Set) →
    -- A is post-fixed point of NatF.
    (∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')) →
    -- Conat is greater than A.
    ∀ {n} → A n → Conat n

------------------------------------------------------------------------------
-- References
--
-- Sander, Herbert P. (1992). A Logic of Functional Programs with an
-- Application to Concurrency. PhD thesis. Department of Computer
-- Sciences: Chalmers University of Technology and University of
-- Gothenburg.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Connectives where

-- Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)
-- open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality)
-- open plfa.part1.Isomorphism.≃-Reasoning

postulate
  -- 外延性の公理
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

-- 同型
infix 0 _≃_
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

≃-refl : ∀ {A : Set}
    -----
  → A ≃ A
≃-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    ; to∘from = λ{y → refl}
    }

≃-trans : ∀ {A B C : Set}
  → A ≃ B
  → B ≃ C
    -----
  → A ≃ C
≃-trans A≃B B≃C =
  record
    { to       = to   B≃C ∘ to   A≃B
    ; from     = from A≃B ∘ from B≃C
    ; from∘to  = λ{x →
        begin
          (from A≃B ∘ from B≃C) ((to B≃C ∘ to A≃B) x)
        ≡⟨⟩
          from A≃B (from B≃C (to B≃C (to A≃B x)))
        ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
          from A≃B (to A≃B x)
        ≡⟨ from∘to A≃B x ⟩
          x
        ∎}
    ; to∘from = λ{y →
        begin
          (to B≃C ∘ to A≃B) ((from A≃B ∘ from B≃C) y)
        ≡⟨⟩
          to B≃C (to A≃B (from A≃B (from B≃C y)))
        ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C y)) ⟩
          to B≃C (from B≃C y)
        ≡⟨ to∘from B≃C y ⟩
          y
        ∎}
     }

module ≃-Reasoning where

  infix  1 ≃-begin_
  infixr 2 _≃⟨_⟩_
  infix  3 _≃-∎

  ≃-begin_ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≃ B
  ≃-begin A≃B = A≃B

  _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≃ B
    → B ≃ C
      -----
    → A ≃ C
  A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

  _≃-∎ : ∀ (A : Set)
      -----
    → A ≃ A
  A ≃-∎ = ≃-refl

open ≃-Reasoning

-- 埋め込み
infix 0 _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

-- Conjunction is product

-- 直積
data _×_ (A B : Set) : Set where

  ⟨_,_⟩ :
      A
    → B
      -----
    → A × B

proj₁ : ∀ {A B : Set}
  → A × B
    -----
  → A
proj₁ ⟨ x , y ⟩ = x

proj₂ : ∀ {A B : Set}
  → A × B
    -----
  → B
proj₂ ⟨ x , y ⟩ = y

record _×′_ (A B : Set) : Set where
  field
    proj₁′ : A
    proj₂′ : B
open _×′_

η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× ⟨ x , y ⟩ = refl

infixr 2 _×_

data Bool : Set where
  true  : Bool
  false : Bool

data Tri : Set where
  aa : Tri
  bb : Tri
  cc : Tri

×-count : Bool × Tri → ℕ
×-count ⟨ true  , aa ⟩ = 1
×-count ⟨ true  , bb ⟩ = 2
×-count ⟨ true  , cc ⟩ = 3
×-count ⟨ false , aa ⟩ = 4
×-count ⟨ false , bb ⟩ = 5
×-count ⟨ false , cc ⟩ = 6

×-comm : ∀ {A B : Set} → A × B ≃ B × A
×-comm =
  record
    { to      = λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ }
    ; from    = λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
    ; from∘to = λ{ ⟨ x , y ⟩ → refl }
    ; to∘from = λ{ ⟨ y , x ⟩ → refl }
    }

×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
×-assoc =
  record
    { to      = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → ⟨ x , ⟨ y , z ⟩ ⟩ }
    ; from    = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ }
    ; from∘to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → refl }
    ; to∘from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → refl }
    }

-- Truth is unit

data ⊤ : Set where

  tt :
    --
    ⊤

η-⊤ : ∀ (w : ⊤) → tt ≡ w
η-⊤ tt = refl

⊤-count : ⊤ → ℕ
⊤-count tt = 1

⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A
⊤-identityˡ =
  record
    { to      = λ{ ⟨ tt , x ⟩ → x }
    ; from    = λ{ x → ⟨ tt , x ⟩ }
    ; from∘to = λ{ ⟨ tt , x ⟩ → refl }
    ; to∘from = λ{ x → refl }
    }

⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A
⊤-identityʳ {A} =
  ≃-begin
    (A × ⊤)
  ≃⟨ ×-comm ⟩
    (⊤ × A)
  ≃⟨ ⊤-identityˡ ⟩
    A
  ≃-∎

-- Disjunction is sum

-- 直和
data _⊎_ (A B : Set) : Set where

  inj₁ :
      A
      -----
    → A ⊎ B

  inj₂ :
      B
      -----
    → A ⊎ B

case-⊎ : ∀ {A B C : Set}
  → (A → C)
  → (B → C)
  → A ⊎ B
    -----------
  → C
case-⊎ f g (inj₁ x) = f x
case-⊎ f g (inj₂ y) = g y

η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w
η-⊎ (inj₁ x) = refl
η-⊎ (inj₂ y) = refl

uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B) →
  case-⊎ (h ∘ inj₁) (h ∘ inj₂) w ≡ h w
uniq-⊎ h (inj₁ x) = refl
uniq-⊎ h (inj₂ y) = refl

infixr 1 _⊎_

⊎-count : Bool ⊎ Tri → ℕ
⊎-count (inj₁ true)  = 1
⊎-count (inj₁ false) = 2
⊎-count (inj₂ aa)    = 3
⊎-count (inj₂ bb)    = 4
⊎-count (inj₂ cc)    = 5

-- False is empty

data ⊥ : Set where
  -- no clauses!

⊥-elim : ∀ {A : Set}
  → ⊥
    --
  → A
⊥-elim ()

uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
uniq-⊥ h ()

⊥-count : ⊥ → ℕ
⊥-count ()

-- Implication is function

→-elim : ∀ {A B : Set}
  → (A → B)
  → A
    -------
  → B
→-elim L M = L M

η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
η-→ f = refl

→-count : (Bool → Tri) → ℕ
→-count f with f true | f false
...          | aa     | aa      =   1
...          | aa     | bb      =   2
...          | aa     | cc      =   3
...          | bb     | aa      =   4
...          | bb     | bb      =   5
...          | bb     | cc      =   6
...          | cc     | aa      =   7
...          | cc     | bb      =   8
...          | cc     | cc      =   9

currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
currying =
  record
    { to      =  λ{ f → λ{ ⟨ x , y ⟩ → f x y }}
    ; from    =  λ{ g → λ{ x → λ{ y → g ⟨ x , y ⟩ }}}
    ; from∘to =  λ{ f → refl }
    ; to∘from =  λ{ g → extensionality λ{ ⟨ x , y ⟩ → refl }}
    }

→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
→-distrib-⊎ =
  record
    { to      = λ{ f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ }
    ; from    = λ{ ⟨ g , h ⟩ → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } }
    ; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } }
    ; to∘from = λ{ ⟨ g , h ⟩ → refl }
    }

→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
→-distrib-× =
  record
    { to      = λ{ f → ⟨ proj₁ ∘ f , proj₂ ∘ f ⟩ }
    ; from    = λ{ ⟨ g , h ⟩ → λ x → ⟨ g x , h x ⟩ }
    ; from∘to = λ{ f → extensionality λ{ x → η-× (f x) } }
    ; to∘from = λ{ ⟨ g , h ⟩ → refl }
    }

-- Distribution

×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
×-distrib-⊎ =
  record
    { to      = λ{ ⟨ inj₁ x , z ⟩ → (inj₁ ⟨ x , z ⟩)
                 ; ⟨ inj₂ y , z ⟩ → (inj₂ ⟨ y , z ⟩)
                 }
    ; from    = λ{ (inj₁ ⟨ x , z ⟩) → ⟨ inj₁ x , z ⟩
                 ; (inj₂ ⟨ y , z ⟩) → ⟨ inj₂ y , z ⟩
                 }
    ; from∘to = λ{ ⟨ inj₁ x , z ⟩ → refl
                 ; ⟨ inj₂ y , z ⟩ → refl
                 }
    ; to∘from = λ{ (inj₁ ⟨ x , z ⟩) → refl
                 ; (inj₂ ⟨ y , z ⟩) → refl
                 }
    }

⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)
⊎-distrib-× =
  record
    { to      = λ{ (inj₁ ⟨ x , y ⟩) → ⟨ inj₁ x , inj₁ y ⟩
                 ; (inj₂ z)         → ⟨ inj₂ z , inj₂ z ⟩
                 }
    ; from    = λ{ ⟨ inj₁ x , inj₁ y ⟩ → (inj₁ ⟨ x , y ⟩)
                 ; ⟨ inj₁ x , inj₂ z ⟩ → (inj₂ z)
                 ; ⟨ inj₂ z , _      ⟩ → (inj₂ z)
                 }
    ; from∘to = λ{ (inj₁ ⟨ x , y ⟩) → refl
                 ; (inj₂ z)         → refl
                 }
    }

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
module Numeral.Natural.Oper.Proofs.Order where

open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Classical
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Relator.Ordering.Proofs
open import Structure.Function.Domain
open import Structure.Operator
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Syntax.Transitivity

[≤]ₗ[+] : ∀{x y : ℕ} → (x + y ≤ x) → (y ≡ 𝟎)
[≤]ₗ[+] {𝟎}               = [≤][0]ᵣ
[≤]ₗ[+] {𝐒(x)}{y} (proof) = [≤]ₗ[+] {x} ([≤]-without-[𝐒] {x + y} {x} (proof))

[≤]-with-[+]ᵣ : ∀{x y z : ℕ} → (x ≤ y) → (x + z ≤ y + z)
[≤]-with-[+]ᵣ {_}{_}{𝟎}    (proof)    = proof
[≤]-with-[+]ᵣ {_}{_}{𝐒(z)} (proof) = [≤]-with-[𝐒] ⦃ [≤]-with-[+]ᵣ {_}{_}{z} (proof) ⦄

[≤]-with-[+]ₗ : ∀{x y z : ℕ} → (x ≤ y) → (z + x ≤ z + y)
[≤]-with-[+]ₗ {.0} {𝟎}   {z } min        = reflexivity(_≤_)
[≤]-with-[+]ₗ {.0} {𝐒 y} {z}  min        = [≤]-successor([≤]-with-[+]ₗ {0}{y}{z} [≤]-minimum)
[≤]-with-[+]ₗ {𝐒 x} {𝐒 y} {z} (succ xy ) = [≤]-with-[𝐒] ⦃ [≤]-with-[+]ₗ {x} {y} {z} xy ⦄

[≤]-of-[+]ᵣ : ∀{x y : ℕ} → (y ≤ x + y)
[≤]-of-[+]ᵣ {x}   {𝟎}   = [≤]-minimum
[≤]-of-[+]ᵣ {𝟎}   {𝐒 x} = reflexivity(_≤_)
[≤]-of-[+]ᵣ {𝐒 x} {𝐒 y} = [≤]-with-[𝐒] ⦃ [≤]-of-[+]ᵣ {𝐒 x}{y} ⦄

[≤]-of-[+]ₗ : ∀{x y : ℕ} → (x ≤ x + y)
[≤]-of-[+]ₗ {𝟎}   {y}   = [≤]-minimum
[≤]-of-[+]ₗ {𝐒 x} {𝟎}   = reflexivity(_≤_)
[≤]-of-[+]ₗ {𝐒 x} {𝐒 y} = [≤]-with-[𝐒] ⦃ [≤]-of-[+]ₗ {x}{𝐒 y} ⦄

[≤]-with-[+] : ∀{x₁ y₁ : ℕ} → ⦃ _ : (x₁ ≤ y₁)⦄ → ∀{x₂ y₂ : ℕ} → ⦃ _ : (x₂ ≤ y₂)⦄ → (x₁ + x₂ ≤ y₁ + y₂)
[≤]-with-[+] {x₁} {y₁} ⦃ x1y1 ⦄ {.0}   {y₂}   ⦃ min ⦄   = transitivity(_≤_) x1y1 [≤]-of-[+]ₗ
[≤]-with-[+] {x₁} {y₁} ⦃ x1y1 ⦄ {𝐒 x₂} {𝐒 y₂} ⦃ succ p ⦄ = succ ([≤]-with-[+] {x₁} {y₁} {x₂} {y₂} ⦃ p ⦄)

[≤]-from-[+] : ∀{ℓ}{P : ℕ → Stmt{ℓ}}{x} → (∀{n} → P(x + n)) → (∀{y} → ⦃ _ : (x ≤ y) ⦄ → P(y))
[≤]-from-[+] {ℓ} {P} {𝟎}   anpxn {y}   ⦃ [≤]-minimum ⦄        = anpxn{y}
[≤]-from-[+] {ℓ} {P} {𝐒 x} anpxn {𝐒 y} ⦃ succ xy ⦄ = [≤]-from-[+] {ℓ} {P ∘ 𝐒} {x} anpxn {y} ⦃ xy ⦄

[−₀][+]-nullify2 : ∀{x y} → (x ≤ y) ↔ (x + (y −₀ x) ≡ y)
[−₀][+]-nullify2 {x}{y} = [↔]-intro (l{x}{y}) (r{x}{y}) where
  l : ∀{x y} → (x ≤ y) ← (x + (y −₀ x) ≡ y)
  l {𝟎}   {_}    _     = [≤]-minimum
  l {𝐒(_)}{𝟎}    ()
  l {𝐒(x)}{𝐒(y)} proof = [≤]-with-[𝐒] ⦃ l{x}{y} (injective(𝐒) proof) ⦄

  r : ∀{x y} → (x ≤ y) → (x + (y −₀ x) ≡ y)
  r {𝟎}   {𝟎}    proof = [≡]-intro
  r {𝟎}   {𝐒(_)} proof = [≡]-intro
  r {𝐒(_)}{𝟎}    ()
  r {𝐒(x)}{𝐒(y)} (succ proof) = [≡]-with(𝐒) (r{x}{y} (proof))

[−₀][+]-nullify2ᵣ : ∀{x y} → (x ≤ y) ↔ ((y −₀ x) + x ≡ y)
[−₀][+]-nullify2ᵣ {x}{y} = [↔]-transitivity [−₀][+]-nullify2 ([≡]-substitution (commutativity(_+_) {x}{y −₀ x}) {_≡ y})

[−₀]-when-0 : ∀{x y} → (x ≤ y) ↔ (x −₀ y ≡ 𝟎)
[−₀]-when-0 {x}{y} = [↔]-intro (l{x}{y}) (r{x}{y}) where
  l : ∀{x y} → (x ≤ y) ← (x −₀ y ≡ 𝟎)
  l {𝟎}   {_}    _     = [≤]-minimum
  l {𝐒(_)}{𝟎}    ()
  l {𝐒(x)}{𝐒(y)} proof = [≤]-with-[𝐒] ⦃ l{x}{y} proof ⦄

  r : ∀{x y} → (x ≤ y) → (x −₀ y ≡ 𝟎)
  r {𝟎}   {_}    proof = [≡]-intro
  r {𝐒(_)}{𝟎}    ()
  r {𝐒(x)}{𝐒(y)} (succ proof) = r{x}{y} (proof)

[−₀]-lesser-[𝐒]ₗ : ∀{x y} → ((x −₀ 𝐒(y)) ≤ (x −₀ y))
[−₀]-lesser-[𝐒]ᵣ : ∀{x y} → ((x −₀ y) ≤ (𝐒(x) −₀ y))

[−₀]-lesser-[𝐒]ₗ {𝟎}   {_}    = [≤]-minimum
[−₀]-lesser-[𝐒]ₗ {𝐒(_)}{𝟎}    = [≤]-of-[𝐒]
[−₀]-lesser-[𝐒]ₗ {𝐒(x)}{𝐒(y)} = [−₀]-lesser-[𝐒]ᵣ {x}{𝐒(y)}

[−₀]-lesser-[𝐒]ᵣ {𝟎}   {_}    = [≤]-minimum
[−₀]-lesser-[𝐒]ᵣ {𝐒(x)}{𝟎}    = [≤]-of-[𝐒]
[−₀]-lesser-[𝐒]ᵣ {𝐒(x)}{𝐒(y)} = [−₀]-lesser-[𝐒]ₗ {𝐒(x)}{y}

[≤][−₀][𝐒]ₗ : ∀{x y} → ((𝐒(x) −₀ y) ≤ 𝐒(x −₀ y))
[≤][−₀][𝐒]ₗ {x}   {𝟎}    = reflexivity(_≤_)
[≤][−₀][𝐒]ₗ {𝟎}   {𝐒(y)} = [≤]-minimum
[≤][−₀][𝐒]ₗ {𝐒(x)}{𝐒(y)} = [≤][−₀][𝐒]ₗ {x}{y}

[−₀][𝐒]ₗ-equality : ∀{x y} → (x ≥ y) ↔ ((𝐒(x) −₀ y) ≡ 𝐒(x −₀ y))
[−₀][𝐒]ₗ-equality = [↔]-intro l r where
  l : ∀{x y} → (x ≥ y) ← ((𝐒(x) −₀ y) ≡ 𝐒(x −₀ y))
  l {𝟎}   {𝟎}   p = [≤]-minimum
  l {𝐒 x} {𝟎}   p = [≤]-minimum
  l {𝐒 x} {𝐒 y} p = [≤]-with-[𝐒] ⦃ l{x}{y} p ⦄

  r : ∀{x y} → (x ≥ y) → ((𝐒(x) −₀ y) ≡ 𝐒(x −₀ y))
  r {x}   {.𝟎}  min       = [≡]-intro
  r {𝐒 x} {𝐒 y} (succ xy) = r xy

[−₀]-lesser : ∀{x y} → ((x −₀ y) ≤ x)
[−₀]-lesser {𝟎}   {_}    = [≤]-minimum
[−₀]-lesser {𝐒(x)}{𝟎}    = reflexivity(_≤_)
[−₀]-lesser {𝐒(x)}{𝐒(y)} = ([−₀]-lesser-[𝐒]ₗ {𝐒(x)}{y}) 🝖 ([−₀]-lesser {𝐒(x)}{y})

-- TODO: Converse is probably also true. One way to prove the equivalence is contraposition of [−₀]-comparison. Another is by [≤]-with-[+]ᵣ and some other stuff, but it seems to require more work
[−₀]-positive : ∀{x y} → (y > x) → (y −₀ x > 0)
[−₀]-positive {𝟎}   {𝐒(y)} _        = [≤]-with-[𝐒] ⦃ [≤]-minimum ⦄
[−₀]-positive {𝐒(x)}{𝐒(y)} (succ p) = [−₀]-positive {x}{y} p

[−₀]-nested-sameₗ : ∀{x y} → (x ≥ y) ↔ (x −₀ (x −₀ y) ≡ y)
[−₀]-nested-sameₗ {x}{y} = [↔]-intro (l{x}{y}) (r{x}{y}) where
  l : ∀{x y} → (x ≥ y) ← (x −₀ (x −₀ y) ≡ y)
  l {x}{y} proof =
    y             🝖[ _≤_ ]-[ [≡]-to-[≤] (symmetry(_≡_) proof) ]
    x −₀ (x −₀ y) 🝖[ _≤_ ]-[ [−₀]-lesser {x}{x −₀ y} ]
    x             🝖[ _≤_ ]-end

  r : ∀{x y} → (x ≥ y) → (x −₀ (x −₀ y) ≡ y)
  r{x}{y} x≥y =
    x −₀ (x −₀ y)              🝖[ _≡_ ]-[ [≡]-with(_−₀ (x −₀ y)) (symmetry(_≡_) ([↔]-to-[→] ([−₀][+]-nullify2 {y}{x}) (x≥y)) 🝖 commutativity(_+_) {y}{x −₀ y}) ]
    ((x −₀ y) + y) −₀ (x −₀ y) 🝖[ _≡_ ]-[ [−₀]ₗ[+]ₗ-nullify {x −₀ y}{y} ]
    y                          🝖-end

[+][−₀]-almost-associativity : ∀{x y z} → (y ≥ z) → ((x + y) −₀ z ≡ x + (y −₀ z))
[+][−₀]-almost-associativity {x} {y}   {.𝟎}  min      = [≡]-intro
[+][−₀]-almost-associativity {x} {𝐒 y} {𝐒 z} (succ p) = [+][−₀]-almost-associativity {x}{y}{z} p

[−₀][𝄩]-equality-condition : ∀{x y} → (x ≥ y) ↔ (x −₀ y ≡ x 𝄩 y)
[−₀][𝄩]-equality-condition = [↔]-intro l r where
  l : ∀{x y} → (x ≥ y) ← (x −₀ y ≡ x 𝄩 y)
  l {_}   {𝟎}   _ = min
  l {𝐒 x} {𝐒 y} p = succ(l p)

  r : ∀{x y} → (x ≥ y) → (x −₀ y ≡ x 𝄩 y)
  r min = [≡]-intro
  r (succ p) = r p

[𝄩]-intro-by[−₀] : ∀{ℓ}{P : ℕ → TYPE(ℓ)} → ∀{x y} → P(x −₀ y) → P(y −₀ x) → P(x 𝄩 y)
[𝄩]-intro-by[−₀] {x = x}{y = y} p1 p2 with [≤][>]-dichotomy {x}{y}
... | [∨]-introₗ le
  rewrite [↔]-to-[→] [−₀][𝄩]-equality-condition le
  rewrite commutativity(_𝄩_) {x}{y}
  = p2
... | [∨]-introᵣ gt
  rewrite [↔]-to-[→] [−₀][𝄩]-equality-condition ([≤]-predecessor gt)
  = p1

[𝄩]-of-𝐒ₗ : ∀{x y} → (x ≥ y) → (𝐒(x) 𝄩 y ≡ 𝐒(x 𝄩 y))
[𝄩]-of-𝐒ₗ {𝟎}   {𝟎}   = const [≡]-intro
[𝄩]-of-𝐒ₗ {𝐒 x} {𝟎}   = const [≡]-intro
[𝄩]-of-𝐒ₗ {𝐒 x} {𝐒 y} = [𝄩]-of-𝐒ₗ {x} {y} ∘ [≤]-without-[𝐒]

[𝄩]-of-𝐒ᵣ : ∀{x y} → (x ≤ y) → (x 𝄩 𝐒(y) ≡ 𝐒(x 𝄩 y))
[𝄩]-of-𝐒ᵣ {𝟎}   {𝟎}   = const [≡]-intro
[𝄩]-of-𝐒ᵣ {𝟎}   {𝐒 y} = const [≡]-intro
[𝄩]-of-𝐒ᵣ {𝐒 x} {𝐒 y} = [𝄩]-of-𝐒ᵣ {x} {y} ∘ [≤]-without-[𝐒]

[<]-with-[+]ᵣ : ∀{x y z} → (x < y) → (x + z < y + z)
[<]-with-[+]ᵣ = [≤]-with-[+]ᵣ

[<]-with-[+]ₗ : ∀{x y z} → (y < z) → (x + y < x + z)
[<]-with-[+]ₗ {x}{y}{z} = [≤]-with-[+]ₗ {𝐒 y}{z}{x}

[<]-with-[+]-weak : ∀{x₁ x₂ y₁ y₂} → ((x₁ ≤ x₂) ∧ (y₁ < y₂)) ∨ ((x₁ < x₂) ∧ (y₁ ≤ y₂)) → (x₁ + y₁ < x₂ + y₂)
[<]-with-[+]-weak ([∨]-introₗ ([∧]-intro x12 y12)) = [≤]-with-[+] ⦃ x12 ⦄ ⦃ y12 ⦄
[<]-with-[+]-weak ([∨]-introᵣ ([∧]-intro x12 y12)) = [≤]-with-[+] ⦃ x12 ⦄ ⦃ y12 ⦄

[<]-with-[+] : ∀{x₁ x₂ y₁ y₂} → (x₁ < x₂) → (y₁ < y₂) → (x₁ + y₁ < x₂ + y₂)
[<]-with-[+] x12 y12 = [≤]-predecessor ([≤]-with-[+] ⦃ x12 ⦄ ⦃ y12 ⦄)

[≤]-with-[⋅]ᵣ : ∀{a b c} → (a ≤ b) → ((a ⋅ c) ≤ (b ⋅ c))
[≤]-with-[⋅]ᵣ {c = 𝟎}   _  = [≤]-minimum
[≤]-with-[⋅]ᵣ {c = 𝐒 c} ab = [≤]-with-[+] ⦃ ab ⦄ ⦃ [≤]-with-[⋅]ᵣ {c = c} ab ⦄

[≤]-with-[⋅]ₗ : ∀{a b c} → (b ≤ c) → ((a ⋅ b) ≤ (a ⋅ c))
[≤]-with-[⋅]ₗ {a}{b}{c}
  rewrite commutativity(_⋅_) {a}{b}
  rewrite commutativity(_⋅_) {a}{c}
  = [≤]-with-[⋅]ᵣ {c = a}

[<]-with-[⋅]ᵣ : ∀{a b c} → (a < b) → ((a ⋅ 𝐒(c)) < (b ⋅ 𝐒(c)))
[<]-with-[⋅]ᵣ {c = 𝟎}   = id
[<]-with-[⋅]ᵣ {c = 𝐒 c} = [<]-with-[+] ∘ₛ [<]-with-[⋅]ᵣ {c = c}

[<]-with-[⋅]ₗ : ∀{a b c} → (b < c) → ((𝐒(a) ⋅ b) < (𝐒(a) ⋅ c))
[<]-with-[⋅]ₗ {a}{b}{c}
  rewrite commutativity(_⋅_) {𝐒(a)}{b}
  rewrite commutativity(_⋅_) {𝐒(a)}{c}
  = [<]-with-[⋅]ᵣ {c = a}

[⋅]ᵣ-growing : ∀{n c} → (1 ≤ c) → (n ≤ (c ⋅ n))
[⋅]ᵣ-growing {n}{𝐒 c} = [≤]-with-[⋅]ᵣ {1}{𝐒(c)}{n}

[⋅]ᵣ-strictly-growing : ∀{n c} → (2 ≤ c) → (𝐒(n) < (c ⋅ 𝐒(n)))
[⋅]ᵣ-strictly-growing {n} {1} (succ())
[⋅]ᵣ-strictly-growing {n} {𝐒(𝐒 c)} = [<]-with-[⋅]ᵣ {1}{𝐒(𝐒(c))}{n}

[^]-positive : ∀{a b} → ((𝐒(a) ^ b) > 0)
[^]-positive {a}{𝟎} = reflexivity(_≤_)
[^]-positive {a}{𝐒 b} =
  𝐒(a) ^ 𝐒(b)       🝖[ _≥_ ]-[]
  𝐒(a) ⋅ (𝐒(a) ^ b) 🝖[ _≥_ ]-[ [<]-with-[⋅]ₗ {a} ([^]-positive {a}{b}) ]
  𝐒(𝐒(a) ⋅ 0)       🝖[ _≥_ ]-[ succ min ]
  1                 🝖[ _≥_ ]-end

[^]ₗ-strictly-growing : ∀{n a b} → (a < b) → ((𝐒(𝐒(n)) ^ a) < (𝐒(𝐒(n)) ^ b))
[^]ₗ-strictly-growing {n} {𝟎}   {.(𝐒 b)} (succ {y = b} p) = [≤]-with-[+]ᵣ [≤]-minimum 🝖 [≤]-with-[⋅]ₗ {𝐒(𝐒(n))}{1}{𝐒(𝐒(n)) ^ b} ([^]-positive {𝐒(n)}{b})
[^]ₗ-strictly-growing {n} {𝐒 a} {.(𝐒 b)} (succ {y = b} p) = [<]-with-[⋅]ₗ {𝐒(n)} ([^]ₗ-strictly-growing {n}{a}{b} p)

[^]ₗ-growing : ∀{n a b} → ¬((n ≡ 𝟎) ∧ (a ≡ 𝟎)) → (a ≤ b) → ((n ^ a) ≤ (n ^ b))
[^]ₗ-growing {𝟎}  {𝟎}   {_}   p _ with () ← p([∧]-intro [≡]-intro [≡]-intro)
[^]ₗ-growing {𝟎}  {𝐒 a} {𝐒 b} _ _ = min
[^]ₗ-growing {𝐒 𝟎}{a}   {b}   _ _
  rewrite [^]-of-𝟏ₗ {a}
  rewrite [^]-of-𝟏ₗ {b}
  = succ min
[^]ₗ-growing {𝐒 (𝐒 n)}{a}{b} _ ab with [≤]-to-[<][≡] ab
... | [∨]-introₗ p         = sub₂(_<_)(_≤_) ([^]ₗ-strictly-growing {n}{a}{b} p)
... | [∨]-introᵣ [≡]-intro = reflexivity(_≤_)

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:
{-# OPTIONS --without-K #-}

module Pi1 where

open import Data.List
open import Data.Nat
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Groupoid

infix  2  _□
infixr 2  _⟷⟨_⟩_
infix  2  _▤
infixr 2  _⇔⟨_⟩_
infixr 10 _◎_
infix 30 _⟷_
infix  4  _∼_   -- homotopy between two paths
infix  4  _≃_   -- type of equivalences

-- Work on ch. on sets and n-levels and n=-2 and n=-1
-- then work on ch. on equivalences
-- then go back to functions are functors; type families are fibrations
-- then work on int construction
-- then work on example from popl

------------------------------------------------------------------------------
-- Level 0:
-- Types at this level are just plain sets with no interesting path structure.
-- The path structure is defined at levels 1 and beyond.

data U : Set where
  ZERO  : U
  ONE   : U
  PLUS  : U → U → U
  TIMES : U → U → U

⟦_⟧ : U → Set
⟦ ZERO ⟧        = ⊥
⟦ ONE ⟧         = ⊤
⟦ PLUS t₁ t₂ ⟧  = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

-- Programs
-- We use pointed types; programs are "fibers" from functions that map a
-- pointed type to another. In other words, each program takes one particular
-- value to another; if we want to work on another value, we generally use
-- another program.
--
-- We can recover a regular function by collecting all the fibers that
-- compose to the identity permutation.

record U• : Set where
  constructor •[_,_]
  field
    ∣_∣ : U
    • : ⟦ ∣_∣ ⟧

open U•

-- examples of plain types, values, and pointed types

ZERO• : {absurd : ⟦ ZERO ⟧} →  U•
ZERO• {absurd} = •[ ZERO , absurd ]

ONE• : U•
ONE• = •[ ONE , tt ]

BOOL : U
BOOL = PLUS ONE ONE

BOOL² : U
BOOL² = TIMES BOOL BOOL

TRUE : ⟦ BOOL ⟧
TRUE = inj₁ tt

FALSE : ⟦ BOOL ⟧
FALSE = inj₂ tt

BOOL•F : U•
BOOL•F = •[ BOOL , FALSE ]

BOOL•T : U•
BOOL•T = •[ BOOL , TRUE ]

-- The actual programs are the commutative semiring isomorphisms between
-- pointed types.

data _⟷_ : U• → U• → Set where
  unite₊  : ∀ {t v} → •[ PLUS ZERO t , inj₂ v ] ⟷ •[ t , v ]
  uniti₊  : ∀ {t v} → •[ t , v ] ⟷ •[ PLUS ZERO t , inj₂ v ]
  swap1₊  : ∀ {t₁ t₂ v₁} →
            •[ PLUS t₁ t₂ , inj₁ v₁ ] ⟷ •[ PLUS t₂ t₁ , inj₂ v₁ ]
  swap2₊  : ∀ {t₁ t₂ v₂} →
            •[ PLUS t₁ t₂ , inj₂ v₂ ] ⟷ •[ PLUS t₂ t₁ , inj₁ v₂ ]
  assocl1₊ : ∀ {t₁ t₂ t₃ v₁} →
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₁ v₁ ] ⟷
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ]
  assocl2₊ : ∀ {t₁ t₂ t₃ v₂} →
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ] ⟷
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ]
  assocl3₊ : ∀ {t₁ t₂ t₃ v₃} →
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ] ⟷
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ]
  assocr1₊ : ∀ {t₁ t₂ t₃ v₁} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₁ v₁ ]
  assocr2₊ : ∀ {t₁ t₂ t₃ v₂} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ]
  assocr3₊ : ∀ {t₁ t₂ t₃ v₃} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ]
  unite⋆  : ∀ {t v} → •[ TIMES ONE t , (tt , v) ] ⟷ •[ t , v ]
  uniti⋆  : ∀ {t v} → •[ t , v ] ⟷ •[ TIMES ONE t , (tt , v) ]
  swap⋆   : ∀ {t₁ t₂ v₁ v₂} → •[ TIMES t₁ t₂ , (v₁ , v₂) ] ⟷
                              •[ TIMES t₂ t₁ , (v₂ , v₁) ]
  assocl⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            •[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ] ⟷
            •[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ]
  assocr⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            •[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ] ⟷
            •[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ]
  distz : ∀ {t v absurd} →
            •[ TIMES ZERO t , (absurd , v) ] ⟷ •[ ZERO , absurd ]
  factorz : ∀ {t v absurd} →
            •[ ZERO , absurd ] ⟷ •[ TIMES ZERO t , (absurd , v) ]
  dist1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ] ⟷
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ]
  dist2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ] ⟷
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ]
  factor1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ] ⟷
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ]
  factor2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ] ⟷
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ]
  id⟷    : ∀ {t v} → •[ t , v ] ⟷ •[ t , v ]
  _◎_ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
           (•[ t₁ , v₁ ] ⟷ •[ t₂ , v₂ ]) →
           (•[ t₂ , v₂ ] ⟷ •[ t₃ , v₃ ]) →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ])
  ⊕1   : ∀ {t₁ t₂ t₃ t₄ v₁ v₃} →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) →
           (•[ PLUS t₁ t₂ , inj₁ v₁ ] ⟷ •[ PLUS t₃ t₄ , inj₁ v₃ ])
  ⊕2   : ∀ {t₁ t₂ t₃ t₄ v₂ v₄} →
           (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
           (•[ PLUS t₁ t₂ , inj₂ v₂ ] ⟷ •[ PLUS t₃ t₄ , inj₂ v₄ ])
  _⊗_     : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) →
           (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
           (•[ TIMES t₁ t₂ , (v₁ , v₂) ] ⟷ •[ TIMES t₃ t₄ , (v₃ , v₄) ])

-- Nicer syntax that shows intermediate values instead of point-free
-- combinators

_⟷⟨_⟩_ : (t₁ : U•) {t₂ : U•} {t₃ : U•} →
          (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
_ ⟷⟨ α ⟩ β = α ◎ β

_□ : (t : U•) → {t : U•} → (t ⟷ t)
_□ t = id⟷

-- trace
-- first every combinator (t + t1) <-> (t + t2) can be decomposed into
-- four relations (or injective partial functions):
-- r11 : t1 -> t2
-- r12 : t1 -> t
-- r21 : t -> t2
-- r22 : t -> t
-- c = r11 ∪ (r12 ◎ r22⋆ ◎ r21)

eval : ∀ {t₁ t₂ v₁ v₂} → (•[ t₁ , v₁ ] ⟷ •[ t₂ , v₂ ]) → List U•
eval {t₁ = ZERO} {v₁ = ()} _
eval {t₂ = ZERO} {v₂ = ()} _
eval {t} {PLUS .ZERO .t} {v} {inj₂ .v} uniti₊ =
  •[ t , v ] ∷ •[ PLUS ZERO t , inj₂ v ] ∷ []
eval {PLUS .ZERO .t} {t} {inj₂ .v} {v} unite₊ =
  •[ PLUS ZERO t , inj₂ v ] ∷ •[ t , v ] ∷ []
eval {PLUS t₁ t₂} {PLUS .t₂ .t₁} {inj₁ v₁} {inj₂ .v₁} swap1₊ =
  •[ PLUS t₁ t₂ , inj₁ v₁ ] ∷ •[ PLUS t₂ t₁ , inj₂ v₁ ] ∷ []
eval {PLUS t₁ t₂} {PLUS .t₂ .t₁} {inj₂ v₂} {inj₁ .v₂} swap2₊ =
  •[ PLUS t₁ t₂ , inj₂ v₂ ] ∷ •[ PLUS t₂ t₁ , inj₁ v₂ ] ∷ []
eval {PLUS t₁ (PLUS t₂ t₃)} {PLUS (PLUS .t₁ .t₂) .t₃}
     {inj₁ v₁} {inj₁ (inj₁ .v₁)} assocl1₊ =
  •[ PLUS t₁ (PLUS t₂ t₃) , inj₁ v₁ ] ∷
  •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ] ∷ []
eval {PLUS t₁ (PLUS t₂ t₃)} {PLUS (PLUS .t₁ .t₂) .t₃}
     {inj₂ (inj₁ v₂)} {inj₁ (inj₂ .v₂)} assocl2₊ =
  •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ] ∷
  •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ] ∷ []
eval {PLUS t₁ (PLUS t₂ t₃)} {PLUS (PLUS .t₁ .t₂) .t₃}
     {inj₂ (inj₂ v₃)} {inj₂ .v₃} assocl3₊ =
  •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ] ∷
  •[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ] ∷ []
eval {PLUS (PLUS .t₁ .t₂) .t₃} {PLUS t₁ (PLUS t₂ t₃)}
     {inj₁ (inj₁ .v₁)} {inj₁ v₁} assocr1₊ =
  •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ] ∷
  •[ PLUS t₁ (PLUS t₂ t₃) , inj₁ v₁ ] ∷ []
eval {PLUS (PLUS .t₁ .t₂) .t₃} {PLUS t₁ (PLUS t₂ t₃)}
     {inj₁ (inj₂ .v₂)} {inj₂ (inj₁ v₂)} assocr2₊ =
  •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ] ∷
  •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ] ∷ []
eval {PLUS (PLUS .t₁ .t₂) .t₃} {PLUS t₁ (PLUS t₂ t₃)}
     {inj₂ .v₃} {inj₂ (inj₂ v₃)} assocr3₊ =
  •[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ] ∷
  •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ] ∷ []
eval {t} {TIMES .ONE .t} {v} {(tt , .v)} uniti⋆ =
  •[ t , v ] ∷ •[ TIMES ONE t , (tt , v) ] ∷ []
eval {TIMES .ONE .t} {t} {(tt , .v)} {v} unite⋆ =
  •[ TIMES ONE t , (tt , v) ] ∷ •[ t , v ] ∷ []
eval {TIMES t₁ t₂} {TIMES .t₂ .t₁} {(v₁ , v₂)} {(.v₂ , .v₁)} swap⋆ =
  •[ TIMES t₁ t₂ , (v₁ , v₂) ] ∷ •[ TIMES t₂ t₁ , (v₂ , v₁) ] ∷ []
eval {TIMES t₁ (TIMES t₂ t₃)} {TIMES (TIMES .t₁ .t₂) .t₃}
     {(v₁ , (v₂ , v₃))} {((.v₁ , .v₂) , .v₃)} assocl⋆ =
  •[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ] ∷
  •[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ] ∷ []
eval {TIMES (TIMES .t₁ .t₂) .t₃} {TIMES t₁ (TIMES t₂ t₃)}
     {((.v₁ , .v₂) , .v₃)} {(v₁ , (v₂ , v₃))} assocr⋆ =
  •[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ] ∷
  •[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ] ∷ []
eval {TIMES (PLUS t₁ t₂) t₃} {PLUS (TIMES .t₁ .t₃) (TIMES .t₂ .t₃)}
     {(inj₁ v₁ , v₃)} {inj₁ (.v₁ , .v₃)} dist1 =
  •[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ] ∷
  •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ] ∷ []
eval {TIMES (PLUS t₁ t₂) t₃} {PLUS (TIMES .t₁ .t₃) (TIMES .t₂ .t₃)}
     {(inj₂ v₂ , v₃)} {inj₂ (.v₂ , .v₃)} dist2 =
  •[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ] ∷
  •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ] ∷ []
eval {PLUS (TIMES .t₁ .t₃) (TIMES .t₂ .t₃)} {TIMES (PLUS t₁ t₂) t₃}
     {inj₁ (.v₁ , .v₃)} {(inj₁ v₁ , v₃)} factor1 =
  •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ] ∷
  •[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ] ∷ []
eval {PLUS (TIMES .t₁ .t₃) (TIMES .t₂ .t₃)} {TIMES (PLUS t₁ t₂) t₃}
     {inj₂ (.v₂ , .v₃)} {(inj₂ v₂ , v₃)} factor2 =
  •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ] ∷
  •[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ] ∷ []
eval {t} {.t} {v} {.v} id⟷ = •[ t , v ] ∷ •[ t , v ] ∷ []
eval {t₁} {t₃} {v₁} {v₃} (_◎_ {t₂ = t₂} {v₂ = v₂} c₁ c₂) =
  eval {t₁} {t₂} {v₁} {v₂} c₁ ++ eval {t₂} {t₃} {v₂} {v₃} c₂
eval {PLUS t₁ t₂} {PLUS t₃ t₄} {inj₁ v₁} {inj₁ v₃} (⊕1 c) =
  eval {t₁} {t₃} {v₁} {v₃} c -- tag
eval {PLUS t₁ t₂} {PLUS t₃ t₄} {inj₂ v₂} {inj₂ v₄} (⊕2 c) =
  eval {t₂} {t₄} {v₂} {v₄} c -- tag
eval {TIMES t₁ t₂} {TIMES t₃ t₄} {(v₁ , v₂)} {(v₃ , v₄)} (c₁ ⊗ c₂) =
  (eval {t₁} {t₃} {v₁} {v₃} c₁) ++ (eval {t₂} {t₄} {v₂} {v₄} c₂)
  -- zip

test = eval (•[ BOOL² , (TRUE , TRUE) ]
               ⟷⟨ dist1 ⟩
             •[ PLUS (TIMES ONE BOOL) (TIMES ONE BOOL) , inj₁ (tt , TRUE) ]
               ⟷⟨ ⊕1 (id⟷ ⊗ swap1₊)⟩
             •[ PLUS (TIMES ONE BOOL) (TIMES ONE BOOL) , inj₁ (tt , FALSE) ]
               ⟷⟨ factor1 ⟩
             •[ BOOL² , (TRUE , FALSE) ] □)

-- The above are "fibers". We collect the fibers into functions.

data SWAP₊ {t₁ t₂ v₁ v₂} :
  (•[ PLUS t₁ t₂ , inj₁ v₁ ] ⟷ •[ PLUS t₂ t₁ , inj₂ v₁ ]) →
  (•[ PLUS t₁ t₂ , inj₂ v₂ ] ⟷ •[ PLUS t₂ t₁ , inj₁ v₂ ]) →
  Set where
  swap₊ : SWAP₊ swap1₊ swap2₊

Fun : (t₁ t₂ : U) → Set
Fun t₁ t₂ = (v₁ : ⟦ t₁ ⟧) → Σ[ v₂ ∈ ⟦ t₂ ⟧ ] (•[ t₁ , v₁ ] ⟷ •[ t₂ , v₂ ])

NOT : Fun BOOL BOOL
NOT (inj₁ tt) = (FALSE , swap1₊)
NOT (inj₂ tt) = (TRUE  , swap2₊)

-- Note that functions are not reversible!!
Squash : Fun BOOL BOOL
Squash (inj₁ x) = inj₂ x , swap1₊
Squash (inj₂ y) = inj₂ y , id⟷

CNOT : Fun BOOL² BOOL²
CNOT (inj₂ tt , b) =
  ((FALSE , b) , dist2 ◎ (⊕2 id⟷) ◎ factor2)
CNOT (inj₁ tt , inj₂ tt) =
  ((TRUE , TRUE) , dist1 ◎ (⊕1 (id⟷ ⊗ swap2₊)) ◎ factor1)
CNOT (inj₁ tt , inj₁ tt) =
  ((TRUE , FALSE) ,
   (•[ BOOL² , (TRUE , TRUE) ]
      ⟷⟨ dist1 ⟩
    •[ PLUS (TIMES ONE BOOL) (TIMES ONE BOOL) , inj₁ (tt , TRUE) ]
      ⟷⟨ ⊕1 (id⟷ ⊗ swap1₊)⟩
    •[ PLUS (TIMES ONE BOOL) (TIMES ONE BOOL) , inj₁ (tt , FALSE) ]
      ⟷⟨ factor1 ⟩
    •[ BOOL² , (TRUE , FALSE) ] □))

-- The universe of types is a groupoid. The objects of this groupoid are the
-- pointed types; the morphisms are the programs; and the equivalence of
-- programs is the degenerate observational equivalence that equates every
-- two programs that are extensionally equivalent.

! : {t₁ t₂ : U•} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
! unite₊ = uniti₊
! uniti₊ = unite₊
! swap1₊ = swap2₊
! swap2₊ = swap1₊
! assocl1₊ = assocr1₊
! assocl2₊ = assocr2₊
! assocl3₊ = assocr3₊
! assocr1₊ = assocl1₊
! assocr2₊ = assocl2₊
! assocr3₊ = assocl3₊
! unite⋆ = uniti⋆
! uniti⋆ = unite⋆
! swap⋆ = swap⋆
! assocl⋆ = assocr⋆
! assocr⋆ = assocl⋆
! distz = factorz
! factorz = distz
! dist1 = factor1
! dist2 = factor2
! factor1 = dist1
! factor2 = dist2
! id⟷ = id⟷
! (c₁ ◎ c₂) = ! c₂ ◎ ! c₁
! (⊕1 c₁) = ⊕1 (! c₁)
! (⊕2 c₂) = ⊕2 (! c₂)
! (c₁ ⊗ c₂) = ! c₁ ⊗ ! c₂

_obs≅_ : {t₁ t₂ : U•} → (c₁ c₂ : t₁ ⟷ t₂) → Set
c₁ obs≅ c₂ = ⊤

UG : 1Groupoid
UG = record
       { set = U•
       ; _↝_ = _⟷_
       ; _≈_ = _obs≅_
       ; id = id⟷
       ; _∘_ = λ y⟷z x⟷y → x⟷y ◎ y⟷z
       ; _⁻¹ = !
       ; lneutr = λ _ → tt
       ; rneutr = λ _ → tt
       ; assoc = λ _ _ _ → tt
       ; equiv = record { refl = tt
                        ; sym = λ _ → tt
                        ; trans = λ _ _ → tt
                        }
       ; linv = λ _ → tt
       ; rinv = λ _ → tt
       ; ∘-resp-≈ = λ _ _ → tt
       }

-- Now let us talk about homotopies and equivalences

-- Two paths starting at the same point are homotopic if they map that point
-- to related points (of course, related by another path)

_∼_ : {t₁ t₂ t₂' : U•} → (p : t₁ ⟷ t₂) → (q : t₁ ⟷ t₂') → Set
_∼_ {t₁} {t₂} {t₂'} p q = (t₂ ⟷ t₂')

refl∼ : {t₁ t₂ : U•} → (p : t₁ ⟷ t₂) → (p ∼ p)
refl∼ {t₁} {t₂} p = id⟷

sym∼ : {t₁ t₂ t₂' : U•} {p : t₁ ⟷ t₂} {q : t₁ ⟷ t₂'} → (p ∼ q) → (q ∼ p)
sym∼ p∼q = ! p∼q

trans∼ : {t₁ t₂ t₂' t₂'' : U•} {p : t₁ ⟷ t₂} {q : t₁ ⟷ t₂'} {r : t₁ ⟷ t₂''} →
         (p ∼ q) → (q ∼ r) → (p ∼ r)
trans∼ p∼q q∼r = p∼q ◎ q∼r

module T where
  -- Note that paths mapping a point FALSE and TRUE can be homotopic

  p : •[ BOOL , FALSE ] ⟷ •[ BOOL , FALSE ]
  p = id⟷

  q : •[ BOOL , FALSE ] ⟷ •[ BOOL , TRUE ]
  q = swap2₊

  p∼q : p ∼ q
  p∼q = swap2₊

-- equivalences

-- the following makes no sense because I can use id⟷ for α and β

record qinv {t₁ t₂ : U•} (p : t₁ ⟷ t₂) : Set where
  constructor mkqinv
  field
    q : t₂ ⟷ t₁
    α : (p ◎ q) ∼ id⟷
    β : (q ◎ p) ∼ id⟷

idqinv : {t : U•} → qinv {t} {t} id⟷
idqinv = record {
           q = id⟷ ;
           α = id⟷ ;
           β = id⟷
         }

record isequiv {t₁ t₂ : U•} (p : t₁ ⟷ t₂) : Set where
  constructor mkisequiv
  field
    q : t₂ ⟷ t₁
    α : (p ◎ q) ∼ id⟷
    r : t₂ ⟷ t₁
    β : (r ◎ p) ∼ id⟷

equiv₁ : {t₁ t₂ : U•} {p : t₁ ⟷ t₂} → qinv p → isequiv p
equiv₁ (mkqinv iq iα iβ) = mkisequiv iq iα iq iβ

_≃_ : (t₁ t₂ : U•) → Set
t₁ ≃ t₂ = Σ[ p ∈ t₁ ⟷ t₂ ] (isequiv p)

id≃ : {t : U•} → t ≃ t
id≃ = (id⟷ , equiv₁ idqinv)

------------------------------------------------------------------------------
-- Level 1:
-- Types are sets of paths. The paths are defined at level 0.  At level 1,
-- there is no interesting 2path structure. From the perspective of level 0,
-- we have points with non-trivial paths between them, i.e., we have a
-- groupoid. The paths cross type boundaries, i.e., we have heterogeneous
-- equality

-- types

data 1U : Set where
  1ZERO  : 1U              -- empty set of paths
  1ONE   : 1U              -- a trivial path
  1PLUS  : 1U → 1U → 1U      -- disjoint union of paths
  1TIMES : 1U → 1U → 1U      -- pairs of paths
  PATH  : (t₁ t₂ : U•) → 1U -- level 0 paths between values

-- values

data Path (t₁ t₂ : U•) : Set where
  path : (c : t₁ ⟷ t₂) → Path t₁ t₂

1⟦_⟧ : 1U → Set
1⟦ 1ZERO ⟧             = ⊥
1⟦ 1ONE ⟧              = ⊤
1⟦ 1PLUS t₁ t₂ ⟧       = 1⟦ t₁ ⟧ ⊎ 1⟦ t₂ ⟧
1⟦ 1TIMES t₁ t₂ ⟧      = 1⟦ t₁ ⟧ × 1⟦ t₂ ⟧
1⟦ PATH t₁ t₂ ⟧ = Path t₁ t₂

-- examples

T⟷F : Set
T⟷F = Path BOOL•T BOOL•F

F⟷T : Set
F⟷T = Path BOOL•F BOOL•T

p₁ p₂ p₃ p₄ p₅ : T⟷F
p₁ = path swap1₊
p₂ = path (id⟷ ◎ swap1₊)
p₃ = path (swap1₊ ◎ swap2₊ ◎ swap1₊)
p₄ = path (swap1₊ ◎ id⟷)
p₅ = path (uniti⋆ ◎ swap⋆ ◎ (swap1₊ ⊗ id⟷) ◎ swap⋆ ◎ unite⋆)

p₆ : (T⟷F × T⟷F) ⊎ F⟷T
p₆ = inj₁ (p₁ , p₂)

-- Programs map paths to paths. We also use pointed types.

record 1U• : Set where
  constructor 1•[_,_]
  field
    1∣_∣ : 1U
    1• : 1⟦ 1∣_∣ ⟧

open 1U•

data _⇔_ : 1U• → 1U• → Set where
  unite₊  : ∀ {t v} → 1•[ 1PLUS 1ZERO t , inj₂ v ] ⇔ 1•[ t , v ]
  uniti₊  : ∀ {t v} → 1•[ t , v ] ⇔ 1•[ 1PLUS 1ZERO t , inj₂ v ]
  swap1₊  : ∀ {t₁ t₂ v₁} →
            1•[ 1PLUS t₁ t₂ , inj₁ v₁ ] ⇔ 1•[ 1PLUS t₂ t₁ , inj₂ v₁ ]
  swap2₊  : ∀ {t₁ t₂ v₂} →
            1•[ 1PLUS t₁ t₂ , inj₂ v₂ ] ⇔ 1•[ 1PLUS t₂ t₁ , inj₁ v₂ ]
  assocl1₊ : ∀ {t₁ t₂ t₃ v₁} →
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₁ v₁ ] ⇔
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ]
  assocl2₊ : ∀ {t₁ t₂ t₃ v₂} →
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₂ (inj₁ v₂) ] ⇔
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ]
  assocl3₊ : ∀ {t₁ t₂ t₃ v₃} →
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₂ (inj₂ v₃) ] ⇔
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₂ v₃ ]
  assocr1₊ : ∀ {t₁ t₂ t₃ v₁} →
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ] ⇔
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₁ v₁ ]
  assocr2₊ : ∀ {t₁ t₂ t₃ v₂} →
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ] ⇔
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₂ (inj₁ v₂) ]
  assocr3₊ : ∀ {t₁ t₂ t₃ v₃} →
             1•[ 1PLUS (1PLUS t₁ t₂) t₃ , inj₂ v₃ ] ⇔
             1•[ 1PLUS t₁ (1PLUS t₂ t₃) , inj₂ (inj₂ v₃) ]
  unite⋆  : ∀ {t v} → 1•[ 1TIMES 1ONE t , (tt , v) ] ⇔ 1•[ t , v ]
  uniti⋆  : ∀ {t v} → 1•[ t , v ] ⇔ 1•[ 1TIMES 1ONE t , (tt , v) ]
  swap⋆   : ∀ {t₁ t₂ v₁ v₂} →
              1•[ 1TIMES t₁ t₂ , (v₁ , v₂) ] ⇔ 1•[ 1TIMES t₂ t₁ , (v₂ , v₁) ]
  assocl⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            1•[ 1TIMES t₁ (1TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ] ⇔
            1•[ 1TIMES (1TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ]
  assocr⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            1•[ 1TIMES (1TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ] ⇔
            1•[ 1TIMES t₁ (1TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ]
  distz : ∀ {t v absurd} →
            1•[ 1TIMES 1ZERO t , (absurd , v) ] ⇔ 1•[ 1ZERO , absurd ]
  factorz : ∀ {t v absurd} →
            1•[ 1ZERO , absurd ] ⇔ 1•[ 1TIMES 1ZERO t , (absurd , v) ]
  dist1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            1•[ 1TIMES (1PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ] ⇔
            1•[ 1PLUS (1TIMES t₁ t₃) (1TIMES t₂ t₃) , inj₁ (v₁ , v₃) ]
  dist2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            1•[ 1TIMES (1PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ] ⇔
            1•[ 1PLUS (1TIMES t₁ t₃) (1TIMES t₂ t₃) , inj₂ (v₂ , v₃) ]
  factor1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            1•[ 1PLUS (1TIMES t₁ t₃) (1TIMES t₂ t₃) , inj₁ (v₁ , v₃) ] ⇔
            1•[ 1TIMES (1PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ]
  factor2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            1•[ 1PLUS (1TIMES t₁ t₃) (1TIMES t₂ t₃) , inj₂ (v₂ , v₃) ] ⇔
            1•[ 1TIMES (1PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ]
  id⇔    : ∀ {t v} → 1•[ t , v ] ⇔ 1•[ t , v ]
  _◎_    : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} → (1•[ t₁ , v₁ ] ⇔ 1•[ t₂ , v₂ ]) →
           (1•[ t₂ , v₂ ] ⇔ 1•[ t₃ , v₃ ]) →
           (1•[ t₁ , v₁ ] ⇔ 1•[ t₃ , v₃ ])
  ⊕1   : ∀ {t₁ t₂ t₃ t₄ v₁ v₃} →
           (1•[ t₁ , v₁ ] ⇔ 1•[ t₃ , v₃ ]) →
           (1•[ 1PLUS t₁ t₂ , inj₁ v₁ ] ⇔ 1•[ 1PLUS t₃ t₄ , inj₁ v₃ ])
  ⊕2   : ∀ {t₁ t₂ t₃ t₄ v₂ v₄} →
           (1•[ t₂ , v₂ ] ⇔ 1•[ t₄ , v₄ ]) →
           (1•[ 1PLUS t₁ t₂ , inj₂ v₂ ] ⇔ 1•[ 1PLUS t₃ t₄ , inj₂ v₄ ])
  _⊗_     : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (1•[ t₁ , v₁ ] ⇔ 1•[ t₃ , v₃ ]) → (1•[ t₂ , v₂ ] ⇔ 1•[ t₄ , v₄ ]) →
          (1•[ 1TIMES t₁ t₂ , (v₁ , v₂) ] ⇔ 1•[ 1TIMES t₃ t₄ , (v₃ , v₄) ])
  lidl : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂} →
        1•[ PATH t₁ t₂ , path (id⟷ ◎ c) ] ⇔ 1•[ PATH t₁ t₂ , path c ]
  lidr : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂} →
        1•[ PATH t₁ t₂ , path c ] ⇔ 1•[ PATH t₁ t₂ , path (id⟷ ◎ c) ]
  ridl : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂} →
        1•[ PATH t₁ t₂ , path (c ◎ id⟷) ] ⇔ 1•[ PATH t₁ t₂ , path c ]
  ridr : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂} →
        1•[ PATH t₁ t₂ , path c ] ⇔ 1•[ PATH t₁ t₂ , path (c ◎ id⟷) ]
  assocl : ∀ {t₁ t₂ t₃ t₄}  →
          {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₃ ⟷ t₄} →
          1•[ PATH t₁ t₄ , path (c₁ ◎ (c₂ ◎ c₃)) ] ⇔
          1•[ PATH t₁ t₄ , path ((c₁ ◎ c₂) ◎ c₃) ]
  assocr : ∀ {t₁ t₂ t₃ t₄}  →
          {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₃ ⟷ t₄} →
          1•[ PATH t₁ t₄ , path ((c₁ ◎ c₂) ◎ c₃) ] ⇔
          1•[ PATH t₁ t₄ , path (c₁ ◎ (c₂ ◎ c₃)) ]
  linv◎l : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂ } →
          1•[ PATH t₁ t₁ , path (c ◎ ! c)] ⇔
          1•[ PATH t₁ t₁ , path id⟷ ]
  linv◎r : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂ } →
          1•[ PATH t₁ t₁ , path id⟷ ] ⇔
          1•[ PATH t₁ t₁ , path (c ◎ ! c) ]
  rinv◎l : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂ } →
          1•[ PATH t₂ t₂ , path (! c ◎ c)] ⇔
          1•[ PATH t₂ t₂ , path id⟷ ]
  rinv◎r : ∀ {t₁ t₂} → {c : t₁ ⟷ t₂ } →
          1•[ PATH t₂ t₂ , path id⟷ ] ⇔
          1•[ PATH t₂ t₂ , path (! c ◎ c) ]
  resp◎   : ∀ {t₁ t₂ t₃} →
           {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₁ ⟷ t₂} {c₄ : t₂ ⟷ t₃} →
           (1•[ PATH t₁ t₂ , path c₁ ] ⇔ 1•[ PATH t₁ t₂ , path c₃ ]) →
           (1•[ PATH t₂ t₃ , path c₂ ] ⇔ 1•[ PATH t₂ t₃ , path c₄ ]) →
           1•[ PATH t₁ t₃ , path (c₁ ◎ c₂) ] ⇔ 1•[ PATH t₁ t₃ , path (c₃ ◎ c₄) ]

1! : {t₁ t₂ : 1U•} → (t₁ ⇔ t₂) → (t₂ ⇔ t₁)
1! unite₊ = uniti₊
1! uniti₊ = unite₊
1! swap1₊ = swap2₊
1! swap2₊ = swap1₊
1! assocl1₊ = assocr1₊
1! assocl2₊ = assocr2₊
1! assocl3₊ = assocr3₊
1! assocr1₊ = assocl1₊
1! assocr2₊ = assocl2₊
1! assocr3₊ = assocl3₊
1! unite⋆ = uniti⋆
1! uniti⋆ = unite⋆
1! swap⋆ = swap⋆
1! assocl⋆ = assocr⋆
1! assocr⋆ = assocl⋆
1! distz = factorz
1! factorz = distz
1! dist1 = factor1
1! dist2 = factor2
1! factor1 = dist1
1! factor2 = dist2
1! id⇔ = id⇔
1! (c₁ ◎ c₂) = 1! c₂ ◎ 1! c₁
1! (⊕1 c₁) = ⊕1 (1! c₁)
1! (⊕2 c₂) = ⊕2 (1! c₂)
1! (c₁ ⊗ c₂) = 1! c₁ ⊗ 1! c₂
1! (resp◎ c₁ c₂) = resp◎ (1! c₁) (1! c₂)
1! ridl = ridr
1! ridr = ridl
1! lidl = lidr
1! lidr = lidl
1! assocl = assocr
1! assocr = assocl
1! linv◎l = linv◎r
1! linv◎r = linv◎l
1! rinv◎l = rinv◎r
1! rinv◎r = rinv◎l

1!≡ : {t₁ t₂ : 1U•} → (c : t₁ ⇔ t₂) → 1! (1! c) ≡ c
1!≡ unite₊ = refl
1!≡ uniti₊ = refl
1!≡ swap1₊ = refl
1!≡ swap2₊ = refl
1!≡ assocl1₊ = refl
1!≡ assocl2₊ = refl
1!≡ assocl3₊ = refl
1!≡ assocr1₊ = refl
1!≡ assocr2₊ = refl
1!≡ assocr3₊ = refl
1!≡ unite⋆ = refl
1!≡ uniti⋆ = refl
1!≡ swap⋆ = refl
1!≡ assocl⋆ = refl
1!≡ assocr⋆ = refl
1!≡ distz = refl
1!≡ factorz = refl
1!≡ dist1 = refl
1!≡ dist2 = refl
1!≡ factor1 = refl
1!≡ factor2 = refl
1!≡ id⇔ = refl
1!≡ (c₁ ◎ c₂) = cong₂ (λ c₁ c₂ → c₁ ◎ c₂) (1!≡ c₁) (1!≡ c₂)
1!≡ (⊕1 c₁) = cong (λ c₁ → ⊕1 c₁) (1!≡ c₁)
1!≡ (⊕2 c₂) = cong (λ c₂ → ⊕2 c₂) (1!≡ c₂)
1!≡ (c₁ ⊗ c₂) = cong₂ (λ c₁ c₂ → c₁ ⊗ c₂) (1!≡ c₁) (1!≡ c₂)
1!≡ lidl = refl
1!≡ lidr = refl
1!≡ ridl = refl
1!≡ ridr = refl
1!≡ (resp◎ c₁ c₂) = cong₂ (λ c₁ c₂ → resp◎ c₁ c₂) (1!≡ c₁) (1!≡ c₂)
1!≡ assocl = refl
1!≡ assocr = refl
1!≡ linv◎l = refl
1!≡ linv◎r = refl
1!≡ rinv◎l = refl
1!≡ rinv◎r = refl

-- better syntax for writing 2paths

_⇔⟨_⟩_ : {t₁ t₂ : U•} (c₁ : t₁ ⟷ t₂) {c₂ : t₁ ⟷ t₂} {c₃ : t₁ ⟷ t₂} →
         (1•[ PATH t₁ t₂ , path c₁ ] ⇔ 1•[ PATH t₁ t₂ , path c₂ ]) →
         (1•[ PATH t₁ t₂ , path c₂ ] ⇔ 1•[ PATH t₁ t₂ , path c₃ ]) →
         (1•[ PATH t₁ t₂ , path c₁ ] ⇔ 1•[ PATH t₁ t₂ , path c₃ ])
_ ⇔⟨ α ⟩ β = α ◎ β

_▤ : {t₁ t₂ : U•} → (c : t₁ ⟷ t₂) →
     1•[ PATH t₁ t₂ , path c ] ⇔ 1•[ PATH t₁ t₂ , path c ]
_▤ c = id⇔

α₁ : 1•[ PATH BOOL•T BOOL•F , p₁ ] ⇔ 1•[ PATH BOOL•T BOOL•F , p₁ ]
α₁ = id⇔

α₂ : 1•[ PATH BOOL•T BOOL•F , p₁ ] ⇔ 1•[ PATH BOOL•T BOOL•F , p₂ ]
α₂ = lidr

-- level 0 is a groupoid with a non-trivial path equivalence the various inv*
-- rules are not justified by the groupoid proof; they are justified by the
-- need for computational rules. So it is important to have not just a
-- groupoid structure but a groupoid structure that we can compute with. So
-- if we say that we want p ◎ p⁻¹ to be id, we must have computational rules
-- that allow us to derive this for any path p, and similarly for all the
-- other groupoid rules. (cf. The canonicity for 2D type theory by Licata and
-- Harper)

G : 1Groupoid
G = record
        { set = U•
        ; _↝_ = _⟷_
        ; _≈_ = λ {t₁} {t₂} c₀ c₁ →
                1•[ PATH t₁ t₂ , path c₀ ] ⇔ 1•[ PATH t₁ t₂ , path c₁ ]
        ; id = id⟷
        ; _∘_ = λ c₀ c₁ → c₁ ◎ c₀
        ; _⁻¹ = !
        ; lneutr = λ _ → ridl
        ; rneutr = λ _ → lidl
        ; assoc = λ _ _ _ → assocl
        ; equiv = record { refl = id⇔
                                ; sym = λ c → 1! c
                                ; trans = λ c₀ c₁ → c₀ ◎ c₁ }
        ; linv = λ {t₁} {t₂} c → linv◎l
        ; rinv = λ {t₁} {t₂} c → rinv◎l
        ; ∘-resp-≈ = λ f⟷h g⟷i → resp◎ g⟷i f⟷h
        }

-- We can now ask whether a given space is a set (Def. 3.1.1)

isSet : U → Set
isSet t = (v v' : ⟦ t ⟧) → (p q : •[ t , v ] ⟷ •[ t , v' ]) →
          (1•[ PATH •[ t , v ] •[ t , v' ] , path p ] ⇔
           1•[ PATH •[ t , v ] •[ t , v' ] , path q ])

0isSet : isSet ZERO
0isSet ()

1isSet : isSet ONE
1isSet tt tt id⟷ id⟷ = id⇔
1isSet tt tt id⟷ (uniti₊ ◎ unite₊) =
  id⟷
    ⇔⟨ rinv◎r ⟩
  uniti₊ ◎ unite₊ ▤
1isSet tt tt id⟷ (uniti₊ ◎ (q₂ ◎ q₃)) =
  id⟷
    ⇔⟨ {!!} ⟩
  (uniti₊ ◎ (q₂ ◎ q₃)) ▤
1isSet tt tt id⟷ (uniti⋆ ◎ unite⋆) = {!!}
1isSet tt tt id⟷ (uniti⋆ ◎ (q₂ ◎ q₃)) = {!!}
1isSet tt tt id⟷ (id⟷ ◎ id⟷) = {!!}
1isSet tt tt id⟷ (id⟷ ◎ (q₂ ◎ q₃)) = {!!}
1isSet tt tt id⟷ ((q₁ ◎ q₂) ◎ unite₊) = {!!}
1isSet tt tt id⟷ ((q₁ ◎ q₂) ◎ unite⋆) = {!!}
1isSet tt tt id⟷ ((q₁ ◎ q₂) ◎ id⟷) = {!!}
1isSet tt tt id⟷ ((q₁ ◎ q₂) ◎ (q₃ ◎ q₄)) = {!!}
1isSet tt tt (p₁ ◎ p₂) id⟷ = {!!}
1isSet tt tt (p₁ ◎ p₂) (q₁ ◎ q₂) = {!!}

------------------------------------------------------------------------------
-- Level 2 etc.

data 2U : Set where
  2ZERO  : 2U
  2ONE   : 2U
  2PLUS  : 2U → 2U → 2U
  2TIMES : 2U → 2U → 2U
  1PATH  : (t₁ t₂ : 1U•) → 2U

data 1Path (t₁ t₂ : 1U•) : Set where
  1path : (c : t₁ ⇔ t₂) → 1Path t₁ t₂

2⟦_⟧ : 2U → Set
2⟦ 2ZERO ⟧             = ⊥
2⟦ 2ONE ⟧              = ⊤
2⟦ 2PLUS t₁ t₂ ⟧       = 2⟦ t₁ ⟧ ⊎ 2⟦ t₂ ⟧
2⟦ 2TIMES t₁ t₂ ⟧      = 2⟦ t₁ ⟧ × 2⟦ t₂ ⟧
2⟦ 1PATH t₁ t₂ ⟧ = 1Path t₁ t₂

record 2U• : Set where
  constructor 2•[_,_]
  field
    2∣_∣ : 2U
    2•   : 2⟦ 2∣_∣ ⟧

data _2⇔_ : 2U• → 2U• → Set where
  id2⇔    : ∀ {t v} → 2•[ t , v ] 2⇔ 2•[ t , v ]
 -- and all the remaining combinators...

-- Eckmann-Hilton

Ω : (t : U) → {v : ⟦ t ⟧} → 1U•
Ω t {v} = 1•[ PATH t• t• , path id⟷ ]
  where t• = •[ t , v ]

Ω² : (t : U) → {v : ⟦ t ⟧} → 2U•
Ω² t {v} = 2•[ 1PATH t• t• , 1path id⇔ ]
  where t• = Ω t {v}

eckmann-hilton : {t : U} {v : ⟦ t ⟧} (α β : (Ω t {v}) ⇔ (Ω t {v})) →
  (2•[ 1PATH (Ω t {v}) (Ω t {v}) , 1path (α ◎ β) ] 2⇔
   2•[ 1PATH (Ω t {v}) (Ω t {v}) , 1path (β ◎ α) ])
eckmann-hilton {t} {v} α β = {!!}

------------------------------------------------------------------------------
-- Int construction

-- Types are of the form t - t'

record Uℤ : Set where
  constructor _-_
  field
    pos  : U
    neg  : U

open Uℤ

ZEROℤ ONEℤ : Uℤ
ZEROℤ = ZERO - ZERO
ONEℤ  = ONE  - ZERO

PLUSℤ : Uℤ → Uℤ → Uℤ
PLUSℤ (pos₁ - neg₁) (pos₂ - neg₂) = PLUS pos₁ pos₂ - PLUS neg₁ neg₂

TIMESℤ : Uℤ → Uℤ → Uℤ
TIMESℤ (pos₁ - neg₁) (pos₂ - neg₂) =
  PLUS (TIMES pos₁ pos₂) (TIMES neg₁ neg₂) -
  PLUS (TIMES pos₁ neg₂) (TIMES neg₁ pos₂)

FLIPℤ : Uℤ → Uℤ
FLIPℤ (pos - neg) = neg - pos

LOLLIℤ : Uℤ → Uℤ → Uℤ
LOLLIℤ (pos₁ - neg₁) (pos₂ - neg₂) = PLUS neg₁ pos₂ - PLUS pos₁ neg₂

-- Pointed types

data Uℤ• : Set where
  pos• : (t : Uℤ) → ⟦ pos t ⟧ → Uℤ•
  neg• : (t : Uℤ) → ⟦ neg t ⟧ → Uℤ•

ZEROℤ+• : {t : U} {v : ⟦ t ⟧} → Uℤ•
ZEROℤ+• {t} {v} = pos• (t - t) v

ZEROℤ-• : {t : U} {v : ⟦ t ⟧} → Uℤ•
ZEROℤ-• {t} {v} = neg• (t - t) v

PLUS1ℤ• : Uℤ• → Uℤ → Uℤ•
PLUS1ℤ• (pos• t₁ v₁) t₂ = pos• (PLUSℤ t₁ t₂) (inj₁ v₁)
PLUS1ℤ• (neg• t₁ v₁) t₂ = neg• (PLUSℤ t₁ t₂) (inj₁ v₁)

PLUS2ℤ• : Uℤ → Uℤ• → Uℤ•
PLUS2ℤ• t₁ (pos• t₂ v₂) = pos• (PLUSℤ t₁ t₂) (inj₂ v₂)
PLUS2ℤ• t₁ (neg• t₂ v₂) = neg• (PLUSℤ t₁ t₂) (inj₂ v₂)

-- Combinators on pointed types

data _⇄_ : Uℤ• → Uℤ• → Set where
  Fwd : ∀ {t₁ t₂ t₃ t₄ v₁ v₃} →
        •[ PLUS t₁ t₄ , inj₁ v₁ ] ⟷ •[ PLUS t₂ t₃ , inj₂ v₃ ] →
        pos• (t₁ - t₂) v₁ ⇄ pos• (t₃ - t₄) v₃
  Bck : ∀ {t₁ t₂ t₃ t₄ v₂ v₄} →
        •[ PLUS t₁ t₄ , inj₂ v₄ ] ⟷ •[ PLUS t₂ t₃ , inj₁ v₂ ] →
        neg• (t₁ - t₂) v₂ ⇄ neg• (t₃ - t₄) v₄
  B2F : ∀ {t v} → neg• (t - t) v ⇄ pos• (t - t) v
  F2B : ∀ {t v} → pos• (t - t) v ⇄ neg• (t - t) v

unite₊⇄ : {t : Uℤ•} → PLUS2ℤ• ZEROℤ t ⇄ t
unite₊⇄ {pos• t v} =
  Fwd (•[ PLUS (PLUS ZERO (pos t)) (neg t) , inj₁ (inj₂ v) ]
         ⟷⟨ assocr2₊ ⟩
       •[ PLUS ZERO (PLUS (pos t) (neg t)) , inj₂ (inj₁ v) ]
         ⟷⟨ unite₊ ◎ swap1₊ ⟩
       •[ PLUS (neg t) (pos t) , inj₂ v ]
         ⟷⟨ uniti₊ ⟩
       •[ PLUS ZERO (PLUS (neg t) (pos t)) , inj₂ (inj₂ v) ]
         ⟷⟨ assocl3₊ ⟩
       •[ PLUS (PLUS ZERO (neg t)) (pos t) , inj₂ v ] □)
unite₊⇄ {neg• t v} =
  Bck (•[ PLUS (PLUS ZERO (pos t)) (neg t) , inj₂ v ]
         ⟷⟨ assocr3₊ ⟩
       •[ PLUS ZERO (PLUS (pos t) (neg t)) , inj₂ (inj₂ v) ]
         ⟷⟨ unite₊ ◎ swap2₊ ◎ uniti₊ ⟩
       •[ PLUS ZERO (PLUS (neg t) (pos t)) , inj₂ (inj₁ v) ]
         ⟷⟨ assocl2₊ ⟩
       •[ PLUS (PLUS ZERO (neg t)) (pos t) , inj₁ (inj₂ v) ] □)

uniti₊⇄ : {t : Uℤ•} → t ⇄ PLUS2ℤ• ZEROℤ t
uniti₊⇄ {pos• t v} =
  Fwd (•[ PLUS (pos t) (PLUS ZERO (neg t)) , inj₁ v ]
        ⟷⟨ assocl1₊ ⟩
       •[ PLUS (PLUS (pos t) ZERO) (neg t) , inj₁ (inj₁ v) ]
        ⟷⟨ swap1₊ ⟩
       •[ PLUS (neg t) (PLUS (pos t) ZERO) , inj₂ (inj₁ v) ]
        ⟷⟨ ⊕2 swap1₊ ⟩
       •[ PLUS (neg t) (PLUS ZERO (pos t)) , inj₂ (inj₂ v) ] □)
uniti₊⇄ {neg• t v} =
  Bck (•[ PLUS (pos t) (PLUS ZERO (neg t)) , inj₂ (inj₂ v) ]
        ⟷⟨ ⊕2 swap2₊ ⟩
       •[ PLUS (pos t) (PLUS (neg t) ZERO) , inj₂ (inj₁ v) ]
        ⟷⟨ swap2₊ ⟩
       •[ PLUS (PLUS (neg t) ZERO) (pos t) , inj₁ (inj₁ v) ]
        ⟷⟨ assocr1₊ ⟩
       •[ PLUS (neg t) (PLUS ZERO (pos t)) , inj₁ v ] □)

swap1₊⇄ : {t₁ : Uℤ•} {t₂ : Uℤ} → PLUS1ℤ• t₁ t₂ ⇄ PLUS2ℤ• t₂ t₁
swap1₊⇄ {pos• t₁ v₁} {t₂} =
  Fwd (•[ PLUS (PLUS (pos t₁) (pos t₂)) (PLUS (neg t₂) (neg t₁)) ,
          inj₁ (inj₁ v₁) ]
        ⟷⟨ {!!} ⟩
       •[ PLUS (PLUS (neg t₁) (neg t₂)) (PLUS (pos t₂) (pos t₁)) ,
          inj₂ (inj₂ v₁) ] □)
swap1₊⇄ {neg• t₁ v₁} {t₂} =
  Bck (•[ PLUS (PLUS (pos t₁) (pos t₂)) (PLUS (neg t₂) (neg t₁)) ,
          inj₂ (inj₂ v₁) ]
        ⟷⟨ {!!} ⟩
       •[ PLUS (PLUS (neg t₁) (neg t₂)) (PLUS (pos t₂) (pos t₁)) ,
          inj₁ (inj₁ v₁) ] □)

swap2₊⇄ : {t₁ : Uℤ} {t₂ : Uℤ•} → PLUS2ℤ• t₁ t₂ ⇄ PLUS1ℤ• t₂ t₁
swap2₊⇄ {t₁} {pos• t₂ v₂} =
  Fwd (•[ PLUS (PLUS (pos t₁) (pos t₂)) (PLUS (neg t₂) (neg t₁)) ,
          inj₁ (inj₂ v₂) ]
        ⟷⟨ {!!} ⟩
       •[ PLUS (PLUS (neg t₁) (neg t₂)) (PLUS (pos t₂) (pos t₁)) ,
          inj₂ (inj₁ v₂) ] □)
swap2₊⇄ {t₁} {neg• t₂ v₂} =
  Bck (•[ PLUS (PLUS (pos t₁) (pos t₂)) (PLUS (neg t₂) (neg t₁)) ,
          inj₂ (inj₁ v₂) ]
        ⟷⟨ {!!} ⟩
       •[ PLUS (PLUS (neg t₁) (neg t₂)) (PLUS (pos t₂) (pos t₁)) ,
          inj₁ (inj₂ v₂) ] □)

assocl1₊⇄ : {t₁ : Uℤ•} {t₂ t₃ : Uℤ} →
            PLUS1ℤ• t₁ (PLUSℤ t₂ t₃) ⇄ PLUS1ℤ• (PLUS1ℤ• t₁ t₂) t₃
assocl1₊⇄ {pos• t₁ v₁} {t₂} {t₃} =
  Fwd (•[ PLUS (PLUS (pos t₁) (pos (PLUSℤ t₂ t₃)))
               (PLUS (neg (PLUSℤ t₁ t₂)) (neg t₃)) ,
          inj₁ (inj₁ v₁) ]
        ⟷⟨ {!!} ⟩
       •[ PLUS (PLUS (neg t₁) (neg (PLUSℤ t₂ t₃)))
               (PLUS (pos (PLUSℤ t₁ t₂)) (pos t₃)) ,
          inj₂ (inj₁ (inj₁ v₁)) ] □)
assocl1₊⇄ {neg• t₁ v₁} {t₂} {t₃} =
  Bck (•[ PLUS (PLUS (pos t₁) (pos (PLUSℤ t₂ t₃)))
               (PLUS (neg (PLUSℤ t₁ t₂)) (neg t₃)) ,
          inj₂ (inj₁ (inj₁ v₁)) ]
        ⟷⟨ {!!} ⟩
       •[ PLUS (PLUS (neg t₁) (neg (PLUSℤ t₂ t₃)))
               (PLUS (pos (PLUSℤ t₁ t₂)) (pos t₃)) ,
          inj₁ (inj₁ v₁) ] □)

{--
  assocl2₊ : ∀ {t₁ t₂ t₃ v₂} →
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ] ⟷
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ]
  assocl3₊ : ∀ {t₁ t₂ t₃ v₃} →
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ] ⟷
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ]
  assocr1₊ : ∀ {t₁ t₂ t₃ v₁} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₁ v₁) ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₁ v₁ ]
  assocr2₊ : ∀ {t₁ t₂ t₃ v₂} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₁ (inj₂ v₂) ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₁ v₂) ]
  assocr3₊ : ∀ {t₁ t₂ t₃ v₃} →
             •[ PLUS (PLUS t₁ t₂) t₃ , inj₂ v₃ ] ⟷
             •[ PLUS t₁ (PLUS t₂ t₃) , inj₂ (inj₂ v₃) ]
  unite⋆  : ∀ {t v} → •[ TIMES ONE t , (tt , v) ] ⟷ •[ t , v ]
  uniti⋆  : ∀ {t v} → •[ t , v ] ⟷ •[ TIMES ONE t , (tt , v) ]
  swap⋆   : ∀ {t₁ t₂ v₁ v₂} →
              •[ TIMES t₁ t₂ , (v₁ , v₂) ] ⟷ •[ TIMES t₂ t₁ , (v₂ , v₁) ]
  assocl⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            •[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ] ⟷
            •[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ]
  assocr⋆ : ∀ {t₁ t₂ t₃ v₁ v₂ v₃} →
            •[ TIMES (TIMES t₁ t₂) t₃ , ((v₁ , v₂) , v₃) ] ⟷
            •[ TIMES t₁ (TIMES t₂ t₃) , (v₁ , (v₂ , v₃)) ]
  distz : ∀ {t v absurd} →
            •[ TIMES ZERO t , (absurd , v) ] ⟷ •[ ZERO , absurd ]
  factorz : ∀ {t v absurd} →
            •[ ZERO , absurd ] ⟷ •[ TIMES ZERO t , (absurd , v) ]
  dist1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ] ⟷
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ]
  dist2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ] ⟷
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ]
  factor1   : ∀ {t₁ t₂ t₃ v₁ v₃} →
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₁ (v₁ , v₃) ] ⟷
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₁ v₁ , v₃) ]
  factor2   : ∀ {t₁ t₂ t₃ v₂ v₃} →
            •[ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) , inj₂ (v₂ , v₃) ] ⟷
            •[ TIMES (PLUS t₁ t₂) t₃ , (inj₂ v₂ , v₃) ]
--}

id⇄ : {t : Uℤ•} → t ⇄ t
id⇄ {pos• t p} = Fwd swap1₊
id⇄ {neg• t n} = Bck swap2₊

{--
_◎⇄_ : {t₁ t₂ t₃ : Uℤ•} → (t₁ ⇄ t₂) → (t₂ ⇄ t₃) → (t₁ ⇄ t₃)
_◎⇄_ {pos• t₁ v₁} {pos• t₂ v₂} {pos• t₃ v₃} (Fwd c₁) (Fwd c₂) =
  Fwd (•[ PLUS (pos t₁) (neg t₃) , inj₁ v₁ ]
        ⟷⟨ {!!} ⟩
       •[ PLUS (neg t₁) (pos t₃) , inj₂ v₃ ] □)
-- c₁ : •[ PLUS (pos t₁) (neg t₂) , inj₁ v₁ ] ⟷
--      •[ PLUS (neg t₁) (pos t₂) , inj₂ v₂ ]
-- c₂ : •[ PLUS (pos t₂) (neg t₃) , inj₁ v₂ ] ⟷
--      •[ PLUS (neg t₂) (pos t₃) , inj₂ v₃ ]
_◎⇄_ {pos• (t₁ - t₂) v₁} {pos• (t₃ - .t₃) v₃} {neg• (.t₃ - .t₃) .v₃}
     (Fwd c) F2B = {!!}
-- ?7 : pos• (t₁ - t₂) v₁ ⇄ neg• (t₃ - t₃) v₃
Bck c₁ ◎⇄ Bck c₂ = Bck {!!}
Bck c ◎⇄ B2F     = {!!}
B2F ◎⇄ Fwd c     = {!!}
B2F ◎⇄ F2B       = id⇄
F2B ◎⇄ Bck c     = {!!}
F2B ◎⇄ B2F       = id⇄
--}

{--
  _⊕1_   : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
           (•[ PLUS t₁ t₂ , inj₁ v₁ ] ⟷ •[ PLUS t₃ t₄ , inj₁ v₃ ])
  _⊕2_   : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
           (•[ PLUS t₁ t₂ , inj₂ v₂ ] ⟷ •[ PLUS t₃ t₄ , inj₂ v₄ ])
  _⊗_     : ∀ {t₁ t₂ t₃ t₄ v₁ v₂ v₃ v₄} →
           (•[ t₁ , v₁ ] ⟷ •[ t₃ , v₃ ]) → (•[ t₂ , v₂ ] ⟷ •[ t₄ , v₄ ]) →
          (•[ TIMES t₁ t₂ , (v₁ , v₂) ] ⟷ •[ TIMES t₃ t₄ , (v₃ , v₄) ])
--}

-- trace

η : ∀ {t v} → ZEROℤ+• {t} {v} ⇄ ZEROℤ-• {t} {v}
η = F2B

ε : ∀ {t v} → ZEROℤ-• {t} {v} ⇄ ZEROℤ+• {t} {v}
ε = B2F

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

variable
  ℓ : Level
  A  : Set ℓ
  n  : Nat

infixr 4 _∷_

data Vec (A : Set) : Nat → Set where
  []  : Vec A 0
  _∷_ : A → Vec A n → Vec A (suc n)

variable
  xs : Vec A n

data T (n : Nat) (f : Nat → Nat) : Set where
  it : T n f

appT : ∀ {f} → T n f → Nat
appT {n = n} {f = f} it = f n

length : Vec A n → Nat
length {n = n} _ = n

-- This should not break.
bar : (xs : Vec Nat n) → T n λ { m → m + length xs }
bar xs = it

ys : Vec Nat 5
ys = 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []

-- Check that it doesn't
no-fail : appT (bar ys) ≡ 10
no-fail = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}
postulate
  Foo : Set

record BaseT : Set₁ where
  field f : Foo

record ParamT (p : Foo) : Set₁ where
  field f : Foo

instance
  postulate asBaseT : ∀ {p} → ParamT p → BaseT
--  BaseT.f (asBaseT p) = ParamT.f p

data Bar : Set where
  o : Bar

data Baz {{_ : BaseT}} : Bar → Set where
  t1 : Baz o
  t2 : Baz o → Baz o
  t3 : Baz o → Baz o → Baz o
  t4 : Baz o → Baz o → Baz o → Baz o

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Experiments.NatMinusTwo.ToNatMinusOne where

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

open import Cubical.Data.NatMinusOne as ℕ₋₁ using (ℕ₋₁)
open import Cubical.Experiments.NatMinusTwo.Base as ℕ₋₂ using (ℕ₋₂; -2+_)

-- Conversions to/from ℕ₋₁

-1+_ : ℕ₋₁ → ℕ₋₂
-1+ (ℕ₋₁.-1+ n) = -2+ n

1+_ : ℕ₋₂ → ℕ₋₁
1+ (-2+ n) = ℕ₋₁.-1+ n

ℕ₋₁→ℕ₋₂ : ℕ₋₁ → ℕ₋₂
ℕ₋₁→ℕ₋₂ (ℕ₋₁.-1+ n) = ℕ₋₂.-1+ n

-- Properties

-1+Path : ℕ₋₁ ≡ ℕ₋₂
-1+Path = isoToPath (iso -1+_ 1+_ (λ _ → refl) (λ _ → refl))

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:
-- Andreas, 2016-06-26, issue #2059 reported by IanOrton

-- An irrelevant parameter in a rewrite rule should still
-- be bound by the lhs.

{-# OPTIONS --rewriting #-}

-- {-# OPTIONS -v tc.pos:10 #-}
-- {-# OPTIONS -v tc.polarity:10 #-}

open import Common.Equality
open import Common.Bool

data ⊥ : Set where

⊥-elim : ∀{a}{A : Set a} → .⊥ → A
⊥-elim ()

_∧_ : (a b : Bool) → Bool
true  ∧ b = b
false ∧ _ = false

obvious : (b b' : Bool) .(p : b ≡ b' → ⊥) → (b ∧ b') ≡ false
obvious false b'    notEq = refl
obvious true  false notEq = refl
obvious true  true  notEq = ⊥-elim (notEq refl)

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE obvious   #-}

-- Should give error:

-- obvious  is not a legal rewrite rule,
-- since the following variables are not bound by the left hand side:  p
-- when checking the pragma REWRITE obvious

oops : (b : Bool) → b ∧ b ≡ false
oops b = refl

true≢false : true ≡ false → ⊥
true≢false ()

bot : ⊥
bot = true≢false (oops true)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda