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

module HoTT-UF-Agda where

open import Universes public

variable
 𝓤 𝓥 𝓦 𝓣 : Universe

data 𝟙 : 𝓤₀ ̇  where
 ⋆ : 𝟙

𝟙-induction : (A : 𝟙 → 𝓤 ̇ ) → A ⋆ → (x : 𝟙) → A x
𝟙-induction A a ⋆ = a

𝟙-recursion : (B : 𝓤 ̇ ) → B → (𝟙 → B)
𝟙-recursion B b x = 𝟙-induction (λ _ → B) b x

!𝟙' : (X : 𝓤 ̇ ) → X → 𝟙
!𝟙' X x = ⋆

!𝟙 : {X : 𝓤 ̇ } → X → 𝟙
!𝟙 x = ⋆

data 𝟘 : 𝓤₀ ̇  where

𝟘-induction : (A : 𝟘 → 𝓤 ̇ ) → (x : 𝟘) → A x
𝟘-induction A ()

𝟘-recursion : (A : 𝓤 ̇ ) → 𝟘 → A
𝟘-recursion A a = 𝟘-induction (λ _ → A) a

!𝟘 : (A : 𝓤 ̇ ) → 𝟘 → A
!𝟘 = 𝟘-recursion

is-empty : 𝓤 ̇ → 𝓤 ̇
is-empty X = X → 𝟘

¬ : 𝓤 ̇ → 𝓤 ̇
¬ X = X → 𝟘

data ℕ : 𝓤₀ ̇  where
 zero : ℕ
 succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

ℕ-induction : (A : ℕ → 𝓤 ̇ )
            → A 0
            → ((n : ℕ) → A n → A (succ n))
            → (n : ℕ) → A n

ℕ-induction A a₀ f = h
 where
  h : (n : ℕ) → A n
  h 0        = a₀
  h (succ n) = f n (h n)

ℕ-recursion : (X : 𝓤 ̇ )
            → X
            → (ℕ → X → X)
            → ℕ → X

ℕ-recursion X = ℕ-induction (λ _ → X)

ℕ-iteration : (X : 𝓤 ̇ )
            → X
            → (X → X)
            → ℕ → X

ℕ-iteration X x f = ℕ-recursion X x (λ _ x → f x)

module Arithmetic where

  _+_  _×_ : ℕ → ℕ → ℕ

  x + 0      = x
  x + succ y = succ (x + y)

  x × 0      = 0
  x × succ y = x + x × y

  infixl 20 _+_
  infixl 21 _×_

module Arithmetic' where

  _+_  _×_ : ℕ → ℕ → ℕ

  x + y = h y
   where
    h : ℕ → ℕ
    h = ℕ-iteration ℕ x succ

  x × y = h y
   where
    h : ℕ → ℕ
    h = ℕ-iteration ℕ 0 (x +_)

  infixl 20 _+_
  infixl 21 _×_

module ℕ-order where

  _≤_ _≥_ : ℕ → ℕ → 𝓤₀ ̇
  0      ≤ y      = 𝟙
  succ x ≤ 0      = 𝟘
  succ x ≤ succ y = x ≤ y

  x ≥ y = y ≤ x

  infix 10 _≤_
  infix 10 _≥_

data _+_ {𝓤 𝓥} (X : 𝓤 ̇ ) (Y : 𝓥 ̇ ) : 𝓤 ⊔ 𝓥 ̇  where
 inl : X → X + Y
 inr : Y → X + Y

+-induction : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (A : X + Y → 𝓦 ̇ )
            → ((x : X) → A (inl x))
            → ((y : Y) → A (inr y))
            → (z : X + Y) → A z

+-induction A f g (inl x) = f x
+-induction A f g (inr y) = g y

+-recursion : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ } → (X → A) → (Y → A) → X + Y → A
+-recursion {𝓤} {𝓥} {𝓦} {X} {Y} {A} = +-induction (λ _ → A)

𝟚 : 𝓤₀ ̇
𝟚 = 𝟙 + 𝟙

pattern ₀ = inl ⋆
pattern ₁ = inr ⋆

𝟚-induction : (A : 𝟚 → 𝓤 ̇ ) → A ₀ → A ₁ → (n : 𝟚) → A n
𝟚-induction A a₀ a₁ ₀ = a₀
𝟚-induction A a₀ a₁ ₁ = a₁

𝟚-induction' : (A : 𝟚 → 𝓤 ̇ ) → A ₀ → A ₁ → (n : 𝟚) → A n
𝟚-induction' A a₀ a₁ = +-induction A
                         (𝟙-induction (λ (x : 𝟙) → A (inl x)) a₀)
                         (𝟙-induction (λ (y : 𝟙) → A (inr y)) a₁)

record Σ {𝓤 𝓥} {X : 𝓤 ̇ } (Y : X → 𝓥 ̇ ) : 𝓤 ⊔ 𝓥 ̇  where
  constructor
   _,_
  field
   x : X
   y : Y x

pr₁ : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } → Σ Y → X
pr₁ (x , y) = x

pr₂ : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } → (z : Σ Y) → Y (pr₁ z)
pr₂ (x , y) = y

-Σ : {𝓤 𝓥 : Universe} (X : 𝓤 ̇ ) (Y : X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
-Σ X Y = Σ Y

syntax -Σ X (λ x → y) = Σ x ꞉ X , y

Σ-induction : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {A : Σ Y → 𝓦 ̇ }
            → ((x : X) (y : Y x) → A (x , y))
            → ((x , y) : Σ Y) → A (x , y)

Σ-induction g (x , y) = g x y

curry : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {A : Σ Y → 𝓦 ̇ }
      → (((x , y) : Σ Y) → A (x , y))
      → ((x : X) (y : Y x) → A (x , y))

curry f x y = f (x , y)

_×_ : 𝓤 ̇ → 𝓥 ̇ → 𝓤 ⊔ 𝓥 ̇
X × Y = Σ x ꞉ X , Y

Π : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
Π {𝓤} {𝓥} {X} A = (x : X) → A x

-Π : {𝓤 𝓥 : Universe} (X : 𝓤 ̇ ) (Y : X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
-Π X Y = Π Y

syntax -Π A (λ x → b) = Π x ꞉ A , b

id : {X : 𝓤 ̇ } → X → X
id x = x

𝑖𝑑 : (X : 𝓤 ̇ ) → X → X
𝑖𝑑 X = id

_∘_ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : Y → 𝓦 ̇ }
    → ((y : Y) → Z y)
    → (f : X → Y)
    → (x : X) → Z (f x)

g ∘ f = λ x → g (f x)

domain : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ̇
domain {𝓤} {𝓥} {X} {Y} f = X

codomain : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓥 ̇
codomain {𝓤} {𝓥} {X} {Y} f = Y

type-of : {X : 𝓤 ̇ } → X → 𝓤 ̇
type-of {𝓤} {X} x = X

data Id {𝓤} (X : 𝓤 ̇ ) : X → X → 𝓤 ̇  where
 refl : (x : X) → Id X x x

_≡_ : {X : 𝓤 ̇ } → X → X → 𝓤 ̇
x ≡ y = Id _ x y

𝕁 : (X : 𝓤 ̇ ) (A : (x y : X) → x ≡ y → 𝓥 ̇ )
  → ((x : X) → A x x (refl x))
  → (x y : X) (p : x ≡ y) → A x y p
𝕁 X A f x x (refl x) = f x

ℍ : {X : 𝓤 ̇ } (x : X) (B : (y : X) → x ≡ y → 𝓥 ̇ )
  → B x (refl x)
  → (y : X) (p : x ≡ y) → B y p
ℍ x B b x (refl x) = b

𝕁' : (X : 𝓤 ̇ ) (A : (x y : X) → x ≡ y → 𝓥 ̇ )
   → ((x : X) → A x x (refl x))
   → (x y : X) (p : x ≡ y) → A x y p
𝕁' X A f x = ℍ x (A x) (f x)

𝕁s-agreement : (X : 𝓤 ̇ ) (A : (x y : X) → x ≡ y → 𝓥 ̇ )
               (f : (x : X) → A x x (refl x)) (x y : X) (p : x ≡ y)
             → 𝕁 X A f x y p ≡ 𝕁' X A f x y p
𝕁s-agreement X A f x x (refl x) = refl (f x)

transport : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) {x y : X}
          → x ≡ y → A x → A y
transport A (refl x) = 𝑖𝑑 (A x)

transport𝕁 : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) {x y : X}
           → x ≡ y → A x → A y
transport𝕁 {𝓤} {𝓥} {X} A {x} {y} = 𝕁 X (λ x y _ → A x → A y) (λ x → 𝑖𝑑 (A x)) x y

nondep-ℍ : {X : 𝓤 ̇ } (x : X) (A : X → 𝓥 ̇ )
         → A x → (y : X) → x ≡ y → A y
nondep-ℍ x A = ℍ x (λ y _ → A y)

transportℍ : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) {x y : X}
           → x ≡ y → A x → A y
transportℍ A {x} {y} p a = nondep-ℍ x A a y p

transports-agreement : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) {x y : X} (p : x ≡ y)
                     → (transportℍ A p ≡ transport A p)
                     × (transport𝕁 A p ≡ transport A p)
transports-agreement A (refl x) = refl (transport A (refl x)) ,
                                  refl (transport A (refl x))

lhs : {X : 𝓤 ̇ } {x y : X} → x ≡ y → X
lhs {𝓤} {X} {x} {y} p = x

rhs : {X : 𝓤 ̇ } {x y : X} → x ≡ y → X
rhs {𝓤} {X} {x} {y} p = y

_∙_ : {X : 𝓤 ̇ } {x y z : X} → x ≡ y → y ≡ z → x ≡ z
p ∙ q = transport (lhs p ≡_) q p

_≡⟨_⟩_ : {X : 𝓤 ̇ } (x : X) {y z : X} → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ p ⟩ q = p ∙ q

_∎ : {X : 𝓤 ̇ } (x : X) → x ≡ x
x ∎ = refl x

_⁻¹ : {X : 𝓤 ̇ } → {x y : X} → x ≡ y → y ≡ x
p ⁻¹ = transport (_≡ lhs p) p (refl (lhs p))

_∙'_ : {X : 𝓤 ̇ } {x y z : X} → x ≡ y → y ≡ z → x ≡ z
p ∙' q = transport (_≡ rhs q) (p ⁻¹) q

∙agreement : {X : 𝓤 ̇ } {x y z : X} (p : x ≡ y) (q : y ≡ z)
          → (p ∙' q) ≡ (p ∙ q)
∙agreement (refl x) (refl x) = refl (refl x)

rdnel : {X : 𝓤 ̇ } {x y : X} (p : x ≡ y)
      → (p ∙ refl y) ≡ p

rdnel p = refl p

rdner : {X : 𝓤 ̇ } {y z : X} (q : y ≡ z)
      → (refl y  ∙' q) ≡ q

rdner q = refl q

ap : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) {x x' : X} → x ≡ x' → f x ≡ f x'
ap f {x} {x'} p = transport (λ - → f x ≡ f -) p (refl (f x))

_∼_ : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } → Π A → Π A → 𝓤 ⊔ 𝓥 ̇
f ∼ g = ∀ x → f x ≡ g x

¬¬ ¬¬¬ : 𝓤 ̇ → 𝓤 ̇
¬¬  A = ¬(¬ A)
¬¬¬ A = ¬(¬¬ A)

dni : (A : 𝓤 ̇ ) → A → ¬¬ A
dni A a u = u a

contrapositive : {A : 𝓤 ̇ } {B : 𝓥 ̇ } → (A → B) → (¬ B → ¬ A)
contrapositive f v a = v (f a)

tno : (A : 𝓤 ̇ ) → ¬¬¬ A → ¬ A
tno A = contrapositive (dni A)

_⇔_ : 𝓤 ̇ → 𝓥 ̇ → 𝓤 ⊔ 𝓥 ̇
X ⇔ Y = (X → Y) × (Y → X)

lr-implication : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X ⇔ Y) → (X → Y)
lr-implication = pr₁

rl-implication : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X ⇔ Y) → (Y → X)
rl-implication = pr₂

absurdity³-is-absurdity : {A : 𝓤 ̇ } → ¬¬¬ A ⇔ ¬ A
absurdity³-is-absurdity {𝓤} {A} = firstly , secondly
 where
  firstly : ¬¬¬ A → ¬ A
  firstly = contrapositive (dni A)

  secondly : ¬ A → ¬¬¬ A
  secondly = dni (¬ A)

_≢_ : {X : 𝓤 ̇ } → X → X → 𝓤 ̇
x ≢ y = ¬(x ≡ y)

≢-sym : {X : 𝓤 ̇ } {x y : X} → x ≢ y → y ≢ x
≢-sym {𝓤} {X} {x} {y} u = λ (p : y ≡ x) → u (p ⁻¹)

Id→Fun : {X Y : 𝓤 ̇ } → X ≡ Y → X → Y
Id→Fun {𝓤} = transport (𝑖𝑑 (𝓤 ̇ ))

Id→Fun' : {X Y : 𝓤 ̇ } → X ≡ Y → X → Y
Id→Fun' (refl X) = 𝑖𝑑 X

Id→Funs-agree : {X Y : 𝓤 ̇ } (p : X ≡ Y)
              → Id→Fun p ≡ Id→Fun' p

Id→Funs-agree (refl X) = refl (𝑖𝑑 X)

𝟙-is-not-𝟘 : 𝟙 ≢ 𝟘
𝟙-is-not-𝟘 p = Id→Fun p ⋆

₁-is-not-₀ : ₁ ≢ ₀
₁-is-not-₀ p = 𝟙-is-not-𝟘 q
 where
  f : 𝟚 → 𝓤₀ ̇
  f ₀ = 𝟘
  f ₁ = 𝟙

  q : 𝟙 ≡ 𝟘
  q = ap f p

₁-is-not-₀[not-an-MLTT-proof] : ¬(₁ ≡ ₀)
₁-is-not-₀[not-an-MLTT-proof] ()

decidable : 𝓤 ̇ → 𝓤 ̇
decidable A = A + ¬ A

has-decidable-equality : 𝓤 ̇ → 𝓤 ̇
has-decidable-equality X = (x y : X) → decidable (x ≡ y)

𝟚-has-decidable-equality : has-decidable-equality 𝟚
𝟚-has-decidable-equality ₀ ₀ = inl (refl ₀)
𝟚-has-decidable-equality ₀ ₁ = inr (≢-sym ₁-is-not-₀)
𝟚-has-decidable-equality ₁ ₀ = inr ₁-is-not-₀
𝟚-has-decidable-equality ₁ ₁ = inl (refl ₁)

not-zero-is-one : (n : 𝟚) → n ≢ ₀ → n ≡ ₁
not-zero-is-one ₀ f = !𝟘 (₀ ≡ ₁) (f (refl ₀))
not-zero-is-one ₁ f = refl ₁

inl-inr-disjoint-images : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {x : X} {y : Y} → inl x ≢ inr y
inl-inr-disjoint-images {𝓤} {𝓥} {X} {Y} p = 𝟙-is-not-𝟘 q
 where
  f : X + Y → 𝓤₀ ̇
  f (inl x) = 𝟙
  f (inr y) = 𝟘

  q : 𝟙 ≡ 𝟘
  q = ap f p

right-fails-gives-left-holds : {P : 𝓤 ̇ } {Q : 𝓥 ̇ } → P + Q → ¬ Q → P
right-fails-gives-left-holds (inl p) u = p
right-fails-gives-left-holds (inr q) u = !𝟘 _ (u q)

module twin-primes where

 open Arithmetic renaming (_×_ to _*_ ; _+_ to _∔_)
 open ℕ-order

 is-prime : ℕ → 𝓤₀ ̇
 is-prime n = (n ≥ 2) × ((x y : ℕ) → x * y ≡ n → (x ≡ 1) + (x ≡ n))

 twin-prime-conjecture : 𝓤₀ ̇
 twin-prime-conjecture =
                       (n : ℕ) → -Σ ℕ (λ p → ((p ≥ n) × is-prime p) × is-prime (p ∔ 2))

positive-not-zero : (x : ℕ) → succ x ≢ 0
positive-not-zero x p = 𝟙-is-not-𝟘 q where
  f : ℕ →  𝓤₀ ̇
  f zero = 𝟘
  f (succ n) = 𝟙

  q : 𝟙 ≡ 𝟘
  q = ap f p

pred : ℕ → ℕ
pred 0        = 0
pred (succ n) = n

succ-lc : {x y : ℕ} → succ x ≡ succ y → x ≡ y
succ-lc = ap pred

ℕ-has-decidable-equality : has-decidable-equality ℕ
ℕ-has-decidable-equality 0 0               = inl (refl 0)
ℕ-has-decidable-equality 0 (succ y)        = inr (≢-sym (positive-not-zero y))
ℕ-has-decidable-equality (succ x) 0        = inr (positive-not-zero x)
ℕ-has-decidable-equality (succ x) (succ y) = f (ℕ-has-decidable-equality x y)
 where
  f : decidable (x ≡ y) → decidable (succ x ≡ succ y)
  f (inl p) = inl (ap succ p)
  f (inr k) = inr (λ (s : succ x ≡ succ y) → k (succ-lc s))

module basic-arithmetic-and-order where

  open ℕ-order public
  open Arithmetic renaming (_+_ to _∔_) hiding (_×_)

  +-assoc : (x y z : ℕ) → ((x ∔ y) ∔ z) ≡ (x ∔ (y ∔ z))
  +-assoc x y zero     =  ((x ∔ y) ∔ 0) ≡⟨ (refl _) ⟩
                          (x ∔ (y ∔ 0)) ∎

  +-assoc x y (succ z) = ((x ∔ y) ∔ succ z)   ≡⟨ (refl _)     ⟩
                         (succ ((x ∔ y) ∔ z)) ≡⟨ ap succ IH ⟩
                         (succ (x ∔ (y ∔ z))) ≡⟨ refl _     ⟩
                         (x ∔ (y ∔ succ z))   ∎
   where
    IH : ((x ∔ y) ∔ z) ≡ (x ∔ (y ∔ z))
    IH = +-assoc x y z

  +-base-on-first : (x : ℕ) → 0 ∔ x ≡ x
  +-base-on-first 0        = refl 0
  +-base-on-first (succ x) = 0 ∔ succ x   ≡⟨ refl _     ⟩
                             succ (0 ∔ x) ≡⟨ ap succ IH ⟩
                             succ x       ∎
   where
    IH : 0 ∔ x ≡ x
    IH = +-base-on-first x

  +-step-on-first : (x y : ℕ) → succ x ∔ y ≡ succ (x ∔ y)
  +-step-on-first x zero     = refl (succ x)
  +-step-on-first x (succ y) = succ x ∔ succ y   ≡⟨ refl _     ⟩
                               succ (succ x ∔ y) ≡⟨ ap succ IH ⟩
                               succ (x ∔ succ y) ∎
   where
    IH : succ x ∔ y ≡ succ (x ∔ y)
    IH = +-step-on-first x y

  +-comm : (x y : ℕ) → x ∔ y ≡ y ∔ x
  +-comm 0 y = 0 ∔ y ≡⟨ +-base-on-first y ⟩
               y     ≡⟨ refl _ ⟩
               y ∔ 0 ∎
  +-comm (succ x) y = succ x ∔ y  ≡⟨ +-step-on-first x y ⟩
                      succ(x ∔ y) ≡⟨ ap succ IH          ⟩
                      succ(y ∔ x) ≡⟨ refl _              ⟩
                      y ∔ succ x  ∎
    where
     IH : x ∔ y ≡ y ∔ x
     IH = +-comm x y

  +-lc : (x y z : ℕ) → x ∔ y ≡ x ∔ z → y ≡ z
  +-lc 0        y z p = y     ≡⟨ (+-base-on-first y)⁻¹ ⟩
                        0 ∔ y ≡⟨ p                     ⟩
                        0 ∔ z ≡⟨ +-base-on-first z     ⟩
                        z     ∎
  +-lc (succ x) y z p = IH
   where
    q = succ (x ∔ y) ≡⟨ (+-step-on-first x y)⁻¹ ⟩
        succ x ∔ y   ≡⟨ p                       ⟩
        succ x ∔ z   ≡⟨ +-step-on-first x z     ⟩
        succ (x ∔ z) ∎

    IH : y ≡ z
    IH = +-lc x y z (succ-lc q)

  _≼_ : ℕ → ℕ → 𝓤₀ ̇
  x ≼ y = Σ z ꞉ ℕ , x ∔ z ≡ y

  ≤-gives-≼ : (x y : ℕ) → x ≤ y → x ≼ y
  ≤-gives-≼ 0 0               l = 0 , refl 0
  ≤-gives-≼ 0 (succ y)        l = succ y , +-base-on-first (succ y)
  ≤-gives-≼ (succ x) 0        l = !𝟘 (succ x ≼ zero) l
  ≤-gives-≼ (succ x) (succ y) l = γ
   where
    IH : x ≼ y
    IH = ≤-gives-≼ x y l

    z : ℕ
    z = pr₁ IH

    p : x ∔ z ≡ y
    p = pr₂ IH

    γ : succ x ≼ succ y
    γ = z , (succ x ∔ z   ≡⟨ +-step-on-first x z ⟩
             succ (x ∔ z) ≡⟨ ap succ p           ⟩
             succ y       ∎)

  ≼-gives-≤ : (x y : ℕ) → x ≼ y → x ≤ y
  ≼-gives-≤ 0 0               (z , p) = ⋆
  ≼-gives-≤ 0 (succ y)        (z , p) = ⋆
  ≼-gives-≤ (succ x) 0        (z , p) = positive-not-zero (x ∔ z) q
   where
    q = succ (x ∔ z) ≡⟨ (+-step-on-first x z)⁻¹ ⟩
        succ x ∔ z   ≡⟨ p                       ⟩
        zero         ∎
  ≼-gives-≤ (succ x) (succ y) (z , p) = IH
   where
    q = succ (x ∔ z) ≡⟨ (+-step-on-first x z)⁻¹ ⟩
        succ x ∔ z   ≡⟨ p                       ⟩
        succ y       ∎

    IH : x ≤ y
    IH = ≼-gives-≤ x y (z , succ-lc q)

  ≤-refl : (n : ℕ) → n ≤ n
  ≤-refl zero     = ⋆
  ≤-refl (succ n) = ≤-refl n

  ≤-trans : (l m n : ℕ) → l ≤ m → m ≤ n → l ≤ n
  ≤-trans zero     m        n        p q = ⋆
  ≤-trans (succ l) zero     n        p q = !𝟘 (succ l ≤ n) p
  ≤-trans (succ l) (succ m) zero     p q = q
  ≤-trans (succ l) (succ m) (succ n) p q = ≤-trans l m n p q

  ≤-anti : (m n : ℕ) → m ≤ n → n ≤ m → m ≡ n
  ≤-anti zero     zero     p q = refl zero
  ≤-anti zero     (succ n) p q = !𝟘 (zero ≡ succ n) q
  ≤-anti (succ m) zero     p q = !𝟘 (succ m ≡ zero) p
  ≤-anti (succ m) (succ n) p q = ap succ (≤-anti m n p q)

  ≤-succ : (n : ℕ) → n ≤ succ n
  ≤-succ zero     = ⋆
  ≤-succ (succ n) = ≤-succ n

  zero-minimal : (n : ℕ) → zero ≤ n
  zero-minimal n = ⋆

  unique-minimal : (n : ℕ) → n ≤ zero → n ≡ zero
  unique-minimal zero     p = refl zero
  unique-minimal (succ n) p = !𝟘 (succ n ≡ zero) p

  ≤-split : (m n : ℕ) → m ≤ succ n → (m ≤ n) + (m ≡ succ n)
  ≤-split zero     n        l = inl l
  ≤-split (succ m) zero     l = inr (ap succ (unique-minimal m l))
  ≤-split (succ m) (succ n) l = +-recursion inl (inr ∘ ap succ) (≤-split m n l)

  _<_ : ℕ → ℕ → 𝓤₀ ̇
  x < y = succ x ≤ y

  infix 10 _<_

  not-<-gives-≥ : (m n : ℕ) → ¬(n < m) → m ≤ n
  not-<-gives-≥ zero     n        u = zero-minimal n
  not-<-gives-≥ (succ m) zero     u = dni (zero < succ m) (zero-minimal m) u
  not-<-gives-≥ (succ m) (succ n) u = not-<-gives-≥ m n u

  bounded-∀-next : (A : ℕ → 𝓤 ̇ ) (k : ℕ)
                 → A k
                 → ((n : ℕ) → n < k → A n)
                 → (n : ℕ) → n < succ k → A n
  bounded-∀-next A k a φ n l = +-recursion f g s
   where
    s : (n < k) + (succ n ≡ succ k)
    s = ≤-split (succ n) k l

    f : n < k → A n
    f = φ n

    g : succ n ≡ succ k → A n
    g p = transport A ((succ-lc p)⁻¹) a

  root : (ℕ → ℕ) → 𝓤₀ ̇
  root f = Σ n ꞉ ℕ , f n ≡ 0

  _has-no-root<_ : (ℕ → ℕ) → ℕ → 𝓤₀ ̇
  f has-no-root< k = (n : ℕ) → n < k → f n ≢ 0

  is-minimal-root : (ℕ → ℕ) → ℕ → 𝓤₀ ̇
  is-minimal-root f m = (f m ≡ 0) × (f has-no-root< m)

  at-most-one-minimal-root : (f : ℕ → ℕ) (m n : ℕ)
                           → is-minimal-root f m → is-minimal-root f n → m ≡ n

  at-most-one-minimal-root f m n (p , φ) (q , ψ) = c m n a b
   where
    a : ¬(m < n)
    a u = ψ m u p

    b : ¬(n < m)
    b v = φ n v q

    c : (m n : ℕ) → ¬(m < n) → ¬(n < m) → m ≡ n
    c m n u v = ≤-anti m n (not-<-gives-≥ m n v) (not-<-gives-≥ n m u)

  minimal-root : (ℕ → ℕ) → 𝓤₀ ̇
  minimal-root f = Σ m ꞉ ℕ , is-minimal-root f m

  minimal-root-is-root : ∀ f → minimal-root f → root f
  minimal-root-is-root f (m , p , _) = m , p

  bounded-ℕ-search : ∀ k f → (minimal-root f) + (f has-no-root< k)
  bounded-ℕ-search zero f = inr (λ n → !𝟘 (f n ≢ 0))
  bounded-ℕ-search (succ k) f = +-recursion φ γ (bounded-ℕ-search k f)
   where
    A : ℕ → (ℕ → ℕ) → 𝓤₀ ̇
    A k f = (minimal-root f) + (f has-no-root< k)

    φ : minimal-root f → A (succ k) f
    φ = inl

    γ : f has-no-root< k → A (succ k) f
    γ u = +-recursion γ₀ γ₁ (ℕ-has-decidable-equality (f k) 0)
     where
      γ₀ : f k ≡ 0 → A (succ k) f
      γ₀ p = inl (k , p , u)

      γ₁ : f k ≢ 0 → A (succ k) f
      γ₁ v = inr (bounded-∀-next (λ n → f n ≢ 0) k v u)

  root-gives-minimal-root : ∀ f → root f → minimal-root f
  root-gives-minimal-root f (n , p) = γ
   where
    g : ¬(f has-no-root< (succ n))
    g φ = φ n (≤-refl n) p

    γ : minimal-root f
    γ = right-fails-gives-left-holds (bounded-ℕ-search (succ n) f) g

is-singleton : 𝓤 ̇ → 𝓤 ̇
is-singleton X = Σ c ꞉ X , ((x : X) → c ≡ x)

is-center : (X : 𝓤 ̇ ) → X → 𝓤 ̇
is-center X c = (x : X) → c ≡ x

𝟙-is-singleton : is-singleton 𝟙
𝟙-is-singleton = ⋆ , λ x → 𝟙-induction (λ y → ⋆ ≡ y) (refl ⋆) x

center : (X : 𝓤 ̇ ) → is-singleton X → X
center X (c , φ) = c

centrality : (X : 𝓤 ̇ ) (i : is-singleton X) (x : X) → center X i ≡ x
centrality X (c , φ) = φ

is-subsingleton : 𝓤 ̇ → 𝓤 ̇
is-subsingleton X = (x y : X) → x ≡ y

𝟘-is-subsingleton : is-subsingleton 𝟘
𝟘-is-subsingleton x y = !𝟘 (x ≡ y) x

singletons-are-subsingletons : (X : 𝓤 ̇ ) → is-singleton X → is-subsingleton X
singletons-are-subsingletons X (c , φ) x y = x ≡⟨ (φ x)⁻¹ ⟩
                                             c ≡⟨ φ y     ⟩
                                             y ∎

𝟙-is-subsingleton : is-subsingleton 𝟙
𝟙-is-subsingleton = singletons-are-subsingletons 𝟙 𝟙-is-singleton

pointed-subsingletons-are-singletons : (X : 𝓤 ̇ )
                                     → X → is-subsingleton X → is-singleton X

pointed-subsingletons-are-singletons X x s = (x , s x)

singleton-iff-pointed-and-subsingleton : {X : 𝓤 ̇ }
                                       → is-singleton X ⇔ (X × is-subsingleton X)

singleton-iff-pointed-and-subsingleton {𝓤} {X} = (a , b)
 where
  a : is-singleton X → X × is-subsingleton X
  a s = center X s , singletons-are-subsingletons X s

  b : X × is-subsingleton X → is-singleton X
  b (x , t) = pointed-subsingletons-are-singletons X x t

is-prop is-truth-value : 𝓤 ̇ → 𝓤 ̇
is-prop        = is-subsingleton
is-truth-value = is-subsingleton

is-set : 𝓤 ̇ → 𝓤 ̇
is-set X = (x y : X) → is-subsingleton (x ≡ y)

EM EM' : ∀ 𝓤 → 𝓤 ⁺ ̇
EM  𝓤 = (X : 𝓤 ̇ ) → is-subsingleton X → X + ¬ X
EM' 𝓤 = (X : 𝓤 ̇ ) → is-subsingleton X → is-singleton X + is-empty X

EM-gives-EM' : EM 𝓤 → EM' 𝓤
EM-gives-EM' em X s = γ (em X s)
 where
  γ : X + ¬ X → is-singleton X + is-empty X
  γ (inl x) = inl (pointed-subsingletons-are-singletons X x s)
  γ (inr x) = inr x

EM'-gives-EM : EM' 𝓤 → EM 𝓤
EM'-gives-EM em' X s = γ (em' X s)
 where
  γ : is-singleton X + is-empty X → X + ¬ X
  γ (inl i) = inl (center X i)
  γ (inr x) = inr x

no-unicorns : ¬(Σ X ꞉ 𝓤 ̇ , is-subsingleton X × ¬(is-singleton X) × ¬(is-empty X))
no-unicorns (X , i , f , g) = c
 where
  e : is-empty X
  e x = f (pointed-subsingletons-are-singletons X x i)

  c : 𝟘
  c = g e

module magmas where

 Magma : (𝓤 : Universe) → 𝓤 ⁺ ̇
 Magma 𝓤 = Σ X ꞉ 𝓤 ̇ , is-set X × (X → X → X)

 ⟨_⟩ : Magma 𝓤 → 𝓤 ̇
 ⟨ X , i , _·_ ⟩ = X

 magma-is-set : (M : Magma 𝓤) → is-set ⟨ M ⟩
 magma-is-set (X , i , _·_) = i

 magma-operation : (M : Magma 𝓤) → ⟨ M ⟩ → ⟨ M ⟩ → ⟨ M ⟩
 magma-operation (X , i , _·_) = _·_

 syntax magma-operation M x y = x ·⟨ M ⟩ y

 is-magma-hom : (M N : Magma 𝓤) → (⟨ M ⟩ → ⟨ N ⟩) → 𝓤 ̇
 is-magma-hom M N f = (x y : ⟨ M ⟩) → f (x ·⟨ M ⟩ y) ≡ f x ·⟨ N ⟩ f y

 id-is-magma-hom : (M : Magma 𝓤) → is-magma-hom M M (𝑖𝑑 ⟨ M ⟩)
 id-is-magma-hom M = λ (x y : ⟨ M ⟩) → refl (x ·⟨ M ⟩ y)

 is-magma-iso : (M N : Magma 𝓤) → (⟨ M ⟩ → ⟨ N ⟩) → 𝓤 ̇
 is-magma-iso M N f = is-magma-hom M N f
                    × (Σ g ꞉ (⟨ N ⟩ → ⟨ M ⟩), is-magma-hom N M g
                                            × (g ∘ f ∼ 𝑖𝑑 ⟨ M ⟩)
                                            × (f ∘ g ∼ 𝑖𝑑 ⟨ N ⟩))

 id-is-magma-iso : (M : Magma 𝓤) → is-magma-iso M M (𝑖𝑑 ⟨ M ⟩)
 id-is-magma-iso M = id-is-magma-hom M ,
                     𝑖𝑑 ⟨ M ⟩ ,
                     id-is-magma-hom M ,
                     refl ,
                     refl

 Id→iso : {M N : Magma 𝓤} → M ≡ N → ⟨ M ⟩ → ⟨ N ⟩
 Id→iso p = transport ⟨_⟩ p

 Id→iso-is-iso : {M N : Magma 𝓤} (p : M ≡ N) → is-magma-iso M N (Id→iso p)
 Id→iso-is-iso (refl M) = id-is-magma-iso M

 _≅ₘ_ : Magma 𝓤 → Magma 𝓤 → 𝓤 ̇
 M ≅ₘ N = Σ f ꞉ (⟨ M ⟩ → ⟨ N ⟩), is-magma-iso M N f

 magma-Id→iso : {M N : Magma 𝓤} → M ≡ N → M ≅ₘ N
 magma-Id→iso p = Id→iso p , Id→iso-is-iso p

 ∞-Magma : (𝓤 : Universe) → 𝓤 ⁺ ̇
 ∞-Magma 𝓤 = Σ X ꞉ 𝓤 ̇ , (X → X → X)

module monoids where

 left-neutral : {X : 𝓤 ̇ } → X → (X → X → X) → 𝓤 ̇
 left-neutral e _·_ = ∀ x → e · x ≡ x

 right-neutral : {X : 𝓤 ̇ } → X → (X → X → X) → 𝓤 ̇
 right-neutral e _·_ = ∀ x → x · e ≡ x

 associative : {X : 𝓤 ̇ } → (X → X → X) → 𝓤 ̇
 associative _·_ = ∀ x y z → (x · y) · z ≡ x · (y · z)

 Monoid : (𝓤 : Universe) → 𝓤 ⁺ ̇
 Monoid 𝓤 = Σ X ꞉ 𝓤  ̇ , is-set X
                      × (Σ · ꞉ (X → X → X) , (Σ e ꞉ X , (left-neutral e ·)
                                                      × (right-neutral e ·)
                                                      × (associative ·)))

module groups where

 left-neutral : {X : 𝓤 ̇ } → X → (X → X → X) → 𝓤 ̇
 left-neutral e _·_ = ∀ x → e · x ≡ x

 right-neutral : {X : 𝓤 ̇ } → X → (X → X → X) → 𝓤 ̇
 right-neutral e _·_ = ∀ x → x · e ≡ x

 associative : {X : 𝓤 ̇ } → (X → X → X) → 𝓤 ̇
 associative _·_ = ∀ x y z → (x · y) · z ≡ x · (y · z)

 inverse : {X : 𝓤 ̇ } → X → (X → X → X) → 𝓤 ̇
 inverse e _·_ = ∀ x → Σ (λ x' → x · x' ≡ e)

 Monoid : (𝓤 : Universe) → 𝓤 ⁺ ̇
 Monoid 𝓤 = Σ X ꞉ 𝓤  ̇ , is-set X
                      × (Σ · ꞉ (X → X → X) , (Σ e ꞉ X , (left-neutral e ·)
                                                      × (right-neutral e ·)
                                                      × (associative ·)
                                                      × (inverse e ·)))

refl-left : {X : 𝓤 ̇ } {x y : X} {p : x ≡ y} → refl x ∙ p ≡ p
refl-left {𝓤} {X} {x} {x} {refl x} = refl (refl x)

refl-right : {X : 𝓤 ̇ } {x y : X} {p : x ≡ y} → p ∙ refl y ≡ p
refl-right {𝓤} {X} {x} {y} {p} = refl p

∙assoc : {X : 𝓤 ̇ } {x y z t : X} (p : x ≡ y) (q : y ≡ z) (r : z ≡ t)
       → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
∙assoc p q (refl z) = refl (p ∙ q)

⁻¹-left∙ : {X : 𝓤 ̇ } {x y : X} (p : x ≡ y)
         → p ⁻¹ ∙ p ≡ refl y
⁻¹-left∙ (refl x) = refl (refl x)

⁻¹-right∙ : {X : 𝓤 ̇ } {x y : X} (p : x ≡ y)
          → p ∙ p ⁻¹ ≡ refl x
⁻¹-right∙ (refl x) = refl (refl x)

⁻¹-involutive : {X : 𝓤 ̇ } {x y : X} (p : x ≡ y)
              → (p ⁻¹)⁻¹ ≡ p
⁻¹-involutive (refl x) = refl (refl x)

ap-refl : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) (x : X)
        → ap f (refl x) ≡ refl (f x)
ap-refl f x = refl (refl (f x))

ap-∙ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) {x y z : X} (p : x ≡ y) (q : y ≡ z)
     → ap f (p ∙ q) ≡ ap f p ∙ ap f q
ap-∙ f p (refl y) = refl (ap f p)

ap⁻¹ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) {x y : X} (p : x ≡ y)
     → (ap f p)⁻¹ ≡ ap f (p ⁻¹)
ap⁻¹ f (refl x) = refl (refl (f x))

ap-id : {X : 𝓤 ̇ } {x y : X} (p : x ≡ y)
      → ap id p ≡ p
ap-id (refl x) = refl (refl x)

ap-∘ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
       (f : X → Y) (g : Y → Z) {x y : X} (p : x ≡ y)
     → ap (g ∘ f) p ≡ (ap g ∘ ap f) p
ap-∘ f g (refl x) = refl (refl (g (f x)))

transport∙ : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) {x y z : X} (p : x ≡ y) (q : y ≡ z)
           → transport A (p ∙ q) ≡ transport A q ∘ transport A p
transport∙ A p (refl y) = refl (transport A p)

Nat : {X : 𝓤 ̇ } → (X → 𝓥 ̇ ) → (X → 𝓦 ̇ ) → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ̇
Nat A B = (x : domain A) → A x → B x

Nats-are-natural : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (τ : Nat A B)
                 → {x y : X} (p : x ≡ y)
                 → τ y ∘ transport A p ≡ transport B p ∘ τ x
Nats-are-natural A B τ (refl x) = refl (τ x)

NatΣ : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {B : X → 𝓦 ̇ } → Nat A B → Σ A → Σ B
NatΣ τ (x , a) = (x , τ x a)

transport-ap : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (A : Y → 𝓦 ̇ )
               (f : X → Y) {x x' : X} (p : x ≡ x') (a : A (f x))
             → transport (A ∘ f) p a ≡ transport A (ap f p) a
transport-ap A f (refl x) a = refl a

data Color : 𝓤₀ ̇  where
 Black White : Color

apd : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } (f : (x : X) → A x) {x y : X}
      (p : x ≡ y) → transport A p (f x) ≡ f y
apd f (refl _) = refl (f _)

module Exercise where

  ≤ : ℕ → ℕ → 𝓤₀ ̇
  ≤ x = ℕ-induction (λ _ → ℕ → 𝓤₀ ̇) (λ _ → 𝟙)
                     (λ _ f x₂ → ℕ-induction (λ _ →  𝓤₀ ̇) 𝟘 (λ n _ → f n) x₂) x

  ℍ' : {X : 𝓤 ̇ } (x : X) (B : (y : X) → x ≡ y → 𝓥 ̇ )
    → B x (refl x)
    → (y : X) (p : x ≡ y) → B y p
  ℍ' {X} x B b y p = {!!}

  ℕ-has-decidable-equality' : has-decidable-equality ℕ
  ℕ-has-decidable-equality' = ℕ-induction (λ z → (x : ℕ) → Id ℕ z x + (z ≢ x))
                                          (λ m → ℕ-induction
                                                 (λ x → Id ℕ zero x + (zero ≢ x))
                                                 (inl (refl zero))
                                                 (λ n _ → inr (λ ())) m)
                                          λ n f → ℕ-induction (λ x → Id ℕ (succ n) x + (succ n ≢ x))
                                                    (inr (λ ()))
                                                    λ n₁ x → g (f n₁)
                              where
                              g : {x y : ℕ} → decidable (x ≡ y) → decidable (succ x ≡ succ y)
                              g (inl p) = inl (ap succ p)
                              g {x} {y} (inr k) = inr (λ (s : succ x ≡ succ y) → k (succ-lc s))

  Sub-EM Sub-EM' : ∀ 𝓤 → 𝓤 ⁺ ̇
  Sub-EM 𝓤 = (X : 𝓤 ̇ ) → is-subsingleton X → ¬¬(is-singleton X + is-empty X)
  Sub-EM' 𝓤 = ¬¬((X : 𝓤 ̇ ) → is-subsingleton X → is-singleton X + is-empty X)

  Sub-EM-gives-Sub-EM' : Sub-EM 𝓤 → Sub-EM' 𝓤
  Sub-EM-gives-Sub-EM' {𝓤} sub neg = {!!}

  Sub-EM'-gives-Sub-EM : Sub-EM' 𝓤 → Sub-EM 𝓤
  Sub-EM'-gives-Sub-EM sub' X subsing neg = sub' λ z → neg (z X subsing)

  ∙assoc' : {X : 𝓤 ̇ } {x y z t : X} (p : x ≡ y) (q : y ≡ z) (r : z ≡ t)
          → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
  ∙assoc' p q r = {!𝕁!}

infix   0 _∼_
infixr 50 _,_
infixr 30 _×_
infixr 20 _+_
infixl 70 _∘_
infix   0 Id
infix   0 _≡_
infix  10 _⇔_
infixl 30 _∙_
infixr  0 _≡⟨_⟩_
infix   1 _∎
infix  40 _⁻¹
infix  10 _◁_
infixr  0 _◁⟨_⟩_
infix   1 _◀
infix  10 _≃_
infixl 30 _●_
infixr  0 _≃⟨_⟩_
infix   1 _■
infix  40 _∈_
infix  30 _[_,_]
infixr -1 -Σ
infixr -1 -Π
infixr -1 -∃!

max_stars_repo_name: UnsoundWitch/proofs

max_issues_repo_name: sym-cereal/proofs

max_forks_repo_name: sym-cereal/proofs


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

open import Prelude
open import Relation.Binary

module Relation.Binary.Construct.LowerBound {e} {E : Type e} {r₁ r₂} (totalOrder : TotalOrder E r₁ r₂) where

open TotalOrder totalOrder renaming (refl to <-refl)
import Data.Unit.UniversePolymorphic as Poly
import Data.Empty.UniversePolymorphic as Poly

data ⌊∙⌋ : Type e where
  ⌊⊥⌋ : ⌊∙⌋
  ⌊_⌋ : E → ⌊∙⌋

⌊_⌋≤_ : E → ⌊∙⌋ → Type _
⌊ x ⌋≤ ⌊⊥⌋ = Poly.⊥
⌊ x ⌋≤ ⌊ y ⌋ = x ≤ y

_⌊≤⌋_ : ⌊∙⌋ → ⌊∙⌋ → Type _
⌊⊥⌋   ⌊≤⌋ y = Poly.⊤
⌊ x ⌋ ⌊≤⌋ y = ⌊ x ⌋≤ y

_<⌊_⌋ : ⌊∙⌋ → E → Type _
⌊⊥⌋   <⌊ y ⌋ = Poly.⊤
⌊ x ⌋ <⌊ y ⌋ = x < y

_⌊<⌋_ : ⌊∙⌋ → ⌊∙⌋ → Type _
_     ⌊<⌋ ⌊⊥⌋   = Poly.⊥
x     ⌊<⌋ ⌊ y ⌋ = x <⌊ y ⌋

lb-pord : PartialOrder ⌊∙⌋ _
Preorder._≤_   (PartialOrder.preorder lb-pord) = _⌊≤⌋_
Preorder.refl  (PartialOrder.preorder lb-pord) {⌊⊥⌋} = _
Preorder.refl  (PartialOrder.preorder lb-pord) {⌊ x ⌋} = <-refl
Preorder.trans (PartialOrder.preorder lb-pord) {⌊⊥⌋} {_} {_} p q = _
Preorder.trans (PartialOrder.preorder lb-pord) {⌊ x ⌋} {⌊ y ⌋} {⌊ z ⌋} p q = ≤-trans p q
PartialOrder.antisym lb-pord {⌊⊥⌋} {⌊⊥⌋} p q = refl
PartialOrder.antisym lb-pord {⌊ x ⌋} {⌊ x₁ ⌋} p q = cong ⌊_⌋ (antisym p q)

lb-sord : StrictPartialOrder ⌊∙⌋ _
StrictPreorder._<_   (StrictPartialOrder.strictPreorder lb-sord) = _⌊<⌋_
StrictPreorder.trans (StrictPartialOrder.strictPreorder lb-sord) {⌊⊥⌋} {⌊⊥⌋} {⌊⊥⌋} p q = q
StrictPreorder.trans (StrictPartialOrder.strictPreorder lb-sord) {⌊⊥⌋} {⌊⊥⌋} {⌊ x ⌋} p q = q
StrictPreorder.trans (StrictPartialOrder.strictPreorder lb-sord) {⌊⊥⌋} {⌊ x ⌋} {⌊ x₁ ⌋} p q = p
StrictPreorder.trans (StrictPartialOrder.strictPreorder lb-sord) {⌊ x ⌋} {⌊ x₁ ⌋} {⌊ x₂ ⌋} p q = <-trans p q
StrictPreorder.irrefl  (StrictPartialOrder.strictPreorder lb-sord) {⌊ x ⌋} = irrefl {x = x}
StrictPartialOrder.conn  lb-sord {⌊⊥⌋} {⌊⊥⌋} p q = refl
StrictPartialOrder.conn  lb-sord {⌊⊥⌋} {⌊ x ⌋} p q = ⊥-elim (p _)
StrictPartialOrder.conn  lb-sord {⌊ x ⌋} {⌊⊥⌋} p q = ⊥-elim (q _)
StrictPartialOrder.conn  lb-sord {⌊ x ⌋} {⌊ x₁ ⌋} p q = cong ⌊_⌋ (conn p q)

lb-lt : ∀ x y → Dec (x ⌊<⌋ y)
lb-lt x ⌊⊥⌋ = no (λ ())
lb-lt ⌊⊥⌋ ⌊ y ⌋ = yes Poly.tt
lb-lt ⌊ x ⌋ ⌊ y ⌋ = x <? y

lb-ord : TotalOrder ⌊∙⌋ _ _
TotalOrder.strictPartialOrder lb-ord = lb-sord
TotalOrder.partialOrder lb-ord = lb-pord
TotalOrder._<?_ lb-ord = lb-lt
TotalOrder.≰⇒> lb-ord {⌊⊥⌋} {⌊⊥⌋} p = ⊥-elim (p _)
TotalOrder.≰⇒> lb-ord {⌊⊥⌋} {⌊ x ⌋} p = ⊥-elim (p _ )
TotalOrder.≰⇒> lb-ord {⌊ x ⌋} {⌊⊥⌋} p = _
TotalOrder.≰⇒> lb-ord {⌊ x ⌋} {⌊ x₁ ⌋} p = ≰⇒> p
TotalOrder.≮⇒≥ lb-ord {x} {⌊⊥⌋} p = _
TotalOrder.≮⇒≥ lb-ord {⌊⊥⌋} {⌊ y ⌋} p = ⊥-elim (p _)
TotalOrder.≮⇒≥ lb-ord {⌊ x ⌋} {⌊ y ⌋} p = ≮⇒≥ p

ext: agda

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

{-
  Properties and definitions regarding Morphisms of a category:
  - Monomorphism
  - Epimorphism
  - Isomorphism
  - (object) equivalence ('spelled' _≅_ ). Exported as the module ≅
-}
open import Categories.Category

module Categories.Morphism {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Relation.Binary hiding (_⇒_)

open import Categories.Morphism.Reasoning.Core 𝒞

open Category 𝒞

private
  variable
    A B C : Obj

Mono : ∀ (f : A ⇒ B) → Set (o ⊔ ℓ ⊔ e)
Mono {A = A} f = ∀ {C} → (g₁ g₂ : C ⇒ A) → f ∘ g₁ ≈ f ∘ g₂ → g₁ ≈ g₂

Epi : ∀ (f : A ⇒ B) → Set (o ⊔ ℓ ⊔ e)
Epi {B = B} f = ∀ {C} → (g₁ g₂ : B ⇒ C) → g₁ ∘ f ≈ g₂ ∘ f → g₁ ≈ g₂

record Iso (from : A ⇒ B) (to : B ⇒ A) : Set e where
  field
    isoˡ : to ∘ from ≈ id
    isoʳ : from ∘ to ≈ id

infix 4 _≅_
record _≅_ (A B : Obj) : Set (ℓ ⊔ e) where
  field
    from : A ⇒ B
    to   : B ⇒ A
    iso  : Iso from to

  open Iso iso public

-- don't pollute the name space too much
private
  ≅-refl : Reflexive _≅_
  ≅-refl = record
    { from = id
    ; to   = id
    ; iso  = record
      { isoˡ = identityˡ
      ; isoʳ = identityʳ
      }
    }

  ≅-sym : Symmetric _≅_
  ≅-sym A≅B = record
    { from = to
    ; to   = from
    ; iso  = record
      { isoˡ = isoʳ
      ; isoʳ = isoˡ
      }
    }
    where open _≅_ A≅B

  ≅-trans : Transitive _≅_
  ≅-trans A≅B B≅C = record
    { from = from B≅C ∘ from A≅B
    ; to   = to A≅B ∘ to B≅C
    ; iso  = record
      { isoˡ = begin
        (to A≅B ∘ to B≅C) ∘ from B≅C ∘ from A≅B ≈⟨ cancelInner (isoˡ B≅C) ⟩
        to A≅B ∘ from A≅B                       ≈⟨  isoˡ A≅B  ⟩
        id                                      ∎
      ; isoʳ = begin
        (from B≅C ∘ from A≅B) ∘ to A≅B ∘ to B≅C ≈⟨ cancelInner (isoʳ A≅B) ⟩
        from B≅C ∘ to B≅C                       ≈⟨ isoʳ B≅C ⟩
        id                                      ∎
      }
    }
    where open _≅_
          open HomReasoning
          open Equiv

≅-isEquivalence : IsEquivalence _≅_
≅-isEquivalence = record
  { refl  = ≅-refl
  ; sym   = ≅-sym
  ; trans = ≅-trans
  }

-- But make accessing it easy:
module ≅ = IsEquivalence ≅-isEquivalence

≅-setoid : Setoid _ _
≅-setoid = record
  { Carrier       = Obj
  ; _≈_           = _≅_
  ; isEquivalence = ≅-isEquivalence
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
------------------------------------------------------------------------
-- Code related to the paper
-- "Operational Semantics Using the Partiality Monad"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- Several definitions and proofs in this code are closely related to
-- definitions and proofs in the paper "Coinductive big-step
-- operational semantics" by Leroy and Grall. See my paper for more
-- detailed references to related work, and also for more explanations
-- of how the code works.

module Operational-semantics-using-the-partiality-monad where

------------------------------------------------------------------------
-- Section 2

-- Fin.

import Data.Fin

-- Vec, lookup.

import Data.Vec

-- The partiality monad.

import Category.Monad.Partiality

-- A variant of trivial, as well as proofs showing that the definition
-- of weak bisimilarity in the paper coincides with Capretta's
-- definition and a more standard definition based on weak
-- bisimulations.

import AdmissibleButNotPostulable

------------------------------------------------------------------------
-- Section 3

-- Tm, Env, Value.

import Lambda.Syntax

-- Big-step functional semantics, Ω.

import Lambda.Closure.Functional

-- The module above uses some workarounds in order to convince Agda
-- that the code is productive. The following module contains (more or
-- less) the same code without the workarounds, but is checked with
-- the termination checker turned off.

import Lambda.Closure.Functional.No-workarounds

-- An alternative definition of the functional semantics. This
-- definition uses continuation-passing style instead of bind.

import Lambda.Closure.Functional.Alternative

------------------------------------------------------------------------
-- Section 4

-- Type system.

import Lambda.Syntax

-- Type soundness.

import Lambda.Closure.Functional.Type-soundness

-- The use of Lift in the paper is replaced by the use of two
-- different predicate transformers: Any for Maybe and All for the
-- partiality monad.

import Data.Maybe
import Category.Monad.Partiality.All

-- An alternative definition of the functional semantics, using
-- substitutions instead of environments and closures, plus a proof of
-- type soundness.

import Lambda.Substitution.Functional

------------------------------------------------------------------------
-- Section 5

-- The relational semantics.

import Lambda.Closure.Relational

-- Proofs of equivalence.

import Lambda.Closure.Equivalence

------------------------------------------------------------------------
-- Section 6

-- The virtual machine. Two semantics are given, one relational and
-- one functional, and they are proved to be equivalent.

import Lambda.VirtualMachine

------------------------------------------------------------------------
-- Section 7

-- The compiler.

import Lambda.VirtualMachine

-- Compiler correctness for the functional semantics.

import Lambda.Closure.Functional
import Lambda.Closure.Functional.No-workarounds

-- Compiler correctness for the relational semantics.

import Lambda.Closure.Relational

------------------------------------------------------------------------
-- Section 8

-- The non-deterministic language along with a compiler and a compiler
-- correctness proof, as well as a type soundness proof.

import Lambda.Closure.Functional.Non-deterministic
import Lambda.Closure.Functional.Non-deterministic.No-workarounds

------------------------------------------------------------------------
-- Section 9

-- A very brief treatment of different kinds of term equivalences,
-- including contextual equivalence and applicative bisimilarity.

import Lambda.Closure.Equivalences

-- _⇓.

import Category.Monad.Partiality

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

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

open import Vehicle
open import Data.Integer as ℤ using (ℤ)
open import Data.Rational as ℚ using (ℚ)

module simple-untypedDecls-temp-output where

fin3 : ∀ {_x0 : Set} {{_x1 : HasNatLits _x0}} → _x0
fin3 = 3

intMinus3 : ∀ {_x4 : Set} {{_x5 : HasNatLits _x4}} {{_x6 : HasNeg _x4}} → _x4
intMinus3 = - 3

ratMinus3 : ∀ {_x10 : Set} {{_x11 : HasRatLits _x10}} {{_x12 : HasNeg _x10}} → _x10
ratMinus3 = - (ℤ.+ 3 ℚ./ 1)

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
module ListTest where
import AlonzoPrelude
import PreludeList
open AlonzoPrelude
open PreludeList
mynil : {A:Set} -> List A
mynil = []

mycons : {A:Set} -> A -> List A -> List A
mycons x xs = x :: xs

head : (A:Set) -> List A -> A
head A (x :: xs) = x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Prelude.Word where

import Agda.Builtin.Word as Word
open import Prelude.Nat
open import Prelude.Number
open import Prelude.Semiring
open import Prelude.Equality
open import Prelude.Equality.Unsafe
open import Prelude.Ord
open import Prelude.Unit
open import Prelude.Function
open import Prelude.Decidable

open Word public using (Word64) renaming (primWord64ToNat to word64ToNat;
                                          primWord64FromNat to word64FromNat)
open Word

private
  2⁶⁴ : Nat
  2⁶⁴ = 18446744073709551616
  {-# INLINE 2⁶⁴ #-}

inv-word64ToNat : ∀ {a} → word64FromNat (word64ToNat a) ≡ a
inv-word64ToNat = unsafeEqual

emb-word64FromNat : ∀ n → word64ToNat (word64FromNat n) ≡ n mod 2⁶⁴
emb-word64FromNat n = unsafeEqual

inj-word64ToNat : ∀ {a b} → word64ToNat a ≡ word64ToNat b → a ≡ b
inj-word64ToNat {a} {b} eq = eraseEquality (
  a ≡⟨ inv-word64ToNat ⟩ʳ
  word64FromNat (word64ToNat a)
    ≡⟨ word64FromNat $≡ eq ⟩
  word64FromNat (word64ToNat b)
    ≡⟨ inv-word64ToNat ⟩
  b ∎)

instance
  NumWord64 : Number Word64
  Number.Constraint NumWord64 _ = ⊤
  fromNat {{NumWord64}} n = word64FromNat n

  EqWord64 : Eq Word64
  _==_ {{EqWord64}} a b =
    case word64ToNat a == word64ToNat b of λ where
      (yes _) → yes unsafeEqual
      (no  _) → no  unsafeNotEqual

  OrdWord64 : Ord Word64
  OrdWord64 = OrdBy inj-word64ToNat

  OrdLawsWord64 : Ord/Laws Word64
  OrdLawsWord64 = OrdLawsBy inj-word64ToNat

-- Arithmetic --

private
  natOp : (Nat → Nat → Nat) → Word64 → Word64 → Word64
  natOp f a b = fromNat (f (word64ToNat a) (word64ToNat b))
  {-# INLINE natOp #-}

add64 : Word64 → Word64 → Word64
add64 = natOp _+_

sub64 : Word64 → Word64 → Word64
sub64 = natOp λ a b → a + 2⁶⁴ - b

mul64 : Word64 → Word64 → Word64
mul64 = natOp _*_

{-# INLINE add64 #-}
{-# INLINE sub64 #-}
{-# INLINE mul64 #-}

NonZero64 : Word64 → Set
NonZero64 a = NonZero (word64ToNat a)

infixl 7 divWord64 modWord64

syntax divWord64 b a = a div64 b
divWord64 : (b : Word64) {{nz : NonZero64 b}} → Word64 → Word64
divWord64 b a = fromNat (word64ToNat a div word64ToNat b)

syntax modWord64 b a = a mod64 b
modWord64 : (b : Word64) {{nz : NonZero64 b}} → Word64 → Word64
modWord64 b a = fromNat (word64ToNat a mod word64ToNat b)

{-# INLINE divWord64 #-}
{-# INLINE modWord64 #-}

instance
  SemiringWord64 : Semiring Word64
  Semiring.zro SemiringWord64 = 0
  Semiring.one SemiringWord64 = 1
  Semiring._+_ SemiringWord64 = add64
  Semiring._*_ SemiringWord64 = mul64

  NegWord64 : Negative Word64
  Negative.Constraint NegWord64 _ = ⊤
  fromNeg {{NegWord64}} n = sub64 0 (fromNat n)

  SubWord64 : Subtractive Word64
  _-_    {{SubWord64}} = sub64
  negate {{SubWord64}} = sub64 0

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


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

open import Cubical.Data.Maybe.Base public
open import Cubical.Data.Maybe.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- 2011-09-09, submitted by mokus.4...@gmail.com
-- This bug report wins the first price in the false golfing tournament!
-- {-# OPTIONS -v term:20 #-}
module Issue444 where

data ⊥ : Set where

relevant : .⊥ → ⊥
relevant ()

false : ⊥
false = relevant false

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Examples.Sorting.Sequential.Comparable

module Examples.Sorting.Sequential.Core (M : Comparable) where

open import Calf.CostMonoid
open CostMonoid costMonoid
  hiding (zero; _+_; _≤_; ≤-refl; ≤-trans) public

open import Examples.Sorting.Core costMonoid fromℕ M public

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module E where
 t : Set -> Set
 t x = x

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
module Term (Gnd : Set)(U : Set)(El : U -> Set) where

open import Basics
open import Pr
open import Nom
import Kind
open module KindGUEl = Kind Gnd U El
import Loc
open module LocK = Loc Kind
import Cxt
open module CxtK = Cxt Kind

data Jud : Set where
  Term : Kind -> Jud
  Args : Kind -> Gnd -> Jud
  Head : Jud

data _[_]-_ : Loc -> Jud -> Kind -> Set where
  [_] : {C : Kind}{L : Loc}{Z : Gnd} ->
        L [ Args C Z ]- C  ->  L [ Term C ]- Ty Z
  fn : {C : Kind}{L : Loc}(A : U){K : El A -> Kind} ->
       ((x : El A) -> L [ Term C ]- K x) -> L [ Term C ]- Pi A K
  \\ : {C : Kind}{L : Loc}{S T : Kind} ->
       (L * S) [ Term C ]- T  ->  L [ Term C ]- (S |> T)
  _^_ : {C : Kind}{L : Loc}{Z : Gnd}{A : U}{K : El A -> Kind} ->
        (x : El A) -> L [ Args C Z ]- K x -> L [ Args C Z ]- Pi A K
  _&_ : {C : Kind}{L : Loc}{S T : Kind}{Z : Gnd} ->
        L [ Term C ]- S  ->  L [ Args C Z ]- T  ->  L [ Args C Z ]- (S |> T)
  nil : {C : Kind}{L : Loc}{Z : Gnd} -> L [ Args C Z ]- Ty Z
  _$_ : {C : Kind}{L : Loc}{T : Kind}{Z : Gnd} ->
        L [ Head ]- T  ->  L [ Args C Z ]- T  ->  L [ Term C ]- Ty Z
  ` : Nom -> {S : Kind}{L : Loc} -> L [ Head ]- S
  # : {L : Loc}{S : Kind} -> L ! S -> L [ Head ]- S

infixr 90 _^_ _&_

infix 40 _[_]-_

Good : Cxt -> {L : Loc}{j : Jud}{T : Kind} -> L [ j ]- T -> Pr
Good G [ c ]      = Good G c
Good G (fn A f)   = all (El A) \a -> Good G (f a)
Good G (\\ b)     = Good G b
Good G (a ^ ss)   = Good G ss
Good G (s & ss)   = Good G s /\ Good G ss
Good G nil        = tt
Good G (x $ ss)   = Good G x /\ Good G ss
Good G (` x {S})  = GooN G S x
Good G (# v)      = tt

data _[_/_]-_ (G : Cxt)(L : Loc)(j : Jud)(T : Kind) : Set where
  _-!_ : (t : L [ j ]- T) -> [| Good G t |] -> G [ L / j ]- T

gtm : {G : Cxt}{L : Loc}{j : Jud}{T : Kind} -> G [ L / j ]- T -> L [ j ]- T
gtm (t -! _) = t

good : {G : Cxt}{L : Loc}{j : Jud}{T : Kind}
       (t : G [ L / j ]- T) -> [| Good G (gtm t) |]
good (t -! g) = g

_[!_!]-_ : Cxt -> Kind -> Kind -> Set
G [! C !]- T = G [ EL / Term C ]- T

G[_] : {G : Cxt}{C : Kind}{L : Loc}{Z : Gnd} ->
       G [ L / Args C Z ]- C ->
     ----------------------------
       G [ L / Term C ]- Ty Z

G[ c -! cg ] = [ c ] -! cg

Gfn : {G : Cxt}{C : Kind}{L : Loc}(A : U){K : El A -> Kind} ->
      ((x : El A) -> G [ L / Term C ]- K x) ->
    -------------------------------------------
      G [ L / Term C ]- Pi A K

Gfn A f = fn A (gtm o f) -! (good o f)

G\\ : {G : Cxt}{C : Kind}{L : Loc}{S T : Kind} ->
      G [ L * S / Term C ]- T ->
    ------------------------------
      G [ L / Term C ]- (S |> T)

G\\ (b -! bg) = \\ b -! bg

_G^_ : {G : Cxt}{C : Kind}{L : Loc}{Z : Gnd}{A : U}{K : El A -> Kind} ->
       (x : El A) ->
       G [ L / Args C Z ]- K x ->
     ------------------------------
       G [ L / Args C Z ]- Pi A K

a G^ (s -! sg) = (a ^ s) -! sg

_G&_ : {G : Cxt}{C : Kind}{L : Loc}{S T : Kind}{Z : Gnd} ->
        G [ L / Term C ]- S  ->
        G [ L / Args C Z ]- T  ->
      ----------------------------------
        G [ L / Args C Z ]- (S |> T)

(r -! rg) G& (s -! sg) = (r & s) -! (rg , sg)

Gnil : {G : Cxt}{C : Kind}{L : Loc}{Z : Gnd} ->
      -----------------------------
        G [ L / Args C Z ]- Ty Z

Gnil = nil -! _

_G$_ : {G : Cxt}{C : Kind}{L : Loc}{T : Kind}{Z : Gnd} ->
        G [ L / Head ]- T  ->
        G [ L / Args C Z ]- T  ->
      -----------------------------
        G [ L / Term C ]- Ty Z

(h -! hg) G$ (s -! sg) = (h $ s) -! (hg , sg)

G` :   {G : Cxt}{S : Kind}{L : Loc} -> Nom :- GooN G S ->
     ------------------------------------------------------
        G [ L / Head ]- S

G` [ x / xg ] = ` x -! xg

G# : {G : Cxt}{L : Loc}{S : Kind} -> L ! S ->
     --------------------------
       G [ L / Head ]- S

G# v = # v -! _

infixr 90 _G^_ _G&_

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Base.Prelude.Integer where

open import Data.Nat                   using (ℕ; zero; suc)
open import Data.Integer               using (+_; -_) renaming (ℤ to ℤᵖ; _+_ to _+ᵖ_; _-_ to _-ᵖ_; _*_ to _*ᵖ_)
open import Data.Integer.Properties    using (_≤?_; _<?_) renaming (_≟_ to _≟ᵖ_)
open import Relation.Nullary.Decidable using (⌊_⌋)

-- Imports for literals.
open import Agda.Builtin.FromNat
open import Agda.Builtin.FromNeg
open import Agda.Builtin.FromNat       public

open import Base.Free                  using (Free; pure; impure; _>>=_)
open import Base.Partial               using (Partial; error)
open import Base.Prelude.Bool          using (𝔹; not)
open import Base.Prelude.Unit          using (⊤ᵖ)

ℤ : (Shape : Set) → (Shape → Set) → Set
ℤ _ _ = ℤᵖ

_+_ : ∀ {S P} → Free S P (ℤ S P) → Free S P (ℤ S P) → Free S P (ℤ S P)
mx + my = mx >>= λ x → my >>= λ y → pure (x +ᵖ y)

_-_ : ∀ {S P} → Free S P (ℤ S P) → Free S P (ℤ S P) → Free S P (ℤ S P)
mx - my = mx >>= λ x → my >>= λ y → pure (x -ᵖ y)

_*_ : ∀ {S P} → Free S P (ℤ S P) → Free S P (ℤ S P) → Free S P (ℤ S P)
mx * my = mx >>= λ x → my >>= λ y → pure (x *ᵖ y)

_≤_ : ∀ {S P} → Free S P (ℤ S P) → Free S P (ℤ S P) → Free S P (𝔹 S P)
mx ≤ my = mx >>= λ x → my >>= λ y → pure ⌊ x ≤? y ⌋

_<_ : ∀ {S P} → Free S P (ℤ S P) → Free S P (ℤ S P) → Free S P (𝔹 S P)
mx < my = mx >>= λ x → my >>= λ y → pure ⌊ x <? y ⌋

_>_ : ∀ {S P} → Free S P (ℤ S P) → Free S P (ℤ S P) → Free S P (𝔹 S P)
mx > my = my ≤ mx

_≥_ : ∀ {S P} → Free S P (ℤ S P) → Free S P (ℤ S P) → Free S P (𝔹 S P)
mx ≥ my = my < mx

_≟_ : ∀ {S P} → Free S P (ℤ S P) → Free S P (ℤ S P) → Free S P (𝔹 S P)
mx ≟ my = mx >>= λ x → my >>= λ y → pure ⌊ x ≟ᵖ y ⌋

_≠_ : ∀ {S P} → Free S P (ℤ S P) → Free S P (ℤ S P) → Free S P (𝔹 S P)
mx ≠ my = not (mx ≟ my)

instance
  number : Number ℤᵖ
  number = record
    { Constraint = λ _ → ⊤ᵖ
    ; fromNat    = λ n → + n
    }

  negative : Negative ℤᵖ
  negative = record
    { Constraint = λ _ → ⊤ᵖ
    ; fromNeg    = λ n → - (+ n)
    }

_^ᵖ_ : ℤᵖ → ℕ → ℤᵖ
b ^ᵖ 0     = 1
b ^ᵖ suc e = b *ᵖ (b ^ᵖ e)

-- If it encounters a negative exponent the Haskell implementation of @(^)@ raises an exception using @errorWithoutStackTrace@.
_^_ : ∀ {S P} → ⦃ Partial S P ⦄ → Free S P (ℤ S P) → Free S P (ℤ S P) → Free S P (ℤ S P)
mb ^ me = me >>= λ where
  (ℤᵖ.negsuc _) → error "Negative exponent"
  (+ 0)         → pure 1
  (+ (suc e))   → mb >>= λ b → pure (b ^ᵖ suc e)

neg : ∀ {S P} → Free S P (ℤ S P) → Free S P (ℤ S P)
neg x = pure -1 * x

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler


text:
------------------------------------------------------------------------
-- Partiality algebras
------------------------------------------------------------------------

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

module Partiality-algebra where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (id; T) renaming (_∘_ to _⊚_)

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

------------------------------------------------------------------------
-- Partiality algebras

-- Partiality algebras for certain universe levels and types, with a
-- certain underlying type (T).

record Partiality-algebra-with
  {a p} (T : Type p) q (A : Type a) : Type (a ⊔ p ⊔ lsuc q) where

  -- A binary relation on the type.

  infix 4 _⊑_ _⊒_

  field
    _⊑_ : T → T → Type q

  _⊒_ : T → T → Type q
  _⊒_ x y = y ⊑ x

  -- Increasing sequences.

  Increasing-sequence : Type (p ⊔ q)
  Increasing-sequence = ∃ λ (f : ℕ → T) → ∀ n → f n ⊑ f (suc n)

  -- Projection functions for Increasing-sequence.

  infix 30 _[_]

  _[_] : Increasing-sequence → ℕ → T
  _[_] s n = proj₁ s n

  increasing : (s : Increasing-sequence) →
               ∀ n → (s [ n ]) ⊑ (s [ suc n ])
  increasing = proj₂

  -- Upper bounds.

  Is-upper-bound : Increasing-sequence → T → Type q
  Is-upper-bound s x = ∀ n → (s [ n ]) ⊑ x

  field
    -- T "constructors".

    never        : T
    now          : A → T
    ⨆            : Increasing-sequence → T
    antisymmetry : ∀ {x y} → x ⊑ y → y ⊑ x → x ≡ y

    -- We have chosen to explicitly make the type set-truncated.
    -- However, this "constructor" is not used anywhere in the
    -- development (except when partiality algebras are modified, see
    -- for instance equality-characterisation-Partiality-algebra-with₁
    -- or Partiality-algebra.Pi.Π-with).
    T-is-set-unused : Is-set T

    -- _⊑_ "constructors".

    ⊑-refl            : ∀ x → x ⊑ x
    ⊑-trans           : ∀ {x y z} → x ⊑ y → y ⊑ z → x ⊑ z
    never⊑            : ∀ x → never ⊑ x
    upper-bound       : ∀ s → Is-upper-bound s (⨆ s)
    least-upper-bound : ∀ s ub → Is-upper-bound s ub → ⨆ s ⊑ ub
    ⊑-propositional   : ∀ {x y} → Is-proposition (x ⊑ y)

  ----------------------------------------------------------------------
  -- Some simple consequences

  private

    -- A lemma.

    T-is-set-and-equality-characterisation : Is-set T × _
    T-is-set-and-equality-characterisation =
      Eq.propositional-identity≃≡
        (λ x y → x ⊑ y × y ⊑ x)
        (λ _ _ → ×-closure 1 ⊑-propositional ⊑-propositional)
        (λ x → ⊑-refl x , ⊑-refl x)
        (λ x y → uncurry {B = λ _ → y ⊑ x} antisymmetry)

  -- T is a set. (This lemma is analogous to Theorem 11.3.9 in
  -- "Homotopy Type Theory: Univalent Foundations of Mathematics"
  -- (first edition).)

  T-is-set : Is-set T
  T-is-set = proj₁ T-is-set-and-equality-characterisation

  -- Equality characterisation lemma for T.

  equality-characterisation-T :
    ∀ {x y} → (x ⊑ y × y ⊑ x) ≃ (x ≡ y)
  equality-characterisation-T =
    proj₂ T-is-set-and-equality-characterisation ext

  -- Equality characterisation lemma for increasing sequences.

  equality-characterisation-increasing :
    ∀ {s₁ s₂} → (∀ n → s₁ [ n ] ≡ s₂ [ n ]) ↔ s₁ ≡ s₂
  equality-characterisation-increasing {s₁} {s₂} =
    (∀ n → s₁ [ n ] ≡ s₂ [ n ])  ↔⟨ Eq.extensionality-isomorphism bad-ext ⟩
    proj₁ s₁ ≡ proj₁ s₂          ↝⟨ ignore-propositional-component
                                      (Π-closure ext 1 λ _ →
                                       ⊑-propositional) ⟩□
    s₁ ≡ s₂                      □

-- Partiality algebras for certain universe levels and types.

record Partiality-algebra {a} p q (A : Type a) :
                          Type (a ⊔ lsuc (p ⊔ q)) where
  constructor ⟨_⟩
  field
    -- A type.

    {T} : Type p

    -- A partiality-algebra with that type as the underlying type.

    partiality-algebra-with : Partiality-algebra-with T q A

  open Partiality-algebra-with partiality-algebra-with public

------------------------------------------------------------------------
-- Partiality algebra morphisms

-- Morphisms from one partiality algebra to another.

record Morphism {a p₁ p₂ q₁ q₂} {A : Type a}
                (P₁ : Partiality-algebra p₁ q₁ A)
                (P₂ : Partiality-algebra p₂ q₂ A) :
                Type (a ⊔ p₁ ⊔ p₂ ⊔ q₁ ⊔ q₂) where

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

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

  sequence-function : P₁.Increasing-sequence → P₂.Increasing-sequence
  sequence-function = Σ-map (function ⊚_) (monotone ⊚_)

  field
    strict       : function P₁.never ≡ P₂.never
    now-to-now   : ∀ x → function (P₁.now x) ≡ P₂.now x
    ω-continuous : ∀ s → function (P₁.⨆ s) ≡ P₂.⨆ (sequence-function s)

-- An identity morphism.

id :
  ∀ {a p q} {A : Type a} {P : Partiality-algebra p q A} →
  Morphism P P
id = record
  { function     = Prelude.id
  ; monotone     = Prelude.id
  ; strict       = refl
  ; now-to-now   = λ _ → refl
  ; ω-continuous = λ _ → refl
  }

-- Composition of morphisms.

_∘_ : ∀ {a p₁ p₂ p₃ q₁ q₂ q₃} {A : Type a}
        {P₁ : Partiality-algebra p₁ q₁ A}
        {P₂ : Partiality-algebra p₂ q₂ A}
        {P₃ : Partiality-algebra p₃ q₃ A} →
      Morphism P₂ P₃ → Morphism P₁ P₂ → Morphism P₁ P₃
_∘_ {P₁ = P₁} {P₂} {P₃} m₁ m₂ = record
  { function     = function m₁ ⊚ function m₂
  ; monotone     = monotone m₁ ⊚ monotone m₂
  ; strict       = function m₁ (function m₂ (never P₁))  ≡⟨ cong (function m₁) (strict m₂) ⟩
                   function m₁ (never P₂)                ≡⟨ strict m₁ ⟩∎
                   never P₃                              ∎
  ; now-to-now   = λ x →
                     function m₁ (function m₂ (now P₁ x))  ≡⟨ cong (function m₁) (now-to-now m₂ x) ⟩
                     function m₁ (now P₂ x)                ≡⟨ now-to-now m₁ x ⟩∎
                     now P₃ x                              ∎
  ; ω-continuous = λ s →
      function m₁ (function m₂ (⨆ P₁ s))                    ≡⟨ cong (function m₁) (ω-continuous m₂ s) ⟩
      function m₁ (⨆ P₂ (sequence-function m₂ s))           ≡⟨ ω-continuous m₁ (sequence-function m₂ s) ⟩∎
      ⨆ P₃ (sequence-function m₁ (sequence-function m₂ s))  ∎
  }
  where
  open Morphism
  open Partiality-algebra

-- Is-morphism-with P Q f holds if f is a morphism from P to Q.

Is-morphism-with :
  ∀ {a p₁ p₂ q₁ q₂} {T₁ : Type p₁} {T₂ : Type p₂} {A : Type a}
  (P₁ : Partiality-algebra-with T₁ q₁ A)
  (P₂ : Partiality-algebra-with T₂ q₂ A) →
  (T₁ → T₂) → Type _
Is-morphism-with P₁ P₂ f =
  ∃ λ (m : ∀ {x y} → x P₁.⊑ y → f x P₂.⊑ f y) →
  f P₁.never ≡ P₂.never
    ×
  (∀ x → f (P₁.now x) ≡ P₂.now x)
    ×
  (∀ s → f (P₁.⨆ s) ≡ P₂.⨆ (Σ-map (f ⊚_) (m ⊚_) s))
  where
  module P₁ = Partiality-algebra-with P₁
  module P₂ = Partiality-algebra-with P₂

-- Is-morphism P Q f holds if f is a morphism from P to Q.

Is-morphism :
  let open Partiality-algebra in
  ∀ {a p₁ p₂ q₁ q₂} {A : Type a}
  (P₁ : Partiality-algebra p₁ q₁ A) (P₂ : Partiality-algebra p₂ q₂ A) →
  (T P₁ → T P₂) → Type _
Is-morphism P₁ P₂ =
  Is-morphism-with P₁.partiality-algebra-with
                   P₂.partiality-algebra-with
  where
  module P₁ = Partiality-algebra P₁
  module P₂ = Partiality-algebra P₂

-- An alternative definition of morphisms.

Morphism-as-Σ :
  ∀ {a p₁ p₂ q₁ q₂} {A : Type a} →
  Partiality-algebra p₁ q₁ A → Partiality-algebra p₂ q₂ A → Type _
Morphism-as-Σ P₁ P₂ =
  ∃ λ (f : P₁.T → P₂.T) → Is-morphism P₁ P₂ f
  where
  module P₁ = Partiality-algebra P₁
  module P₂ = Partiality-algebra P₂

-- The two definitions are isomorphic.

Morphism↔Morphism-as-Σ :
  ∀ {a p₁ p₂ q₁ q₂} {A : Type a}
    {P₁ : Partiality-algebra p₁ q₁ A}
    {P₂ : Partiality-algebra p₂ q₂ A} →
  Morphism P₁ P₂ ↔ Morphism-as-Σ P₁ P₂
Morphism↔Morphism-as-Σ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ m → function m
                   , monotone m
                   , strict m
                   , now-to-now m
                   , ω-continuous m
      ; from = λ { (f , m , s , n , ω) → record
                   { function     = f
                   ; monotone     = m
                   ; strict       = s
                   ; now-to-now   = n
                   ; ω-continuous = ω
                   }
                 }
      }
    ; right-inverse-of = λ _ → refl
    }
  ; left-inverse-of = λ _ → refl
  }
  where
  open Morphism

abstract

  -- Is-morphism-with is pointwise propositional.

  Is-morphism-with-propositional :
    let open Partiality-algebra in
    ∀ {a p₁ p₂ q₁ q₂} {T₁ : Type p₁} {T₂ : Type p₂} {A : Type a}
      (P₁ : Partiality-algebra-with T₁ q₁ A)
      (P₂ : Partiality-algebra-with T₂ q₂ A)
      {f : T₁ → T₂} →
    Is-proposition (Is-morphism-with P₁ P₂ f)
  Is-morphism-with-propositional _ P₂ =
    Σ-closure 1 (implicit-Π-closure ext 1 λ _ →
                 implicit-Π-closure ext 1 λ _ →
                 Π-closure ext 1 λ _ →
                 P₂.⊑-propositional) λ _ →
    ×-closure 1 P₂.T-is-set $
    ×-closure 1 (Π-closure ext 1 λ _ →
                 P₂.T-is-set) $
    Π-closure ext 1 λ _ →
    P₂.T-is-set
    where
    module P₂ = Partiality-algebra-with P₂

  -- Is-morphism is pointwise propositional.

  Is-morphism-propositional :
    let open Partiality-algebra in
    ∀ {a p₁ p₂ q₁ q₂} {A : Type a}
      (P₁ : Partiality-algebra p₁ q₁ A)
      (P₂ : Partiality-algebra p₂ q₂ A)
      {f : T P₁ → T P₂} →
    Is-proposition (Is-morphism P₁ P₂ f)
  Is-morphism-propositional P₁ P₂ =
    Is-morphism-with-propositional
      P₁.partiality-algebra-with
      P₂.partiality-algebra-with
    where
    module P₁ = Partiality-algebra P₁
    module P₂ = Partiality-algebra P₂

  -- An equality characterisation lemma for morphisms.

  equality-characterisation-Morphism :
    ∀ {a p₁ p₂ q₁ q₂} {A : Type a}
      {P₁ : Partiality-algebra p₁ q₁ A}
      {P₂ : Partiality-algebra p₂ q₂ A} →
      {m₁ m₂ : Morphism P₁ P₂} →

    Morphism.function m₁ ≡ Morphism.function m₂
      ↔
    m₁ ≡ m₂
  equality-characterisation-Morphism {P₁ = P₁} {P₂} {m₁} {m₂} =
    function m₁ ≡ function m₂                                            ↝⟨ ignore-propositional-component (Is-morphism-propositional P₁ P₂) ⟩
    _↔_.to Morphism↔Morphism-as-Σ m₁ ≡ _↔_.to Morphism↔Morphism-as-Σ m₂  ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ Morphism↔Morphism-as-Σ) ⟩□
    m₁ ≡ m₂                                                              □
    where
    open Morphism

  -- The type of morphisms is a set.

  Morphism-set :
    ∀  {a p₁ p₂ q₁ q₂} {A : Type a}
       {P₁ : Partiality-algebra p₁ q₁ A}
       {P₂ : Partiality-algebra p₂ q₂ A} →
    Is-set (Morphism P₁ P₂)
  Morphism-set {P₂ = P₂} =
    H-level.respects-surjection
      (_↔_.surjection equality-characterisation-Morphism)
      1
      (Π-closure ext 2 λ _ → T-is-set P₂)
    where
    open Partiality-algebra

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
------------------------------------------------------------------------------
-- Twice funcion
------------------------------------------------------------------------------

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

module LTC-PCF.Twice where

open import LTC-PCF.Base

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

twice : (D → D) → D → D
twice f x = f (f x)

twice-succ : ∀ n → twice succ₁ n ≡ succ₁ (succ₁ n)
twice-succ n = refl

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-  This example test that the order in which unification
    constraints are generated doesn't matter. The pattern
    matching in foo generates the unification problem
      [x, zero] = [n + m, n]
    with n and m flexible. The first equation can only be
    solved after the second one has been solved. For completeness
    we check that the other way around also works.
-}
module PostponedUnification where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

data T : Nat -> Nat -> Set where
  t  : (x : Nat) -> T x zero

foo : (n m : Nat) -> T (n + m) n -> Set
foo ._ ._ (t x) = Nat

data U : Nat -> Nat -> Set where
  u  : (x : Nat) -> U zero x

bar : (n m : Nat) -> U n (n + m) -> Set
bar ._ ._ (u x) = Nat


text:
------------------------------------------------------------------------
-- Bijections
------------------------------------------------------------------------

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

open import Equality

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

open Derived-definitions-and-properties eq
open import Equality.Decision-procedures eq
open import H-level eq
open import Injection eq using (Injective; _↣_)
open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)
open import Surjection eq as Surjection using (_↠_; module _↠_)

------------------------------------------------------------------------
-- Bijections

infix 0 _↔_

record _↔_ {f t} (From : Type f) (To : Type t) : Type (f ⊔ t) where
  field
    surjection : From ↠ To

  open _↠_ surjection

  field
    left-inverse-of : ∀ x → from (to x) ≡ x

  injective : Injective to
  injective {x = x} {y = y} to-x≡to-y =
    x            ≡⟨ sym (left-inverse-of x) ⟩
    from (to x)  ≡⟨ cong from to-x≡to-y ⟩
    from (to y)  ≡⟨ left-inverse-of y ⟩∎
    y            ∎

  injection : From ↣ To
  injection = record
    { to        = to
    ; injective = injective
    }

  -- A lemma.

  to-from : ∀ {x y} → to x ≡ y → from y ≡ x
  to-from {x} {y} to-x≡y =
    from y       ≡⟨ cong from $ sym to-x≡y ⟩
    from (to x)  ≡⟨ left-inverse-of x ⟩∎
    x            ∎

  -- Every right inverse of to is pointwise equal to from.

  right-inverse-unique :
    (f : To → From) →
    (∀ x → to (f x) ≡ x) →
    (∀ x → f x ≡ from x)
  right-inverse-unique _ right x = sym $ to-from (right x)

  -- Every left inverse of from is pointwise equal to to.

  left-inverse-of-from-unique :
    (f : From → To) →
    (∀ x → f (from x) ≡ x) →
    (∀ x → f x ≡ to x)
  left-inverse-of-from-unique f left x =
    f x              ≡⟨ cong f $ sym $ left-inverse-of _ ⟩
    f (from (to x))  ≡⟨ left _ ⟩∎
    to x             ∎

  open _↠_ surjection public

-- The type of quasi-inverses of a function (as defined in the HoTT
-- book).

Has-quasi-inverse :
  ∀ {a b} {A : Type a} {B : Type b} →
  (A → B) → Type (a ⊔ b)
Has-quasi-inverse {A = A} {B = B} to =
  ∃ λ (from : B → A) →
    (∀ x → to (from x) ≡ x) ×
    (∀ x → from (to x) ≡ x)

-- An alternative characterisation of bijections.

↔-as-Σ :
  ∀ {a b} {A : Type a} {B : Type b} →
  (A ↔ B) ↔ ∃ λ (f : A → B) → Has-quasi-inverse f
↔-as-Σ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ A↔B → _↔_.to A↔B
                     , _↔_.from A↔B
                     , _↔_.right-inverse-of A↔B
                     , _↔_.left-inverse-of A↔B
      ; from = λ (t , f , r , l) → record
          { surjection = record
            { logical-equivalence = record
              { to   = t
              ; from = f
              }
            ; right-inverse-of = r
            }
          ; left-inverse-of = l
          }
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

------------------------------------------------------------------------
-- Equivalence

-- _↔_ is an equivalence relation.

id : ∀ {a} {A : Type a} → A ↔ A
id = record
  { surjection      = Surjection.id
  ; left-inverse-of = refl
  }

inverse : ∀ {a b} {A : Type a} {B : Type b} → A ↔ B → B ↔ A
inverse A↔B = record
  { surjection = record
    { logical-equivalence = Logical-equivalence.inverse
                              logical-equivalence
    ; right-inverse-of    = left-inverse-of
    }
  ; left-inverse-of = right-inverse-of
  } where open _↔_ A↔B

infixr 9 _∘_

_∘_ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} →
      B ↔ C → A ↔ B → A ↔ C
f ∘ g = record
  { surjection      = Surjection._∘_ (surjection f) (surjection g)
  ; left-inverse-of = from∘to
  }
  where
  open _↔_

  from∘to : ∀ x → from g (from f (to f (to g x))) ≡ x
  from∘to = λ x →
    from g (from f (to f (to g x)))  ≡⟨ cong (from g) (left-inverse-of f (to g x)) ⟩
    from g (to g x)                  ≡⟨ left-inverse-of g x ⟩∎
    x                                ∎

-- "Equational" reasoning combinators.

infix  -1 finally-↔
infixr -2 step-↔

-- For an explanation of why step-↔ is defined in this way, see
-- Equality.step-≡.

step-↔ : ∀ {a b c} (A : Type a) {B : Type b} {C : Type c} →
         B ↔ C → A ↔ B → A ↔ C
step-↔ _ = _∘_

syntax step-↔ A B↔C A↔B = A ↔⟨ A↔B ⟩ B↔C

finally-↔ : ∀ {a b} (A : Type a) (B : Type b) → A ↔ B → A ↔ B
finally-↔ _ _ A↔B = A↔B

syntax finally-↔ A B A↔B = A ↔⟨ A↔B ⟩□ B □

------------------------------------------------------------------------
-- One can replace either of the functions with an extensionally equal
-- function

with-other-function :
  ∀ {a b} {A : Type a} {B : Type b}
  (A↔B : A ↔ B) (f : A → B) →
  (∀ x → _↔_.to A↔B x ≡ f x) →
  A ↔ B
with-other-function A↔B f ≡f = record
  { surjection = record
    { logical-equivalence = record
      { to   = f
      ; from = _↔_.from A↔B
      }
    ; right-inverse-of = λ x →
        f (_↔_.from A↔B x)           ≡⟨ sym $ ≡f _ ⟩
        _↔_.to A↔B (_↔_.from A↔B x)  ≡⟨ _↔_.right-inverse-of A↔B _ ⟩∎
        x                            ∎
    }
  ; left-inverse-of = λ x →
      _↔_.from A↔B (f x)           ≡⟨ cong (_↔_.from A↔B) $ sym $ ≡f _ ⟩
      _↔_.from A↔B (_↔_.to A↔B x)  ≡⟨ _↔_.left-inverse-of A↔B _ ⟩∎
      x                            ∎
  }

with-other-inverse :
  ∀ {a b} {A : Type a} {B : Type b}
  (A↔B : A ↔ B) (f : B → A) →
  (∀ x → _↔_.from A↔B x ≡ f x) →
  A ↔ B
with-other-inverse A↔B f ≡f =
  inverse $ with-other-function (inverse A↔B) f ≡f

private

  -- The two functions above compute in the right way.

  to∘with-other-function :
    ∀ {a b} {A : Type a} {B : Type b}
    (A↔B : A ↔ B) (f : A → B)
    (to≡f : ∀ x → _↔_.to A↔B x ≡ f x) →
    _↔_.to (with-other-function A↔B f to≡f) ≡ f
  to∘with-other-function _ _ _ = refl _

  from∘with-other-function :
    ∀ {a b} {A : Type a} {B : Type b}
    (A↔B : A ↔ B) (f : A → B)
    (to≡f : ∀ x → _↔_.to A↔B x ≡ f x) →
    _↔_.from (with-other-function A↔B f to≡f) ≡ _↔_.from A↔B
  from∘with-other-function _ _ _ = refl _

  to∘with-other-inverse :
    ∀ {a b} {A : Type a} {B : Type b}
    (A↔B : A ↔ B) (g : B → A)
    (from≡g : ∀ x → _↔_.from A↔B x ≡ g x) →
    _↔_.to (with-other-inverse A↔B g from≡g) ≡ _↔_.to A↔B
  to∘with-other-inverse _ _ _ = refl _

  from∘with-other-inverse :
    ∀ {a b} {A : Type a} {B : Type b}
    (A↔B : A ↔ B) (g : B → A)
    (from≡g : ∀ x → _↔_.from A↔B x ≡ g x) →
    _↔_.from (with-other-inverse A↔B g from≡g) ≡ g
  from∘with-other-inverse _ _ _ = refl _

------------------------------------------------------------------------
-- More lemmas

-- Uninhabited types are isomorphic to the empty type.

⊥↔uninhabited : ∀ {a ℓ} {A : Type a} → ¬ A → ⊥ {ℓ = ℓ} ↔ A
⊥↔uninhabited ¬A = record
  { surjection = record
    { logical-equivalence = record
      { to   = ⊥-elim
      ; from = ⊥-elim ⊚ ¬A
      }
    ; right-inverse-of = ⊥-elim ⊚ ¬A
    }
  ; left-inverse-of = λ ()
  }

-- A lifted set is isomorphic to the underlying one.

↑↔ : ∀ {a b} {A : Type a} → ↑ b A ↔ A
↑↔ {b = b} {A} = record
  { surjection = record
    { logical-equivalence = record
      { to   = lower
      ; from = lift
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- Equality between pairs can be expressed as a pair of equalities.

Σ-≡,≡↔≡ : ∀ {a b} {A : Type a} {B : A → Type b} {p₁ p₂ : Σ A B} →
          (∃ λ (p : proj₁ p₁ ≡ proj₁ p₂) →
             subst B p (proj₂ p₁) ≡ proj₂ p₂) ↔
          (p₁ ≡ p₂)
Σ-≡,≡↔≡ {A = A} {B} {p₁} {p₂} = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  from-P = λ {p₁ p₂ : Σ A B} (_ : p₁ ≡ p₂) →
             ∃ λ (p : proj₁ p₁ ≡ proj₁ p₂) →
               subst B p (proj₂ p₁) ≡ proj₂ p₂

  from : {p₁ p₂ : Σ A B} →
         p₁ ≡ p₂ →
         ∃ λ (p : proj₁ p₁ ≡ proj₁ p₂) →
           subst B p (proj₂ p₁) ≡ proj₂ p₂
  from = Σ-≡,≡←≡

  to : {p₁ p₂ : Σ A B} →
       (∃ λ (p : proj₁ p₁ ≡ proj₁ p₂) →
          subst B p (proj₂ p₁) ≡ proj₂ p₂) →
       p₁ ≡ p₂
  to = uncurry Σ-≡,≡→≡

  abstract

    to∘from : ∀ eq → to (from {p₁ = p₁} {p₂ = p₂} eq) ≡ eq
    to∘from = elim (λ p≡q → to (from p≡q) ≡ p≡q) λ x →
      let lem = subst-refl B (proj₂ x) in
      to (from (refl x))                          ≡⟨ cong to (elim-refl from-P _) ⟩
      to (refl (proj₁ x) , lem)                   ≡⟨ Σ-≡,≡→≡-reflˡ _ ⟩
      cong (_,_ (proj₁ x)) (trans (sym lem) lem)  ≡⟨ cong (cong (_,_ (proj₁ x))) $ trans-symˡ lem ⟩
      cong (_,_ (proj₁ x)) (refl (proj₂ x))       ≡⟨ cong-refl (_,_ (proj₁ x)) ⟩∎
      refl x                                      ∎

    from∘to : ∀ p → from (to {p₁ = p₁} {p₂ = p₂} p) ≡ p
    from∘to p = elim
      (λ {x₁ x₂} x₁≡x₂ →
         ∀ {y₁ y₂} (y₁′≡y₂ : subst B x₁≡x₂ y₁ ≡ y₂) →
         from (to (x₁≡x₂ , y₁′≡y₂)) ≡ (x₁≡x₂ , y₁′≡y₂))
      (λ x {y₁} y₁′≡y₂ → elim
         (λ {y₁ y₂} (y₁≡y₂ : y₁ ≡ y₂) →
            (y₁′≡y₂ : subst B (refl x) y₁ ≡ y₂) →
            y₁≡y₂ ≡ trans (sym $ subst-refl B y₁) y₁′≡y₂ →
            from (to (refl x , y₁′≡y₂)) ≡ (refl x , y₁′≡y₂))
         (λ y y′≡y eq →
          let lem = subst-refl B y in
          from (to (refl x , y′≡y))                   ≡⟨ cong from $ Σ-≡,≡→≡-reflˡ _ ⟩
          from (cong (_,_ x) (trans (sym lem) y′≡y))  ≡⟨ cong (from ⊚ cong (_,_ x)) $ sym eq ⟩
          from (cong (_,_ x) (refl y))                ≡⟨ cong from $ cong-refl (_,_ x) ⟩
          from (refl (x , y))                         ≡⟨ elim-refl from-P _ ⟩
          (refl x , lem)                              ≡⟨ cong (_,_ (refl x)) (
             lem                                           ≡⟨ sym $ trans-reflʳ _ ⟩
             trans lem (refl _)                            ≡⟨ cong (trans lem) eq ⟩
             trans lem (trans (sym lem) y′≡y)              ≡⟨ sym $ trans-assoc _ _ _ ⟩
             trans (trans lem (sym lem)) y′≡y              ≡⟨ cong (λ p → trans p y′≡y) $ trans-symʳ lem ⟩
             trans (refl _) y′≡y                           ≡⟨ trans-reflˡ _ ⟩∎
             y′≡y                                          ∎) ⟩∎
          (refl x , y′≡y)                             ∎)
         (trans (sym $ subst-refl B y₁) y₁′≡y₂)
         y₁′≡y₂
         (refl _))
      (proj₁ p) (proj₂ p)

-- Equalities are closed, in a strong sense, under applications of
-- certain injections (at least inj₁ and inj₂).

≡↔inj₁≡inj₁ : ∀ {a b} {A : Type a} {B : Type b} {x y : A} →
              (x ≡ y) ↔ _≡_ {A = A ⊎ B} (inj₁ x) (inj₁ y)
≡↔inj₁≡inj₁ {A = A} {B} {x} {y} = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  to : x ≡ y → _≡_ {A = A ⊎ B} (inj₁ x) (inj₁ y)
  to = cong inj₁

  from = ⊎.cancel-inj₁

  abstract

    to∘from : ∀ ix≡iy → to (from ix≡iy) ≡ ix≡iy
    to∘from ix≡iy =
      cong inj₁ (⊎.cancel-inj₁ ix≡iy)              ≡⟨ cong-∘ inj₁ [ P.id , const x ] ix≡iy ⟩
      cong f ix≡iy                                 ≡⟨ cong-roughly-id f p ix≡iy _ _ f≡id ⟩
      trans (refl _) (trans ix≡iy $ sym (refl _))  ≡⟨ trans-reflˡ _ ⟩
      trans ix≡iy (sym $ refl _)                   ≡⟨ cong (trans ix≡iy) sym-refl ⟩
      trans ix≡iy (refl _)                         ≡⟨ trans-reflʳ _ ⟩∎
      ix≡iy                                        ∎
      where
      f : A ⊎ B → A ⊎ B
      f = inj₁ ⊚ [ P.id , const x ]

      p : A ⊎ B → Bool
      p = if_then true else false

      f≡id : ∀ z → T (p z) → f z ≡ z
      f≡id (inj₁ x) = const (refl (inj₁ x))
      f≡id (inj₂ y) = ⊥-elim

    from∘to : ∀ x≡y → from (to x≡y) ≡ x≡y
    from∘to x≡y =
      cong [ P.id , const x ] (cong inj₁ x≡y)  ≡⟨ cong-∘ [ P.id , const x ] inj₁ _ ⟩
      cong P.id x≡y                            ≡⟨ sym $ cong-id _ ⟩∎
      x≡y                                      ∎

≡↔inj₂≡inj₂ : ∀ {a b} {A : Type a} {B : Type b} {x y : B} →
              (x ≡ y) ↔ _≡_ {A = A ⊎ B} (inj₂ x) (inj₂ y)
≡↔inj₂≡inj₂ {A = A} {B} {x} {y} = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  to : x ≡ y → _≡_ {A = A ⊎ B} (inj₂ x) (inj₂ y)
  to = cong inj₂

  from = ⊎.cancel-inj₂

  abstract

    to∘from : ∀ ix≡iy → to (from ix≡iy) ≡ ix≡iy
    to∘from ix≡iy =
      cong inj₂ (⊎.cancel-inj₂ ix≡iy)              ≡⟨ cong-∘ inj₂ [ const x , P.id ] ix≡iy ⟩
      cong f ix≡iy                                 ≡⟨ cong-roughly-id f p ix≡iy _ _ f≡id ⟩
      trans (refl _) (trans ix≡iy $ sym (refl _))  ≡⟨ trans-reflˡ _ ⟩
      trans ix≡iy (sym $ refl _)                   ≡⟨ cong (trans ix≡iy) sym-refl ⟩
      trans ix≡iy (refl _)                         ≡⟨ trans-reflʳ _ ⟩∎
      ix≡iy                                        ∎
      where
      f : A ⊎ B → A ⊎ B
      f = inj₂ ⊚ [ const x , P.id ]

      p : A ⊎ B → Bool
      p = if_then false else true

      f≡id : ∀ z → T (p z) → f z ≡ z
      f≡id (inj₁ x) = ⊥-elim
      f≡id (inj₂ y) = const (refl (inj₂ y))

    from∘to : ∀ x≡y → from (to x≡y) ≡ x≡y
    from∘to x≡y =
      cong [ const x , P.id ] (cong inj₂ x≡y)  ≡⟨ cong-∘ [ const x , P.id ] inj₂ _ ⟩
      cong P.id x≡y                            ≡⟨ sym $ cong-id _ ⟩∎
      x≡y                                      ∎

-- An alternative characterisation of equality for binary sums.

Equality-⊎ : ∀ {a b} {A : Type a} {B : Type b} →
             A ⊎ B → A ⊎ B → Type (a ⊔ b)
Equality-⊎ {b = b} (inj₁ x) (inj₁ y) = ↑ b (x ≡ y)
Equality-⊎         (inj₁ x) (inj₂ y) = ⊥
Equality-⊎         (inj₂ x) (inj₁ y) = ⊥
Equality-⊎ {a = a} (inj₂ x) (inj₂ y) = ↑ a (x ≡ y)

≡↔⊎ : ∀ {a b} {A : Type a} {B : Type b} {x y : A ⊎ B} →
      x ≡ y ↔ Equality-⊎ x y
≡↔⊎ {x = inj₁ x} {inj₁ y} = inj₁ x ≡ inj₁ y  ↔⟨ inverse ≡↔inj₁≡inj₁ ⟩
                            x ≡ y            ↔⟨ inverse ↑↔ ⟩□
                            ↑ _ (x ≡ y)      □
≡↔⊎ {x = inj₁ x} {inj₂ y} = inj₁ x ≡ inj₂ y  ↔⟨ inverse (⊥↔uninhabited ⊎.inj₁≢inj₂) ⟩□
                            ⊥                □
≡↔⊎ {x = inj₂ x} {inj₁ y} = inj₂ x ≡ inj₁ y  ↔⟨ inverse (⊥↔uninhabited (⊎.inj₁≢inj₂ ⊚ sym)) ⟩□
                            ⊥                □
≡↔⊎ {x = inj₂ x} {inj₂ y} = inj₂ x ≡ inj₂ y  ↔⟨ inverse ≡↔inj₂≡inj₂ ⟩
                            x ≡ y            ↔⟨ inverse ↑↔ ⟩□
                            ↑ _ (x ≡ y)      □

-- Decidable equality respects bijections.

decidable-equality-respects :
  ∀ {a b} {A : Type a} {B : Type b} →
  A ↔ B → Decidable-equality A → Decidable-equality B
decidable-equality-respects A↔B _≟A_ x y =
  ⊎-map (_↔_.injective (inverse A↔B))
                       (λ from-x≢from-y → from-x≢from-y ⊚ cong from)
        (from x ≟A from y)
  where open _↔_ A↔B

-- All contractible types are isomorphic.

contractible-isomorphic :
  ∀ {a b} {A : Type a} {B : Type b} →
  Contractible A → Contractible B → A ↔ B
contractible-isomorphic {A} {B} cA cB = record
  { surjection = record
    { logical-equivalence = record
      { to   = const (proj₁ cB)
      ; from = const (proj₁ cA)
      }
    ; right-inverse-of = proj₂ cB
    }
  ; left-inverse-of = proj₂ cA
  }

-- Implicit and explicit Π's are isomorphic.

implicit-Π↔Π : ∀ {a b} {A : Type a} {B : A → Type b} →
               ({x : A} → B x) ↔ ((x : A) → B x)
implicit-Π↔Π = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f x → f {x}
      ; from = λ f {x} → f x
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- Implicit and explicit Π's with erased domains are isomorphic.

implicit-Πᴱ↔Πᴱ :
  ∀ {a b} {A : Type a} {B : A → Type b} →
  ({@0 x : A} → B x) ↔ ((@0 x : A) → B x)
implicit-Πᴱ↔Πᴱ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f x → f {x}
      ; from = λ f {x} → f x
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- A variant of implicit-Πᴱ↔Πᴱ.

implicit-Πᴱ↔Πᴱ′ :
  ∀ {a b} {@0 A : Type a} {B : @0 A → Type b} →
  ({@0 x : A} → B x) ↔ ((@0 x : A) → B x)
implicit-Πᴱ↔Πᴱ′ {A = A} {B = B} = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f x → f {x}
      ; from = λ f {x} → f x
      }
    ; right-inverse-of = refl {A = (@0 x : A) → B x}
    }
  ; left-inverse-of = refl {A = {@0 x : A} → B x}
  }

-- Σ is associative.

Σ-assoc : ∀ {a b c}
            {A : Type a} {B : A → Type b} {C : (x : A) → B x → Type c} →
          (Σ A λ x → Σ (B x) (C x)) ↔ Σ (Σ A B) (uncurry C)
Σ-assoc = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (x , (y , z)) → (x , y) , z }
      ; from = λ { ((x , y) , z) → x , (y , z) }
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- Π and Σ commute (in a certain sense).

ΠΣ-comm :
  ∀ {a b c} {A : Type a} {B : A → Type b} {C : (x : A) → B x → Type c} →
  (∀ x → ∃ λ (y : B x) → C x y)
    ↔
  (∃ λ (f : ∀ x → B x) → ∀ x → C x (f x))
ΠΣ-comm = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f → proj₁ ⊚ f , proj₂ ⊚ f
      ; from = λ { (f , g) x → f x , g x }
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- Equality is commutative.

≡-comm :
  ∀ {a} {A : Type a} {x y : A} →
  x ≡ y ↔ y ≡ x
≡-comm = record
  { surjection = record
    { logical-equivalence = record { to = sym }
    ; right-inverse-of    = sym-sym
    }
  ; left-inverse-of = sym-sym
  }

-- Families of functions that satisfy a kind of involution property
-- can be turned into bijections.

bijection-from-involutive-family :
  ∀ {a b} {A : Type a} {B : A → Type b} →
  (f : ∀ a₁ a₂ → B a₁ → B a₂) →
  (∀ a₁ a₂ (x : B a₁) → f _ _ (f _ a₂ x) ≡ x) →
  ∀ a₁ a₂ → B a₁ ↔ B a₂
bijection-from-involutive-family f f-involutive _ _ = record
  { surjection = record
    { logical-equivalence = record
      { to   = f _ _
      ; from = f _ _
      }
    ; right-inverse-of = f-involutive _ _
    }
  ; left-inverse-of = f-involutive _ _
  }

abstract

  -- An equality rearrangement lemma.

  trans-to-to≡to-trans :
    ∀ {a b} {A : Type a} {B : Type b} {f : A → B}
    (iso : ∀ x y → f x ≡ f y ↔ x ≡ y) →
    (∀ x → _↔_.from (iso x x) (refl x) ≡ refl (f x)) →
    ∀ {x y z p q} →
    trans (_↔_.to (iso x y) p) (_↔_.to (iso y z) q) ≡
    _↔_.to (iso x z) (trans p q)
  trans-to-to≡to-trans {f = f} iso iso-refl {x} {y} {z} {p} {q} =
    trans (_↔_.to (iso x y) p) (_↔_.to (iso y z) q)               ≡⟨ elim₁ (λ {x} p → trans p (_↔_.to (iso y z) q) ≡
                                                                                _↔_.to (iso x z) (trans (_↔_.from (iso x y) p) q)) (
        trans (refl y) (_↔_.to (iso y z) q)                              ≡⟨ trans-reflˡ _ ⟩
        _↔_.to (iso y z) q                                               ≡⟨ cong (_↔_.to (iso y z)) $ sym $ trans-reflˡ _ ⟩
        _↔_.to (iso y z) (trans (refl (f y)) q)                          ≡⟨ cong (_↔_.to (iso y z) ⊚ flip trans _) $ sym $ iso-refl y ⟩∎
        _↔_.to (iso y z) (trans (_↔_.from (iso y y) (refl y)) q)         ∎)
                                                                           (_↔_.to (iso x y) p) ⟩
    _↔_.to (iso x z)
      (trans (_↔_.from (iso x y) (_↔_.to (iso x y) p)) q)         ≡⟨ cong (_↔_.to (iso x z) ⊚ flip trans _) $
                                                                       _↔_.left-inverse-of (iso _ _) _ ⟩∎
    _↔_.to (iso x z) (trans p q)                                  ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Andreas, 2018-08-14, re issue #1558
-- Termination checking functions over inductive-inductive types

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

mutual
  data Cxt : Set where
    ε    :  Cxt
    _,_  :  (Γ : Cxt) (A : Ty Γ) → Cxt

  data Ty : (Γ : Cxt) → Set where
    u  :  ∀ Γ → Ty Γ
    Π  :  ∀ Γ (A : Ty Γ) (B : Ty (Γ , A)) → Ty Γ

mutual
  f : Cxt → Cxt
  f ε        =  ε
  f (Γ , T)  =  (f Γ , g Γ T)

  g : ∀ Γ → Ty Γ → Ty (f Γ)
  g Γ (u .Γ)      =  u (f Γ)
  g Γ (Π .Γ A B)  =  Π (f Γ) (g Γ A) (g (Γ , A) B)

-- The type of g contains a call
--
--   g Γ _ --> f Γ
--
-- which is now recorded by the termination checker.

-- Should pass termination.


text:
-- Andreas, 2018-11-23, issue #3304, report and test case by Nisse

open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

map : {A B : Set} {P : A → Set} {Q : B → Set} →
      (f : A → B) → (∀ {x} → P x → Q (f x)) →
      Σ A P → Σ B Q
map f g (x , y) = (f x , g y)

postulate
  F         : Set → Set → Set
  apply     : {A B : Set} → F A B → A → B
  construct : {A B : Set} → (A → B) → F A B
  A         : Set
  B         : A → Set
  f         : A → A
  g         : ∀ {x} → B x → B (f x)

mutual

  k : Σ A B → Σ A _
  k = map f g

  h : F (Σ A B) (Σ A B)
  h = construct k

P : ∀ {x y} → k x ≡ k y → Set₁
P refl = Set

-- WAS: internal error in
-- TypeChecking.Rules.Term.catchIlltypedPatternBlockedOnMeta
--
-- EXPECTED:
-- I'm not sure if there should be a case for the constructor refl,
-- because I get stuck when trying to solve the following unification
-- problems (inferred index ≟ expected index):
--   k x ≟ k y
-- when checking that the pattern refl has type k x ≡ k y


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

open import LogicalFormulae
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.IntegralDomains.Definition

module Rings.Associates.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where

open import Rings.Divisible.Definition R
open import Rings.IntegralDomains.Lemmas intDom
open import Rings.Associates.Definition intDom
open import Rings.Ideals.Definition R
open Setoid S
open Ring R
open Equivalence eq

associatesEquiv : Equivalence Associates
Equivalence.reflexive associatesEquiv {x} = 1R , ((1R , identIsIdent) ,, symmetric (transitive *Commutative identIsIdent))
Equivalence.symmetric associatesEquiv {x} {y} (a , ((invA , prInv) ,, x=ya)) = invA , ((a , transitive *Commutative prInv) ,, transitive (symmetric identIsIdent) (transitive (*WellDefined (symmetric prInv) reflexive) (transitive *Commutative (transitive *Associative (*WellDefined (symmetric x=ya) reflexive)))))
Equivalence.transitive associatesEquiv {x} {y} {z} (a , ((invA , prInvA) ,, x=ya)) (b , ((invB , prInvB) ,, y=zb)) = (a * b) , (((invA * invB) , transitive *Associative (transitive (*WellDefined (transitive *Commutative *Associative) reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined (transitive *Commutative prInvA) prInvB) identIsIdent)))) ,, transitive x=ya (transitive (*WellDefined y=zb reflexive) (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative))))

associateImpliesMutualDivision : {a b : A} → Associates a b → a ∣ b
associateImpliesMutualDivision {a} {b} (x , ((invX , prInvX) ,, a=bx)) = invX , transitive (transitive (*WellDefined a=bx reflexive) (transitive (transitive (symmetric *Associative) (*WellDefined reflexive prInvX)) *Commutative)) identIsIdent

mutualDivisionImpliesAssociate : {a b : A} → (a ∣ b) → (b ∣ a) → ((a ∼ 0R) → False) → Associates a b
mutualDivisionImpliesAssociate {a} {b} (r , ar=b) (s , bs=a) a!=0 = s , ((r , cancelIntDom {a = a} (transitive (transitive (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (*WellDefined ar=b reflexive))) bs=a) (transitive (symmetric identIsIdent) *Commutative)) a!=0) ,, symmetric bs=a)

mutualDivisionImpliesAssociate' : {a b : A} → (a ∣ b) → (b ∣ a) → (a ∼ 0R) → Associates a b
mutualDivisionImpliesAssociate' {a} {b} (r , ar=b) (s , bs=a) a=0 = 1R , ((1R , identIsIdent) ,, transitive a=0 (symmetric (transitive (*WellDefined b=0 reflexive) (transitive *Commutative timesZero))))
  where
    b=0 : b ∼ 0R
    b=0 = transitive (symmetric ar=b) (transitive (transitive *Commutative (*WellDefined reflexive a=0)) (timesZero {r}))

associateImpliesGeneratedIdealsEqual : {a b : A} → Associates a b → {x : A} → generatedIdealPred a x → generatedIdealPred b x
associateImpliesGeneratedIdealsEqual {a} {b} (r , ((s , rs=1) ,, a=br)) {x} (c , ac=x) = (r * c) , transitive *Associative (transitive (*WellDefined (symmetric a=br) reflexive) ac=x)

associateImpliesGeneratedIdealsEqual' : {a b : A} → Associates a b → {x : A} → generatedIdealPred b x → generatedIdealPred a x
associateImpliesGeneratedIdealsEqual' assoc = associateImpliesGeneratedIdealsEqual (Equivalence.symmetric associatesEquiv assoc)


text:
{-# OPTIONS --universe-polymorphism #-}

open import Categories.Category

module Categories.Object.Products.Properties {o ℓ e}
  (C : Category o ℓ e) where

open Category C

open import Level

import Categories.Object.Terminal
open Categories.Object.Terminal C

import Categories.Object.BinaryProducts
open Categories.Object.BinaryProducts C

import Categories.Object.Products
open Categories.Object.Products C

import Categories.Morphisms
open Categories.Morphisms C

module Properties (P : Products) where
  open Products P

  open Terminal terminal
  open BinaryProducts binary
  open HomReasoning
  open Equiv

  unitˡ : ∀ {X} → (⊤ × X) ≅ X
  unitˡ {X} = record
    { f = π₂
    ; g = ⟨ ! , id {X} ⟩
    ; iso = record
      { isoˡ =
        begin
          ⟨ ! , id {X} ⟩ ∘ π₂
        ↓⟨ ⟨⟩∘ ⟩
          ⟨ ! ∘ π₂ , id ∘ π₂ ⟩
        ↓⟨ ⟨⟩-cong₂ (!-unique₂ (! ∘ π₂) π₁) (identityˡ) ⟩
          ⟨ π₁ , π₂ ⟩
        ↓⟨ η ⟩
          id
        ∎
      ; isoʳ = commute₂
      }
    }

  .unitˡ-natural : ∀ {X Y} {f : X ⇒ Y} → ⟨ ! , id {Y} ⟩ ∘ f ≡ second f ∘ ⟨ ! , id {X} ⟩
  unitˡ-natural {f = f} =
    begin
      ⟨ ! , id ⟩ ∘ f
    ↓⟨ ⟨⟩∘ ⟩
      ⟨ ! ∘ f , id ∘ f ⟩
    ↑⟨ ⟨⟩-cong₂ (!-unique (! ∘ f)) (id-comm {f = f}) ⟩
      ⟨ ! , f ∘ id ⟩
    ↑⟨ second∘⟨⟩ ⟩
      second f ∘ ⟨ ! , id ⟩
    ∎

  unitʳ : ∀ {X} → (X × ⊤) ≅ X
  unitʳ {X} = record
    { f = π₁
    ; g = ⟨ id {X} , ! ⟩
    ; iso = record
      { isoˡ =
        begin
          ⟨ id {X} , ! ⟩ ∘ π₁
        ↓⟨ ⟨⟩∘ ⟩
          ⟨ id ∘ π₁ , ! ∘ π₁ ⟩
        ↓⟨ ⟨⟩-cong₂ (identityˡ) (!-unique₂ (! ∘ π₁) π₂)  ⟩
          ⟨ π₁ , π₂ ⟩
        ↓⟨ η ⟩
          id
        ∎
      ; isoʳ = commute₁
      }
    }

  .unitʳ-natural : ∀ {X Y} {f : X ⇒ Y} → ⟨ id , ! ⟩ ∘ f ≡ first f ∘ ⟨ id , ! ⟩
  unitʳ-natural {f = f} =
    begin
      ⟨ id , ! ⟩ ∘ f
    ↓⟨ ⟨⟩∘ ⟩
      ⟨ id ∘ f , ! ∘ f ⟩
    ↑⟨ ⟨⟩-cong₂ (id-comm {f = f}) (!-unique (! ∘ f)) ⟩
      ⟨ f ∘ id , ! ⟩
    ↑⟨ first∘⟨⟩ ⟩
      first f ∘ ⟨ id , ! ⟩
    ∎

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Check where

open import Data.Fin         using (Fin)
open import Data.Nat         using (ℕ; suc)
open import Data.Vec         hiding (head; tail)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (Dec; yes; no)

open import Types
open import Utils

data Check {n} (Γ : Ctx n) : Syntax → Set where
  yes : (τ : Type) (t : Term Γ τ) → Check Γ (erase t)
  no  : {e : Syntax} → Check Γ e

check : ∀ {n} (Γ : Ctx n) (t : Syntax) → Check Γ t
check Γ bitI = yes 𝔹 bitI
check Γ bitO = yes 𝔹 bitO

check Γ [] = yes (𝔹⁺ 0) []

check Γ (x ∷ xs) with check Γ x | check Γ xs
check Γ (.(erase t) ∷ .(erase t₁)) | yes 𝔹 t | yes (𝔹⁺ n) t₁ = yes (𝔹⁺ (suc n)) (t ∷ t₁)
check Γ (x ∷ xs) | _ | _ = no

check Γ (x nand y) with check Γ x | check Γ y
check Γ (._ nand ._) | yes 𝔹 x | yes 𝔹 y = yes 𝔹 (x nand y)
check Γ (_ nand _) | _ | _ = no

check Γ (reg xt ft) with check Γ xt | check Γ ft
check Γ (reg ._ ._) | yes τ xt | yes (τ′ ⇒ (τ″ × σ)) ft with τ ≟T τ′ | τ ≟T τ″
check Γ (reg ._ ._) | yes τ xt | yes (.τ ⇒ (.τ × σ)) ft | yes refl | yes refl = yes _ (reg xt ft)
check Γ (reg ._ ._) | yes τ xt | yes (τ′ ⇒ (τ″ × σ)) ft | _ | _ = no
check Γ (reg _ _) | _ | _ = no

check Γ (pair xt yt) with check Γ xt | check Γ yt
check Γ (pair ._ ._) | yes σ t | yes τ t₁ with σ ≟T τ
check Γ (pair ._ ._) | yes σ t | yes .σ t₁ | yes refl = yes (σ × σ) (pair t t₁)
check Γ (pair ._ ._) | yes σ t | yes τ t₁ | no _ = no
check Γ (pair xt yt) | _ | _ = no

check Γ (latest t) with check Γ t
check Γ (latest ._) | yes (ℂ τ) t′ = yes τ (latest t′)
check Γ (latest t) | _ = no

check Γ (head x) with check Γ x
check Γ (head ._) | yes (𝔹⁺ (suc n)) t = yes 𝔹 (head t)
check Γ (head _) | _ = no

check Γ (tail xs) with check Γ xs
check Γ (tail .(erase t)) | yes (𝔹⁺ (suc n)) t = yes (𝔹⁺ n) (tail t)
check Γ (tail xs) | _ = no

check {n} Γ (var i) with fromℕ n i
check Γ (var ._) | yes m = yes (lookup m Γ) (var m refl)
check Γ (var ._) | no m = no

check Γ (x ∙ y) with check Γ x | check Γ y
check Γ (._ ∙ ._) | yes (σ ⇒ τ) x | yes σ′ y with σ ≟T σ′
check Γ (._ ∙ ._) | yes (σ ⇒ τ) x | yes .σ y | yes refl = yes τ (x ∙ y)
check Γ (._ ∙ ._) | yes (σ ⇒ τ) x | yes σ′ y | no ¬p = no
check Γ (x ∙ y) | _ | _ = no

check Γ (lam τ x) with check (τ ∷ Γ) x
check Γ (lam τ ._) | yes τ₁ t = yes (τ ⇒ τ₁) (lam t)
check Γ (lam τ x) | no = no

max_stars_repo_name: bens/hwlc

max_issues_repo_name: bens/hwlc

max_forks_repo_name: bens/hwlc


text:
data Bool : Set where
  true : Bool
  false : Bool

if_then_else : ∀ {l} {A : Set l} -> Bool -> A -> A -> A
if true then t else e = t
if false then t else e = e

if2_,_then_else1_else2_else_ : ∀ {l} {A : Set l} -> (b1 b2 : Bool) -> (t e1 e2 e : A) -> A
if2 true , true then t else1 e1 else2 e2 else e = t
if2 true , false then t else1 e1 else2 e2 else e = e1
if2 false , true then t else1 e1 else2 e2 else e = e2
if2 false , false then t else1 e1 else2 e2 else e = e

example : Bool
example = if2 true , false then true else1 false else2 true else false

max_issues_repo_name: seanwallawalla-forks/RosettaCodeData

max_forks_repo_name: seanwallawalla-forks/RosettaCodeData


text:
{-# OPTIONS --without-K #-}
module sets.vec.properties where

open import equality.core
open import function.core
open import function.extensionality
open import function.isomorphism
open import sets.nat.core using (ℕ; zero; suc)
open import sets.fin using (Fin; zero; suc)
open import sets.vec.core

tabulate-lookup : ∀ {i}{A : Set i}{n : ℕ}
                → (xs : Vec A n)
                → tabulate (lookup xs) ≡ xs
tabulate-lookup [] = refl
tabulate-lookup (x ∷ xs) = ap (_∷_ x) (tabulate-lookup xs)

lookup-tabulate-funext : ∀ {i}{A : Set i}{n : ℕ}
                    → (f : Fin n → A)(i : Fin n)
                    → lookup (tabulate f) i ≡ f i
lookup-tabulate-funext {n = zero} f ()
lookup-tabulate-funext {n = suc m} f zero = refl
lookup-tabulate-funext {n = suc m} f (suc i) =
  lookup-tabulate-funext (f ∘ suc) i

lookup-tabulate : ∀ {i}{A : Set i}{n : ℕ}
                → (f : Fin n → A)
                → lookup (tabulate f) ≡ f
lookup-tabulate f = funext (lookup-tabulate-funext f)

lookup-iso : ∀ {i}{A : Set i}{n : ℕ}
           → Vec A n ≅ (Fin n → A)
lookup-iso = iso lookup tabulate tabulate-lookup lookup-tabulate

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
------------------------------------------------------------------------
-- The two definitions of context extensions are isomorphic
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Context.Extension.Isomorphic
  {i u e} (Uni : IndexedUniverse i u e) where

import deBruijn.Context.Basics          as Basics
import deBruijn.Context.Extension.Left  as Left
import deBruijn.Context.Extension.Right as Right
open import Function.Base
open import Function.Inverse using (_↔_)
import Relation.Binary.PropositionalEquality as P

open Basics Uni
open Left   Uni
open Right  Uni
open P.≡-Reasoning

-- Ctxt₊-s can be turned into Ctxt⁺-s.

₊-to-⁺ : ∀ {Γ} → Ctxt₊ Γ → Ctxt⁺ Γ
₊-to-⁺ ε        = ε
₊-to-⁺ (σ ◅ Γ₊) = ε ▻ σ ⁺++⁺ ₊-to-⁺ Γ₊

abstract

  -- The semantics is preserved.

  ++⁺-₊-to-⁺ : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → Γ ++₊ Γ₊ ≅-Ctxt Γ ++⁺ ₊-to-⁺ Γ₊
  ++⁺-₊-to-⁺     ε        = P.refl
  ++⁺-₊-to-⁺ {Γ} (σ ◅ Γ₊) = begin
    Γ ▻ σ ++₊ Γ₊                  ≡⟨ ++⁺-₊-to-⁺ Γ₊ ⟩
    Γ ▻ σ ++⁺ ₊-to-⁺ Γ₊           ≡⟨ ++⁺-++⁺ (ε ▻ σ) (₊-to-⁺ Γ₊) ⟩
    Γ ++⁺ (ε ▻ σ ⁺++⁺ ₊-to-⁺ Γ₊)  ∎

mutual

  -- Ctxt⁺-s can be turned into Ctxt₊-s.

  ⁺-to-₊ : ∀ {Γ} → Ctxt⁺ Γ → Ctxt₊ Γ
  ⁺-to-₊ ε        = ε
  ⁺-to-₊ (Γ⁺ ▻ σ) =
    ⁺-to-₊ Γ⁺ ₊++₊ P.subst Ctxt₊ (++₊-⁺-to-₊ Γ⁺) (σ ◅ ε)

  abstract

    -- The semantics is preserved.

    ++₊-⁺-to-₊ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Γ ++⁺ Γ⁺ ≅-Ctxt Γ ++₊ ⁺-to-₊ Γ⁺
    ++₊-⁺-to-₊     ε        = P.refl
    ++₊-⁺-to-₊ {Γ} (Γ⁺ ▻ σ) =
      let σ◅ε = P.subst Ctxt₊ (++₊-⁺-to-₊ Γ⁺) (σ ◅ ε)

      in begin
      Γ ++⁺ Γ⁺ ▻ σ                ≡⟨ P.refl ⟩
      Γ ++⁺ Γ⁺ ++₊ (σ ◅ ε)        ≡⟨ P.sym $ ++₊-cong $ drop-subst-Ctxt₊ id (++₊-⁺-to-₊ Γ⁺) ⟩
      Γ ++₊ ⁺-to-₊ Γ⁺ ++₊ σ◅ε     ≡⟨ ++₊-++₊ (⁺-to-₊ Γ⁺) σ◅ε ⟩
      Γ ++₊ (⁺-to-₊ Γ⁺ ₊++₊ σ◅ε)  ∎

-- Some congruence lemmas.

₊-to-⁺-cong : ∀ {Γ₁} {Γ₊₁ : Ctxt₊ Γ₁}
                {Γ₂} {Γ₊₂ : Ctxt₊ Γ₂} →
              Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ₊-to-⁺ Γ₊₁ ≅-Ctxt⁺ ₊-to-⁺ Γ₊₂
₊-to-⁺-cong P.refl = P.refl

⁺-to-₊-cong : ∀ {Γ₁} {Γ⁺₁ : Ctxt⁺ Γ₁}
                {Γ₂} {Γ⁺₂ : Ctxt⁺ Γ₂} →
              Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ⁺-to-₊ Γ⁺₁ ≅-Ctxt₊ ⁺-to-₊ Γ⁺₂
⁺-to-₊-cong P.refl = P.refl

-- Ctxt⁺ and Ctxt₊ are isomorphic.

Ctxt⁺↔Ctxt₊ : ∀ Γ → Ctxt⁺ Γ ↔ Ctxt₊ Γ
Ctxt⁺↔Ctxt₊ Γ = record
  { to         = P.→-to-⟶ ⁺-to-₊
  ; from       = P.→-to-⟶ ₊-to-⁺
  ; inverse-of = record
    { left-inverse-of  = λ Γ⁺ → ≅-Ctxt⁺-⇒-≡ $ ₊-to-⁺-⁺-to-₊ Γ⁺
    ; right-inverse-of = λ Γ₊ → ≅-Ctxt₊-⇒-≡ $ ⁺-to-₊-₊-to-⁺ Γ₊
    }
  }
  where
  abstract
    ₊-to-⁺-⁺-to-₊ : (Γ⁺ : Ctxt⁺ Γ) → ₊-to-⁺ (⁺-to-₊ Γ⁺) ≅-Ctxt⁺ Γ⁺
    ₊-to-⁺-⁺-to-₊ Γ⁺ = cancel-++⁺-left _ _ (begin
      Γ ++⁺ ₊-to-⁺ (⁺-to-₊ Γ⁺)  ≡⟨ P.sym $ ++⁺-₊-to-⁺ (⁺-to-₊ Γ⁺) ⟩
      Γ ++₊ (⁺-to-₊ Γ⁺)         ≡⟨ P.sym $ ++₊-⁺-to-₊ Γ⁺ ⟩
      Γ ++⁺ Γ⁺                  ∎)

    ⁺-to-₊-₊-to-⁺ : (Γ₊ : Ctxt₊ Γ) → ⁺-to-₊ (₊-to-⁺ Γ₊) ≅-Ctxt₊ Γ₊
    ⁺-to-₊-₊-to-⁺ Γ₊ = cancel-++₊-left _ _ (begin
      Γ ++₊ ⁺-to-₊ (₊-to-⁺ Γ₊)  ≡⟨ P.sym $ ++₊-⁺-to-₊ (₊-to-⁺ Γ₊) ⟩
      Γ ++⁺ (₊-to-⁺ Γ₊)         ≡⟨ P.sym $ ++⁺-₊-to-⁺ Γ₊ ⟩
      Γ ++₊ Γ₊                  ∎)

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
module UniDB.Morph.Sim where

open import UniDB.Spec
open import UniDB.Subst.Core
open import UniDB.Morph.Depth
import Level
open import Relation.Binary.PropositionalEquality

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

record Sim (T : STX) (γ₁ γ₂ : Dom) : Set where
  constructor sim
  field
    lk-sim : (i : Ix γ₁) → T γ₂
open Sim public

module _ {T : STX} where
  instance
    iLkSim : {{vrT : Vr T}} → Lk T (Sim T)
    lk {{iLkSim}} = lk-sim

    iWkSim : {{wkT : Wk T}} → {γ₁ : Dom} → Wk (Sim T γ₁)
    wk₁     {{iWkSim}}         (sim f) = sim (wk₁ ∘ f)
    wk      {{iWkSim}} δ       (sim f) = sim (wk δ ∘ f)
    wk-zero {{iWkSim {{wkT}}}} (sim f) = cong sim (ext (wk-zero {T} ∘ f))
      where postulate ext : Extensionality Level.zero Level.zero
    wk-suc {{iWkSim}} δ        (sim f) = cong sim (ext (wk-suc {T} δ ∘ f))
      where postulate ext : Extensionality Level.zero Level.zero

    iSnocSim : Snoc T (Sim T)
    snoc {{iSnocSim}} (sim f) t = sim λ
      { zero    → t
      ; (suc i) → f i
      }

    iUpSim : {{vrT : Vr T}} {{wkT : Wk T}} → Up (Sim T)
    _↑₁ {{iUpSim}} ξ = snoc {T} {Sim T} (wk₁ ξ) (vr {T} zero)
    _↑_ {{iUpSim}} ξ 0 = ξ
    _↑_ {{iUpSim}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
    ↑-zero {{iUpSim}} ξ = refl
    ↑-suc {{iUpSim}} ξ δ⁺ = refl

    iIdmSim : {{vrT : Vr T}} → Idm (Sim T)
    idm {{iIdmSim}} γ = sim (vr {T})

    iWkmSim : {{vrT : Vr T}} → Wkm (Sim T)
    wkm {{iWkmSim}} δ = sim (vr {T} ∘ wk δ)

    iBetaSim : {{vrT : Vr T}} → Beta T (Sim T)
    beta {{iBetaSim}} t = snoc {T} {Sim T} (idm {Sim T} _) t

    iCompSim : {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}} → Comp (Sim T)
    lk-sim (_⊙_ {{iCompSim}} ξ ζ) i =
      ap {T} {T} {Sim T} ζ (lk {T} {Sim T} ξ i)

    iLkUpSim : {{vrT : Vr T}} {{wkT : Wk T}} → LkUp T (Sim T)
    lk-↑₁-zero {{iLkUpSim}} ξ         = refl
    lk-↑₁-suc  {{iLkUpSim}} ξ zero    = refl
    lk-↑₁-suc  {{iLkUpSim}} ξ (suc i) = refl

    iLkWkmSim : {{vrT : Vr T}} → LkWkm T (Sim T)
    lk-wkm {{iLkWkmSim}} δ i = refl

    iLkIdmSim : {{vrT : Vr T}} → LkIdm T (Sim T)
    lk-idm {{iLkIdmSim}} i = refl

    iLkCompSim : {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}} → LkCompAp T (Sim T)
    lk-⊙-ap {{iLkCompSim}} ξ₁ ξ₂ i = refl

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

module SimIxInstances (T : STX) where

  instance
    iLkSimIx : {{vrT : Vr T}} → Lk T (Sim Ix)
    lk {{iLkSimIx}} ξ i = vr {T} (lk {Ix} {Sim Ix} ξ i)

    iLkUpSimIx : {{vrT : Vr T}} {{wkT : Wk T}}
      {{wkVrT : WkVr T}} → LkUp T (Sim Ix)
    lk-↑₁-zero {{iLkUpSimIx}} ξ   = refl
    lk-↑₁-suc  {{iLkUpSimIx}} ξ i = sym (wk₁-vr {T} (lk {Ix} {Sim Ix} ξ i))

    iLkWkmSimIx : {{vrT : Vr T}} → LkWkm T (Sim Ix)
    lk-wkm {{iLkWkmSimIx}} δ i = refl

    iLkIdmSimIx : {{vrT : Vr T}} → LkIdm T (Sim Ix)
    lk-idm {{iLkIdmSimIx}} i = refl

    iLkCompSimIx : {{vrT : Vr T}} {{apTT : Ap T T}}
      {{apVrT : ApVr T}} → LkCompAp T (Sim Ix)
    lk-⊙-ap {{iLkCompSimIx}} ξ₁ ξ₂ i =
      sym (ap-vr {T} {Sim Ix} ξ₂ (lk {Ix} {Sim Ix} ξ₁ i))

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda