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

module A where

open import Data.Nat
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product

infix  4  _≡_   -- propositional equality
infixr 10 _◎_
infixr 30 _⟷_

------------------------------------------------------------------------------
-- Our own version of refl that makes 'a' explicit

data _≡_ {ℓ} {A : Set ℓ} : (a b : A) → Set ℓ where
  refl : (a : A) → (a ≡ a)

sym : ∀ {ℓ} {A : Set ℓ} {a b : A} → (a ≡ b) → (b ≡ a)
sym {a = a} {b = .a} (refl .a) = refl a

{--

Just confirming that the following does not typecheck!

proof-irrelevance : {A : Set} {x y : A} (p q : x ≡ y) →  p ≡ q
proof-irrelevance (refl x) (refl .x) = refl (refl x)

--}

------------------------------------------------------------------------------
{--
Types are higher groupoids:
- 0 is empty
- 1 has one element and one path refl
- sum type is disjoint union; paths are component wise
- product type is cartesian product; paths are pairs of paths
--}

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

-- Points

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

BOOL : U
BOOL = PLUS ONE ONE

BOOL² : U
BOOL² = TIMES BOOL BOOL

TRUE : ⟦ BOOL ⟧
TRUE = inj₁ tt

FALSE : ⟦ BOOL ⟧
FALSE = inj₂ tt

NOT : ⟦ BOOL ⟧ → ⟦ BOOL ⟧
NOT (inj₁ tt) = FALSE
NOT (inj₂ tt) = TRUE

CNOT : ⟦ BOOL ⟧ → ⟦ BOOL ⟧ → ⟦ BOOL ⟧ × ⟦ BOOL ⟧
CNOT (inj₁ tt) b = (TRUE , NOT b)
CNOT (inj₂ tt) b = (FALSE , b)

------------------------------------------------------------------------------
-- Paths connect points in t₁ and t₂ if there is an isomorphism between the
-- types t₁ and t₂. The family ⟷ plays the role of identity types in HoTT

data _⟷_ : U → U → Set where
  unite₊  : {t : U} → PLUS ZERO t ⟷ t
  uniti₊  : {t : U} → t ⟷ PLUS ZERO t
  swap₊   : {t₁ t₂ : U} → PLUS t₁ t₂ ⟷ PLUS t₂ t₁
  assocl₊ : {t₁ t₂ t₃ : U} → PLUS t₁ (PLUS t₂ t₃) ⟷ PLUS (PLUS t₁ t₂) t₃
  assocr₊ : {t₁ t₂ t₃ : U} → PLUS (PLUS t₁ t₂) t₃ ⟷ PLUS t₁ (PLUS t₂ t₃)
  unite⋆  : {t : U} → TIMES ONE t ⟷ t
  uniti⋆  : {t : U} → t ⟷ TIMES ONE t
  swap⋆   : {t₁ t₂ : U} → TIMES t₁ t₂ ⟷ TIMES t₂ t₁
  assocl⋆ : {t₁ t₂ t₃ : U} → TIMES t₁ (TIMES t₂ t₃) ⟷ TIMES (TIMES t₁ t₂) t₃
  assocr⋆ : {t₁ t₂ t₃ : U} → TIMES (TIMES t₁ t₂) t₃ ⟷ TIMES t₁ (TIMES t₂ t₃)
  distz   : {t : U} → TIMES ZERO t ⟷ ZERO
  factorz : {t : U} → ZERO ⟷ TIMES ZERO t
  dist    : {t₁ t₂ t₃ : U} →
            TIMES (PLUS t₁ t₂) t₃ ⟷ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)
  factor  : {t₁ t₂ t₃ : U} →
            PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) ⟷ TIMES (PLUS t₁ t₂) t₃
  id⟷    : {t : U} → t ⟷ t
  sym⟷   : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
  _◎_     : {t₁ t₂ t₃ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  _⊕_     : {t₁ t₂ t₃ t₄ : U} →
            (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (PLUS t₁ t₂ ⟷ PLUS t₃ t₄)
  _⊗_     : {t₁ t₂ t₃ t₄ : U} →
            (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (TIMES t₁ t₂ ⟷ TIMES t₃ t₄)

cond : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₁ ⟷ t₂) →
       ((TIMES BOOL t₁) ⟷ (TIMES BOOL t₂))
cond f g = dist ◎ ((id⟷ ⊗ f) ⊕ (id⟷ ⊗ g)) ◎ factor

controlled : {t : U} → (t ⟷ t) → ((TIMES BOOL t) ⟷ (TIMES BOOL t))
controlled f = cond f id⟷

cnot : BOOL² ⟷ BOOL²
cnot = controlled swap₊

-- Paths: each combinator defines a space of paths between its end points

mutual

  Paths : {t₁ t₂ : U} → (t₁ ⟷ t₂) → ⟦ t₁ ⟧ → ⟦ t₂ ⟧ → Set
  Paths unite₊ (inj₁ ())
  Paths unite₊ (inj₂ v) v' = (v ≡ v')
  Paths uniti₊ v (inj₁ ())
  Paths uniti₊ v (inj₂ v') = (v ≡ v')
  Paths swap₊ (inj₁ v) (inj₁ v') = ⊥
  Paths swap₊ (inj₁ v) (inj₂ v') = (v ≡ v')
  Paths swap₊ (inj₂ v) (inj₁ v') = (v ≡ v')
  Paths swap₊ (inj₂ v) (inj₂ v') = ⊥
  Paths assocl₊ (inj₁ v) (inj₁ (inj₁ v')) = (v ≡ v')
  Paths assocl₊ (inj₁ v) (inj₁ (inj₂ v')) = ⊥
  Paths assocl₊ (inj₁ v) (inj₂ v') = ⊥
  Paths assocl₊ (inj₂ (inj₁ v)) (inj₁ (inj₁ v')) = ⊥
  Paths assocl₊ (inj₂ (inj₁ v)) (inj₁ (inj₂ v')) = (v ≡ v')
  Paths assocl₊ (inj₂ (inj₁ v)) (inj₂ v') = ⊥
  Paths assocl₊ (inj₂ (inj₂ v)) (inj₁ v') = ⊥
  Paths assocl₊ (inj₂ (inj₂ v)) (inj₂ v') = (v ≡ v')
  Paths assocr₊ (inj₁ (inj₁ v)) (inj₁ v') = (v ≡ v')
  Paths assocr₊ (inj₁ (inj₁ v)) (inj₂ v') = ⊥
  Paths assocr₊ (inj₁ (inj₂ v)) (inj₁ v') = ⊥
  Paths assocr₊ (inj₁ (inj₂ v)) (inj₂ (inj₁ v')) = (v ≡ v')
  Paths assocr₊ (inj₁ (inj₂ v)) (inj₂ (inj₂ v')) = ⊥
  Paths assocr₊ (inj₂ v) (inj₁ v') = ⊥
  Paths assocr₊ (inj₂ v) (inj₂ (inj₁ v')) = ⊥
  Paths assocr₊ (inj₂ v) (inj₂ (inj₂ v')) = (v ≡ v')
  Paths unite⋆ (tt , v) v' = (v ≡ v')
  Paths uniti⋆ v (tt , v') = (v ≡ v')
  Paths swap⋆ (v₁ , v₂) (v₂' , v₁') = (v₁ ≡ v₁') × (v₂ ≡ v₂')
  Paths assocl⋆ (v₁ , (v₂ , v₃)) ((v₁' , v₂') , v₃') =
    (v₁ ≡ v₁') × (v₂ ≡ v₂') × (v₃ ≡ v₃')
  Paths assocr⋆ ((v₁ , v₂) , v₃) (v₁' , (v₂' , v₃')) =
    (v₁ ≡ v₁') × (v₂ ≡ v₂') × (v₃ ≡ v₃')
  Paths distz (() , v)
  Paths factorz ()
  Paths dist (inj₁ v₁ , v₃) (inj₁ (v₁' , v₃')) = (v₁ ≡ v₁') × (v₃ ≡ v₃')
  Paths dist (inj₁ v₁ , v₃) (inj₂ (v₂' , v₃')) = ⊥
  Paths dist (inj₂ v₂ , v₃) (inj₁ (v₁' , v₃')) = ⊥
  Paths dist (inj₂ v₂ , v₃) (inj₂ (v₂' , v₃')) = (v₂ ≡ v₂') × (v₃ ≡ v₃')
  Paths factor (inj₁ (v₁ , v₃)) (inj₁ v₁' , v₃') =
    (v₁ ≡ v₁') × (v₃ ≡ v₃')
  Paths factor (inj₁ (v₁ , v₃)) (inj₂ v₂' , v₃') = ⊥
  Paths factor (inj₂ (v₂ , v₃)) (inj₁ v₁' , v₃') = ⊥
  Paths factor (inj₂ (v₂ , v₃)) (inj₂ v₂' , v₃') =
    (v₂ ≡ v₂') × (v₃ ≡ v₃')
  Paths {t} id⟷ v v' = (v ≡ v')
  Paths (sym⟷ c) v v' = PathsB c v v'
  Paths (_◎_ {t₁} {t₂} {t₃} c₁ c₂) v v' =
    Σ[ u ∈ ⟦ t₂ ⟧ ] (Paths c₁ v u × Paths c₂ u v')
  Paths (c₁ ⊕ c₂) (inj₁ v) (inj₁ v') = Paths c₁ v v'
  Paths (c₁ ⊕ c₂) (inj₁ v) (inj₂ v') = ⊥
  Paths (c₁ ⊕ c₂) (inj₂ v) (inj₁ v') = ⊥
  Paths (c₁ ⊕ c₂) (inj₂ v) (inj₂ v') = Paths c₂ v v'
  Paths (c₁ ⊗ c₂) (v₁ , v₂) (v₁' , v₂') =
    Paths c₁ v₁ v₁' × Paths c₂ v₂ v₂'

  PathsB : {t₁ t₂ : U} → (t₁ ⟷ t₂) → ⟦ t₂ ⟧ → ⟦ t₁ ⟧ → Set
  PathsB unite₊ v (inj₁ ())
  PathsB unite₊ v (inj₂ v') = (v ≡ v')
  PathsB uniti₊ (inj₁ ())
  PathsB uniti₊ (inj₂ v) v' = (v ≡ v')
  PathsB swap₊ (inj₁ v) (inj₁ v') = ⊥
  PathsB swap₊ (inj₁ v) (inj₂ v') = (v ≡ v')
  PathsB swap₊ (inj₂ v) (inj₁ v') = (v ≡ v')
  PathsB swap₊ (inj₂ v) (inj₂ v') = ⊥
  PathsB assocl₊ (inj₁ (inj₁ v)) (inj₁ v') = (v ≡ v')
  PathsB assocl₊ (inj₁ (inj₁ v)) (inj₂ v') = ⊥
  PathsB assocl₊ (inj₁ (inj₂ v)) (inj₁ v') = ⊥
  PathsB assocl₊ (inj₁ (inj₂ v)) (inj₂ (inj₁ v')) = (v ≡ v')
  PathsB assocl₊ (inj₁ (inj₂ v)) (inj₂ (inj₂ v')) = ⊥
  PathsB assocl₊ (inj₂ v) (inj₁ v') = ⊥
  PathsB assocl₊ (inj₂ v) (inj₂ (inj₁ v')) = ⊥
  PathsB assocl₊ (inj₂ v) (inj₂ (inj₂ v')) = (v ≡ v')
  PathsB assocr₊ (inj₁ v) (inj₁ (inj₁ v')) = (v ≡ v')
  PathsB assocr₊ (inj₁ v) (inj₁ (inj₂ v')) = ⊥
  PathsB assocr₊ (inj₁ v) (inj₂ v') = ⊥
  PathsB assocr₊ (inj₂ (inj₁ v)) (inj₁ (inj₁ v')) = ⊥
  PathsB assocr₊ (inj₂ (inj₁ v)) (inj₁ (inj₂ v')) = (v ≡ v')
  PathsB assocr₊ (inj₂ (inj₁ v)) (inj₂ v') = ⊥
  PathsB assocr₊ (inj₂ (inj₂ v)) (inj₁ v') = ⊥
  PathsB assocr₊ (inj₂ (inj₂ v)) (inj₂ v') = (v ≡ v')
  PathsB unite⋆ v (tt , v') = (v ≡ v')
  PathsB uniti⋆ (tt , v) v' = (v ≡ v')
  PathsB swap⋆ (v₁ , v₂) (v₂' , v₁') = (v₁ ≡ v₁') × (v₂ ≡ v₂')
  PathsB assocl⋆ ((v₁ , v₂) , v₃) (v₁' , (v₂' , v₃')) =
    (v₁ ≡ v₁') × (v₂ ≡ v₂') × (v₃ ≡ v₃')
  PathsB assocr⋆ (v₁ , (v₂ , v₃)) ((v₁' , v₂') , v₃') =
    (v₁ ≡ v₁') × (v₂ ≡ v₂') × (v₃ ≡ v₃')
  PathsB distz ()
  PathsB factorz (() , v)
  PathsB dist (inj₁ (v₁ , v₃)) (inj₁ v₁' , v₃') =
    (v₁ ≡ v₁') × (v₃ ≡ v₃')
  PathsB dist (inj₁ (v₁ , v₃)) (inj₂ v₂' , v₃') = ⊥
  PathsB dist (inj₂ (v₂ , v₃)) (inj₁ v₁' , v₃') = ⊥
  PathsB dist (inj₂ (v₂ , v₃)) (inj₂ v₂' , v₃') =
    (v₂ ≡ v₂') × (v₃ ≡ v₃')
  PathsB factor (inj₁ v₁ , v₃) (inj₁ (v₁' , v₃')) =
    (v₁ ≡ v₁') × (v₃ ≡ v₃')
  PathsB factor (inj₁ v₁ , v₃) (inj₂ (v₂' , v₃')) = ⊥
  PathsB factor (inj₂ v₂ , v₃) (inj₁ (v₁' , v₃')) = ⊥
  PathsB factor (inj₂ v₂ , v₃) (inj₂ (v₂' , v₃')) =
    (v₂ ≡ v₂') × (v₃ ≡ v₃')
  PathsB {t} id⟷ v v' = (v ≡ v')
  PathsB (sym⟷ c) v v' = Paths c v v'
  PathsB (_◎_ {t₁} {t₂} {t₃} c₁ c₂) v v' =
    Σ[ u ∈ ⟦ t₂ ⟧ ] (PathsB c₂ v u × PathsB c₁ u v')
  PathsB (c₁ ⊕ c₂) (inj₁ v) (inj₁ v') = PathsB c₁ v v'
  PathsB (c₁ ⊕ c₂) (inj₁ v) (inj₂ v') = ⊥
  PathsB (c₁ ⊕ c₂) (inj₂ v) (inj₁ v') = ⊥
  PathsB (c₁ ⊕ c₂) (inj₂ v) (inj₂ v') = PathsB c₂ v v'
  PathsB (c₁ ⊗ c₂) (v₁ , v₂) (v₁' , v₂') =
    PathsB c₁ v₁ v₁' × PathsB c₂ v₂ v₂'

-- Given a combinator c : t₁ ⟷ t₂ and values v₁ : ⟦ t₁ ⟧ and v₂ : ⟦ t₂ ⟧,
-- Paths c v₁ v₂ gives us the space of paths that could connect v₁ and v₂
-- Examples:

pathIdtt : Paths id⟷ tt tt
pathIdtt = refl tt

-- four different ways of relating F to F:

pathIdFF : Paths id⟷ FALSE FALSE
pathIdFF = refl FALSE

pathIdIdFF : Paths (id⟷ ◎ id⟷) FALSE FALSE
pathIdIdFF = (FALSE , refl FALSE , refl FALSE)

pathNotNotFF : Paths (swap₊ ◎ swap₊) FALSE FALSE
pathNotNotFF = TRUE , refl tt , refl tt

pathPlusFF : Paths (id⟷ ⊕ id⟷) FALSE FALSE
pathPlusFF = refl tt

-- are there 2-paths between the above 3 paths???

-- space of paths is empty; cannot produce any path; can
-- use pattern matching to confirm that the space is empty
pathIdFT : Paths id⟷ FALSE TRUE → ⊤
pathIdFT ()

-- three different ways of relating (F,F) to (F,F)

pathIdFFFF : Paths id⟷ (FALSE , FALSE) (FALSE , FALSE)
pathIdFFFF = refl (FALSE , FALSE)

pathTimesFFFF : Paths (id⟷ ⊗ id⟷) (FALSE , FALSE) (FALSE , FALSE)
pathTimesFFFF = (refl FALSE , refl FALSE)

pathTimesPlusFFFF : Paths
                      ((id⟷ ⊕ id⟷) ⊗ (id⟷ ⊕ id⟷))
                      (FALSE , FALSE) (FALSE , FALSE)
pathTimesPlusFFFF = (refl tt , refl tt)

pathSwap₊FT : Paths swap₊ FALSE TRUE
pathSwap₊FT = refl tt

pathSwap₊TF : Paths swap₊ TRUE FALSE
pathSwap₊TF = refl tt

-- no path
pathSwap₊FF : Paths swap₊ FALSE FALSE → ⊤
pathSwap₊FF ()

-- intuitively the two paths below should not be related by a 2-path because
-- pathCnotTF is "essentially" cnot which would map (F,F) to (F,F) but
-- pathIdNotTF would map (F,F) to (F,T).

pathIdNotFF : Paths (id⟷ ⊗ swap₊) (FALSE , FALSE) (FALSE , TRUE)
pathIdNotFF = refl FALSE , refl tt

pathIdNotFT : Paths (id⟷ ⊗ swap₊) (FALSE , TRUE) (FALSE , FALSE)
pathIdNotFT = refl FALSE , refl tt

pathIdNotTF : Paths (id⟷ ⊗ swap₊) (TRUE , FALSE) (TRUE , TRUE)
pathIdNotTF = refl TRUE , refl tt

pathIdNotTT : Paths (id⟷ ⊗ swap₊) (TRUE , TRUE) (TRUE , FALSE)
pathIdNotTT = refl TRUE , refl tt

pathIdNotb : {b₁ b₂ : ⟦ BOOL ⟧} → Paths (id⟷ ⊗ swap₊) (b₁ , b₂) (b₁ , NOT b₂)
pathIdNotb {b₁} {inj₁ tt} = refl b₁ , refl tt
pathIdNotb {b₁} {inj₂ tt} = refl b₁ , refl tt

pathCnotbb : {b₁ b₂ : ⟦ BOOL ⟧} → Paths cnot (b₁ , b₂) (CNOT b₁ b₂)
pathCnotbb {inj₁ tt} {inj₁ tt} = inj₁ (tt , TRUE) ,
                                 (refl tt , refl TRUE) ,
                                 (inj₁ (tt , FALSE) ,
                                 (refl tt , refl tt) ,
                                 (refl tt , refl FALSE))
pathCnotbb {inj₁ tt} {inj₂ tt} = inj₁ (tt , FALSE) ,
                                 (refl tt , refl FALSE) ,
                                 (inj₁ (tt , TRUE) ,
                                 (refl tt , refl tt) ,
                                 (refl tt , refl TRUE))
pathCnotbb {inj₂ tt} {b₂} = inj₂ (tt , b₂) ,
                            (refl tt , refl b₂) ,
                            (inj₂ (tt , b₂) ,
                            (refl tt , refl b₂) ,
                            (refl tt , refl b₂))

pathCnotFF : Paths cnot (FALSE , FALSE) (FALSE , FALSE)
pathCnotFF = inj₂ (tt , FALSE) ,
             (refl tt , refl FALSE) ,
             (inj₂ (tt , FALSE) ,
             (refl tt , refl FALSE) ,
             (refl tt , refl FALSE))

pathCnotFT : Paths cnot (FALSE , TRUE) (FALSE , TRUE)
pathCnotFT = inj₂ (tt , TRUE) ,
             (refl tt , refl TRUE) ,
             (inj₂ (tt , TRUE) ,
             (refl tt , refl TRUE) ,
             (refl tt , refl TRUE))

pathCnotTF : Paths cnot (TRUE , FALSE) (TRUE , TRUE)
pathCnotTF = inj₁ (tt , FALSE) , -- first intermediate value
             -- path using dist from (T,F) to (inj₁ (tt , F))
             (refl tt , refl FALSE) ,
             -- path from (inj₁ (tt , F)) to (T,T)
             (inj₁ (tt , TRUE) , -- next intermediate value
             (refl tt , refl tt) ,
             (refl tt , refl TRUE))

pathCnotTT : Paths cnot (TRUE , TRUE) (TRUE , FALSE)
pathCnotTT = inj₁ (tt , TRUE) ,
             (refl tt , refl TRUE) ,
             (inj₁ (tt , FALSE) ,
             (refl tt , refl tt) ,
             (refl tt , refl FALSE))

pathUnite₊ : {t : U} {v v' : ⟦ t ⟧} → (v ≡ v') → Paths unite₊ (inj₂ v) v'
pathUnite₊ p = p

-- Higher groupoid structure

-- For every path between v₁ and v₂ there is a path between v₂ and v₁

mutual

  pathInv : {t₁ t₂ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} {c : t₁ ⟷ t₂} →
            Paths c v₁ v₂ → Paths (sym⟷ c) v₂ v₁
  pathInv {v₁ = inj₁ ()} {v₂ = v} {unite₊}
  pathInv {v₁ = inj₂ v} {v₂ = v'} {unite₊} p = sym p
  pathInv {v₁ = v} {v₂ = inj₁ ()} {uniti₊}
  pathInv {v₁ = v} {v₂ = inj₂ v'} {uniti₊} p = sym p
  pathInv {v₁ = inj₁ v} {v₂ = inj₁ v'} {swap₊} ()
  pathInv {v₁ = inj₁ v} {v₂ = inj₂ v'} {swap₊} p = sym p
  pathInv {v₁ = inj₂ v} {v₂ = inj₁ v'} {swap₊} p = sym p
  pathInv {v₁ = inj₂ v} {v₂ = inj₂ v'} {swap₊} ()
  pathInv {v₁ = inj₁ v} {v₂ = inj₁ (inj₁ v')} {assocl₊} p = sym p
  pathInv {v₁ = inj₁ v} {v₂ = inj₁ (inj₂ v')} {assocl₊} ()
  pathInv {v₁ = inj₁ v} {v₂ = inj₂ v'} {assocl₊} ()
  pathInv {v₁ = inj₂ (inj₁ v)} {v₂ = inj₁ (inj₁ v')} {assocl₊} ()
  pathInv {v₁ = inj₂ (inj₁ v)} {v₂ = inj₁ (inj₂ v')} {assocl₊} p = sym p
  pathInv {v₁ = inj₂ (inj₁ v)} {v₂ = inj₂ v'} {assocl₊} ()
  pathInv {v₁ = inj₂ (inj₂ v)} {v₂ = inj₁ v'} {assocl₊} ()
  pathInv {v₁ = inj₂ (inj₂ v)} {v₂ = inj₂ v'} {assocl₊} p = sym p
  pathInv {v₁ = inj₁ (inj₁ v)} {v₂ = inj₁ v'} {assocr₊} p = sym p
  pathInv {v₁ = inj₁ (inj₁ v)} {v₂ = inj₂ v'} {assocr₊} ()
  pathInv {v₁ = inj₁ (inj₂ v)} {v₂ = inj₁ v'} {assocr₊} ()
  pathInv {v₁ = inj₁ (inj₂ v)} {v₂ = inj₂ (inj₁ v')} {assocr₊} p = sym p
  pathInv {v₁ = inj₁ (inj₂ v)} {v₂ = inj₂ (inj₂ v')} {assocr₊} ()
  pathInv {v₁ = inj₂ v} {v₂ = inj₁ v'} {assocr₊} ()
  pathInv {v₁ = inj₂ v} {v₂ = inj₂ (inj₁ v')} {assocr₊} ()
  pathInv {v₁ = inj₂ v} {v₂ = inj₂ (inj₂ v')} {assocr₊} p = sym p
  pathInv {v₁ = (tt , v)} {v₂ = v'} {unite⋆} p = sym p
  pathInv {v₁ = v} {v₂ = (tt , v')} {uniti⋆} p = sym p
  pathInv {v₁ = (u , v)} {v₂ = (v' , u')} {swap⋆} (p₁ , p₂) = (sym p₂ , sym p₁)
  pathInv {v₁ = (u , (v , w))} {v₂ = ((u' , v') , w')} {assocl⋆} (p₁ , p₂ , p₃)
    = (sym p₁ , sym p₂ , sym p₃)
  pathInv {v₁ = ((u , v) , w)} {v₂ = (u' , (v' , w'))} {assocr⋆} (p₁ , p₂ , p₃)
    = (sym p₁ , sym p₂ , sym p₃)
  pathInv {v₁ = _} {v₂ = ()} {distz}
  pathInv {v₁ = ()} {v₂ = _} {factorz}
  pathInv {v₁ = (inj₁ v₁ , v₃)} {v₂ = inj₁ (v₁' , v₃')} {dist} (p₁ , p₂) =
    (sym p₁ , sym p₂)
  pathInv {v₁ = (inj₁ v₁ , v₃)} {v₂ = inj₂ (v₂' , v₃')} {dist} ()
  pathInv {v₁ = (inj₂ v₂ , v₃)} {v₂ = inj₁ (v₁' , v₃')} {dist} ()
  pathInv {v₁ = (inj₂ v₂ , v₃)} {v₂ = inj₂ (v₂' , v₃')} {dist} (p₁ , p₂) =
    (sym p₁ , sym p₂)
  pathInv {v₁ = inj₁ (v₁ , v₃)} {v₂ = (inj₁ v₁' , v₃')} {factor} (p₁ , p₂) =
    (sym p₁ , sym p₂)
  pathInv {v₁ = inj₁ (v₁ , v₃)} {v₂ = (inj₂ v₂' , v₃')} {factor} ()
  pathInv {v₁ = inj₂ (v₂ , v₃)} {v₂ = (inj₁ v₁' , v₃')} {factor} ()
  pathInv {v₁ = inj₂ (v₂ , v₃)} {v₂ = (inj₂ v₂' , v₃')} {factor} (p₁ , p₂) =
    (sym p₁ , sym p₂)
  pathInv {v₁ = v} {v₂ = v'} {id⟷} p = sym p
  pathInv {v₁ = v} {v₂ = v'} {sym⟷ c} p = pathBInv {v₁ = v'} {v₂ = v} {c} p
  pathInv {v₁ = v} {v₂ = v'} {c₁ ◎ c₂} (u , (p₁ , p₂)) =
    (u , (pathInv {c = c₂} p₂  , pathInv {c = c₁} p₁))
  pathInv {v₁ = inj₁ v} {v₂ = inj₁ v'} {c₁ ⊕ c₂} p = pathInv {c = c₁} p
  pathInv {v₁ = inj₁ v} {v₂ = inj₂ v'} {c₁ ⊕ c₂} ()
  pathInv {v₁ = inj₂ v} {v₂ = inj₁ v'} {c₁ ⊕ c₂} ()
  pathInv {v₁ = inj₂ v} {v₂ = inj₂ v'} {c₁ ⊕ c₂} p = pathInv {c = c₂} p
  pathInv {v₁ = (u , v)} {v₂ = (u' , v')} {c₁ ⊗ c₂} (p₁ , p₂) =
    (pathInv {c = c₁} p₁ , pathInv {c = c₂} p₂)

  pathBInv : {t₁ t₂ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} {c : t₁ ⟷ t₂} →
             PathsB c v₂ v₁ → PathsB (sym⟷ c) v₁ v₂
  pathBInv {v₁ = inj₁ ()} {v₂ = v} {unite₊}
  pathBInv {v₁ = inj₂ v} {v₂ = v'} {unite₊} p = sym p
  pathBInv {v₁ = v} {v₂ = inj₁ ()} {uniti₊}
  pathBInv {v₁ = v} {v₂ = inj₂ v'} {uniti₊} p = sym p
  pathBInv {v₁ = inj₁ v} {v₂ = inj₁ v'} {swap₊} ()
  pathBInv {v₁ = inj₁ v} {v₂ = inj₂ v'} {swap₊} p = sym p
  pathBInv {v₁ = inj₂ v} {v₂ = inj₁ v'} {swap₊} p = sym p
  pathBInv {v₁ = inj₂ v} {v₂ = inj₂ v'} {swap₊} ()

  pathBInv {v₁ = inj₁ v} {v₂ = inj₁ (inj₁ v')} {assocl₊} p = sym p
  pathBInv {v₁ = inj₂ v} {v₂ = inj₁ (inj₁ v')} {assocl₊} ()
  pathBInv {v₁ = inj₁ v} {v₂ = inj₁ (inj₂ v')} {assocl₊} ()
  pathBInv {v₁ = inj₂ (inj₁ v)} {v₂ = inj₁ (inj₂ v')} {assocl₊} p = sym p
  pathBInv {v₁ = inj₂ (inj₂ v)} {v₂ = inj₁ (inj₂ v')} {assocl₊} ()
  pathBInv {v₁ = inj₁ v} {v₂ = inj₂ v'} {assocl₊} ()
  pathBInv {v₁ = inj₂ (inj₁ v)} {v₂ = inj₂ v'} {assocl₊} ()
  pathBInv {v₁ = inj₂ (inj₂ v)} {v₂ = inj₂ v'} {assocl₊} p = sym p
  pathBInv {v₁ = inj₁ (inj₁ v)} {v₂ = inj₁ v'} {assocr₊} p = sym p
  pathBInv {v₁ = inj₁ (inj₂ v)} {v₂ = inj₁ v'} {assocr₊} ()
  pathBInv {v₁ = inj₂ v} {v₂ = inj₁ v'} {assocr₊} ()
  pathBInv {v₁ = inj₁ (inj₁ v)} {v₂ = inj₂ (inj₁ v')} {assocr₊} ()
  pathBInv {v₁ = inj₁ (inj₂ v)} {v₂ = inj₂ (inj₁ v')} {assocr₊} p = sym p
  pathBInv {v₁ = inj₂ v} {v₂ = inj₂ (inj₁ v')} {assocr₊} ()
  pathBInv {v₁ = inj₁ v} {v₂ = inj₂ (inj₂ v')} {assocr₊} ()
  pathBInv {v₁ = inj₂ v} {v₂ = inj₂ (inj₂ v')} {assocr₊} p = sym p
  pathBInv {v₁ = (tt , v)} {v₂ = v'} {unite⋆} p = sym p
  pathBInv {v₁ = v} {v₂ = (tt , v')} {uniti⋆} p = sym p
  pathBInv {v₁ = (u , v)} {v₂ = (v' , u')} {swap⋆} (p₁ , p₂) = (sym p₂ , sym p₁)
  pathBInv {v₁ = (u , (v , w))} {v₂ = ((u' , v') , w')} {assocl⋆} (p₁ , p₂ , p₃)
    = (sym p₁ , sym p₂ , sym p₃)
  pathBInv {v₁ = ((u , v) , w)} {v₂ = (u' , (v' , w'))} {assocr⋆} (p₁ , p₂ , p₃)
    = (sym p₁ , sym p₂ , sym p₃)
  pathBInv {v₁ = _} {v₂ = ()} {distz}
  pathBInv {v₁ = ()} {v₂ = _} {factorz}
  pathBInv {v₁ = (inj₁ v₁ , v₃)} {v₂ = inj₁ (v₁' , v₃')} {dist} (p₁ , p₂) =
    (sym p₁ , sym p₂)
  pathBInv {v₁ = (inj₁ v₁ , v₃)} {v₂ = inj₂ (v₂' , v₃')} {dist} ()
  pathBInv {v₁ = (inj₂ v₂ , v₃)} {v₂ = inj₁ (v₁' , v₃')} {dist} ()
  pathBInv {v₁ = (inj₂ v₂ , v₃)} {v₂ = inj₂ (v₂' , v₃')} {dist} (p₁ , p₂) =
    (sym p₁ , sym p₂)
  pathBInv {v₁ = inj₁ (v₁ , v₃)} {v₂ = (inj₁ v₁' , v₃')} {factor} (p₁ , p₂) =
    (sym p₁ , sym p₂)
  pathBInv {v₁ = inj₁ (v₁ , v₃)} {v₂ = (inj₂ v₂' , v₃')} {factor} ()
  pathBInv {v₁ = inj₂ (v₂ , v₃)} {v₂ = (inj₁ v₁' , v₃')} {factor} ()
  pathBInv {v₁ = inj₂ (v₂ , v₃)} {v₂ = (inj₂ v₂' , v₃')} {factor} (p₁ , p₂) =
    (sym p₁ , sym p₂)
  pathBInv {v₁ = v} {v₂ = v'} {id⟷} p = sym p
  pathBInv {v₁ = v} {v₂ = v'} {sym⟷ c} p = pathInv {v₁ = v'} {v₂ = v} {c} p
  pathBInv {t₁} {t₂} {v₁} {v₂} {c₁ ◎ c₂} (u , (p₂ , p₁)) =
    (u , (pathBInv {v₁ = v₁} {v₂ = u} {c = c₁} p₁ ,
          pathBInv {v₁ = u} {v₂ = v₂} {c = c₂} p₂))
  pathBInv {v₁ = inj₁ v} {v₂ = inj₁ v'} {c₁ ⊕ c₂} p = pathBInv {c = c₁} p
  pathBInv {v₁ = inj₁ v} {v₂ = inj₂ v'} {c₁ ⊕ c₂} ()
  pathBInv {v₁ = inj₂ v} {v₂ = inj₁ v'} {c₁ ⊕ c₂} ()
  pathBInv {v₁ = inj₂ v} {v₂ = inj₂ v'} {c₁ ⊕ c₂} p = pathBInv {c = c₂} p
  pathBInv {v₁ = (u , v)} {v₂ = (u' , v')} {c₁ ⊗ c₂} (p₁ , p₂) =
    (pathBInv {c = c₁} p₁ , pathBInv {c = c₂} p₂)

-- for every paths from v1 to v2 and from v2 to v3, there is a path from v1
-- to v3 that (obviously) goes through v2

pathTrans : {t₁ t₂ t₃ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} {v₃ : ⟦ t₃ ⟧}
            {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} →
            Paths c₁ v₁ v₂ → Paths c₂ v₂ v₃ → Paths (c₁ ◎ c₂) v₁ v₃
pathTrans {v₂ = v₂} p q = (v₂ , p , q)

pathBTrans : {t₁ t₂ t₃ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} {v₃ : ⟦ t₃ ⟧}
             {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} →
             PathsB c₁ v₂ v₁ → PathsB c₂ v₃ v₂ → PathsB (c₁ ◎ c₂) v₃ v₁
pathBTrans {v₂ = v₂} p q = (v₂ , q , p)

-- we always have a canonical path from v to v
pathId : {t : U} {v : ⟦ t ⟧} → Paths id⟷ v v
pathId {v = v} = refl v

------------------------------------------------------------------------------
-- Int construction
-- this will allow us to represents paths as values and then define 2paths
-- between them

data DU : Set where
  diff : U → U → DU

pos : DU → U
pos (diff t₁ t₂) = t₁

neg : DU → U
neg (diff t₁ t₂) = t₂

zeroD : DU
zeroD = diff ZERO ZERO

oneD : DU
oneD = diff ONE ZERO

plusD : DU → DU → DU
plusD (diff t₁ t₂) (diff t₁' t₂') = diff (PLUS t₁ t₁') (PLUS t₂ t₂')

timesD : DU → DU → DU
timesD (diff t₁ t₂) (diff t₁' t₂') =
  diff (PLUS (TIMES t₁ t₁') (TIMES t₂ t₂'))
       (PLUS (TIMES t₂ t₁') (TIMES t₁ t₂'))

dualD : DU → DU
dualD (diff t₁ t₂) = diff t₂ t₁

lolliD : DU → DU → DU
lolliD (diff t₁ t₂) (diff t₁' t₂') = diff (PLUS t₂ t₁') (PLUS t₁ t₂')

_≤=>_ : DU → DU → Set
d₁ ≤=> d₂ = PLUS (pos d₁) (neg d₂) ⟷ PLUS (neg d₁) (pos d₂)

idD : {d : DU} → d ≤=> d
idD = swap₊

--curryD : {d₁ d₂ d₃ : DU} → (plusD d₁ d₂ ≤=> d₃) → (d₁ ≤=> lolliD d₂ d₃)
--curryD f = assocl₊ ◎ f ◎ assocr₊
-- take a path and represent it as a value of type lolli and then use
-- ≤=> between these values as the definition of 2paths???

------------------------------------------------------------------------------
-- Can we show:
-- p : Paths c v₁ v₂ == pathTrans p (refl v₂)

-- Groupoid structure (i.e. laws), for 2Paths.  Some of the rest of
-- the structure is given above already
-- If the following is right, we can come up with syntax (like _[_]⟺[_]_ ) for  p₁ [c₁]⟺[c₂] p₂ .  We really do
-- need to index the ⟺ by the combinators 'explicitly' as Agda can never infer them.
data 2P {t₁ t₂ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧ } : {c₁ c₂ : t₁ ⟷ t₂} → Paths c₁ v₁ v₂ → Paths c₂ v₁ v₂ → Set where
  id2 : {c : t₁ ⟷ t₂} {p : Paths c v₁ v₂} → 2P {c₁ = c} {c} p p
  inv2  : {c₁ c₂ : t₁ ⟷ t₂} {p₁ : Paths c₁ v₁ v₂} {p₂ : Paths c₂ v₁ v₂} → 2P {c₁ = c₁} {c₂} p₁ p₂ → 2P {c₁ = c₂} {c₁} p₂ p₁
  comp2 : {c₁ c₂ c₃ : t₁ ⟷ t₂} {p₁ : Paths c₁ v₁ v₂} {p₂ : Paths c₂ v₁ v₂} {p₃ : Paths c₃ v₁ v₂} →
    2P {c₁ = c₁} {c₂} p₁ p₂ → 2P {c₁ = c₂} {c₃} p₂ p₃ → 2P {c₁ = c₁} {c₃} p₁ p₃
  -- should define composition which effectively does as below??
  lid : {c : t₁ ⟷ t₂} {p : Paths c v₁ v₂} → 2P {c₁ = id⟷ ◎ c} {c} (pathTrans {c₁ = id⟷} {c} pathId p) p
  rid : {c : t₁ ⟷ t₂} {p : Paths c v₁ v₂} → 2P {c₁ = c ◎ id⟷} {c} (pathTrans {c₁ = c} {id⟷} p pathId) p
-- also need:
-- assoc
--  linv : {c : t₁ ⟷ t₂} {p : Paths c v₁ v₂} → 2P {c₁ = c}
-- linv
-- rinv
-- and perhaps cong, i.e. ◎-resp-2P

mutual
  2Paths :  {t₁ t₂ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧ } {c₁ c₂ : t₁ ⟷ t₂} {p₁ : Paths c₁ v₁ v₂} {p₂ : Paths c₂ v₁ v₂} → 2P {c₁ = c₁} {c₂} p₁ p₂ → Paths c₁ v₁ v₂ → Paths c₂ v₁ v₂ → Set
  2Paths id2 p₁ p₂ = p₁ ≡ p₂
  2Paths (inv2 p) p₁ p₂ = 2PathsB p p₁ p₂
  2Paths {t₁} {t₂} {v₁} {v₂} (comp2 {c₁ = c₁} {c₂} {c₃} {p₁} {p₂} {p₃} p q) α₁ α₂ =
      Σ[ r ∈ Paths c₂ v₁ v₂ ] (2P {c₁ = c₁} {c₂} α₁ r × 2P {c₁ = c₂} {c₃} r α₂)
  2Paths lid (a , refl .a , p₂) p₃ = p₂ ≡ p₃
  2Paths rid (a , p₂ , refl .a) p₃ = p₂ ≡ p₃

  2PathsB : {t₁ t₂ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧ } {c₁ c₂ : t₁ ⟷ t₂} {p₁ : Paths c₁ v₁ v₂} {p₂ : Paths c₂ v₁ v₂} → 2P {c₁ = c₁} {c₂} p₁ p₂ → Paths c₂ v₁ v₂ → Paths c₁ v₁ v₂ → Set
  2PathsB id2 p q = q ≡ p
  2PathsB (inv2 p) p₁ p₂ = 2PathsB p p₂ p₁
  2PathsB (comp2 p q) p₁ p₂ = {!!}
  2PathsB lid p (a , refl .a , p₃) = p ≡ p₃
  2PathsB rid p (a , p₂ , refl .a) = p ≡ p₂

example : 2Paths {t₁ = BOOL} {t₂ = BOOL} {v₁ = FALSE} {v₂ = FALSE}
          {c₁ = id⟷ ◎ id⟷} {c₂ = id⟷} {p₁ = pathIdIdFF}
          lid pathIdIdFF pathIdFF
example = refl (refl FALSE)

{--
2Paths : {t₁ t₂ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} {c₁ c₂ : t₁ ⟷ t₂} →
         Paths c₁ v₁ v₂ → Paths c₂ v₁ v₂ → Set
2Paths p q = {!!}

reflR : {t₁ t₂ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} {c : t₁ ⟷ t₂}
        {p : Paths c v₁ v₂} → {q : Paths (c ◎ id⟷) v₁ v₂} →
        2Paths {t₁} {t₂} {v₁} {v₂} {c} {c ◎ id⟷} p q
reflR {c = unite₊} = {!!}
-- p : Paths unite₊ .v₁ .v₂
-- q : Paths (unite₊ ◎ id⟷) .v₁ .v₂
-- 2Paths p q
reflR {c = uniti₊} = {!!}
reflR {c = swap₊} = {!!}
reflR {c = assocl₊} = {!!}
reflR {c = assocr₊} = {!!}
reflR {c = unite⋆} = {!!}
reflR {c = uniti⋆} = {!!}
reflR {c = swap⋆} = {!!}
reflR {c = assocl⋆} = {!!}
reflR {c = assocr⋆} = {!!}
reflR {c = distz} = {!!}
reflR {c = factorz} = {!!}
reflR {c = dist} = {!!}
reflR {c = factor} = {!!}
reflR {c = id⟷} = {!!}
reflR {c = sym⟷ c} = {!!}
reflR {c = c₁ ◎ c₂} = {!!}
reflR {c = c₁ ⊕ c₂} = {!!}
reflR {c = c₁ ⊗ c₂} = {!!}
--}

{--
-- If we have a path between v₁ and v₁' and a combinator that connects v₁ to
-- v₂, then the combinator also connects v₁' to some v₂' such that there is
-- path between v₂ and v₂'

pathFunctor : {t₁ t₂ : U} {v₁ v₁' : ⟦ t₁ ⟧} {v₂ v₂' : ⟦ t₂ ⟧} {c : t₁ ⟷ t₂} →
  (v₁ ≡ v₁') → Paths c v₁ v₂ → (v₂ ≡ v₂') → Paths c v₁' v₂'
pathFunctor = {!!}

All kind of structure to investigate in the HoTT book. Let's push forward
with cubical types though...
--}

------------------------------------------------------------------------------
-- N dimensional version

{-
data C : ℕ → Set where
  ZD   : U → C 0
  Node : {n : ℕ} → C n → C n → C (suc n)

⟦_⟧N : {n : ℕ} → C n → Set
⟦ ZD t ⟧N = ⟦ t ⟧
⟦ Node c₁ c₂ ⟧N = ⟦ c₁ ⟧N ⊎ ⟦ c₂ ⟧N

liftN : (n : ℕ) → (t : U) → C n
liftN 0 t = ZD t
liftN (suc n) t = Node (liftN n t) (liftN n ZERO)

zeroN : (n : ℕ) → C n
zeroN n = liftN n ZERO

oneN : (n : ℕ) → C n
oneN n = liftN n ONE

plus : {n : ℕ} → C n → C n → C n
plus (ZD t₁) (ZD t₂) = ZD (PLUS t₁ t₂)
plus (Node c₁ c₂) (Node c₁' c₂') = Node (plus c₁ c₁') (plus c₂ c₂')

times : {m n : ℕ} → C m → C n → C (m + n)
times (ZD t₁) (ZD t₂) = ZD (TIMES t₁ t₂)
times (ZD t) (Node c₁ c₂) = Node (times (ZD t) c₁) (times (ZD t) c₂)
times (Node c₁ c₂) c = Node (times c₁ c) (times c₂ c)

-- N-dimensional paths connect points in c₁ and c₂ if there is an isomorphism
-- between the types c₁ and c₂.

data _⟺_ : {n : ℕ} → C n → C n → Set where
  baseC : {t₁ t₂ : U} → (t₁ ⟷ t₂) → ((ZD t₁) ⟺ (ZD t₂))
  nodeC : {n : ℕ} {c₁ : C n} {c₂ : C n} {c₃ : C n} {c₄ : C n} →
          (c₁ ⟺ c₂) → (c₃ ⟺ c₄) → ((Node c₁ c₃) ⟺ (Node c₂ c₄))
--  zerolC : {n : ℕ} {c : C n} → ((Node c c) ⟺ (zeroN (suc n)))
--  zerorC : {n : ℕ} {c : C n} → ((zeroN (suc n)) ⟺ (Node c c))

NPaths : {n : ℕ} {c₁ c₂ : C n} → (c₁ ⟺ c₂) → ⟦ c₁ ⟧N → ⟦ c₂ ⟧N → Set
NPaths (baseC c) v₁ v₂ = Paths c v₁ v₂
NPaths (nodeC α₁ α₂) (inj₁ v₁) (inj₁ v₂) = NPaths α₁ v₁ v₂
NPaths (nodeC α₁ α₂) (inj₁ v₁) (inj₂ v₂) = ⊥
NPaths (nodeC α₁ α₂) (inj₂ v₁) (inj₁ v₂) = ⊥
NPaths (nodeC α₁ α₂) (inj₂ v₁) (inj₂ v₂) = NPaths α₂ v₁ v₂
--NPaths zerolC v₁ v₂ = {!!}
--NPaths zerorC v₁ v₂ = {!!}

-}
------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- 2015-02-24 Andrea Vezzosi

-- Since type constructors are considered injective by the forcing analysis we are able to define the type for the "russel" paradox:

open import Common.Product

Type = Set₁

data Box : Type -> Set where

-- The following type should be rejected, as A is not forced.
data Tree' : Set -> Type where
  sup' : ∀ (A : Type) -> (A → ∃ Tree') → Tree' (Box A)

Tree = ∃ Tree'

sup : (a : Type) -> (f : a -> Tree) -> Tree
sup a f = _ , sup' a f

a : Tree -> Type
a (._ , sup' a _) = a

f : (t : Tree) -> a t -> Tree
f (._ , sup' a f) = f

-- The rest is the standard paradox

open import Common.Equality
open import Common.Prelude

normal : Tree -> Type
normal t = Σ (a t) (λ (y : a t) → (f t y ≡ sup (a t) (f t))) -> ⊥

nt : Type
nt = Σ Tree \ (t : Tree) -> normal t

p : nt -> Tree
p (x , _) = x

q : (y : nt) -> normal (p y)
q (x , y) = y

r : Tree
r = sup nt p

lemma : normal r
lemma ((y1 , y2) , z) = y2 (subst (\ y3 -> Σ _ \ (y : a y3) ->  f y3 y ≡ sup (a y3) (f y3)) (sym z) ((y1 , y2) , z))

russel : ⊥
russel = lemma ((r , lemma) , refl)

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of These
------------------------------------------------------------------------

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

module Data.These.Properties where

open import Data.These
open import Function using (_∘_)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no)

------------------------------------------------------------------------
-- Equality

module _ {a b} {A : Set a} {B : Set b} where

  this-injective : ∀ {x y : A} → this {B = B} x ≡ this y → x ≡ y
  this-injective refl = refl

  that-injective : ∀ {a b : B} → that {A = A} a ≡ that b → a ≡ b
  that-injective refl = refl

  these-injectiveˡ : ∀ {x y : A} {a b : B} → these x a ≡ these y b → x ≡ y
  these-injectiveˡ refl = refl

  these-injectiveʳ : ∀ {x y : A} {a b : B} → these x a ≡ these y b → a ≡ b
  these-injectiveʳ refl = refl

  ≡-dec : Decidable _≡_ → Decidable _≡_ → Decidable {A = These A B} _≡_
  ≡-dec dec₁ dec₂ (this x)    (this y)    with dec₁ x y
  ... | yes refl = yes refl
  ... | no  x≢y  = no (x≢y ∘ this-injective)
  ≡-dec dec₁ dec₂ (this x)    (that y)    = no λ()
  ≡-dec dec₁ dec₂ (this x)    (these y b) = no λ()
  ≡-dec dec₁ dec₂ (that x)    (this y)    = no λ()
  ≡-dec dec₁ dec₂ (that x)    (that y)    with dec₂ x y
  ... | yes refl = yes refl
  ... | no  x≢y  = no (x≢y ∘ that-injective)
  ≡-dec dec₁ dec₂ (that x)    (these y b) = no λ()
  ≡-dec dec₁ dec₂ (these x a) (this y)    = no λ()
  ≡-dec dec₁ dec₂ (these x a) (that y)    = no λ()
  ≡-dec dec₁ dec₂ (these x a) (these y b) with dec₁ x y | dec₂ a b
  ... | yes refl | yes refl = yes refl
  ... | no  x≢y  | _        = no (x≢y ∘ these-injectiveˡ)
  ... | yes _    | no  a≢b  = no (a≢b ∘ these-injectiveʳ)


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Smap
open import Oscar.Data.Fin
open import Oscar.Data.Term
open import Oscar.Data.Vec
import Oscar.Class.Surjection.⋆

module Oscar.Class.Smap.ExtensionFinExtensionTerm where

module _ {𝔭} {𝔓 : Ø 𝔭} where

  open Term 𝔓

  private

    mutual

      𝓼urjectivityExtensionFinExtensionTerm : Smap!.type (Extension Fin) (Extension Term)
      𝓼urjectivityExtensionFinExtensionTerm x (i y) = i (x y)
      𝓼urjectivityExtensionFinExtensionTerm x leaf = leaf
      𝓼urjectivityExtensionFinExtensionTerm x (l fork r) = 𝓼urjectivityExtensionFinExtensionTerm x l fork 𝓼urjectivityExtensionFinExtensionTerm x r
      𝓼urjectivityExtensionFinExtensionTerm x (function f ts) = function f $ 𝓼urjectivityExtensionFinExtensionTerms x ts

      𝓼urjectivityExtensionFinExtensionTerms : ∀ {N} → Smap!.type (Extension Fin) (Extension $ Terms N)
      𝓼urjectivityExtensionFinExtensionTerms x ∅ = ∅
      𝓼urjectivityExtensionFinExtensionTerms x (t , ts) = 𝓼urjectivityExtensionFinExtensionTerm x t , 𝓼urjectivityExtensionFinExtensionTerms x ts

  instance

    𝓢urjectivityExtensionFinExtensionTerm : Smap!.class (Extension Fin) (Extension Term)
    𝓢urjectivityExtensionFinExtensionTerm .⋆ _ _ = 𝓼urjectivityExtensionFinExtensionTerm

    𝓢urjectivityExtensionFinExtensionTerms : ∀ {N} → Smap!.class (Extension Fin) (Extension $ Terms N)
    𝓢urjectivityExtensionFinExtensionTerms .⋆ _ _ = 𝓼urjectivityExtensionFinExtensionTerms


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

open import Types
open import Paths

{- Stuff about truncation levels (aka h-levers) that do not require the notion
   of equivalence or function extensionality -}

module HLevel {i} where

-- Definition of truncation levels

is-contr : Set i → Set i
is-contr A = Σ A (λ x → ((y : A) → y ≡ x))

is-truncated : ℕ₋₂ → (Set i → Set i)
is-truncated ⟨-2⟩ A = is-contr A
is-truncated (S n) A = (x y : A) → is-truncated n (x ≡ y)

is-prop = is-truncated ⟨-1⟩
is-set  = is-truncated ⟨0⟩
is-gpd  = is-truncated ⟨1⟩

-- The original notion of h-level can be defined in the following way.
-- We won’t use this definition though.
is-hlevel : ℕ → (Set i → Set i)
is-hlevel n A = is-truncated (n -2) A where
  _-2 : ℕ → ℕ₋₂
  O -2 = ⟨-2⟩
  (S n) -2 = S (n -2)

-- The following property is equivalent to being a proposition
has-all-paths : Set i → Set i
has-all-paths A = (x y : A) → x ≡ y

-- Having decidable equality is stronger that being a set
has-dec-eq : Set i → Set i
has-dec-eq A = (x y : A) → (x ≡ y) ⊔ (x ≢ y)

abstract
  all-paths-is-prop : {A : Set i} → (has-all-paths A → is-prop A)
  all-paths-is-prop {A} c x y = (c x y , canon-path) where
    lemma : {x y : A} (p : x ≡ y) → c x y ≡ p ∘ c y y
    lemma refl = refl

    canon-path : {x y : A} (p : x ≡ y) → p ≡ c x y
    canon-path {.y} {y} refl = anti-whisker-right (c y y) (lemma (c y y))

  -- Truncation levels are cumulative
  truncated-is-truncated-S : {A : Set i} (n : ℕ₋₂)
    → (is-truncated n A → is-truncated (S n) A)
  truncated-is-truncated-S ⟨-2⟩ q =
    all-paths-is-prop (λ x y → π₂ q x ∘ ! (π₂ q y))
  truncated-is-truncated-S (S n) q =
    λ x y → truncated-is-truncated-S n (q x y)

  -- A type with a decidable equality is a set
  dec-eq-is-set : {A : Set i} → (has-dec-eq A → is-set A)
  dec-eq-is-set dec x y with dec x y
  dec-eq-is-set dec x y | inr p⊥ = λ p → abort-nondep (p⊥ p)
  dec-eq-is-set {A} dec x y | inl q = paths-A-is-prop q where

    -- The fact that equality is decidable on A gives a canonical path parallel
    -- to every path [p], depending only on the endpoints
    get-path : {u v : A} (r : u ≡ v) → u ≡ v
    get-path {u} {v} r with dec u v
    get-path r | inl q = q
    get-path r | inr r⊥ = abort-nondep (r⊥ r)

    get-path-eq : {u : A} (r : u ≡ u) → get-path r ≡ get-path refl
    get-path-eq {u} r with dec u u
    get-path-eq r | inl q = refl
    get-path-eq r | inr r⊥ = abort-nondep (r⊥ refl)

    lemma : {u v : A} (r : u ≡ v) → r ∘ get-path refl ≡ get-path r
    lemma refl = refl

    paths-A-is-prop : {u v : A} (q : u ≡ v) → is-prop (u ≡ v)
    paths-A-is-prop {u} {.u} refl =
      truncated-is-truncated-S ⟨-2⟩
        (refl , λ r → anti-whisker-right (get-path refl)
                                         (lemma r ∘ get-path-eq r))

module _ {A : Set i} where
  abstract
    contr-has-all-paths : is-contr A → has-all-paths A
    contr-has-all-paths c x y = π₂ c x ∘ ! (π₂ c y)

    prop-has-all-paths : is-prop A → has-all-paths A
    prop-has-all-paths c x y = π₁ (c x y)

    inhab-prop-is-contr : A → is-prop A → is-contr A
    inhab-prop-is-contr x₀ p = (x₀ , λ y → π₁ (p y x₀))

    contr-is-truncated : (n : ℕ₋₂) → (is-contr A → is-truncated n A)
    contr-is-truncated ⟨-2⟩ p = p
    contr-is-truncated (S n) p =
      truncated-is-truncated-S n (contr-is-truncated n p)

    prop-is-truncated-S : (n : ℕ₋₂) → (is-prop A → is-truncated (S n) A)
    prop-is-truncated-S ⟨-2⟩ p = p
    prop-is-truncated-S (S n) p =
      truncated-is-truncated-S (S n) (prop-is-truncated-S n p)

    set-is-truncated-SS : (n : ℕ₋₂) → (is-set A → is-truncated (S (S n)) A)
    set-is-truncated-SS ⟨-2⟩ p = p
    set-is-truncated-SS (S n) p = truncated-is-truncated-S (S (S n))
                                                  (set-is-truncated-SS n p)

    contr-is-prop : is-contr A → is-prop A
    contr-is-prop = contr-is-truncated ⟨-1⟩

    contr-is-set : is-contr A → is-set A
    contr-is-set = contr-is-truncated ⟨0⟩

    contr-is-gpd : is-contr A → is-gpd A
    contr-is-gpd = contr-is-truncated ⟨1⟩

    prop-is-set : is-prop A → is-set A
    prop-is-set = prop-is-truncated-S ⟨-1⟩

    prop-is-gpd : is-prop A → is-gpd A
    prop-is-gpd = prop-is-truncated-S ⟨0⟩

    set-is-gpd : is-set A → is-gpd A
    set-is-gpd = set-is-truncated-SS ⟨-1⟩

    -- If [A] is n-truncated, then so does [x ≡ y] for [x y : A]
    ≡-is-truncated : (n : ℕ₋₂) {x y : A}
      → (is-truncated n A → is-truncated n (x ≡ y))
    ≡-is-truncated ⟨-2⟩ p = (contr-has-all-paths p _ _ , unique-path) where
      unique-path : {u v : A} (q : u ≡ v)
        → q ≡ contr-has-all-paths p u v
      unique-path refl = ! (opposite-right-inverse (π₂ p _))
    ≡-is-truncated (S n) {x} {y} p = truncated-is-truncated-S n (p x y)

  -- The type of paths to a fixed point is contractible
  pathto-is-contr : (x : A) → is-contr (Σ A (λ t → t ≡ x))
  pathto-is-contr x = ((x , refl) , pathto-unique-path) where
    pathto-unique-path : {u : A} (pp : Σ A (λ t → t ≡ u)) → pp ≡ (u , refl)
    pathto-unique-path (u , refl) = refl

  -- Specilization
  module _ where
    ≡-is-set : {x y : A} → (is-set A → is-set (x ≡ y))
    ≡-is-set = ≡-is-truncated ⟨0⟩

    ≡-is-prop : {x y : A} → (is-prop A → is-prop (x ≡ y))
    ≡-is-prop = ≡-is-truncated ⟨-1⟩

abstract
  -- Unit is contractible
  -- I do not need to specify the universe level because in this file [is-contr]
  -- is not yet universe polymorphic ([i] is a global argument)
  unit-is-contr : is-contr unit
  unit-is-contr = (tt , λ y → refl)

  unit-is-truncated : (n : ℕ₋₂) → is-truncated n unit
  unit-is-truncated n = contr-is-truncated n unit-is-contr

  -- [unit-is-truncated#instance] produces unsolved metas
  unit-is-truncated-S#instance : {n : ℕ₋₂} → is-truncated (S n) unit
  unit-is-truncated-S#instance = contr-is-truncated _ unit-is-contr

  unit-is-prop : is-prop unit
  unit-is-prop = unit-is-truncated ⟨-1⟩

  unit-is-set : is-set unit
  unit-is-set = unit-is-truncated ⟨0⟩

  contr-has-section : ∀ {j} {A : Set i} {P : A → Set j}
    → (is-contr A → (x : A) → (u : P x) → Π A P)
  contr-has-section (x , p) x₀ y₀ t = transport _ (p x₀ ∘ ! (p t)) y₀

private
  bool-true≢false-type : bool {i} → Set
  bool-true≢false-type true  = ⊤
  bool-true≢false-type false = ⊥

abstract
  bool-true≢false : true {i} ≢ false
  bool-true≢false p = transport bool-true≢false-type p tt

  bool-false≢true : false {i} ≢ true
  bool-false≢true p = transport bool-true≢false-type (! p) tt

  bool-has-dec-eq : has-dec-eq bool
  bool-has-dec-eq true true = inl refl
  bool-has-dec-eq true false = inr bool-true≢false
  bool-has-dec-eq false true = inr bool-false≢true
  bool-has-dec-eq false false = inl refl

  bool-is-set : is-set bool
  bool-is-set = dec-eq-is-set bool-has-dec-eq

  ⊥-is-prop : is-prop ⊥
  ⊥-is-prop ()

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Haskell.Prim.String where

open import Agda.Builtin.Char
open import Agda.Builtin.Unit
open import Agda.Builtin.FromString
import Agda.Builtin.String as Str

open import Haskell.Prim
open import Haskell.Prim.List
open import Haskell.Prim.Foldable

--------------------------------------------------
-- String

String = List Char

instance
  iIsStringString : IsString String
  iIsStringString .IsString.Constraint _ = ⊤
  iIsStringString .fromString s = Str.primStringToList s

private
  cons : Char → List String → List String
  cons c []       = (c ∷ []) ∷ []
  cons c (s ∷ ss) = (c ∷ s) ∷ ss

lines : String → List String
lines []         = []
lines ('\n' ∷ s) = [] ∷ lines s
lines (c    ∷ s) = cons c (lines s)

private
 mutual
  space : String → List String
  space [] = []
  space (c ∷ s) = if primIsSpace c then space s else cons c (word s)

  word  : String → List String
  word []      = []
  word (c ∷ s) = if primIsSpace c then [] ∷ space s else cons c (word s)

words : String → List String
words [] = []
words s@(c ∷ s₁) = if primIsSpace c then space s₁ else word s

unlines : List String → String
unlines = concatMap (_++ "\n")

unwords : List String → String
unwords [] = ""
unwords (w ∷ []) = w
unwords (w ∷ ws) = w ++ ' ' ∷ unwords ws


text:
------------------------------------------------------------------------------
-- The McCarthy 91 function: A function with nested recursion
------------------------------------------------------------------------------

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

module FOTC.Program.McCarthy91.McCarthy91 where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.UnaryNumbers

------------------------------------------------------------------------------
-- The McCarthy 91 function.
postulate
  f₉₁    : D → D
  f₉₁-eq : ∀ n → f₉₁ n ≡ (if (gt n 100') then n ∸ 10' else f₉₁ (f₉₁ (n + 11')))
{-# ATP axiom f₉₁-eq #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Sample non-literate Agda program
-- ================================
--
-- A remark to test bulleted lists:
--
-- * This file serves as example for agda2lagda.
--
-- * The content may be non-sensical.
--
-- Indeed!

module Foo where

-- Some data type.

data D : Set where
  c : D

-- A function.
foo : D → D
foo c = c   -- basically, the identity

{- This part is commented out.
{-
bar : D → Set
bar x = D
-- -}
-- -}

-- A subheading
---------------

module Submodule where

  postulate
    zeta : D

-- That's it.
-- Bye.


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sparse polynomials in a commutative ring, encoded in Horner normal
-- form.
--
-- Horner normal form encodes a polynomial as a list of coefficients.
-- As an example take the polynomial:
--
--   3 + 2x² + 4x⁵ + 2x⁷
--
-- Then expand it out, filling in the missing coefficients:
--
--   3x⁰ + 0x¹ + 2x² + 0x³ + 0x⁴ + 4x⁵ + 0x⁶ + 2x⁷
--
-- And then encode that as a list:
--
--   [3, 0, 2, 0, 0, 4, 0, 2]
--
-- The representation we use here is optimised from the above. First,
-- we remove the zero terms, and add a "gap" index next to every
-- coefficient:
--
--   [(3,0),(2,1),(4,2),(2,1)]
--
-- Which can be thought of as a representation of the expression:
--
--   x⁰ * (3 + x * x¹ * (2 + x * x² * (4 + x * x¹ * (2 + x * 0))))
--
-- This is "sparse" Horner normal form.
--
-- The second optimisation deals with representing multiple variables
-- in a polynomial. The standard trick is to encode a polynomial in n
-- variables as a polynomial with coefficients in n-1 variables,
-- recursing until you hit 0 which is simply the type of the coefficient
-- itself.
--
-- We again encode "gaps" here, with the injection index. Since the
-- number of variables in a polynomial is contained in its type,
-- however, operations on this gap are type-relevant, so it's not
-- convenient to simply use ℕ. We use _≤′_ instead.
------------------------------------------------------------------------

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

open import Tactic.RingSolver.Core.Polynomial.Parameters

module Tactic.RingSolver.Core.Polynomial.Base
  {ℓ₁ ℓ₂} (coeffs : RawCoeff ℓ₁ ℓ₂) where

open RawCoeff coeffs

open import Data.Bool              using (Bool; true; false; T)
open import Data.Empty             using (⊥)
open import Data.Fin.Base as Fin        using (Fin; zero; suc)
open import Data.List.Kleene
open import Data.Nat.Base as ℕ          using (ℕ; suc; zero; _≤′_; compare; ≤′-refl; ≤′-step; _<′_)
open import Data.Nat.Properties    using (z≤′n; ≤′-trans)
open import Data.Nat.Induction
open import Data.Product           using (_×_; _,_; map₁; curry; uncurry)
open import Data.Unit              using (⊤; tt)
open import Function.Base
open import Relation.Nullary       using (¬_; Dec; yes; no)

open import Algebra.Operations.Ring rawRing

------------------------------------------------------------------------
-- Injection indices.
------------------------------------------------------------------------

-- First, we define comparisons on _≤′_.
-- The following is analagous to Ordering and compare from
-- Data.Nat.Base.
data InjectionOrdering {n : ℕ} : ∀ {i j} (i≤n : i ≤′ n) (j≤n : j ≤′ n) → Set
                      where
  inj-lt : ∀ {i j-1} (i≤j-1 : i ≤′ j-1) (j≤n : suc j-1 ≤′ n) →
           InjectionOrdering (≤′-step i≤j-1 ⟨ ≤′-trans ⟩ j≤n) j≤n

  inj-gt : ∀ {i-1 j} (i≤n : suc i-1 ≤′ n) (j≤i-1 : j ≤′ i-1) →
           InjectionOrdering i≤n (≤′-step j≤i-1 ⟨ ≤′-trans ⟩ i≤n)

  inj-eq : ∀ {i} (i≤n : i ≤′ n) →
           InjectionOrdering i≤n i≤n

inj-compare : ∀ {i j n} (x : i ≤′ n) (y : j ≤′ n) → InjectionOrdering x y
inj-compare ≤′-refl     ≤′-refl     = inj-eq ≤′-refl
inj-compare ≤′-refl     (≤′-step y) = inj-gt ≤′-refl y
inj-compare (≤′-step x) ≤′-refl     = inj-lt x ≤′-refl
inj-compare (≤′-step x) (≤′-step y) = case inj-compare x y of
    λ { (inj-lt i≤j-1 y) → inj-lt i≤j-1 (≤′-step y)
      ; (inj-gt x j≤i-1) → inj-gt (≤′-step x) j≤i-1
      ; (inj-eq x)       → inj-eq (≤′-step x)
      }

-- The "space" above a Fin n is the number of unique "Fin n"s greater
-- than or equal to it.
space : ∀ {n} → Fin n → ℕ
space f = suc (go f)
  where
  go : ∀ {n} → Fin n → ℕ
  go {suc n} Fin.zero = n
  go (Fin.suc x) = go x

space≤′n : ∀ {n} (x : Fin n) → space x ≤′ n
space≤′n zero    = ≤′-refl
space≤′n (suc x) = ≤′-step (space≤′n x)

-------------------------------------------------------------------------
-- Definition
-------------------------------------------------------------------------

infixl 6 _Δ_
record PowInd {c} (C : Set c) : Set c where
  constructor _Δ_
  field
    coeff : C
    pow   : ℕ
open PowInd public

record Poly (n : ℕ) : Set ℓ₁
data FlatPoly : ℕ → Set ℓ₁
Coeff : ℕ → Set ℓ₁
record NonZero (i : ℕ) : Set ℓ₁
Zero : ∀ {n} → Poly n → Set
Normalised : ∀ {i} → Coeff i + → Set

-- A Polynomial is indexed by the number of variables it contains.
infixl 6 _⊐_
record Poly n where
  inductive
  constructor _⊐_
  field
    {i}  : ℕ
    flat : FlatPoly i
    i≤n  : i ≤′ n

data FlatPoly where
  Κ : Carrier → FlatPoly zero
  ⅀ : ∀ {n} (xs : Coeff n +) {xn : Normalised xs} → FlatPoly (suc n)

Coeff n = PowInd (NonZero n)

-- We disallow zeroes in the coefficient list. This condition alone
-- is enough to ensure a unique representation for any polynomial.
infixl 6 _≠0
record NonZero i where
  inductive
  constructor _≠0
  field
    poly      : Poly i
    .{poly≠0} : ¬ Zero poly

-- This predicate is used (in its negation) to ensure that no
-- coefficient is zero, preventing any trailing zeroes.
Zero (Κ x ⊐ _) = T (isZero x)
Zero (⅀ _ ⊐ _) = ⊥

-- This predicate is used to ensure that all polynomials are in
-- normal form: if a particular level is constant, then it can
-- be collapsed into the level below it.
Normalised (_ Δ zero  & [])  = ⊥
Normalised (_ Δ zero  & ∹ _) = ⊤
Normalised (_ Δ suc _ & _)   = ⊤
open NonZero public
open Poly public

----------------------------------------------------------------------
-- Special operations

-- Decision procedure for Zero
zero? : ∀ {n} → (p : Poly n) → Dec (Zero p)
zero? (⅀ _ ⊐ _) = no id
zero? (Κ x ⊐ _) with isZero x
... | true  = yes tt
... | false = no  id
{-# INLINE zero? #-}

-- Exponentiate the first variable of a polynomial
infixr 8 _⍓*_ _⍓+_
_⍓*_ : ∀ {n} → Coeff n * → ℕ → Coeff n *
_⍓+_ : ∀ {n} → Coeff n + → ℕ → Coeff n +

[] ⍓* _ = []
(∹ xs) ⍓* i = ∹ xs ⍓+ i

coeff (head (xs ⍓+ i)) = coeff (head xs)
pow   (head (xs ⍓+ i)) = pow (head xs) ℕ.+ i
tail  (xs ⍓+ i)        = tail xs

infixr 5 _∷↓_
_∷↓_ : ∀ {n} → PowInd (Poly n) → Coeff n * → Coeff n *
x Δ i ∷↓ xs = case zero? x of
  λ { (yes p) → xs ⍓* suc i
    ; (no ¬p) → ∹ _≠0 x {¬p} Δ i & xs
    }
{-# INLINE _∷↓_ #-}

-- Inject a polynomial into a larger polynomial with more variables
_⊐↑_ : ∀ {n m} → Poly n → (suc n ≤′ m) → Poly m
(xs ⊐ i≤n) ⊐↑ n≤m = xs ⊐ (≤′-step i≤n ⟨ ≤′-trans ⟩ n≤m)
{-# INLINE _⊐↑_ #-}

infixr 4 _⊐↓_
_⊐↓_ : ∀ {i n} → Coeff i * → suc i ≤′ n → Poly n
[]                        ⊐↓ i≤n = Κ 0# ⊐ z≤′n
(∹ (x ≠0 Δ zero  & []  )) ⊐↓ i≤n = x ⊐↑ i≤n
(∹ (x    Δ zero  & ∹ xs)) ⊐↓ i≤n = ⅀ (x Δ zero  & ∹ xs) ⊐ i≤n
(∹ (x    Δ suc j & xs  )) ⊐↓ i≤n = ⅀ (x Δ suc j & xs)   ⊐ i≤n
{-# INLINE _⊐↓_ #-}

----------------------------------------------------------------------
-- Standard operations
----------------------------------------------------------------------

----------------------------------------------------------------------
-- Folds

-- These folds allow us to abstract over the proofs later: we try to avoid
-- using ∷↓ and ⊐↓ directly anywhere except here, so if we prove that this fold
-- acts the same on a normalised or non-normalised polynomial, we can prove th
-- same about any operation which uses it.

PolyF : ℕ → Set ℓ₁
PolyF i = Poly i × Coeff i *

Fold : ℕ → Set ℓ₁
Fold i = PolyF i → PolyF i

para : ∀ {i} → Fold i → Coeff i + → Coeff i *
para f (x ≠0 Δ i & [])   = case f (x , [])        of λ {(y , ys) → y Δ i ∷↓ ys}
para f (x ≠0 Δ i & ∹ xs) = case f (x , para f xs) of λ {(y , ys) → y Δ i ∷↓ ys}

poly-map : ∀ {i} → (Poly i → Poly i) → Coeff i + → Coeff i *
poly-map f = para (map₁ f)
{-# INLINE poly-map #-}

----------------------------------------------------------------------
-- Addition

-- The reason the following code is so verbose is termination
-- checking. For instance, in the third case for ⊞-coeffs, we call a
-- helper function. Instead, you could conceivably use a with-block
-- (on ℕ.compare p q):
--
-- ⊞-coeffs ((x , p) ∷ xs) ((y , q) ∷ ys) with (ℕ.compare p q)
-- ... | ℕ.less    p k = (x , p) ∷ ⊞-coeffs xs ((y , k) ∷ ys)
-- ... | ℕ.equal   p   = (fst~ x ⊞ fst~ y , p) ∷↓ ⊞-coeffs xs ys
-- ... | ℕ.greater q k = (y , q) ∷ ⊞-coeffs ((x , k) ∷ xs) ys
--
-- However, because the first and third recursive calls each rewrap
-- a list that was already pattern-matched on, the recursive call
-- does not strictly decrease the size of its argument.
--
-- Interestingly, if --without-K is turned off, we don't need the
-- helper function ⊞-coeffs; we could pattern match on _⊞_ directly.
--
-- _⊞_ {zero} (lift x) (lift y) = lift (x + y)
-- _⊞_ {suc n} [] ys = ys
-- _⊞_ {suc n} (x ∷ xs) [] = x ∷ xs
-- _⊞_ {suc n} ((x , p) ∷ xs) ((y , q) ∷ ys) = ⊞-zip (ℕ.compare p q) x xs y ys

mutual
  infixl 6 _⊞_
  _⊞_ : ∀ {n} → Poly n → Poly n → Poly n
  (xs ⊐ i≤n) ⊞ (ys ⊐ j≤n) = ⊞-match (inj-compare i≤n j≤n) xs ys

  ⊞-match : ∀ {i j n}
        → {i≤n : i ≤′ n}
        → {j≤n : j ≤′ n}
        → InjectionOrdering i≤n j≤n
        → FlatPoly i
        → FlatPoly j
        → Poly n
  ⊞-match (inj-eq i&j≤n)     (Κ x)  (Κ y)  = Κ (x + y)         ⊐  i&j≤n
  ⊞-match (inj-eq i&j≤n)     (⅀ (x Δ i & xs)) (⅀ (y Δ j & ys)) = ⊞-zip (compare i j) x xs y ys ⊐↓ i&j≤n
  ⊞-match (inj-lt i≤j-1 j≤n)  xs    (⅀ ys) = ⊞-inj i≤j-1 xs ys ⊐↓ j≤n
  ⊞-match (inj-gt i≤n j≤i-1) (⅀ xs)  ys    = ⊞-inj j≤i-1 ys xs ⊐↓ i≤n

  ⊞-inj : ∀ {i k}
        → (i ≤′ k)
        → FlatPoly i
        → Coeff k +
        → Coeff k *
  ⊞-inj i≤k xs (y ⊐ j≤k ≠0 Δ zero  & ys) = ⊞-match (inj-compare j≤k i≤k) y xs Δ zero ∷↓ ys
  ⊞-inj i≤k xs (y          Δ suc j & ys) = xs ⊐ i≤k Δ zero ∷↓ ∹ y Δ j & ys

  ⊞-coeffs : ∀ {n} → Coeff n * → Coeff n * → Coeff n *
  ⊞-coeffs (∹ x Δ i & xs) ys = ⊞-zip-r x i xs ys
  ⊞-coeffs []             ys = ys

  ⊞-zip : ∀ {p q n}
        → ℕ.Ordering p q
        → NonZero n
        → Coeff n *
        → NonZero n
        → Coeff n *
        → Coeff n *
  ⊞-zip (ℕ.less    i k) x xs y ys = ∹ x Δ i & ⊞-zip-r y k ys xs
  ⊞-zip (ℕ.greater j k) x xs y ys = ∹ y Δ j & ⊞-zip-r x k xs ys
  ⊞-zip (ℕ.equal   i  ) x xs y ys = (x .poly ⊞ y .poly) Δ i ∷↓ ⊞-coeffs xs ys
  {-# INLINE ⊞-zip #-}

  ⊞-zip-r : ∀ {n} → NonZero n → ℕ → Coeff n * → Coeff n * → Coeff n *
  ⊞-zip-r x i xs [] = ∹ x Δ i & xs
  ⊞-zip-r x i xs (∹ y Δ j & ys) = ⊞-zip (compare i j) x xs y ys

----------------------------------------------------------------------
-- Negation

-- recurse on acc directly
-- https://github.com/agda/agda/issues/3190#issuecomment-416900716

⊟-step : ∀ {n} → Acc _<′_ n → Poly n → Poly n
⊟-step (acc wf) (Κ x  ⊐ i≤n) = Κ (- x) ⊐ i≤n
⊟-step (acc wf) (⅀ xs ⊐ i≤n) = poly-map (⊟-step (wf _ i≤n)) xs ⊐↓ i≤n

⊟_ : ∀ {n} → Poly n → Poly n
⊟_ = ⊟-step (<′-wellFounded _)
{-# INLINE ⊟_ #-}

----------------------------------------------------------------------
-- Multiplication

mutual
  ⊠-step′ : ∀ {n} → Acc _<′_ n → Poly n → Poly n → Poly n
  ⊠-step′ a (x ⊐ i≤n) = ⊠-step a x i≤n

  ⊠-step : ∀ {i n} → Acc _<′_ n → FlatPoly i → i ≤′ n → Poly n → Poly n
  ⊠-step a (Κ x) _ = ⊠-Κ a x
  ⊠-step a (⅀ xs)  = ⊠-⅀ a xs

  ⊠-Κ : ∀ {n} → Acc _<′_ n → Carrier → Poly n → Poly n
  ⊠-Κ (acc _ ) x (Κ y  ⊐ i≤n) = Κ (x * y) ⊐ i≤n
  ⊠-Κ (acc wf) x (⅀ xs ⊐ i≤n) = ⊠-Κ-inj (wf _ i≤n) x xs ⊐↓ i≤n
  {-# INLINE ⊠-Κ #-}

  ⊠-⅀ : ∀ {i n} → Acc _<′_ n → Coeff i + → i <′ n → Poly n → Poly n
  ⊠-⅀ (acc wf) xs i≤n (⅀ ys ⊐ j≤n) = ⊠-match  (acc wf) (inj-compare i≤n j≤n) xs ys
  ⊠-⅀ (acc wf) xs i≤n (Κ y ⊐ _)    = ⊠-Κ-inj (wf _ i≤n) y xs ⊐↓ i≤n

  ⊠-Κ-inj : ∀ {i}  → Acc _<′_ i → Carrier → Coeff i + → Coeff i *
  ⊠-Κ-inj a x xs = poly-map (⊠-Κ a x) (xs)

  ⊠-⅀-inj : ∀ {i k}
          → Acc _<′_ k
          → i <′ k
          → Coeff i +
          → Poly k
          → Poly k
  ⊠-⅀-inj (acc wf) i≤k x (⅀ y ⊐ j≤k) = ⊠-match (acc wf) (inj-compare i≤k j≤k) x y
  ⊠-⅀-inj (acc wf) i≤k x (Κ y ⊐ j≤k) = ⊠-Κ-inj (wf _ i≤k) y x ⊐↓ i≤k

  ⊠-match : ∀ {i j n}
          → Acc _<′_ n
          → {i≤n : i <′ n}
          → {j≤n : j <′ n}
          → InjectionOrdering i≤n j≤n
          → Coeff i +
          → Coeff j +
          → Poly n
  ⊠-match (acc wf) (inj-eq i&j≤n)     xs ys = ⊠-coeffs (wf _ i&j≤n) xs ys               ⊐↓ i&j≤n
  ⊠-match (acc wf) (inj-lt i≤j-1 j≤n) xs ys = poly-map (⊠-⅀-inj (wf _ j≤n) i≤j-1 xs) (ys) ⊐↓ j≤n
  ⊠-match (acc wf) (inj-gt i≤n j≤i-1) xs ys = poly-map (⊠-⅀-inj (wf _ i≤n) j≤i-1 ys) (xs) ⊐↓ i≤n

  ⊠-coeffs : ∀ {n} → Acc _<′_ n → Coeff n + → Coeff n + → Coeff n *
  ⊠-coeffs a (xs) (y ≠0 Δ j & [])   = poly-map (⊠-step′ a y) (xs) ⍓* j
  ⊠-coeffs a (xs) (y ≠0 Δ j & ∹ ys) = para (⊠-cons a y ys) (xs) ⍓* j
  {-# INLINE ⊠-coeffs #-}

  ⊠-cons : ∀ {n}
          → Acc _<′_ n
          → Poly n
          → Coeff n +
          → Fold n
  ⊠-cons a y ys (x ⊐ j≤n , xs) =
    ⊠-step a x j≤n y , ⊞-coeffs (poly-map (⊠-step a x j≤n) ys) xs
  {-# INLINE ⊠-cons #-}

infixl 7 _⊠_
_⊠_ : ∀ {n} → Poly n → Poly n → Poly n
_⊠_ = ⊠-step′ (<′-wellFounded _)
{-# INLINE _⊠_ #-}

----------------------------------------------------------------------
-- Constants and variables

-- The constant polynomial
κ : ∀ {n} → Carrier → Poly n
κ x = Κ x ⊐ z≤′n
{-# INLINE κ #-}

-- A variable
ι : ∀ {n} → Fin n → Poly n
ι i = (κ 1# Δ 1 ∷↓ []) ⊐↓ space≤′n i
{-# INLINE ι #-}

----------------------------------------------------------------------
-- Exponentiation

-- We try very hard to never do things like multiply by 1
-- unnecessarily. That's what all the weirdness here is for.

⊡-mult : ∀ {n} → ℕ → Poly n → Poly n
⊡-mult zero    xs = xs
⊡-mult (suc n) xs = ⊡-mult n xs ⊠ xs

_⊡_+1 : ∀ {n} → Poly n → ℕ → Poly n
(Κ x  ⊐ i≤n)           ⊡ i +1  = Κ (x ^ i +1) ⊐ i≤n
(⅀ (x Δ j & []) ⊐ i≤n) ⊡ i +1  = x .poly ⊡ i +1 Δ (j ℕ.+ i ℕ.* j) ∷↓ [] ⊐↓ i≤n
xs@(⅀ (_ & ∹ _) ⊐ i≤n) ⊡ i +1  = ⊡-mult i xs

infixr 8 _⊡_
_⊡_ : ∀ {n} → Poly n → ℕ → Poly n
_  ⊡ zero  = κ 1#
xs ⊡ suc i = xs ⊡ i +1
{-# INLINE _⊡_ #-}


text:
open import Agda.Builtin.Nat

f : Nat → Nat
f v@n with n
... | zero = zero
... | suc m with m
...   | zero  = {!!}
...   | suc o with o
...     | zero  = {!!}
...     | suc p = {!!}


text:
import      Lvl
open import Type

module Type.Cardinality {ℓₗ : Lvl.Level} where

import Type.Functions
import Logic.Predicate

module _ {ℓₒ₁}{ℓₒ₂} (X : Type{ℓₒ₁}) (Y : Type{ℓₒ₂}) where
  open Type.Functions{ℓₗ}{ℓₒ₁}{ℓₒ₂}
  open Logic.Predicate{ℓₗ}

  _≍_ : Type{ℓₗ Lvl.⊔ ℓₒ₁ Lvl.⊔ ℓₒ₂}
  _≍_ = ∃(Bijective{X}{Y})

  _≼_ : Type{ℓₗ Lvl.⊔ ℓₒ₁ Lvl.⊔ ℓₒ₂}
  _≼_ = ∃(Injective{X}{Y})

  _≽_ : Type{ℓₗ Lvl.⊔ ℓₒ₁ Lvl.⊔ ℓₒ₂}
  _≽_ = ∃(Surjective{X}{Y})

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 module-layout where
 f : Set1
 f = Set

max_stars_repo_name: dubinsky/intellij-dtlc

max_issues_repo_name: dubinsky/intellij-dtlc

max_forks_repo_name: dubinsky/intellij-dtlc


text:
{-# OPTIONS --without-K #-}
module HoTT.Base where

open import Agda.Primitive public

-- Universe
𝒰 : (i : Level) → Set (lsuc i)
𝒰 i = Set i

𝒰₀ : Set₁
𝒰₀ = Set₀

module variables where
  variable
    i j : Level
    A B : 𝒰 i
    P Q : A → 𝒰 i
open variables

record Lift {i j} (A : 𝒰 j) : 𝒰 (i ⊔ j) where
  constructor lift
  field lower : A
open Lift public

-- Instance search
⟨⟩ : ∀ {i} {A : 𝒰 i} → ⦃ A ⦄ → A
⟨⟩ ⦃ a ⦄ = a

-- Dependent functions (Π-types)
Π : (A : 𝒰 i) (B : A → 𝒰 j) → 𝒰 (i ⊔ j)
Π A B = (x : A) → B x
syntax Π A (λ x → Φ) = Π[ x ∶ A ] Φ
infixr 6 Π

id : {A : 𝒰 i} → A → A
id x = x

const : A → B → A
const x _ = x

swap : {C : A → B → 𝒰 i} → ((x : A) (y : B) → C x y) →
       (y : B) (x : A) → C x y
swap f y x = f x y

_∘_ : {C : {x : A} → P x → 𝒰 i} →
      ({x : A} → Π (P x) C) → (g : Π A P) → (x : A) → C (g x)
f ∘ g = λ x → f (g x)
infixr 30 _∘_

_$_ : Π A P → Π A P
_$_ = id
infixr 0 _$_

-- Identity
data _==_ {A : 𝒰 i} (a : A) : A → 𝒰 i where
  instance refl : a == a
infixr 10 _==_
{-# BUILTIN EQUALITY _==_ #-}

=-ind : (C : (x y : A) → x == y → 𝒰 i) → ((x : A) → C x x refl) →
        {x y : A} → (p : x == y) → C x y p
=-ind C c refl = c _

-- Based path induction
=-ind' : {a : A} → (C : (x : A) → a == x → 𝒰 i) → C a refl →
         {x : A} → (p : a == x) → C x p
=-ind' C c refl = c

-- Lemma 2.1.1
_⁻¹ : {x y : A} → x == y → y == x
_⁻¹ refl = refl
infix 30 _⁻¹

-- Lemma 2.1.2
_∙_ : {x y z : A} → x == y → y == z → x == z
_∙_ refl refl = refl
infixl 20 _∙_

-- Lemma 2.2.1
ap : {x y : A} (f : A → B) → x == y → f x == f y
ap f refl = refl

ap² : {C : 𝒰 i} {x y : A} {z w : B} (f : A → B → C) → x == y → z == w → f x z == f y w
ap² _ refl refl = refl

-- Lemma 2.3.1
transport : {x y : A} (P : A → 𝒰 j) → x == y → P x → P y
transport _ refl = id

-- Lemma 2.3.4
apd : {x y : A} (f : (x : A) → P x) (p : x == y) → transport P p (f x) == f y
apd f refl = refl

-- Empty
data 𝟎 {i} : 𝒰 i where

𝟎-rec : {C : 𝒰 i} → 𝟎 {j} → C
𝟎-rec ()

𝟎-ind : {C : 𝟎 → 𝒰 i} → (z : 𝟎 {j}) → C z
𝟎-ind ()

¬_ : 𝒰 i → 𝒰 i
¬_ {i} A = A → 𝟎 {i}
infix 25 ¬_

_≠_ : A → A → 𝒰 _
_≠_ x y = ¬ (x == y)

-- Unit
record 𝟏 {i} : 𝒰 i where
  no-eta-equality
  instance constructor ★

𝟏-ind : (C : 𝟏 → 𝒰 i) → C ★ → (x : 𝟏 {j}) → C x
𝟏-ind C c ★ = c

𝟏-uniq : (x : 𝟏 {i}) → x == ★
𝟏-uniq ★ = refl

-- Boolean
data 𝟐 : 𝒰₀ where
  0₂ : 𝟐
  1₂ : 𝟐
{-# BUILTIN BOOL 𝟐 #-}
{-# BUILTIN FALSE 0₂ #-}
{-# BUILTIN TRUE 1₂ #-}

𝟐-rec : {C : 𝒰 i} → C → C → 𝟐 → C
𝟐-rec c₀ c₁ 0₂ = c₀
𝟐-rec c₀ c₁ 1₂ = c₁

𝟐-ind : (C : 𝟐 → 𝒰 i) → C 0₂ → C 1₂ → (x : 𝟐) → C x
𝟐-ind C c₀ c₁ 0₂ = c₀
𝟐-ind C c₀ c₁ 1₂ = c₁

-- Dependent pairs (Σ-types)
record Σ (A : 𝒰 i) (B : A → 𝒰 j) : 𝒰 (i ⊔ j) where
  no-eta-equality
  constructor _,_
  field
    pr₁ : A
    pr₂ : B pr₁
infixr 15 _,_
open Σ public
syntax Σ A (λ x → Φ) = Σ[ x ∶ A ] Φ
infixr 6 Σ

Σ-rec : (C : 𝒰 i) → ((x : A) → P x → C) → (Σ A λ x → P x) → C
Σ-rec C g (a , b) = g a b

Σ-ind : (C : Σ A P → 𝒰 i) → ((a : A) → (b : P a) → C (a , b)) →
        (p : Σ A P) → C p
Σ-ind C g (a , b) = g a b

Σ-uniq : (x : Σ A P) → pr₁ x , pr₂ x == x
Σ-uniq (a , b) = refl

-- Product
_×_ : (A : 𝒰 i) (B : 𝒰 j) → 𝒰 (i ⊔ j)
A × B = Σ[ _ ∶ A ] B
infixr 8 _×_

×-rec : (C : 𝒰 i) → (A → B → C) → A × B → C
×-rec _ g (a , b) = g a b

×-ind : (C : A × B → 𝒰 i) → ((x : A) (y : B) → C (x , y)) →
        (x : A × B) → C x
×-ind _ g (a , b) = g a b

×-uniq : (x : A × B) → pr₁ x , pr₂ x == x
×-uniq (a , b) = refl

-- Coproduct
data _+_ (A : 𝒰 i) (B : 𝒰 j) : 𝒰 (i ⊔ j) where
  inl : A → A + B
  inr : B → A + B
infixr 8 _+_

+-rec : {C : 𝒰 i} → (A → C) → (B → C) → A + B → C
+-rec gₗ gᵣ (inl a) = gₗ a
+-rec gₗ gᵣ (inr b) = gᵣ b

+-ind : (C : A + B → 𝒰 i) →
        ((a : A) → C (inl a)) →
        ((b : B) → C (inr b)) → (x : A + B) → C x
+-ind C g₀ g₁ (inl a) = g₀ a
+-ind C g₀ g₁ (inr b) = g₁ b

-- Natural numbers
data ℕ : 𝒰₀ where
  zero : ℕ
  succ : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

ℕ-rec : {C : 𝒰 i} → C → (ℕ → C → C) → ℕ → C
ℕ-rec c₀ cₛ zero = c₀
ℕ-rec c₀ cₛ (succ n) = cₛ n (ℕ-rec c₀ cₛ n)

ℕ-ind : (C : ℕ → 𝒰 i) → C 0 → ((n : ℕ) → C n → C (succ n)) → (n : ℕ) → C n
ℕ-ind C c₀ cₛ 0 = c₀
ℕ-ind C c₀ cₛ (succ n) = cₛ n (ℕ-ind C c₀ cₛ n)

-- Homotopy
_~_ : (f g : Π A P) → 𝒰 _
f ~ g = ∀ x → f x == g x

happly : {f g : Π A P} → f == g → f ~ g
happly refl _ = refl

-- Lemma 2.4.2
reflₕ : {f : Π A P} → f ~ f
reflₕ _ = refl

_∙ₕ_ : {f g h : Π A P} → f ~ g → g ~ h → f ~ h
α ∙ₕ β = λ x → α x ∙ β x
infixl 20 _∙ₕ_

_⁻¹ₕ : {f g : Π A P} → f ~ g → g ~ f
α ⁻¹ₕ = λ x → α x ⁻¹

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


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

open import HoTT

open import stash.modalities.JoinAdj

module stash.modalities.Orthogonality where

  module PathSplit {i} (X : Type i) (x y : X) where

    to : (x == y) → Σ X (λ z → (x == z) × (z == y))
    to p = x , (idp , p)

    from : Σ X (λ z → (x == z) × (z == y)) → x == y
    from (z , p , q) = p ∙ q

    abstract

      to-from : (b : Σ X (λ z → (x == z) × (z == y))) → to (from b) == b
      to-from (z , p , q) = pair= p (↓-×-in (↓-cst=idf-in (∙'-unit-l p)) (↓-idf=cst-in idp))

      from-to : (p : x == y) → from (to p) == p
      from-to p = idp

    path-split : (x == y) ≃ Σ X (λ z → (x == z) × (z == y))
    path-split = equiv to from to-from from-to

  module _ {i} where

    Δ : (X A : Type i) → X → (A → X)
    Δ X A = cst

    -- Δ-ap : {X A : Type i} {x y : X} (φ : A → x == y) (a : A)
    --   → λ= φ == ap cst (φ a)
    -- Δ-ap φ a = equiv-is-inj {f = app=} (snd app=-equiv) (λ= φ) (ap cst (φ a)) (λ= (λ a₀ → app=-β φ a₀ ∙ {!lem a₀!}))

    --   where lem : ∀ a₀ → φ a₀ == app= (ap cst (φ a₀)) a₀
    --         lem = {!!}

    ⟦_⊥_⟧ : (A : Type i) (X : Type i) → Type i
    ⟦ A ⊥ X ⟧ = is-equiv (Δ X A)

    ctr : {A X : Type i} → ⟦ A ⊥ X ⟧ → (A → X) → X
    ctr A⊥X φ = is-equiv.g A⊥X φ

    ctr-null : {A X : Type i} (A⊥X : ⟦ A ⊥ X ⟧) (φ : A → X)
      → cst (ctr A⊥X φ) == φ
    ctr-null A⊥X φ = is-equiv.f-g A⊥X φ

    ctr-cst : {A X : Type i} (A⊥X : ⟦ A ⊥ X ⟧)
      → (x : X) → ctr A⊥X (cst x) == x
    ctr-cst A⊥X x = is-equiv.g-f A⊥X x

    Unit-orth : (A : Type i) → ⟦ Lift ⊤ ⊥ A ⟧
    Unit-orth A = record {
      g = λ φ → φ (lift unit) ;
      f-g = λ φ → λ= (λ { (lift unit) → idp }) ;
      g-f = λ a → idp ;
      adj = λ a → λ=-η idp }

    Δ-equiv-is-contr : (A : Type i) → is-equiv (Δ A A) → is-contr A
    Δ-equiv-is-contr A e = is-equiv.g e (idf A) , (λ a → app= (is-equiv.f-g e (idf A)) a)

    self-orth-is-contr : (A : Type i) → ⟦ A ⊥ A ⟧ → is-contr A
    self-orth-is-contr A ω = Δ-equiv-is-contr A ω

    equiv-preserves-orth-l : {A B X : Type i} → (A ≃ B) → ⟦ A ⊥ X ⟧ → ⟦ B ⊥ X ⟧
    equiv-preserves-orth-l {A} {B} {X} (f , f-ise) ω = is-eq (Δ X B) g f-g ω.g-f

      where module ω = is-equiv ω
            module f = is-equiv f-ise

            g : (B → X) → X
            g φ = ω.g (φ ∘ f)

            f-g : (φ : B → X) → Δ X B (g φ) == φ
            f-g φ = λ= λ b → app= (ω.f-g (φ ∘ f)) (f.g b) ∙ ap φ (f.f-g b)

    equiv-preserves-orth-r : {A X Y : Type i} → (X ≃ Y) → ⟦ A ⊥ X ⟧ → ⟦ A ⊥ Y ⟧
    equiv-preserves-orth-r {A} {X} {Y} (f , f-ise) ω = is-eq (Δ Y A) g f-g g-f

      where module ω = is-equiv ω
            module f = is-equiv f-ise

            g : (A → Y) → Y
            g φ = f (ω.g (f.g ∘ φ))

            f-g : (φ : A → Y) → Δ Y A (g φ) == φ
            f-g φ = λ= λ x → ap f (app= (ω.f-g (f.g ∘ φ)) x) ∙ f.f-g (φ x)

            g-f : (y : Y) → g (Δ Y A y) == y
            g-f y = ap f (ω.g-f (f.g y)) ∙ f.f-g y

    Σ-orth : {A X : Type i} {B : A → Type i} → ⟦ A ⊥ X ⟧ → (B⊥ : (a : A) → ⟦ B a ⊥ X ⟧) → ⟦ Σ A B ⊥ X ⟧
    Σ-orth {A} {X} {B} A⊥ B⊥ = is-eq _ from to-from from-to

      where from : (Σ A B → X) → X
            from φ = ctr A⊥ (λ a → ctr (B⊥ a) (λ b → φ (a , b)))

            to-from : (φ : Σ A B → X) → cst (from φ) == φ
            to-from φ = λ= (λ { (a , b) → app= (ctr-null A⊥ (λ a → ctr (B⊥ a) (λ b → φ (a , b)))) a ∙
                                           app= (ctr-null (B⊥ a) (λ b → φ (a , b))) b })

            from-to : (x : X) → from (cst x) == x
            from-to x = ap (ctr A⊥) (λ= (λ a → ctr-cst (B⊥ a) x)) ∙ ctr-cst A⊥ x

    -- -- This works if the base is connected, but you'll have to add that
    -- fib-orth : {A X : Type i} {B : A → Type i} → ⟦ Σ A B ⊥ X ⟧ →  (a : A) → ⟦ B a ⊥ X ⟧
    -- fib-orth {A} {X} {B} Σ⊥ a = is-eq _ g {!!} {!!}

    --   where g : (φ : B a → X) → X
    --         g φ = ctr Σ⊥ {!!}

    -- -- This looks doomed ...
    -- base-orth : {A X : Type i} {B : A → Type i} → ⟦ Σ A B ⊥ X ⟧ → ⟦ A ⊥ X ⟧
    -- base-orth {A} {X} {B} Σ⊥ = is-eq _ g f-g {!!}

    --   where g : (φ : A → X) → X
    --         g φ = ctr Σ⊥ (uncurry (λ a _ → φ a))

    --         f-g : (φ : A → X) → cst (g φ) == φ
    --         f-g φ = λ= (λ a → app= (ctr-null Σ⊥ (uncurry (λ a _ → φ a))) (a , {!!}))

    ×-orth : {A B X : Type i} → ⟦ A ⊥ X ⟧ → ⟦ B ⊥ X ⟧ → ⟦ A × B ⊥ X ⟧
    ×-orth {B = B} A⊥ B⊥ = Σ-orth {B = λ _ → B} A⊥ (λ _ → B⊥)

    -- Okay, you need to find a simpler way.
    -- *-orth : {A B X : Type i} → ⟦ B ⊥ X ⟧ → ⟦ A * B ⊥ X ⟧
    -- *-orth {A} {B} {X} ω = is-eq (Δ X (A * B)) from to-from from-to

    --   where from : (A * B → X) → X
    --         from f = is-equiv.g ω (f ∘ right)

    --           where test : A → hfiber cst (f ∘ right)
    --                 test =  snd (–> (join-adj A B X) f)

    --         to-from : (f : A * B → X) → Δ X (A * B) (from f) == f
    --         to-from f = {!!}

    --         from-to : (x : X) → from (Δ X (A * B) x) == x
    --         from-to x = {!is-equiv.g-f ω x!}

    postulate

      -- Right, this is a special case of the join adjunction ...
      adj-orth : (A X : Type i) → ⟦ Susp A ⊥ X ⟧ → (x y : X) → ⟦ A ⊥ x == y ⟧

    pths-orth : {A X : Type i} {x y : X} → ⟦ A ⊥ X ⟧ → ⟦ A ⊥ x == y ⟧
    pths-orth {A} {X} {x} {y} A⊥X = is-eq (Δ (x == y) A) g to-from from-to

      where g : (A → x == y) → x == y
            g φ = ! (ctr-cst A⊥X x) ∙ ap (ctr A⊥X) (λ= φ) ∙ ctr-cst A⊥X y

            to-from : (φ : A → x == y) → Δ (x == y) A (g φ) == φ
            to-from φ = λ= coh

              where coh : (a : A) → g φ == φ a
                    coh a = ! (ctr-cst A⊥X x) ∙ ap (ctr A⊥X) (λ= φ) ∙ ctr-cst A⊥X y =⟨ {!!} ⟩
                            φ a ∎

                      where puzzle = ap (ctr A⊥X) (λ= φ) =⟨ {!a !} ⟩
                                     ap (ctr A⊥X) (ap cst (φ a)) =⟨ ∘-ap (ctr A⊥X) cst (φ a) ⟩
                                     ap ((ctr A⊥X) ∘ cst) (φ a) ∎

                            eq : ctr-cst A⊥X x ∙' φ a == ap ((ctr A⊥X) ∘ cst) (φ a) ∙ ctr-cst A⊥X y
                            eq = ↓-app=idf-out (apd (ctr-cst A⊥X) (φ a))

                            eq₀ : ctr-null A⊥X (cst x) ∙' λ= φ == ap (cst ∘ (ctr A⊥X)) (λ= φ) ∙ ctr-null A⊥X (cst y)
                            eq₀ = ↓-app=idf-out (apd (ctr-null A⊥X) (λ= φ))

                            adj : ap cst (ctr-cst A⊥X x) == ctr-null A⊥X (cst x)
                            adj = is-equiv.adj A⊥X x

                            adj' : ap (ctr A⊥X) (ctr-null A⊥X (cst x)) == ctr-cst A⊥X (ctr A⊥X (cst x))
                            adj' = is-equiv.adj' A⊥X (cst x)

                            claim : (λ= φ) == ! (ap cst (ctr-cst A⊥X x)) ∙ ap cst (ap (ctr A⊥X) (λ= φ)) ∙ ap cst (ctr-cst A⊥X y)
                            claim = {!!}

                            then : (λ= φ) == ap cst (! (ctr-cst A⊥X x) ∙ ap (ctr A⊥X) (λ= φ) ∙ ctr-cst A⊥X y)
                            then = {!!}

            from-to : (p : x == y) → g (cst p) == p
            from-to p = {!!}

  -- Weak cellular inequalities
  module _ {i} where

    _≻_ : Type i → Type i → Type _
    X ≻ A = (Y : Type i) → ⟦ A ⊥ Y ⟧ → ⟦ X ⊥ Y ⟧

    equiv-preserves-≻-l : {X Y : Type i} {A : Type i} → X ≃ Y → X ≻ A → Y ≻ A
    equiv-preserves-≻-l {X} {Y} {A} e ω Z o = equiv-preserves-orth-l e (ω Z o)

    ≻-trivial : (A : Type i) → (Lift ⊤) ≻ A
    ≻-trivial A X _ = Unit-orth X

    ≻-reflexive : (A : Type i) → A ≻ A
    ≻-reflexive A Y x = x

    ≻-trans : (A B C : Type i) → A ≻ B → B ≻ C → A ≻ C
    ≻-trans A B C ω₀ ω₁ Y cy = ω₀ Y (ω₁ Y cy)

    ≻-⊤-is-contr : (A : Type i) → A ≻ (Lift ⊤) → is-contr A
    ≻-⊤-is-contr A ω = self-orth-is-contr A (ω A (Unit-orth A))

    Σ-≻ : {A X : Type i} {P : X → Type i} → X ≻ A → (P≻A : (x : X) → P x ≻ A) → Σ X P ≻ A
    Σ-≻ X≻A P≻A Y A⊥Y = Σ-orth (X≻A Y A⊥Y) (λ x → P≻A x Y A⊥Y)

    -- We jump a universe level, but its certainly convenient ...
    is-hyper-prop : Type i → Type (lsucc i)
    is-hyper-prop A = (X Y : Type i) (f : X → Y) → X ≻ A → Y ≻ A → (y : Y) → hfiber f y ≻ A

    hp-kills-paths : (A : Type i) → is-hyper-prop A
      → (X : Type i) → X ≻ A
      → (x y : X) → (x == y) ≻ A
    hp-kills-paths A hp X X≻A x y = equiv-preserves-≻-l
      (equiv snd (λ p → (_ , p)) (λ _ → idp) (λ _ → idp))
      (hp (Lift ⊤) X (λ _ → x) (≻-trivial A) X≻A y)

    -- Okay, so in some sense this is much more natural.
    -- It just says the connected guys have to be closed under
    -- diagonals.
    kills-paths-hp : (A : Type i)
      → (κ : (X : Type i) → X ≻ A → (x y : X) → (x == y) ≻ A)
      → is-hyper-prop A
    kills-paths-hp A κ X Y f X≻A Y≻A y = Σ-≻ X≻A (λ x → κ Y Y≻A (f x) y)

    -- You'll have to think a bit about why this is equivalent
    -- to *preserving* the path spaces.

    ×-≻ : {A B X : Type i} → A ≻ X → B ≻ X → A × B ≻ X
    ×-≻ ω₀ ω₁ Y e = ×-orth (ω₀ Y e) (ω₁ Y e)

    postulate
      susp-≻ : (A : Type i) → Susp A ≻ A

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module sort where

open import bool
open import eq
open import nat
open import list
open import nondet
open import nondet-thms

-- non-deterministic insert.
--This takes a nondeterministic list because I need to be able to call it with the result of perm
--
--implementation in curry:
-- ndinsert x [] = []
-- ndinsert x (y:ys) = (x : y : xs) ? (y : insert x ys)
ndinsert : {A : Set} -> A -> ND (list A) -> ND (list A)
ndinsert x (Val [] )       = Val ( x :: [])
ndinsert x (Val (y :: ys)) = (Val ( x :: y :: ys )) ?? ((_::_ y) $* (ndinsert x (Val ys)))
ndinsert x (l ?? r)        = (ndinsert x l) ?? (ndinsert x r)

--non-deterministic permutation
--this is identical to the curry code (except for the Val constructor)
perm : {A : Set} -> (list A) -> ND (list A)
perm []        = Val []
perm (x :: xs) = ndinsert x (perm xs)

--insert a value into a sorted list.
--this is identical to curry or haskell code.
--
--note that the structure here is identical to ndinsert
insert : {A : Set} -> (A -> A -> 𝔹) -> A -> list A -> list A
insert _   x []        = x :: []
insert _<_ x (y :: ys) = if x < y
                         then (x :: y :: ys)
                         else (y :: insert _<_ x ys)

--simple insertion sort
--again this is identical to curry or haskell
--also, note that the structure is identical to perm
sort : {A : Set} -> (A -> A -> 𝔹) -> list A -> list A
sort _ []     = []
sort p (x :: xs) = insert p x (sort p xs)

-- Proof:  if xs ∈ nxs then x::xs ∈ ndinsert x nxs
insId : {A : Set} -> (x : A) -> (xs : list A) -> (x :: xs) ∈ (ndinsert x (Val xs))
insId x [] = ndrefl
insId x (y :: xs) = left (Val (x :: y :: xs)) ((_::_ y) $* (ndinsert x (Val xs))) ndrefl

--If introduction rule for non-deterministic values.
--if x and y are both possible values in z then
--∀ c. if c then x else y will give us either x or y, so it must be a possible value of z.
--
ifIntro : {A : Set} -> (x : A) -> (y : A) -> (z : ND A) -> (p : x ∈ z) -> (q : y ∈ z) -> (c : 𝔹) -> (if c then x else y) ∈ z
ifIntro x y z p q tt = p
ifIntro x y z p q ff = q

---------------------------------------------------------------------------
--
-- this should prove that if xs ∈ nxs then, insert x xs ∈ ndinsert x nxs
-- parameters:
-- c         : a comparison operator that is needed for insert
-- x         : the value we are inserting into the list
-- xs        : the list
-- nxs       : a non-deterministic list, we know that xs is a possible value for nxs
-- xs ∈ nxs : the proof that xs is somewhere in nxs
--
--retruns: insert c x xs ∈ ndinsert x nxs
--  a proof that inserting a value in a list is ok with non-deterministic lists
insert=ndinsert : {A : Set} -> (c : A -> A -> 𝔹) -> (x : A) -> (xs : list A) -> (nxs : ND (list A)) -> xs ∈ nxs -> (insert c x xs) ∈ (ndinsert x nxs)

--the first two cases are simple, either we are inserting into an empty list, in which case it's trivial
--or, the list doesn't match the non-deterministic case.  This is an imposible case
insert=ndinsert _ x [] (Val [])       _  = ndrefl
insert=ndinsert _ x [] (Val (_ :: _)) ()

--the next two cases are just structural recursion on the non-deterministic tree.
insert=ndinsert c x ys (l ?? r) (left  .l .r p) = left  (ndinsert x l) (ndinsert x r) (insert=ndinsert c x ys l p)
insert=ndinsert c x ys (l ?? r) (right .l .r p) = right (ndinsert x l) (ndinsert x r) (insert=ndinsert c x ys r p)

--The final case is the interesting one.
--We reached a leaf in the non-deterministic tree, so we have a deterministic value.
--by definition this is equal to the deterministic list (y :: ys)
--At this point we have two possible cases.
--Either x is smaller then every element in (y :: ys), in which case it's inserted at the front,
--or x is larger than y, in which case it's inserted somewhere in ys.
--Since both of these cases are covered by ndinsert we can invoke the ifIntro lemma, to say that we don't care which case it is.
--
--variables:
-- step    : one step of insert
-- l       : the left hand side of insert c x xs (the then branch)
-- r       : the right hand side of insert c x xs (the else branch)
-- nr      : a non-deterministic r
-- (Val l) : a non-deterministic l (but since ndinsert only has a deterministic value on the left it's not very interesting)
-- rec     : The recursive call.  If x isn't inserted into the front, then we need to find it.
-- l∈step : a proof that l is a possible value for step
-- r∈step : a proof that r is a possible value for step
insert=ndinsert _<_ x (y :: ys) (Val (.y :: .ys)) ndrefl = ifIntro l r step l∈step r∈step (x < y)
  where step   = ndinsert x (Val (y :: ys))
        l      = ( x :: y :: ys)
        r      = y :: insert _<_ x ys
        nr     = (_::_ y) $* (ndinsert x (Val ys))
        rec    = ∈-$* (_::_ y) (insert _<_ x ys) (ndinsert x (Val ys)) (insert=ndinsert _<_ x ys (Val ys) ndrefl)
        r∈step = right (Val l) nr rec
        l∈step = left  (Val l) nr ndrefl

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

-- main theorem.  Sorting a list preserves permutations
--all of the work is really done by insert=ndinsert
sortPerm : {A : Set} -> (c : A -> A -> 𝔹) -> (xs : list A) -> sort c xs ∈ perm xs
sortPerm _<_ []        = ndrefl
sortPerm _<_ (x :: xs) = insert=ndinsert _<_ x (sort _<_ xs) (perm xs) (sortPerm _<_ xs)

max_stars_repo_name: mihanus/curry-agda

max_issues_repo_name: mihanus/curry-agda

max_forks_repo_name: mihanus/curry-agda


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas
open import Rings.Subrings.Definition
open import Rings.Cosets
open import Rings.Isomorphisms.Definition
open import Groups.Isomorphisms.Definition

module Rings.Ideals.FirstIsomorphismTheorem {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_+A_ _*A_ : A → A → A} {_+B_ _*B_ : B → B → B} {R1 : Ring S _+A_ _*A_} {R2 : Ring T _+B_ _*B_} {f : A → B} (hom : RingHom R1 R2 f) where

open import Rings.Quotients.Definition R1 R2 hom
open import Rings.Homomorphisms.Image hom
open import Rings.Homomorphisms.Kernel hom
open Setoid T
open Equivalence eq
open import Groups.FirstIsomorphismTheorem (RingHom.groupHom hom)

ringFirstIsomorphismTheorem : RingsIsomorphic (cosetRing R1 ringKernelIsIdeal) (subringIsRing R2 imageGroupSubring)
RingsIsomorphic.f ringFirstIsomorphismTheorem = GroupsIsomorphic.isomorphism groupFirstIsomorphismTheorem
RingHom.preserves1 (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem)) = RingHom.preserves1 hom
RingHom.ringHom (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem)) = RingHom.ringHom hom
GroupHom.groupHom (RingHom.groupHom (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem))) = GroupHom.groupHom (RingHom.groupHom hom)
GroupHom.wellDefined (RingHom.groupHom (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem))) {x} {y} x=y = transferToRight (Ring.additiveGroup R2) t
  where
    t : f x +B Group.inverse (Ring.additiveGroup R2) (f y) ∼ Ring.0R R2
    t = transitive (Ring.groupIsAbelian R2) (transitive (Group.+WellDefined (Ring.additiveGroup R2) (symmetric (homRespectsInverse (RingHom.groupHom hom))) reflexive) (transitive (symmetric (GroupHom.groupHom (RingHom.groupHom hom))) x=y))
RingIso.bijective (RingsIsomorphic.iso ringFirstIsomorphismTheorem) = GroupIso.bij (GroupsIsomorphic.proof groupFirstIsomorphismTheorem)

ringFirstIsomorphismTheorem' : RingsIsomorphic quotientByRingHom (subringIsRing R2 imageGroupSubring)
RingsIsomorphic.f ringFirstIsomorphismTheorem' a = f a , (a , reflexive)
RingHom.preserves1 (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem')) = RingHom.preserves1 hom
RingHom.ringHom (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem')) {r} {s} = RingHom.ringHom hom
RingHom.groupHom (RingIso.ringHom (RingsIsomorphic.iso ringFirstIsomorphismTheorem')) = GroupIso.groupHom (GroupsIsomorphic.proof (groupFirstIsomorphismTheorem'))
RingIso.bijective (RingsIsomorphic.iso ringFirstIsomorphismTheorem') = GroupIso.bij (GroupsIsomorphic.proof groupFirstIsomorphismTheorem')


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to All
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.All.Properties where

open import Axiom.Extensionality.Propositional using (Extensionality)
open import Data.Bool.Base using (Bool; T)
open import Data.Bool.Properties
open import Data.Empty
open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
open import Data.List.Base
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
import Data.List.Relation.Binary.Equality.Setoid as ListEq using (_≋_; []; _∷_)
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Data.Maybe.Relation.Unary.All as MAll using (just; nothing)
open import Data.Nat using (zero; suc; z≤n; s≤s; _<_)
open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; equivalence; Equivalence)
open import Function.Inverse using (_↔_; inverse)
open import Function.Surjection using (_↠_; surjection)
open import Relation.Binary using (Setoid; _Respects_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Unary
  using (Decidable; Pred; Universal) renaming (_⊆_ to _⋐_)

------------------------------------------------------------------------
-- Lemmas relating Any, All and negation.

module _ {a p} {A : Set a} {P : A → Set p} where

  ¬Any⇒All¬ : ∀ xs → ¬ Any P xs → All (¬_ ∘ P) xs
  ¬Any⇒All¬ []       ¬p = []
  ¬Any⇒All¬ (x ∷ xs) ¬p = ¬p ∘ here ∷ ¬Any⇒All¬ xs (¬p ∘ there)

  All¬⇒¬Any : ∀ {xs} → All (¬_ ∘ P) xs → ¬ Any P xs
  All¬⇒¬Any []        ()
  All¬⇒¬Any (¬p ∷ _)  (here  p) = ¬p p
  All¬⇒¬Any (_  ∷ ¬p) (there p) = All¬⇒¬Any ¬p p

  ¬All⇒Any¬ : Decidable P → ∀ xs → ¬ All P xs → Any (¬_ ∘ P) xs
  ¬All⇒Any¬ dec []       ¬∀ = ⊥-elim (¬∀ [])
  ¬All⇒Any¬ dec (x ∷ xs) ¬∀ with dec x
  ... | yes p = there (¬All⇒Any¬ dec xs (¬∀ ∘ _∷_ p))
  ... | no ¬p = here ¬p

  Any¬→¬All : ∀ {xs} → Any (¬_ ∘ P) xs → ¬ All P xs
  Any¬→¬All (here  ¬p) = ¬p           ∘ All.head
  Any¬→¬All (there ¬p) = Any¬→¬All ¬p ∘ All.tail

  ¬Any↠All¬ : ∀ {xs} → (¬ Any P xs) ↠ All (¬_ ∘ P) xs
  ¬Any↠All¬ = surjection (¬Any⇒All¬ _) All¬⇒¬Any to∘from
    where
    to∘from : ∀ {xs} (¬p : All (¬_ ∘ P) xs) → ¬Any⇒All¬ xs (All¬⇒¬Any ¬p) ≡ ¬p
    to∘from []         = P.refl
    to∘from (¬p ∷ ¬ps) = P.cong₂ _∷_ P.refl (to∘from ¬ps)

    -- If equality of functions were extensional, then the surjection
    -- could be strengthened to a bijection.

    from∘to : Extensionality _ _ →
              ∀ xs → (¬p : ¬ Any P xs) → All¬⇒¬Any (¬Any⇒All¬ xs ¬p) ≡ ¬p
    from∘to ext []       ¬p = ext λ ()
    from∘to ext (x ∷ xs) ¬p = ext λ
      { (here p)  → P.refl
      ; (there p) → P.cong (λ f → f p) $ from∘to ext xs (¬p ∘ there)
      }

  Any¬⇔¬All : ∀ {xs} → Decidable P → Any (¬_ ∘ P) xs ⇔ (¬ All P xs)
  Any¬⇔¬All dec = equivalence Any¬→¬All (¬All⇒Any¬ dec _)
    where
    -- If equality of functions were extensional, then the logical
    -- equivalence could be strengthened to a surjection.
    to∘from : Extensionality _ _ →
              ∀ {xs} (¬∀ : ¬ All P xs) → Any¬→¬All (¬All⇒Any¬ dec xs ¬∀) ≡ ¬∀
    to∘from ext ¬∀ = ext (⊥-elim ∘ ¬∀)

------------------------------------------------------------------------
-- Properties of operations over `All`
------------------------------------------------------------------------
-- map

module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} {f : P ⋐ Q} where

  map-cong : ∀ {xs} {g : P ⋐ Q} (ps : All P xs) →
             (∀ {x} → f {x} P.≗ g) → All.map f ps ≡ All.map g ps
  map-cong []        _   = P.refl
  map-cong (px ∷ ps) feq = P.cong₂ _∷_ (feq px) (map-cong ps feq)

  map-id : ∀ {xs} (ps : All P xs) → All.map id ps ≡ ps
  map-id []        = P.refl
  map-id (px ∷ ps) = P.cong (px ∷_)  (map-id ps)

  map-compose : ∀ {r} {R : Pred A r} {xs} {g : Q ⋐ R} (ps : All P xs) →
                All.map g (All.map f ps) ≡ All.map (g ∘ f) ps
  map-compose []        = P.refl
  map-compose (px ∷ ps) = P.cong (_ ∷_) (map-compose ps)

  lookup-map : ∀ {xs x} (ps : All P xs) (i : x ∈ xs) →
               All.lookup (All.map f ps) i ≡ f (All.lookup ps i)
  lookup-map (px ∷ pxs) (here P.refl) = P.refl
  lookup-map (px ∷ pxs) (there i) = lookup-map pxs i

------------------------------------------------------------------------
-- _[_]%=_/updateAt

module _ {a p} {A : Set a} {P : Pred A p} where

  updateAt-updates : ∀ {x xs px} (pxs : All P xs) (i : x ∈ xs)
                     {f : P x → P x} → All.lookup pxs i ≡ px →
                     All.lookup (pxs All.[ i ]%= f) i ≡ f px
  updateAt-updates [] ()
  updateAt-updates (px ∷ pxs) (here P.refl) P.refl = P.refl
  updateAt-updates (px ∷ pxs) (there i) = updateAt-updates pxs i

  updateAt-cong : ∀ {x xs} (pxs : All P xs) (i : x ∈ xs)
                  {f g : P x → P x} →
                  f (All.lookup pxs i) ≡ g (All.lookup pxs i) →
                  (pxs All.[ i ]%= f) ≡ (pxs All.[ i ]%= g)
  updateAt-cong (px ∷ pxs) (here P.refl)     = P.cong (_∷ pxs)
  updateAt-cong (px ∷ pxs) (there i)     f≗g = P.cong (px ∷_) (updateAt-cong pxs i f≗g)

  updateAt-id : ∀ {x xs} (pxs : All P xs) (i : x ∈ xs) →
                (pxs All.[ i ]%= id) ≡ pxs
  updateAt-id (px ∷ pxs) (here P.refl) = P.refl
  updateAt-id (px ∷ pxs) (there i)     = P.cong (px ∷_) (updateAt-id pxs i)

  updateAt-compose : ∀ {x xs} (pxs : All P xs) (i : x ∈ xs) {f g : P x → P x} →
                     (pxs All.[ i ]%= f All.[ i ]%= g) ≡ pxs All.[ i ]%= (g ∘ f)
  updateAt-compose (px ∷ pxs) (here P.refl) = P.refl
  updateAt-compose (px ∷ pxs) (there i)     = P.cong (px ∷_) (updateAt-compose pxs i)

  map-updateAt : ∀ {q x} {Q : Pred A q} {xs} →
                 ∀ {f : P ⋐ Q} {g : P x → P x} {h : Q x → Q x}
                 (pxs : All P xs) (i : x ∈ xs) →
                 f (g (All.lookup pxs i)) ≡ h (f (All.lookup pxs i)) →
                 All.map f (pxs All.[ i ]%= g) ≡ (All.map f pxs) All.[ i ]%= h
  map-updateAt (px ∷ pxs) (here P.refl) = P.cong (_∷ _)
  map-updateAt (px ∷ pxs) (there i) feq = P.cong (_ ∷_) (map-updateAt pxs i feq)

------------------------------------------------------------------------
-- Introduction (⁺) and elimination (⁻) rules for list operations
------------------------------------------------------------------------
-- map

module _ {a b p} {A : Set a} {B : Set b} {P : B → Set p} {f : A → B} where

  map⁺ : ∀ {xs} → All (P ∘ f) xs → All P (map f xs)
  map⁺ []       = []
  map⁺ (p ∷ ps) = p ∷ map⁺ ps

  map⁻ : ∀ {xs} → All P (map f xs) → All (P ∘ f) xs
  map⁻ {xs = []}    []       = []
  map⁻ {xs = _ ∷ _} (p ∷ ps) = p ∷ map⁻ ps

-- A variant of All.map.

module _ {a b p q} {A : Set a} {B : Set b} {f : A → B}
         {P : A → Set p} {Q : B → Set q} where

  gmap : P ⋐ Q ∘ f → All P ⋐ All Q ∘ map f
  gmap g = map⁺ ∘ All.map g

------------------------------------------------------------------------
-- mapMaybe

module _ {a b p} {A : Set a} {B : Set b}
         (P : B → Set p) {f : A → Maybe B} where

  mapMaybe⁺ : ∀ {xs} → All (MAll.All P) (map f xs) → All P (mapMaybe f xs)
  mapMaybe⁺ {[]}     [] = []
  mapMaybe⁺ {x ∷ xs} (px ∷ pxs) with f x
  ... | nothing = mapMaybe⁺ pxs
  ... | just v with px
  ...   | just pv = pv ∷ mapMaybe⁺ pxs

------------------------------------------------------------------------
-- _++_

module _ {a p} {A : Set a} {P : A → Set p} where

  ++⁺ : ∀ {xs ys} → All P xs → All P ys → All P (xs ++ ys)
  ++⁺ []         pys = pys
  ++⁺ (px ∷ pxs) pys = px ∷ ++⁺ pxs pys

  ++⁻ˡ : ∀ xs {ys} → All P (xs ++ ys) → All P xs
  ++⁻ˡ []       p          = []
  ++⁻ˡ (x ∷ xs) (px ∷ pxs) = px ∷ (++⁻ˡ _ pxs)

  ++⁻ʳ : ∀ xs {ys} → All P (xs ++ ys) → All P ys
  ++⁻ʳ []       p          = p
  ++⁻ʳ (x ∷ xs) (px ∷ pxs) = ++⁻ʳ xs pxs

  ++⁻ : ∀ xs {ys} → All P (xs ++ ys) → All P xs × All P ys
  ++⁻ []       p          = [] , p
  ++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map (px ∷_) id (++⁻ _ pxs)

  ++↔ : ∀ {xs ys} → (All P xs × All P ys) ↔ All P (xs ++ ys)
  ++↔ {xs} = inverse (uncurry ++⁺) (++⁻ xs) ++⁻∘++⁺ (++⁺∘++⁻ xs)
    where
    ++⁺∘++⁻ : ∀ xs {ys} (p : All P (xs ++ ys)) →
              uncurry′ ++⁺ (++⁻ xs p) ≡ p
    ++⁺∘++⁻ []       p          = P.refl
    ++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = P.cong (_∷_ px) $ ++⁺∘++⁻ xs pxs

    ++⁻∘++⁺ : ∀ {xs ys} (p : All P xs × All P ys) →
              ++⁻ xs (uncurry ++⁺ p) ≡ p
    ++⁻∘++⁺ ([]       , pys) = P.refl
    ++⁻∘++⁺ (px ∷ pxs , pys) rewrite ++⁻∘++⁺ (pxs , pys) = P.refl

------------------------------------------------------------------------
-- concat

module _ {a p} {A : Set a} {P : A → Set p} where

  concat⁺ : ∀ {xss} → All (All P) xss → All P (concat xss)
  concat⁺ []           = []
  concat⁺ (pxs ∷ pxss) = ++⁺ pxs (concat⁺ pxss)

  concat⁻ : ∀ {xss} → All P (concat xss) → All (All P) xss
  concat⁻ {[]}       []  = []
  concat⁻ {xs ∷ xss} pxs = ++⁻ˡ xs pxs ∷ concat⁻ (++⁻ʳ xs pxs)

------------------------------------------------------------------------
-- take and drop

module _ {a p} {A : Set a} {P : A → Set p} where

  drop⁺ : ∀ {xs} n → All P xs → All P (drop n xs)
  drop⁺ zero    pxs        = pxs
  drop⁺ (suc n) []         = []
  drop⁺ (suc n) (px ∷ pxs) = drop⁺ n pxs

  take⁺ : ∀ {xs} n → All P xs → All P (take n xs)
  take⁺ zero    pxs        = []
  take⁺ (suc n) []         = []
  take⁺ (suc n) (px ∷ pxs) = px ∷ take⁺ n pxs

------------------------------------------------------------------------
-- applyUpTo

module _ {a p} {A : Set a} {P : A → Set p} where

  applyUpTo⁺₁ : ∀ f n → (∀ {i} → i < n → P (f i)) → All P (applyUpTo f n)
  applyUpTo⁺₁ f zero    Pf = []
  applyUpTo⁺₁ f (suc n) Pf = Pf (s≤s z≤n) ∷ applyUpTo⁺₁ (f ∘ suc) n (Pf ∘ s≤s)

  applyUpTo⁺₂ : ∀ f n → (∀ i → P (f i)) → All P (applyUpTo f n)
  applyUpTo⁺₂ f n Pf = applyUpTo⁺₁ f n (λ _ → Pf _)

  applyUpTo⁻ : ∀ f n → All P (applyUpTo f n) → ∀ {i} → i < n → P (f i)
  applyUpTo⁻ f zero    pxs        ()
  applyUpTo⁻ f (suc n) (px ∷ _)   (s≤s z≤n)       = px
  applyUpTo⁻ f (suc n) (_  ∷ pxs) (s≤s (s≤s i<n)) =
    applyUpTo⁻ (f ∘ suc) n pxs (s≤s i<n)

------------------------------------------------------------------------
-- tabulate

module _ {a p} {A : Set a} {P : A → Set p} where

  tabulate⁺ : ∀ {n} {f : Fin n → A} →
              (∀ i → P (f i)) → All P (tabulate f)
  tabulate⁺ {zero}  Pf = []
  tabulate⁺ {suc n} Pf = Pf fzero ∷ tabulate⁺ (Pf ∘ fsuc)

  tabulate⁻ : ∀ {n} {f : Fin n → A} →
              All P (tabulate f) → (∀ i → P (f i))
  tabulate⁻ {zero}  pf       ()
  tabulate⁻ {suc n} (px ∷ _) fzero    = px
  tabulate⁻ {suc n} (_ ∷ pf) (fsuc i) = tabulate⁻ pf i

------------------------------------------------------------------------
-- remove

module _ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} where

  ─⁺ : ∀ {xs} (p : Any P xs) → All Q xs → All Q (xs Any.─ p)
  ─⁺ (here px) (_ ∷ qs) = qs
  ─⁺ (there p) (q ∷ qs) = q ∷ ─⁺ p qs

  ─⁻ : ∀ {xs} (p : Any P xs) → Q (Any.lookup p) → All Q (xs Any.─ p) → All Q xs
  ─⁻ (here px) q qs        = q ∷ qs
  ─⁻ (there p) q (q′ ∷ qs) = q′ ∷ ─⁻ p q qs

------------------------------------------------------------------------
-- filter

module _ {a p} {A : Set a} {P : A → Set p} (P? : Decidable P) where

  all-filter : ∀ xs → All P (filter P? xs)
  all-filter []       = []
  all-filter (x ∷ xs) with P? x
  ... | yes Px = Px ∷ all-filter xs
  ... | no  _  = all-filter xs

  filter⁺ : ∀ {q} {Q : A → Set q} {xs} → All Q xs → All Q (filter P? xs)
  filter⁺ {xs = _}     [] = []
  filter⁺ {xs = x ∷ _} (Qx ∷ Qxs) with P? x
  ... | no  _ = filter⁺ Qxs
  ... | yes _ = Qx ∷ filter⁺ Qxs

------------------------------------------------------------------------
-- zipWith

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

  zipWith⁺ : ∀ {p} (P : C → Set p) (f : A → B → C) {xs ys} →
             Pointwise (λ x y → P (f x y)) xs ys →
             All P (zipWith f xs ys)
  zipWith⁺ P f []              = []
  zipWith⁺ P f (Pfxy ∷ Pfxsys) = Pfxy ∷ zipWith⁺ P f Pfxsys

------------------------------------------------------------------------
-- Operations for constructing lists
------------------------------------------------------------------------
-- singleton

module _ {a p} {A : Set a} {P : A → Set p} where

  singleton⁻ : ∀ {x} → All P [ x ] → P x
  singleton⁻ (px ∷ []) = px

------------------------------------------------------------------------
-- snoc

module _ {a p} {A : Set a} {P : A → Set p} where

  ∷ʳ⁺ : ∀ {xs x} → All P xs → P x → All P (xs ∷ʳ x)
  ∷ʳ⁺ pxs px = ++⁺ pxs (px ∷ [])

  ∷ʳ⁻ : ∀ {xs x} → All P (xs ∷ʳ x) → All P xs × P x
  ∷ʳ⁻ {xs} pxs = Prod.map₂ singleton⁻ $ ++⁻ xs pxs

------------------------------------------------------------------------
-- fromMaybe

  fromMaybe⁺ : ∀ {mx} → MAll.All P mx → All P (fromMaybe mx)
  fromMaybe⁺ (just px) = px ∷ []
  fromMaybe⁺ nothing   = []

  fromMaybe⁻ : ∀ mx → All P (fromMaybe mx) → MAll.All P mx
  fromMaybe⁻ (just x) (px ∷ []) = just px
  fromMaybe⁻ nothing  p         = nothing

------------------------------------------------------------------------
-- replicate

  replicate⁺ : ∀ n {x} → P x → All P (replicate n x)
  replicate⁺ zero    px = []
  replicate⁺ (suc n) px = px ∷ replicate⁺ n px

  replicate⁻ : ∀ {n x} → All P (replicate (suc n) x) → P x
  replicate⁻ (px ∷ _) = px

module _ {a p} {A : Set a} {P : A → Set p} where

------------------------------------------------------------------------
-- inits

  inits⁺ : ∀ {xs} → All P xs → All (All P) (inits xs)
  inits⁺ []         = [] ∷ []
  inits⁺ (px ∷ pxs) = [] ∷ gmap (px ∷_) (inits⁺ pxs)

  inits⁻ : ∀ xs → All (All P) (inits xs) → All P xs
  inits⁻ []               pxs                   = []
  inits⁻ (x ∷ [])         ([] ∷ p[x] ∷ [])      = p[x]
  inits⁻ (x ∷ xs@(_ ∷ _)) ([] ∷ pxs@(p[x] ∷ _)) =
    singleton⁻ p[x] ∷ inits⁻ xs (All.map (drop⁺ 1) (map⁻ pxs))

------------------------------------------------------------------------
-- tails

  tails⁺ : ∀ {xs} → All P xs → All (All P) (tails xs)
  tails⁺ []             = [] ∷ []
  tails⁺ pxxs@(_ ∷ pxs) = pxxs ∷ tails⁺ pxs

  tails⁻ : ∀ xs → All (All P) (tails xs) → All P xs
  tails⁻ []       pxs        = []
  tails⁻ (x ∷ xs) (pxxs ∷ _) = pxxs

------------------------------------------------------------------------
-- all

module _ {a} {A : Set a} (p : A → Bool) where

  all⁺ : ∀ xs → T (all p xs) → All (T ∘ p) xs
  all⁺ []       _     = []
  all⁺ (x ∷ xs) px∷xs with Equivalence.to (T-∧ {p x}) ⟨$⟩ px∷xs
  ... | (px , pxs) = px ∷ all⁺ xs pxs

  all⁻ : ∀ {xs} → All (T ∘ p) xs → T (all p xs)
  all⁻ []         = _
  all⁻ (px ∷ pxs) = Equivalence.from T-∧ ⟨$⟩ (px , all⁻ pxs)

------------------------------------------------------------------------
-- All is anti-monotone.

anti-mono : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} →
            xs ⊆ ys → All P ys → All P xs
anti-mono xs⊆ys pys = All.tabulate (All.lookup pys ∘ xs⊆ys)

all-anti-mono : ∀ {a} {A : Set a} (p : A → Bool) {xs ys} →
                xs ⊆ ys → T (all p ys) → T (all p xs)
all-anti-mono p xs⊆ys = all⁻ p ∘ anti-mono xs⊆ys ∘ all⁺ p _

------------------------------------------------------------------------
-- Interactions with pointwise equality
------------------------------------------------------------------------

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S renaming (Carrier to A)
  open ListEq S

  respects : ∀ {p} {P : Pred A p} → P Respects _≈_ → (All P) Respects _≋_
  respects p≈ []            []         = []
  respects p≈ (x≈y ∷ xs≈ys) (px ∷ pxs) = p≈ x≈y px ∷ respects p≈ xs≈ys pxs

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.16

All-all = all⁻
{-# WARNING_ON_USAGE All-all
"Warning: All-all was deprecated in v0.16.
Please use all⁻ instead."
#-}
all-All = all⁺
{-# WARNING_ON_USAGE all-All
"Warning: all-All was deprecated in v0.16.
Please use all⁺ instead."
#-}
All-map = map⁺
{-# WARNING_ON_USAGE All-map
"Warning: All-map was deprecated in v0.16.
Please use map⁺ instead."
#-}
map-All = map⁻
{-# WARNING_ON_USAGE map-All
"Warning: map-All was deprecated in v0.16.
Please use map⁻ instead."
#-}

-- Version 1.0

filter⁺₁ = all-filter
{-# WARNING_ON_USAGE filter⁺₁
"Warning: filter⁺₁ was deprecated in v1.0.
Please use all-filter instead."
#-}
filter⁺₂ = filter⁺
{-# WARNING_ON_USAGE filter⁺₂
"Warning: filter⁺₂ was deprecated in v1.0.
Please use filter⁺ instead."
#-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Least Common Multiple for integers
------------------------------------------------------------------------

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

module Data.Integer.LCM where

open import Data.Integer.Base
open import Data.Integer.Divisibility
open import Data.Integer.GCD
open import Data.Nat.Base using (ℕ)
import Data.Nat.LCM as ℕ
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Definition
------------------------------------------------------------------------

lcm : ℤ → ℤ → ℤ
lcm i j = + ℕ.lcm ∣ i ∣ ∣ j ∣

------------------------------------------------------------------------
-- Properties
------------------------------------------------------------------------

i∣lcm[i,j] : ∀ i j → i ∣ lcm i j
i∣lcm[i,j] i j = ℕ.m∣lcm[m,n] ∣ i ∣ ∣ j ∣

j∣lcm[i,j] : ∀ i j → j ∣ lcm i j
j∣lcm[i,j] i j = ℕ.n∣lcm[m,n] ∣ i ∣ ∣ j ∣

lcm-least : ∀ {i j c} → i ∣ c → j ∣ c → lcm i j ∣ c
lcm-least c∣i c∣j = ℕ.lcm-least c∣i c∣j

lcm[0,i]≡0 : ∀ i → lcm 0ℤ i ≡ 0ℤ
lcm[0,i]≡0 i = cong (+_) (ℕ.lcm[0,n]≡0 ∣ i ∣)

lcm[i,0]≡0 : ∀ i → lcm i 0ℤ ≡ 0ℤ
lcm[i,0]≡0 i = cong (+_) (ℕ.lcm[n,0]≡0 ∣ i ∣)

lcm-comm : ∀ i j → lcm i j ≡ lcm j i
lcm-comm i j = cong (+_) (ℕ.lcm-comm ∣ i ∣ ∣ j ∣)


text:
module SortedBinaryTree where
  infix 4 _≡_
  data _≡_ {a} {A : Set a} (x : A) : A → Set a where
    refl : x ≡ x
  {-# BUILTIN EQUALITY _≡_  #-}
  {-# BUILTIN REFL     refl #-}

  open import Sec4
  postulate A : Set -- XXX: E.g., Nat or Bool some base type

  -- XXX: Postulates for ≤
  postulate _≤_ : A → A → Prop
  postulate antisym-≤ : (a b : A) → (a ≤ b) → (b ≤ a) → (a ≡ b)
  postulate tot-≤ : (a b : A) → (a ≤ b) ∨ (b ≤ a)
  postulate refl-≤ : (a : A) → (a ≤ a)
  postulate trans-≤ : (a b c : A) → (a ≤ b) → (b ≤ a) → (a ≤ c)

  -- XXX: Postulates for ≥
  postulate _≥_ : A → A → Prop
  postulate antisym-≥ : (a b : A) → (a ≥ b) → (b ≥ a) → (a ≡ b)
  postulate tot-≥ : (a b : A) → (a ≥ b) ∨ (b ≥ a)
  postulate refl-≥ : (a : A) → (a ≥ a)
  postulate trans-≥ : (a b c : A) → (a ≥ b) → (b ≥ a) → (a ≥ c)

-- XXX: Definition of a binary tree.
  data SortedBinaryTree (A : Set) : Set where
    Leaf : SortedBinaryTree A
    Node : (a : A) → (l : SortedBinaryTree A) → (r : SortedBinaryTree A) → SortedBinaryTree A

  all-leq : (a : A) → (t : SortedBinaryTree A) → Prop
  all-leq a₁ Leaf = ⊤
  all-leq a₁ (Node a₂ l r) = (a₂ ≤ a₁) ∧ ((all-leq a₁ l) ∧ (all-leq a₁ r))

  all-geq : (a : A) → (t : SortedBinaryTree A) → Prop
  all-geq a₁ Leaf = ⊤
  all-geq a₁ (Node a₂ l r) = (a₂ ≥ a₁) ∧ ((all-geq a₁ l) ∧ (all-geq a₁ r))

-- XXX: What is a sorted tree. A BTree is sorted, if all elements in the
-- left substree are ≥ root and all elements in the right subtree are ≤
-- root.
  ordered : SortedBinaryTree A → Prop
  ordered Leaf = ⊤
  ordered (Node a l r) = ((all-leq a l) ∧ (all-geq a r)) ∧ ((ordered l) ∧ (ordered r))

-- XXX: Insert function for SortedBinaryTree
  insert : (a : A) → SortedBinaryTree A → SortedBinaryTree A
  insert x Leaf = Node x Leaf Leaf
  insert x (Node a t t₁) with (tot-≤ x a)
  insert x (Node a t t₁) | ora x₁ = insert x t
  insert x (Node a t t₁) | orb x₁ = insert x t₁

-- XXX: Prove that the tree obtained after insertion is sorted
  insert-sorted : (a : A)
                  → (t : SortedBinaryTree A)
                  → (p : ordered t)
                  → ordered (insert a t)
  insert-sorted a Leaf _ = and (and ⋆ ⋆) (and ⋆ ⋆)
  insert-sorted a (Node a₁ t t₁) (and (and x x1) (and x2 x3)) with (tot-≤ a a₁)
  insert-sorted a (Node a₁ t t₁) (and (and p1 p2) (and p3 p4)) | ora w = insert-sorted a t p3
  insert-sorted a (Node a₁ t t₁) (and (and p1 p2) (and p3 p4)) | orb w = insert-sorted a t₁ p4

-- XXX: Proof carrying code
  insert' : (a : A)
            → (t : SortedBinaryTree A)
            → (p : ordered t)
            → Exists (SortedBinaryTree A) (λ t' → ordered t')
  insert' a t p = [ insert a t , insert-sorted a t p ]

-- XXX: Write Proof that delete works.

-- XXX: Write a version with record and setoid carrying the ≤, etc


text:
module Pi where

open import Agda.Builtin.Equality
  using (_≡_; refl)

f
  : {A : Set}
  → {x y : A}
  → (z w : A)
  → x ≡ z
  → z ≡ x
f _ _ refl
  = refl

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused