text:
{-# OPTIONS --allow-unsolved-metas #-}
module nat where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary
open import  Relation.Binary.PropositionalEquality
open import  Relation.Binary.Core
open import  Relation.Binary.Definitions
open import  logic
open import Level hiding ( zero ; suc )

nat-<> : { x y : ℕ } → x < y → y < x → ⊥
nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x

nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x

nat-<≡ : { x : ℕ } → x < x → ⊥
nat-<≡  (s≤s lt) = nat-<≡ lt

nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
nat-≡< refl lt = nat-<≡ lt

¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
¬a≤a  (s≤s lt) = ¬a≤a  lt

a<sa : {la : ℕ} → la < suc la
a<sa {zero} = s≤s z≤n
a<sa {suc la} = s≤s a<sa

=→¬< : {x : ℕ  } → ¬ ( x < x )
=→¬< {zero} ()
=→¬< {suc x} (s≤s lt) = =→¬< lt

>→¬< : {x y : ℕ  } → (x < y ) → ¬ ( y < x )
>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x

<-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
<-∨ {zero} {zero} (s≤s z≤n) = case1 refl
<-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n)
<-∨ {suc x} {zero} (s≤s ())
<-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt
<-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
<-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)

max : (x y : ℕ) → ℕ
max zero zero = zero
max zero (suc x) = (suc x)
max (suc x) zero = (suc x)
max (suc x) (suc y) = suc ( max x y )

-- _*_ : ℕ → ℕ → ℕ
-- _*_ zero _ = zero
-- _*_ (suc n) m = m + ( n * m )

-- x ^ y
exp : ℕ → ℕ → ℕ
exp _ zero = 1
exp n (suc m) = n * ( exp n m )

div2 : ℕ → (ℕ ∧ Bool )
div2 zero =  ⟪ 0 , false ⟫
div2 (suc zero) =  ⟪ 0 , true ⟫
div2 (suc (suc n)) =  ⟪ suc (proj1 (div2 n)) , proj2 (div2 n) ⟫ where
    open _∧_

div2-rev : (ℕ ∧ Bool ) → ℕ
div2-rev ⟪ x , true ⟫ = suc (x + x)
div2-rev ⟪ x , false ⟫ = x + x

div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
div2-eq zero = refl
div2-eq (suc zero) = refl
div2-eq (suc (suc x)) with div2 x | inspect div2 x
... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫
     div2-rev ⟪ suc x1 , true ⟫ ≡⟨⟩
     suc (suc (x1 + suc x1)) ≡⟨ cong (λ k → suc (suc k )) (+-comm x1  _ ) ⟩
     suc (suc (suc (x1 + x1))) ≡⟨⟩
     suc (suc (div2-rev ⟪ x1 , true ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩
     suc (suc (div2-rev (div2 x)))      ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩
     suc (suc x) ∎  where open ≡-Reasoning
... | ⟪ x1 , false ⟫ | record { eq = eq1 } = begin
     div2-rev ⟪ suc x1 , false ⟫ ≡⟨⟩
     suc (x1 + suc x1) ≡⟨ cong (λ k → (suc k )) (+-comm x1  _ ) ⟩
     suc (suc (x1 + x1)) ≡⟨⟩
     suc (suc (div2-rev ⟪ x1 , false ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩
     suc (suc (div2-rev (div2 x)))      ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩
     suc (suc x) ∎  where open ≡-Reasoning

sucprd : {i : ℕ } → 0 < i  → suc (pred i) ≡ i
sucprd {suc i} 0<i = refl

0<s : {x : ℕ } → zero < suc x
0<s {_} = s≤s z≤n

px<py : {x y : ℕ } → pred x  < pred y → x < y
px<py {zero} {suc y} lt = 0<s
px<py {suc zero} {suc (suc y)} (s≤s lt) = s≤s 0<s
px<py {suc (suc x)} {suc (suc y)} (s≤s lt) = s≤s (px<py {suc x} {suc y} lt)

minus : (a b : ℕ ) →  ℕ
minus a zero = a
minus zero (suc b) = zero
minus (suc a) (suc b) = minus a b

_-_ = minus

m+= : {i j  m : ℕ } → m + i ≡ m + j → i ≡ j
m+= {i} {j} {zero} refl = refl
m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )

+m= : {i j  m : ℕ } → i + m ≡ j + m → i ≡ j
+m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )

less-1 :  { n m : ℕ } → suc n < m → n < m
less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)

sa=b→a<b :  { n m : ℕ } → suc n ≡ m → n < m
sa=b→a<b {0} {suc zero} refl = s≤s z≤n
sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)

minus+n : {x y : ℕ } → suc x > y  → minus x y + y ≡ x
minus+n {x} {zero} _ = trans (sym (+-comm zero  _ )) refl
minus+n {zero} {suc y} (s≤s ())
minus+n {suc x} {suc y} (s≤s lt) = begin
           minus (suc x) (suc y) + suc y
        ≡⟨ +-comm _ (suc y)    ⟩
           suc y + minus x y
        ≡⟨ cong ( λ k → suc k ) (
           begin
                 y + minus x y
              ≡⟨ +-comm y  _ ⟩
                 minus x y + y
              ≡⟨ minus+n {x} {y} lt ⟩
                 x
           ∎
           ) ⟩
           suc x
        ∎  where open ≡-Reasoning

<-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
<-minus-0 {x} {suc _} {zero} lt = lt
<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt

<-minus : {x y z : ℕ } → x + z < y + z → x < y
<-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt )

x≤x+y : {z y : ℕ } → z ≤ z + y
x≤x+y {zero} {y} = z≤n
x≤x+y {suc z} {y} = s≤s  (x≤x+y {z} {y})

x≤y+x : {z y : ℕ } → z ≤ y + z
x≤y+x {z} {y} = subst (λ k → z ≤ k ) (+-comm _ y ) x≤x+y

<-plus : {x y z : ℕ } → x < y → x + z < y + z
<-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y  )
<-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt)

<-plus-0 : {x y z : ℕ } → x < y → z + x < z + y
<-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt )

≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z
≤-plus {0} {y} {zero} z≤n = z≤n
≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y
≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt )

≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y
≤-plus-0 {x} {y} {zero} lt = lt
≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt )

x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z
x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n
x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )

*≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z
*≤ lt = *-mono-≤ lt ≤-refl

*< : {x y z : ℕ } → x < y → x * suc z < y * suc z
*< {zero} {suc y} lt = s≤s z≤n
*< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)

<to<s : {x y  : ℕ } → x < y → x < suc y
<to<s {zero} {suc y} (s≤s lt) = s≤s z≤n
<to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)

<tos<s : {x y  : ℕ } → x < y → suc x < suc y
<tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n)
<tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt)

<to≤ : {x y  : ℕ } → x < y → x ≤ y
<to≤ {zero} {suc y} (s≤s z≤n) = z≤n
<to≤ {suc x} {suc y} (s≤s lt) = s≤s (<to≤ {x} {y}  lt)

refl-≤s : {x : ℕ } → x ≤ suc x
refl-≤s {zero} = z≤n
refl-≤s {suc x} = s≤s (refl-≤s {x})

refl-≤ : {x : ℕ } → x ≤ x
refl-≤ {zero} = z≤n
refl-≤ {suc x} = s≤s (refl-≤ {x})

x<y→≤ : {x y : ℕ } → x < y →  x ≤ suc y
x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)

≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j
≤→= {0} {0} z≤n z≤n = refl
≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i )

px≤x : {x  : ℕ } → pred x ≤ x
px≤x {zero} = refl-≤
px≤x {suc x} = refl-≤s

px≤py : {x y : ℕ } → x ≤ y → pred x  ≤ pred y
px≤py {zero} {zero} lt = refl-≤
px≤py {zero} {suc y} lt = z≤n
px≤py {suc x} {suc y} (s≤s lt) = lt

open import Data.Product

i-j=0→i=j : {i j  : ℕ } → j ≤ i  → i - j ≡ 0 → i ≡ j
i-j=0→i=j {zero} {zero} _ refl = refl
i-j=0→i=j {zero} {suc j} () refl
i-j=0→i=j {suc i} {zero} z≤n ()
i-j=0→i=j {suc i} {suc j} (s≤s lt) eq = cong suc (i-j=0→i=j {i} {j} lt eq)

m*n=0⇒m=0∨n=0 : {i j : ℕ} → i * j ≡ 0 → (i ≡ 0) ∨ ( j ≡ 0 )
m*n=0⇒m=0∨n=0 {zero} {j} refl = case1 refl
m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl

minus+1 : {x y  : ℕ } → y ≤ x  → suc (minus x y)  ≡ minus (suc x) y
minus+1 {zero} {zero} y≤x = refl
minus+1 {suc x} {zero} y≤x = refl
minus+1 {suc x} {suc y} (s≤s y≤x) = minus+1 {x} {y} y≤x

minus+yz : {x y z : ℕ } → z ≤ y  → x + minus y z  ≡ minus (x + y) z
minus+yz {zero} {y} {z} _ = refl
minus+yz {suc x} {y} {z} z≤y = begin
         suc x + minus y z ≡⟨ cong suc ( minus+yz z≤y ) ⟩
         suc (minus (x + y) z) ≡⟨ minus+1 {x + y} {z} (≤-trans z≤y (subst (λ g → y ≤ g) (+-comm y x) x≤x+y) ) ⟩
         minus (suc x + y) z ∎  where open ≡-Reasoning

minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
minus<=0 {0} {zero} z≤n = refl
minus<=0 {0} {suc y} z≤n = refl
minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le

minus>0 : {x y : ℕ } → x < y → 0 < minus y x
minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt

minus>0→x<y : {x y : ℕ } → 0 < minus y x  → x < y
minus>0→x<y {x} {y} lt with <-cmp x y
... | tri< a ¬b ¬c = a
... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< (sym (minus<=0 {x} ≤-refl)) lt )
... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (minus<=0 {y} (≤-trans refl-≤s c ))) lt )

minus+y-y : {x y : ℕ } → (x + y) - y  ≡ x
minus+y-y {zero} {y} = minus<=0 {zero + y} {y} ≤-refl
minus+y-y {suc x} {y} = begin
         (suc x + y) - y ≡⟨ sym (minus+1 {_} {y} x≤y+x) ⟩
         suc ((x + y) - y) ≡⟨ cong suc (minus+y-y {x} {y}) ⟩
         suc x ∎  where open ≡-Reasoning

minus+yx-yz : {x y z : ℕ } → (y + x) - (y + z)  ≡ x - z
minus+yx-yz {x} {zero} {z} = refl
minus+yx-yz {x} {suc y} {z} = minus+yx-yz {x} {y} {z}

minus+xy-zy : {x y z : ℕ } → (x + y) - (z + y)  ≡ x - z
minus+xy-zy {x} {y} {z} = subst₂ (λ j k → j - k ≡ x - z  ) (+-comm y x) (+-comm y z) (minus+yx-yz {x} {y} {z})

y-x<y : {x y : ℕ } → 0 < x → 0 < y  → y - x  <  y
y-x<y {x} {y} 0<x 0<y with <-cmp x (suc y)
... | tri< a ¬b ¬c = +-cancelʳ-< {x} (y - x) y ( begin
         suc ((y - x) + x) ≡⟨ cong suc (minus+n {y} {x} a ) ⟩
         suc y  ≡⟨ +-comm 1 _ ⟩
         y + suc 0  ≤⟨ +-mono-≤ ≤-refl 0<x ⟩
         y + x ∎ )  where open ≤-Reasoning
... | tri≈ ¬a refl ¬c = subst ( λ k → k < y ) (sym (minus<=0 {y} {x} refl-≤s )) 0<y
... | tri> ¬a ¬b c = subst ( λ k → k < y ) (sym (minus<=0 {y} {x} (≤-trans (≤-trans refl-≤s refl-≤s) c))) 0<y -- suc (suc y) ≤ x → y ≤ x

open import Relation.Binary.Definitions

distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z)
distr-minus-* {x} {zero} {z} = refl
distr-minus-* {x} {suc y} {z} with <-cmp x y
distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin
          minus x (suc y) * z
        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩
           0 * z
        ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩
          minus (x * z) (z + y * z)
        ∎  where
            open ≡-Reasoning
            le : x * z ≤ z + y * z
            le  = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where
               lemma : x * z ≤ y * z
               lemma = *≤ {x} {y} {z} (<to≤ a)
distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin
          minus x (suc y) * z
        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩
           0 * z
        ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩
          minus (x * z) (z + y * z)
        ∎  where
            open ≡-Reasoning
            lt : {x z : ℕ } →  x * z ≤ z + x * z
            lt {zero} {zero} = z≤n
            lt {suc x} {zero} = lt {x} {zero}
            lt {x} {suc z} = ≤-trans lemma refl-≤s where
               lemma : x * suc z ≤   z + x * suc z
               lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z})
distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin
           minus x (suc y) * z + suc y * z
        ≡⟨ sym (proj₂ *-distrib-+ z  (minus x (suc y) )  _) ⟩
           ( minus x (suc y) + suc y ) * z
        ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c))  ⟩
           x * z
        ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩
           minus (x * z) (suc y * z) + suc y * z
        ∎ ) where
            open ≡-Reasoning
            lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z
            lt {x} {y} {z} le = *≤ le

distr-minus-*' : {z x y : ℕ } → z * (minus x y)  ≡ minus (z * x) (z * y)
distr-minus-*' {z} {x} {y} = begin
        z * (minus x y) ≡⟨ *-comm _ (x - y) ⟩
        (minus x y) * z ≡⟨ distr-minus-* {x} {y} {z} ⟩
        minus (x * z) (y * z) ≡⟨ cong₂ (λ j k → j - k ) (*-comm x z ) (*-comm y z) ⟩
        minus (z * x) (z * y) ∎  where open ≡-Reasoning

minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z)
minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin
           minus (minus x y) z + z
        ≡⟨ minus+n {_} {z} lemma ⟩
           minus x y
        ≡⟨ +m= {_} {_} {y} ( begin
              minus x y + y
           ≡⟨ minus+n {_} {y} lemma1 ⟩
              x
           ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩
              minus x (z + y) + (z + y)
           ≡⟨ sym ( +-assoc (minus x (z + y)) _  _ ) ⟩
              minus x (z + y) + z + y
           ∎ ) ⟩
           minus x (z + y) + z
        ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y )  ⟩
           minus x (y + z) + z
        ∎  ) where
             open ≡-Reasoning
             lemma1 : suc x > y
             lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt )
             lemma : suc (minus x y) > z
             lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y}  lemma1 ))  gt )

minus-* : {M k n : ℕ } → n < k  → minus k (suc n) * M ≡ minus (minus k n * M ) M
minus-* {zero} {k} {n} lt = begin
           minus k (suc n) * zero
        ≡⟨ *-comm (minus k (suc n)) zero ⟩
           zero * minus k (suc n)
        ≡⟨⟩
           0 * minus k n
        ≡⟨ *-comm 0 (minus k n) ⟩
           minus (minus k n * 0 ) 0
        ∎  where
        open ≡-Reasoning
minus-* {suc m} {k} {n} lt with <-cmp k 1
minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl
minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl
minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl
minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt
minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c
minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin
           minus k (suc n) * M
        ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
           minus (k * M ) ((suc n) * M)
        ≡⟨⟩
           minus (k * M ) (M + n * M  )
        ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩
           minus (k * M ) ((n * M) + M )
        ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩
           minus (minus (k * M ) (n * M)) M
        ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
           minus (minus k n * M ) M
        ∎  where
             M = suc m
             lemma : {n k m : ℕ } → n < k  → suc (k * suc m) > suc m + n * suc m
             lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
             lemma {suc n} {suc k} {m} lt = begin
                         suc (suc m + suc n * suc m)
                      ≡⟨⟩
                         suc ( suc (suc n) * suc m)
                      ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
                         suc (suc k * suc m)
                      ∎   where open ≤-Reasoning
             open ≡-Reasoning

x=y+z→x-z=y : {x y z : ℕ } → x ≡ y + z → x - z ≡ y
x=y+z→x-z=y {x} {zero} {.x} refl = minus<=0 {x} {x} refl-≤ -- x ≡ suc (y + z) → (x ≡ y + z → x - z ≡ y)   → (x - z) ≡ suc y
x=y+z→x-z=y {suc x} {suc y} {zero} eq = begin -- suc x ≡ suc (y + zero) → (suc x - zero) ≡ suc y
       suc x - zero ≡⟨ refl ⟩
       suc x  ≡⟨ eq ⟩
       suc y + zero ≡⟨ +-comm _ zero ⟩
       suc y ∎  where open ≡-Reasoning
x=y+z→x-z=y {suc x} {suc y} {suc z} eq = x=y+z→x-z=y {x} {suc y} {z} ( begin
       x ≡⟨ cong pred eq ⟩
       pred (suc y + suc z) ≡⟨ +-comm _ (suc z)  ⟩
       suc z + y ≡⟨ cong suc ( +-comm _ y ) ⟩
       suc y + z ∎  ) where open ≡-Reasoning

m*1=m : {m : ℕ } → m * 1 ≡ m
m*1=m {zero} = refl
m*1=m {suc m} = cong suc m*1=m

record Finduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set  (n Level.⊔ m) where
  field
    fzero   : {p : P} → f p ≡ zero → Q p
    pnext : (p : P ) → P
    decline : {p : P} → 0 < f p  → f (pnext p) < f p
    ind : {p : P} → Q (pnext p) → Q p

y<sx→y≤x : {x y : ℕ} → y < suc x → y ≤ x
y<sx→y≤x (s≤s lt) = lt

fi0 : (x : ℕ) → x ≤ zero → x ≡ zero
fi0 .0 z≤n = refl

f-induction : {n m : Level} {P : Set n } → {Q : P → Set m }
  → (f : P → ℕ)
  → Finduction P Q f
  → (p : P ) → Q p
f-induction {n} {m} {P} {Q} f I p with <-cmp 0 (f p)
... | tri> ¬a ¬b ()
... | tri≈ ¬a b ¬c = Finduction.fzero I (sym b)
... | tri< lt _ _ = f-induction0 p (f p) (<to≤ (Finduction.decline I lt)) where
   f-induction0 : (p : P) → (x : ℕ) → (f (Finduction.pnext I p)) ≤ x → Q p
   f-induction0 p zero le = Finduction.ind I (Finduction.fzero I (fi0 _ le))
   f-induction0 p (suc x) le with <-cmp (f (Finduction.pnext I p)) (suc x)
   ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a
   ... | tri≈ ¬a b ¬c = Finduction.ind I (f-induction0 (Finduction.pnext I p) x (y<sx→y≤x f1)) where
       f1 : f (Finduction.pnext I (Finduction.pnext I p)) < suc x
       f1 = subst (λ k → f (Finduction.pnext I (Finduction.pnext I p)) < k ) b ( Finduction.decline I {Finduction.pnext I p}
         (subst (λ k → 0 < k ) (sym b) (s≤s z≤n ) ))
   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c )

record Ninduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set  (n Level.⊔ m) where
  field
    pnext : (p : P ) → P
    fzero   : {p : P} → f (pnext p) ≡ zero → Q p
    decline : {p : P} → 0 < f p  → f (pnext p) < f p
    ind : {p : P} → Q (pnext p) → Q p

s≤s→≤ : { i j : ℕ} → suc i ≤ suc j → i ≤ j
s≤s→≤ (s≤s lt) = lt

n-induction : {n m : Level} {P : Set n } → {Q : P → Set m }
  → (f : P → ℕ)
  → Ninduction P Q f
  → (p : P ) → Q p
n-induction {n} {m} {P} {Q} f I p  = f-induction0 p (f (Ninduction.pnext I p)) ≤-refl where
   f-induction0 : (p : P) → (x : ℕ) → (f (Ninduction.pnext I p)) ≤ x  →  Q p
   f-induction0 p zero lt = Ninduction.fzero I {p} (fi0 _ lt)
   f-induction0 p (suc x) le with <-cmp (f (Ninduction.pnext I p)) (suc x)
   ... | tri< (s≤s a)  ¬b ¬c = f-induction0 p x a
   ... | tri≈ ¬a b ¬c = Ninduction.ind I (f-induction0 (Ninduction.pnext I p) x (s≤s→≤ nle) ) where
      f>0 :  0 < f (Ninduction.pnext I p)
      f>0 = subst (λ k → 0 < k ) (sym b) ( s≤s z≤n )
      nle : suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ suc x
      nle = subst (λ k → suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ k) b (Ninduction.decline I {Ninduction.pnext I p} f>0 )
   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c )

record Factor (n m : ℕ ) : Set where
   field
      factor : ℕ
      remain : ℕ
      is-factor : factor * n + remain ≡ m

record Dividable (n m : ℕ ) : Set where
   field
      factor : ℕ
      is-factor : factor * n + 0 ≡ m

open Factor

DtoF : {n m : ℕ} → Dividable n m → Factor n m
DtoF {n} {m} record { factor = f ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa }

FtoD : {n m : ℕ} → (fc : Factor n m) → remain fc ≡ 0 → Dividable n m
FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } refl = record { factor = f ; is-factor = fa }

--divdable^2 : ( n k : ℕ ) → Dividable k ( n * n ) → Dividable k n
--divdable^2 n k dn2 = {!!}

decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } =
 decf1 {n} {k} f r fa where
  decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n)  → Factor k n
  decf1 {n} {k} f (suc r) fa  =  -- this case must be the first
     record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n
        f * k + r ≡⟨ cong pred ( begin
          suc ( f * k + r ) ≡⟨ +-comm _ r ⟩
          r + suc (f * k)  ≡⟨ sym (+-assoc r 1 _) ⟩
          (r + 1) + f * k ≡⟨ cong (λ t → t + f * k ) (+-comm r 1) ⟩
          (suc r ) + f * k ≡⟨ +-comm (suc r) _ ⟩
          f * k + suc r  ≡⟨ fa ⟩
          suc n ∎ ) ⟩
        n ∎ ) }  where open ≡-Reasoning
  decf1 {n} {zero} (suc f) zero fa  = ⊥-elim ( nat-≡< fa (
        begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero)  ⟩
        suc (f * 0) ≡⟨ cong suc (*-comm f zero)  ⟩
        suc zero ≤⟨ s≤s z≤n ⟩
        suc n ∎ )) where open ≤-Reasoning
  decf1 {n} {suc k} (suc f) zero fa  =
     record { factor = f ; remain = k ; is-factor = ( begin -- fa : suc (k + f * suc k + zero) ≡ suc n
        f * suc k + k ≡⟨ +-comm _ k ⟩
        k + f * suc k ≡⟨ +-comm zero _ ⟩
        (k + f * suc k) + zero  ≡⟨ cong pred fa ⟩
        n ∎ ) }  where open ≡-Reasoning

div0 :  {k : ℕ} → Dividable k 0
div0 {k} = record { factor = 0; is-factor = refl }

div= :  {k : ℕ} → Dividable k k
div= {k} = record { factor = 1; is-factor = ( begin
        k + 0 * k + 0  ≡⟨ trans ( +-comm _ 0) ( +-comm _ 0) ⟩
        k ∎ ) }  where open ≡-Reasoning

div1 : { k : ℕ } → k > 1 →  ¬  Dividable k 1
div1 {k} k>1 record { factor = (suc f) ; is-factor = fa } = ⊥-elim ( nat-≡< (sym fa) ( begin
    2 ≤⟨ k>1 ⟩
    k ≡⟨ +-comm 0 _ ⟩
    k + 0 ≡⟨ refl  ⟩
    1 * k ≤⟨ *-mono-≤ {1} {suc f} (s≤s z≤n ) ≤-refl ⟩
    suc f * k ≡⟨ +-comm 0 _ ⟩
    suc f * k + 0 ∎  )) where open ≤-Reasoning

div+div : { i j k : ℕ } →  Dividable k i →  Dividable k j → Dividable k (i + j) ∧ Dividable k (j + i)
div+div {i} {j} {k} di dj = ⟪ div+div1 , subst (λ g → Dividable k g) (+-comm i j) div+div1 ⟫ where
      fki = Dividable.factor di
      fkj = Dividable.factor dj
      div+div1 : Dividable k (i + j)
      div+div1 = record { factor = fki + fkj  ; is-factor = ( begin
          (fki + fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩
          (fki + fkj) * k  ≡⟨ *-distribʳ-+ k fki _ ⟩
          fki * k + fkj * k  ≡⟨ cong₂ ( λ i j → i + j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩
          (fki * k + 0) + (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i + j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩
          i + j  ∎ ) } where
             open ≡-Reasoning

div-div : { i j k : ℕ } → k > 1 →  Dividable k i →  Dividable k j → Dividable k (i - j) ∧ Dividable k (j - i)
div-div {i} {j} {k} k>1 di dj = ⟪ div-div1 di dj , div-div1 dj di ⟫ where
      div-div1 : {i j : ℕ } → Dividable k i →  Dividable k j → Dividable k (i - j)
      div-div1 {i} {j} di dj = record { factor = fki - fkj  ; is-factor = ( begin
          (fki - fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩
          (fki - fkj) * k  ≡⟨ distr-minus-* {fki} {fkj}  ⟩
          (fki * k) - (fkj * k)  ≡⟨ cong₂ ( λ i j → i - j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩
          (fki * k + 0) - (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i - j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩
          i - j  ∎ ) } where
             open ≡-Reasoning
             fki = Dividable.factor di
             fkj = Dividable.factor dj

open _∧_

div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)
div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where
   div+11 : Dividable k 1
   div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1  ) )

div<k : { m k : ℕ } → k > 1 → m > 0 →  m < k →  ¬ Dividable k m
div<k {m} {k} k>1 m>0 m<k d = ⊥-elim ( nat-≤> (div<k1 (Dividable.factor d) (Dividable.is-factor d)) m<k ) where
    div<k1 : (f : ℕ ) → f * k + 0 ≡ m → k ≤ m
    div<k1 zero eq = ⊥-elim (nat-≡< eq m>0 )
    div<k1 (suc f) eq = begin
          k ≤⟨ x≤x+y ⟩
          k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩
          k + f * k + 0 ≡⟨ eq ⟩
          m ∎  where open ≤-Reasoning

div→k≤m : { m k : ℕ } → k > 1 → m > 0 →  Dividable k m → m ≥ k
div→k≤m {m} {k} k>1 m>0 d with <-cmp m k
... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 m>0 a d )
... | tri≈ ¬a refl ¬c = ≤-refl
... | tri> ¬a ¬b c = <to≤ c

div1*k+0=k : {k : ℕ } → 1 * k + 0 ≡ k
div1*k+0=k {k} =  begin
   1 * k + 0 ≡⟨ cong (λ g → g + 0) (+-comm _ 0) ⟩
   k + 0 ≡⟨ +-comm _ 0 ⟩
   k  ∎ where open ≡-Reasoning

decD : {k m : ℕ} → k > 1 → Dec (Dividable k m )
decD {k} {m} k>1 = n-induction {_} {_} {ℕ} {λ m → Dec (Dividable k m ) } F I m where
        F : ℕ → ℕ
        F m = m
        F0 : ( m : ℕ ) → F (m - k) ≡ 0 →  Dec  (Dividable k m  )
        F0 0 eq = yes record { factor = 0 ; is-factor = refl }
        F0 (suc m) eq with <-cmp k (suc m)
        ... | tri< a ¬b ¬c = yes  record { factor = 1 ; is-factor =
            subst (λ g → 1 * k + 0 ≡ g ) (sym (i-j=0→i=j (<to≤ a) eq )) div1*k+0=k }  -- (suc m - k) ≡ 0 → k ≡ suc m, k ≤ suc m
        ... | tri≈ ¬a refl ¬c =  yes   record { factor = 1 ; is-factor = div1*k+0=k }
        ... | tri> ¬a ¬b c = no ( λ d →  ⊥-elim (div<k k>1 (s≤s z≤n ) c d) )
        decl : {m  : ℕ } → 0 < m → m - k < m
        decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m
        ind : (p : ℕ ) → Dec (Dividable k (p - k) ) → Dec (Dividable k p )
        ind p (yes y) with <-cmp p k
        ... | tri≈ ¬a refl ¬c = yes (subst (λ g → Dividable k g) (minus+n ≤-refl ) (proj1 ( div+div y div= )))
        ... | tri> ¬a ¬b k<p  = yes (subst (λ g → Dividable k g) (minus+n (<-trans k<p a<sa)) (proj1 ( div+div y div= )))
        ... | tri< a ¬b ¬c with <-cmp p 0
        ... | tri≈ ¬a refl ¬c₁ = yes div0
        ... | tri> ¬a ¬b₁ c = no (λ d → not-div p (Dividable.factor d) a c (Dividable.is-factor d) ) where
            not-div : (p f : ℕ) → p < k  → 0 < p → f * k + 0 ≡ p → ⊥
            not-div (suc p) (suc f) p<k 0<p eq = nat-≡< (sym eq) ( begin -- ≤-trans p<k {!!}) -- suc p ≤ k
              suc (suc p) ≤⟨ p<k ⟩
              k ≤⟨ x≤x+y  ⟩
              k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩
              suc f * k + 0 ∎  ) where open ≤-Reasoning
        ind p (no n) = no (λ d → n (proj1 (div-div k>1 d div=))  )
        I : Ninduction ℕ  _  F
        I = record {
              pnext = λ p → p - k
            ; fzero = λ {m} eq → F0 m eq
            ; decline = λ {m} lt → decl lt
            ; ind = λ {p} prev → ind p prev
          }

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


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

module Cubical.Data.Fin.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Embedding
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence

open import Cubical.Data.Fin.Base
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty
open import Cubical.Data.Sum
open import Cubical.Data.Sigma

open import Cubical.Induction.WellFounded

private
  -- Σ is more convenient than the inductive ×, but I don't
  -- want to have to write λ_→ all over.
  _×_ : Type₀ → Type₀ → Type₀
  A × B = Σ A λ _ → B

-- Fin 0 is empty, and thus a proposition.
Fin0-isProp : isProp (Fin 0)
Fin0-isProp = ⊥-elim ∘ ¬Fin0

-- Fin 1 has only one value.
Fin1-isContr : isContr (Fin 1)
Fin1-isContr
  = fzero , λ
  { (zero , _) → toℕ-injective refl
  ; (suc k , sk<1) → ⊥-elim (¬-<-zero (pred-≤-pred sk<1))
  }

-- Regardless of k, Fin k is a set.
isSetFin : ∀{k} → isSet (Fin k)
isSetFin {k} = isOfHLevelΣ 2 isSetℕ (λ _ → isProp→isSet m≤n-isProp)

-- Helper function for the reduction procedure below.
--
-- If n = expand o k m, then n is congruent to m modulo k.
expand : ℕ → ℕ → ℕ → ℕ
expand 0 k m = m
expand (suc o) k m = k + expand o k m

expand≡ : ∀ k m o → expand o k m ≡ o * k + m
expand≡ k m zero = refl
expand≡ k m (suc o)
  = cong (k +_) (expand≡ k m o) ∙ +-assoc k (o * k) m

-- Expand a pair. This is useful because the whole function is
-- injective.
expand× : ∀{k} → (Fin k × ℕ) → ℕ
expand× {k} (f , o) = expand o k (toℕ f)

private
  lemma₀ : ∀{k m n r} → r ≡ n → k + m ≡ n → k ≤ r
  lemma₀ {k = k} {m} p q = m , +-comm m k ∙ q ∙ sym p

  expand×Inj : ∀ k → {t1 t2 : Fin (suc k) × ℕ} → expand× t1 ≡ expand× t2 → t1 ≡ t2
  expand×Inj k {f1 , zero} {f2 , zero} p i
    = toℕ-injective {fj = f1} {f2} p i , zero
  expand×Inj k {f1 , suc o1} {(r , r<sk) , zero} p
    = ⊥-elim (<-asym r<sk (lemma₀ refl p))
  expand×Inj k {(r , r<sk) , zero} {f2 , suc o2} p
    = ⊥-elim (<-asym r<sk (lemma₀ refl (sym p)))
  expand×Inj k {f1 , suc o1} {f2 , suc o2}
    = cong (λ { (f , o) → (f , suc o) })
    ∘ expand×Inj k {f1 , o1} {f2 , o2}
    ∘ inj-m+ {suc k}

  expand×Emb : ∀ k → isEmbedding (expand× {k})
  expand×Emb 0 = ⊥-elim ∘ ¬Fin0 ∘ fst
  expand×Emb (suc k)
    = injEmbedding (isOfHLevelΣ 2 isSetFin (λ _ → isSetℕ)) isSetℕ (expand×Inj k)

-- A Residue is a family of types representing evidence that a
-- natural is congruent to a value of a finite type.
Residue : ℕ → ℕ → Type₀
Residue k n = Σ[ tup ∈ Fin k × ℕ ] expand× tup ≡ n

extract : ∀{k n} → Residue k n → Fin k
extract = fst ∘ fst

-- There is at most one canonical finite value congruent to each
-- natural.
isPropResidue : ∀ k n → isProp (Residue k n)
isPropResidue k = isEmbedding→hasPropFibers (expand×Emb k)

-- A value of a finite type is its own residue.
Fin→Residue : ∀{k} → (f : Fin k) → Residue k (toℕ f)
Fin→Residue f = (f , 0) , refl

-- Fibers of numbers that differ by k are equivalent in a more obvious
-- way than via the fact that they are propositions.
Residue+k : (k n : ℕ) → Residue k n → Residue k (k + n)
Residue+k k n ((f , o) , p) = (f , suc o) , cong (k +_) p

Residue-k : (k n : ℕ) → Residue k (k + n) → Residue k n
Residue-k k n (((r , r<k) , zero) , p) = ⊥-elim (<-asym r<k (lemma₀ p refl))
Residue-k k n ((f , suc o) , p) = ((f , o) , inj-m+ p)

Residue+k-k
  : (k n : ℕ)
  → (R : Residue k (k + n))
  → Residue+k k n (Residue-k k n R) ≡ R
Residue+k-k k n (((r , r<k) , zero) , p) = ⊥-elim (<-asym r<k (lemma₀ p refl))
Residue+k-k k n ((f , suc o) , p)
  = ΣProp≡ (λ tup → isSetℕ (expand× tup) (k + n)) refl

Residue-k+k
  : (k n : ℕ)
  → (R : Residue k n)
  → Residue-k k n (Residue+k k n R) ≡ R
Residue-k+k k n ((f , o) , p)
  = ΣProp≡ (λ tup → isSetℕ (expand× tup) n) refl

private
  Residue≃ : ∀ k n → Residue k n ≃ Residue k (k + n)
  Residue≃ k n
    = Residue+k k n
    , isoToIsEquiv (iso (Residue+k k n) (Residue-k k n)
                        (Residue+k-k k n) (Residue-k+k k n))

Residue≡ : ∀ k n → Residue k n ≡ Residue k (k + n)
Residue≡ k n = ua (Residue≃ k n)

-- For positive `k`, all `n` have a canonical residue mod `k`.
module Reduce (k₀ : ℕ) where
  k : ℕ
  k = suc k₀

  base : ∀ n (n<k : n < k) → Residue k n
  base n n<k = Fin→Residue (n , n<k)

  step : ∀ n → Residue k n → Residue k (k + n)
  step n = transport (Residue≡ k n)

  reduce : ∀ n → Residue k n
  reduce = +induction k₀ (Residue k) base step

  reduce≡
    : ∀ n → transport (Residue≡ k n) (reduce n) ≡ reduce (k + n)
  reduce≡ n
    = sym (+inductionStep k₀ _ base step n)

  reduceP
    : ∀ n → PathP (λ i → Residue≡ k n i) (reduce n) (reduce (k + n))
  reduceP n = toPathP (reduce≡ n)

open Reduce using (reduce; reduce≡) public

private
  lemma₅
    : ∀ k n (R : Residue k n)
    →  extract R ≡ extract (transport (Residue≡ k n) R)
  lemma₅ k n = sym ∘ cong extract ∘ uaβ (Residue≃ k n)

-- The residue of n modulo k is the same as the residue of k + n.
extract≡ : ∀ k n → extract (reduce k n) ≡ extract (reduce k (suc k + n))
extract≡ k n
  = lemma₅ (suc k) n (reduce k n) ∙ cong extract (Reduce.reduce≡ k n)

isContrResidue : ∀{k n} → isContr (Residue (suc k) n)
isContrResidue {k} {n} = inhProp→isContr (reduce k n) (isPropResidue (suc k) n)

ext: agda

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
-- Displayed SIP
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Foundations.SIP
open import Cubical.Data.Sigma

open import Cubical.Relation.Binary

private
  variable
    ℓ ℓ' ℓ'' ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓA ℓ≅A ℓB ℓ≅B ℓC ℓ≅C ℓ≅ᴰ : Level

-- a univalent reflexive graph structure on a type
record URGStr (A : Type ℓA) (ℓ≅A : Level) : Type (ℓ-max ℓA (ℓ-suc ℓ≅A)) where
  no-eta-equality
  constructor urgstr
  field
    _≅_ : Rel A A ℓ≅A
    ρ : isRefl _≅_
    uni : isUnivalent _≅_ ρ

-- another constructor for URGStr that uses that if the
-- relational singleton is contractible, the relation is univalent
make-𝒮 : {A : Type ℓA} {_≅_ : Rel A A ℓ≅A}
         (ρ : isRefl _≅_) (contrTotal : contrRelSingl _≅_)
         → URGStr A ℓ≅A
make-𝒮 {_≅_ = _≅_} _ _ .URGStr._≅_ = _≅_
make-𝒮 ρ _ .URGStr.ρ = ρ
make-𝒮 {_≅_ = _≅_} ρ contrTotal .URGStr.uni = contrRelSingl→isUnivalent _≅_ ρ contrTotal

module _ where
  open URGStr
  η-URGStr : {A : Type ℓA} {ℓ≅A : Level}
             (𝒮-A : URGStr A ℓ≅A) → urgstr (_≅_ 𝒮-A) (ρ 𝒮-A) (uni 𝒮-A) ≡ 𝒮-A
  _≅_ (η-URGStr 𝒮-A i) = _≅_ 𝒮-A
  ρ (η-URGStr 𝒮-A i) = ρ 𝒮-A
  uni (η-URGStr 𝒮-A i) = uni 𝒮-A

-- a displayed univalent reflexive graph structure over a URGStr on a type
record URGStrᴰ {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
               (B : A → Type ℓB) (ℓ≅ᴰ : Level) : Type (ℓ-max (ℓ-max (ℓ-max ℓA ℓB) ℓ≅A) (ℓ-suc ℓ≅ᴰ)) where
  no-eta-equality
  constructor urgstrᴰ
  open URGStr 𝒮-A

  field
    _≅ᴰ⟨_⟩_ : {a a' : A} → B a → a ≅ a' → B a' → Type ℓ≅ᴰ
    ρᴰ : {a : A} → isRefl _≅ᴰ⟨ ρ a ⟩_
    uniᴰ : {a : A} → isUnivalent _≅ᴰ⟨ ρ a ⟩_ ρᴰ

open URGStrᴰ

-- another constructor for URGStrᴰ, using contractability of relational singletons
-- rather than univalence
make-𝒮ᴰ : {A : Type ℓA} {𝒮-A : URGStr A ℓ≅A}
          {B : A → Type ℓB}
          (_≅ᴰ⟨_⟩_ : {a a' : A} → B a → URGStr._≅_ 𝒮-A a a' → B a' → Type ℓ≅ᴰ)
          (ρᴰ : {a : A} → isRefl _≅ᴰ⟨ URGStr.ρ 𝒮-A a ⟩_)
          (contrTotal : (a : A) → contrRelSingl _≅ᴰ⟨ URGStr.ρ 𝒮-A a ⟩_)
          → URGStrᴰ 𝒮-A B ℓ≅ᴰ
make-𝒮ᴰ {A = A} {𝒮-A = 𝒮-A} _≅ᴰ⟨_⟩_ ρᴰ contrTotal ._≅ᴰ⟨_⟩_ = _≅ᴰ⟨_⟩_
make-𝒮ᴰ {A = A} {𝒮-A = 𝒮-A} _≅ᴰ⟨_⟩_ ρᴰ contrTotal .ρᴰ = ρᴰ
make-𝒮ᴰ {A = A} {𝒮-A = 𝒮-A} _≅ᴰ⟨_⟩_ ρᴰ contrTotal .uniᴰ {a} b b' = contrRelSingl→isUnivalent (_≅ᴰ⟨ URGStr.ρ 𝒮-A a ⟩_) (ρᴰ {a}) (contrTotal a) b b'

-- abbreviation to obtain contractibility of total space
𝒮→cTS : {A : Type ℓA} (StrA : URGStr A ℓ≅A) → contrRelSingl (URGStr._≅_ StrA)
𝒮→cTS StrA = isUnivalent→contrRelSingl _≅_ ρ uni
  where open URGStr StrA

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------
-- Convenient syntax for "equational reasoning" using a strict partial
-- order
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.StrictPartialOrderReasoning
         (p : StrictPartialOrder) where

import Relation.Binary.PreorderReasoning as PreR
import Relation.Binary.Props.StrictPartialOrder as SPO
open PreR (SPO.preorder p) public renaming (_∼⟨_⟩_ to _<⟨_⟩_)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Andreas, 2013-05-16, raised by Andrea 2015-02-10

open import Common.Size
open import Common.Prelude

data Wrap (A : SizeUniv) : SizeUniv where
-- data Wrap (A : Set) : Set where
  wrap : A → Wrap A

module M (f : ∀ i → Wrap (Size< i)) where

  test : ∀ i → Wrap (Size< i) → ⊥
  test i (wrap j) = test j (f j)

module N (pred : ∀ i → Size< i) where

  f = (λ i → wrap (pred i))
  open M f

  loop : Size → ⊥
  loop i = test i (f i)
  -- = test i (wrap (pred i))
  -- = test (pred i) ((λ i → wrap (pred i)) (pred i))
  -- = test (pred i) (wrap (pred (pred i)))
  -- = test (pred (pred i)) (wrap (pred (pred (pred i))))
  -- = ...

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
module NTypes.Universe where

open import Equivalence
open import NTypes
open import PathOperations
open import PathStructure.Coproduct
open import Types
open import Univalence

Bool : Set
Bool = ⊤ ⊎ ⊤

not : Bool → Bool
not = case (λ _ → Bool) (λ _ → inr _) (λ _ → inl _)

not-not : ∀ x → not (not x) ≡ x
not-not = case
  (λ x → not (not x) ≡ x)
  (λ _ → refl) (λ _ → refl)

Bool-eq₁ : Bool ≃ Bool
Bool-eq₁ = ≡→eq refl

Bool-eq₂ : Bool ≃ Bool
Bool-eq₂
  = not
  , (not , not-not)
  , (not , not-not)

nope : Bool-eq₁ ≡ Bool-eq₂ → ⊥
nope x = lower (split-path (happly (ap π₁ x) (inl _)))

-- With Lift, we could prove stronger statement
-- (∀ ℓ → isSet (Set ℓ) → ⊥), but the idea is same - pick
-- something equivalent to Bool in Set ℓ, find two different
-- ways in which this type is equivalent and derive
-- a contradiction.
¬U-set : (∀ ℓ → isSet (Set ℓ)) → ⊥
¬U-set U-set = nope
  ( from-to-eq _ ⁻¹
  · ap from-≡
    (U-set _ Bool Bool (to-≡ Bool-eq₁) (to-≡ Bool-eq₂))
  · from-to-eq _
  )
  where
  from-≡     =         π₁ (ua {A = Bool} {B = Bool})
  to-≡       = π₁ (π₁ (π₂ (ua {A = Bool} {B = Bool})))
  from-to-eq = π₂ (π₁ (π₂ (ua {A = Bool} {B = Bool})))

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
-- Basic intuitionistic propositional calculus, without ∨ or ⊥.
-- Translation between different formalisations of syntax.

module BasicIPC.Syntax.Translation where

open import BasicIPC.Syntax.Common public

import BasicIPC.Syntax.ClosedHilbertSequential as CHS
import BasicIPC.Syntax.ClosedHilbert as CH
import BasicIPC.Syntax.HilbertSequential as HS
import BasicIPC.Syntax.Hilbert as H
import BasicIPC.Syntax.Gentzen as G

open HS using () renaming (_⊦⊢_ to HS⟨_⊦⊢_⟩ ; _⊢_ to HS⟨_⊢_⟩) public
open H using () renaming (_⊢_ to H⟨_⊢_⟩) public
open G using () renaming (_⊢_ to G⟨_⊢_⟩) public

-- Available translations.
--
--       ┌─────┬─────┬─────┬─────┬─────┐
--       │ CHS │ CH  │ HS  │ H   │ G   │
-- ┌─────┼─────┼─────┼─────┼─────┼─────┤
-- │ CHS │     │ d   │ d   │ ∘   │ ∘   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ CH  │ d   │     │ ∘   │ d   │ ∘   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ HS  │ d   │ ∘   │     │ d   │ ∘   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ H   │ ∘   │ d   │ d   │     │ d   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ G   │ ∘   │ ∘   │ ∘   │ d   │     │
-- └─────┴─────┴─────┴─────┴─────┴─────┘
--
-- d : Direct translation.
-- ∘ : Composition of translations.

-- Translation from closed Hilbert-style sequential to closed Hilbert-style.

chs→ch : ∀ {A} → CHS.⊢ A → CH.⊢ A
chs→ch (Ξ , ts) = chs⊦→ch ts top
  where
    chs⊦→ch : ∀ {A Ξ} → CHS.⊦⊢ Ξ → A ∈ Ξ → CH.⊢ A
    chs⊦→ch (CHS.mp i j ts) top     = CH.app (chs⊦→ch ts i) (chs⊦→ch ts j)
    chs⊦→ch (CHS.ci ts)     top     = CH.ci
    chs⊦→ch (CHS.ck ts)     top     = CH.ck
    chs⊦→ch (CHS.cs ts)     top     = CH.cs
    chs⊦→ch (CHS.cpair ts)  top     = CH.cpair
    chs⊦→ch (CHS.cfst ts)   top     = CH.cfst
    chs⊦→ch (CHS.csnd ts)   top     = CH.csnd
    chs⊦→ch (CHS.unit ts)   top     = CH.unit
    chs⊦→ch (CHS.mp i j ts) (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.ci ts)     (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.ck ts)     (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.cs ts)     (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.cpair ts)  (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.cfst ts)   (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.csnd ts)   (pop k) = chs⊦→ch ts k
    chs⊦→ch (CHS.unit ts)   (pop k) = chs⊦→ch ts k

-- Translation from closed Hilbert-style to closed Hilbert-style sequential.

ch→chs : ∀ {A} → CH.⊢ A → CHS.⊢ A
ch→chs (CH.app t u) = CHS.app (ch→chs t) (ch→chs u)
ch→chs CH.ci        = ∅ , CHS.ci CHS.nil
ch→chs CH.ck        = ∅ , CHS.ck CHS.nil
ch→chs CH.cs        = ∅ , CHS.cs CHS.nil
ch→chs CH.cpair     = ∅ , CHS.cpair CHS.nil
ch→chs CH.cfst      = ∅ , CHS.cfst CHS.nil
ch→chs CH.csnd      = ∅ , CHS.csnd CHS.nil
ch→chs CH.unit      = ∅ , CHS.unit CHS.nil

-- Translation from Hilbert-style sequential to Hilbert-style.

hs→h : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → H⟨ Γ ⊢ A ⟩
hs→h (Ξ , ts) = hs⊦→h ts top
  where
    hs⊦→h : ∀ {A Ξ Γ} → HS⟨ Γ ⊦⊢ Ξ ⟩ → A ∈ Ξ → H⟨ Γ ⊢ A ⟩
    hs⊦→h (HS.var i ts)  top     = H.var i
    hs⊦→h (HS.mp i j ts) top     = H.app (hs⊦→h ts i) (hs⊦→h ts j)
    hs⊦→h (HS.ci ts)     top     = H.ci
    hs⊦→h (HS.ck ts)     top     = H.ck
    hs⊦→h (HS.cs ts)     top     = H.cs
    hs⊦→h (HS.cpair ts)  top     = H.cpair
    hs⊦→h (HS.cfst ts)   top     = H.cfst
    hs⊦→h (HS.csnd ts)   top     = H.csnd
    hs⊦→h (HS.unit ts)   top     = H.unit
    hs⊦→h (HS.var i ts)  (pop k) = hs⊦→h ts k
    hs⊦→h (HS.mp i j ts) (pop k) = hs⊦→h ts k
    hs⊦→h (HS.ci ts)     (pop k) = hs⊦→h ts k
    hs⊦→h (HS.ck ts)     (pop k) = hs⊦→h ts k
    hs⊦→h (HS.cs ts)     (pop k) = hs⊦→h ts k
    hs⊦→h (HS.cpair ts)  (pop k) = hs⊦→h ts k
    hs⊦→h (HS.cfst ts)   (pop k) = hs⊦→h ts k
    hs⊦→h (HS.csnd ts)   (pop k) = hs⊦→h ts k
    hs⊦→h (HS.unit ts)   (pop k) = hs⊦→h ts k

-- Translation from Hilbert-style to Hilbert-style sequential.

h→hs : ∀ {A Γ} → H⟨ Γ ⊢ A ⟩ → HS⟨ Γ ⊢ A ⟩
h→hs (H.var i)   = ∅ , HS.var i HS.nil
h→hs (H.app t u) = HS.app (h→hs t) (h→hs u)
h→hs H.ci        = ∅ , HS.ci HS.nil
h→hs H.ck        = ∅ , HS.ck HS.nil
h→hs H.cs        = ∅ , HS.cs HS.nil
h→hs H.cpair     = ∅ , HS.cpair HS.nil
h→hs H.cfst      = ∅ , HS.cfst HS.nil
h→hs H.csnd      = ∅ , HS.csnd HS.nil
h→hs H.unit      = ∅ , HS.unit HS.nil

-- Deduction and detachment theorems for Hilbert-style sequential.

hs-lam : ∀ {A B Γ} → HS⟨ Γ , A ⊢ B ⟩ → HS⟨ Γ ⊢ A ▻ B ⟩
hs-lam = h→hs ∘ H.lam ∘ hs→h

hs-lam⋆₀ : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → HS⟨ ∅ ⊢ Γ ▻⋯▻ A ⟩
hs-lam⋆₀ = h→hs ∘ H.lam⋆₀ ∘ hs→h

hs-det : ∀ {A B Γ} → HS⟨ Γ ⊢ A ▻ B ⟩ → HS⟨ Γ , A ⊢ B ⟩
hs-det = h→hs ∘ H.det ∘ hs→h

hs-det⋆₀ : ∀ {A Γ} → HS⟨ ∅ ⊢ Γ ▻⋯▻ A ⟩ → HS⟨ Γ ⊢ A ⟩
hs-det⋆₀ = h→hs ∘ H.det⋆₀ ∘ hs→h

-- Translation from closed Hilbert-style sequential to Hilbert-style sequential.

chs→hs₀ : ∀ {A} → CHS.⊢ A → HS⟨ ∅ ⊢ A ⟩
chs→hs₀ (Ξ , ts) = Ξ , chs⊦→hs₀⊦ ts
  where
    chs⊦→hs₀⊦ : ∀ {Ξ} → CHS.⊦⊢ Ξ → HS⟨ ∅ ⊦⊢ Ξ ⟩
    chs⊦→hs₀⊦ CHS.nil         = HS.nil
    chs⊦→hs₀⊦ (CHS.mp i j ts) = HS.mp i j (chs⊦→hs₀⊦ ts)
    chs⊦→hs₀⊦ (CHS.ci ts)     = HS.ci (chs⊦→hs₀⊦ ts)
    chs⊦→hs₀⊦ (CHS.ck ts)     = HS.ck (chs⊦→hs₀⊦ ts)
    chs⊦→hs₀⊦ (CHS.cs ts)     = HS.cs (chs⊦→hs₀⊦ ts)
    chs⊦→hs₀⊦ (CHS.cpair ts)  = HS.cpair (chs⊦→hs₀⊦ ts)
    chs⊦→hs₀⊦ (CHS.cfst ts)   = HS.cfst (chs⊦→hs₀⊦ ts)
    chs⊦→hs₀⊦ (CHS.csnd ts)   = HS.csnd (chs⊦→hs₀⊦ ts)
    chs⊦→hs₀⊦ (CHS.unit ts)   = HS.unit (chs⊦→hs₀⊦ ts)

chs→hs : ∀ {A Γ} → CHS.⊢ Γ ▻⋯▻ A → HS⟨ Γ ⊢ A ⟩
chs→hs t = hs-det⋆₀ (chs→hs₀ t)

-- Translation from Hilbert-style sequential to closed Hilbert-style sequential.

hs₀→chs : ∀ {A} → HS⟨ ∅ ⊢ A ⟩ → CHS.⊢ A
hs₀→chs (Ξ , ts) = Ξ , hs₀⊦→chs⊦ ts
  where
    hs₀⊦→chs⊦ : ∀ {Ξ} → HS⟨ ∅ ⊦⊢ Ξ ⟩ → CHS.⊦⊢ Ξ
    hs₀⊦→chs⊦ HS.nil         = CHS.nil
    hs₀⊦→chs⊦ (HS.var () ts)
    hs₀⊦→chs⊦ (HS.mp i j ts) = CHS.mp i j (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.ci ts)     = CHS.ci (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.ck ts)     = CHS.ck (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.cs ts)     = CHS.cs (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.cpair ts)  = CHS.cpair (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.cfst ts)   = CHS.cfst (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.csnd ts)   = CHS.csnd (hs₀⊦→chs⊦ ts)
    hs₀⊦→chs⊦ (HS.unit ts)   = CHS.unit (hs₀⊦→chs⊦ ts)

hs→chs : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → CHS.⊢ Γ ▻⋯▻ A
hs→chs t = hs₀→chs (hs-lam⋆₀ t)

-- Translation from closed Hilbert-style to Hilbert-style.

ch→h₀ : ∀ {A} → CH.⊢ A → H⟨ ∅ ⊢ A ⟩
ch→h₀ (CH.app t u) = H.app (ch→h₀ t) (ch→h₀ u)
ch→h₀ CH.ci        = H.ci
ch→h₀ CH.ck        = H.ck
ch→h₀ CH.cs        = H.cs
ch→h₀ CH.cpair     = H.cpair
ch→h₀ CH.cfst      = H.cfst
ch→h₀ CH.csnd      = H.csnd
ch→h₀ CH.unit      = H.unit

ch→h : ∀ {A Γ} → CH.⊢ Γ ▻⋯▻ A → H⟨ Γ ⊢ A ⟩
ch→h t = H.det⋆₀ (ch→h₀ t)

-- Translation from Hilbert-style to closed Hilbert-style.

h₀→ch : ∀ {A} → H⟨ ∅ ⊢ A ⟩ → CH.⊢ A
h₀→ch (H.var ())
h₀→ch (H.app t u) = CH.app (h₀→ch t) (h₀→ch u)
h₀→ch H.ci        = CH.ci
h₀→ch H.ck        = CH.ck
h₀→ch H.cs        = CH.cs
h₀→ch H.cpair     = CH.cpair
h₀→ch H.cfst      = CH.cfst
h₀→ch H.csnd      = CH.csnd
h₀→ch H.unit      = CH.unit

h→ch : ∀ {A Γ} → H⟨ Γ ⊢ A ⟩ → CH.⊢ Γ ▻⋯▻ A
h→ch t = h₀→ch (H.lam⋆₀ t)

-- Translation from Hilbert-style to Gentzen-style.

h→g : ∀ {A Γ} → H⟨ Γ ⊢ A ⟩ → G⟨ Γ ⊢ A ⟩
h→g (H.var i)   = G.var i
h→g (H.app t u) = G.app (h→g t) (h→g u)
h→g H.ci        = G.ci
h→g H.ck        = G.ck
h→g H.cs        = G.cs
h→g H.cpair     = G.cpair
h→g H.cfst      = G.cfst
h→g H.csnd      = G.csnd
h→g H.unit      = G.unit

-- Translation from Gentzen-style to Hilbert-style.

g→h : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → H⟨ Γ ⊢ A ⟩
g→h (G.var i)    = H.var i
g→h (G.lam t)    = H.lam (g→h t)
g→h (G.app t u)  = H.app (g→h t) (g→h u)
g→h (G.pair t u) = H.pair (g→h t) (g→h u)
g→h (G.fst t)    = H.fst (g→h t)
g→h (G.snd t)    = H.snd (g→h t)
g→h G.unit       = H.unit

-- Additional translations from closed Hilbert-style sequential.

chs→h₀ : ∀ {A} → CHS.⊢ A → H⟨ ∅ ⊢ A ⟩
chs→h₀ = ch→h₀ ∘ chs→ch

chs→h : ∀ {A Γ} → CHS.⊢ Γ ▻⋯▻ A → H⟨ Γ ⊢ A ⟩
chs→h = ch→h ∘ chs→ch

chs→g₀ : ∀ {A} → CHS.⊢ A → G⟨ ∅ ⊢ A ⟩
chs→g₀ = h→g ∘ chs→h₀

chs→g : ∀ {A Γ} → CHS.⊢ Γ ▻⋯▻ A → G⟨ Γ ⊢ A ⟩
chs→g = h→g ∘ chs→h

-- Additional translations from closed Hilbert-style.

ch→hs₀ : ∀ {A} → CH.⊢ A → HS⟨ ∅ ⊢ A ⟩
ch→hs₀ = chs→hs₀ ∘ ch→chs

ch→hs : ∀ {A Γ} → CH.⊢ Γ ▻⋯▻ A → HS⟨ Γ ⊢ A ⟩
ch→hs = chs→hs ∘ ch→chs

ch→g₀ : ∀ {A} → CH.⊢ A → G⟨ ∅ ⊢ A ⟩
ch→g₀ = h→g ∘ ch→h₀

ch→g : ∀ {A Γ} → CH.⊢ Γ ▻⋯▻ A → G⟨ Γ ⊢ A ⟩
ch→g = h→g ∘ ch→h

-- Additional translations from Hilbert-style sequential.

hs₀→ch : ∀ {A} → HS⟨ ∅ ⊢ A ⟩ → CH.⊢ A
hs₀→ch = chs→ch ∘ hs₀→chs

hs→ch : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → CH.⊢ Γ ▻⋯▻ A
hs→ch = chs→ch ∘ hs→chs

hs→g : ∀ {A Γ} → HS⟨ Γ ⊢ A ⟩ → G⟨ Γ ⊢ A ⟩
hs→g = h→g ∘ hs→h

-- Additional translations from Hilbert-style.

h₀→chs : ∀ {A} → H⟨ ∅ ⊢ A ⟩ → CHS.⊢ A
h₀→chs = ch→chs ∘ h₀→ch

h→chs : ∀ {A Γ} → H⟨ Γ ⊢ A ⟩ → CHS.⊢ Γ ▻⋯▻ A
h→chs = ch→chs ∘ h→ch

-- Additional translations from Gentzen-style.

g₀→chs : ∀ {A} → G⟨ ∅ ⊢ A ⟩ → CHS.⊢ A
g₀→chs = h₀→chs ∘ g→h

g→chs : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → CHS.⊢ Γ ▻⋯▻ A
g→chs = h→chs ∘ g→h

g₀→ch : ∀ {A} → G⟨ ∅ ⊢ A ⟩ → CH.⊢ A
g₀→ch = h₀→ch ∘ g→h

g→ch : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → CH.⊢ Γ ▻⋯▻ A
g→ch = h→ch ∘ g→h

g→hs : ∀ {A Γ} → G⟨ Γ ⊢ A ⟩ → HS⟨ Γ ⊢ A ⟩
g→hs = h→hs ∘ g→h

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Numeral.Natural.Relation.Order.Category where

open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.IntroInstances
import      Lvl
open import Numeral.Natural
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
import      Structure.Categorical.Names as Names
open import Structure.Categorical.Properties
open import Structure.Category
import      Structure.Function.Names as Names
open import Structure.Operator
open import Structure.Relator.Properties
open import Type

instance
  [≤]-identityₗ : Morphism.Identityₗ{Obj = ℕ}(\{x} → swap(transitivity(_≤_) {x})) (reflexivity(_≤_))
  [≤]-identityₗ = Morphism.intro proof where
    proof : Names.Morphism.Identityₗ{Obj = ℕ}(\{x} → swap(transitivity(_≤_) {x})) (reflexivity(_≤_))
    proof {𝟎}   {y}   {min} = [≡]-intro
    proof {𝐒 x} {𝐒 y} {succ p} = [≡]-with succ (proof {x}{y} {p})

instance
  [≤]-identityᵣ : Morphism.Identityᵣ{Obj = ℕ}(\{x} → swap(transitivity(_≤_) {x})) (reflexivity(_≤_))
  [≤]-identityᵣ = Morphism.intro proof where
    proof : Names.Morphism.Identityᵣ{Obj = ℕ}(\{x} → swap(transitivity(_≤_) {x})) (reflexivity(_≤_))
    proof {𝟎}   {y}   {min} = [≡]-intro
    proof {𝐒 x} {𝐒 y} {succ p} = [≡]-with (p ↦ [≤]-with-[𝐒] ⦃ p ⦄) (proof {x}{y} {p})

instance
  [≤]-associativity : Morphism.Associativity{Obj = ℕ}(\{x} → swap(transitivity(_≤_) {x}))
  [≤]-associativity = Morphism.intro proof where
    proof : Names.Morphism.Associativity{Obj = ℕ}(\{x} → swap(transitivity(_≤_) {x}))
    proof {.𝟎}     {.𝟎}     {.𝟎}     {w}      {min}    {min}    {min}    = [≡]-intro
    proof {.𝟎}     {.𝟎}     {.(𝐒 _)} {.(𝐒 _)} {succ _} {min}    {min}    = [≡]-intro
    proof {.𝟎}     {.(𝐒 _)} {.(𝐒 _)} {.(𝐒 _)} {succ _} {succ _} {min}    = [≡]-intro
    proof {.(𝐒 _)} {.(𝐒 _)} {.(𝐒 _)} {.(𝐒 _)} {succ _} {succ _} {succ _} = [≡]-with succ proof

instance
  [≤]-category : Category(_≤_)
  Category._∘_ [≤]-category = swap(transitivity(_≤_))
  Category.id  [≤]-category = reflexivity(_≤_)
  Category.binaryOperator [≤]-category = intro(\{[≡]-intro [≡]-intro → [≡]-intro})

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Constructions.Exponential where

open import Level

open import Cats.Category.Base
open import Cats.Category.Constructions.Product as Product using
  (HasBinaryProducts)
open import Cats.Util.Conv

import Cats.Category.Constructions.Iso as Iso
import Cats.Category.Constructions.Unique as Unique

module Build {lo la l≈}
  (Cat : Category lo la l≈)
  {{hasBinaryProducts : HasBinaryProducts Cat}}
  where

  open Category Cat
  open ≈-Reasoning
  open Unique.Build Cat
  open Iso.Build Cat
  open HasBinaryProducts hasBinaryProducts
  open _≅_

  record Exp (B C : Obj) : Set (lo ⊔ la ⊔ l≈) where
    field
      Cᴮ : Obj
      eval : Cᴮ × B ⇒ C
      curry′ : ∀ {A} (f : A × B ⇒ C)
        → ∃![ f̃ ∈ A ⇒ Cᴮ ] (eval ∘ ⟨ f̃ × id ⟩ ≈ f)

    curry : ∀ {A} → A × B ⇒ C → A ⇒ Cᴮ
    curry f = curry′ f ⃗

    eval-curry : ∀ {A} {f : A × B ⇒ C}
      → eval ∘ ⟨ curry f × id ⟩ ≈ f
    eval-curry {f = f} = ∃!′.prop (curry′ f)

    curry-unique : ∀ {A} {f : A × B ⇒ C} {g}
      → eval ∘ ⟨ g × id ⟩ ≈ f
      → curry f ≈ g
    curry-unique {f = f} = ∃!′.unique (curry′ f)

    uncurry : ∀ {A} → A ⇒ Cᴮ → A × B ⇒ C
    uncurry f = eval ∘ ⟨ f × id ⟩

    curry∘uncurry : ∀ {A} {f : A ⇒ Cᴮ}
      → curry (uncurry f) ≈ f
    curry∘uncurry = curry-unique ≈.refl

    uncurry∘curry : ∀ {A} {f : A × B ⇒ C}
      → uncurry (curry f) ≈ f
    uncurry∘curry = eval-curry

  instance HasObj-Exp : ∀ {B C} → HasObj (Exp B C) lo la l≈
  HasObj-Exp = record { Cat = Cat ; _ᴼ = Exp.Cᴮ }

  open Exp public

  curry∘curry : ∀ {A B C Y Z} (Cᴮ : Exp B C) (Yᶻ : Exp Y Z)
    → {f : Cᴮ ᴼ × Y ⇒ Z} {g : A × B ⇒ C}
    → curry Yᶻ f ∘ curry Cᴮ g ≈ curry Yᶻ (f ∘ ⟨ curry Cᴮ g × id ⟩)
  curry∘curry Cᴮ Yᶻ {f} {g} = ≈.sym (curry-unique Yᶻ (
      begin
        eval Yᶻ ∘ ⟨ curry Yᶻ f ∘ curry Cᴮ g × id ⟩
      ≈⟨ ∘-resp-r (⟨×⟩-resp ≈.refl (≈.sym id-l)) ⟩
        eval Yᶻ ∘ ⟨ curry Yᶻ f ∘ curry Cᴮ g × id ∘ id ⟩
      ≈⟨ ∘-resp-r (≈.sym ⟨×⟩-∘) ⟩
        eval Yᶻ ∘ ⟨ curry Yᶻ f × id ⟩ ∘ ⟨ curry Cᴮ g × id ⟩
      ≈⟨ unassoc ⟩
        (eval Yᶻ ∘ ⟨ curry Yᶻ f × id ⟩) ∘ ⟨ curry Cᴮ g × id ⟩
      ≈⟨ ∘-resp-l (eval-curry Yᶻ) ⟩
        f ∘ ⟨ curry Cᴮ g × id ⟩
      ∎
    ))

  Exp-resp-≅ : ∀ {A A′ B B′}
    → A ≅ A′
    → B ≅ B′
    → (E : Exp A B) (E′ : Exp A′ B′)
    → E ᴼ ≅ E′ ᴼ
  Exp-resp-≅ A≅A′ B≅B′ E E′ = record
    { forth = curry E′ (B≅B′ .forth ∘ eval E ∘ ⟨ id × A≅A′ .back ⟩)
    ; back = curry E (B≅B′ .back ∘ eval E′ ∘ ⟨ id × A≅A′ .forth ⟩)
    -- Today in our series on 'trivial' properties (also copy-and-paste
    -- programming).
    ; back-forth = ≈.trans (curry∘curry E′ E)
        (curry-unique E (≈.trans (∘-resp-r ⟨×⟩-id) (≈.trans id-r
        (≈.sym (≈.trans assoc (≈.trans (∘-resp-r (≈.trans assoc (≈.trans
        (∘-resp-r (≈.trans ⟨×⟩-∘
        (≈.trans (⟨×⟩-resp (≈.trans id-l (≈.sym id-r)) (≈.trans id-r (≈.sym id-l)))
        (≈.sym ⟨×⟩-∘)))) (≈.trans unassoc (∘-resp-l (eval-curry E′))))))
        (≈.trans unassoc (≈.trans (∘-resp-l (≈.trans unassoc
        (≈.trans (∘-resp-l (B≅B′ .back-forth)) id-l)))
        (≈.trans assoc (≈.trans (∘-resp-r (≈.trans ⟨×⟩-∘
        (≈.trans (⟨×⟩-resp id-l (A≅A′ .back-forth)) ⟨×⟩-id))) id-r))))))))))
    ; forth-back = ≈.trans (curry∘curry E E′)
        (curry-unique E′ (≈.trans (∘-resp-r ⟨×⟩-id) (≈.trans id-r
        (≈.sym (≈.trans assoc (≈.trans (∘-resp-r (≈.trans assoc (≈.trans
        (∘-resp-r (≈.trans ⟨×⟩-∘
        (≈.trans (⟨×⟩-resp (≈.trans id-l (≈.sym id-r)) (≈.trans id-r (≈.sym id-l)))
        (≈.sym ⟨×⟩-∘)))) (≈.trans unassoc (∘-resp-l (eval-curry E))))))
        (≈.trans unassoc (≈.trans (∘-resp-l (≈.trans unassoc
        (≈.trans (∘-resp-l (B≅B′ .forth-back)) id-l)))
        (≈.trans assoc (≈.trans (∘-resp-r (≈.trans ⟨×⟩-∘
        (≈.trans (⟨×⟩-resp id-l (A≅A′ .forth-back)) ⟨×⟩-id))) id-r))))))))))
    }

record HasExponentials {lo la l≈}
  (Cat : Category lo la l≈)
  : Set (lo ⊔ la ⊔ l≈)
  where
  private open module Bld = Build Cat using (Exp)
  open Category Cat
  open Unique.Build Cat
  open Iso.Build Cat

  infixr 1 _↝′_ _↝_

  field
    {{hasBinaryProducts}} : HasBinaryProducts Cat
    _↝′_ : ∀ B C → Exp B C

  open HasBinaryProducts hasBinaryProducts

  _↝_ : Obj → Obj → Obj
  B ↝ C = (B ↝′ C) ᴼ

  eval : ∀ {B C} → (B ↝ C) × B ⇒ C
  eval {B} {C} = Bld.eval (B ↝′ C)

  curry : ∀ {A B C} → A × B ⇒ C → A ⇒ B ↝ C
  curry {B = B} {C} f = Bld.curry (B ↝′ C) f

  uncurry : ∀ {A B C} → A ⇒ B ↝ C → A × B ⇒ C
  uncurry {B = B} {C} = Bld.uncurry (B ↝′ C)

  eval-curry : ∀ {A B C} {f : A × B ⇒ C}
    → eval ∘ ⟨ curry f × id ⟩ ≈ f
  eval-curry {B = B} {C} = Bld.eval-curry (B ↝′ C)

  curry-unique : ∀ {A B C} {f : A × B ⇒ C} {g}
    → eval ∘ ⟨ g × id ⟩ ≈ f
    → curry f ≈ g
  curry-unique {B = B} {C} = Bld.curry-unique (B ↝′ C)

  curry∘uncurry : ∀ {A B C} {f : A ⇒ B ↝ C}
    → curry (uncurry f) ≈ f
  curry∘uncurry {B = B} {C} = Bld.curry∘uncurry (B ↝′ C)

  uncurry∘curry : ∀ {A B C} {f : A × B ⇒ C}
    → uncurry (curry f) ≈ f
  uncurry∘curry {B = B} {C} = Bld.uncurry∘curry (B ↝′ C)

  curry∘curry : ∀ {A B C Y Z}
    → {f : (B ↝ C) × Y ⇒ Z} {g : A × B ⇒ C}
    → curry f ∘ curry g ≈ curry (f ∘ ⟨ curry g × id ⟩)
  curry∘curry {B = B} {C} {Y} {Z} = Bld.curry∘curry (B ↝′ C) (Y ↝′ Z)

  ↝-resp-≅ : ∀ {A A′ B B′}
    → A ≅ A′
    → B ≅ B′
    → (A ↝ B) ≅ (A′ ↝ B′)
  ↝-resp-≅ {A} {A′} {B} {B′} A≅A′ B≅B′
    = Bld.Exp-resp-≅ A≅A′ B≅B′ (A ↝′ B) (A′ ↝′ B′)

open Build public

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


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

module Control.Monad.Levels.Eliminators where

open import Prelude
open import Data.Bag
open import Control.Monad.Levels.Definition

record Eliminator {a p} (A : Type a) (P : Levels A → Type p) : Type (a ℓ⊔ p) where
  constructor elim
  field
    ⟦_⟧-set : ∀ {xs} → isSet (P xs)
    ⟦_⟧_∷_⟨_⟩ : ∀ x xs → P xs → P (x ∷ xs)
    ⟦_⟧[] : P []
    ⟦_⟧-trail : PathP (λ i → P (trail i)) (⟦_⟧_∷_⟨_⟩ [] [] ⟦_⟧[]) ⟦_⟧[]

  run : ∀ xs → P xs
  run (x ∷ xs) = ⟦_⟧_∷_⟨_⟩ x xs (run xs)
  run [] = ⟦_⟧[]
  run (trail i) = ⟦_⟧-trail i
  run (trunc xs ys x y i j) =
    isOfHLevel→isOfHLevelDep 2
      (λ xs → ⟦_⟧-set {xs})
      (run xs) (run ys)
      (cong run x) (cong run y)
      (trunc xs ys x y)
      i j

  _⇓_ : (xs : Levels A) → P xs
  _⇓_ = run
  {-# INLINE _⇓_ #-}
open Eliminator public
infixr 1 Eliminator

syntax Eliminator A (λ v → e) = Levels-Π[ v ⦂ e ] A

record Recursor (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
  constructor rec
  field
    [_]-set : isSet B
    [_]_∷_⟨_⟩ : (x : ⟅ A ⟆) → (xs : Levels A) → B → B
    [_][] : B
  private f = [_]_∷_⟨_⟩; z = [_][]
  field
    [_]-trail : f [] [] z ≡ z

  _↑ : Eliminator A (λ _ → B)
  _↑ = elim [_]-set f z [_]-trail

  _↓_ : Levels A → B
  _↓_ = run _↑
  {-# INLINE _↑ #-}
  {-# INLINE _↓_ #-}
open Recursor public

infixr 1 Recursor

syntax Recursor A B = Levels-ϕ[ A ] B

infix 4 _⊜_
record AnEquality (A : Type a) : Type a where
  constructor _⊜_
  field lhs rhs : Levels A
open AnEquality public

record Property {r} (A : Type a) (P : Levels A → Type r) : Type (a ℓ⊔ r) where
  constructor property
  field
    ∥_∥-prop : ∀ {xs} → isProp (P xs)
    ∥_∥_∷_⟨_⟩ : (x : ⟅ A ⟆) → (xs : Levels A) → P xs → P (x ∷ xs)
    ∥_∥[] : P []
  private z = ∥_∥[]; f = ∥_∥_∷_⟨_⟩
  ∥_∥⇑ = elim
          (λ {xs} → isProp→isSet (∥_∥-prop {xs}))
          f z
          (toPathP (∥_∥-prop (transp (λ i → P (trail i)) i0 (f [] [] z)) z))
  ∥_∥⇓ = run ∥_∥⇑
  {-# INLINE ∥_∥⇑ #-}
  {-# INLINE ∥_∥⇓ #-}
open Property public

infixr 1 Property

syntax Property A (λ v → e) = Levels-ψ[ v ⦂ A ] e

record EqualityProof {B : Type b} (A : Type a) (P : Levels A → AnEquality B) : Type (a ℓ⊔ b) where
  Pr : Levels A → Type b
  Pr xs = let e = P xs in lhs e ≡ rhs e

  field
    ⟦_⟧≡_∷_⟨_⟩ : (x : ⟅ A ⟆) → (xs : Levels A) → Pr xs → Pr (x ∷ xs)
    ⟦_⟧≡[] : Pr []

  _⇑≡ : Eliminator A Pr
  _⇑≡ = ∥ property (trunc _ _) ⟦_⟧≡_∷_⟨_⟩ ⟦_⟧≡[] ∥⇑

  _⇓≡_ : (xs : Levels A) → Pr xs
  _⇓≡_ = run _⇑≡
  {-# INLINE _⇑≡ #-}
  {-# INLINE _⇓≡_ #-}
open EqualityProof public

infixr 1 EqualityProof
syntax EqualityProof A (λ v → e) = Levels-ψ[ v ⦂ A ]≡ e

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import LogicalFormulae
open import Groups.Groups
open import Functions.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Integers.Integers
open import Numbers.Modulo.Group
open import Numbers.Modulo.Definition
open import Rings.Examples.Proofs
open import Numbers.Primes.PrimeNumbers
open import Setoids.Setoids
open import Rings.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Sets.EquivalenceRelations

module Rings.Examples.Examples where

multiplicationNotGroup : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) → (nontrivial : Setoid._∼_ S (Ring.1R R) (Ring.0R R) → False) → Group S _*_ → False
multiplicationNotGroup {S = S} R 1!=0 gr = exFalso (1!=0 (groupsHaveLeftCancellation gr (Ring.0R R) (Ring.1R R) (Ring.0R R) (transitive (Ring.timesZero' R) (symmetric (Ring.timesZero' R)))))
  where
    open Setoid S
    open Equivalence eq

nToZn : (n : ℕ) (pr : 0 <N n) (x : ℕ) → ℤn n pr
nToZn n pr x = nToZn' n pr x

mod : (n : ℕ) → (pr : 0 <N n) → ℤ → ℤn n pr
mod n pr a = mod' n pr a

modNExampleSurjective : (n : ℕ) → (pr : 0 <N n) → Surjection (mod n pr)
modNExampleSurjective n pr = modNExampleSurjective' n pr

{-
  modNExampleGroupHom : (n : ℕ) → (pr : 0 <N n) → GroupHom ℤGroup (ℤnGroup n pr) (mod n pr)
  modNExampleGroupHom n pr = modNExampleGroupHom' n pr

  embedZnInZ : {n : ℕ} {pr : 0 <N n} → (a : ℤn n pr) → ℤ
  embedZnInZ record { x = x } = nonneg x

  modNRoundTrip : (n : ℕ) → (pr : 0 <N n) → (a : ℤn n pr) → mod n pr (embedZnInZ a) ≡ a
  modNRoundTrip zero ()
  modNRoundTrip (succ n) pr record { x = x ; xLess = xLess } with divisionAlg (succ n) x
  modNRoundTrip (succ n) _ record { x = x ; xLess = xLess } | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = quotSmall } = equalityZn _ _ p
    where
      p : rem ≡ x
      p = modIsUnique record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = quotSmall } record { quot = 0 ; rem = x ; pr = identityOfIndiscernablesLeft _ _ _ _≡_ refl (applyEquality (λ i → i +N x) (multiplicationNIsCommutative 0 n)) ; remIsSmall = inl xLess ; quotSmall = inl (succIsPositive n) }
  modNRoundTrip (succ n) _ record { x = x ; xLess = xLess } | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inr () }

-}


text:
open import Common.Reflection
open import Common.Unit
open import Common.Prelude

macro

  t1 : (A : Set) -> Term -> Term -> Tactic
  t1 x y z = give y

  t2 : Term -> (A : Set) -> Term -> Tactic
  t2 x y z = give x

  t3 : Term -> Term -> (A : Set) -> QName -> Tactic
  t3 x y z n = give x

  t4 : Term -> Term -> (A : Set) -> A -> Tactic
  t4 x y z a = give x

f1 : {A : Set} -> A -> A
f1 x = t1 Unit x x

f2 : {A : Set} -> A -> A
f2 x = t2 x Unit x

y : Set
y = Unit

f3 : {A : Set} -> A -> A
f3 x = (t3 x x Unit y)

f4 : {A : Set} -> A -> A
f4 x = t4 x x Unit unit

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module lambda.untyped where

open import Data.Nat
open import Data.Fin hiding (lift)

data term (n : ℕ) : Set where
  lam : term (suc n) → term n
  var : Fin n → term n
  app : term n → term n → term n

data norm {n : ℕ} : term n → Set
data neut {n : ℕ} : term n → Set

data norm {n} where
  lam : {x : term (suc n)} → norm x → norm (lam x)
  gnd : {x : term n} → neut x → norm x

data neut {n} where
  var : {i : Fin n} → neut (var i)
  app : {x y : term n} → neut x → norm y → neut (app x y)

lift : ∀ {n} → term n → term (suc n)
lift (lam x) = lam (lift x)
lift (var i) = var (suc i)
lift (app x y) = app (lift x) (lift y)

lift₁ : ∀ {n} → term (suc n) → term (suc (suc n))
lift₁ (lam x) = lam (lift₁ x)
lift₁ (var zero) = var zero
lift₁ (var (suc i)) = var (suc (suc i))
lift₁ (app x y) = app (lift₁ x) (lift₁ y)

↑ : ∀ {n m} → (Fin n → term m) → Fin (suc n) → term (suc m)
↑ ρ zero = var zero
↑ ρ (suc i) = lift (ρ i)

subst : ∀ {n m} → term n → (Fin n → term m) → term m
subst (lam x) ρ = lam (subst x (↑ ρ))
subst (var i) ρ = ρ i
subst (app x y) ρ = app (subst x ρ) (subst y ρ)

subst₁ : ∀ {n} → term (suc n) → term n → term n
subst₁ x y = subst x (λ {zero → y; (suc i) → var i})

data _→β_ {n : ℕ} : term n → term n → Set where
  β-beta : ∀ {x y} → app (lam x) y →β subst₁ x y
  β-app₁ : ∀ {x y z} → x →β y → app x z →β app y z
  β-app₂ : ∀ {x y z} → y →β z → app x y →β app x z
  β-lam : ∀ {x y} → x →β y → lam x →β lam y

data _β*_ {n : ℕ} : term n → term n → Set where
  ε : ∀ {x} → x β* x
  _←_ : ∀ {x y z} → x →β y → y β* z → x β* z


text:
{-# OPTIONS --without-K --no-pattern-matching #-}

module Ch2-6 where

open import Level hiding (lift)

open import Ch2-1
open import Ch2-2
open import Ch2-3
open import Ch2-4
open import Ch2-5

open import Data.Product
open import Function using (id; _∘_)

-- Definition 2.6.1
Definition-2-6-1 : ∀ {a b} {A : Set a} {B : Set b} {x y : A × B}
  → (p : x ≡ y)
  → proj₁ x ≡ proj₁ y × proj₂ x ≡ proj₂ y
Definition-2-6-1 {_} {_} {A} {B} {x} {y} p = J (A × B) D d x y p
  where
    D : (x y : A × B) (p : x ≡ y) → Set _
    D x y p = proj₁ x ≡ proj₁ y × proj₂ x ≡ proj₂ y

    d : (x : A × B) → D x x refl
    d x = refl , refl

-- Definition 2.6.3
Definition-2-6-3 : ∀ {i j} {A : Set i} {B : Set j} {x y : A × B}
  → proj₁ x ≡ proj₁ y × proj₂ x ≡ proj₂ y → x ≡ y
Definition-2-6-3 {_} {_} {A} {B} {x} {y} p
  = J A D d (proj₁ x) (proj₁ y) (proj₁ p) (proj₂ x) (proj₂ y) (proj₂ p)
  where
    D : (a b : A) (fst : a ≡ b) → Set _
    D a b fst = (a' b' : B) (snd : a' ≡ b') → (a , a') ≡ (b , b')

    d : (x : A) → D x x refl
    d x a' b' snd = J B E e a' b' snd x

      where
        E : (a' b' : B) (snd : a' ≡ b') → Set _
        E a' b' snd = (x : A) → (x , a') ≡ (x , b')

        e : (x : B) → E x x refl
        e x y = refl

pair≡ :  ∀ {a b} {A : Set a} {B : Set b} {x y : A × B}
  → proj₁ x ≡ proj₁ y × proj₂ x ≡ proj₂ y → x ≡ y
pair≡ = Definition-2-6-3

-- Theorem 2.6.2
Theorem-2-6-2 : ∀ {a b} {A : Set a} {B : Set b} (x y : A × B)
  → (x ≡ y) ≅ (proj₁ x ≡ proj₁ y × proj₂ x ≡ proj₂ y)
Theorem-2-6-2 {_} {_} {A} {B} a b = Definition-2-6-1 , it-isequiv
  --
  where
    it-isequiv : isequiv Definition-2-6-1
    it-isequiv = (Definition-2-6-3 , α) , (Definition-2-6-3 , β)

      where
        α : Definition-2-6-1 ∘ Definition-2-6-3 ~ id
        α p = J A D d (proj₁ a) (proj₁ b) (proj₁ p) (proj₂ a) (proj₂ b) (proj₂ p)
          where
            D : (x y : A) (p : x ≡ y) → Set _
            D x y p = (x' y' : B) (snd : x' ≡ y')
              → (Definition-2-6-1 ∘ Definition-2-6-3) (p , snd) ≡ ((p , snd))

            d : (x : A) → D x x refl
            d x x' y' q = J B E e x' y' q
              where
                E : (x' y' : B) (q : x' ≡ y') → Set _
                E x' y' q = (Definition-2-6-1 ∘ Definition-2-6-3) (refl , q) ≡ ((refl , q))

                e : (x' : B) → E x' x' refl
                e x' = refl

        β : Definition-2-6-3 ∘ Definition-2-6-1 ~ id
        β p = J (A × B) D d a b p
          where
            D : (x y : A × B) (p : x ≡ y) → Set _
            D x y p = (Definition-2-6-3 ∘ Definition-2-6-1) p ≡ id p

            d : (x : A × B) → D x x refl
            d x = refl

-- Definition 2.6.4
_X_ : {a b : Level} {Z : Set a}
  → (A B : Z → Set b)
  → Z → Set _
_X_ {a} {b} {Z} A B z = A z × B z

-- Theorem 2.6.4
Theorem-2-6-4 : {a b : Level} {Z : Set a}
  → (A B : Z → Set b)
  → {z w : Z} (p : z ≡ w)
  → (x : (A X B) z)
  → transport (A X B) p x ≡ ((transport A p (proj₁ x)) , transport B p (proj₂ x))
Theorem-2-6-4 {_} {_} {Z} A B {z} {w} p x = J _ D d z w p x
  where
    D : (z w : Z) (p : z ≡ w) → Set _
    D z w p = (x : (A X B) z)
      → transport (A X B) p x ≡
        (transport A p (proj₁ x) , transport B p (proj₂ x))

    d : (z : Z) → D z z refl
    d z x = refl

-- Definition 2.6.5
Definition-2-6-5 : {a a' b b' : Level}
  → {A : Set a} {A' : Set a'} {B : Set b} {B' : Set b'}
  → (g : A → A') (h : B → B')
  → A × B
  → A' × B'
Definition-2-6-5 g h x = g (proj₁ x) , h (proj₂ x)

-- Theorem 2.6.5
Theorem-2-6-5 : {a a' b b' : Level}
  → {A : Set a} {A' : Set a'} {B : Set b} {B' : Set b'}
  → (g : A → A') (h : B → B')
  → {x y : A × B}
  → (p : proj₁ x ≡ proj₁ y)
  → (q : proj₂ x ≡ proj₂ y)
  → ap (Definition-2-6-5 g h) (Definition-2-6-3 (p , q)) ≡ Definition-2-6-3 (ap g p , ap h q)
Theorem-2-6-5 {A = A} {A'} {B} {B'} g h {x} {y} p q = J _ D d (proj₁ x) (proj₁ y) p g h (proj₂ x) (proj₂ y) q
  where
    D : (x₁ y₁ : A) (p : x₁ ≡ y₁) → Set _
    D x₁ y₁ p = (g : A → A') (h : B → B') (x₂ y₂ : B) (q : x₂ ≡ y₂)
      → ap (Definition-2-6-5 g h) (Definition-2-6-3 (p , q)) ≡
        Definition-2-6-3 (ap g p , ap h q)

    d : (x : A) → D x x refl
    d x g h x₂ y₂ q = J _ E e x₂ y₂ q g h

      where
        E : (x₂ y₂ : B) (q : x₂ ≡ y₂) → Set _
        E x₂ y₂ q = (g : A → A') (h : B → B')
          → ap (Definition-2-6-5 g h) (Definition-2-6-3 (refl , q)) ≡
            Definition-2-6-3 (ap g refl , ap h q)

        e : (y : B) → E y y refl
        e y g h = refl

max_stars_repo_name: banacorn/hott

max_issues_repo_name: banacorn/hott

max_forks_repo_name: banacorn/hott


text:
module L.Base.Empty.Core where

open import Agda.Primitive

-- Introducing the empty type
data ⊥ : Set where

exfalso : ∀{c} (C : ⊥ → Set c) → (a : ⊥) → C a
exfalso = λ C ()

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
-- Andreas, 2020-03-26, issue #4481, reported by gallais

-- #952 unintentionally added named lambdas; tests here.

-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.term.expr.top:15 #-}
-- {-# OPTIONS -v tc.term.lambda:30 #-}

open import Agda.Primitive

-- Named lambdas:

postulate f : ({A : Set} → Set) → Set
_ = f λ {A = A} → A

postulate
  A : Set
  g : ({{a : A}} → A) → A
_ = g λ {{a = a}} → a

data ⊥ : Set where
record ⊤ : Set where

proj2 : ∀ a {A B : Set a} → Set a
proj2 = λ _ {B = B} → B

agdaIsConsistent : proj2 lzero {⊥} {⊤}
agdaIsConsistent = _

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

open import HoTT renaming (pt to ⊙pt)
open import cw.CW
open import cw.FinCW
open import cohomology.Theory
open import groups.Int
open import groups.DisjointlyPointedSet

module cw.cohomology.cochainequiv.AugmentCommSquare (OT : OrdinaryTheory lzero)
  (⊙fin-skel : ⊙FinSkeleton 0) where

open OrdinaryTheory OT
open import cw.cohomology.reconstructed.TipAndAugment OT ⊙⦉ ⊙fin-skel ⦊

private
  I = ⊙FinSkeleton.skel ⊙fin-skel
  ac = ⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel lzero
  pt = ⊙FinSkeleton.skel ⊙fin-skel

abstract
  augment-comm-sqr :
    CommSquareEquiv
      (GroupHom.f cw-coε)
      (_∘ᴳ FreeAbGroup-extend (Lift-abgroup {j = lzero} ℤ-abgroup) λ _ → lift 1)
      ((_∘ᴳ lower-hom {j = lzero}) ∘ <– (ℤ→ᴳ-equiv-idf (C2 0)))
      (FreeAbGroup-extend (C2-abgroup 0) ∘ GroupIso.f (C2×CX₀-diag-β ac))
  augment-comm-sqr = comm-sqr (λ g → equiv-adj'
    (GroupIso.f-equiv (FreeAbGroup-extend-iso (C2-abgroup 0) ∘eᴳ C2×CX₀-diag-β ac))
    (! $ pair×= idp
      ( ap (GroupIso.g (CX₀-diag-β ac)) (λ= λ _ → Group.inv-r (C2 0) g)
      ∙ GroupHom.pres-ident (GroupIso.g-hom (CX₀-diag-β ac))))) ,
    (GroupIso.f-is-equiv (pre∘ᴳ-iso (C2-abgroup 0) (lower-iso {j = lzero}) ∘eᴳ ℤ→ᴳ-iso-idf (C2-abgroup 0) ⁻¹ᴳ)) ,
    (GroupIso.f-is-equiv (FreeAbGroup-extend-iso (C2-abgroup 0) ∘eᴳ C2×CX₀-diag-β ac))

  augment-comm-sqrᴳ :
    CommSquareEquivᴳ
      cw-coε
      (pre∘ᴳ-hom (C2-abgroup 0) (FreeAbGroup-extend (Lift-abgroup {j = lzero} ℤ-abgroup) λ _ → lift 1))
      (pre∘ᴳ-hom (C2-abgroup 0) (lower-hom {j = lzero}) ∘ᴳ GroupIso.g-hom (ℤ→ᴳ-iso-idf (C2-abgroup 0)))
      (FreeAbGroup-extend-hom (C2-abgroup 0) ∘ᴳ GroupIso.f-hom (C2×CX₀-diag-β ac))
  augment-comm-sqrᴳ =
    comm-sqrᴳ (fst augment-comm-sqr □$_) , snd augment-comm-sqr

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module WErrorOverride where

postulate
  IO : Set → Set

{-# COMPILE GHC IO = type IO #-}
{-# BUILTIN IO IO #-}

infixl 1 _>>=_

postulate
  return : {A : Set} → A → IO A
  _>>=_  : {A : Set} {B : Set} → IO A → (A → IO B) → IO B

{-# COMPILE GHC return = \_ -> return  #-}
{-# COMPILE GHC _>>=_  = \_ _ -> (>>=) #-}

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

-- An error should be raised if one tries to do something like this:

data PartialBool : Set where
  true : PartialBool

{-# COMPILE GHC PartialBool = data Bool (True) #-}

-- However one can override such behaviour by passing the flag
-- --ghc-flag=-Wwarn to Agda upon compilation.

main = return true


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

module Cubical.Categories.Limits.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Unit
open import Cubical.Data.Sigma using (ΣPathP)
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Instances.Sets

private
  variable
    ℓJ ℓJ' ℓC ℓC' : Level
    ℓ ℓ' ℓ'' : Level

module _ {J : Category ℓJ ℓJ'}
         {C : Category ℓC ℓC'} where
  open Category
  open Functor
  open NatTrans

  -- functor which sends all objects to c and all
  -- morphisms to the identity
  constF : (c : C .ob) → Functor J C
  constF c .F-ob _ = c
  constF c .F-hom _ = C .id
  constF c .F-id = refl
  constF c .F-seq _ _ = sym (C .⋆IdL _)

  -- a cone is a natural transformation from the constant functor at x to K
  Cone : (K : Functor J C) → C .ob → Type _
  Cone K x = NatTrans (constF x) K

  module _ {K : Functor J C} where

    -- precomposes a cone with a morphism
    _◼_ : ∀ {d c : C .ob}
        → (f : C [ d , c ])
        → Cone K c
        → Cone K d
    (f ◼ μ) .N-ob x = f ⋆⟨ C ⟩ μ ⟦ x ⟧
    (f ◼ μ) .N-hom {x = x} {y} k
      = C .id ⋆⟨ C ⟩ (f ⋆⟨ C ⟩ μ ⟦ y ⟧)
      ≡⟨ C .⋆IdL _ ⟩
        f ⋆⟨ C ⟩ μ ⟦ y ⟧
      ≡⟨ cong (λ v → f ⋆⟨ C ⟩ v) (sym (C .⋆IdL _)) ⟩
        f ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ μ ⟦ y ⟧)
      ≡⟨ cong (λ v → f ⋆⟨ C ⟩ v) (μ .N-hom k) ⟩
        f ⋆⟨ C ⟩ (μ ⟦ x ⟧ ⋆⟨ C ⟩ K ⟪ k ⟫)
      ≡⟨ sym (C .⋆Assoc _ _ _) ⟩
        f ⋆⟨ C ⟩ μ ⟦ x ⟧ ⋆⟨ C ⟩ K ⟪ k ⟫
      ∎

    -- μ factors ν if there's a morphism such that the natural transformation
    -- from precomposing it with ν gives you back μ
    _factors_ : {u v : C .ob} (μ : Cone K u) (ν : Cone K v) → Type _
    _factors_ {u} {v} μ ν = Σ[ mor ∈ C [ v , u ] ] ν ≡ (mor ◼ μ)

    -- μ uniquely factors ν if the factor from above is contractible
    _uniquelyFactors_ : {u v : C .ob} (μ : Cone K u) (ν : Cone K v) → Type _
    _uniquelyFactors_ {u} {v} μ ν = isContr (μ factors ν)

  module _ (K : Functor J C) where

    -- a Limit is a cone such that all cones are uniquely factored by it
    record isLimit (head : C .ob) : Type (ℓ-max (ℓ-max ℓJ ℓJ') (ℓ-max ℓC ℓC'))  where
      field
        cone : Cone K head
        -- TODO: change this to terminal object in category of Cones?
        up   : ∀ {v} (ν : Cone K v) → cone uniquelyFactors ν

    record Limit : Type (ℓ-max (ℓ-max ℓJ ℓJ') (ℓ-max ℓC ℓC'))  where
      field
        head : C .ob
        islim : isLimit head

-- a Category is complete if it has all limits
complete' : {ℓJ ℓJ' : Level} (C : Category ℓC ℓC') → Type _
complete' {ℓJ = ℓJ} {ℓJ'} C = (J : Category ℓJ ℓJ') (K : Functor J C) → Limit K

complete : (C : Category ℓC ℓC') → Typeω
complete C = ∀ {ℓJ ℓJ'} → complete' {ℓJ = ℓJ} {ℓJ'} C

open Limit
open NatTrans
open Category

-- TODO:

-- 1. every diagram has limits isomorphic to the limit of an equalizer of products

-- 2. every equalizer can be made into a pullback

-- 3. every product can be made into an equalizer

-- 4. a category with all pullbacks and a terminal object has all limits

-- SET is complete

-- notes:
-- didn't need to restrict to *finite* diagrams , why is that required in Set theoretic?
-- didn't use coinduction here because Agda didn't like me referencing 'cone' frome 'up' (termination check)

isCompleteSET : ∀ {ℓJ ℓJ'} → complete' {ℓJ = ℓJ} {ℓJ'} (SET (ℓ-max ℓJ ℓJ'))
isCompleteSET J K = record
                  { head = head'
                  ; islim = record { cone = cone' ; up = up' } }
  where
    -- the limit is defined as the Set of all cones with head Unit
    head' = Cone K (Unit* , isOfHLevelLift 2 isSetUnit) , isSetNat

    -- the legs are defined by taking a cone to its component at j
    cone' : Cone K head'
    cone' .N-ob j μ = (μ ⟦ j ⟧) tt*
    -- Naturality follows from naturality of the Unit cone
    cone' .N-hom {x = i} {j} f
      = funExt λ μ → (μ ⟦ j ⟧) tt*
        ≡[ i ]⟨ (μ .N-hom f i) tt* ⟩
          (K ⟪ f ⟫) ((μ ⟦ i ⟧) tt*)
        ∎

    -- Given another cone α, we want a unique function f from α → cone' which factors it
    -- factorization property enforces that (cone' ⟦ j ⟧ ● f) ≡ α ⟦ j ⟧
    -- but cone' ⟦ j ⟧ simply takes the jth component the output Cone K Unit from f
    -- so this enforces that for all x ∈ A, (f x) ⟦ j ⟧ ≡ α ⟦ j ⟧ x
    -- this determines the *only* possible factoring morphism
    up' : ∀ {A} (α : Cone K A) → cone' uniquelyFactors α
    up' {A} α = (f , fact) , unique
      where
        f : fst A → Cone K (Unit* , isOfHLevelLift 2 isSetUnit)
        f x = natTrans (λ j _ → α .N-ob j x)
                       (λ {m} {n} f → funExt λ μ i → α .N-hom f i x)

        fact : α ≡ (f ◼ cone')
        fact = makeNatTransPath refl -- I LOVE DEFINITIONAL EQUALITY

        unique : (τ : cone' factors α) → (f , fact) ≡ τ
        unique (f' , fact') = ΣPathP (f≡f' , fact≡fact')
          where
            f≡f' : f ≡ f'
            f≡f' = funExt λ x → makeNatTransPath (funExt λ _ → sym eq2)
              where
                -- the factorization property enforces that f' must have the same behavior as f
                eq1 : ∀ {x j} → ((cone' ⟦ j ⟧) (f' x)) ≡ (α ⟦ j ⟧) x
                eq1 {x} {j} i = ((fact' (~ i)) ⟦ j ⟧) x

                eq2 : ∀ {x j} → (f' x) ⟦ j ⟧ ≡ λ _ → (α ⟦ j ⟧) x -- = (f x) ⟦ j ⟧
                eq2 {x} {j} = funExt λ _ → eq1

            -- follows from Set having homsets
            fact≡fact' : PathP (λ i → α ≡ ((f≡f' i) ◼ cone')) fact fact'
            fact≡fact' = isOfHLevel→isOfHLevelDep 1 (λ β → isSetNat α β) fact fact' λ i → (f≡f' i) ◼ cone'

max_stars_repo_name: mzeuner/cubical

max_issues_repo_name: mzeuner/cubical

max_forks_repo_name: mzeuner/cubical


text:
{-# OPTIONS --cubical --safe --no-import-sorts #-}

module Cubical.Data.Fin.Recursive.Base where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty as Empty hiding (rec; elim)
open import Cubical.Data.Nat hiding (elim)

data FinF (X : Type₀) : Type₀ where
  zero : FinF X
  suc : X → FinF X

Fin : ℕ → Type₀
Fin zero = ⊥
Fin (suc k) = FinF (Fin k)

private
  variable
    ℓ : Level
    k : ℕ
    R : Type ℓ

rec : R → (R → R) → Fin k → R
rec {k = suc k} z _ zero = z
rec {k = suc k} z s (suc x) = s (rec z s x)

elim
  : ∀(P : ∀{k} → Fin k → Type ℓ)
  → (∀{k} → P {suc k} zero)
  → (∀{k} (fn : Fin k) → P fn → P {suc k} (suc fn))
  → (fn : Fin k) → P fn
elim {k = suc k} P fz fs zero = fz
elim {k = suc k} P fz fs (suc x) = fs x (elim P fz fs x)

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:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Bool where

open import Cubical.Data.Bool.Base public

open import Cubical.Data.Bool.Properties public


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Propositional (intensional) equality
------------------------------------------------------------------------

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

module Relation.Binary.PropositionalEquality where

import Axiom.Extensionality.Propositional as Ext
open import Axiom.UniquenessOfIdentityProofs
open import Function
open import Function.Equality using (Π; _⟶_; ≡-setoid)
open import Level
open import Data.Empty
open import Data.Product
open import Relation.Nullary using (yes ; no)
open import Relation.Unary using (Pred)
open import Relation.Binary
open import Relation.Binary.Indexed.Heterogeneous
  using (IndexedSetoid)
import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
  as Trivial

------------------------------------------------------------------------
-- Re-export contents of core module

open import Relation.Binary.PropositionalEquality.Core public

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

subst₂ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p)
         {x₁ x₂ y₁ y₂} → x₁ ≡ x₂ → y₁ ≡ y₂ → P x₁ y₁ → P x₂ y₂
subst₂ P refl refl p = p

cong-app : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
           f ≡ g → (x : A) → f x ≡ g x
cong-app refl x = refl

cong₂ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
        (f : A → B → C) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v
cong₂ f refl refl = refl

setoid : ∀ {a} → Set a → Setoid _ _
setoid A = record
  { Carrier       = A
  ; _≈_           = _≡_
  ; isEquivalence = isEquivalence
  }

decSetoid : ∀ {a} {A : Set a} → Decidable {A = A} _≡_ → DecSetoid _ _
decSetoid dec = record
  { _≈_              = _≡_
  ; isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = dec
      }
  }

isPreorder : ∀ {a} {A : Set a} → IsPreorder {A = A} _≡_ _≡_
isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = id
  ; trans         = trans
  }

preorder : ∀ {a} → Set a → Preorder _ _ _
preorder A = record
  { Carrier    = A
  ; _≈_        = _≡_
  ; _∼_        = _≡_
  ; isPreorder = isPreorder
  }

------------------------------------------------------------------------
-- Pointwise equality

infix 4 _≗_

_→-setoid_ : ∀ {a b} (A : Set a) (B : Set b) → Setoid _ _
A →-setoid B = ≡-setoid A (Trivial.indexedSetoid (setoid B))

_≗_ : ∀ {a b} {A : Set a} {B : Set b} (f g : A → B) → Set _
_≗_ {A = A} {B} = Setoid._≈_ (A →-setoid B)

:→-to-Π : ∀ {a b₁ b₂} {A : Set a} {B : IndexedSetoid _ b₁ b₂} →
          ((x : A) → IndexedSetoid.Carrier B x) → Π (setoid A) B
:→-to-Π {B = B} f = record { _⟨$⟩_ = f; cong = cong′ }
  where
  open IndexedSetoid B using (_≈_)

  cong′ : ∀ {x y} → x ≡ y → f x ≈ f y
  cong′ refl = IndexedSetoid.refl B

→-to-⟶ : ∀ {a b₁ b₂} {A : Set a} {B : Setoid b₁ b₂} →
         (A → Setoid.Carrier B) → setoid A ⟶ B
→-to-⟶ = :→-to-Π

------------------------------------------------------------------------
-- Inspect

-- Inspect can be used when you want to pattern match on the result r
-- of some expression e, and you also need to "remember" that r ≡ e.

record Reveal_·_is_ {a b} {A : Set a} {B : A → Set b}
                    (f : (x : A) → B x) (x : A) (y : B x) :
                    Set (a ⊔ b) where
  constructor [_]
  field eq : f x ≡ y

inspect : ∀ {a b} {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]

-- Example usage:

-- f x y with g x | inspect g x
-- f x y | c z | [ eq ] = ...

------------------------------------------------------------------------
-- Propositionality

isPropositional : ∀ {a} → Set a → Set a
isPropositional A = (a b : A) → a ≡ b

------------------------------------------------------------------------
-- Various equality rearrangement lemmas

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

  trans-injectiveˡ : ∀ {z} {p₁ p₂ : x ≡ y} (q : y ≡ z) →
                     trans p₁ q ≡ trans p₂ q → p₁ ≡ p₂
  trans-injectiveˡ refl = subst₂ _≡_ (trans-reflʳ _) (trans-reflʳ _)

  trans-injectiveʳ : ∀ {z} (p : x ≡ y) {q₁ q₂ : y ≡ z} →
                     trans p q₁ ≡ trans p q₂ → q₁ ≡ q₂
  trans-injectiveʳ refl eq = eq

cong-id :
  ∀ {a} {A : Set a} {x y : A} (p : x ≡ y) →
  cong id p ≡ p
cong-id refl = refl

cong-∘ :
  ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} {x y : A}
    {f : B → C} {g : A → B}
  (p : x ≡ y) →
  cong (f ∘ g) p ≡ cong f (cong g p)
cong-∘ refl = refl

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

  subst-injective : ∀ (x≡y : x ≡ y) {p q : P x} →
    subst P x≡y p ≡ subst P x≡y q → p ≡ q
  subst-injective refl p≡q = p≡q

  subst-subst : ∀ {z} (x≡y : x ≡ y) {y≡z : y ≡ z} {p : P x} →
    subst P y≡z (subst P x≡y p) ≡ subst P (trans x≡y y≡z) p
  subst-subst refl = refl

  subst-subst-sym : (x≡y : x ≡ y) {p : P y} →
    subst P x≡y (subst P (sym x≡y) p) ≡ p
  subst-subst-sym refl = refl

  subst-sym-subst : (x≡y : x ≡ y) {p : P x} →
    subst P (sym x≡y) (subst P x≡y p) ≡ p
  subst-sym-subst refl = refl

subst-∘ :
  ∀ {a b p} {A : Set a} {B : Set b} {x y : A} {P : B → Set p}
    {f : A → B}
  (x≡y : x ≡ y) {p : P (f x)} →
  subst (P ∘ f) x≡y p ≡ subst P (cong f x≡y) p
subst-∘ refl = refl

subst-application :
  ∀ {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
    (B₁ : A₁ → Set b₁) {B₂ : A₂ → Set b₂}
    {f : A₂ → A₁} {x₁ x₂ : A₂} {y : B₁ (f x₁)}
  (g : ∀ x → B₁ (f x) → B₂ x) (eq : x₁ ≡ x₂) →
  subst B₂ eq (g x₁ y) ≡ g x₂ (subst B₁ (cong f eq) y)
subst-application _ _ refl = refl

-- A lemma that is very similar to Lemma 2.4.3 from the HoTT book.

naturality :
  ∀ {a b} {A : Set a} {B : Set b} {x y} {x≡y : x ≡ y} {f g : A → B}
  (f≡g : ∀ x → f x ≡ g x) →
  trans (cong f x≡y) (f≡g y) ≡ trans (f≡g x) (cong g x≡y)
naturality {x = x} {x≡y = refl} f≡g =
  f≡g x               ≡⟨ sym (trans-reflʳ _) ⟩
  trans (f≡g x) refl  ∎
  where
  open ≡-Reasoning

-- A lemma that is very similar to Corollary 2.4.4 from the HoTT book.

cong-≡id :
  ∀ {a} {A : Set a} {f : A → A} {x : A}
  (f≡id : ∀ x → f x ≡ x) →
  cong f (f≡id x) ≡ f≡id (f x)
cong-≡id {f = f} {x} f≡id =
  cong f (f≡id x)                                               ≡⟨ sym (trans-reflʳ _) ⟩
  trans (cong f (f≡id x)) refl                                  ≡⟨ cong (trans _) (sym (trans-symʳ (f≡id x))) ⟩
  trans (cong f (f≡id x)) (trans (f≡id x) (sym (f≡id x)))       ≡⟨ sym (trans-assoc (cong f (f≡id x))) ⟩
  trans (trans (cong f (f≡id x)) (f≡id x)) (sym (f≡id x))       ≡⟨ cong (λ p → trans p (sym _)) (naturality f≡id) ⟩
  trans (trans (f≡id (f x)) (cong id (f≡id x))) (sym (f≡id x))  ≡⟨ cong (λ p → trans (trans (f≡id (f x)) p) (sym (f≡id x))) (cong-id _) ⟩
  trans (trans (f≡id (f x)) (f≡id x)) (sym (f≡id x))            ≡⟨ trans-assoc (f≡id (f x)) ⟩
  trans (f≡id (f x)) (trans (f≡id x) (sym (f≡id x)))            ≡⟨ cong (trans _) (trans-symʳ (f≡id x)) ⟩
  trans (f≡id (f x)) refl                                       ≡⟨ trans-reflʳ _ ⟩
  f≡id (f x)                                                    ∎
  where
  open ≡-Reasoning

module _ {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A})) {a : A} where

  ≡-≟-identity : ∀ {b} (eq : a ≡ b) → a ≟ b ≡ yes eq
  ≡-≟-identity {b} eq with a ≟ b
  ... | yes p = cong yes (Decidable⇒UIP.≡-irrelevant _≟_ p eq)
  ... | no ¬p = ⊥-elim (¬p eq)

  ≢-≟-identity : ∀ {b} → a ≢ b → ∃ λ ¬eq → a ≟ b ≡ no ¬eq
  ≢-≟-identity {b} ¬eq with a ≟ b
  ... | yes p = ⊥-elim (¬eq p)
  ... | no ¬p = ¬p , refl

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

-- Version 1.0

Extensionality = Ext.Extensionality
{-# WARNING_ON_USAGE Extensionality
"Warning: Extensionality was deprecated in v1.0.
Please use Extensionality from `Axiom.Extensionality.Propositional` instead."
#-}
extensionality-for-lower-levels = Ext.lower-extensionality
{-# WARNING_ON_USAGE extensionality-for-lower-levels
"Warning: extensionality-for-lower-levels was deprecated in v1.0.
Please use lower-extensionality from `Axiom.Extensionality.Propositional` instead."
#-}
∀-extensionality = Ext.∀-extensionality
{-# WARNING_ON_USAGE ∀-extensionality
"Warning: ∀-extensionality was deprecated in v1.0.
Please use ∀-extensionality from `Axiom.Extensionality.Propositional` instead."
#-}