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

module 05-identity-types where

import 04-inductive-types
open 04-inductive-types public

-- Section 5.1

-- Definition 5.1.1

{- We introduce the identity type. -}

data Id {i : Level} {A : UU i} (x : A) : A → UU i where
  refl : Id x x

{- In the following definition we give a construction of path induction.
   However, in the development of this library we will mostly use Agda's
   built-in methods to give constructions by path induction. -}

ind-Id :
  {i j : Level} {A : UU i} (x : A) (B : (y : A) (p : Id x y) → UU j) →
  (B x refl) → (y : A) (p : Id x y) → B y p
ind-Id x B b y refl = b

-- Section 5.2 The groupoid structure of types

-- Definition 5.2.1

_∙_ :
  {i : Level} {A : UU i} {x y z : A} → Id x y → Id y z → Id x z
refl ∙ q = q

concat :
  {i : Level} {A : UU i} {x y : A} → Id x y → (z : A) → Id y z → Id x z
concat p z q = p ∙ q

-- Definition 5.2.2

inv :
  {i : Level} {A : UU i} {x y : A} → Id x y → Id y x
inv refl = refl

-- Definition 5.2.3

assoc :
  {i : Level} {A : UU i} {x y z w : A} (p : Id x y) (q : Id y z)
  (r : Id z w) → Id ((p ∙ q) ∙ r) (p ∙ (q ∙ r))
assoc refl q r = refl

-- Definition 5.2.4

left-unit :
  {i : Level} {A : UU i} {x y : A} {p : Id x y} → Id (refl ∙ p) p
left-unit = refl

right-unit :
  {i : Level} {A : UU i} {x y : A} {p : Id x y} → Id (p ∙ refl) p
right-unit {p = refl} = refl

-- Definition 5.2.5

left-inv :
  {i : Level} {A : UU i} {x y : A} (p : Id x y) →
  Id ((inv p) ∙ p) refl
left-inv refl = refl

right-inv :
  {i : Level} {A : UU i} {x y : A} (p : Id x y) →
  Id (p ∙ (inv p)) refl
right-inv refl = refl

-- Section 5.3 The action on paths of functions

-- Definition 5.3.1

ap :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) {x y : A} (p : Id x y) →
  Id (f x) (f y)
ap f refl = refl

ap-id :
  {i : Level} {A : UU i} {x y : A} (p : Id x y) → Id (ap id p) p
ap-id refl = refl

ap-comp :
  {i j k : Level} {A : UU i} {B : UU j} {C : UU k} (g : B → C)
  (f : A → B) {x y : A} (p : Id x y) → Id (ap (g ∘ f) p) (ap g (ap f p))
ap-comp g f refl = refl

-- Definition 5.3.2

ap-refl :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) (x : A) →
  Id (ap f (refl {_} {_} {x})) refl
ap-refl f x = refl

ap-concat :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) {x y z : A}
  (p : Id x y) (q : Id y z) → Id (ap f (p ∙ q)) ((ap f p) ∙ (ap f q))
ap-concat f refl q = refl

ap-inv :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) {x y : A}
  (p : Id x y) → Id (ap f (inv p)) (inv (ap f p))
ap-inv f refl = refl

-- Section 5.4 Transport

-- Definition 5.4.1

tr :
  {i j : Level} {A : UU i} (B : A → UU j) {x y : A} (p : Id x y) → B x → B y
tr B refl b = b

-- Definition 5.4.2

apd :
  {i j : Level} {A : UU i} {B : A → UU j} (f : (x : A) → B x) {x y : A}
  (p : Id x y) → Id (tr B p (f x)) (f y)
apd f refl = refl

path-over :
  {i j : Level} {A :  UU i} (B : A → UU j) {x x' : A} (p : Id x x') →
  B x → B x' → UU j
path-over B p y y' = Id (tr B p y) y'

refl-path-over :
  {i j : Level} {A : UU i} (B : A → UU j) (x : A) (y : B x) →
  path-over B refl y y
refl-path-over B x y = refl

-- Exercises

-- Exercise 5.1

-- Exercise 5.2

distributive-inv-concat :
  {i : Level} {A : UU i} {x y : A} (p : Id x y) {z : A}
  (q : Id y z) → Id (inv (p ∙ q)) ((inv q) ∙ (inv p))
distributive-inv-concat refl refl = refl

-- Exercise 5.3

inv-con :
  {i : Level} {A : UU i} {x y : A} (p : Id x y) {z : A} (q : Id y z)
  (r : Id x z) → (Id (p ∙ q) r) → Id q ((inv p) ∙ r)
inv-con refl q r = id

con-inv :
  {i : Level} {A : UU i} {x y : A} (p : Id x y) {z : A} (q : Id y z)
  (r : Id x z) → (Id (p ∙ q) r) → Id p (r ∙ (inv q))
con-inv p refl r =
  ( λ α → α ∙ (inv right-unit)) ∘ (concat (inv right-unit) r)

-- Exercise 5.4

lift :
  {i j : Level} {A : UU i} {B : A → UU j} {x y : A} (p : Id x y)
  (b : B x) → Id (pair x b) (pair y (tr B p b))
lift refl b = refl

-- Exercise 5.5

-- Exercise 5.5(a)

abstract
  right-unit-law-add-ℕ :
    (x : ℕ) → Id (add-ℕ x zero-ℕ) x
  right-unit-law-add-ℕ x = refl

  left-unit-law-add-ℕ :
    (x : ℕ) → Id (add-ℕ zero-ℕ x) x
  left-unit-law-add-ℕ zero-ℕ = refl
  left-unit-law-add-ℕ (succ-ℕ x) = ap succ-ℕ (left-unit-law-add-ℕ x)

  left-successor-law-add-ℕ :
    (x y : ℕ) → Id (add-ℕ (succ-ℕ x) y) (succ-ℕ (add-ℕ x y))
  left-successor-law-add-ℕ x zero-ℕ = refl
  left-successor-law-add-ℕ x (succ-ℕ y) =
    ap succ-ℕ (left-successor-law-add-ℕ x y)

  right-successor-law-add-ℕ :
    (x y : ℕ) → Id (add-ℕ x (succ-ℕ y)) (succ-ℕ (add-ℕ x y))
  right-successor-law-add-ℕ x y = refl

-- Exercise 5.5(b)

abstract
  associative-add-ℕ :
    (x y z : ℕ) → Id (add-ℕ (add-ℕ x y) z) (add-ℕ x (add-ℕ y z))
  associative-add-ℕ x y zero-ℕ = refl
  associative-add-ℕ x y (succ-ℕ z) = ap succ-ℕ (associative-add-ℕ x y z)

abstract
  commutative-add-ℕ : (x y : ℕ) → Id (add-ℕ x y) (add-ℕ y x)
  commutative-add-ℕ zero-ℕ y = left-unit-law-add-ℕ y
  commutative-add-ℕ (succ-ℕ x) y =
    (left-successor-law-add-ℕ x y) ∙ (ap succ-ℕ (commutative-add-ℕ x y))

-- Exercise 5.5(c)

abstract
  left-zero-law-mul-ℕ :
    (x : ℕ) → Id (mul-ℕ zero-ℕ x) zero-ℕ
  left-zero-law-mul-ℕ x = refl

  right-zero-law-mul-ℕ :
    (x : ℕ) → Id (mul-ℕ x zero-ℕ) zero-ℕ
  right-zero-law-mul-ℕ zero-ℕ = refl
  right-zero-law-mul-ℕ (succ-ℕ x) =
    ( right-unit-law-add-ℕ (mul-ℕ x zero-ℕ)) ∙ (right-zero-law-mul-ℕ x)

abstract
  right-unit-law-mul-ℕ :
    (x : ℕ) → Id (mul-ℕ x one-ℕ) x
  right-unit-law-mul-ℕ zero-ℕ = refl
  right-unit-law-mul-ℕ (succ-ℕ x) = ap succ-ℕ (right-unit-law-mul-ℕ x)

  left-unit-law-mul-ℕ :
    (x : ℕ) → Id (mul-ℕ one-ℕ x) x
  left-unit-law-mul-ℕ zero-ℕ = refl
  left-unit-law-mul-ℕ (succ-ℕ x) = ap succ-ℕ (left-unit-law-mul-ℕ x)

abstract
  left-successor-law-mul-ℕ :
    (x y : ℕ) → Id (mul-ℕ (succ-ℕ x) y) (add-ℕ (mul-ℕ x y) y)
  left-successor-law-mul-ℕ x y = refl

  right-successor-law-mul-ℕ :
    (x y : ℕ) → Id (mul-ℕ x (succ-ℕ y)) (add-ℕ x (mul-ℕ x y))
  right-successor-law-mul-ℕ zero-ℕ y = refl
  right-successor-law-mul-ℕ (succ-ℕ x) y =
    ( ( ap (λ t → succ-ℕ (add-ℕ t y)) (right-successor-law-mul-ℕ x y)) ∙
      ( ap succ-ℕ (associative-add-ℕ x (mul-ℕ x y) y))) ∙
    ( inv (left-successor-law-add-ℕ x (add-ℕ (mul-ℕ x y) y)))

-- Exercise 5.5(d)

abstract
  commutative-mul-ℕ :
    (x y : ℕ) → Id (mul-ℕ x y) (mul-ℕ y x)
  commutative-mul-ℕ zero-ℕ y = inv (right-zero-law-mul-ℕ y)
  commutative-mul-ℕ (succ-ℕ x) y =
    ( commutative-add-ℕ (mul-ℕ x y) y) ∙
    ( ( ap (add-ℕ y) (commutative-mul-ℕ x y)) ∙
      ( inv (right-successor-law-mul-ℕ y x)))

-- Exercise 5.5(e)

abstract
  left-distributive-mul-add-ℕ :
    (x y z : ℕ) → Id (mul-ℕ x (add-ℕ y z)) (add-ℕ (mul-ℕ x y) (mul-ℕ x z))
  left-distributive-mul-add-ℕ zero-ℕ y z = refl
  left-distributive-mul-add-ℕ (succ-ℕ x) y z =
    ( left-successor-law-mul-ℕ x (add-ℕ y z)) ∙
    ( ( ap (λ t → add-ℕ t (add-ℕ y z)) (left-distributive-mul-add-ℕ x y z)) ∙
      ( ( associative-add-ℕ (mul-ℕ x y) (mul-ℕ x z) (add-ℕ y z)) ∙
        ( ( ap ( add-ℕ (mul-ℕ x y))
               ( ( inv (associative-add-ℕ (mul-ℕ x z) y z)) ∙
                 ( ( ap (λ t → add-ℕ t z) (commutative-add-ℕ (mul-ℕ x z) y)) ∙
                   ( associative-add-ℕ y (mul-ℕ x z) z)))) ∙
          ( inv (associative-add-ℕ (mul-ℕ x y) y (add-ℕ (mul-ℕ x z) z))))))

abstract
  right-distributive-mul-add-ℕ :
    (x y z : ℕ) → Id (mul-ℕ (add-ℕ x y) z) (add-ℕ (mul-ℕ x z) (mul-ℕ y z))
  right-distributive-mul-add-ℕ x y z =
    ( commutative-mul-ℕ (add-ℕ x y) z) ∙
    ( ( left-distributive-mul-add-ℕ z x y) ∙
      ( ( ap (λ t → add-ℕ t (mul-ℕ z y)) (commutative-mul-ℕ z x)) ∙
        ( ap (λ t → add-ℕ (mul-ℕ x z) t) (commutative-mul-ℕ z y))))

-- Exercise 5.5(f)

abstract
  associative-mul-ℕ :
    (x y z : ℕ) → Id (mul-ℕ (mul-ℕ x y) z) (mul-ℕ x (mul-ℕ y z))
  associative-mul-ℕ zero-ℕ y z = refl
  associative-mul-ℕ (succ-ℕ x) y z =
    ( right-distributive-mul-add-ℕ (mul-ℕ x y) y z) ∙
    ( ap (λ t → add-ℕ t (mul-ℕ y z)) (associative-mul-ℕ x y z))

-- Exercise 5.6

Mac-Lane-pentagon :
  {i : Level} {A : UU i} {a b c d e : A}
  (p : Id a b) (q : Id b c) (r : Id c d) (s : Id d e) →
  let α₁ = (ap (λ t → t ∙ s) (assoc p q r))
      α₂ = (assoc p (q ∙ r) s)
      α₃ = (ap (λ t → p ∙ t) (assoc q r s))
      α₄ = (assoc (p ∙ q) r s)
      α₅ = (assoc p q (r ∙ s))
  in
  Id ((α₁ ∙ α₂) ∙ α₃) (α₄ ∙ α₅)
Mac-Lane-pentagon refl refl refl refl = refl

{- The following code is an experiment that shows that constructions in an
   abstract environment do remember the specific definitions of previous
   definitions in abstract environments. -}

abstract
  abstract-concat :
    {l : Level} {A : UU l} {x y z : A} → Id x y → Id y z → Id x z
  abstract-concat refl q = q

  abstract-left-unit-law :
    {l : Level} {A : UU l} {x y : A} (q : Id x y) → Id (abstract-concat refl q) q
  abstract-left-unit-law q = refl

{- We just make some random definition to make sure that we are not in the
   same abstract envirnoment anymore. -}
one : ℕ
one = succ-ℕ zero-ℕ

abstract
  abstract-right-unit-law :
    {l : Level} {A : UU l} {x y : A} (p : Id x y) →
      Id (abstract-concat p refl) p
  abstract-right-unit-law refl = refl

  {- The term refl should not be accepted if the definition of abstract-concat
     were forgotten. A definition that would work under all circumstances is
     abstract-left-unit refl. -}

-- The ring axioms for ℤ

abstract
  left-inverse-pred-ℤ :
    (k : ℤ) → Id (pred-ℤ (succ-ℤ k)) k
  left-inverse-pred-ℤ (inl zero-ℕ) = refl
  left-inverse-pred-ℤ (inl (succ-ℕ x)) = refl
  left-inverse-pred-ℤ (inr (inl star)) = refl
  left-inverse-pred-ℤ (inr (inr zero-ℕ)) = refl
  left-inverse-pred-ℤ (inr (inr (succ-ℕ x))) = refl

  right-inverse-pred-ℤ :
    (k : ℤ) → Id (succ-ℤ (pred-ℤ k)) k
  right-inverse-pred-ℤ (inl zero-ℕ) = refl
  right-inverse-pred-ℤ (inl (succ-ℕ x)) = refl
  right-inverse-pred-ℤ (inr (inl star)) = refl
  right-inverse-pred-ℤ (inr (inr zero-ℕ)) = refl
  right-inverse-pred-ℤ (inr (inr (succ-ℕ x))) = refl

{- Exercise 6.12 (a) simply asks to prove the unit laws. The left unit law
   holds by judgmental equality. -}

abstract
  left-unit-law-add-ℤ :
    (k : ℤ) → Id (add-ℤ zero-ℤ k) k
  left-unit-law-add-ℤ k = refl

  right-unit-law-add-ℤ :
    (k : ℤ) → Id (add-ℤ k zero-ℤ) k
  right-unit-law-add-ℤ (inl zero-ℕ) = refl
  right-unit-law-add-ℤ (inl (succ-ℕ x)) =
    ap pred-ℤ (right-unit-law-add-ℤ (inl x))
  right-unit-law-add-ℤ (inr (inl star)) = refl
  right-unit-law-add-ℤ (inr (inr zero-ℕ)) = refl
  right-unit-law-add-ℤ (inr (inr (succ-ℕ x))) =
    ap succ-ℤ (right-unit-law-add-ℤ (inr (inr x)))

{- Exercise 6.12 (b) asks to show the left and right predecessor and successor
   laws. These are helpful to give proofs of associativity and commutativity.
   -}

abstract
  left-predecessor-law-add-ℤ :
    (x y : ℤ) → Id (add-ℤ (pred-ℤ x) y) (pred-ℤ (add-ℤ x y))
  left-predecessor-law-add-ℤ (inl n) y = refl
  left-predecessor-law-add-ℤ (inr (inl star)) y = refl
  left-predecessor-law-add-ℤ (inr (inr zero-ℕ)) y =
    ( ap (λ t → add-ℤ t y) (left-inverse-pred-ℤ zero-ℤ)) ∙
    ( inv (left-inverse-pred-ℤ y))
  left-predecessor-law-add-ℤ (inr (inr (succ-ℕ x))) y =
    ( ap (λ t → (add-ℤ t y)) (left-inverse-pred-ℤ (inr (inr x)))) ∙
    ( inv (left-inverse-pred-ℤ (add-ℤ (inr (inr x)) y)))

  right-predecessor-law-add-ℤ :
    (x y : ℤ) → Id (add-ℤ x (pred-ℤ y)) (pred-ℤ (add-ℤ x y))
  right-predecessor-law-add-ℤ (inl zero-ℕ) n = refl
  right-predecessor-law-add-ℤ (inl (succ-ℕ m)) n =
    ap pred-ℤ (right-predecessor-law-add-ℤ (inl m) n)
  right-predecessor-law-add-ℤ (inr (inl star)) n = refl
  right-predecessor-law-add-ℤ (inr (inr zero-ℕ)) n =
    (right-inverse-pred-ℤ n) ∙ (inv (left-inverse-pred-ℤ n))
  right-predecessor-law-add-ℤ (inr (inr (succ-ℕ x))) n =
    ( ap succ-ℤ (right-predecessor-law-add-ℤ (inr (inr x)) n)) ∙
    ( ( right-inverse-pred-ℤ (add-ℤ (inr (inr x)) n)) ∙
      ( inv (left-inverse-pred-ℤ (add-ℤ (inr (inr x)) n))))

abstract
  left-successor-law-add-ℤ :
    (x y : ℤ) → Id (add-ℤ (succ-ℤ x) y) (succ-ℤ (add-ℤ x y))
  left-successor-law-add-ℤ (inl zero-ℕ) y =
    ( ap (λ t → add-ℤ t y) (right-inverse-pred-ℤ zero-ℤ)) ∙
    ( inv (right-inverse-pred-ℤ y))
  left-successor-law-add-ℤ (inl (succ-ℕ x)) y =
    ( inv (right-inverse-pred-ℤ (add-ℤ (inl x) y))) ∙
    ( ap succ-ℤ (inv (left-predecessor-law-add-ℤ (inl x) y)))
  left-successor-law-add-ℤ (inr (inl star)) y = refl
  left-successor-law-add-ℤ (inr (inr x)) y = refl

  right-successor-law-add-ℤ :
    (x y : ℤ) → Id (add-ℤ x (succ-ℤ y)) (succ-ℤ (add-ℤ x y))
  right-successor-law-add-ℤ (inl zero-ℕ) y =
    (left-inverse-pred-ℤ y) ∙ (inv (right-inverse-pred-ℤ y))
  right-successor-law-add-ℤ (inl (succ-ℕ x)) y =
    ( ap pred-ℤ (right-successor-law-add-ℤ (inl x) y)) ∙
    ( ( left-inverse-pred-ℤ (add-ℤ (inl x) y)) ∙
      ( inv (right-inverse-pred-ℤ (add-ℤ (inl x) y))))
  right-successor-law-add-ℤ (inr (inl star)) y = refl
  right-successor-law-add-ℤ (inr (inr zero-ℕ)) y = refl
  right-successor-law-add-ℤ (inr (inr (succ-ℕ x))) y =
    ap succ-ℤ (right-successor-law-add-ℤ (inr (inr x)) y)

{- Exercise 6.12 (c) asks to prove associativity and commutativity. Note that
   we avoid an unwieldy amount of cases by only using induction on the first
   argument. The resulting proof term is fairly short, and we don't have to
   present ℤ as a certain quotient of ℕ × ℕ. -}

abstract
  associative-add-ℤ :
    (x y z : ℤ) → Id (add-ℤ (add-ℤ x y) z) (add-ℤ x (add-ℤ y z))
  associative-add-ℤ (inl zero-ℕ) y z =
    ( ap (λ t → add-ℤ t z) (left-predecessor-law-add-ℤ zero-ℤ y)) ∙
    ( ( left-predecessor-law-add-ℤ y z) ∙
      ( inv (left-predecessor-law-add-ℤ zero-ℤ (add-ℤ y z))))
  associative-add-ℤ (inl (succ-ℕ x)) y z =
    ( ap (λ t → add-ℤ t z) (left-predecessor-law-add-ℤ (inl x) y)) ∙
    ( ( left-predecessor-law-add-ℤ (add-ℤ (inl x) y) z) ∙
      ( ( ap pred-ℤ (associative-add-ℤ (inl x) y z)) ∙
        ( inv (left-predecessor-law-add-ℤ (inl x) (add-ℤ y z)))))
  associative-add-ℤ (inr (inl star)) y z = refl
  associative-add-ℤ (inr (inr zero-ℕ)) y z =
    ( ap (λ t → add-ℤ t z) (left-successor-law-add-ℤ zero-ℤ y)) ∙
    ( ( left-successor-law-add-ℤ y z) ∙
      ( inv (left-successor-law-add-ℤ zero-ℤ (add-ℤ y z))))
  associative-add-ℤ (inr (inr (succ-ℕ x))) y z =
    ( ap (λ t → add-ℤ t z) (left-successor-law-add-ℤ (inr (inr x)) y)) ∙
    ( ( left-successor-law-add-ℤ (add-ℤ (inr (inr x)) y) z) ∙
      ( ( ap succ-ℤ (associative-add-ℤ (inr (inr x)) y z)) ∙
        ( inv (left-successor-law-add-ℤ (inr (inr x)) (add-ℤ y z)))))

abstract
  commutative-add-ℤ :
    (x y : ℤ) → Id (add-ℤ x y) (add-ℤ y x)
  commutative-add-ℤ (inl zero-ℕ) y =
    ( left-predecessor-law-add-ℤ zero-ℤ y) ∙
    ( inv
      ( ( right-predecessor-law-add-ℤ y zero-ℤ) ∙
        ( ap pred-ℤ (right-unit-law-add-ℤ y))))
  commutative-add-ℤ (inl (succ-ℕ x)) y =
    ( ap pred-ℤ (commutative-add-ℤ (inl x) y)) ∙
    ( inv (right-predecessor-law-add-ℤ y (inl x)))
  commutative-add-ℤ (inr (inl star)) y = inv (right-unit-law-add-ℤ y)
  commutative-add-ℤ (inr (inr zero-ℕ)) y =
    inv
      ( ( right-successor-law-add-ℤ y zero-ℤ) ∙
        ( ap succ-ℤ (right-unit-law-add-ℤ y)))
  commutative-add-ℤ (inr (inr (succ-ℕ x))) y =
    ( ap succ-ℤ (commutative-add-ℤ (inr (inr x)) y)) ∙
    ( inv (right-successor-law-add-ℤ y (inr (inr x))))

{- Exercise 6.12 (d) finally asks to show the inverse laws, completing the
   verification of the group laws. Combined with associativity and
   commutativity we conclude that (add-ℤ x) and (λ x → add-ℤ x y) are
   equivalences, for every x : ℤ and y : ℤ, respectively. -}

abstract
  left-inverse-law-add-ℤ :
    (x : ℤ) → Id (add-ℤ (neg-ℤ x) x) zero-ℤ
  left-inverse-law-add-ℤ (inl zero-ℕ) = refl
  left-inverse-law-add-ℤ (inl (succ-ℕ x)) =
    ( ap succ-ℤ (right-predecessor-law-add-ℤ (inr (inr x)) (inl x))) ∙
    ( ( right-inverse-pred-ℤ (add-ℤ (inr (inr x)) (inl x))) ∙
      ( left-inverse-law-add-ℤ (inl x)))
  left-inverse-law-add-ℤ (inr (inl star)) = refl
  left-inverse-law-add-ℤ (inr (inr x)) =
    ( commutative-add-ℤ (inl x) (inr (inr x))) ∙
    ( left-inverse-law-add-ℤ (inl x))

  right-inverse-law-add-ℤ :
    (x : ℤ) → Id (add-ℤ x (neg-ℤ x)) zero-ℤ
  right-inverse-law-add-ℤ x =
    ( commutative-add-ℤ x (neg-ℤ x)) ∙ (left-inverse-law-add-ℤ x)

-- Similar for multiplication on ℤ

neg-neg-ℤ : (k : ℤ) → Id (neg-ℤ (neg-ℤ k)) k
neg-neg-ℤ (inl n) = refl
neg-neg-ℤ (inr (inl star)) = refl
neg-neg-ℤ (inr (inr n)) = refl

neg-pred-ℤ :
  (k : ℤ) → Id (neg-ℤ (pred-ℤ k)) (succ-ℤ (neg-ℤ k))
neg-pred-ℤ (inl x) = refl
neg-pred-ℤ (inr (inl star)) = refl
neg-pred-ℤ (inr (inr zero-ℕ)) = refl
neg-pred-ℤ (inr (inr (succ-ℕ x))) = refl

pred-neg-ℤ :
  (k : ℤ) → Id (pred-ℤ (neg-ℤ k)) (neg-ℤ (succ-ℤ k))
pred-neg-ℤ (inl zero-ℕ) = refl
pred-neg-ℤ (inl (succ-ℕ x)) = refl
pred-neg-ℤ (inr (inl star)) = refl
pred-neg-ℤ (inr (inr x)) = refl

right-negative-law-add-ℤ :
  (k l : ℤ) → Id (add-ℤ k (neg-ℤ l)) (neg-ℤ (add-ℤ (neg-ℤ k) l))
right-negative-law-add-ℤ (inl zero-ℕ) l =
  ( left-predecessor-law-add-ℤ zero-ℤ (neg-ℤ l)) ∙
  ( pred-neg-ℤ l)
right-negative-law-add-ℤ (inl (succ-ℕ x)) l =
  ( left-predecessor-law-add-ℤ (inl x) (neg-ℤ l)) ∙
  ( ( ap pred-ℤ (right-negative-law-add-ℤ (inl x) l)) ∙
    ( pred-neg-ℤ (add-ℤ (inr (inr x)) l)))
right-negative-law-add-ℤ (inr (inl star)) l = refl
right-negative-law-add-ℤ (inr (inr zero-ℕ)) l = inv (neg-pred-ℤ l)
right-negative-law-add-ℤ (inr (inr (succ-ℕ n))) l =
  ( left-successor-law-add-ℤ (in-pos n) (neg-ℤ l)) ∙
  ( ( ap succ-ℤ (right-negative-law-add-ℤ (inr (inr n)) l)) ∙
    ( inv (neg-pred-ℤ (add-ℤ (inl n) l))))

distributive-neg-add-ℤ :
  (k l : ℤ) → Id (neg-ℤ (add-ℤ k l)) (add-ℤ (neg-ℤ k) (neg-ℤ l))
distributive-neg-add-ℤ (inl zero-ℕ) l =
  ( ap neg-ℤ (left-predecessor-law-add-ℤ zero-ℤ l)) ∙
  ( neg-pred-ℤ l)
distributive-neg-add-ℤ (inl (succ-ℕ n)) l =
  ( neg-pred-ℤ (add-ℤ (inl n) l)) ∙
  ( ( ap succ-ℤ (distributive-neg-add-ℤ (inl n) l)) ∙
    ( ap (λ t → add-ℤ t (neg-ℤ l)) (inv (neg-pred-ℤ (inl n)))))
distributive-neg-add-ℤ (inr (inl star)) l = refl
distributive-neg-add-ℤ (inr (inr zero-ℕ)) l = inv (pred-neg-ℤ l)
distributive-neg-add-ℤ (inr (inr (succ-ℕ n))) l =
  ( inv (pred-neg-ℤ (add-ℤ (in-pos n) l))) ∙
  ( ap pred-ℤ (distributive-neg-add-ℤ (inr (inr n)) l))

left-zero-law-mul-ℤ : (k : ℤ) → Id (mul-ℤ zero-ℤ k) zero-ℤ
left-zero-law-mul-ℤ k = refl

right-zero-law-mul-ℤ : (k : ℤ) → Id (mul-ℤ k zero-ℤ) zero-ℤ
right-zero-law-mul-ℤ (inl zero-ℕ) = refl
right-zero-law-mul-ℤ (inl (succ-ℕ n)) =
  right-zero-law-mul-ℤ (inl n)
right-zero-law-mul-ℤ (inr (inl star)) = refl
right-zero-law-mul-ℤ (inr (inr zero-ℕ)) = refl
right-zero-law-mul-ℤ (inr (inr (succ-ℕ n))) =
  right-zero-law-mul-ℤ (inr (inr n))

left-unit-law-mul-ℤ : (k : ℤ) → Id (mul-ℤ one-ℤ k) k
left-unit-law-mul-ℤ k = refl

right-unit-law-mul-ℤ : (k : ℤ) → Id (mul-ℤ k one-ℤ) k
right-unit-law-mul-ℤ (inl zero-ℕ) = refl
right-unit-law-mul-ℤ (inl (succ-ℕ n)) =
  ap (add-ℤ (neg-one-ℤ)) (right-unit-law-mul-ℤ (inl n))
right-unit-law-mul-ℤ (inr (inl star)) = refl
right-unit-law-mul-ℤ (inr (inr zero-ℕ)) = refl
right-unit-law-mul-ℤ (inr (inr (succ-ℕ n))) =
  ap (add-ℤ one-ℤ) (right-unit-law-mul-ℤ (inr (inr n)))

left-neg-unit-law-mul-ℤ : (k : ℤ) → Id (mul-ℤ neg-one-ℤ k) (neg-ℤ k)
left-neg-unit-law-mul-ℤ k = refl

right-neg-unit-law-mul-ℤ : (k : ℤ) → Id (mul-ℤ k neg-one-ℤ) (neg-ℤ k)
right-neg-unit-law-mul-ℤ (inl zero-ℕ) = refl
right-neg-unit-law-mul-ℤ (inl (succ-ℕ n)) =
  ap (add-ℤ one-ℤ) (right-neg-unit-law-mul-ℤ (inl n))
right-neg-unit-law-mul-ℤ (inr (inl star)) = refl
right-neg-unit-law-mul-ℤ (inr (inr zero-ℕ)) = refl
right-neg-unit-law-mul-ℤ (inr (inr (succ-ℕ n))) =
  ap (add-ℤ neg-one-ℤ) (right-neg-unit-law-mul-ℤ (inr (inr n)))

left-successor-law-mul-ℤ :
  (k l : ℤ) → Id (mul-ℤ (succ-ℤ k) l) (add-ℤ l (mul-ℤ k l))
left-successor-law-mul-ℤ (inl zero-ℕ) l =
  inv (right-inverse-law-add-ℤ l)
left-successor-law-mul-ℤ (inl (succ-ℕ n)) l =
  ( ( inv (left-unit-law-add-ℤ (mul-ℤ (inl n) l))) ∙
    ( ap
      ( λ x → add-ℤ x (mul-ℤ (inl n) l))
      ( inv (right-inverse-law-add-ℤ l)))) ∙
  ( associative-add-ℤ l (neg-ℤ l) (mul-ℤ (inl n) l))
left-successor-law-mul-ℤ (inr (inl star)) l =
  inv (right-unit-law-add-ℤ l)
left-successor-law-mul-ℤ (inr (inr n)) l = refl

left-predecessor-law-mul-ℤ :
  (k l : ℤ) → Id (mul-ℤ (pred-ℤ k) l) (add-ℤ (neg-ℤ l) (mul-ℤ k l))
left-predecessor-law-mul-ℤ (inl n) l = refl
left-predecessor-law-mul-ℤ (inr (inl star)) l =
  ( left-neg-unit-law-mul-ℤ l) ∙
  ( inv (right-unit-law-add-ℤ (neg-ℤ l)))
left-predecessor-law-mul-ℤ (inr (inr zero-ℕ)) l =
  inv (left-inverse-law-add-ℤ l)
left-predecessor-law-mul-ℤ (inr (inr (succ-ℕ x))) l =
   ( ap
     ( λ t → add-ℤ t (mul-ℤ (in-pos x) l))
     ( inv (left-inverse-law-add-ℤ l))) ∙
   ( associative-add-ℤ (neg-ℤ l) l (mul-ℤ (in-pos x) l))

right-successor-law-mul-ℤ :
  (k l : ℤ) → Id (mul-ℤ k (succ-ℤ l)) (add-ℤ k (mul-ℤ k l))
right-successor-law-mul-ℤ (inl zero-ℕ) l = inv (pred-neg-ℤ l)
right-successor-law-mul-ℤ (inl (succ-ℕ n)) l =
  ( left-predecessor-law-mul-ℤ (inl n) (succ-ℤ l)) ∙
  ( ( ap (add-ℤ (neg-ℤ (succ-ℤ l))) (right-successor-law-mul-ℤ (inl n) l)) ∙
    ( ( inv (associative-add-ℤ (neg-ℤ (succ-ℤ l)) (inl n) (mul-ℤ (inl n) l))) ∙
      ( ( ap
          ( λ t → add-ℤ t (mul-ℤ (inl n) l))
          { x = add-ℤ (neg-ℤ (succ-ℤ l)) (inl n)}
          { y = add-ℤ (inl (succ-ℕ n)) (neg-ℤ l)}
          ( ( right-successor-law-add-ℤ (neg-ℤ (succ-ℤ l)) (inl (succ-ℕ n))) ∙
            ( ( ap succ-ℤ
                ( commutative-add-ℤ (neg-ℤ (succ-ℤ l)) (inl (succ-ℕ n)))) ∙
              ( ( inv
                  ( right-successor-law-add-ℤ
                    ( inl (succ-ℕ n))
                    ( neg-ℤ (succ-ℤ l)))) ∙
                ( ap
                  ( add-ℤ (inl (succ-ℕ n)))
                  ( ( ap succ-ℤ (inv (pred-neg-ℤ l))) ∙
                    ( right-inverse-pred-ℤ (neg-ℤ l)))))))) ∙
        ( associative-add-ℤ (inl (succ-ℕ n)) (neg-ℤ l) (mul-ℤ (inl n) l)))))
right-successor-law-mul-ℤ (inr (inl star)) l = refl
right-successor-law-mul-ℤ (inr (inr zero-ℕ)) l = refl
right-successor-law-mul-ℤ (inr (inr (succ-ℕ n))) l =
  ( left-successor-law-mul-ℤ (in-pos n) (succ-ℤ l)) ∙
  ( ( ap (add-ℤ (succ-ℤ l)) (right-successor-law-mul-ℤ (inr (inr n)) l)) ∙
    ( ( inv (associative-add-ℤ (succ-ℤ l) (in-pos n) (mul-ℤ (in-pos n) l))) ∙
      ( ( ap
          ( λ t → add-ℤ t (mul-ℤ (in-pos n) l))
          { x = add-ℤ (succ-ℤ l) (in-pos n)}
          { y = add-ℤ (in-pos (succ-ℕ n)) l}
          ( ( left-successor-law-add-ℤ l (in-pos n)) ∙
            ( ( ap succ-ℤ (commutative-add-ℤ l (in-pos n))) ∙
              ( inv (left-successor-law-add-ℤ (in-pos n) l))))) ∙
        ( associative-add-ℤ (inr (inr (succ-ℕ n))) l (mul-ℤ (inr (inr n)) l)))))

right-predecessor-law-mul-ℤ :
  (k l : ℤ) → Id (mul-ℤ k (pred-ℤ l)) (add-ℤ (neg-ℤ k) (mul-ℤ k l))
right-predecessor-law-mul-ℤ (inl zero-ℕ) l =
  ( left-neg-unit-law-mul-ℤ (pred-ℤ l)) ∙
  ( neg-pred-ℤ l)
right-predecessor-law-mul-ℤ (inl (succ-ℕ n)) l =
  ( left-predecessor-law-mul-ℤ (inl n) (pred-ℤ l)) ∙
  ( ( ap (add-ℤ (neg-ℤ (pred-ℤ l))) (right-predecessor-law-mul-ℤ (inl n) l)) ∙
    ( ( inv
        ( associative-add-ℤ (neg-ℤ (pred-ℤ l)) (in-pos n) (mul-ℤ (inl n) l))) ∙
      ( ( ap
          ( λ t → add-ℤ t (mul-ℤ (inl n) l))
          { x = add-ℤ (neg-ℤ (pred-ℤ l)) (inr (inr n))}
          { y = add-ℤ (neg-ℤ (inl (succ-ℕ n))) (neg-ℤ l)}
          ( ( ap (λ t → add-ℤ t (in-pos n)) (neg-pred-ℤ l)) ∙
            ( ( left-successor-law-add-ℤ (neg-ℤ l) (in-pos n)) ∙
              ( ( ap succ-ℤ (commutative-add-ℤ (neg-ℤ l) (in-pos n))) ∙
                ( inv (left-successor-law-add-ℤ (in-pos n) (neg-ℤ l))))))) ∙
        ( associative-add-ℤ (in-pos (succ-ℕ n)) (neg-ℤ l) (mul-ℤ (inl n) l)))))
right-predecessor-law-mul-ℤ (inr (inl star)) l = refl
right-predecessor-law-mul-ℤ (inr (inr zero-ℕ)) l = refl
right-predecessor-law-mul-ℤ (inr (inr (succ-ℕ n))) l =
  ( left-successor-law-mul-ℤ (in-pos n) (pred-ℤ l)) ∙
  ( ( ap (add-ℤ (pred-ℤ l)) (right-predecessor-law-mul-ℤ (inr (inr n)) l)) ∙
    ( ( inv (associative-add-ℤ (pred-ℤ l) (inl n) (mul-ℤ (inr (inr n)) l))) ∙
      ( ( ap
          ( λ t → add-ℤ t (mul-ℤ (in-pos n) l))
          { x = add-ℤ (pred-ℤ l) (inl n)}
          { y = add-ℤ (neg-ℤ (in-pos (succ-ℕ n))) l}
          ( ( left-predecessor-law-add-ℤ l (inl n)) ∙
            ( ( ap pred-ℤ (commutative-add-ℤ l (inl n))) ∙
              ( inv (left-predecessor-law-add-ℤ (inl n) l))))) ∙
        ( associative-add-ℤ (inl (succ-ℕ n)) l (mul-ℤ (inr (inr n)) l)))))

right-distributive-mul-add-ℤ :
  (k l m : ℤ) → Id (mul-ℤ (add-ℤ k l) m) (add-ℤ (mul-ℤ k m) (mul-ℤ l m))
right-distributive-mul-add-ℤ (inl zero-ℕ) l m =
  ( left-predecessor-law-mul-ℤ l m) ∙
  ( ap
    ( λ t → add-ℤ t (mul-ℤ l m))
    ( inv
      ( ( left-predecessor-law-mul-ℤ zero-ℤ m) ∙
        ( right-unit-law-add-ℤ (neg-ℤ m)))))
right-distributive-mul-add-ℤ (inl (succ-ℕ x)) l m =
  ( left-predecessor-law-mul-ℤ (add-ℤ (inl x) l) m) ∙
  ( ( ap (add-ℤ (neg-ℤ m)) (right-distributive-mul-add-ℤ (inl x) l m)) ∙
    ( inv (associative-add-ℤ (neg-ℤ m) (mul-ℤ (inl x) m) (mul-ℤ l m))))
right-distributive-mul-add-ℤ (inr (inl star)) l m = refl
right-distributive-mul-add-ℤ (inr (inr zero-ℕ)) l m =
  left-successor-law-mul-ℤ l m
right-distributive-mul-add-ℤ (inr (inr (succ-ℕ n))) l m =
  ( left-successor-law-mul-ℤ (add-ℤ (in-pos n) l) m) ∙
  ( ( ap (add-ℤ m) (right-distributive-mul-add-ℤ (inr (inr n)) l m)) ∙
    ( inv (associative-add-ℤ m (mul-ℤ (in-pos n) m) (mul-ℤ l m))))

left-negative-law-mul-ℤ :
  (k l : ℤ) → Id (mul-ℤ (neg-ℤ k) l) (neg-ℤ (mul-ℤ k l))
left-negative-law-mul-ℤ (inl zero-ℕ) l =
  ( left-unit-law-mul-ℤ l) ∙
  ( inv (neg-neg-ℤ l))
left-negative-law-mul-ℤ (inl (succ-ℕ n)) l =
  ( ap (λ t → mul-ℤ t l) (neg-pred-ℤ (inl n))) ∙
  ( ( left-successor-law-mul-ℤ (neg-ℤ (inl n)) l) ∙
    ( ( ap (add-ℤ l) (left-negative-law-mul-ℤ (inl n) l)) ∙
      ( right-negative-law-add-ℤ l (mul-ℤ (inl n) l))))
left-negative-law-mul-ℤ (inr (inl star)) l = refl
left-negative-law-mul-ℤ (inr (inr zero-ℕ)) l = refl
left-negative-law-mul-ℤ (inr (inr (succ-ℕ n))) l =
  ( left-predecessor-law-mul-ℤ (inl n) l) ∙
  ( ( ap (add-ℤ (neg-ℤ l)) (left-negative-law-mul-ℤ (inr (inr n)) l)) ∙
    ( inv (distributive-neg-add-ℤ l (mul-ℤ (in-pos n) l))))

associative-mul-ℤ :
  (k l m : ℤ) → Id (mul-ℤ (mul-ℤ k l) m) (mul-ℤ k (mul-ℤ l m))
associative-mul-ℤ (inl zero-ℕ) l m =
  left-negative-law-mul-ℤ l m
associative-mul-ℤ (inl (succ-ℕ n)) l m =
  ( right-distributive-mul-add-ℤ (neg-ℤ l) (mul-ℤ (inl n) l) m) ∙
  ( ( ap (add-ℤ (mul-ℤ (neg-ℤ l) m)) (associative-mul-ℤ (inl n) l m)) ∙
    ( ap
      ( λ t → add-ℤ t (mul-ℤ (inl n) (mul-ℤ l m)))
      ( left-negative-law-mul-ℤ l m)))
associative-mul-ℤ (inr (inl star)) l m = refl
associative-mul-ℤ (inr (inr zero-ℕ)) l m = refl
associative-mul-ℤ (inr (inr (succ-ℕ n))) l m =
  ( right-distributive-mul-add-ℤ l (mul-ℤ (in-pos n) l) m) ∙
  ( ap (add-ℤ (mul-ℤ l m)) (associative-mul-ℤ (inr (inr n)) l m))

commutative-mul-ℤ :
  (k l : ℤ) → Id (mul-ℤ k l) (mul-ℤ l k)
commutative-mul-ℤ (inl zero-ℕ) l = inv (right-neg-unit-law-mul-ℤ l)
commutative-mul-ℤ (inl (succ-ℕ n)) l =
  ( ap (add-ℤ (neg-ℤ l)) (commutative-mul-ℤ (inl n) l)) ∙
  ( inv (right-predecessor-law-mul-ℤ l (inl n)))
commutative-mul-ℤ (inr (inl star)) l = inv (right-zero-law-mul-ℤ l)
commutative-mul-ℤ (inr (inr zero-ℕ)) l = inv (right-unit-law-mul-ℤ l)
commutative-mul-ℤ (inr (inr (succ-ℕ n))) l =
  ( ap (add-ℤ l) (commutative-mul-ℤ (inr (inr n)) l)) ∙
  ( inv (right-successor-law-mul-ℤ l (in-pos n)))

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
-- There was a bug when postponing a type checking problem under
-- a non-empty context. Fixed now.
module PostponedTypeChecking where

data Unit : Set where
  unit : Unit

record R : Set where
 field f : Unit

data *_ (A : Set) : Set where
  <_> : A -> * A

get : {A : Set} -> * A -> A
get < x > = x

mk : Unit -> Unit -> * R
mk _ _ = < record { f = unit } >

r : R
r = get (mk unit unit)

data IsUnit : Unit -> Set where
  isUnit : IsUnit unit

foo : IsUnit (R.f r)
foo = isUnit

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
-- Lifting the dependent axiom of choice to sums and products

open import Type
open import Function.NP
open import Function.Extensionality
open import Data.Nat
open import Data.Product
open import Data.Fin using (Fin)
open import Explore.Core
open import Explore.Properties
open import Relation.Binary.PropositionalEquality.NP
open import Type.Identities
open import HoTT
open ≡-Reasoning
open Adequacy _≡_

module Explore.BigDistr
                {A B          : ★₀}
                {Πᴬ           : Product A}
                (adequate-Πᴬ  : Adequate-product Πᴬ)
                {Σᴮ           : Sum B}
                (adequate-Σᴮ  : Adequate-sum Σᴮ)
                {Σᴬᴮ          : Sum (A → B)}
                (adequate-Σᴬᴮ : Adequate-sum Σᴬᴮ)
                (F            : A → B → ℕ)
                {{_           : UA}}
                {{_           : FunExt}}
                where

big-distr : Πᴬ (Σᴮ ∘ F) ≡ Σᴬᴮ λ f → Πᴬ (F ˢ f)
big-distr =
  Fin-injective
  ( Fin (Πᴬ (Σᴮ ∘ F))
  ≡⟨ adequate-Πᴬ (Σᴮ ∘ F) ⟩
    Π A (Fin ∘ Σᴮ ∘ F)
  ≡⟨ Π=′ A (adequate-Σᴮ ∘ F) ⟩
    Π A (λ x → Σ B (Fin ∘ F x))
  ≡⟨ ΠΣ-comm ⟩
    Σ (Π A (const B)) (λ f → Π A (λ x → Fin (F x (f x))))
  ≡⟨ Σ=′ (A → B) (λ f → ! (adequate-Πᴬ (F ˢ f))) ⟩
    Σ (A → B) (λ f → Fin (Πᴬ (F ˢ f)))
  ≡⟨ ! (adequate-Σᴬᴮ (λ f → Πᴬ (F ˢ f))) ⟩
    Fin (Σᴬᴮ (λ f → Πᴬ (F ˢ f)))
  ∎)

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module FFI.Data.ByteString where

{-# FOREIGN GHC import qualified Data.ByteString #-}

postulate ByteString : Set
{-# COMPILE GHC ByteString = type Data.ByteString.ByteString #-}

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
module BadRefl where

open import AgdaPrelude

plus =
  natElim
    ( \ _ -> Nat -> Nat )           -- motive
    ( \ n -> n )                    -- case for Zero
    ( \ p rec n -> Succ (rec n) )   -- case for Succ

-- the other direction requires induction on N:
postulate pNPlus0isN : (n : Nat) -> Eq Nat (plus n Zero) n

-- the other direction requires induction on N:
succPlus : (n : Nat) -> Eq Nat  (Succ n) (plus (Succ n) Zero)
succPlus =
  (\n -> pNPlus0isN (Succ n))

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
data ⊥ : Set where -- keep this on the first line!!

Type = Set  -- This should not be gobbled up under the data declaration

-- Andreas, 2021-04-15, issue #1145
-- Allow stacking of layout keywords on the same line.

-- This files contains tests for the new layout rules
-- and also tests from debugging the original implementation.
--
-- Some original failures where influenced by whether
-- there were comments or black lines, so please don't
-- "clean up" this file.

postulate A : Set; B : Set
          C : Set

-- First example

private postulate  -- Bar
  D : Set
  _>>_ : Set → Set → Set

module _ where
  private {- this block comment
             removes the line breaks
             between the layout keywords -} postulate
    D1 : Set
    E1 : Set

-- Second example

private module PM where              -- stack
  module PMM where
  private module PMPM1 where
          module PMPM2 where private -- stack
            module PMPM2M where
  module PMM2 where

-- Testing whether do-notation still works

test = do A; B
          C

let-example =
   let X = A
       in  B

do-example = do
  Set
  where
    Y : Set
    Y = A

F = Set

private
  doey = do
    Set
    where postulate poey : Set

E = Set

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --copatterns #-}

module examplesPaperJFP.ExampleDrawingProgram where

open import Size
open import Data.Bool.Base
open import Data.Char.Base
open import Data.Nat.Base hiding (_⊓_; _+_; _*_)
open import Data.List.Base hiding (_++_)
open import Data.Integer.Base hiding (suc)
open import Data.String.Base
open import Data.Maybe.Base
open import Agda.Builtin.Char using (primCharEquality)

open import Function

open import SizedIO.Base
open import SizedIO.IOGraphicsLib hiding (translateIOGraphics)  renaming (translateIOGraphicsLocal to translateNative)

open import NativeInt --PrimTypeHelpers
open import NativeIO

open import examplesPaperJFP.triangleRightOperator

integerLess     :  ℤ →  ℤ → Bool
integerLess x y with ∣(y - (x ⊓ y))∣
... | zero = true
... | z = false

line : Point → Point → Graphic
line p  newpoint = withColor red (polygon
                       (nativePoint x y
                        ∷ nativePoint a b
                        ∷ nativePoint (a + xAddition) (b + yAddition)
                        ∷ nativePoint (x + xAddition) (y + yAddition)
                        ∷ [] ) )
  where
  x = nativeProj1Point p
  y = nativeProj2Point p
  a = nativeProj1Point newpoint
  b = nativeProj2Point newpoint

  diffx = + ∣ (a - x) ∣
  diffy = + ∣ (b - y) ∣

  diffx*3 = diffx * (+ 3)
  diffy*3 = diffy * (+ 3)

  condition = (integerLess diffx diffy*3) ∧ (integerLess diffy diffx*3)

  xAddition = if condition then + 2 else + 1
  yAddition = if condition then + 2 else + 1

State = Maybe Point

mutual

  loop              :  ∀{i} → Window → State → IOGraphics i Unit
  force (loop w s)  =  exec'  (getWindowEvent w) λ e →
                       winEvtHandler w s e

  winEvtHandler : ∀{i} → Window → State → Event → IOGraphics i Unit
  winEvtHandler w s (Key c t)       =  if primCharEquality c 'x'
                                       then (exec (closeWindow w) return)
                                       else loop w s
  winEvtHandler w s (MouseMove p₂)  =  s ▹ λ
                                         { nothing    →  loop w (just p₂)
                                         ; (just p₁)  →  exec (drawInWindow w (line p₁ p₂)) λ _ →
                                                         loop w (just p₂)   }
  winEvtHandler w s _               =  loop w s

program : ∀{i} → IOGraphics i Unit
program =
  exec  (openWindow "Drawing Prog" nothing 1000 1000
      nativeDrawGraphic nothing) λ win →
  loop win nothing

translateIOGraphics : IOGraphics ∞ Unit → NativeIO Unit
translateIOGraphics = translateIO translateNative

main : NativeIO Unit
main = nativeRunGraphics (translateIOGraphics program)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
-- Andreas, 2015-08-18 Test case for COMPILED_DATA on record

-- open import Common.String
open import Common.IO

infixr 4 _,_
infixr 2 _×_

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

open _×_ public

{-# COMPILED_DATA _×_ (,) (,) #-}

-- Note: could not get this to work for Σ.
-- Also, the universe-polymorphic version of _×_ would require more trickery.

swap : ∀{A B : Set} (p : A × B) → B × A
swap (x , y) = y , x

swap' : ∀{A B : Set} (p : A × B) → B × A
swap' p = proj₂ p , proj₁ p

main = putStrLn (proj₁ (swap (swap' (swap ("no" , "yes")))))


text:
module TooManyFields where

postulate X : Set

record D : Set where
  field x : X

d : X -> D
d x = record {x = x; y = x}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
module FRP.JS.Level where

infixl 6 _⊔_

postulate
  Level : Set
  zero  : Level
  suc   : Level → Level
  _⊔_   : Level → Level → Level

{-# COMPILED_JS zero 0 #-}
{-# COMPILED_JS suc  function(x) { return x + 1; } #-}
{-# COMPILED_JS _⊔_  function(x) { return function(y) { return Math.max(x,y); }; } #-}

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module CoPatWith where

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A -> Maybe A

data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

record CoList (A : Set) : Set where
  constructor inn
  field
    out : Maybe (A × CoList A)

open CoList

module With where

  map : {A B : Set}(f : A -> B)(l : CoList A) -> CoList B
  out (map f l) with out l
  out (map f l) | nothing = nothing
  out (map f l) | just (a , as) = just (f a , map f as)

module NoWith where

  map : {A B : Set}(f : A -> B)(l : CoList A) -> CoList B
  out (map {A = A}{B = B} f l) = map' f l (out l)
    where outmap : (f : A -> B)(l : CoList A)(outl : Maybe (A × CoList A)) -> Maybe (B × CoList B)
          outmap f l nothing = nothing
          outmap f l (just (a , as)) = just (f a , map f as)

module With2 where

  map : {A B : Set}(f : A -> B)(l : CoList A) -> CoList B
  out (map f (inn l)) with l
  out (map f (inn .nothing))         | nothing       = nothing
  out (map f (inn .(just (a , as)))) | just (a , as) = just (f a , map f as)

module NoWith2 where

  map : {A B : Set}(f : A -> B)(l : CoList A) -> CoList B
  out (map {A = A}{B = B} f l) = map' f l (out l)
    where outmap : (f : A -> B)(l : CoList A)(outl : Maybe (A × CoList A)) -> Maybe (B × CoList B)
          outmap f (inn .nothing)         nothing         = nothing
          outmap f (inn .(just (a , as))) (just (a , as)) = just (f a , map f as)

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection

infix -100 This:_ this:_
data This:_ {a} {A : Set a} : A → Set where
  this:_ : ∀ x → This: x

macro
  runT : Tactic → Tactic
  runT m = m

  evalT : ∀ {a} {A : Set a} → TC A → Tactic
  evalT m hole = m >>= quoteTC >>= unify hole

-- The context on the rhs of each of the two functions below is the same, a single String

Γ = vArg (def (quote String) []) ∷ []

context-Γ₀ : String → This: Γ
context-Γ₀ s = this: evalT getContext

module _ (S : String) where
  context-Γ₁ : This: Γ
  context-Γ₁ = this: evalT getContext

replicate : {A : Set} → Nat → A → List A
replicate zero x = []
replicate (suc n) x = x ∷ replicate n x

f-type : Term
f-type = def (quote String) []

f-pats : Nat → List (Arg Pattern)
f-pats n = replicate n (vArg (var "_"))

f-term : Nat → Term
f-term n = var n []

defineFresh : Nat → Nat → TC QName
defineFresh #pats #term =
  freshName "f" >>= λ f →
  define (vArg f) (funDef f-type (clause (f-pats #pats) (f-term #term) ∷ [])) >>= λ _ →
  returnTC f

freshFun : Nat → Nat → TC Bool
freshFun #pats #term =
  catchTC (defineFresh #pats #term >>= λ _ → returnTC true)
          (returnTC false)

-- Check that the pattern list must be of length 0
-- and the context features 1 available variable.

define-Γ₀-0-0 : String → This: true
define-Γ₀-0-0 s = this: evalT (freshFun 0 0)

define-Γ₀-1-0 : String → This: false
define-Γ₀-1-0 s = this: evalT (freshFun 1 0)

define-Γ₀-1-1 : String → This: false
define-Γ₀-1-1 s = this: evalT (freshFun 0 1)

module _ (S : String) where
  define-Γ₁-0-0 : This: true
  define-Γ₁-0-0 = this: evalT (freshFun 0 0)

  define-Γ₁-0-1 : This: false
  define-Γ₁-0-1 = this: evalT (freshFun 0 1)

  define-Γ₁-1-0 : This: false
  define-Γ₁-1-0 = this: evalT (freshFun 1 0)

f₀ : String → String
f₀ s = runT λ hole → defineFresh 0 0 >>= λ f → unify hole (def f [])

f₁ : String → String
f₁ = λ s → runT λ hole → defineFresh 0 0 >>= λ f → unify hole (def f [])

f₂ : String → String
f₂ s = runT λ hole → defineFresh 0 0 >>= λ f → unify hole (def f [])
  where x = 0


text:
open import Prelude

open import Level using (_⊔_; Lift; lift) renaming (suc to ls; zero to lz)
open import Data.String using (String)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Nat using (_≤_)

open import RW.Data.RTrie.Decl

module RW.Data.RTrie.Lookup
    where

  postulate
    trie-err : ∀{a}{A : Set a} → String → A

  open import RW.Utils.Monads
  open Monad {{...}}
  open Eq {{...}}

  import RW.Data.PMap (RTermᵢ ⊥) as IdxMap
  import RW.Data.PMap ℕ as ℕmap

  -------------------------------
  -- Some type boilerplate

  Label : Set
  Label = ℕ ⊎ Name

  Lst : Set
  Lst = ℕmap.to (RTerm ⊥) × Maybe Label

  Lst-empty : Lst
  Lst-empty = ℕmap.empty , nothing

  Lst-open : Lst → (ℕmap.to (RTerm ⊥) × Maybe Name)
  Lst-open (e , l) = (e , lbl-join l)
    where
      lbl-join : Maybe Label → Maybe Name
      lbl-join nothing = nothing
      lbl-join (just (i1 _)) = nothing
      lbl-join (just (i2 a)) = just a

  ---------------------------
  -- Lookup monad

  L : Set → Set
  L = Reader (List Lst)

  ----------------------------
  -- Rule application

  -- Note how a mismatch erases labels!
  applyBRule1 : Rule → Lst → Lst
  applyBRule1 (Gr x)   (e , _) = e , just (i1 x)
  applyBRule1 (Tr x y) (e , just (i1 l))
    with x ≟-ℕ l
  ...| yes _ = e , just (i1 y)
  ...| no  _ = e , nothing
  applyBRule1 (Tr x y) (e , just (i2 _)) = e , nothing
  applyBRule1 (Fr x y) (e , just (i1 l))
    with x ≟-ℕ l
  ...| yes _ = e , just (i2 y)
  ...| no  _ = e , nothing
  applyBRule1 (Fr _ _) (e , just (i2 _)) = e , nothing
  applyBRule1 _        (e , nothing) = e , nothing

  applyBRule : Rule → L (List Lst)
  applyBRule r = reader-ask >>= return ∘ (Prelude.map (applyBRule1 r))

  ruleList : List Rule → L (List Lst)
  ruleList rs = mapM applyBRule rs >>= return ∘ concat
    where
      isNothing : ∀{a}{A : Set a} → Maybe A → Bool
      isNothing nothing = true
      isNothing _       = false

      prune : List Lst → List Lst
      prune = Prelude.filter (isNothing ∘ p2)

  ------------------------------
  -- Actual Lookup

  map-filter : ∀{a}{A B : Set a} → (B → Bool) → (A → B) → List A → List B
  map-filter p f = foldr (λ h r → let x = f h in ite (p x) (x ∷ r) r) []
    where
      ite : ∀{a}{A : Set a} → Bool → A → A → A
      ite true  t _ = t
      ite false _ e = e

  mutual
    -- TODO: refine this, only apply the rules after validating and adding bindings.
    lkup-inst1 : RTerm ⊥ → ℕ × List Rule → L (List Lst)
    lkup-inst1 k (s , r)
      = ruleList r
      >>= return ∘ map-filter (isValid s k) (addUnbound s k)
      where
        addUnbound : ℕ → RTerm ⊥ → Lst → Lst
        addUnbound s k (e , l) = (ℕmap.alter (maybe just (just k)) s e , l)

        toBool : ∀{a}{A : Set a} → Dec A → Bool
        toBool (yes _) = true
        toBool (no  _) = false

        isValid : ℕ → RTerm ⊥ → Lst → Bool
        isValid s k (e , l) = toBool (ℕmap.lkup s e ≟2 just k)
          where
            _≟2_ : (a₁ a₂ : Maybe (RTerm ⊥)) → Dec (a₁ ≡ a₂)
            _≟2_ a b = Eq.cmp eq-Maybe a b

    -- Looks up a term given a list of instantiations.
    -- This is not, by far, a lookup function. We're just adding all possibilities together.
    lkup-inst : RTerm ⊥ → List (ℕ × List Rule) → L (List Lst)
    lkup-inst t [] = return []
    lkup-inst t rs = mapM (lkup-inst1 t) rs >>= return ∘ concat

    -- Looks a list of RTerms in their respecive cells.
    {-# TERMINATING #-}
    lkup-list : List (RTerm ⊥ × Cell)
              → L (List Lst)
    lkup-list [] = return []
    lkup-list ((t , (d , mh) , bs) ∷ ts)
      = lkup-aux t (Fork (((d , mh) , bs) ∷ []))
      >>= λ s₁ → (reader-local (_++_ s₁) $ lkup-list ts)
      >>= return ∘ (_++_ s₁)

    lkup-aux : RTerm ⊥ → RTrie → L (List Lst)
    lkup-aux _ (Leaf r) = ruleList r
    lkup-aux k (Fork (((d , rs) , bs) ∷ []))
      = let tid , tr = out k
      in lkup-inst k bs
      -- If tid ∉ mh, we run the lookup again, but in the default branch.
      -- Otherwise, we run a lkup-list.
      >>= λ r → maybe (lkup≡just tr) (lkup-aux k d) (IdxMap.lkup tid rs)
      >>= return ∘ (_++_ r)
      where
        lkup≡just : List (RTerm ⊥) → RTrie → L (List Lst)
        lkup≡just [] (Leaf r) = ruleList r
        lkup≡just _  (Leaf _) = return []
        lkup≡just tr (Fork ms) = lkup-list (zip tr ms)

    lkup-aux _ _ = trie-err "lkup-aux takes 1-cell forks"

  -- Interfacing
  lookup : RTerm ⊥ → RTrie → List (ℕmap.to (RTerm ⊥) × Name)
  lookup t bt = accept (Prelude.map Lst-open (lkup-aux t bt (Lst-empty ∷ [])))
    where
      accept : ∀{a}{A : Set a} → List (A × Maybe Name) → List (A × Name)
      accept [] = []
      accept ((a , just b) ∷ hs) = (a , b) ∷ accept hs
      accept (_ ∷ hs)            = accept hs

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
module _ where

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

postulate
  A : Set
  f : .A → A
  g : A → A

mutual
  X : Bool → .A → A
  X = _

  Y : .A → A → A
  Y = _ -- should be solved!

  foo : .(x : A) {y : A} → X true x ≡ g (Y x y)
  foo _ = refl
  -- this prunes both x and y from Y,
  -- so later Y cannot be solved to \ .x y → f x

  bar : .(x : A){y : A} → f x ≡ Y x y
  bar _ = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
------------------------------------------------------------------------
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Props.Ring (r : Ring) where

open Ring r
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Data.Function
open import Data.Product

-‿*-distribˡ : ∀ x y → - x * y ≈ - (x * y)
-‿*-distribˡ x y = begin
  - x * y                        ≈⟨ sym $ proj₂ +-identity _ ⟩
  - x * y + 0#                   ≈⟨ refl ⟨ +-pres-≈ ⟩ sym (proj₂ -‿inverse _) ⟩
  - x * y + (x * y + - (x * y))  ≈⟨ sym $ +-assoc _ _ _  ⟩
  - x * y + x * y + - (x * y)    ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-pres-≈ ⟩ refl ⟩
  (- x + x) * y + - (x * y)      ≈⟨ (proj₁ -‿inverse _ ⟨ *-pres-≈ ⟩ refl)
                                      ⟨ +-pres-≈ ⟩
                                    refl ⟩
  0# * y + - (x * y)             ≈⟨ proj₁ zero _ ⟨ +-pres-≈ ⟩ refl ⟩
  0# + - (x * y)                 ≈⟨ proj₁ +-identity _ ⟩
  - (x * y)                      ∎

-‿*-distribʳ : ∀ x y → x * - y ≈ - (x * y)
-‿*-distribʳ x y = begin
  x * - y                        ≈⟨ sym $ proj₁ +-identity _ ⟩
  0# + x * - y                   ≈⟨ sym (proj₁ -‿inverse _) ⟨ +-pres-≈ ⟩ refl ⟩
  - (x * y) + x * y + x * - y    ≈⟨ +-assoc _ _ _  ⟩
  - (x * y) + (x * y + x * - y)  ≈⟨ refl ⟨ +-pres-≈ ⟩ sym (proj₁ distrib _ _ _)  ⟩
  - (x * y) + x * (y + - y)      ≈⟨ refl ⟨ +-pres-≈ ⟩ (refl ⟨ *-pres-≈ ⟩ proj₂ -‿inverse _) ⟩
  - (x * y) + x * 0#             ≈⟨ refl ⟨ +-pres-≈ ⟩ proj₂ zero _ ⟩
  - (x * y) + 0#                 ≈⟨ proj₂ +-identity _ ⟩
  - (x * y)                      ∎

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module Container.Foldable where

open import Prelude

record Foldable {a b w} (F : Set a → Set b) : Set (lsuc w ⊔ lsuc a ⊔ b) where
  field
    foldMap : ∀ {A}{W : Set w} {{MonW : Monoid W}} → (A → W) → F A → W
    overlap {{super}} : Functor F

open Foldable {{...}} public

fold : ∀ {a w} {W : Set w} {F : Set w → Set a} {{FoldF : Foldable F}} {{MonW : Monoid W}} → F W → W
fold = foldMap id

minimum : ∀ {a w} {W : Set w} {F : Set w → Set a} {{FoldF : Foldable F}} {{OrdW : Ord W}} → F W → Maybe W
minimum = foldMap {{MonW = monoid}} just
  where
    monoid : Monoid _
    Monoid.mempty monoid = nothing
    Monoid._<>_ monoid (just x) (just y) = just (min x y)
    Monoid._<>_ monoid (just x) nothing = just x
    Monoid._<>_ monoid nothing (just y) = just y
    Monoid._<>_ monoid nothing nothing = nothing

maximum : ∀ {a w} {W : Set w} {F : Set w → Set a} {{FoldF : Foldable F}} {{OrdW : Ord W}} → F W → Maybe W
maximum = foldMap {{MonW = monoid}} just
  where
    monoid : Monoid _
    Monoid.mempty monoid = nothing
    Monoid._<>_ monoid (just x) (just y) = just (max x y)
    Monoid._<>_ monoid (just x) nothing = just x
    Monoid._<>_ monoid nothing (just y) = just y
    Monoid._<>_ monoid nothing nothing = nothing

--- Instances ---

instance
  FoldableList : ∀ {a w} → Foldable {a = a} {w = w} List
  foldMap {{FoldableList}} f = foldr (λ x w → f x <> w) mempty

  FoldableMaybe : ∀ {a w} → Foldable {a = a} {w = w} Maybe
  foldMap {{FoldableMaybe}} = maybe mempty

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module Bin where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Naturals using (ℕ; zero; suc; _+_; _*_)

-- 2進数の表現
data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

-- 2進数のインクリメント
inc : Bin → Bin
inc ⟨⟩    = ⟨⟩ I
inc (b O) = b I
inc (b I) = inc b O

_ : inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
_ = refl

_ : inc (⟨⟩ O O O O) ≡ ⟨⟩ O O O I
_ = refl

_ : inc (⟨⟩ O O O I) ≡ ⟨⟩ O O I O
_ = refl

_ : inc (⟨⟩ O O I O) ≡ ⟨⟩ O O I I
_ = refl

_ : inc (⟨⟩ O O I I) ≡ ⟨⟩ O I O O
_ = refl

_ : inc (⟨⟩ O I O O) ≡ ⟨⟩ O I O I
_ = refl

-- 自然数から2進数への変換
to : ℕ → Bin
to zero    = ⟨⟩ O
to (suc n) = inc (to n)

_ : to 0 ≡ ⟨⟩ O
_ = refl

_ : to 1 ≡ ⟨⟩ I
_ = refl

_ : to 2 ≡ ⟨⟩ I O
_ = refl

_ : to 3 ≡ ⟨⟩ I I
_ = refl

_ : to 4 ≡ ⟨⟩ I O O
_ = refl

-- 2進数から自然数への変換
from : Bin → ℕ
from ⟨⟩    = zero
from (b O) = 2 * (from b)
from (b I) = 2 * (from b) + 1

_ : from (⟨⟩ O) ≡ 0
_ = refl

_ : from (⟨⟩ I) ≡ 1
_ = refl

_ : from (⟨⟩ I O) ≡ 2
_ = refl

_ : from (⟨⟩ I I) ≡ 3
_ = refl

_ : from (⟨⟩ I O O) ≡ 4
_ = refl

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
module TypeConstructorsWhichPreserveGuardedness3 where

record ⊤ : Set where

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

-- This should not be allowed.

ℕ : Set
ℕ = ⊤ ⊎ ℕ


text:
module plfa.Induction where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_ ;_∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)

-- @practice: exercise `operators` start
--
-- 1. _+_ _*_: Unit (Zero), Associativity, Commutativity
-- operator _*_ distributes over operator _+_ from the left and right.
--
-- 2. x operator of matrices: Unit (Unit matrix),
-- Associativity (Associativity of the Linear transformation)
-- No Commutativity

-- @practice: exercise `operators` end

_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
  begin
    (3 + 4) + 5
  ≡⟨⟩
    7 + 5
  ≡⟨⟩
    12
  ≡⟨⟩
    3 + 9
  ≡⟨⟩
    3 + (4 + 5)
  ∎

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

-- examples start

+-assoc-2 : ∀ (n p : ℕ) → (2 + n) + p ≡ 2 + (n + p)
+-assoc-2 n p =
  begin
    (2 + n) + p
  ≡⟨⟩
    suc (1 + n) + p
  ≡⟨⟩
    suc ((1 + n) + p)
  ≡⟨ cong suc (+-assoc-1 n p) ⟩
    suc (1 + (n + p))
  ≡⟨⟩
    2 + (n + p)
  ∎
  where
  +-assoc-1 : ∀ (n p : ℕ) → (1 + n) + p ≡ 1 + (n + p)
  +-assoc-1 n p =
    begin
      (1 + n) + p
    ≡⟨⟩
      suc (0 + n) + p
    ≡⟨⟩
      suc ((0 + n) + p)
    ≡⟨ cong suc (+-assoc-0 n p) ⟩
      suc (0 + (n + p))
    ≡⟨⟩
      1 + (n + p)
    ∎
    where
    +-assoc-0 : ∀ (n p : ℕ) → (0 + n) + p ≡ 0 + (n + p)
    +-assoc-0 n p =
      begin
        (0 + n) + p
      ≡⟨⟩
        n + p
      ≡⟨⟩
        0 + (n + p)
      ∎

-- examples end

+-identityʳ : ∀ ( m : ℕ ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
  ∎

+-suc : ∀ ( m n : ℕ ) → m + suc n ≡ suc ( m + n )
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc ( m + suc n )
  ≡⟨ cong suc (+-suc m n)⟩
    suc ( suc ( m + n ))
  ≡⟨⟩
    suc ( suc m + n)
  ∎

+-comm : ∀ ( m n : ℕ ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc ( +-comm m n )⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

+-rearrange : ∀ (m n p q : ℕ) → (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange m n p q =
  begin
    (m + n) + (p + q)
  ≡⟨ +-assoc m n (p + q) ⟩
    m + (n + (p + q))
  ≡⟨ cong ( m +_ ) (sym (+-assoc n p q)) ⟩
    m + ((n + p) + q)
  ≡⟨ sym (+-assoc m (n + p) q)⟩
    (m + (n + p)) + q
  ∎

-- @stretch: exercise `finite-+-assoc` start

-- Day 0

-- Day 1
-- 0: ℕ

--Day 2
-- 1: ℕ
-- (0 + 0) + 0 ≡ 0 + (0 + 0)

-- Day 3
-- 2: ℕ
-- (0 + 0) + 1 ≡ 0 + (0 + 1)
-- (0 + 1) + 0 ≡ 0 + (1 + 0)
-- (0 + 1) + 1 ≡ 0 + (1 + 1)
-- (1 + 0) + 0 ≡ 1 + (0 + 0)
-- (1 + 0) + 1 ≡ 1 + (0 + 1)
-- (1 + 1) + 0 ≡ 1 + (1 + 0)
-- (1 + 1) + 1 ≡ 1 + (1 + 1)

-- Day 4
-- 3 : ℕ
-- (0 + 0) + 2 ≡ 0 + (0 + 2)
-- (0 + 1) + 2 ≡ 0 + (1 + 2)
-- (0 + 2) + 0 ≡ 0 + (2 + 0)
-- (0 + 2) + 1 ≡ 0 + (2 + 1)
-- (0 + 2) + 2 ≡ 0 + (2 + 2)
-- (1 + 0) + 2 ≡ 1 + (0 + 2)
-- (1 + 1) + 2 ≡ 1 + (1 + 2)
-- (1 + 2) + 0 ≡ 1 + (2 + 0)
-- (1 + 2) + 1 ≡ 1 + (2 + 1)
-- (1 + 2) + 2 ≡ 1 + (2 + 2)
-- (2 + 0) + 0 ≡ 2 + (0 + 0)
-- (2 + 0) + 1 ≡ 2 + (0 + 1)
-- (2 + 0) + 2 ≡ 2 + (0 + 2)
-- (2 + 1) + 0 ≡ 2 + (1 + 0)
-- (2 + 1) + 1 ≡ 2 + (1 + 1)
-- (2 + 1) + 2 ≡ 2 + (1 + 2)
-- (2 + 2) + 0 ≡ 2 + (2 + 0)
-- (2 + 2) + 1 ≡ 2 + (2 + 1)
-- (2 + 2) + 2 ≡ 2 + (2 + 2)

-- @stretch: exercise `finite-+-assoc` end

+-assoc' : ∀ ( m n p : ℕ ) → (m + n) + p ≡ m + (n + p)
+-assoc' zero n p = refl
+-assoc' (suc m) n p rewrite +-assoc' m n p  = refl

+-identity' : ∀ ( n : ℕ ) → n + zero ≡ n
+-identity' zero = refl
+-identity' (suc m) rewrite +-identity' m = refl

+-suc' : ∀ ( m n : ℕ ) → m + suc n ≡ suc (m + n)
+-suc' zero n = refl
+-suc' (suc m) n rewrite +-suc' m n  = refl

+-comm' : ∀ ( m n : ℕ ) → m + n ≡ n + m
+-comm' m zero rewrite +-identity' m = refl
+-comm' m (suc n) rewrite +-suc' m n | +-comm' m n = refl

-- with hole

+-assoc'' : ∀ (m n p : ℕ ) → ( m + n ) + p ≡ m + (n + p)
+-assoc'' zero n p = refl
+-assoc'' (suc m) n p rewrite +-assoc'' m n p = refl

-- @recommended: exercise `+-swap` start

+-swap : ∀ ( m n p : ℕ ) → m + (n + p) ≡ n + (m + p)
+-swap zero n p = refl
+-swap (suc m) n p rewrite +-swap m n p | +-suc n (m + p) = refl

-- @recommended: exercise `+-swap` end

-- @recommended: exercise `*-distrib-+` start

*-distrib-+ : ∀ ( m n p : ℕ ) → ( m + n ) * p ≡ m * p + n * p
*-distrib-+ zero n p = refl
*-distrib-+ (suc m) n p rewrite *-distrib-+ m n p | +-assoc p (m * p) (n * p) = refl

-- @recommended: exercise `*-distrib-+` end

-- @recommended: exercise `*-assoc` start

*-assoc : ∀ ( m n p : ℕ ) → (m * n) * p ≡ m * ( n * p)
*-assoc zero n p = refl
*-assoc (suc m) n p rewrite *-distrib-+ n (m * n) p | *-assoc m n p = refl

-- @recommended: exercise `*-assoc` end

-- @practice: exercise `*-comm` start

*-zeroʳ : ∀ ( m : ℕ ) → m * zero ≡ zero
*-zeroʳ zero = refl
*-zeroʳ ( suc m ) rewrite *-distrib-+ 1 m zero | *-zeroʳ m = refl

*-suc : ∀ ( n m : ℕ ) → n + n * m ≡ n * suc m
*-suc zero m = refl
*-suc (suc n) m
  rewrite
    sym (*-suc n m) |
    sym (+-assoc m n ( n * m )) | sym ( +-assoc n m ( n * m )) |
    +-comm m n = refl

*-comm : ∀ ( m n : ℕ ) → m * n ≡ n * m
*-comm zero n rewrite *-zeroʳ n = refl
*-comm (suc m) n rewrite *-distrib-+ 1 m n | +-identityʳ n | *-comm m n | *-suc n m =  refl

-- @practice: exercise `*-comm` end
-- @practice: exercise `0∸n≡0` start

0∸n≡0 : ∀ ( n : ℕ ) → 0 ∸ n ≡ 0
0∸n≡0 zero = refl
0∸n≡0 (suc n) = refl

-- @practice: exercise `0∸n≡0` end
-- @practice: exercise `∸-|-assoc` start

∸-|-assoc : ∀ ( m n p : ℕ ) → m ∸ n ∸ p ≡ m ∸ ( n + p )
∸-|-assoc zero n p rewrite 0∸n≡0 n | 0∸n≡0 p | 0∸n≡0 ( n + p )  = refl
∸-|-assoc (suc m) zero p = refl
∸-|-assoc (suc m) (suc n) p rewrite ∸-|-assoc m n p = refl

-- @practice: exercise `∸-|-assoc` end

-- @stretch: exercise `+*^` start

^-distribʳ-+-* : ∀ ( m n p : ℕ ) → m ^ ( n + p ) ≡ (m ^ n) * (m ^ p)
^-distribʳ-+-* m zero zero = refl
^-distribʳ-+-* m zero (suc p) rewrite +-identityʳ (m * (m ^ p)) = refl
^-distribʳ-+-* m (suc n) p =
  begin
    m ^ (suc n + p)
  ≡⟨⟩
    m ^ suc ( n + p )
  ≡⟨⟩
    m * ( m ^ ( n + p ) )
  ≡⟨ cong (_*_ m) ( ^-distribʳ-+-* m n p ) ⟩
    m * ( ( m ^ n ) * ( m ^ p ) )
  ≡⟨ sym (*-assoc m (m ^ n) (m ^ p)) ⟩
    m * ( m ^ n ) * (m ^ p)
  ≡⟨⟩
    (m ^ suc n ) * ( m ^ p )
  ∎

^-sucʳ : ∀ ( n p : ℕ ) → n ^ suc p ≡ n * n ^ p
^-sucʳ n p  = refl

^-distribˡ-* : ∀ ( m n p : ℕ ) → (m * n) ^ p ≡ ( m ^ p ) * ( n ^ p)
^-distribˡ-* m n zero = refl
^-distribˡ-* m n (suc p) =
  begin
    (m * n) ^ ( suc p )
  ≡⟨ ^-sucʳ (m * n) p ⟩
    (m * n) * ((m * n) ^ p)
  ≡⟨ cong (_*_ (m * n)) (^-distribˡ-* m n p) ⟩
    m * n  * ((m ^ p) * (n ^ p))
  ≡⟨ sym (*-assoc (m * n) (m ^ p) (n ^ p)) ⟩
    m * n * (m ^ p) * (n ^ p)
  ≡⟨ *-1234-[13][24] m n (m ^ p) (n ^ p) ⟩
    (m * m ^ p ) * (n * n ^ p)
  ≡⟨ cong (_*_ (m * m ^ p)) (sym (^-sucʳ n p))⟩
    (m * m ^ p ) * ( n ^ suc p)
  ≡⟨ cong (λ {x → x * (n ^ suc p)}) (^-sucʳ m p) ⟩
    (m ^ suc p) * (n ^ suc p)
  ∎
  where
  *-1234-[13][24] : ∀ ( a b c d : ℕ ) → a * b * c * d ≡ (a * c) * ( b * d )
  *-1234-[13][24] a b c d
    rewrite
      *-assoc a b c |
      *-comm b c |
      sym (*-assoc a c b) |
      *-assoc (a * c) b d = refl

^-oneˡ : ∀ ( p : ℕ ) → 1 ^ p ≡ 1
^-oneˡ zero = refl
^-oneˡ (suc p) rewrite ^-oneˡ p = refl

^-distribʳ-* :  ∀ ( m n p : ℕ ) → m ^ (n * p) ≡ (m ^ n) ^ p
^-distribʳ-* m zero p rewrite ^-oneˡ p = refl
^-distribʳ-* m n zero rewrite *-zeroʳ n = refl
^-distribʳ-* m (suc n) (suc p)
  rewrite
    ^-distribʳ-+-* m p ( n * suc p) |
    ^-distribˡ-* m (m ^ n) p |
    ^-distribʳ-* m n (suc p) =
    begin
      m * ((m ^ p) * ((m ^ n) * ((m ^ n) ^ p)))
    ≡⟨ *-1[2[34]]-13[24] m (m ^ p) (m ^ n) ((m ^ n) ^ p) ⟩
      m * (m ^ n) * ((m ^ p) * ((m ^ n) ^ p))
    ∎
    where
    *-1[2[34]]-13[24] : ∀ ( a b c d : ℕ ) → a * ( b * ( c * d ) ) ≡ a * c * ( b * d )
    *-1[2[34]]-13[24] a b c d
      rewrite
        sym (*-assoc b c d) |
        *-comm b c |
        *-assoc c b d |
        sym (*-assoc a c (b * d)) = refl

-- @stretch: exercise `+*^` end

-- @stretch: exercise `Bin-laws` start

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc (m O) = m I
inc (m I) = (inc m) O
inc ⟨⟩ = ⟨⟩ I

to : ℕ → Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)

from : Bin -> ℕ
from (m O) = 2 * (from m)
from (m I) = 2 * (from m) + 1
from ⟨⟩ = 0

comm-+-from : ∀ ( b : Bin ) → from (inc b) ≡ suc (from b)
comm-+-from ⟨⟩ = refl
comm-+-from (b O)
  rewrite
    sym ( +-suc' (from b) (from b + zero)) |
    +-assoc' (from b) (from b + 0) 1 |
    +-identityʳ (from b) |
    +-comm' (from b) 1 = refl
comm-+-from (b I)
  rewrite
    +-identityʳ (from (inc b)) | +-identityʳ ( from b) |
    comm-+-from b |
    sym (+-comm' (from b) 1) |
    +-assoc' (from b) (from b) 1 = refl

identity-to-from : ∀ ( n : ℕ ) → from (to n) ≡ n
identity-to-from zero = refl
identity-to-from (suc n) rewrite comm-+-from (to n) | identity-to-from n  = refl

-- ⟨⟩ !== ⟨⟩ O
-- @todo: rewrite with ∃-syntax

-- @stretch: exercise `Bin-laws` end

-- import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)

max_stars_repo_name: lonelyhentai/workspace

max_issues_repo_name: lonelyhentai/workspace

max_forks_repo_name: lonelyhentai/workspace


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Polynomials.UnivariateFun.Base where

open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyFun public

{-

The Univariate Functional Polynomials over a CommRing A is a CommRing.
The base type is define using almost null sequences ie functions.
This definition enables to defined a direct sum indexed by ℕ.
Thus base type and the AbGroup part of the CommRing is define an instance
of the more general Direct Sum one which can be found here :
-}

open import Cubical.Algebra.DirectSum.DirectSumFun.Base

{-

On this definition of the Direct Sum, it is possible to raise a Graded Ring structure.
Then complete it to be a CommRing. Those version of the polynomials are hence
a instance of this graded ring structure.

see : for the details of the constructions

-}

open import Cubical.Algebra.GradedRing.DirectSumFun

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-

Part 2: Transport and composition

• Cubical transport
• Subst as a special case of cubical transport
• Path induction from subst
• Homogeneous composition (hcomp)
• Binary composition of paths as special case of hcomp

-}

{-# OPTIONS --cubical #-}
module Part2 where

open import Part1

-- While path types are great for reasoning about equality they don't
-- let us transport along paths between types or even compose paths.
-- Furthermore, as paths are not inductively defined we don't
-- automatically get an induction principle for them. In order to
-- remedy this Cubical Agda also has a built-in (generalized)
-- transport operation and homogeneous composition operation from
-- which the induction principle (and much more!) is derivable.

-- The basic operation is called transp and we will soon explain it,
-- but let's first focus on the special case of cubical transport:
transport : A ≡ B → A → B
transport p a = transp (λ i → p i) i0 a

-- This is a more primitive operation than "transport" in HoTT as it
-- only lets us turn a path into a function. However, the transport of
-- HoTT can easily be proved from cubical transport and in order to
-- avoid a name clash we call it "subst":
subst : (B : A → Type ℓ') {x y : A} (p : x ≡ y) → B x → B y
subst B p pa = transport (λ i → B (p i)) pa

-- The transp operation is a generalized transport in the sense that
-- it lets us specify where the transport is the identity function.
-- The general type of transp is:
--
--   transp : (A : I → Type ℓ) (r : I) (a : A i0) → A i1
--
-- There is an additional side condition which to be satisfied for
-- Cubical Agda to typecheck "transp A r a". This is that A has to be
-- "constant" on r. This means that A should be a constant function
-- whenever r = i1 is satisfied. This side condition is vacuously true
-- when r = i0, so there is nothing to check when writing transport as
-- above. However, when r is equal to i1 the transp function will
-- compute as the identity function.
--
--   transp A i1 a = a
--
-- Having this extra generality is useful for quite technical reasons,
-- for instance we can easily relate a with its transport over p:
transportFill : (p : A ≡ B) (a : A) → PathP (λ i → p i) a (transport p a)
transportFill p a i = transp (λ j → p (i ∧ j)) (~ i) a

-- Another result that follows easily from transp is that transporting
-- in a constant family is the identity function (up to a path). Note
-- that this is *not* proved by refl. This is maybe not surprising as
-- transport is not defined by pattern-matching on p.
transportRefl : (x : A) → transport refl x ≡ x
transportRefl {A = A} x i = transp (λ _ → A) i x

-- Having transp lets us prove many more useful lemmas like this. For
-- details see:
--
--   Cubical.Foundations.Transport
--
-- For experts: the file
--
--   Cubical.Foundations.CartesianKanOps
--
-- contains a reformulation of these operations which might be useful
-- for people familiar with "cartesian" cubical type theory.

-- We can also define the J eliminator (aka path induction)
J : {x : A} (P : (z : A) → x ≡ z → Type ℓ'')
    (d : P x refl) {y : A} (p : x ≡ y) → P y p
J {x = x} P d p = subst (λ X → P (fst X) (snd X)) (isContrSingl x .snd (_ , p)) d

-- Unfolded version:
--
-- transport (λ i → P (p i) (λ j → p (i ∧ j))) d

-- So J is provable, but it doesn't satisfy the computation rule of
-- refl definitionally as _≡_ is not inductively defined. See
-- exercises for how to prove it. Not having this hold definitionally
-- is almost never a problem in practice as the cubical primitives
-- satisfy many new definitional equalities (c.f. cong).

-- As we now have J we can define path concatenation and many more
-- things, however this is not the way to do things in Cubical
-- Agda. One of the key features of cubical type theory is that the
-- transp primitive reduces differently for different types formers
-- (see CCHM or the Cubical Agda paper for details). For paths it
-- reduces to another primitive operation called hcomp. This primitive
-- is much better suited for concatenating paths than J as it is much
-- more general. In particular, it lets us compose multiple higher
-- dimensional cubes directly. We will explain it by example.

-- In order to compose two paths we write:
compPath : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
compPath {x = x} p q i = hcomp (λ j → λ { (i = i0) → x
                                        ; (i = i1) → q j })
                               (p i)

-- This is best understood with the following drawing:
--
--     x             z
--     ^             ^
--     ¦             ¦
--   x ¦             ¦ q j
--     ¦             ¦
--     x ----------> y
--           p i
--
-- In the drawing the direction i goes left-to-right and j goes
-- bottom-to-top. As we are constructing a path from x to z along i we
-- have i : I in the context already and we put p i as bottom. The
-- direction j that we are doing the composition in is abstracted in
-- the first argument to hcomp.

-- These are related to lifting conditions for Kan cubical sets.

-- A more natural form of composition of paths in Cubical Agda is
-- ternary composition:
--
--          x             w
--          ^             ^
--          ¦             ¦
--  p (~ j) ¦             ¦ r j
--          ¦             ¦
--          y ----------> z
--                q i
--
-- This is written p ∙∙ q ∙∙ r in the agda/cubical library (∙ is "\.")
-- and implemented by:

_∙∙_∙∙_ : {x y z w : A} → x ≡ y → y ≡ z → z ≡ w → x ≡ w
(p ∙∙ q ∙∙ r) i = hcomp (λ j → λ { (i = i0) → p (~ j)
                                 ; (i = i1) → r j })
                        (q i)

-- Note that we can easily define mixfix operators with many arguments
-- in Agda.

-- Using this we can define compPath much slicker:
_∙_ : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
p ∙ q = refl ∙∙ p ∙∙ q

-- To prove algebraic properties of this operation (in particular that
-- it's a groupoid) we need to talk about filling using the hfill
-- operation. There is no time for this today, but the interested
-- reader can consult
--
--    Cubical.Foundations.GroupoidLaws

-- In case there is time I might show the following briefly:

doubleCompPath-filler : {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
                      → PathP (λ j → p (~ j) ≡ r j) q (p ∙∙ q ∙∙ r)
doubleCompPath-filler p q r j i =
  hfill (λ j → λ { (i = i0) → p (~ j)
                 ; (i = i1) → r j })
        (inS (q i)) j

compPath-filler : {x y z : A} (p : x ≡ y) (q : y ≡ z)
                → PathP (λ j → x ≡ q j) p (p ∙ q)
compPath-filler p q = doubleCompPath-filler refl p q

rUnit : {x y : A} (p : x ≡ y) → p ≡ p ∙ refl
rUnit p i j = compPath-filler p refl i j

-- Having hcomp as a primitive operation lets us prove many things
-- very directly. For instance, we can prove that any proposition is
-- also a set using a higher dimensional hcomp.
isProp→isSet : isProp A → isSet A
isProp→isSet h a b p q j i =
  hcomp (λ k → λ { (i = i0) → h a a k
                 ; (i = i1) → h a b k
                 ; (j = i0) → h a (p i) k
                 ; (j = i1) → h a (q i) k }) a

-- Geometric picture: start with a square with a everywhere as base,
-- then change its sides so that they connect p with q over refl_a and
-- refl_b.

isPropIsProp : isProp (isProp A)
isPropIsProp f g i a b = isProp→isSet f a b (f a b) (g a b) i

isPropIsSet : isProp (isSet A)
isPropIsSet h1 h2 i x y = isPropIsProp (h1 x y) (h2 x y) i

-- In order to understand what the second argument to hcomp is one
-- should read about partial elements. We refer the interested reader
-- to the Cubical Agda documentation:
--
-- https://agda.readthedocs.io/en/v2.6.1.3/language/cubical.html#partial-elements
--
-- However, for beginners one doesn't need to write hcomp to prove
-- thing as the library provide many basic lemmas. In particular, the
-- library provides equational reasoning combinators as in regular
-- Agda which let us write things like:
--
-- inverseUniqueness : (r : R) → isProp (Σ[ r' ∈ R ] r · r' ≡ 1r)
-- inverseUniqueness r (r' , rr'≡1) (r'' , rr''≡1) = Σ≡Prop (λ _ → is-set _ _) path
--  where
--  path : r' ≡ r''
--  path = r'             ≡⟨ sym (·Rid _) ⟩
--         r' · 1r        ≡⟨ cong (r' ·_) (sym rr''≡1) ⟩
--         r' · (r · r'') ≡⟨ ·Assoc _ _ _ ⟩
--         (r' · r) · r'' ≡⟨ cong (_· r'') (·-comm _ _) ⟩
--         (r · r') · r'' ≡⟨ cong (_· r'') rr'≡1 ⟩
--         1r · r''       ≡⟨ ·Lid _ ⟩
--         r''            ∎


text:
module GUIgeneric.loadAllRepository where

open import GUIgeneric.GUI
open import GUIgeneric.GUIDefinitions
open import GUIgeneric.GUIExample
open import GUIgeneric.GUIExampleBankAccount
open import GUIgeneric.GUIExampleLib
open import GUIgeneric.GUIFeatures
open import GUIgeneric.GUIFeaturesPart2
open import GUIgeneric.GUIFeaturesPart3
open import GUIgeneric.GUIFeaturesPart4
open import GUIgeneric.GUIFeaturesPart5
open import GUIgeneric.GUIModel
open import GUIgeneric.GUIModelExample
open import GUIgeneric.Prelude

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


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

open import HoTT

module homotopy.SuspensionLoopSpaceInverse where

{- corollary about inversion in ⊙Trunc k (⊙Ω (⊙Susp (de⊙ X))) -}
private
  custom-path-alg : ∀ {l} {A : Type l}
    {n s : A} (p q : n == s)
    → ! (p ∙ ! q) == ! (! q) ∙ (! p ∙ q) ∙' ! q
  custom-path-alg p q@idp = ap ! (∙-unit-r p) ∙ ! (∙-unit-r (! p))

  Ω-!-Susp-flip-seq : ∀ {i} (X : Ptd i) (x : de⊙ X)
    → ! (merid x ∙ ! (merid (pt X)))
      =-=
      Ω-fmap (⊙Susp-flip X) (σloop X x)
  Ω-!-Susp-flip-seq X x =
    ! (merid x ∙ ! (merid (pt X)))
      =⟪ custom-path-alg (merid x) (merid (pt X)) ⟫
    ! (! (merid (pt X))) ∙ (! (merid x) ∙ merid (pt X)) ∙' ! (merid (pt X))
      =⟪ ap (λ q → ! (! (merid (pt X))) ∙ q ∙' ! (merid (pt X)))
            (! (Susp-flip-σloop X x)) ⟫
    ! (! (merid (pt X))) ∙ ap Susp-flip (σloop X x) ∙' ! (merid (pt X))
      =⟪ ! (Ω-fmap-β (⊙Susp-flip X) (merid x ∙ ! (merid (pt X)))) ⟫
    Ω-fmap (⊙Susp-flip X) (σloop X x) ∎∎

  Ω-!-Susp-flip' : ∀ {i} (X : Ptd i)
    → Ω-! ∘ σloop X ∼ Ω-fmap (⊙Susp-flip X) ∘ σloop X
  Ω-!-Susp-flip' X x = ↯ (Ω-!-Susp-flip-seq X x)

  ⊙Ω-!-Susp-flip' : ∀ {i} (X : Ptd i)
    → ⊙Ω-! ◃⊙∘
      ⊙σloop X ◃⊙idf
      =⊙∘
      ⊙Ω-fmap (⊙Susp-flip X) ◃⊙∘
      ⊙σloop X ◃⊙idf
  ⊙Ω-!-Susp-flip' X = ⊙seq-λ= (Ω-!-Susp-flip' X) $ !ₛ $
    ↯ (Ω-!-Susp-flip-seq X (pt X)) ◃∙
    ap (Ω-fmap (⊙Susp-flip X)) (!-inv-r (merid (pt X))) ◃∙
    snd (⊙Ω-fmap (⊙Susp-flip X)) ◃∎
      =ₛ⟨ 0 & 1 & expand (Ω-!-Susp-flip-seq X (pt X)) ⟩
    custom-path-alg (merid (pt X)) (merid (pt X)) ◃∙
    ap (λ q → ! (! (merid (pt X))) ∙ q ∙' ! (merid (pt X)))
       (! (Susp-flip-σloop X (pt X))) ◃∙
    ! (Ω-fmap-β (⊙Susp-flip X) (merid (pt X) ∙ ! (merid (pt X)))) ◃∙
    ap (Ω-fmap (⊙Susp-flip X)) (!-inv-r (merid (pt X))) ◃∙
    snd (⊙Ω-fmap (⊙Susp-flip X)) ◃∎
      =ₛ⟨ 2 & 2 & !ₛ $ homotopy-naturality
            (λ p → ! (! (merid (pt X))) ∙ ap Susp-flip p ∙' ! (merid (pt X)))
            (λ p → Ω-fmap (⊙Susp-flip X) p)
            (λ p → ! (Ω-fmap-β (⊙Susp-flip X) p))
            (!-inv-r (merid (pt X))) ⟩
    custom-path-alg (merid (pt X)) (merid (pt X)) ◃∙
    ap (λ q → ! (! (merid (pt X))) ∙ q ∙' ! (merid (pt X)))
       (! (Susp-flip-σloop X (pt X))) ◃∙
    ap (λ p → ! (! (merid (pt X))) ∙ ap Susp-flip p ∙' ! (merid (pt X)))
       (!-inv-r (merid (pt X))) ◃∙
    ! (Ω-fmap-β (⊙Susp-flip X) idp) ◃∙
    snd (⊙Ω-fmap (⊙Susp-flip X)) ◃∎
      =ₛ⟨ 3 & 2 & pre-rotate'-in $ Ω-fmap-pt (⊙Susp-flip X) ⟩
    custom-path-alg (merid (pt X)) (merid (pt X)) ◃∙
    ap (λ q → ! (! (merid (pt X))) ∙ q ∙' ! (merid (pt X)))
       (! (Susp-flip-σloop X (pt X))) ◃∙
    ap (λ p → ! (! (merid (pt X))) ∙ ap Susp-flip p ∙' ! (merid (pt X)))
       (!-inv-r (merid (pt X))) ◃∙
    ap (! (! (merid (pt X))) ∙_) (∙'-unit-l (snd (⊙Susp-flip X))) ◃∙
    !-inv-l (snd (⊙Susp-flip X)) ◃∎
      =ₛ₁⟨ 2 & 1 & ap-∘ (λ q → ! (! (merid (pt X))) ∙ q ∙' ! (merid (pt X)))
                        (ap Susp-flip)
                        (!-inv-r (merid (pt X))) ⟩
    custom-path-alg (merid (pt X)) (merid (pt X)) ◃∙
    ap (λ q → ! (! (merid (pt X))) ∙ q ∙' ! (merid (pt X)))
       (! (Susp-flip-σloop X (pt X))) ◃∙
    ap (λ q → ! (! (merid (pt X))) ∙ q ∙' ! (merid (pt X)))
       (ap (ap Susp-flip) (!-inv-r (merid (pt X)))) ◃∙
    ap (! (! (merid (pt X))) ∙_) (∙'-unit-l (snd (⊙Susp-flip X))) ◃∙
    !-inv-l (snd (⊙Susp-flip X)) ◃∎
      =ₛ⟨ 1 & 2 & ap-seq-=ₛ (λ q → ! (! (merid (pt X))) ∙ q ∙' ! (merid (pt X))) $
                  !ₛ $ post-rotate-out $ pre-rotate-in $ Susp-flip-σloop-pt X ⟩
    custom-path-alg (merid (pt X)) (merid (pt X)) ◃∙
    ap (λ q → ! (! (merid (pt X))) ∙ q ∙' ! (merid (pt X)))
       (!-inv-l (merid (pt X))) ◃∙
    ap (! (! (merid (pt X))) ∙_) (∙'-unit-l (! (merid (pt X)))) ◃∙
    !-inv-l (! (merid (pt X))) ◃∎
      =ₛ⟨ custom-path-alg-coh (merid (pt X)) ⟩
    ap ! (!-inv-r (merid (pt X))) ◃∎
      =ₛ⟨ 1 & 0 & contract ⟩
    ap ! (!-inv-r (merid (pt X))) ◃∙
    idp ◃∎ ∎ₛ
    where
    custom-path-alg-coh : ∀ {l} {A : Type l}
      {n s : A} (p : n == s)
      → custom-path-alg p p ◃∙
        ap (λ q → ! (! p) ∙ q ∙' ! p) (!-inv-l p) ◃∙
        ap (! (! p) ∙_) (∙'-unit-l (! p)) ◃∙
        !-inv-l (! p) ◃∎
        =ₛ
        ap ! (!-inv-r p) ◃∎
    custom-path-alg-coh p@idp = =ₛ-in idp

⊙Ω-!-⊙Susp-flip : ∀ {i} (X : Ptd i) (n : ℕ₋₂)
  → is-equiv (Trunc-fmap {n = n} (σloop X))
  → ⊙Trunc-fmap {n = n} ⊙Ω-! == ⊙Trunc-fmap {n = n} (⊙Ω-fmap (⊙Susp-flip X))
⊙Ω-!-⊙Susp-flip X n is-eq =
  –>-is-inj
    (pre⊙∘-equiv
      {Z = ⊙Trunc n (⊙Ω (⊙Susp (de⊙ X)))}
      (⊙Trunc-fmap {n = n} (⊙σloop X) , is-eq))
    (⊙Trunc-fmap {n = n} ⊙Ω-!)
    (⊙Trunc-fmap {n = n} (⊙Ω-fmap (⊙Susp-flip X)))
    (=⊙∘-out (⊙Trunc-fmap-seq-=⊙∘ {n = n} (⊙Ω-!-Susp-flip' X)))

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Structures.Monoid where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Prod.Base hiding (_×_) renaming (_×Σ_ to _×_)

open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)

open import Cubical.Structures.Pointed
open import Cubical.Structures.InftyMagma

private
  variable
    ℓ : Level

-- Now we're getting serious: Monoids
raw-monoid-structure : Type ℓ → Type ℓ
raw-monoid-structure X = X × (X → X → X)

raw-monoid-iso : StrIso raw-monoid-structure ℓ
raw-monoid-iso (M , e , _·_) (N , d , _∗_) f =
    (equivFun f e ≡ d)
  × ((x y : M) → equivFun f (x · y) ≡ (equivFun f x) ∗ (equivFun f y))

-- If we ignore the axioms we get something like a "raw" monoid, which
-- essentially is the join of a pointed type and an ∞-magma
raw-monoid-is-SNS : SNS {ℓ} raw-monoid-structure raw-monoid-iso
raw-monoid-is-SNS = join-SNS pointed-structure pointed-iso pointed-is-SNS
                             ∞-magma-structure ∞-magma-iso ∞-magma-is-SNS

-- Now define monoids
monoid-axioms : (X : Type ℓ) → raw-monoid-structure X → Type ℓ
monoid-axioms X (e , _·_ ) = isSet X
                           × ((x y z : X) → (x · (y · z)) ≡ ((x · y) · z))
                           × ((x : X) → (x · e) ≡ x)
                           × ((x : X) → (e · x) ≡ x)

monoid-structure : Type ℓ → Type ℓ
monoid-structure = add-to-structure (raw-monoid-structure) monoid-axioms

Monoids : Type (ℓ-suc ℓ)
Monoids {ℓ} = TypeWithStr ℓ monoid-structure

monoid-iso : StrIso monoid-structure ℓ
monoid-iso = add-to-iso raw-monoid-structure raw-monoid-iso monoid-axioms

-- We have to show that the monoid axioms are indeed propositions
monoid-axioms-are-Props : (X : Type ℓ) (s : raw-monoid-structure X) → isProp (monoid-axioms X s)
monoid-axioms-are-Props X (e , _·_) s = β s
   where
   α = s .fst
   -- TODO: it would be nice to have versions of this lemmas for higher arities
   β =     isPropΣ isPropIsSet
     λ _ → isPropΣ (isPropPi (λ x → isPropPi (λ y → isPropPi (λ z → α (x · (y · z)) ((x · y) · z)))))
     λ _ → isPropΣ (isPropPi (λ x → α (x · e) x))
     λ _ →          isPropPi (λ x → α (e · x) x)

monoid-is-SNS : SNS {ℓ} monoid-structure monoid-iso
monoid-is-SNS = add-axioms-SNS raw-monoid-structure raw-monoid-iso
                               monoid-axioms monoid-axioms-are-Props raw-monoid-is-SNS

MonoidPath : (M N : Monoids {ℓ}) → (M ≃[ monoid-iso ] N) ≃ (M ≡ N)
MonoidPath M N = SIP monoid-structure monoid-iso monoid-is-SNS M N

-- Added for groups
-- If there exists a inverse of an element it is unique

inv-lemma : (X : Type ℓ) (e : X) (_·_ : X → X → X)
          → monoid-axioms X (e , _·_)
          → (x y z : X)
          → y · x ≡ e
          → x · z ≡ e
          → y ≡ z
inv-lemma X e _·_ (is-set-X , assoc , runit , lunit) x y z left-inverse right-inverse =
  y           ≡⟨ sym (runit y) ⟩
  y · e       ≡⟨ cong (y ·_) (sym right-inverse) ⟩
  y · (x · z) ≡⟨ assoc y x z ⟩
  (y · x) · z ≡⟨ cong (_· z) left-inverse ⟩
  e · z       ≡⟨ lunit z ⟩
  z ∎

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
{- Name: Bowornmet (Ben) Hudson

-- define the source language from the paper

-}

open import Preliminaries
open import Preorder-withmax

module Proofs where

  -- define the source language from the paper
  -- we want to focus on arrow, cross, and nat types
  data Tp : Set where
    unit : Tp
    nat : Tp
    susp : Tp → Tp
    _->s_ : Tp → Tp → Tp
    _×s_ : Tp → Tp → Tp

  data Cost : Set where
    0c : Cost
    1c : Cost
    _+c_ : Cost → Cost → Cost

  data Equals0c : Cost → Set where
    Eq0-0c : Equals0c 0c
    Eq0-+c : ∀ {c c'} → Equals0c c → Equals0c c' → Equals0c (c +c c')

  -- represent a context as a list of types
  Ctx = List Tp

  -- de Bruijn indices (for free variables)
  data _∈_ : Tp → Ctx → Set where
    i0 : ∀ {Γ τ}
       → τ ∈ (τ :: Γ)
    iS : ∀ {Γ τ τ1}
       → τ ∈ Γ
       → τ ∈ (τ1 :: Γ)

  data _|-_ : Ctx → Tp → Set where
    unit : ∀ {Γ}
         → Γ |- unit
    var : ∀ {Γ τ}
        → τ ∈ Γ
        → Γ |- τ
    z : ∀ {Γ}
      → Γ |- nat
    suc : ∀ {Γ}
        → (e : Γ |- nat)
        → Γ |- nat
    rec : ∀ {Γ τ}
        → Γ |- nat
        → Γ |- τ
        → (nat :: (susp τ :: Γ)) |- τ
        → Γ |- τ
    lam : ∀ {Γ τ ρ}
        → (ρ :: Γ) |- τ
        → Γ |- (ρ ->s τ)
    app : ∀ {Γ τ1 τ2}
        → Γ |- (τ2 ->s τ1)
        → Γ |- τ2
        → Γ |- τ1
    prod : ∀ {Γ τ1 τ2}
         → Γ |- τ1
         → Γ |- τ2
         → Γ |- (τ1 ×s τ2)
    l-proj : ∀ {Γ τ1 τ2}
           → Γ |- (τ1 ×s τ2)
           → Γ |- τ1
    r-proj : ∀ {Γ τ1 τ2}
           → Γ |- (τ1 ×s τ2)
           → Γ |- τ2
    -- include split, delay/susp/force instead of usual elim rules for products
    delay : ∀ {Γ τ}
          → Γ |- τ
          → Γ |- susp τ
    force : ∀ {Γ τ}
          → Γ |- susp τ
          → Γ |- τ
    split : ∀ {Γ τ τ1 τ2}
          → Γ |- (τ1 ×s τ2)
          → (τ1 :: (τ2 :: Γ)) |- τ
          → Γ |- τ

------weakening and substitution lemmas

 -- renaming function
  rctx : Ctx → Ctx → Set
  rctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → τ ∈ Γ

  -- re: transferring variables in contexts
  lem1 : ∀ {Γ Γ' τ} → rctx Γ Γ' → rctx (τ :: Γ) (τ :: Γ')
  lem1 d i0 = i0
  lem1 d (iS x) = iS (d x)

  -- renaming lemma
  ren : ∀ {Γ Γ' τ} → Γ' |- τ → rctx Γ Γ' → Γ |- τ
  ren unit d = unit
  ren (var x) d = var (d x)
  ren z d = z
  ren (suc e) d = suc (ren e d)
  ren (rec e e0 e1) d = rec (ren e d) (ren e0 d) (ren e1 (lem1 (lem1 d)))
  ren (lam e) d = lam (ren e (lem1 d))
  ren (app e1 e2) d = app (ren e1 d) (ren e2 d)
  ren (prod e1 e2) d = prod (ren e1 d) (ren e2 d)
  ren (l-proj e) d = l-proj (ren e d)
  ren (r-proj e) d = r-proj (ren e d)
  ren (delay e) d = delay (ren e d)
  ren (force e) d = force (ren e d)
  ren (split e e1) d = split (ren e d) (ren e1 (lem1 (lem1 d)))

  -- substitution
  sctx : Ctx → Ctx → Set
  sctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → Γ |- τ

  -- weakening a context
  wkn : ∀ {Γ τ1 τ2} → Γ |- τ2 → (τ1 :: Γ) |- τ2
  wkn e = ren e iS

  -- weakening also works with substitution
  wkn-s : ∀ {Γ τ1 Γ'} → sctx Γ Γ' → sctx (τ1 :: Γ) Γ'
  wkn-s d = λ f → wkn (d f)

  wkn-r : ∀ {Γ τ1 Γ'} → rctx Γ Γ' → rctx (τ1 :: Γ) Γ'
  wkn-r d = λ x → iS (d x)

  -- lem2 (need a lemma for subst like we did for renaming)
  lem2 : ∀ {Γ Γ' τ} → sctx Γ Γ' → sctx (τ :: Γ) (τ :: Γ')
  lem2 d i0 = var i0
  lem2 d (iS i) = wkn (d i)

  -- another substitution lemma
  lem3 : ∀ {Γ τ} → Γ |- τ → sctx Γ (τ :: Γ)
  lem3 e i0 = e
  lem3 e (iS i) = var i

  lem3' : ∀ {Γ Γ' τ} → sctx Γ Γ' → Γ |- τ → sctx Γ (τ :: Γ')
  lem3' Θ e i0 = e
  lem3' Θ e (iS i) = Θ i

  -- one final lemma needed for the last stepping rule. Thank you Professor Licata!
  lem4 : ∀ {Γ τ1 τ2} → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ))
  lem4 e1 e2 i0 = e1
  lem4 e1 e2 (iS i0) = e2
  lem4 e1 e2 (iS (iS i)) = var i

  lem4' : ∀ {Γ Γ' τ1 τ2} → sctx Γ Γ' → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ'))
  lem4' Θ a b i0 = a
  lem4' Θ a b (iS i0) = b
  lem4' Θ a b (iS (iS i)) = Θ i

  lem5 : ∀ {Γ τ1 τ2} → Γ |- (τ1 ×s τ2) → sctx Γ ((τ1 ×s τ2) :: (τ1 :: (τ2 :: Γ)))
  lem5 e i0 = e
  lem5 e (iS i0) = l-proj e
  lem5 e (iS (iS i0)) = r-proj e
  lem5 e (iS (iS (iS i))) = var i

  -- the 'real' substitution lemma (if (x : τ') :: Γ |- (e : τ) and Γ |- (e : τ') , then Γ |- e[x -> e'] : τ)
  subst : ∀ {Γ Γ' τ} → sctx Γ Γ' → Γ' |- τ → Γ |- τ
  subst d unit = unit
  subst d (var x) = d x
  subst d z = z
  subst d (suc x) = suc (subst d x)
  subst d (rec e e0 e1) = rec (subst d e) (subst d e0) (subst (lem2 (lem2 d)) e1)
  subst d (lam e) = lam (subst (lem2 d) e)
  subst d (app e1 e2) = app (subst d e1) (subst d e2)
  subst d (prod e1 e2) = prod (subst d e1) (subst d e2)
  subst d (l-proj e) = l-proj (subst d e)
  subst d (r-proj e) = r-proj (subst d e)
  subst d (delay e) = delay (subst d e)
  subst d (force e) = force (subst d e)
  subst d (split e e1) = split (subst d e) (subst (lem2 (lem2 d)) e1)

  subst-compose : ∀ {Γ Γ' τ τ1} (Θ : sctx Γ Γ') (v : Γ |- τ) (e : (τ :: Γ' |- τ1) )
                → subst (lem3 v) (subst (lem2 Θ) e) == subst (lem3' Θ v) e
  subst-compose Θ unit e = {!!}
  subst-compose Θ (var x) e = {!!}
  subst-compose Θ z e = {!!}
  subst-compose Θ (suc v) e = {!!}
  subst-compose Θ (rec v v₁ v₂) e = {!!}
  subst-compose Θ (lam v) e = {!!}
  subst-compose Θ (app v v₁) e = {!!}
  subst-compose Θ (prod v v₁) e = {!!}
  subst-compose Θ (l-proj v) e = {!!}
  subst-compose Θ (r-proj v) e = {!!}
  subst-compose Θ (delay v) e = {!!}
  subst-compose Θ (force v) e = {!!}
  subst-compose Θ (split v v₁) e = {!!}

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommSemiring.Instances.UpperNat where
{-
  based on:
  https://github.com/DavidJaz/Cohesion/blob/master/UpperNaturals.agda

  and the slides here (for arithmetic operation):
  https://felix-cherubini.de/myers-slides-II.pdf
-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Functions.Logic
open import Cubical.Functions.Embedding

open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.OrderedCommMonoid
open import Cubical.Algebra.OrderedCommMonoid.PropCompletion
open import Cubical.Algebra.OrderedCommMonoid.Instances
open import Cubical.Algebra.CommSemiring

open import Cubical.Data.Nat using (ℕ; ·-distribˡ)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty hiding (⊥)
open import Cubical.Data.Sigma

open import Cubical.HITs.Truncation
open import Cubical.HITs.PropositionalTruncation as PT

private
  variable
    ℓ : Level

{- The Upper Naturals
   An upper natural is an upward closed proposition on natural numbers.
   The interpretation is that an upper natural is a natural ``defined by its upper bounds'', in the
   sense that for the proposition N holding of a natural n means that n is an upper bound of N.
   The important bit about upper naturals is that they satisfy the well-ordering principle,
   constructively (no proof of that is given here).

   Example Application:
   The degree of a polynomial P=∑_{i=0}^{n} aᵢ · Xⁱ may be defined as an upper natural:

     deg(P) :≡ (λ n → all non-zero indices have index smaller n)

     Or: deg(∑_{i=0}^{n} aᵢ · Xⁱ) = λ (k : ℕ) → ∀ (k+1 ≤ i ≤ n) aᵢ≡0

   This works even if a constructive definition of polynomial is used.

   However the upper naturals are a bit too unconstraint and do not even form a semiring,
   since they include 'infinity' elements like the proposition that is always false.

   This is different for the subtype of *bounded* upper naturals ℕ↑b.
-}

module ConstructionUnbounded where
  ℕ↑-+ = PropCompletion ℕ≤+
  ℕ↑-· = PropCompletion ℕ≤·

  open OrderedCommMonoidStr (snd ℕ↑-+)
    hiding (_≤_; MonotoneL; MonotoneR)
    renaming (·Assoc to +Assoc; ·Comm to +Comm; ·IdR to +Rid;
              _·_ to _+_; ε to 0↑)

  open OrderedCommMonoidStr (snd ℕ≤·)
   using (MonotoneL; MonotoneR)

  open OrderedCommMonoidStr (snd ℕ≤+)
   hiding (_≤_)
   renaming (_·_ to _+ℕ_;
             MonotoneL to +MonotoneL; MonotoneR to +MonotoneR;
             ·Comm to ℕ+Comm)

  open OrderedCommMonoidStr ⦃...⦄
    using (_·_ ; ·Assoc ; ·Comm )
    renaming (·IdR to ·Rid)

  private
    instance
      _ : OrderedCommMonoidStr _ _
      _  = snd ℕ↑-·
      _ : OrderedCommMonoidStr _ _
      _ = snd ℕ≤·

  ℕ↑ : Type₁
  ℕ↑ = fst ℕ↑-+

  open PropCompletion ℓ-zero ℕ≤+
    using (typeAt; pathFromImplications)

  open <-Reasoning using (_≤⟨_⟩_)

  +LDist· : (x y z : ℕ↑) →
            x · (y + z) ≡ (x · y) + (x · z)
  +LDist· x y z =
    pathFromImplications
      (x · (y + z)) ((x · y) + (x · z))
      (⇒) ⇐
    where
      ⇒ : (n : ℕ) → typeAt n (x · (y + z))  → typeAt n ((x · y) + (x · z))
      ⇒ n = PT.rec
             isPropPropTrunc
             λ {((a , b) , xa , (y+zb , a·b≤n)) →
                 PT.rec
                   isPropPropTrunc
                   (λ {((a' , b') , ya' , (zb' , a'+b'≤b))
                     → ∣ ((a · a') , (a · b')) ,
                          ∣ (a , a') , (xa , (ya' , ≤-refl)) ∣₁ ,
                          (∣ (a , b') , (xa , (zb' , ≤-refl)) ∣₁ ,
                          subst (_≤ n) (sym (·-distribˡ a a' b'))
                            (≤-trans (MonotoneL {z = a} a'+b'≤b) a·b≤n)) ∣₁ })
                   y+zb}

      ⇐ : (n : ℕ) → _
      ⇐ n =
        PT.rec
          isPropPropTrunc
          λ {((a , b) , x·ya , (x·zb , a+b≤n))
          → PT.rec
              isPropPropTrunc
              (λ {((a' , b') , a'x , (b'y , a'·b'≤a))
              → PT.rec
                  isPropPropTrunc
                  (λ {((a″ , b″) , a″x , (zb″ , a″·b″≤b))
                  → ∣ ≤CaseInduction {n = a'} {m = a″}
                        (λ a'≤a″ →
                          (a' , (b' +ℕ b″)) , a'x ,

                          (∣ (b' , b″) , (b'y , (zb″ , ≤-refl)) ∣₁ ,
                           (a' · (b' +ℕ b″)       ≤⟨ subst
                                                       (_≤ (a' · b') +ℕ (a' · b″))
                                                       (·-distribˡ a' b' b″) ≤-refl ⟩
                           (a' · b') +ℕ (a' · b″) ≤⟨ +MonotoneR a'·b'≤a ⟩
                            a +ℕ (a' · b″)        ≤⟨ +MonotoneL
                                                       (≤-trans (MonotoneR a'≤a″) a″·b″≤b) ⟩
                            a+b≤n ))
                        )
                        (λ a″≤a' →
                         (a″ , (b' +ℕ b″)) , (a″x ,
                         (∣ (b' , b″) , (b'y , (zb″ , ≤-refl)) ∣₁ ,
                           ((a″ · (b' +ℕ b″))      ≤⟨ subst
                                                        (_≤ (a″ · b') +ℕ (a″ · b″))
                                                        (·-distribˡ a″ b' b″) ≤-refl ⟩
                            (a″ · b') +ℕ (a″ · b″) ≤⟨ +MonotoneR
                                                        ((a″ · b') ≤⟨ MonotoneR a″≤a' ⟩ a'·b'≤a) ⟩
                            a +ℕ (a″ · b″)         ≤⟨ +MonotoneL a″·b″≤b  ⟩
                            a+b≤n)))
                        )
                    ∣₁})
                  x·zb})
              x·ya}

module ConstructionBounded where
  ℕ↑-+b = BoundedPropCompletion ℕ≤+
  ℕ↑-·b = BoundedPropCompletion ℕ≤·

  open OrderedCommMonoidStr (snd ℕ≤+)
    renaming (_·_ to _+ℕ_; ·IdR to +IdR; ·Comm to ℕ+Comm)
  open OrderedCommMonoidStr (snd ℕ↑-+b)
    renaming (_·_ to _+_; ε to 0↑)

  open OrderedCommMonoidStr (snd ℕ↑-·b)
    using (_·_)

  open PropCompletion ℓ-zero ℕ≤+
    using (typeAt; pathFromImplications)

  ℕ↑b : Type₁
  ℕ↑b = fst ℕ↑-+b

  AnnihilL : (x : ℕ↑b) → 0↑ · x ≡ 0↑
  AnnihilL x =
    Σ≡Prop (λ s → PropCompletion.isPropIsBounded ℓ-zero ℕ≤+ s)
           (pathFromImplications (fst (0↑ · x)) (fst 0↑) (⇒) ⇐)
    where
     ⇒ : (n : ℕ) → typeAt n (fst (0↑ · x)) → typeAt n (fst 0↑)
     ⇒ n _ = n , ℕ+Comm n 0
     ⇐ : (n : ℕ) → typeAt n (fst 0↑) → typeAt n (fst (0↑ · x))
     ⇐ n _ =
       PT.rec
         isPropPropTrunc
         (λ {(m , mIsUpperBound) → ∣ (0 , m) , ((0 , refl) , (mIsUpperBound , n ,  +IdR n)) ∣₁})
         (snd x)

  asCommSemiring : CommSemiring (ℓ-suc ℓ-zero)
  fst asCommSemiring = ℕ↑b
  CommSemiringStr.0r (snd asCommSemiring) = 0↑
  CommSemiringStr.1r (snd asCommSemiring) = OrderedCommMonoidStr.ε (snd ℕ↑-·b)
  CommSemiringStr._+_ (snd asCommSemiring) = _+_
  CommSemiringStr._·_ (snd asCommSemiring) = _·_
  IsCommSemiring.+IsCommMonoid (CommSemiringStr.isCommSemiring (snd asCommSemiring)) =
    OrderedCommMonoidStr.isCommMonoid (snd ℕ↑-+b)
  IsCommSemiring.·IsCommMonoid (CommSemiringStr.isCommSemiring (snd asCommSemiring)) =
    OrderedCommMonoidStr.isCommMonoid (snd ℕ↑-·b)
  IsCommSemiring.·LDist+ (CommSemiringStr.isCommSemiring (snd asCommSemiring)) =
    λ x y z → Σ≡Prop (λ s → PropCompletion.isPropIsBounded ℓ-zero ℕ≤+ s)
                     (ConstructionUnbounded.+LDist· (fst x) (fst y) (fst z))
  IsCommSemiring.AnnihilL (CommSemiringStr.isCommSemiring (snd asCommSemiring)) = AnnihilL


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

open import HoTT

{- Proof that if [A] and [B] are two propositions, then so is [A * B]. -}

module homotopy.PropJoinProp
  {i} (A : Type i) {pA : (a a' : A) → a == a'}
  {j} (B : Type j) {pB : (b b' : B) → b == b'} where

{-
We first prove that [left a == y] for all [a : A] and [y : A * B].
For that we will need the coherence condition [coh1] below.
-}

eq-left : (a : A) (y : A * B) → left a == y
eq-left = EqLeft.f  module M where

  coh1 : {b' : B} {a a' : A} (p : a == a')
    → ap left p ∙ glue (a' , b') == glue (a , b') :> (left a == right b' :> A * B)
  coh1 idp = idp

  module EqLeft (a : A) =
    PushoutElim (λ a' → ap left (pA a a'))
                (λ b' → glue (a , b'))
                (λ {(a' , b') → ↓-cst=idf-in (coh1 (pA a a'))})

open M

{-
Now we prove that [right b == y] for all [b : B] and [y : A * B].
We will again need some coherence condition [coh2].
-}

eq-right : (b : B) (y : A * B) → right b == y
eq-right = EqRight.f  module M' where

  coh2 : {a' : A} {b b' : B} (p : b == b')
    → ! (glue (a' , b)) ∙ glue (a' , b') == ap right p :> (right b == right b' :> A * B)
  coh2 idp = !-inv-l (glue _)

  module EqRight (b : B) =
    PushoutElim (λ a' → ! (glue (a' , b)))
                (λ b' → ap right (pB b b'))
                (λ {(a' , b') → ↓-cst=idf-in (coh2 (pB b b'))})

open M'

{-
Then we prove the missing cases.
For the cases [x == left a'] and [x == right b'] we will need the coherence
conditions [coh3] and [coh4].
For the last case, we need a "2-dimensional" coherence condition [coh²],
relating [coh1], [coh2], [coh3] and [coh4].
-}

eq : (x y : A * B) → x == y
eq = Pushout-elim eq-left eq-right
       (λ {(a , b) → ↓-cst→app-in (Pushout-elim (λ a' → ↓-idf=cst-in (coh3 (pA a a')))
                                                (λ b' → ↓-idf=cst-in (coh4 (pB b b')))
                                                (λ {(a' , b') → ↓-idf=cst-in=↓ (↓-=-in
   (coh3 (pA a a') ◃ apd (λ x → glue (a , b) ∙' eq-right b x) (glue (a' , b'))
          =⟨ apd∙' (λ x → glue (a , b)) (eq-right b) (glue (a' , b')) |in-ctx (λ u → coh3 (pA a a') ◃ u) ⟩
    coh3 (pA a a') ◃ (apd (λ x → glue (a , b)) (glue (a' , b')) ∙'2ᵈ apd (eq-right b) (glue (a' , b')))
          =⟨ EqRight.glue-β b (a' , b') |in-ctx (λ u → coh3 (pA a a') ◃ (apd (λ x → glue (a , b)) (glue (a' , b')) ∙'2ᵈ u)) ⟩
    coh3 (pA a a') ◃ (apd (λ x → glue (a , b)) (glue (a' , b')) ∙'2ᵈ ↓-cst=idf-in {p = glue _} {u = ! (glue _)} (coh2 (pB b b')))
          =⟨ coh² (pA a a') (pB b b') ⟩
    ↓-cst=idf-in (coh1 (pA a a')) ▹ coh4 (pB b b')
          =⟨ ! (EqLeft.glue-β a (a' , b')) |in-ctx (λ u → u ▹ coh4 (pB b b')) ⟩
    apd (eq-left a) (glue (a' , b')) ▹ coh4 (pB b b') ∎))}))})

  where

  coh3 : {b : B} {a a' : A} (p : a == a')
    → ap left p == (glue (a , b) ∙' ! (glue (a' , b))) :> (left a == left a' :> A * B)
  coh3 idp = ! (!-inv-r (glue _)) ∙ ∙=∙' (glue _) (! (glue _))

  coh4 : {a : A} {b b' : B} (p : b == b')
    → glue (a , b') == (glue (a , b) ∙' ap right p) :> (left a == right b' :> A * B)
  coh4 idp = idp

  {- Should go to lib.types.Paths -}
  ↓-idf=cst-in=↓ : ∀ {i} {A : Type i} {a a' : A} {p : a == a'} {a0 a0' : A} {p0 : a0 == a0'} {f : (a : A) → a0 == a} {g : (a : A) → a0' == a}
    {q : f a == p0 ∙' g a } {r : f a' == p0 ∙' g a'}
    → q == r [ (λ a → f a == p0 ∙' g a) ↓ p ]
    → ↓-idf=cst-in q == ↓-idf=cst-in r [ (λ a → f a == g a [ (λ x → x == a) ↓ p0 ]) ↓ p ]
  ↓-idf=cst-in=↓ {p = idp} {p0 = idp} idp = idp

  abstract
    coh² : {a a' : A} {b b' : B} (p : a == a') (q : b == b')
      → coh3 {b = b} p ◃ (apd (λ x → glue (a , b)) (glue (a' , b')) ∙'2ᵈ ↓-cst=idf-in {p = glue (a' , b')} {u = ! (glue (a' , b))} (coh2 q))
        == ↓-cst=idf-in (coh1 p) ▹ coh4 q
    coh² idp idp = aux (glue _)  where

      abstract
        aux : {x y : A * B} (p : x == y) →
              (! (!-inv-r p) ∙ ∙=∙' p (! p))
              ◃
              (apd (λ x → p) p ∙'2ᵈ ↓-cst=idf-in {p = p} {u = ! p} (!-inv-l p))
              == ↓-cst=idf-in idp ▹ idp
        aux idp = idp

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Issue448 where

postulate
 Unit : Set
 unit : Unit
 D    : Set → Set
 d    : (A : Set) → A → D A

record R : Set₁ where
 field F : Set

r : _
r = record { F = Unit }

postulate
 D′ : R.F r → D (R.F r) → Set
 d′ : ∀ f τ → D′ f (d _ τ)

data D″ (f : Unit) : D′ f (d Unit unit) → Set where
  d″ : ∀ (x : Unit) → D″ _ (d′ f unit)

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/MetaVars.hs:583


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Names used in the reflection machinery
------------------------------------------------------------------------

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

module Reflection.Name where

open import Data.List.Base
import Data.Product.Properties as Prodₚ
import Data.Word.Properties as Wₚ
open import Function
open import Relation.Nullary.Decidable using (map′)
open import Relation.Binary
import Relation.Binary.Construct.On as On
open import Relation.Binary.PropositionalEquality

----------------------------------------------------------------------
-- Re-export built-ins

open import Agda.Builtin.Reflection public
  using (Name) renaming (primQNameToWord64s to toWords)

open import Agda.Builtin.Reflection.Properties public
  renaming (primQNameToWord64sInjective to toWords-injective)

----------------------------------------------------------------------
-- More definitions
----------------------------------------------------------------------

Names : Set
Names = List Name

----------------------------------------------------------------------
-- Decidable equality for names
----------------------------------------------------------------------

_≈_ : Rel Name _
_≈_ = _≡_ on toWords

infix 4 _≈?_ _≟_

_≈?_ : Decidable _≈_
_≈?_ = On.decidable toWords _≡_ (Prodₚ.≡-dec Wₚ._≟_ Wₚ._≟_)

_≟_ : DecidableEquality Name
m ≟ n = map′ (toWords-injective _ _) (cong toWords) (m ≈? n)


text:
import Agda.Builtin.FromNat as FromNat -- not opened
open import Agda.Builtin.Nat

-- Since fromNat is not in scope unqualified this should work without
-- a Number instance for Nat.
x : Nat
x = 0

-- Renaming fromNat should not make a difference
open FromNat renaming (fromNat to fromℕ)
open import Agda.Builtin.Unit

data MyNat : Set where
  mkNat : Nat → MyNat

instance
  numMyNat : Number MyNat
  numMyNat .Number.Constraint _ = ⊤
  numMyNat .fromℕ n = mkNat n

y : MyNat
y = 1

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2020-06-23, issue #4773
-- reported by gallais, originally reported on mailing list by mechvel

-- Regression in 2.5.1:
-- import directives applied to modules no longer warn
-- when private names are mentioned

-- {-# OPTIONS -v scope:40 #-}

module _ where

-- MWE:
-------

module M where
  private
    X = Set
    Y = Set
    Z = Set

module N  = M using  (X) renaming (Y to Y') hiding (Z)

-- EXPECTED: warning about X, Y, Z

-- Extended original example, using 'open M args'
-------------------------------------------------

module A (X : Set₁) where
 Y = X

module B (X : Set₁) where
  open A X using (Y)
  private Z = Set

open B Set renaming (Y to Y') renaming (Z to Z')

-- EXPECTED: warning about Y, Z

-- Y' is not in scope
-- test = Y'


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by strict partial orders
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.Properties.StrictTotalOrder
       {s₁ s₂ s₃} (STO : StrictTotalOrder s₁ s₂ s₃)
       where

open Relation.Binary.StrictTotalOrder STO
import Relation.Binary.StrictToNonStrict as Conv
open Conv _≈_ _<_
import Relation.Binary.Properties.StrictPartialOrder as SPO
open import Relation.Binary.Consequences

------------------------------------------------------------------------
-- Strict total orders can be converted to decidable total orders

decTotalOrder : DecTotalOrder _ _ _
decTotalOrder = record
  { isDecTotalOrder = record
    { isTotalOrder = record
      { isPartialOrder = SPO.isPartialOrder strictPartialOrder
      ; total          = total compare
      }
    ; _≟_  = _≟_
    ; _≤?_ = decidable' compare
    }
  }

open DecTotalOrder decTotalOrder public