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

module Data.Nat.Fold where

open import Prelude
open import Data.Nat

foldr-ℕ : (A → A) → A → ℕ → A
foldr-ℕ f b zero = b
foldr-ℕ f b (suc n) = f (foldr-ℕ f b n)

foldr-ℕ-universal : ∀ (h : ℕ → A) f x →
                   (h zero ≡ x) →
                   (∀ n → h (suc n) ≡ f (h n)) →
                   ∀ n → h n ≡ foldr-ℕ f x n
foldr-ℕ-universal h f x base step zero = base
foldr-ℕ-universal h f x base step (suc n) = step n ; cong f (foldr-ℕ-universal h f x base step n)

foldl-ℕ-go : (A → A) → ℕ → A → A
foldl-ℕ-go f zero    x = x
foldl-ℕ-go f (suc n) x = foldl-ℕ-go f n $! f x

foldl-ℕ : (A → A) → A → ℕ → A
foldl-ℕ f x n = foldl-ℕ-go f n $! x
{-# INLINE foldl-ℕ #-}

f-comm : ∀ (f : A → A) x n → f (foldr-ℕ f x n) ≡ foldr-ℕ f (f x) n
f-comm f x zero    i = f x
f-comm f x (suc n) i = f (f-comm f x n i)

foldl-ℕ-foldr : ∀ f (x : A) n → foldr-ℕ f x n ≡ foldl-ℕ f x n
foldl-ℕ-foldr f x zero    = sym ($!-≡ (foldl-ℕ-go f zero) x)
foldl-ℕ-foldr f x (suc n) = f-comm f x n ; foldl-ℕ-foldr f (f x) n ; sym ($!-≡ (foldl-ℕ-go f (suc n)) x)

foldl-ℕ-universal : ∀ (h : ℕ → A) f x →
                   (h zero ≡ x) →
                   (∀ n → h (suc n) ≡ f (h n)) →
                   ∀ n → h n ≡ foldl-ℕ f x n
foldl-ℕ-universal h f x base step n = foldr-ℕ-universal h f x base step n ; foldl-ℕ-foldr f x n

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

module Calf.Prelude where

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite public

Ω = Prop
□ = Set

postulate
  funext : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (a : A) → B a} → (∀ x → f x ≡ g x) → f ≡ g
  funext/Ω : {A : Prop} {B : □} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

ext: agda

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


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

module Data.Binary.FromZeroed where

open import Data.Binary.Definition
open import Prelude

inc-z : 𝔹 → 𝔹
inc-z 0ᵇ = 2ᵇ 0ᵇ
inc-z (1ᵇ xs) = 2ᵇ xs
inc-z (2ᵇ xs) = 1ᵇ inc-z xs

toZ : 𝔹 → 𝔹
toZ 0ᵇ = 0ᵇ
toZ (1ᵇ xs) = 2ᵇ toZ xs
toZ (2ᵇ xs) = 1ᵇ inc-z (toZ xs)

ones : ℕ → 𝔹 → 𝔹
ones zero    xs = xs
ones (suc n) xs = 1ᵇ ones n xs

fromZ₁ : ℕ → 𝔹 → 𝔹
fromZ₁ n 0ᵇ      = 0ᵇ
fromZ₁ n (1ᵇ xs) = fromZ₁ (suc n) xs
fromZ₁ n (2ᵇ xs) = 2ᵇ ones n (fromZ₁ 0 xs)

fromZ : 𝔹 → 𝔹
fromZ 0ᵇ = 0ᵇ
fromZ (1ᵇ xs) = fromZ₁ zero xs
fromZ (2ᵇ xs) = 1ᵇ fromZ xs

import Data.Binary.Conversion.Fast as Fast

open import Data.List using (List; _⋯_; map)

round-trip : ℕ → Type
round-trip n = map (fromZ ∘ toZ) nums ≡ nums
  where
  nums : List 𝔹
  nums = map Fast.⟦_⇑⟧ (0 ⋯ n)

_ : round-trip 300
_ = refl


text:
open import bool
open import bool-thms2
open import eq
open import product
open import product-thms
open import bool-relations

module minmax {A : Set} (_≤A_ : A → A → 𝔹)
              (≤A-trans : transitive _≤A_)
              (≤A-total : total _≤A_) where

≤A-refl : reflexive _≤A_
≤A-refl = total-reflexive _≤A_ ≤A-total

min : A → A → A
min = λ x y → if x ≤A y then x else y

max : A → A → A
max = λ x y → if x ≤A y then y else x

min-≤1 : ∀{x y : A} → min x y ≤A x ≡ tt
min-≤1{x}{y} with keep (x ≤A y)
min-≤1{x}{y} | tt , p rewrite p = ≤A-refl
min-≤1{x}{y} | ff , p rewrite p = ≤A-total p

min-≤2 : ∀{x y : A} → min x y ≤A y ≡ tt
min-≤2{x}{y} with keep (x ≤A y)
min-≤2{x}{y} | tt , p rewrite p = p
min-≤2{x}{y} | ff , p rewrite p = ≤A-refl

max-≤1 : ∀{x y : A} → x ≤A max x y ≡ tt
max-≤1{x}{y} with keep (x ≤A y)
max-≤1{x}{y} | tt , p rewrite p = p
max-≤1{x}{y} | ff , p rewrite p = ≤A-refl

max-≤2 : ∀{x y : A} → y ≤A max x y ≡ tt
max-≤2{x}{y} with keep (x ≤A y)
max-≤2{x}{y} | tt , p rewrite p = ≤A-refl
max-≤2{x}{y} | ff , p rewrite p = ≤A-total p

min1-mono : ∀{x x' y : A} → x ≤A x' ≡ tt → min x y ≤A min x' y ≡ tt
min1-mono{x}{x'}{y} p with keep (x ≤A y) | keep (x' ≤A y)
min1-mono p | tt , q | tt , q' rewrite q | q' = p
min1-mono p | tt , q | ff , q' rewrite q | q' = q
min1-mono p | ff , q | tt , q' rewrite q | q' | ≤A-trans p q' with q
min1-mono p | ff , q | tt , q' | ()
min1-mono p | ff , q | ff , q' rewrite q | q' = ≤A-refl

min2-mono : ∀{x y y' : A} → y ≤A y' ≡ tt → min x y ≤A min x y' ≡ tt
min2-mono{x}{y}{y'} p with keep (x ≤A y) | keep (x ≤A y')
min2-mono p | tt , q | tt , q' rewrite q | q' = ≤A-refl
min2-mono p | tt , q | ff , q' rewrite q | q' | ≤A-trans q p with q'
min2-mono p | tt , q | ff , q' | ()
min2-mono p | ff , q | tt , q' rewrite q | q' = ≤A-total q
min2-mono p | ff , q | ff , q' rewrite q | q' = p

max2-mono : ∀{x y y' : A} → y ≤A y' ≡ tt → max x y ≤A max x y' ≡ tt
max2-mono{x}{y}{y'} p with keep (x ≤A y) | keep (x ≤A y')
max2-mono p | tt , q | tt , q' rewrite q | q' = p
max2-mono p | tt , q | ff , q' rewrite q | q' = ≤A-trans p (≤A-total q')
max2-mono p | ff , q | tt , q' rewrite q | q' = q'
max2-mono p | ff , q | ff , q' rewrite q | q' = ≤A-refl

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module 020-equivalence where

-- We need False to represent logical contradiction.

open import 010-false-true

-- Next, we need to be able to work with equalities. Equalities are
-- defined between objects of the same type. Two objects are equal if
-- we have a proof of their equality. In Agda, we can represent this
-- by means of a function which takes two instances of some type M,
-- and maps this to a proof of equality.

-- To be a reasonable model for equality, we demand that this function
-- has the properties of an equivalence relation: (i) we must have a
-- proof that every object r in M equals itself, (ii) given a proof
-- that r == s, we must be able to prove that s == r, and (iii) given
-- proofs of r == s and s == t, we must be able to prove that r == t.

-- A convenient way to store all these properties, goes by means of a
-- record, which is in essence a local parametrised module, where the
-- parameters and fields correspond to postulates (theorems that can
-- be stated without proof), and declarations are theorems derived
-- from parameters and fields. A good question is, what should be a
-- parameter, and what should be a field? Fields can be considered as
-- named parameters, so probably anything that would otherwise not be
-- obvious without name should go into a field.

-- Here we declare the type and equality function (which maps pairs of
-- elements to proofs) as parameters, and the equivalence axioms as
-- fields. The parameter M is optional because it can be derived
-- unambiguously from the type signature of the equality function.

record Equivalence
  {M : Set}
  (_==_ : M -> M -> Set)
  : Set1 where

  {- axioms -}
  field
    refl : ∀ {r} -> (r == r)
    symm : ∀ {r s} -> (r == s) -> (s == r)
    trans : ∀ {r s t} -> (r == s) -> (s == t) -> (r == t)

  -- We have a proof of inequality if we can prove contradiction from
  -- equality, and this is precisely how we define the inequality
  -- relation.

  _!=_ : M -> M -> Set
  m != n = (m == n) -> False

  -- Prove transitivity chains.
  -- (TODO: Use a type dependent function for these chains.)
  trans3 : ∀ {r s t u}
           -> (r == s) -> (s == t) -> (t == u) -> (r == u)
  trans3 p1 p2 p3 = trans (trans p1 p2) p3
  trans4 : ∀ {r s t u v}
           -> (r == s) -> (s == t) -> (t == u) -> (u == v) -> (r == v)
  trans4 p1 p2 p3 p4 = trans (trans3 p1 p2 p3) p4
  trans5 : ∀ {r s t u v w}
           -> (r == s) -> (s == t) -> (t == u) -> (u == v) -> (v == w)
           -> (r == w)
  trans5 p1 p2 p3 p4 p5 = trans (trans4 p1 p2 p3 p4) p5
  trans6 : ∀ {r s t u v w x}
           -> (r == s) -> (s == t) -> (t == u) -> (u == v) -> (v == w)
           -> (w == x) -> (r == x)
  trans6 p1 p2 p3 p4 p5 p6 = trans (trans5 p1 p2 p3 p4 p5) p6

-- Now we construct a trivial model of equivalence: two instances of a
-- type are equivalent if they reduce to the same normal form. (Note
-- that Agda reduces expressions to normal form for us.)

data _≡_ {A : Set} : A -> A -> Set where
  refl : ∀ {r} -> r ≡ r

thm-≡-is-equivalence : {A : Set} -> Equivalence {A} _≡_
thm-≡-is-equivalence = record {
  refl = refl;
  symm = symm;
  trans = trans
  }
  where
    symm : ∀ {r s} -> r ≡ s -> s ≡ r
    symm refl = refl
    trans : ∀ {r s t} -> r ≡ s -> s ≡ t -> r ≡ t
    trans refl refl = refl

max_stars_repo_name: mcmtroffaes/agda-proofs

max_issues_repo_name: mcmtroffaes/agda-proofs

max_forks_repo_name: mcmtroffaes/agda-proofs


text:
import Issue2447.M

Rejected : Set
Rejected = Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some Vec-related properties that depend on the K rule or make use
-- of heterogeneous equality
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Vec.Properties.WithK where

open import Data.Nat
open import Data.Nat.Properties using (+-assoc)
open import Data.Vec
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl)

------------------------------------------------------------------------
-- _[_]=_

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

  []=-irrelevant : ∀ {n} {xs : Vec A n} {i x} →
                    (p q : xs [ i ]= x) → p ≡ q
  []=-irrelevant here            here             = refl
  []=-irrelevant (there xs[i]=x) (there xs[i]=x') =
    P.cong there ([]=-irrelevant xs[i]=x xs[i]=x')

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

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

  ++-assoc : ∀ {m n k} (xs : Vec A m) (ys : Vec A n) (zs : Vec A k) →
             (xs ++ ys) ++ zs ≅ xs ++ (ys ++ zs)
  ++-assoc         []       ys zs = refl
  ++-assoc {suc m} (x ∷ xs) ys zs =
    H.icong (Vec A) (+-assoc m _ _) (x ∷_) (++-assoc xs ys zs)

------------------------------------------------------------------------
-- foldr

foldr-cong : ∀ {a b} {A : Set a}
             {B : ℕ → Set b} {f : ∀ {n} → A → B n → B (suc n)} {d}
             {C : ℕ → Set b} {g : ∀ {n} → A → C n → C (suc n)} {e} →
             (∀ {n x} {y : B n} {z : C n} → y ≅ z → f x y ≅ g x z) →
             d ≅ e → ∀ {n} (xs : Vec A n) →
             foldr B f d xs ≅ foldr C g e xs
foldr-cong _   d≅e []       = d≅e
foldr-cong f≅g d≅e (x ∷ xs) = f≅g (foldr-cong f≅g d≅e xs)

------------------------------------------------------------------------
-- foldl

foldl-cong : ∀ {a b} {A : Set a}
             {B : ℕ → Set b} {f : ∀ {n} → B n → A → B (suc n)} {d}
             {C : ℕ → Set b} {g : ∀ {n} → C n → A → C (suc n)} {e} →
             (∀ {n x} {y : B n} {z : C n} → y ≅ z → f y x ≅ g z x) →
             d ≅ e → ∀ {n} (xs : Vec A n) →
             foldl B f d xs ≅ foldl C g e xs
foldl-cong _   d≅e []       = d≅e
foldl-cong f≅g d≅e (x ∷ xs) = foldl-cong f≅g (f≅g d≅e) xs

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

-- Version 1.0

[]=-irrelevance = []=-irrelevant
{-# WARNING_ON_USAGE []=-irrelevance
"Warning: []=-irrelevance was deprecated in v1.0.
Please use []=-irrelevant instead."
#-}


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

module 17-number-theory where

import 16-sets
open 16-sets public

-- Section 10.1 Decidability.

{- Recall that a proposition P is decidable if P + (¬ P) holds. -}

classical-Prop :
  (l : Level) → UU (lsuc l)
classical-Prop l = Σ (UU-Prop l) (λ P → is-decidable (pr1 P))

is-decidable-leq-ℕ :
  (m n : ℕ) → is-decidable (leq-ℕ m n)
is-decidable-leq-ℕ zero-ℕ zero-ℕ = inl star
is-decidable-leq-ℕ zero-ℕ (succ-ℕ n) = inl star
is-decidable-leq-ℕ (succ-ℕ m) zero-ℕ = inr id
is-decidable-leq-ℕ (succ-ℕ m) (succ-ℕ n) = is-decidable-leq-ℕ m n

is-decidable-le-ℕ :
  (m n : ℕ) → is-decidable (le-ℕ m n)
is-decidable-le-ℕ zero-ℕ zero-ℕ = inr id
is-decidable-le-ℕ zero-ℕ (succ-ℕ n) = inl star
is-decidable-le-ℕ (succ-ℕ m) zero-ℕ = inr id
is-decidable-le-ℕ (succ-ℕ m) (succ-ℕ n) = is-decidable-le-ℕ m n

{- We show that if A is a proposition, then so is is-decidable A. -}

is-prop-is-decidable :
  {l : Level} {A : UU l} → is-prop A → is-prop (is-decidable A)
is-prop-is-decidable is-prop-A =
  is-prop-coprod intro-dn is-prop-A is-prop-neg

{- Not every type is decidable. -}

case-elim :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  ¬ B → coprod A B → A
case-elim nb (inl a) = a
case-elim nb (inr b) = ex-falso (nb b)

simplify-not-all-2-element-types-decidable :
  {l : Level} →
  ((X : UU l) (p : type-trunc-Prop (bool ≃ X)) → is-decidable X) →
  ((X : UU l) (p : type-trunc-Prop (bool ≃ X)) → X)
simplify-not-all-2-element-types-decidable d X p =
  case-elim
    ( map-universal-property-trunc-Prop
      ( dn-Prop' X)
      ( λ e → intro-dn (map-equiv e true))
      ( p))
    ( d X p)

{-
not-all-2-element-types-decidable :
  {l : Level} → ¬ ((X : UU l) (p : type-trunc-Prop (bool ≃ X)) → is-decidable X)
not-all-2-element-types-decidable d = {!simplify-not-all-2-element-types-decidable d (raise _ bool) ?!}

not-all-types-decidable :
  {l : Level} → ¬ ((X : UU l) → is-decidable X)
not-all-types-decidable d =
  not-all-2-element-types-decidable (λ X p → d X)
-}

{- Types with decidable equality are closed under coproducts. -}

has-decidable-equality-coprod : {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  has-decidable-equality A → has-decidable-equality B →
  has-decidable-equality (coprod A B)
has-decidable-equality-coprod dec-A dec-B (inl x) (inl y) =
  functor-coprod
    ( ap inl)
    ( λ f p → f (inv-is-equiv (is-emb-inl _ _ x y) p))
    ( dec-A x y)
has-decidable-equality-coprod {A = A} {B = B} dec-A dec-B (inl x) (inr y) =
  inr
    ( λ p →
      inv-is-equiv
        ( is-equiv-map-raise _ empty)
        ( Eq-coprod-eq A B (inl x) (inr y) p))
has-decidable-equality-coprod {A = A} {B = B} dec-A dec-B (inr x) (inl y) =
  inr
    ( λ p →
      inv-is-equiv
        ( is-equiv-map-raise _ empty)
        ( Eq-coprod-eq A B (inr x) (inl y) p))
has-decidable-equality-coprod dec-A dec-B (inr x) (inr y) =
  functor-coprod
    ( ap inr)
    ( λ f p → f (inv-is-equiv (is-emb-inr _ _ x y) p))
    ( dec-B x y)

{- Decidable equality of Fin n. -}

has-decidable-equality-empty : has-decidable-equality empty
has-decidable-equality-empty ()

has-decidable-equality-unit :
  has-decidable-equality unit
has-decidable-equality-unit star star = inl refl

has-decidable-equality-Fin :
  (n : ℕ) → has-decidable-equality (Fin n)
has-decidable-equality-Fin zero-ℕ = has-decidable-equality-empty
has-decidable-equality-Fin (succ-ℕ n) =
  has-decidable-equality-coprod
    ( has-decidable-equality-Fin n)
    ( has-decidable-equality-unit)

decidable-Eq-Fin :
  (n : ℕ) (i j : Fin n) → classical-Prop lzero
decidable-Eq-Fin n i j =
  pair
    ( pair (Id i j) (is-set-Fin n i j))
    ( has-decidable-equality-Fin n i j)

{- Decidable equality of ℤ. -}

has-decidable-equality-ℤ : has-decidable-equality ℤ
has-decidable-equality-ℤ =
  has-decidable-equality-coprod
    has-decidable-equality-ℕ
    ( has-decidable-equality-coprod
      has-decidable-equality-unit
      has-decidable-equality-ℕ)

{- Next, we show that types with decidable equality are sets. To see this, we
   will construct a fiberwise equivalence with the binary relation R that is
   defined by R x y := unit if (x = y), and empty otherwise. In order to define
   this relation, we first define a type family over ((x = y) + ¬(x = y)) that
   returns unit on the left and empty on the right. -}

splitting-decidable-equality : {l : Level} (A : UU l) (x y : A) →
  is-decidable (Id x y) → UU lzero
splitting-decidable-equality A x y (inl p) = unit
splitting-decidable-equality A x y (inr f) = empty

is-prop-splitting-decidable-equality : {l : Level} (A : UU l) (x y : A) →
  (t : is-decidable (Id x y)) →
  is-prop (splitting-decidable-equality A x y t)
is-prop-splitting-decidable-equality A x y (inl p) = is-prop-unit
is-prop-splitting-decidable-equality A x y (inr f) = is-prop-empty

reflexive-splitting-decidable-equality : {l : Level} (A : UU l) (x : A) →
  (t : is-decidable (Id x x)) → splitting-decidable-equality A x x t
reflexive-splitting-decidable-equality A x (inl p) = star
reflexive-splitting-decidable-equality A x (inr f) =
  ind-empty {P = λ t → splitting-decidable-equality A x x (inr f)} (f refl)

eq-splitting-decidable-equality : {l : Level} (A : UU l) (x y : A) →
  (t : is-decidable (Id x y)) →
  splitting-decidable-equality A x y t → Id x y
eq-splitting-decidable-equality A x y (inl p) t = p
eq-splitting-decidable-equality A x y (inr f) t =
  ind-empty {P = λ s → Id x y} t

is-set-has-decidable-equality : {l : Level} (A : UU l) →
  has-decidable-equality A → is-set A
is-set-has-decidable-equality A d =
  is-set-prop-in-id
    ( λ x y → splitting-decidable-equality A x y (d x y))
    ( λ x y → is-prop-splitting-decidable-equality A x y (d x y))
    ( λ x → reflexive-splitting-decidable-equality A x (d x x))
    ( λ x y → eq-splitting-decidable-equality A x y (d x y))

{- Closure of decidable types under retracts and equivalences. -}

is-decidable-retract-of :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  A retract-of B → is-decidable B → is-decidable A
is-decidable-retract-of (pair i (pair r H)) (inl b) = inl (r b)
is-decidable-retract-of (pair i (pair r H)) (inr f) = inr (f ∘ i)

is-decidable-is-equiv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
  (is-equiv-f : is-equiv f) → is-decidable B → is-decidable A
is-decidable-is-equiv {f = f} (pair (pair g G) (pair h H)) =
  is-decidable-retract-of (pair f (pair h H))

is-decidable-equiv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) →
  is-decidable B → is-decidable A
is-decidable-equiv e = is-decidable-is-equiv (is-equiv-map-equiv e)

is-decidable-equiv' :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) →
  is-decidable A → is-decidable B
is-decidable-equiv' e = is-decidable-equiv (inv-equiv e)

has-decidable-equality-retract-of :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  A retract-of B → has-decidable-equality B → has-decidable-equality A
has-decidable-equality-retract-of (pair i (pair r H)) d x y =
  is-decidable-retract-of
    ( Id-retract-of-Id (pair i (pair r H)) x y)
    ( d (i x) (i y))

{- The well-ordering principle. -}

is-minimal-element-ℕ :
  {l : Level} (P : ℕ → UU l) (n : ℕ) (p : P n) → UU l
is-minimal-element-ℕ P n p =
  (m : ℕ) → P m → (leq-ℕ n m)

minimal-element-ℕ :
  {l : Level} (P : ℕ → UU l) → UU l
minimal-element-ℕ P = Σ ℕ (λ n → Σ (P n) (is-minimal-element-ℕ P n))

is-minimal-element-succ-ℕ :
  {l : Level} (P : ℕ → UU l) (d : (n : ℕ) → is-decidable (P n))
  (m : ℕ) (pm : P (succ-ℕ m))
  (is-min-m : is-minimal-element-ℕ (λ x → P (succ-ℕ x)) m pm) →
  ¬ (P zero-ℕ) → is-minimal-element-ℕ P (succ-ℕ m) pm
is-minimal-element-succ-ℕ P d m pm is-min-m neg-p0 zero-ℕ p0 =
  ind-empty (neg-p0 p0)
is-minimal-element-succ-ℕ P d zero-ℕ pm is-min-m neg-p0 (succ-ℕ n) psuccn =
  leq-zero-ℕ n
is-minimal-element-succ-ℕ P d (succ-ℕ m) pm is-min-m neg-p0 (succ-ℕ n) psuccn =
  is-minimal-element-succ-ℕ (λ x → P (succ-ℕ x)) (λ x → d (succ-ℕ x)) m pm
    ( λ m → is-min-m (succ-ℕ m))
    ( is-min-m zero-ℕ)
    ( n)
    ( psuccn)

well-ordering-principle-succ-ℕ :
  {l : Level} (P : ℕ → UU l) (d : (n : ℕ) → is-decidable (P n))
  (n : ℕ) (p : P (succ-ℕ n)) →
  is-decidable (P zero-ℕ) →
  minimal-element-ℕ (λ m → P (succ-ℕ m)) → minimal-element-ℕ P
well-ordering-principle-succ-ℕ P d n p (inl p0) _ =
  pair zero-ℕ (pair p0 (λ m q → leq-zero-ℕ m))
well-ordering-principle-succ-ℕ P d n p
  (inr neg-p0) (pair m (pair pm is-min-m)) =
  pair
    ( succ-ℕ m)
    ( pair pm
      ( is-minimal-element-succ-ℕ P d m pm is-min-m neg-p0))

well-ordering-principle-ℕ :
  {l : Level} (P : ℕ → UU l) (d : (n : ℕ) → is-decidable (P n)) →
  Σ ℕ P → minimal-element-ℕ P
well-ordering-principle-ℕ P d (pair zero-ℕ p) =
  pair zero-ℕ (pair p (λ m q → leq-zero-ℕ m))
well-ordering-principle-ℕ P d (pair (succ-ℕ n) p) =
  well-ordering-principle-succ-ℕ P d n p (d zero-ℕ)
    ( well-ordering-principle-ℕ
      ( λ m → P (succ-ℕ m))
      ( λ m → d (succ-ℕ m))
      ( pair n p))

-- Exercise 6.7

-- We prove that the induction principle for ℕ implies strong induction.

-- We first prove some lemmas about inequality.

is-prop-leq-ℕ :
  (m n : ℕ) → is-prop (leq-ℕ m n)
is-prop-leq-ℕ zero-ℕ zero-ℕ = is-prop-unit
is-prop-leq-ℕ zero-ℕ (succ-ℕ n) = is-prop-unit
is-prop-leq-ℕ (succ-ℕ m) zero-ℕ = is-prop-empty
is-prop-leq-ℕ (succ-ℕ m) (succ-ℕ n) = is-prop-leq-ℕ m n

neg-succ-leq-ℕ :
  (n : ℕ) → ¬ (leq-ℕ (succ-ℕ n) n)
neg-succ-leq-ℕ zero-ℕ = id
neg-succ-leq-ℕ (succ-ℕ n) = neg-succ-leq-ℕ n

leq-eq-left-ℕ :
  {m m' : ℕ} → Id m m' → (n : ℕ) → leq-ℕ m n → leq-ℕ m' n
leq-eq-left-ℕ refl n = id

leq-eq-right-ℕ :
  (m : ℕ) {n n' : ℕ} → Id n n' → leq-ℕ m n → leq-ℕ m n'
leq-eq-right-ℕ m refl = id

-- Now we begin with the proof of the theorem

fam-strong-ind-ℕ :
  { l : Level} → (ℕ → UU l) → ℕ → UU l
fam-strong-ind-ℕ P n = (m : ℕ) → (leq-ℕ m n) → P m

-- We first take care of the zero case, with appropriate computation rule.

zero-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) → P zero-ℕ → fam-strong-ind-ℕ P zero-ℕ
zero-strong-ind-ℕ P p0 zero-ℕ t = p0
zero-strong-ind-ℕ P p0 (succ-ℕ m) ()

eq-zero-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) (p0 : P zero-ℕ) (t : leq-ℕ zero-ℕ zero-ℕ) →
  Id (zero-strong-ind-ℕ P p0 zero-ℕ t) p0
eq-zero-strong-ind-ℕ P p0 t = refl

-- Next, we take care of the successor case, with appropriate computation rule.

{- In the successor case, we need to define a map

   fam-strong-ind-ℕ P k → fam-strong-ind-ℕ P (succ-ℕ k).

   The dependent function in the codomain is defined by case analysis, where
   the cases are that either m ≤ k or m = k+1.
   -}

-- We use the following definition to get a map (m≤k+1) → coprod (m≤k) (m=k+1).

cases-leq-succ-ℕ :
  {m n : ℕ} → leq-ℕ m (succ-ℕ n) → coprod (leq-ℕ m n) (Id m (succ-ℕ n))
cases-leq-succ-ℕ {zero-ℕ} {n} star = inl star
cases-leq-succ-ℕ {succ-ℕ m} {zero-ℕ} p =
  inr (ap succ-ℕ (anti-symmetric-leq-ℕ m zero-ℕ p star))
cases-leq-succ-ℕ {succ-ℕ m} {succ-ℕ n} p =
  functor-coprod id (ap succ-ℕ) (cases-leq-succ-ℕ p)

cases-succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( (n : ℕ) → (fam-strong-ind-ℕ P n) → P (succ-ℕ n)) →
  ( n : ℕ) (H : fam-strong-ind-ℕ P n) →
  ( m : ℕ) ( c : coprod (leq-ℕ m n) (Id m (succ-ℕ n))) → P m
cases-succ-strong-ind-ℕ P pS n H m (inl q) = H m q
cases-succ-strong-ind-ℕ P pS n H .(succ-ℕ n) (inr refl) = pS n H

succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  ( k : ℕ) → (fam-strong-ind-ℕ P k) → (fam-strong-ind-ℕ P (succ-ℕ k))
succ-strong-ind-ℕ P pS k H m p =
  cases-succ-strong-ind-ℕ P pS k H m (cases-leq-succ-ℕ p)

-- We use a similar case analysis to obtain the computation rule.

{-
exclusive-coprod-leq-eq-succ-ℕ :
  (m n : ℕ) → leq-ℕ m n → ¬ (Id m (succ-ℕ n))
exclusive-coprod-leq-eq-succ-ℕ zero-ℕ zero-ℕ star = {!Eq-eq-ℕ!}
exclusive-coprod-leq-eq-succ-ℕ zero-ℕ (succ-ℕ n) p = {!!}
exclusive-coprod-leq-eq-succ-ℕ (succ-ℕ m) (succ-ℕ n) p = {!!}

is-prop'-coprod-leq-eq-succ :
  (m n : ℕ) → is-prop' (coprod (leq-ℕ m n) (Id m (succ-ℕ n)))
is-prop'-coprod-leq-eq-succ m n =
  is-prop'-exclusive-coprod
    ( exclusive-coprod-leq-eq-succ-ℕ m n)
    ( is-prop'-is-prop (is-prop-leq-ℕ m n))
    ( is-prop'-is-prop (is-set-ℕ m (succ-ℕ n)))

tr-eq-succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k))
  ( n : ℕ) (H : fam-strong-ind-ℕ P n)
  ( m : ℕ) (p : leq-ℕ m (succ-ℕ n))
  ( x : coprod (leq-ℕ m n) (Id m (succ-ℕ n))) (y : P m) →
  Id (succ-strong-ind-ℕ P pS n H m p) y →
  Id (cases-succ-strong-ind-ℕ P pS n H m x) y
tr-eq-succ-strong-ind-ℕ P pS n H m p x y =
  tr ( λ t → Id (cases-succ-strong-ind-ℕ P pS n H m t) y)
     ( is-prop'-coprod-leq-eq-succ m n (cases-leq-succ-ℕ p) x)
-}

cases-htpy-succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  ( k : ℕ) (H : fam-strong-ind-ℕ P k) (m : ℕ)
  ( c : coprod (leq-ℕ m k) (Id m (succ-ℕ k))) →
  ( q : leq-ℕ m k) →
  Id
    ( cases-succ-strong-ind-ℕ P pS k H m c)
    ( H m q)
cases-htpy-succ-strong-ind-ℕ P pS k H m (inl p) q =
  ap (H m) (is-prop'-is-prop (is-prop-leq-ℕ m k) p q)
cases-htpy-succ-strong-ind-ℕ P pS k H m (inr α) q =
  ex-falso
    ( neg-succ-leq-ℕ k (leq-eq-left-ℕ α k q))

htpy-succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  ( k : ℕ) (H : fam-strong-ind-ℕ P k) (m : ℕ)
  ( p : leq-ℕ m (succ-ℕ k)) →
  ( q : leq-ℕ m k) →
  Id
    ( succ-strong-ind-ℕ P pS k H m p)
    ( H m q)
htpy-succ-strong-ind-ℕ P pS k H m p q =
  cases-htpy-succ-strong-ind-ℕ P pS k H m (cases-leq-succ-ℕ p) q

cases-eq-succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  ( k : ℕ) (H : fam-strong-ind-ℕ P k)
  ( c : coprod (leq-ℕ (succ-ℕ k) k) (Id (succ-ℕ k) (succ-ℕ k))) →
  Id ( (cases-succ-strong-ind-ℕ P pS k H (succ-ℕ k) c))
     ( pS k H)
cases-eq-succ-strong-ind-ℕ P pS k H (inl p) = ex-falso (neg-succ-leq-ℕ k p)
cases-eq-succ-strong-ind-ℕ P pS k H (inr α) =
  ap ( (cases-succ-strong-ind-ℕ P pS k H (succ-ℕ k)) ∘ inr)
     ( is-prop'-is-prop (is-set-ℕ (succ-ℕ k) (succ-ℕ k)) α refl)

eq-succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  ( k : ℕ) (H : fam-strong-ind-ℕ P k)
  ( p : leq-ℕ (succ-ℕ k) (succ-ℕ k)) →
  Id ( (succ-strong-ind-ℕ P pS k H (succ-ℕ k) p))
     ( pS k H)
eq-succ-strong-ind-ℕ P pS k H p =
  cases-eq-succ-strong-ind-ℕ P pS k H (cases-leq-succ-ℕ p)

{- Now that we have the base case and inductive step covered, we can proceed
   by induction. -}

induction-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( fam-strong-ind-ℕ P zero-ℕ) →
  ( (k : ℕ) → (fam-strong-ind-ℕ P k) → (fam-strong-ind-ℕ P (succ-ℕ k))) →
  ( n : ℕ) → fam-strong-ind-ℕ P n
induction-strong-ind-ℕ P q0 qS zero-ℕ = q0
induction-strong-ind-ℕ P q0 qS (succ-ℕ n) =
  qS n (induction-strong-ind-ℕ P q0 qS n)

computation-succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( q0 : fam-strong-ind-ℕ P zero-ℕ) →
  ( qS : (k : ℕ) → (fam-strong-ind-ℕ P k) → (fam-strong-ind-ℕ P (succ-ℕ k))) →
  ( n : ℕ) →
  Id ( induction-strong-ind-ℕ P q0 qS (succ-ℕ n))
     ( qS n (induction-strong-ind-ℕ P q0 qS n))
computation-succ-strong-ind-ℕ P q0 qS n = refl

{- However, to obtain the conclusion we need to make one more small step. -}

conclusion-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( ( n : ℕ) → fam-strong-ind-ℕ P n) → (n : ℕ) → P n
conclusion-strong-ind-ℕ P f n = f n n (reflexive-leq-ℕ n)

{- We are finally ready to put things together and define strong-ind-ℕ. -}

strong-ind-ℕ :
  { l : Level} → (P : ℕ → UU l) (p0 : P zero-ℕ) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  ( n : ℕ) → P n
strong-ind-ℕ P p0 pS =
  conclusion-strong-ind-ℕ P
    ( induction-strong-ind-ℕ P
      ( zero-strong-ind-ℕ P p0)
      ( succ-strong-ind-ℕ P pS))

{- The computation rule for the base case holds by definition. -}

comp-zero-strong-ind-ℕ :
  { l : Level} → (P : ℕ → UU l) (p0 : P zero-ℕ) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  Id (strong-ind-ℕ P p0 pS zero-ℕ) p0
comp-zero-strong-ind-ℕ P p0 pS = refl

{- For the computation rule of the inductive step, we use our hard work. -}

cases-leq-succ-reflexive-leq-ℕ :
  {n : ℕ} → Id (cases-leq-succ-ℕ {succ-ℕ n} {n} (reflexive-leq-ℕ n)) (inr refl)
cases-leq-succ-reflexive-leq-ℕ {zero-ℕ} = refl
cases-leq-succ-reflexive-leq-ℕ {succ-ℕ n} =
  ap (functor-coprod id (ap succ-ℕ)) cases-leq-succ-reflexive-leq-ℕ

cases-eq-comp-succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) (p0 : P zero-ℕ) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  ( n : ℕ) →
  ( α :
    ( m : ℕ) (p : leq-ℕ m n) →
    Id ( induction-strong-ind-ℕ P (zero-strong-ind-ℕ P p0)
         ( λ k z m₁ z₁ →
           cases-succ-strong-ind-ℕ P pS k z m₁ (cases-leq-succ-ℕ z₁))
         n m p)
     ( strong-ind-ℕ P p0 pS m)) →
  ( m : ℕ) (p : leq-ℕ m (succ-ℕ n)) →
  ( q : coprod (leq-ℕ m n) (Id m (succ-ℕ n))) →
  Id ( succ-strong-ind-ℕ P pS n
       ( induction-strong-ind-ℕ P
         ( zero-strong-ind-ℕ P p0)
         ( succ-strong-ind-ℕ P pS) n) m p)
     ( strong-ind-ℕ P p0 pS m)
cases-eq-comp-succ-strong-ind-ℕ P p0 pS n α m p (inl x) =
  ( htpy-succ-strong-ind-ℕ P pS n
    ( induction-strong-ind-ℕ P
      ( zero-strong-ind-ℕ P p0)
      ( succ-strong-ind-ℕ P pS) n)
    m p x) ∙
  ( α m x)
cases-eq-comp-succ-strong-ind-ℕ P p0 pS n α .(succ-ℕ n) p (inr refl) =
  ( eq-succ-strong-ind-ℕ P pS n
    ( induction-strong-ind-ℕ P
      ( zero-strong-ind-ℕ P p0)
      ( succ-strong-ind-ℕ P pS) n)
    ( p)) ∙
  ( inv
    ( ap
      ( cases-succ-strong-ind-ℕ P pS n
        ( induction-strong-ind-ℕ P
          ( zero-strong-ind-ℕ P p0)
          ( λ k H m p₁ →
            cases-succ-strong-ind-ℕ P pS k H m (cases-leq-succ-ℕ p₁))
          n)
        ( succ-ℕ n))
       cases-leq-succ-reflexive-leq-ℕ))

eq-comp-succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) (p0 : P zero-ℕ) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  ( n : ℕ) →
  ( m : ℕ) (p : leq-ℕ m n) →
  Id ( induction-strong-ind-ℕ P (zero-strong-ind-ℕ P p0)
       ( λ k z m₁ z₁ →
         cases-succ-strong-ind-ℕ P pS k z m₁ (cases-leq-succ-ℕ z₁))
       n m p)
     ( strong-ind-ℕ P p0 pS m)
eq-comp-succ-strong-ind-ℕ P p0 pS zero-ℕ zero-ℕ star = refl
eq-comp-succ-strong-ind-ℕ P p0 pS zero-ℕ (succ-ℕ m) ()
eq-comp-succ-strong-ind-ℕ P p0 pS (succ-ℕ n) m p =
  cases-eq-comp-succ-strong-ind-ℕ P p0 pS n
    ( eq-comp-succ-strong-ind-ℕ P p0 pS n) m p
    ( cases-leq-succ-ℕ p)

comp-succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) (p0 : P zero-ℕ) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  ( n : ℕ) →
  Id (strong-ind-ℕ P p0 pS (succ-ℕ n)) (pS n (λ m p → strong-ind-ℕ P p0 pS m))
comp-succ-strong-ind-ℕ P p0 pS n =
  ( eq-succ-strong-ind-ℕ P pS n
    ( induction-strong-ind-ℕ P
      ( zero-strong-ind-ℕ P p0)
      ( succ-strong-ind-ℕ P pS)
      ( n))
    ( reflexive-leq-ℕ n)) ∙
  ( ap ( pS n)
       ( eq-htpy
         ( λ m → eq-htpy
           ( λ p → eq-comp-succ-strong-ind-ℕ P p0 pS n m p))))

total-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) (p0 : P zero-ℕ) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  Σ ( (n : ℕ) → P n)
    ( λ h →
      ( Id (h zero-ℕ) p0) ×
      ( (n : ℕ) → Id (h (succ-ℕ n)) (pS n (λ m p → h m))))
total-strong-ind-ℕ P p0 pS =
  pair
    ( strong-ind-ℕ P p0 pS)
    ( pair
      ( comp-zero-strong-ind-ℕ P p0 pS)
      ( comp-succ-strong-ind-ℕ P p0 pS))

-- The Euclidean algorithm

subtract-ℕ : ℕ → ℕ → ℕ
subtract-ℕ zero-ℕ zero-ℕ = zero-ℕ
subtract-ℕ zero-ℕ (succ-ℕ b) = zero-ℕ
subtract-ℕ (succ-ℕ a) zero-ℕ = succ-ℕ a
subtract-ℕ (succ-ℕ a) (succ-ℕ b) = subtract-ℕ a b

leq-subtract-ℕ : (a b : ℕ) → leq-ℕ (subtract-ℕ a b) a
leq-subtract-ℕ zero-ℕ zero-ℕ = star
leq-subtract-ℕ zero-ℕ (succ-ℕ b) = star
leq-subtract-ℕ (succ-ℕ a) zero-ℕ = reflexive-leq-ℕ a
leq-subtract-ℕ (succ-ℕ a) (succ-ℕ b) =
  transitive-leq-ℕ (subtract-ℕ a b) a (succ-ℕ a)
    ( leq-subtract-ℕ a b)
    ( succ-leq-ℕ a)

decide-order-ℕ : (a b : ℕ) → coprod (leq-ℕ b a) (le-ℕ a b)
decide-order-ℕ zero-ℕ zero-ℕ = inl star
decide-order-ℕ zero-ℕ (succ-ℕ b) = inr star
decide-order-ℕ (succ-ℕ a) zero-ℕ = inl star
decide-order-ℕ (succ-ℕ a) (succ-ℕ b) = decide-order-ℕ a b

cases-gcd-euclid :
  ( a b : ℕ)
  ( F : (x : ℕ) (p : leq-ℕ x a) → ℕ → ℕ)
  ( G : (y : ℕ) (q : leq-ℕ y b) → ℕ) →
  ( coprod (leq-ℕ b a) (le-ℕ a b)) → ℕ
cases-gcd-euclid a b F G (inl t) =
  F (subtract-ℕ a b) (leq-subtract-ℕ a b) (succ-ℕ b)
cases-gcd-euclid a b F G (inr t) =
  G (subtract-ℕ b a) (leq-subtract-ℕ b a)

succ-gcd-euclid : (a : ℕ) (F : (x : ℕ) → (leq-ℕ x a) → ℕ → ℕ) → ℕ → ℕ
succ-gcd-euclid a F =
  strong-ind-ℕ
    ( λ x → ℕ)
    ( succ-ℕ a)
    ( λ b G →
      ind-coprod
        { A = leq-ℕ b a}
        { B = le-ℕ a b}
        ( λ x → ℕ)
        ( λ t → F (subtract-ℕ a b) (leq-subtract-ℕ a b) (succ-ℕ b))
        ( λ t → G (subtract-ℕ b a) (leq-subtract-ℕ b a))
        ( decide-order-ℕ a b))

comp-zero-succ-gcd-euclid :
  (a : ℕ) (F : (x : ℕ) → (leq-ℕ x a) → ℕ → ℕ) →
  Id (succ-gcd-euclid a F zero-ℕ) (succ-ℕ a)
comp-zero-succ-gcd-euclid a F =
  comp-zero-strong-ind-ℕ
    ( λ x → ℕ)
    ( succ-ℕ a)
    ( λ b G →
      ind-coprod
        { A = leq-ℕ b a}
        { B = le-ℕ a b}
        ( λ x → ℕ)
        ( λ t → F (subtract-ℕ a b) (leq-subtract-ℕ a b) (succ-ℕ b))
        ( λ t → G (subtract-ℕ b a) (leq-subtract-ℕ b a))
        ( decide-order-ℕ a b))

comp-succ-succ-gcd-euclid :
  (a : ℕ) (F : (x : ℕ) → (leq-ℕ x a) → ℕ → ℕ) (b : ℕ) →
  Id (succ-gcd-euclid a F (succ-ℕ b))
     ( ind-coprod
       { A = leq-ℕ b a}
       { B = le-ℕ a b}
       ( λ x → ℕ)
       ( λ t → F (subtract-ℕ a b) (leq-subtract-ℕ a b) (succ-ℕ b))
       ( λ t → succ-gcd-euclid a F (subtract-ℕ b a))
       ( decide-order-ℕ a b))
comp-succ-succ-gcd-euclid a F b =
  comp-succ-strong-ind-ℕ
    ( λ x → ℕ)
    ( succ-ℕ a)
    ( λ k z →
         ind-coprod (λ _ → ℕ)
         (λ x → F (subtract-ℕ a k) (leq-subtract-ℕ a k) (succ-ℕ k))
         (λ y → z (subtract-ℕ k a) (leq-subtract-ℕ k a))
         (decide-order-ℕ a k))
    ( b)

gcd-euclid : ℕ → ℕ → ℕ
gcd-euclid =
  strong-ind-ℕ
    ( λ x → ℕ → ℕ)
    ( id)
    ( succ-gcd-euclid)

comp-succ-gcd-euclid :
  (a : ℕ) →
  Id (gcd-euclid (succ-ℕ a)) (succ-gcd-euclid a (λ x p → gcd-euclid x))
comp-succ-gcd-euclid =
  comp-succ-strong-ind-ℕ (λ x → ℕ → ℕ) id succ-gcd-euclid

-- Properties of the greatest common divisor

left-zero-law-gcd-euclid : (gcd-euclid zero-ℕ) ~ id
left-zero-law-gcd-euclid =
  htpy-eq (comp-zero-strong-ind-ℕ (λ x → ℕ → ℕ) id succ-gcd-euclid)

right-zero-law-gcd-euclid : (a : ℕ) → Id (gcd-euclid a zero-ℕ) a
right-zero-law-gcd-euclid zero-ℕ = refl
right-zero-law-gcd-euclid (succ-ℕ a) =
   ( ap
     ( λ t →
       cases-succ-strong-ind-ℕ (λ x → ℕ → ℕ) succ-gcd-euclid a
       ( induction-strong-ind-ℕ
         ( λ x → ℕ → ℕ)
         ( zero-strong-ind-ℕ (λ x → ℕ → ℕ) (λ a₁ → a₁))
         ( λ k H m p →
           cases-succ-strong-ind-ℕ (λ x → ℕ → ℕ) succ-gcd-euclid k H m
           (cases-leq-succ-ℕ p))
         ( a))
       ( succ-ℕ a) t zero-ℕ)
     cases-leq-succ-reflexive-leq-ℕ) ∙
  ( comp-zero-succ-gcd-euclid a (λ x _ z → z))

is-prop-le-ℕ : (a b : ℕ) → is-prop (le-ℕ a b)
is-prop-le-ℕ zero-ℕ zero-ℕ = is-prop-empty
is-prop-le-ℕ zero-ℕ (succ-ℕ b) = is-prop-unit
is-prop-le-ℕ (succ-ℕ a) zero-ℕ = is-prop-empty
is-prop-le-ℕ (succ-ℕ a) (succ-ℕ b) = is-prop-le-ℕ a b

is-prop'-le-ℕ : (a b : ℕ) → is-prop' (le-ℕ a b)
is-prop'-le-ℕ a b = is-prop'-is-prop (is-prop-le-ℕ a b)

{-
left-lesser-law-gcd-euclid : (a b : ℕ) → (le-ℕ a b) →
  Id (gcd-euclid a b) (gcd-euclid a (subtract-ℕ b a))
left-lesser-law-gcd-euclid zero-ℕ (succ-ℕ b) H = refl
left-lesser-law-gcd-euclid (succ-ℕ a) (succ-ℕ b) H =
  ( htpy-eq (comp-succ-gcd-euclid a) (succ-ℕ b)) ∙ {!!}
-}

{-  ( (comp-succ-succ-gcd-euclid a (λ x t → gcd-euclid x) b) ∙
    ( ( {!!} ∙ apd (λ t → (ind-coprod (λ x → ℕ)
     (λ t → gcd-euclid (subtract-ℕ a b) (succ-ℕ b))
     (λ t → succ-gcd-euclid a (λ x t₁ → gcd-euclid x) (subtract-ℕ b a))
     t)) (ap inr (is-prop'-le-ℕ a b {!!} {!!}))) ∙ {!!}
{-      ( inv (ap (λ t → cases-succ-strong-ind-ℕ (λ x → ℕ → ℕ) succ-gcd-euclid a
        (induction-strong-ind-ℕ (λ x → ℕ → ℕ)
        (zero-strong-ind-ℕ (λ x → ℕ → ℕ) (λ a₁ → a₁))
        (λ k H₁ m p →
        cases-succ-strong-ind-ℕ (λ x → ℕ → ℕ) succ-gcd-euclid k H₁ m
        (cases-leq-succ-ℕ p))
        a)
        (succ-ℕ a) t
        (subtract-ℕ (succ-ℕ b) (succ-ℕ a))) cases-leq-succ-reflexive-leq-ℕ))-}))
-}

-- We show that induction on ℕ implies ordinal induction.

fam-ordinal-ind-ℕ :
  { l : Level} → (ℕ → UU l) → ℕ → UU l
fam-ordinal-ind-ℕ P n = (m : ℕ) → (le-ℕ m n) → P m

le-zero-ℕ :
  (m : ℕ) → (le-ℕ m zero-ℕ) → empty
le-zero-ℕ zero-ℕ ()
le-zero-ℕ (succ-ℕ m) ()

zero-ordinal-ind-ℕ :
  { l : Level} (P : ℕ → UU l) → fam-ordinal-ind-ℕ P zero-ℕ
zero-ordinal-ind-ℕ P m t = ind-empty (le-zero-ℕ m t)

le-one-ℕ :
  (n : ℕ) → le-ℕ (succ-ℕ n) one-ℕ → empty
le-one-ℕ zero-ℕ ()
le-one-ℕ (succ-ℕ n) ()

transitive-le-ℕ' :
  (k l m : ℕ) → (le-ℕ k l) → (le-ℕ l (succ-ℕ m)) → le-ℕ k m
transitive-le-ℕ' zero-ℕ zero-ℕ m () s
transitive-le-ℕ' (succ-ℕ k) zero-ℕ m () s
transitive-le-ℕ' zero-ℕ (succ-ℕ l) zero-ℕ star s = ind-empty (le-one-ℕ l s)
transitive-le-ℕ' (succ-ℕ k) (succ-ℕ l) zero-ℕ t s = ind-empty (le-one-ℕ l s)
transitive-le-ℕ' zero-ℕ (succ-ℕ l) (succ-ℕ m) star s = star
transitive-le-ℕ' (succ-ℕ k) (succ-ℕ l) (succ-ℕ m) t s =
  transitive-le-ℕ' k l m t s

succ-ordinal-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( (n : ℕ) → (fam-ordinal-ind-ℕ P n) → P n) →
  ( k : ℕ) → fam-ordinal-ind-ℕ P k → fam-ordinal-ind-ℕ P (succ-ℕ k)
succ-ordinal-ind-ℕ P f k g m t =
  f m (λ m' t' → g m' (transitive-le-ℕ' m' m k t' t))

induction-ordinal-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( qS : (k : ℕ) → fam-ordinal-ind-ℕ P k → fam-ordinal-ind-ℕ P (succ-ℕ k))
  ( n : ℕ) → fam-ordinal-ind-ℕ P n
induction-ordinal-ind-ℕ P qS zero-ℕ = zero-ordinal-ind-ℕ P
induction-ordinal-ind-ℕ P qS (succ-ℕ n) =
  qS n (induction-ordinal-ind-ℕ P qS n)

conclusion-ordinal-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  (( n : ℕ) → fam-ordinal-ind-ℕ P n) → (n : ℕ) → P n
conclusion-ordinal-ind-ℕ P f n = f (succ-ℕ n) n (succ-le-ℕ n)

ordinal-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( (n : ℕ) → (fam-ordinal-ind-ℕ P n) → P n) →
  ( n : ℕ) → P n
ordinal-ind-ℕ P f =
  conclusion-ordinal-ind-ℕ P
    ( induction-ordinal-ind-ℕ P (succ-ordinal-ind-ℕ P f))

{- The Pigeon hole principle. -}

{- First we write a function that counts the number of elements in a decidable
   subset of a finite set. -}

count-Fin-succ-ℕ :
  {l : Level} (n : ℕ) (P : Fin (succ-ℕ n) → classical-Prop l) →
  ℕ → is-decidable (pr1 (pr1 (P (inr star)))) → ℕ
count-Fin-succ-ℕ n P m (inl x) = succ-ℕ m
count-Fin-succ-ℕ n P m (inr x) = m

count-Fin :
  {l : Level} (n : ℕ) (P : Fin n → classical-Prop l) → ℕ
count-Fin zero-ℕ P = zero-ℕ
count-Fin (succ-ℕ n) P =
  count-Fin-succ-ℕ n P
    ( count-Fin n (P ∘ inl))
    ( pr2 (P (inr star)))

{- Next we prove the pigeonhole principle. -}

max-Fin :
  (n : ℕ) → Fin (succ-ℕ n)
max-Fin n = inr star

contraction-Fin-one-ℕ :
  (t : Fin one-ℕ) → Id (inr star) t
contraction-Fin-one-ℕ (inr star) = refl

is-contr-Fin-one-ℕ :
  is-contr (Fin one-ℕ)
is-contr-Fin-one-ℕ = pair (inr star) contraction-Fin-one-ℕ

skip :
  (n : ℕ) → Fin (succ-ℕ n) → Fin n → Fin (succ-ℕ n)
skip (succ-ℕ n) (inl i) (inl j) = inl (skip n i j)
skip (succ-ℕ n) (inl i) (inr star) = inr star
skip (succ-ℕ n) (inr star) j = inl j

repeat :
  (n : ℕ) → Fin n → Fin (succ-ℕ n) → Fin n
repeat (succ-ℕ n) (inl i) (inl j) = inl (repeat n i j)
repeat (succ-ℕ n) (inl j) (inr star) = inr star
repeat (succ-ℕ n) (inr star) (inl j) = j
repeat (succ-ℕ n) (inr star) (inr star) = inr star

repeat-repeat :
  (n : ℕ) (i j : Fin n) →
    ((repeat n i) ∘ (repeat (succ-ℕ n) (skip n (inl i) j))) ~
    ((repeat n j) ∘ (repeat (succ-ℕ n) (skip n (inl j) i)))
repeat-repeat zero-ℕ () j k
repeat-repeat (succ-ℕ n) (inl i) (inl j) (inl k) =
  ap inl (repeat-repeat n i j k)
repeat-repeat (succ-ℕ n) (inl i) (inl j) (inr star) = refl
repeat-repeat (succ-ℕ n) (inl i) (inr star) (inr star) = refl
repeat-repeat (succ-ℕ n) (inr star) (inl j) (inr star) = refl
repeat-repeat (succ-ℕ n) (inr star) (inr star) (inl k) = refl
repeat-repeat (succ-ℕ n) (inr star) (inr star) (inr star) = refl
repeat-repeat (succ-ℕ zero-ℕ) (inl ()) (inr star) (inl k)
repeat-repeat (succ-ℕ (succ-ℕ n)) (inl i) (inr star) (inl k) = refl
repeat-repeat (succ-ℕ zero-ℕ) (inr star) (inl ()) (inl k)
repeat-repeat (succ-ℕ (succ-ℕ n)) (inr star) (inl j) (inl k) = refl

{-
skip-repeat :
  (n : ℕ) (i : Fin n) → ((skip n (inl i)) ∘ (repeat n i)) ~ id
skip-repeat (succ-ℕ n) (inl x) (inl y) = ap inl (skip-repeat n x y)
skip-repeat (succ-ℕ n) (inl x) (inr star) = refl
skip-repeat (succ-ℕ n) (inr star) (inl (inl x)) = ap inl {!ap (skip n) ?!}
skip-repeat (succ-ℕ n) (inr star) (inl (inr star)) = {!!}
skip-repeat (succ-ℕ n) (inr star) (inr star) = {!!}
-}

map-lift-Fin :
  (m n : ℕ) (f : Fin (succ-ℕ m) → Fin (succ-ℕ n))
  (i : Fin (succ-ℕ n)) (H : fib f i → empty) →
  Fin m → Fin n
map-lift-Fin m n f (inl i) H = (repeat n i) ∘ (f ∘ inl)
map-lift-Fin m (succ-ℕ n) f (inr star) H =
  ( repeat (succ-ℕ n) (max-Fin n)) ∘
  ( f ∘ inl)
map-lift-Fin zero-ℕ zero-ℕ f (inr star) H = ind-empty
map-lift-Fin (succ-ℕ m) zero-ℕ f (inr star) H =
  ex-falso
    ( H (pair (inr star) (inv (contraction-Fin-one-ℕ (f (inr star))))))

{-
is-lift-lift-Fin :
  (m n : ℕ) (f : Fin (succ-ℕ m) → Fin (succ-ℕ n))
  (i : Fin (succ-ℕ n)) (H : fib f i → empty) →
  (f ∘ inl) ~ ((skip n i) ∘ (map-lift-Fin m n f i H))
is-lift-lift-Fin m n f (inl i) H x = {!!}
is-lift-lift-Fin m n f (inr i) H x = {!!}
-}

-- The greatest common divisor

{- First we show that mul-ℕ n is an embedding whenever n > 0. In order to do
   this, we have to show that add-ℕ n is injective. -}

{-  FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX
is-injective-add-ℕ' :
  (n : ℕ) → is-injective is-set-ℕ is-set-ℕ (add-ℕ n)
is-injective-add-ℕ' n k l p = is-injective-add-ℕ' n k l
  (((commutative-add-ℕ n k) ∙ ?) ∙ (commutative-add-ℕ l n))

is-emb-add-ℕ :
  (n : ℕ) → is-emb (add-ℕ n)
is-emb-add-ℕ n =
  is-emb-is-injective is-set-ℕ is-set-ℕ (add-ℕ n) (is-injective-add-ℕ n)

equiv-fib-add-fib-add-ℕ' :
  (m n : ℕ) → fib (add-ℕ' m) n ≃ fib (add-ℕ m) n
equiv-fib-add-fib-add-ℕ' m n =
  equiv-tot (λ k → equiv-concat (commutative-add-ℕ m k) n)

leq-fib-add-ℕ' :
  (m n : ℕ) → fib (add-ℕ' m) n → (leq-ℕ m n)
leq-fib-add-ℕ' zero-ℕ n (pair k p) = leq-zero-ℕ n
leq-fib-add-ℕ' (succ-ℕ m) (succ-ℕ n) (pair k p) =
  leq-fib-add-ℕ' m n (pair k (is-injective-succ-ℕ (add-ℕ k m) n p))

leq-fib-add-ℕ :
  (m n : ℕ) → fib (add-ℕ m) n → (leq-ℕ m n)
leq-fib-add-ℕ m .m (pair zero-ℕ refl) = reflexive-leq-ℕ m
leq-fib-add-ℕ m .(add-ℕ m (succ-ℕ k)) (pair (succ-ℕ k) refl) =
  transitive-leq-ℕ m (add-ℕ m k) (succ-ℕ (add-ℕ m k))
    ( leq-fib-add-ℕ m (add-ℕ m k) (pair k refl))
    ( succ-leq-ℕ (add-ℕ m k))
-}

{-
fib-add-leq-ℕ :
  (m n : ℕ) → (leq-ℕ m n) → fib (add-ℕ m) n
fib-add-leq-ℕ zero-ℕ zero-ℕ star = pair zero-ℕ refl
fib-add-leq-ℕ zero-ℕ (succ-ℕ n) star = {!!}
fib-add-leq-ℕ (succ-ℕ m) (succ-ℕ n) p = {!!}

{-
fib-add-leq-ℕ zero-ℕ zero-ℕ H = pair zero-ℕ refl
fib-add-leq-ℕ zero-ℕ (succ-ℕ n) H = pair (succ-ℕ n) refl
fib-add-leq-ℕ (succ-ℕ m) (succ-ℕ n) H =
  pair
    ( pr1 (fib-add-leq-ℕ m n H))
    ( ap succ-ℕ (pr2 (fib-add-leq-ℕ m n H)))
-}

is-equiv-leq-fib-add-ℕ :
  (m n : ℕ) → is-equiv (leq-fib-add-ℕ m n)
is-equiv-leq-fib-add-ℕ m n =
  is-equiv-is-prop
    ( is-prop-map-is-emb _ (is-emb-add-ℕ m) n)
    ( is-prop-leq-ℕ m n)
    ( fib-add-leq-ℕ m n)

is-equiv-fib-add-leq-ℕ :
  (m n : ℕ) → is-equiv (fib-add-leq-ℕ m n)
is-equiv-fib-add-leq-ℕ m n =
  is-equiv-is-prop
    ( is-prop-leq-ℕ m n)
    ( is-prop-map-is-emb _ (is-emb-add-ℕ m) n)
    ( leq-fib-add-ℕ m n)
-}

is-emb-mul-ℕ :
  (n : ℕ) → is-emb (mul-ℕ' (succ-ℕ n))
is-emb-mul-ℕ n =
  is-emb-is-injective is-set-ℕ is-set-ℕ
    ( mul-ℕ' (succ-ℕ n))
    ( is-injective-mul-ℕ n)

{- FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX
is-emb-mul-ℕ' :
  (n : ℕ) → (le-ℕ zero-ℕ n) → is-emb (λ m → mul-ℕ m n)
is-emb-mul-ℕ' n t =
  is-emb-htpy'
    ( mul-ℕ n)
    ( λ m → mul-ℕ m n)
    ( commutative-mul-ℕ n)
    ( is-emb-mul-ℕ n)
-}

{- We conclude that the division relation is a property. -}

{-  FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX FIX
is-prop-div-ℕ :
  (m n : ℕ) → (le-ℕ zero-ℕ m) → is-prop (div-ℕ m n)
is-prop-div-ℕ (succ-ℕ m) n star =
  is-prop-map-is-emb
    ( λ z → mul-ℕ z (succ-ℕ m))
    ( is-emb-mul-ℕ' (succ-ℕ m) star)
    n
-}

{- We now construct the division with remainder. -}

le-mul-ℕ :
  (d n k : ℕ) → UU lzero
le-mul-ℕ d n k = le-ℕ n (mul-ℕ k d)

is-decidable-le-mul-ℕ :
  (d n k : ℕ) → is-decidable (le-mul-ℕ d n k)
is-decidable-le-mul-ℕ d n k =
  is-decidable-le-ℕ n (mul-ℕ k d)

order-preserving-succ-ℕ :
  (n n' : ℕ) → (leq-ℕ n n') → (leq-ℕ (succ-ℕ n) (succ-ℕ n'))
order-preserving-succ-ℕ n n' H = H

{-
order-preserving-add-ℕ :
  (m n m' n' : ℕ) →
  (leq-ℕ m m') → (leq-ℕ n n') → (leq-ℕ (add-ℕ m n) (add-ℕ m' n'))
order-preserving-add-ℕ = {!!}
-}

{-
order-preserving-add-ℕ zero-ℕ zero-ℕ m' n' Hm Hn = star
order-preserving-add-ℕ zero-ℕ (succ-ℕ n) zero-ℕ (succ-ℕ n') Hm Hn = Hn
order-preserving-add-ℕ zero-ℕ (succ-ℕ n) (succ-ℕ m') (succ-ℕ n') Hm Hn =
  leq-eq-right-ℕ n
    ( inv (right-successor-law-add-ℕ m' n'))
    ( order-preserving-add-ℕ zero-ℕ n (succ-ℕ m') n' Hm Hn)
order-preserving-add-ℕ (succ-ℕ m) n (succ-ℕ m') n' Hm Hn =
  order-preserving-add-ℕ m n m' n' Hm Hn
-}

le-eq-right-ℕ :
  (m : ℕ) {n n' : ℕ} → Id n n' → le-ℕ m n' → le-ℕ m n
le-eq-right-ℕ m refl = id

{-
le-add-ℕ :
  (m n : ℕ) → (leq-ℕ one-ℕ n) → le-ℕ m (add-ℕ m n)
le-add-ℕ = {!!}

{-
le-add-ℕ zero-ℕ (succ-ℕ n) star = star
le-add-ℕ (succ-ℕ m) (succ-ℕ n) star = le-add-ℕ m (succ-ℕ n) star
-}

le-mul-self-ℕ :
  (d n : ℕ) → (leq-ℕ one-ℕ d) → (leq-ℕ one-ℕ n) → le-mul-ℕ d n n
le-mul-self-ℕ (succ-ℕ d) (succ-ℕ n) star star =
  le-eq-right-ℕ
    ( succ-ℕ n)
    ( right-successor-law-mul-ℕ (succ-ℕ n) d)
    ( le-add-ℕ (succ-ℕ n) (mul-ℕ (succ-ℕ n) d) {!leq-eq-right-ℕ !})
-}

{-
leq-multiple-ℕ :
  (n m : ℕ) → (leq-ℕ one-ℕ m) → leq-ℕ n (mul-ℕ n m)
leq-multiple-ℕ n (succ-ℕ m) H =
  leq-eq-right-ℕ n
    ( inv (right-successor-law-mul-ℕ n m))
    ( leq-fib-add-ℕ n (add-ℕ n (mul-ℕ n m)) (pair (mul-ℕ n m) refl))

least-factor-least-larger-multiple-ℕ :
  (d n : ℕ) → (leq-ℕ one-ℕ d) →
  minimal-element-ℕ (λ k → leq-ℕ n (mul-ℕ k d))
least-factor-least-larger-multiple-ℕ d n H =
  well-ordering-principle-ℕ
    ( λ k → leq-ℕ n (mul-ℕ k d))
    ( λ k → is-decidable-leq-ℕ n (mul-ℕ k d))
    ( pair n (leq-multiple-ℕ n d H))

factor-least-larger-multiple-ℕ :
  (d n : ℕ) → (leq-ℕ one-ℕ d) → ℕ
factor-least-larger-multiple-ℕ d n H =
  pr1 (least-factor-least-larger-multiple-ℕ d n H)

least-larger-multiple-ℕ :
  (d n : ℕ) → (leq-ℕ one-ℕ d) → ℕ
least-larger-multiple-ℕ d n H =
  mul-ℕ (factor-least-larger-multiple-ℕ d n H) d

leq-least-larger-multiple-ℕ :
  (d n : ℕ) (H : leq-ℕ one-ℕ d) →
  leq-ℕ n (least-larger-multiple-ℕ d n H)
leq-least-larger-multiple-ℕ d n H =
  pr1 (pr2 (least-factor-least-larger-multiple-ℕ d n H))

is-minimal-least-larger-multiple-ℕ :
  (d n : ℕ) (H : leq-ℕ one-ℕ d) (k : ℕ) (K : leq-ℕ n (mul-ℕ k d)) →
  leq-ℕ (factor-least-larger-multiple-ℕ d n H) k
is-minimal-least-larger-multiple-ℕ d n H =
  pr2 (pr2 (least-factor-least-larger-multiple-ℕ d n H))
-}

{-
is-decidable-div-is-decidable-eq-least-larger-multiple-ℕ :
  (d n : ℕ) (H : leq-ℕ one-ℕ d) →
  is-decidable (Id (least-larger-multiple-ℕ d n H) n) → is-decidable (div-ℕ d n)
is-decidable-div-is-decidable-eq-least-larger-multiple-ℕ d n H (inl p) =
  inl (pair (factor-least-larger-multiple-ℕ d n H) p)
is-decidable-div-is-decidable-eq-least-larger-multiple-ℕ d n H (inr f) =
  inr (λ x → {!!})

is-decidable-div-ℕ' :
  (d n : ℕ) → (leq-ℕ one-ℕ d) → is-decidable (div-ℕ d n)
is-decidable-div-ℕ' d n H = {!!}

is-decidable-div-ℕ :
  (d n : ℕ) → is-decidable (div-ℕ d n)
is-decidable-div-ℕ zero-ℕ zero-ℕ = inl (pair zero-ℕ refl)
is-decidable-div-ℕ zero-ℕ (succ-ℕ n) =
  inr ( λ p →
    Eq-ℕ-eq {-zero-ℕ (succ-ℕ n)-} ((inv (right-zero-law-mul-ℕ (pr1 p))) ∙ (pr2 p)))
is-decidable-div-ℕ (succ-ℕ d) n =
  is-decidable-div-ℕ' (succ-ℕ d) n (leq-zero-ℕ d)
-}

-- Operations on decidable bounded subsets of ℕ

iterated-operation-ℕ :
  (strict-upper-bound : ℕ) (operation : ℕ → ℕ → ℕ) (base-value : ℕ) → ℕ
iterated-operation-ℕ zero-ℕ μ e = e
iterated-operation-ℕ (succ-ℕ b) μ e = μ (iterated-operation-ℕ b μ e) b

iterated-sum-ℕ :
  (summand : ℕ → ℕ) (b : ℕ) → ℕ
iterated-sum-ℕ f zero-ℕ = zero-ℕ
iterated-sum-ℕ f (succ-ℕ b) = add-ℕ (iterated-sum-ℕ f b) (f (succ-ℕ b))

ranged-sum-ℕ :
  (summand : ℕ → ℕ) (l u : ℕ) → ℕ
ranged-sum-ℕ f zero-ℕ u = iterated-sum-ℕ f u
ranged-sum-ℕ f (succ-ℕ l) zero-ℕ = zero-ℕ
ranged-sum-ℕ f (succ-ℕ l) (succ-ℕ u) =
  ranged-sum-ℕ (f ∘ succ-ℕ) l u

succ-iterated-operation-fam-ℕ :
  { l : Level}
  ( P : ℕ → UU l) (is-decidable-P : (n : ℕ) → is-decidable (P n)) →
  ( predecessor-strict-upper-bound : ℕ) (operation : ℕ → ℕ → ℕ) →
  is-decidable (P predecessor-strict-upper-bound) → ℕ → ℕ
succ-iterated-operation-fam-ℕ
  P is-decidable-P b μ (inl p) m = μ m b
succ-iterated-operation-fam-ℕ
  P is-decidable-P b μ (inr f) m = m

iterated-operation-fam-ℕ :
  { l : Level} (P : ℕ → UU l) (is-decidable-P : (n : ℕ) → is-decidable (P n)) →
  ( strict-upper-bound : ℕ) (operation : ℕ → ℕ → ℕ) (base-value : ℕ) → ℕ
iterated-operation-fam-ℕ P d zero-ℕ μ e = e
iterated-operation-fam-ℕ P d (succ-ℕ b) μ e =
  succ-iterated-operation-fam-ℕ P d b μ (d b)
    ( iterated-operation-fam-ℕ P d b μ e)

Sum-fam-ℕ :
  { l : Level} (P : ℕ → UU l) (is-decidable-P : (n : ℕ) → is-decidable (P n)) →
  ( upper-bound : ℕ) ( summand : ℕ → ℕ) → ℕ
Sum-fam-ℕ P d b f = iterated-operation-fam-ℕ P d (succ-ℕ b) (λ x y → add-ℕ x (f y)) zero-ℕ

{-
iterated-operation-fam-ℕ
  P is-decidable-P zero-ℕ is-bounded-P μ base-value =
  base-value
iterated-operation-fam-ℕ
  P is-decidable-P (succ-ℕ b) is-bounded-P μ base-value =
  succ-iterated-operation-ℕ P is-decidable-P b is-bounded-P μ
    ( is-decidable-P b)
    ( iterated-operation-ℕ
      ( introduce-bound-on-fam-ℕ b P)
      ( is-decidable-introduce-bound-on-fam-ℕ b P is-decidable-P)
      ( b)
      ( is-bounded-introduce-bound-on-fam-ℕ b P)
      ( μ)
      ( base-value))

product-decidable-bounded-fam-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( is-decidable-P : (n : ℕ) → is-decidable (P n))
  ( b : ℕ) ( is-bounded-P : is-bounded-fam-ℕ b P) → ℕ
product-decidable-bounded-fam-ℕ P is-decidable-P b is-bounded-P =
  iterated-operation-ℕ P is-decidable-P b is-bounded-P mul-ℕ one-ℕ

twenty-four-ℕ : ℕ
twenty-four-ℕ =
  product-decidable-bounded-fam-ℕ
    ( λ x → le-ℕ x five-ℕ)
    ( λ x → is-decidable-le-ℕ x five-ℕ)
    ( five-ℕ)
    ( λ x → id)
-}

{-
test-zero-twenty-four-ℕ : Id twenty-four-ℕ zero-ℕ
test-zero-twenty-four-ℕ = refl

test-twenty-four-ℕ : Id twenty-four-ℕ (factorial four-ℕ)
test-twenty-four-ℕ = refl
-}

-- Exercises

-- Exercise 10.?

abstract
  has-decidable-equality-𝟚 : has-decidable-equality bool
  has-decidable-equality-𝟚 true true = inl refl
  has-decidable-equality-𝟚 true false = inr (Eq-𝟚-eq true false)
  has-decidable-equality-𝟚 false true = inr (Eq-𝟚-eq false true)
  has-decidable-equality-𝟚 false false = inl refl

-- Exercise 10.?

abstract
  has-decidable-equality-prod' : {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    (x x' : A) (y y' : B) → is-decidable (Id x x') → is-decidable (Id y y') →
    is-decidable (Id (pair x y) (pair x' y'))
  has-decidable-equality-prod' x x' y y' (inl p) (inl q) =
    inl (eq-pair-triv (pair p q))
  has-decidable-equality-prod' x x' y y' (inl p) (inr g) =
    inr (λ h → g (ap pr2 h))
  has-decidable-equality-prod' x x' y y' (inr f) (inl q) =
    inr (λ h → f (ap pr1 h))
  has-decidable-equality-prod' x x' y y' (inr f) (inr g) =
    inr (λ h → f (ap pr1 h))

abstract
  has-decidable-equality-prod : {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    has-decidable-equality A → has-decidable-equality B →
    has-decidable-equality (A × B)
  has-decidable-equality-prod dec-A dec-B (pair x y) (pair x' y') =
    has-decidable-equality-prod' x x' y y' (dec-A x x') (dec-B y y')

{-

bounds-fam-ℕ :
  {l : Level} (P : ℕ → UU l) → UU l
bounds-fam-ℕ P = Σ ℕ (λ n → is-bounded-fam-ℕ n P)

is-minimal-ℕ :
  {l : Level} (P : ℕ → UU l) → Σ ℕ P → UU l
is-minimal-ℕ P (pair n p) = (t : Σ ℕ P) → leq-ℕ n (pr1 t)

fam-succ-ℕ :
  {l : Level} → (ℕ → UU l) → (ℕ → UU l)
fam-succ-ℕ P n = P (succ-ℕ n)

is-decidable-fam-succ-ℕ :
  {l : Level} (P : ℕ → UU l) →
  ((n : ℕ) → is-decidable (P n)) → ((n : ℕ) → is-decidable (P (succ-ℕ n)))
is-decidable-fam-succ-ℕ P d n = d (succ-ℕ n)

min-is-bounded-not-zero-ℕ :
  {l : Level} (P : ℕ → UU l) → ((n : ℕ) → is-decidable (P n)) →
  Σ ℕ (λ n → is-bounded-fam-ℕ n P) →
  ¬ (P zero-ℕ) →
  Σ (Σ ℕ (fam-succ-ℕ P)) (is-minimal-ℕ (fam-succ-ℕ P)) →
  Σ (Σ ℕ P) (is-minimal-ℕ P)
min-is-bounded-not-zero-ℕ P d b np0 t = {!!}

min-is-bounded-ℕ :
  {l : Level} (P : ℕ → UU l) → ((n : ℕ) → is-decidable (P n)) →
  Σ ℕ (λ n → is-bounded-fam-ℕ n P) →
  Σ ℕ P → Σ (Σ ℕ P) (is-minimal-ℕ P)
min-is-bounded-ℕ P d (pair zero-ℕ b) t =
  pair
    ( pair
      ( zero-ℕ)
      ( tr P (eq-zero-leq-zero-ℕ (pr1 t) (b (pr1 t) (pr2 t))) (pr2 t)))
    ( λ p → leq-zero-ℕ (pr1 p))
min-is-bounded-ℕ P d (pair (succ-ℕ n) b) t =
  ind-coprod
    ( λ (t : is-decidable (P zero-ℕ)) → Σ (Σ ℕ P) (is-minimal-ℕ P))
    ( λ p0 → pair (pair zero-ℕ p0) (λ p → leq-zero-ℕ (pr1 p)))
    ( λ y → min-is-bounded-not-zero-ℕ P d (pair (succ-ℕ n) b) y
      ( min-is-bounded-ℕ
        ( fam-succ-ℕ P)
        ( is-decidable-fam-succ-ℕ P d)
        {!!}
        {!!}))
    ( d zero-ℕ)

{- We show that every non-empty decidable subset of ℕ has a least element. -}

least-ℕ :
  {l : Level} (P : ℕ → UU l) → Σ ℕ P → UU l
least-ℕ P (pair n p) = (m : ℕ) → P m → leq-ℕ n m

least-element-non-empty-decidable-subset-ℕ :
  {l : Level} (P : ℕ → UU l) (d : (n : ℕ) → is-decidable (P n)) →
  Σ ℕ P → Σ (Σ ℕ P) (least-ℕ P)
least-element-non-empty-decidable-subset-ℕ P d (pair zero-ℕ p) =
  pair (pair zero-ℕ p) {!!}
least-element-non-empty-decidable-subset-ℕ P d (pair (succ-ℕ n) p) = {!!}
-}

{-
zero-Fin :
  (n : ℕ) → Fin (succ-ℕ n)
zero-Fin zero-ℕ = inr star
zero-Fin (succ-ℕ n) = inl (zero-Fin n)

succ-Fin :
  (n : ℕ) → Fin n → Fin n
succ-Fin (succ-ℕ n) (inr star) = zero-Fin n
succ-Fin (succ-ℕ (succ-ℕ n)) (inl (inl x)) = inl (succ-Fin (succ-ℕ n) (inl x))
succ-Fin (succ-ℕ (succ-ℕ n)) (inl (inr star)) = inr star

iterated-succ-Fin :
  (k : ℕ) → (n : ℕ) → Fin n → Fin n
iterated-succ-Fin zero-ℕ n = id
iterated-succ-Fin (succ-ℕ k) n = (succ-Fin n) ∘ (iterated-succ-Fin k n)

quotient-ℕ-Fin :
  (n : ℕ) → Fin (succ-ℕ n)
quotient-ℕ-Fin n = iterated-succ-Fin n (succ-ℕ n) (zero-Fin n)

pred-Fin :
  (n : ℕ) → Fin n → Fin n
pred-Fin (succ-ℕ zero-ℕ) (inr star) = inr star
pred-Fin (succ-ℕ (succ-ℕ n)) (inl x) = {!!}
pred-Fin (succ-ℕ (succ-ℕ n)) (inr star) = inl (inr star)

add-Fin :
  (n : ℕ) → Fin n → Fin n → Fin n
add-Fin (succ-ℕ n) (inl x) j = {!!}
add-Fin (succ-ℕ n) (inr x) j = {!!}

idempotent-succ-Fin :
  (n : ℕ) (i : Fin n) → Id (iterated-succ-Fin n n i) i
idempotent-succ-Fin (succ-ℕ zero-ℕ) (inr star) = refl
idempotent-succ-Fin (succ-ℕ (succ-ℕ n)) (inl x) = {!!}
idempotent-succ-Fin (succ-ℕ (succ-ℕ n)) (inr x) = {!!}

-}

in-nat-ℤ : ℕ → ℤ
in-nat-ℤ zero-ℕ = zero-ℤ
in-nat-ℤ (succ-ℕ n) = in-pos n

div-ℤ :
  (k l : ℤ) → UU lzero
div-ℤ k l = Σ ℤ (λ x → Id (mul-ℤ x k) l)

-- _≡_mod_ :
--   (k l : ℤ) (n : ℕ) → UU lzero
-- k ≡ l mod n = div-ℤ (in-nat-ℤ n) (add-ℤ k (neg-ℤ l))

-- From before

is-even-ℕ : ℕ → UU lzero
is-even-ℕ n = div-ℕ two-ℕ n

is-prime : ℕ → UU lzero
is-prime n = (one-ℕ < n) × ((m : ℕ) → (one-ℕ < m) → (div-ℕ m n) → Id m n)

{- The Goldbach conjecture asserts that every even number above 2 is the sum
   of two primes. -}

Goldbach-conjecture : UU lzero
Goldbach-conjecture =
  ( n : ℕ) → (two-ℕ < n) → (is-even-ℕ n) →
    Σ ℕ (λ p → (is-prime p) × (Σ ℕ (λ q → (is-prime q) × Id (add-ℕ p q) n)))

is-twin-prime : ℕ → UU lzero
is-twin-prime n = (is-prime n) × (is-prime (succ-ℕ (succ-ℕ n)))

{- The twin prime conjecture asserts that there are infinitely many twin
   primes. We assert that there are infinitely twin primes by asserting that
   for every n : ℕ there is a twin prime that is larger than n. -}

Twin-prime-conjecture : UU lzero
Twin-prime-conjecture = (n : ℕ) → Σ ℕ (λ p → (is-twin-prime p) × (leq-ℕ n p))

-- Exercise

unit-classical-Prop : classical-Prop lzero
unit-classical-Prop =
  pair unit-Prop (inl star)

raise-unit-classical-Prop :
  (l : Level) → classical-Prop l
raise-unit-classical-Prop l =
  pair
    ( pair
      ( raise l unit)
      ( is-prop-is-equiv' unit
        ( map-raise)
        ( is-equiv-map-raise l unit)
        ( is-prop-unit)))
    ( inl (map-raise star))

bool-classical-Prop :
  (l : Level) → classical-Prop l → bool
bool-classical-Prop l (pair P (inl x)) = true
bool-classical-Prop l (pair P (inr x)) = false

{-
classical-Prop-bool :
  (l : Level) → bool → classical-Prop l
classical-Prop-bool l true = raise-unit-classical-Prop l
classical-Prop-bool l false = {!!}
-}

max_stars_repo_name: tmoux/HoTT-Intro

max_issues_repo_name: tmoux/HoTT-Intro

max_forks_repo_name: tmoux/HoTT-Intro


text:
-- Check that the termination checker can handle recursive
-- calls on subterms which aren't simply variables.
module SubtermTermination where

data N : Set where
  zero : N
  suc  : N → N

f : N → N
f (suc zero) = f zero
f _          = zero

data One? : N → Set where
  one : One? (suc zero)
  other : ∀ {n} → One? n

-- Should work for dot patterns as well
f′ : (n : N) → One? n → N
f′ (suc .zero) one = f′ zero other
f′ _           _   = zero

f″ : (n : N) → One? n → N
f″ ._ one = f″ zero other
f″ _  _   = zero

data D : Set where
  c₁ : D
  c₂ : D → D
  c₃ : D → D → D

g : D → D
g (c₃ (c₂ x) y) = g (c₂ x)
g _ = c₁

{- Andreas, 2011-07-07 subterm is not complete
   does not work with postulates or definitions

postulate
  i : {A : Set} → A → A

data NAT : N → Set where
  Zero : NAT zero
  Suc  : ∀ n → NAT (i n) → NAT (suc (i n))

h : (n : N) -> NAT n -> Set
h .zero Zero = N
h .(suc (i n)) (Suc n m) = h (i n) (i m)
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- The paradoxical combinator
------------------------------------------------------------------------------

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

-- See (Barendregt 2004, corollary 6.1.3).

module FOT.LTC-PCF.Y where

open import LTC-PCF.Base hiding ( fix ; fix-eq )

------------------------------------------------------------------------------
-- This is the fixed-point combinator used by (Dybjer 1985).
Y : D
Y = lam (λ f → lam (λ x → f · (x · x)) · lam (λ x → f · (x · x)))

-- We define a higher-order Y.
Y₁ : (D → D) → D
Y₁ f = Y · lam f

------------------------------------------------------------------------------
-- References
--
-- Barendregt, Henk (2004). The Lambda Calculus. Its Syntax and
-- Semantics. 2nd ed. Vol. 103. Studies in Logic and the Foundations
-- of Mathematics. 6th impression. Elsevier.
--
-- Dybjer, Peter (1985). Program Verification in a Logical Theory of
-- Constructions. In: Functional Programming Languages and Computer
-- Architecture. Ed. by Jouannaud,
-- Jean-Pierre. Vol. 201. LNCS. Appears in revised form as Programming
-- Methodology Group Report 26, University of Gothenburg and Chalmers
-- University of Technology, June 1986. Springer, pp. 334–349 (cit. on
-- p. 26).

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Data.Vec.Inductive where

open import Prelude
open import Data.List using (List; _∷_; []; length)

private
  variable
    n m : ℕ

infixr 5 _∷_
data Vec (A : Type a) : ℕ → Type a where
  [] : Vec A 0
  _∷_ : A → Vec A n → Vec A (suc n)

foldr : ∀ {p} (P : ℕ → Type p) →
          (∀ {n} → A → P n → P (suc n)) →
          P zero →
          Vec A n → P n
foldr P f b [] = b
foldr P f b (x ∷ xs) = f x (foldr P f b xs)

foldl : ∀ {p} (P : ℕ → Type p) →
          (∀ {n} → A → P n → P (suc n)) →
          P zero →
          Vec A n → P n
foldl P f b [] = b
foldl P f b (x ∷ xs) = foldl (P ∘ suc) f (f x b) xs

foldr′ : (A → B → B) → B → Vec A n → B
foldr′ f = foldr (const _) (λ x xs → f x xs)

foldl′ : (A → B → B) → B → Vec A n → B
foldl′ f = foldl (const _) (λ x xs → f x xs)

vecFromList : (xs : List A) → Vec A (length xs)
vecFromList [] = []
vecFromList (x ∷ xs) = x ∷ vecFromList xs

vecToList : Vec A n → List A
vecToList [] = []
vecToList (x ∷ xs) = x ∷ vecToList xs

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-
  Finitely presented algebras.
  An R-algebra A is finitely presented, if there merely is an exact sequence
  of R-modules:

    (f₁,⋯,fₘ) → R[X₁,⋯,Xₙ] → A → 0

  (where f₁,⋯,fₘ ∈ R[X₁,⋯,Xₙ])
-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.FPAlgebra where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure

open import Cubical.Data.FinData
open import Cubical.Data.Nat
open import Cubical.Data.Vec
open import Cubical.Data.Sigma
open import Cubical.Data.Empty

open import Cubical.HITs.PropositionalTruncation

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal using (inclOfFGIdeal)
open import Cubical.Algebra.CommAlgebra
open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra
  renaming (inducedHom to freeInducedHom)
open import Cubical.Algebra.CommAlgebra.QuotientAlgebra
  renaming (inducedHom to quotientInducedHom)
open import Cubical.Algebra.CommAlgebra.Ideal
open import Cubical.Algebra.CommAlgebra.FGIdeal
open import Cubical.Algebra.CommAlgebra.Instances.Initial
open import Cubical.Algebra.CommAlgebra.Instances.Unit
  renaming (UnitCommAlgebra to TerminalCAlg)
open import Cubical.Algebra.CommAlgebra.Kernel
open import Cubical.Algebra.Algebra.Properties
open import Cubical.Algebra.Algebra

private
  variable
    ℓ : Level

module _ {R : CommRing ℓ} where
  open Construction using (var)
  Polynomials : (n : ℕ) → CommAlgebra R ℓ
  Polynomials n = R [ Fin n ]

  evPoly : {n : ℕ} (A : CommAlgebra R ℓ) → ⟨ Polynomials n ⟩ → FinVec ⟨ A ⟩ n → ⟨ A ⟩
  evPoly A P values = fst (freeInducedHom A values) P

  evPolyPoly : {n : ℕ} (P : ⟨ Polynomials n ⟩) → evPoly (Polynomials n) P var ≡ P
  evPolyPoly {n = n} P = cong (λ u → fst u P) (inducedHomVar R (Fin n))

  evPolyHomomorphic : {n : ℕ} (A B : CommAlgebra R ℓ) (f : CommAlgebraHom A B)
                     → (P : ⟨ Polynomials n ⟩) → (values : FinVec ⟨ A ⟩ n)
                     → (fst f) (evPoly A P values) ≡ evPoly B P (fst f ∘ values)
  evPolyHomomorphic A B f P values =
    (fst f) (evPoly A P values)                         ≡⟨ refl ⟩
    (fst f) (fst (freeInducedHom A values) P)           ≡⟨ refl ⟩
    fst (f ∘a freeInducedHom A values) P                ≡⟨ cong (λ u → fst u P) (natIndHomR f values) ⟩
    fst (freeInducedHom B (fst f ∘ values)) P           ≡⟨ refl ⟩
    evPoly B P (fst f ∘ values) ∎
    where open AlgebraHoms

  module _ {m : ℕ} (n : ℕ) (relation : FinVec ⟨ Polynomials n ⟩ m) where
    open CommAlgebraStr using (0a)
    open Cubical.Algebra.Algebra.Properties.AlgebraHoms

    relationsIdeal = generatedIdeal (Polynomials n) relation

    abstract
      {-
        The following definitions are abstract because of type checking speed
        problems - complete unfolding of FPAlgebra is triggered otherwise.
        This also means, the where blocks contain more type declarations than usual.
      -}
      FPAlgebra : CommAlgebra R ℓ
      FPAlgebra = Polynomials n / relationsIdeal

      modRelations : CommAlgebraHom (Polynomials n) (Polynomials n / relationsIdeal)
      modRelations = quotientHom (Polynomials n) relationsIdeal

      generator : (i : Fin n) → ⟨ FPAlgebra ⟩
      generator = fst modRelations ∘ var

      relationsHold : (i : Fin m) → evPoly FPAlgebra (relation i) generator ≡ 0a (snd FPAlgebra)
      relationsHold i =
        evPoly FPAlgebra (relation i) generator
        ≡⟨ sym (evPolyHomomorphic (Polynomials n) FPAlgebra modRelations (relation i) var) ⟩
        fst modRelations (evPoly (Polynomials n) (relation i) var)
        ≡⟨ cong (λ u → fst modRelations u) (evPolyPoly (relation i)) ⟩
        fst modRelations (relation i)
        ≡⟨ isZeroFromIdeal {R = R}
                           {A = (Polynomials n)}
                           {I = relationsIdeal}
                           (relation i)
                           (incInIdeal (Polynomials n) relation i ) ⟩
        0a (snd FPAlgebra) ∎

      inducedHom :
        (A : CommAlgebra R ℓ)
        (values : FinVec ⟨ A ⟩ n)
        (relationsHold : (i : Fin m) → evPoly A (relation i) values ≡ 0a (snd A))
        → CommAlgebraHom FPAlgebra A
      inducedHom A values relationsHold =
        quotientInducedHom
          (Polynomials n)
          relationsIdeal
          A
          freeHom
          isInKernel
        where
          freeHom : CommAlgebraHom (Polynomials n) A
          freeHom = freeInducedHom A values
          isInKernel :   fst (generatedIdeal (Polynomials n) relation)
                       ⊆ fst (kernel (Polynomials n) A freeHom)
          isInKernel = inclOfFGIdeal
                         (CommAlgebra→CommRing (Polynomials n))
                         relation
                         (kernel (Polynomials n) A freeHom)
                         relationsHold

      inducedHomOnGenerators :
        (A : CommAlgebra R ℓ)
        (values : FinVec ⟨ A ⟩ n)
        (relationsHold : (i : Fin m) → evPoly A (relation i) values ≡ 0a (snd A))
        (i : Fin n)
        → fst (inducedHom A values relationsHold) (generator i) ≡ values i
      inducedHomOnGenerators _ _ _ _ = refl

      unique :
             {A : CommAlgebra R ℓ}
             (values : FinVec ⟨ A ⟩ n)
             (relationsHold : (i : Fin m) → evPoly A (relation i) values ≡ 0a (snd A))
             (f : CommAlgebraHom FPAlgebra A)
             → ((i : Fin n) → fst f (generator i) ≡ values i)
             → inducedHom A values relationsHold ≡ f
      unique {A = A} values relationsHold f hasCorrectValues =
        injectivePrecomp
          (Polynomials n)
          relationsIdeal
          A
          (inducedHom A values relationsHold)
          f
          (sym (
           f'     ≡⟨ sym (inv f') ⟩
           freeInducedHom A (evaluateAt A f')    ≡⟨ cong (freeInducedHom A)
                                                         (funExt hasCorrectValues) ⟩
           freeInducedHom A values               ≡⟨ cong (freeInducedHom A) refl ⟩
           freeInducedHom A (evaluateAt A iHom') ≡⟨ inv iHom' ⟩
           iHom' ∎))
        where
          {-
                     Poly n
                      |    \
            modRelations    f'
                      ↓      ↘
                 FPAlgebra ─f→ A
          -}
          f' iHom' : CommAlgebraHom (Polynomials n) A
          f' = compAlgebraHom modRelations f
          iHom' = compAlgebraHom modRelations (inducedHom A values relationsHold)

          inv : retract (Iso.fun (homMapIso {I = Fin n} A)) (Iso.inv (homMapIso A))
          inv = Iso.leftInv (homMapIso {R = R} {I = Fin n} A)

      universal :
             (A : CommAlgebra R ℓ)
             (values : FinVec ⟨ A ⟩ n)
             (relationsHold : (i : Fin m) → evPoly A (relation i) values ≡ 0a (snd A))
             → isContr (Σ[ f ∈ CommAlgebraHom FPAlgebra A ] ((i : Fin n) → fst f (generator i) ≡ values i))
      universal A values relationsHold =
        ( (inducedHom A values relationsHold)
          , (inducedHomOnGenerators A values relationsHold) )
        , λ {(f , mapsValues)
            → Σ≡Prop (λ _ → isPropΠ (λ _ → isSetCommAlgebra A _ _))
                     (unique values relationsHold f mapsValues)}

      {- ∀ A : Comm-R-Algebra,
         ∀ J : Finitely-generated-Ideal,
         Hom(R[I]/J,A) is isomorphic to the Set of roots of the generators of J
      -}

      zeroLocus : (A : CommAlgebra R ℓ) → Type ℓ
      zeroLocus A = Σ[ v ∈ FinVec ⟨ A ⟩ n ] ((i : Fin m) → evPoly A (relation i) v ≡ 0a (snd A))

      inducedHomFP : (A : CommAlgebra R ℓ) →
                      zeroLocus A → CommAlgebraHom FPAlgebra A
      inducedHomFP A d = inducedHom A (fst d) (snd d)

      evaluateAtFP : {A : CommAlgebra R ℓ} →
                      CommAlgebraHom FPAlgebra A → zeroLocus A
      evaluateAtFP {A} f = value ,
        λ i →  evPoly A (relation i) value                            ≡⟨ step1 (relation i) ⟩
            fst compHom (evPoly (Polynomials n) (relation i) var)  ≡⟨ refl ⟩
            (fst f) ((fst modRelations)
                       (evPoly (Polynomials n) (relation i) var))  ≡⟨ cong
                                                                       (fst f)
                                                                       (evPolyHomomorphic
                                                                         (Polynomials n)
                                                                         FPAlgebra
                                                                         modRelations
                                                                         (relation i) var) ⟩
            (fst f) (evPoly FPAlgebra (relation i) generator)      ≡⟨ cong (fst f) (relationsHold i) ⟩
            (fst f) (0a (snd FPAlgebra))                           ≡⟨ IsAlgebraHom.pres0 (snd f) ⟩
            0a (snd A) ∎
        where
          compHom : CommAlgebraHom (Polynomials n) A
          compHom = CommAlgebraHoms.compCommAlgebraHom (Polynomials n) FPAlgebra A modRelations f
          value : FinVec ⟨ A ⟩ n
          value = (Iso.fun (homMapIso A)) compHom
          step1 : (x : ⟨ Polynomials n ⟩) → evPoly A x value ≡ fst compHom (evPoly (Polynomials n) x var)
          step1 x = sym (evPolyHomomorphic (Polynomials n) A compHom x var)

      FPHomIso : {A : CommAlgebra R ℓ} →
                  Iso (CommAlgebraHom FPAlgebra A) (zeroLocus A)
      Iso.fun FPHomIso = evaluateAtFP
      Iso.inv FPHomIso = inducedHomFP _
      Iso.rightInv (FPHomIso {A}) =
        λ b → Σ≡Prop
                (λ x → isPropΠ
                  (λ i → isSetCommAlgebra A
                          (evPoly A (relation i) x)
                          (0a (snd A))))
                refl
      Iso.leftInv (FPHomIso {A}) =
        λ a → Σ≡Prop (λ f → isPropIsCommAlgebraHom {ℓ} {R} {ℓ} {ℓ} {FPAlgebra} {A} f)
                 λ i → fst (unique {A}
                             (fst (evaluateAtFP {A} a))
                             (snd (evaluateAtFP a))
                             a
                             (λ j → refl)
                             i)

      homMapPathFP : (A : CommAlgebra R ℓ)→ CommAlgebraHom FPAlgebra A ≡ zeroLocus A
      homMapPathFP A = isoToPath (FPHomIso {A})

      isSetZeroLocus : (A : CommAlgebra R ℓ) → isSet (zeroLocus A)
      isSetZeroLocus A =  J (λ y _ → isSet y)
                       (isSetAlgebraHom (CommAlgebra→Algebra FPAlgebra) (CommAlgebra→Algebra A))
                       (homMapPathFP A)

  record FinitePresentation (A : CommAlgebra R ℓ) : Type ℓ where
    field
      n : ℕ
      m : ℕ
      relations : FinVec ⟨ Polynomials n ⟩ m
      equiv : CommAlgebraEquiv (FPAlgebra n relations) A

  isFPAlgebra : (A : CommAlgebra R ℓ) → Type _
  isFPAlgebra A = ∥ FinitePresentation A ∥₁

  isFPAlgebraIsProp : {A : CommAlgebra R ℓ} → isProp (isFPAlgebra A)
  isFPAlgebraIsProp = isPropPropTrunc

module Instances (R : CommRing ℓ) where
  open FinitePresentation

  {- Every (multivariate) polynomial algebra is finitely presented -}
  module _ (n : ℕ) where
    private
      A : CommAlgebra R ℓ
      A = Polynomials n

      emptyGen : FinVec (fst A) 0
      emptyGen = λ ()

      B : CommAlgebra R ℓ
      B = FPAlgebra n emptyGen

    polynomialAlgFP : FinitePresentation A
    FinitePresentation.n polynomialAlgFP = n
    m polynomialAlgFP = 0
    relations polynomialAlgFP = emptyGen
    equiv polynomialAlgFP =
      -- Idea: A and B enjoy the same universal property.
      toAAsEquiv , snd toA
      where
        toA : CommAlgebraHom B A
        toA = inducedHom n emptyGen A Construction.var (λ ())
        fromA : CommAlgebraHom A B
        fromA = freeInducedHom B (generator _ _)
        open AlgebraHoms
        inverse1 : fromA ∘a toA ≡ idAlgebraHom _
        inverse1 =
          fromA ∘a toA
            ≡⟨ sym (unique _ _ _ _ _ (λ i → cong (fst fromA) (
                 fst toA (generator n emptyGen i)
                   ≡⟨ inducedHomOnGenerators _ _ _ _ _ _ ⟩
                 Construction.var i
                   ∎))) ⟩
          inducedHom n emptyGen B (generator _ _) (relationsHold _ _)
            ≡⟨ unique _ _ _ _ _ (λ i → refl) ⟩
          idAlgebraHom _
            ∎
        inverse2 : toA ∘a fromA ≡ idAlgebraHom _
        inverse2 = isoFunInjective (homMapIso A) _ _ (
          evaluateAt A (toA ∘a fromA)   ≡⟨ sym (naturalEvR {A = B} {B = A} toA fromA) ⟩
          fst toA ∘ evaluateAt B fromA  ≡⟨ refl ⟩
          fst toA ∘ generator _ _       ≡⟨ funExt (inducedHomOnGenerators _ _ _ _ _)⟩
          Construction.var              ∎)
        toAAsEquiv : ⟨ B ⟩ ≃ ⟨ A ⟩
        toAAsEquiv = isoToEquiv (iso (fst toA)
                                     (fst fromA)
                                     (λ a i → fst (inverse2 i) a)
                                     (λ b i → fst (inverse1 i) b))

  {- The initial R-algebra is finitely presented -}
  private
    R[⊥] : CommAlgebra R ℓ
    R[⊥] = Polynomials 0

    emptyGen : FinVec (fst R[⊥]) 0
    emptyGen = λ ()

    R[⊥]/⟨0⟩ : CommAlgebra R ℓ
    R[⊥]/⟨0⟩ = FPAlgebra 0 emptyGen

  R[⊥]/⟨0⟩IsInitial : (B : CommAlgebra R ℓ)
                     → isContr (CommAlgebraHom R[⊥]/⟨0⟩ B)
  R[⊥]/⟨0⟩IsInitial B = iHom , uniqueness
    where
      iHom : CommAlgebraHom R[⊥]/⟨0⟩ B
      iHom = inducedHom 0 emptyGen B (λ ()) (λ ())
      uniqueness : (f : CommAlgebraHom R[⊥]/⟨0⟩ B) →
                   iHom ≡ f
      uniqueness f = unique 0 emptyGen {A = B} (λ ()) (λ ()) f (λ ())

  initialCAlgFP : FinitePresentation (initialCAlg R)
  n initialCAlgFP = 0
  m initialCAlgFP = 0
  relations initialCAlgFP = emptyGen
  equiv initialCAlgFP =
    equivByInitiality R R[⊥]/⟨0⟩ R[⊥]/⟨0⟩IsInitial

  {- The terminal R-algebra is finitely presented -}
  private
    unitGen : FinVec (fst R[⊥]) 1
    unitGen zero = 1a
      where open CommAlgebraStr (snd R[⊥])

    R[⊥]/⟨1⟩ : CommAlgebra R ℓ
    R[⊥]/⟨1⟩ = FPAlgebra 0 unitGen

  terminalCAlgFP : FinitePresentation (TerminalCAlg R)
  n terminalCAlgFP = 0
  m terminalCAlgFP = 1
  relations terminalCAlgFP = unitGen
  equiv terminalCAlgFP = equivFrom1≡0 R R[⊥]/⟨1⟩
                                      (sym (⋆-lid 1a) ∙ relationsHold 0 unitGen zero)
    where open CommAlgebraStr (snd R[⊥]/⟨1⟩)

  {-
    Quotients of the base ring by principal ideals are finitely presented.
  -}
  module _ (x : ⟨ R ⟩) where
    ⟨x⟩ : IdealsIn (initialCAlg R)
    ⟨x⟩ = generatedIdeal (initialCAlg R) (replicateFinVec 1 x)

    R/⟨x⟩ = (initialCAlg R) / ⟨x⟩

    open CommAlgebraStr ⦃...⦄
    private
      relation : FinVec ⟨ Polynomials {R = R} 0 ⟩ 1
      relation = replicateFinVec 1 (Construction.const x)

      B = FPAlgebra 0 relation

      π = quotientHom (initialCAlg R) ⟨x⟩
      instance
        _ = snd R/⟨x⟩
        _ = snd (initialCAlg R)
        _ = snd B

      πx≡0 : π $a x ≡ 0a
      πx≡0 = isZeroFromIdeal {A = initialCAlg R} {I = ⟨x⟩} x
               (incInIdeal (initialCAlg R) (replicateFinVec 1 x) zero)

    R/⟨x⟩FP : FinitePresentation R/⟨x⟩
    n R/⟨x⟩FP = 0
    m R/⟨x⟩FP = 1
    relations R/⟨x⟩FP = relation
    equiv R/⟨x⟩FP = (isoToEquiv (iso (fst toA) (fst fromA)
                                    (λ a i → toFrom i $a a)
                                    λ a i → fromTo i $a a))
                   , (snd toA)
      where
        toA : CommAlgebraHom B R/⟨x⟩
        toA = inducedHom 0 relation R/⟨x⟩ (λ ()) relation-holds
          where
            vals : FinVec ⟨ R/⟨x⟩ ⟩ 0
            vals ()
            vals' : FinVec ⟨ initialCAlg R ⟩ 0
            vals' ()
            relation-holds = λ zero →
              evPoly R/⟨x⟩ (relation zero) (λ ())    ≡⟨ sym
                                                       (evPolyHomomorphic
                                                         (initialCAlg R)
                                                          R/⟨x⟩
                                                          π
                                                          (Construction.const x)
                                                          vals') ⟩
              π $a (evPoly (initialCAlg R)
                           (Construction.const x)
                           vals')                   ≡⟨ cong (π $a_) (·Rid x) ⟩
              π $a x                                ≡⟨ πx≡0 ⟩
              0a                               ∎
        {-
            R ─→   R/⟨x⟩
          id↓       ↓ ∃!
            R ─→   R[⊥]/⟨const x⟩
        -}
        fromA : CommAlgebraHom R/⟨x⟩ B
        fromA =
          quotientInducedHom
            (initialCAlg R)
            ⟨x⟩
            B
            (initialMap R B)
            (inclOfFGIdeal
              (CommAlgebra→CommRing (initialCAlg R))
              (replicateFinVec 1 x)
              (kernel (initialCAlg R) B (initialMap R B))
              λ {Fin.zero → relationsHold 0 relation Fin.zero})

        open AlgebraHoms

        fromTo : fromA ∘a toA ≡ idCAlgHom B
        fromTo = cong fst
          (isContr→isProp (universal 0 relation B (λ ()) (relationsHold 0 relation))
                          (fromA ∘a toA , (λ ()))
                          (idCAlgHom B , (λ ())))

        toFrom : toA ∘a fromA ≡ idCAlgHom R/⟨x⟩
        toFrom = injectivePrecomp (initialCAlg R) ⟨x⟩ R/⟨x⟩ (toA ∘a fromA) (idCAlgHom R/⟨x⟩)
                   (isContr→isProp (initialityContr R R/⟨x⟩) _ _)

max_stars_repo_name: gmagaf/cubical

max_issues_repo_name: gmagaf/cubical

max_forks_repo_name: gmagaf/cubical


text:
------------------------------------------------------------------------
-- A variant of Induction for Set₁
------------------------------------------------------------------------

-- I want universe polymorphism.

module Induction1 where

open import Relation.Unary1

-- A RecStruct describes the allowed structure of recursion. The
-- examples in Induction.Nat should explain what this is all about.

RecStruct : Set → Set₂
RecStruct a = Pred a → Pred a

-- A recursor builder constructs an instance of a recursion structure
-- for a given input.

RecursorBuilder : ∀ {a} → RecStruct a → Set₂
RecursorBuilder {a} Rec = (P : Pred a) → Rec P ⊆′ P → Universal (Rec P)

-- A recursor can be used to actually compute/prove something useful.

Recursor : ∀ {a} → RecStruct a → Set₂
Recursor {a} Rec = (P : Pred a) → Rec P ⊆′ P → Universal P

-- And recursors can be constructed from recursor builders.

build : ∀ {a} {Rec : RecStruct a} →
        RecursorBuilder Rec →
        Recursor Rec
build builder P f x = f x (builder P f x)

-- We can repeat the exercise above for subsets of the type we are
-- recursing over.

SubsetRecursorBuilder : ∀ {a} → Pred a → RecStruct a → Set₂
SubsetRecursorBuilder {a} Q Rec = (P : Pred a) → Rec P ⊆′ P → Q ⊆′ Rec P

SubsetRecursor : ∀ {a} → Pred a → RecStruct a → Set₂
SubsetRecursor {a} Q Rec = (P : Pred a) → Rec P ⊆′ P → Q ⊆′ P

subsetBuild : ∀ {a} {Q : Pred a} {Rec : RecStruct a} →
              SubsetRecursorBuilder Q Rec →
              SubsetRecursor Q Rec
subsetBuild builder P f x q = f x (builder P f x q)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Andreas, 2012-03-09 do not solve relevant meta variable by irr. constraint
module Issue351a where

open import Common.Irrelevance
open import Common.Equality

data Bool : Set where
  true false : Bool

-- the Boolean b is not(!) constrained by the equation
f : (b : Bool) -> squash b ≡ squash true -> Bool
f b _ = b

test = f _ refl
-- meta needs to remain unsolved

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2018-06-10, issue #2797
-- Analysis and test case by Ulf

-- Relevance check was missing for overloaded projections.

{-# OPTIONS --irrelevant-projections #-}

-- {-# OPTIONS -v tc.proj.amb:30 #-}

open import Agda.Builtin.Nat

record Dummy : Set₁ where
  field nat : Set
open Dummy

record S : Set where
  field .nat : Nat
open S

mkS : Nat → S
mkS n .nat = n

-- The following should not pass, as projection
-- .nat is irrelevant for record type S

unS : S → Nat
unS s = s .nat

-- Error NOW, could be better:
-- Cannot resolve overloaded projection nat because no matching candidate found
-- when checking that the expression s .nat has type Nat

viaS : Nat → Nat
viaS n = unS (mkS n)

idN : Nat → Nat
idN zero    = zero
idN (suc n) = suc n

canonicity-fail : Nat
canonicity-fail = idN (viaS 17)
-- C-c C-n canonicity-fail
-- idN .(17)