text:
open import Nat
open import Prelude
open import Hazelnut-core

module Hazelnut-declarative where
   -- declarative type checking judgement for ė
  data _⊢_::_ : (Γ : ·ctx) → (e : ė) → (t : τ̇) → Set where
     DVar    : {Γ : ·ctx} {t : τ̇} {n : Nat} →
                (n , t) ∈ Γ →
                Γ ⊢ X n :: t
     DAp     : {Γ : ·ctx} {e1 e2 : ė} {t t2 : τ̇} →
                Γ ⊢ e1 :: (t2 ==> t) →
                Γ ⊢ e2 :: t2 →
                Γ ⊢ (e1 ∘ e2) :: t
     DNum    :  {Γ : ·ctx} {n : Nat} →
                Γ ⊢ N n :: num
     DPlus   : {Γ : ·ctx} {e1 e2 : ė}  →
                Γ ⊢ e1 :: num →
                Γ ⊢ e2 :: num →
                Γ ⊢ (e1 ·+ e2) :: num
     DEHole  : {Γ : ·ctx} → Γ ⊢ <||> :: <||>
     DFHole  : {Γ : ·ctx} {e : ė} {t : τ̇} →
                Γ ⊢ e :: t →
                Γ ⊢ <| e |> :: <||>
     DApHole : {Γ : ·ctx} {e1 e2 : ė} →
                Γ ⊢ e1 :: <||> →
                Γ ⊢ e2 :: <||> →
                Γ ⊢ (e1 ∘ e2) :: <||>
     DLam : {Γ : ·ctx} {e : ė} {t1 t2 : τ̇} {n : Nat} →
                n # Γ →
                (Γ ,, (n , t1)) ⊢ e :: t2 →
                Γ ⊢ (·λ n e) :: (t1 ==> t2)

  -- erasure of ascriptions, following the 312 notes.
  data ||_|| : {e : ė} → ė → Set where
     -- EraseAsc : {e : ė} {x : Nat} →
  -- ||_|| : ė → ė
  -- || e ·: x ||   = || e ||
  -- || X x ||      = X x
  -- || ·λ x e ||   = ·λ x || e ||
  -- || N n ||      = N n
  -- || e1 ·+ e2 || = || e1 || ·+ || e2 ||
  -- || <||> ||     = <||>
  -- || <| e |> ||  = <| || e || |>
  -- || e1 ∘ e2 ||  = || e1 || ∘ || e2 ||

  decbidir : {Γ : ·ctx} {e : ė} {t : τ̇}
                → Γ ⊢ e :: t
                → (Γ ⊢ e => t) + (Γ ⊢ e <= t)
    -- synthesis cases
  decbidir (DVar x) = Inl (SVar x)
  decbidir (DAp d1 d2) with decbidir d1 | decbidir d2
  ... | Inl s1 | Inl s2 = Inl (SAp s1 (ASubsume s2 TCRefl))
  ... | Inl s1 | Inr a2 = Inl (SAp s1 a2)
  ... | Inr a1 | Inl s2 = Inl (SAp {!!} (ASubsume s2 TCRefl))
  ... | Inr a1 | Inr a2 = Inl (SAp {!!} a2)
  decbidir DNum = Inl SNum
  decbidir (DPlus d1 d2) with decbidir d1 | decbidir d2
  ... | Inl s1 | Inl s2 = Inl (SPlus (ASubsume s1 TCRefl) (ASubsume s2 TCRefl))
  ... | Inl s1 | Inr a2 = Inl (SPlus (ASubsume s1 TCRefl) a2)
  ... | Inr a1 | Inl s1 = Inl (SPlus a1                   (ASubsume s1 TCRefl))
  ... | Inr a1 | Inr a2 = Inl (SPlus a1                   a2)
  decbidir DEHole = Inl SEHole
  decbidir (DFHole d) with decbidir d
  ... | Inl synth = Inl (SFHole synth)
  ... | Inr (ASubsume d' _) = Inl (SFHole d')
  ... | Inr (ALam x ana) = Inl {!!}
  decbidir (DApHole d1 d2)  with decbidir d1 | decbidir d2
  ... | Inl s1 | Inl s2 = Inl (SApHole s1 (ASubsume s2 TCRefl))
  ... | Inl s1 | Inr a2 = Inl (SApHole s1 a2)
  ... | Inr a1 | Inl s2 = Inl (SApHole {!!} (ASubsume s2 TCRefl))
  ... | Inr a1 | Inr a2 = Inl (SApHole {!!} a2)
    -- analysis case
  decbidir (DLam x d) = Inr (ALam {!!} {!!})

  bidirdec : {Γ : ·ctx} {e : ė} {t : τ̇}
                → (Γ ⊢ e => t) + (Γ ⊢ e <= t)
                → Γ ⊢ e :: t
    -- synthesis cases
  bidirdec (Inl (SAsc d)) = {!!}
  bidirdec (Inl (SVar x)) = DVar x
  bidirdec (Inl (SAp d1 d2)) = DAp (bidirdec (Inl d1)) (bidirdec (Inr d2))
  bidirdec (Inl SNum) = DNum
  bidirdec (Inl (SPlus d1 d2)) = DPlus (bidirdec (Inr d1)) (bidirdec (Inr d2))
  bidirdec (Inl SEHole) = DEHole
  bidirdec (Inl (SFHole d)) = DFHole (bidirdec (Inl d))
  bidirdec (Inl (SApHole d1 d2)) = DApHole (bidirdec (Inl d1)) (bidirdec (Inr d2))
    --analysis cases
  bidirdec (Inr (ASubsume x x₁)) = {!synthunicity!}
  bidirdec (Inr (ALam x d)) = DLam x (bidirdec (Inr d))

  -- to be an isomoprhism you have to preserve structure.
  -- to : {Γ : ·ctx} {e : ė} {t : τ̇} →
  --        (d : Γ ⊢ e :: t) →
  --        (bidirdec (decbidir d)) == d
  -- to d = {!!}

  -- from : {Γ : ·ctx} {e : ė} {t : τ̇} →
  --        (dd : (Γ ⊢ e => t) + (Γ ⊢ e <= t)) →
  --        (decbidir (bidirdec dd)) == dd
  -- from dd = {!!}


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

module Data.Integer.Literals where

open import Data.Integer
open import Literals.Number
open import Data.Unit

instance
  numberNat : Number ℤ
  numberNat = record
    { Constraint = λ _ → ⊤
    ; fromNat    = λ n → ⁺ n
    }

ext: agda

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module plfa-exercises.Practice where

--------------------------------------- Naturals ---------------------------------------

-- Inductive definition of Numbers (new datatype)
data ℕ : Set where
-- Judgements (two in total for this case)
  zero : ℕ       -- No hypothesis and one conclusion
  suc  : ℕ → ℕ   -- One hypothesis and one conclusion

seven : ℕ
seven = suc (suc (suc (suc (suc (suc (suc zero))))))
--seven′ = --7

pred : ℕ → ℕ
pred zero = zero
pred (suc n) = n

---

-- Gives us the power of writing 3 to signify suc (suc (suc zero)) :)
{-# BUILTIN NATURAL ℕ #-}

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl; cong; sym; trans)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Function.Base using (flip)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product using (_×_; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)

_+_ : ℕ → ℕ → ℕ
zero + n = n                -- +-def₀
(suc m) + n = suc (m + n)   -- +-def₁

--_ : (suc (suc zero)) + (suc (suc (suc zero))) ≡ (suc (suc (suc (suc (suc zero)))))
--_ =
--  begin
--    (suc (suc zero)) + (suc (suc (suc zero)))
--  ≡⟨⟩    -- inductive case
--    suc ((suc zero) + (suc (suc (suc zero))))
--  ≡⟨⟩    -- inductive case
--    suc (suc (zero + (suc (suc (suc zero)))))
--  ≡⟨⟩    -- base case
--    suc (suc (suc (suc (suc zero))))
--  ∎
--
--_ : 2 + 3 ≡ 5
--_ =
--  begin
--    2 + 3
--    (suc 1) + 3
--  ≡⟨⟩
--    suc (1 + 3)
--  ≡⟨⟩
--    suc (suc 0 + 3)
--  ≡⟨⟩
--    suc (suc (0 + 3))
--  ≡⟨⟩
--    suc (suc 3)
--  ≡⟨⟩
--    suc 4
--  ≡⟨⟩
--    5
--  ∎
--
--
--_ : (suc (suc zero)) + (suc (suc (suc zero))) ≡ (suc (suc (suc (suc (suc zero)))))
--_ = refl

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

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

-- Monus
_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

infixl 6  _+_  _∸_
infixl 7  _*_
infixr 8  _^_

-- Superfun binary numbers :D
data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

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

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

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

fromᵇ : Bin → ℕ
fromᵇ ⟨⟩ = zero
fromᵇ (b O) = let n = fromᵇ b in n + n
fromᵇ (b I) = let n = fromᵇ b in suc (n + n)

_ : toᵇ 11 ≡ (⟨⟩ I O I I)
_ = refl

_ : fromᵇ (inc (⟨⟩ I O I I)) ≡ 12
_ = refl
--_ = begin
--      (fromᵇ (⟨⟩ I I O O))
--    ≡⟨ 12 ≡⟨⟩ 12 ∎ ⟩
--      12
--    ∎

--_ : Set₉₁₁₁₁₁₁₁₁₁₁₁₁₁₁₁₁₁₁₁₁
--_ : Set₀
_ : Set
_ = suc 11 ≡ 12

_+ᵇ_ : Bin → Bin → Bin
⟨⟩    +ᵇ b     = b
b     +ᵇ ⟨⟩    = b
--(b O) +ᵇ ⟨⟩    = b O
(b O) +ᵇ (d O) = (b +ᵇ d) O
(b O) +ᵇ (d I) = (b +ᵇ d) I
--(b I) +ᵇ ⟨⟩    = b I
(b I) +ᵇ (d O) = (b +ᵇ d) I
(b I) +ᵇ (d I) = (inc (b +ᵇ d)) O

-- Proving the following is trivial
mod-left : ∀ {b : Bin} → ⟨⟩ +ᵇ b ≡ b
mod-left = refl
-- But not its complement. This is due to "case trees" (or how Agda implements
-- functions under the hood)
-- https://agda.readthedocs.io/en/v2.6.0.1/language/function-definitions.html#case-trees
mod-right : ∀ {b : Bin} → b +ᵇ ⟨⟩ ≡ b
mod-right {⟨⟩}  = refl
mod-right {b O} = refl
mod-right {b I} = refl
-- Also, I'm confused on the implications of improper "case trees". If the
-- second rule wasn't reachable, the following code would run even
-- if the rule was nonesense (eg, changing `b +ᵇ ⟨⟩ = b O O`) but it doesn't
-- work! The rule must make sense. So, Agda is applying the rule after all and
-- not ignoring it even thought it can't be reached directly in proofs
_ : (⟨⟩ I O I I I) +ᵇ (⟨⟩ O O I) ≡ ⟨⟩ I I O O O
_ = refl

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

-- Taken it from book
assoc-+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
assoc-+ zero n p = refl
assoc-+ (suc m) n p rewrite assoc-+ m n p = refl

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

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

comm-+ : ∀ (n m : ℕ) → n + m ≡ m + n
comm-+ zero n = sym (comm-+₀ n)
comm-+ (suc n) m rewrite comm-+ n m | succ_right m n = refl
--comm-+ (suc n) m = trans (cong suc (comm-+ n m)) (succ_right m n)
--comm-+ (suc n) m =
--  begin
--    suc n + m
--  ≡⟨⟩ -- +-def₁
--    suc (n + m)
--  ≡⟨ cong suc (comm-+ n m) ⟩
--    suc (m + n)
--  ≡⟨ succ_right m n ⟩
--    m + suc n
--  ∎

-- Try evaluating and type-checking the following expressions:
-- comm-+ zero
-- (flip comm-+) zero
-- λ n m → cong suc (comm-+ n m)
-- λ m n → succ_right m n
-- λ m n → sym (succ_right m n)
-- λ n m → trans (cong suc (comm-+ n m)) (succ_right m n)

monus : ∀ (n : ℕ) → zero ∸ n ≡ zero
monus zero = refl
monus (suc n) = refl
--monus : ∀ {n : ℕ} → zero ∸ n ≡ zero
--monus {zero} = refl
--monus {suc n} = refl

inc≡suc : ∀ (b : Bin) → fromᵇ (inc b) ≡ suc (fromᵇ b)
inc≡suc ⟨⟩ = refl
inc≡suc (b O) rewrite sym (comm-+₀ (fromᵇ b)) = refl
inc≡suc (b I)
  rewrite
    comm-+₀ (fromᵇ (inc b))
  | inc≡suc b
  | succ_right (fromᵇ b) (fromᵇ b)
  | comm-+₀ (fromᵇ b)
  | succ_right (fromᵇ b) (fromᵇ b) = refl

-- `toᵇ (fromᵇ b) ≡ b` doesn't hold for all values, just for some.
-- So the following is false
--tofromb≢b : ∀ (b : Bin) → ¬ (toᵇ (fromᵇ b) ≡ b)
--tofromb≢b ⟨⟩ = λ()
--tofromb≢b = ? -- impossible to prove

_ : ¬ (toᵇ (fromᵇ ⟨⟩) ≡ ⟨⟩)
_ = λ()

--from∘toᵇ₀ : ∀ (n : ℕ) → fromᵇ ((toᵇ n) O) ≡ fromᵇ (toᵇ n) + fromᵇ (toᵇ n)
--from∘toᵇ₀ zero = refl
--from∘toᵇ₀ (suc n) = refl
--
--from∘toᵇ₁ : ∀ (n : ℕ) → fromᵇ ((toᵇ n) I) ≡ suc (fromᵇ (toᵇ n) + fromᵇ (toᵇ n))
--from∘toᵇ₁ zero = refl
--from∘toᵇ₁ (suc n) = refl

monobin₀ : ∀ (b : Bin) → inc (inc (b +ᵇ b)) ≡ (inc b +ᵇ inc b)
monobin₀ ⟨⟩ = refl
monobin₀ (b O) = refl
monobin₀ (b I) rewrite monobin₀ b = refl

monobin : ∀ (n : ℕ) → toᵇ (n + n) ≡ (toᵇ n) +ᵇ (toᵇ n)
monobin zero = refl
monobin (suc n) rewrite
    sym (succ_right n n)
  | monobin n
  | monobin₀ (toᵇ n) = refl

--mononat₀ : ∀ (a : Bin) → a +ᵇ ⟨⟩ ≡ a
--mononat₀ ⟨⟩ = refl
--mononat₀ (b O) = refl
--mononat₀ (b I) = refl
--
--mononat₁ : ∀ (a b : Bin) → fromᵇ (inc (a +ᵇ b)) ≡ suc (fromᵇ a + fromᵇ b)
--mononat₁ ⟨⟩ b rewrite inc≡suc b = refl
--mononat₁ a ⟨⟩ rewrite mononat₀ a | comm-+₀ (fromᵇ a) | inc≡suc a = refl
--mononat₁ = ?
---- λ a → fromᵇ (inc (a +ᵇ ⟨⟩)) ≡ suc (fromᵇ a + fromᵇ ⟨⟩)
---- fromᵇ (inc b) ≡ suc (fromᵇ b)
--
--mononat : ∀ (a b : Bin) → fromᵇ (a +ᵇ b) ≡ fromᵇ a + fromᵇ b
--mononat ⟨⟩ _ = refl
--mononat a ⟨⟩ rewrite mononat₀ a | comm-+₀ (fromᵇ a) = refl
----mononat a ⟨⟩ =
----  begin
----    fromᵇ (a +ᵇ ⟨⟩)
----    ≡⟨ cong fromᵇ (mononat₀ a) ⟩
----    fromᵇ (a)
----    ≡⟨ sym (comm-+₀ (fromᵇ a)) ⟩
----    fromᵇ a + zero
----    ≡⟨⟩
----    fromᵇ a + fromᵇ ⟨⟩
----  ∎
--mononat (a O) (b O) rewrite
--    mononat a b
--  | assoc-+ (fromᵇ a) (fromᵇ b) (fromᵇ a + fromᵇ b)
--  | comm-+ (fromᵇ b) (fromᵇ a + fromᵇ b)
--  | assoc-+ (fromᵇ a) (fromᵇ a) (fromᵇ b + fromᵇ b)
--  | assoc-+ (fromᵇ a) (fromᵇ b) (fromᵇ b)
--  = refl
--mononat (a I) (b O) rewrite
--    mononat a b
--  | assoc-+ (fromᵇ a) (fromᵇ b) (fromᵇ a + fromᵇ b)
--  | comm-+ (fromᵇ b) (fromᵇ a + fromᵇ b)
--  | assoc-+ (fromᵇ a) (fromᵇ a) (fromᵇ b + fromᵇ b)
--  | assoc-+ (fromᵇ a) (fromᵇ b) (fromᵇ b)
--  = refl
--mononat (a O) (b I) rewrite
--    mononat a b
--  | sym (succ_right (fromᵇ a + fromᵇ a) (fromᵇ b + fromᵇ b))
--  | assoc-+ (fromᵇ a) (fromᵇ b) (fromᵇ a + fromᵇ b)
--  | comm-+ (fromᵇ b) (fromᵇ a + fromᵇ b)
--  | assoc-+ (fromᵇ a) (fromᵇ a) (fromᵇ b + fromᵇ b)
--  | assoc-+ (fromᵇ a) (fromᵇ b) (fromᵇ b)
--  = refl
--mononat (a I) (b I) rewrite
--    mononat₁ a b
--  | sym (succ_right (fromᵇ a + fromᵇ a) (fromᵇ b + fromᵇ b))
--  | sym (succ_right (fromᵇ a + fromᵇ b) (fromᵇ a + fromᵇ b))
--  | assoc-+ (fromᵇ a) (fromᵇ b) (fromᵇ a + fromᵇ b)
--  | comm-+ (fromᵇ b) (fromᵇ a + fromᵇ b)
--  | assoc-+ (fromᵇ a) (fromᵇ a) (fromᵇ b + fromᵇ b)
--  | assoc-+ (fromᵇ a) (fromᵇ b) (fromᵇ b)
--  = refl

-- Really hard!! Keep working on it!
-- IT WASN'T HARD!!! I JUST COULDN'T SEE THE RIGHT REWRITE!!
from∘toᵇ : ∀ (n : ℕ) → fromᵇ (toᵇ n) ≡ n
from∘toᵇ zero = refl
from∘toᵇ (suc n) rewrite inc≡suc (toᵇ n) | from∘toᵇ n = refl
--from∘toᵇ (suc n) =
--  begin
--    fromᵇ (toᵇ (suc n))
--  ≡⟨⟩
--    fromᵇ (inc (toᵇ n))
--  ≡⟨ inc≡suc (toᵇ n) ⟩
--    suc (fromᵇ (toᵇ n))
--  ≡⟨ cong suc (from∘toᵇ n) ⟩
--    suc n
--  ∎

swap-m-n-+ : ∀ (m n p) → m + (n + p) ≡ n + (m + p)
swap-m-n-+ m n p rewrite
    sym (assoc-+ m n p)
  | sym (assoc-+ n m p)
  | comm-+ m n
  = refl

right-zero-* : ∀ (n : ℕ) → n * 0 ≡ 0
right-zero-* zero    = refl
right-zero-* (suc n) rewrite right-zero-* n = refl

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

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

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

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

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

swap-m-n-* : ∀ (m n p) → m * (n * p) ≡ n * (m * p)
swap-m-n-* m n p rewrite
    sym (assoc-* m n p)
  | sym (assoc-* n m p)
  | comm-* m n
  = refl

distr-^-* : ∀ (m n p) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
--distr-^-* m n zero    =
--  begin
--    (m * n) ^ zero
--  ≡⟨⟩
--    (m * n) ^ 0
--  ≡⟨⟩
--    suc 0
--  ≡⟨⟩
--    1
--  ≡⟨⟩
--    1 + 0
--  ≡⟨⟩
--    1 + 0 * 1
--  ≡⟨⟩
--    (suc 0) * 1
--  ≡⟨⟩
--    (suc 0) * 1
--  ≡⟨⟩
--    1 * 1
--  ≡⟨⟩
--    1 * (n ^ 0)
--  ≡⟨⟩
--    (m ^ zero) * (n ^ zero)
--  ≡⟨⟩
--    (m ^ 0) * (n ^ 0)
--  ∎
distr-^-* _       _       zero    = refl
distr-^-* zero    zero    (suc p) = refl
distr-^-* zero    (suc n) (suc p) = refl
distr-^-* (suc m) zero    (suc p)
  rewrite
    right-zero-* (suc m ^ suc p)
  | right-zero-* m
  = refl
distr-^-* (suc m) (suc n) (suc p)
  rewrite
--  (suc m * suc n) ^ suc p ≡ suc m ^ suc p * suc n ^ suc p
--
--    suc (n + m * suc n) ^ p + (n + m * suc n) * suc (n + m * suc n) ^ p
--  ≡ (suc m ^ p + m * suc m ^ p) * (suc n ^ p + n * suc n ^ p)
    distr-*-+ (suc m ^ p) (m * suc m ^ p) (suc n ^ p + n * suc n ^ p)
--    suc (n + m * suc n) ^ p + (n + m * suc n) * suc (n + m * suc n) ^ p
--  ≡
--    suc m ^ p * (suc n ^ p + n * suc n ^ p)
--    + m * suc m ^ p * (suc n ^ p + n * suc n ^ p)
  | assoc-* m (suc m ^ p) (suc n ^ p + n * suc n ^ p)
--    suc (n + m * suc n) ^ p + (n + m * suc n) * suc (n + m * suc n) ^ p
--  ≡
--    suc m ^ p * (suc n ^ p + n * suc n ^ p)
--    + m * (suc m ^ p * (suc n ^ p + n * suc n ^ p))
  | distl-*-+ (suc m ^ p) (suc n ^ p) (n * suc n ^ p)
--    suc (n + m * suc n) ^ p + (n + m * suc n) * suc (n + m * suc n) ^ p
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | comm-* m (suc n)
--    suc (n + (m + n * m)) ^ p
--    + (n + (m + n * m)) * suc (n + (m + n * m)) ^ p
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | comm-* n m
--    suc (n + (m + m * n)) ^ p
--    + (n + (m + m * n)) * suc (n + (m + m * n)) ^ p
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | sym (suc-right-* m n)
--    suc (n + m * suc n) ^ p
--    + (n + m * suc n) * suc (n + m * suc n) ^ p
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | distr-^-* (suc m) (suc n) p
--    suc m ^ p * suc n ^ p + (n + m * suc n) * (suc m ^ p * suc n ^ p)
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | distr-*-+ n (m * suc n) (suc m ^ p * suc n ^ p)
--    suc m ^ p * suc n ^ p + (n * (suc m ^ p * suc n ^ p)
--    + m * suc n * (suc m ^ p * suc n ^ p))
--    ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + m * (suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p))
  | distl-*-+ m (suc m ^ p * suc n ^ p) (suc m ^ p * (n * suc n ^ p))
--    suc m ^ p * suc n ^ p + (n * (suc m ^ p * suc n ^ p)
--    + m * suc n * (suc m ^ p * suc n ^ p))
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + (m * (suc m ^ p * suc n ^ p) + m * (suc m ^ p * (n * suc n ^ p)))
  | comm-* m (suc n)
--    suc m ^ p * suc n ^ p + (n * (suc m ^ p * suc n ^ p)
--    + (m + n * m) * (suc m ^ p * suc n ^ p))
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p)
--    + (m * (suc m ^ p * suc n ^ p) + m * (suc m ^ p * (n * suc n ^ p)))
  | distr-*-+ m (n * m) (suc m ^ p * suc n ^ p)
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p) +
--    (m * (suc m ^ p * suc n ^ p) + m * (suc m ^ p * (n * suc n ^ p)))
  | swap-m-n-* n (suc m ^ p) (suc n ^ p)
--    suc m ^ p * suc n ^ p +
--    (suc m ^ p * (n * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--  ≡
--    suc m ^ p * suc n ^ p + suc m ^ p * (n * suc n ^ p) +
--    (m * (suc m ^ p * suc n ^ p) + m * (suc m ^ p * (n * suc n ^ p)))
  | swap-m-n-* (suc m ^ p) n (suc n ^ p)
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--  ≡
--    suc m ^ p * suc n ^ p + n * (suc m ^ p * suc n ^ p) +
--    (m * (suc m ^ p * suc n ^ p) + m * (n * (suc m ^ p * suc n ^ p)))
  | sym (assoc-* m n (suc m ^ p * suc n ^ p))
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--  ≡
--    suc m ^ p * suc n ^ p + n * (suc m ^ p * suc n ^ p) +
--    (m * (suc m ^ p * suc n ^ p) + m * n * (suc m ^ p * suc n ^ p))
  | comm-* m n
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--    ≡
--    suc m ^ p * suc n ^ p + n * (suc m ^ p * suc n ^ p) +
--    (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p))
  | assoc-+ (suc m ^ p * suc n ^ p) (n * (suc m ^ p * suc n ^ p))
    (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p))
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
--    ≡
--    suc m ^ p * suc n ^ p +
--    (n * (suc m ^ p * suc n ^ p) +
--     (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p)))
-- QED
  = refl

--distr-^-* (suc m) (suc n) (suc p)
--  rewrite
--    distr-*-+ (suc m ^ p) (m * suc m ^ p) (suc n ^ p + n * suc n ^ p)
--  | assoc-* m (suc m ^ p) (suc n ^ p + n * suc n ^ p)
--  | distl-*-+ (suc m ^ p) (suc n ^ p) (n * suc n ^ p)
--  | comm-* m (suc n)
--  | comm-* n m
--  | sym (suc-right-* m n)
--  | distr-^-* (suc m) (suc n) p
--  | distr-*-+ n (m * suc n) (suc m ^ p * suc n ^ p)
--  | distl-*-+ m (suc m ^ p * suc n ^ p) (suc m ^ p * (n * suc n ^ p))
--  | comm-* m (suc n)
--  | distr-*-+ m (n * m) (suc m ^ p * suc n ^ p)
--  | swap-m-n-* n (suc m ^ p) (suc n ^ p)
--  | swap-m-n-* (suc m ^ p) n (suc n ^ p)
--  | sym (assoc-* m n (suc m ^ p * suc n ^ p))
--  | comm-* m n
--  | assoc-+ (suc m ^ p * suc n ^ p) (n * (suc m ^ p * suc n ^ p))
--    (m * (suc m ^ p * suc n ^ p) + n * m * (suc m ^ p * suc n ^ p))
--  = refl

--------------------------------------- Relations ---------------------------------------

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n : ℕ} → zero ≤ n
  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

_ : 2 ≤ 4
_ = s≤s (s≤s z≤n)
--_ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))

inv-s≤s : ∀ {m n : ℕ} → suc m ≤ suc n → m ≤ n
inv-s≤s (s≤s m≤n) = m≤n

inv-z≤n : ∀ {m : ℕ} → m ≤ zero → m ≡ zero
inv-z≤n z≤n = refl

refl-≤ : ∀ {n : ℕ} → n ≤ n
refl-≤ {zero}  = z≤n
refl-≤ {suc o} = s≤s refl-≤

trans-≤ : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
trans-≤ z≤n       _         = z≤n
trans-≤ (s≤s m≤n) (s≤s n≤p) = s≤s (trans-≤ m≤n n≤p)

antisym-≤ : ∀ {m n : ℕ} → m ≤ n → n ≤ m → m ≡ n
antisym-≤ z≤n       n≤m       = sym (inv-z≤n n≤m)
antisym-≤ (s≤s m≤n) (s≤s n≤m) = cong suc (antisym-≤ m≤n n≤m)

open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)

--data Total (m n : ℕ) : Set where
--  forward : m ≤ n → Total m n
--  flipped : n ≤ m → Total m n
--
--total-≤ : ∀ (m n : ℕ) → Total m n
--total-≤ zero    _    = forward z≤n
--total-≤ (suc m) zero = flipped z≤n
--total-≤ (suc m) (suc n) with total-≤ m n
--...                     | forward m≤n = forward (s≤s m≤n)
--...                     | flipped n≤m = flipped (s≤s n≤m)

total-≤` : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m
total-≤` zero    _       = inj₁ z≤n
total-≤` _       zero    = inj₂ z≤n
total-≤` (suc m) (suc n) with total-≤` m n
...                      | inj₁ m≤n = inj₁ (s≤s m≤n)
...                      | inj₂ n≤m = inj₂ (s≤s n≤m)

--+-monoʳ-≤ : ∀ (n p q : ℕ) → p ≤ q → (n + p) ≤ (n + q)
--+-monoʳ-≤ zero    _ _ p≤q = p≤q
--+-monoʳ-≤ (suc n) p q p≤q = s≤s (+-monoʳ-≤ n p q p≤q)

+-monoʳ-≤ : ∀ {n p q : ℕ} → p ≤ q → (n + p) ≤ (n + q)
+-monoʳ-≤ {zero}  p≤q = p≤q
+-monoʳ-≤ {suc n} p≤q = s≤s (+-monoʳ-≤ {n} p≤q)

+-monoˡ-≤ : ∀ {m n p : ℕ} → m ≤ n → (m + p) ≤ (n + p)
+-monoˡ-≤ {m} {n} {p} m≤n rewrite comm-+ m p | comm-+ n p = +-monoʳ-≤ m≤n

-- From book
≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
≤-trans z≤n       _          =  z≤n
≤-trans (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans m≤n n≤p)

+-mono-≤ : ∀ {m n p q : ℕ} → m ≤ n → p ≤ q → (m + p) ≤ (n + q)
+-mono-≤ m≤n p≤q = ≤-trans (+-monoˡ-≤ m≤n) (+-monoʳ-≤ p≤q)

-- Exercises
*-monoʳ-≤ : ∀ {n p q : ℕ} → p ≤ q → (n * p) ≤ (n * q)
*-monoʳ-≤ {zero}  p≤q = z≤n
*-monoʳ-≤ {suc n} p≤q = +-mono-≤ p≤q (*-monoʳ-≤ {n} p≤q)

*-monoˡ-≤ : ∀ {m n p : ℕ} → m ≤ n → (m * p) ≤ (n * p)
*-monoˡ-≤ {m} {n} {p} m≤n rewrite comm-* m p | comm-* n p = *-monoʳ-≤ {p} {m} {n} m≤n

*-mono-≤ : ∀ {m n p q : ℕ} → m ≤ n → p ≤ q → (m * p) ≤ (n * q)
*-mono-≤ {_} {n} m≤n p≤q = ≤-trans (*-monoˡ-≤ m≤n) (*-monoʳ-≤ {n} p≤q)

infix 4 _<_

data _<_ : ℕ → ℕ → Set where
  z<s : ∀ {n : ℕ} → zero < suc n
  s<s : ∀ {m n : ℕ} → m < n → suc m < suc n

<-trans : ∀ {m n p} → m < n → n < p → m < p
--<-trans {m} {suc n} {suc p} z<s (s<s n<p) = z<s {p}
--<-trans {suc m} {suc n} {suc p} (s<s m<n) (s<s n<p) = s<s (<-trans m<n n<p)
<-trans z<s       (s<s n<p) = z<s
<-trans (s<s m<n) (s<s n<p) = s<s (<-trans m<n n<p)

trichotomy : ∀ (m n) → (m ≡ n) ⊎ (m < n) ⊎ (n < m)
trichotomy zero    zero    = inj₁ refl
trichotomy zero    (suc n) = inj₂ (inj₁ z<s)
trichotomy (suc m) zero    = inj₂ (inj₂ z<s)
trichotomy (suc m) (suc n) with trichotomy m n
...                       | inj₁ m≡n        = inj₁ (cong suc m≡n)
...                       | inj₂ (inj₁ m<n) = inj₂ (inj₁ (s<s m<n))
...                       | inj₂ (inj₂ n<m) = inj₂ (inj₂ (s<s n<m))

+-monoʳ-< : ∀ {n p q} → p < q → (n + p) < (n + q)
+-monoʳ-< {zero}  p<q = p<q
+-monoʳ-< {suc n} p<q = s<s (+-monoʳ-< p<q)

+-monoˡ-< : ∀ {m n p} → m < n → (m + p) < (n + p)
+-monoˡ-< {m} {n} {p} m<n rewrite comm-+ m p | comm-+ n p = +-monoʳ-< m<n

+-mono-< : ∀ {m n p q} → m < n → p < q → (m + p) < (n + q)
+-mono-< m<n p<q = <-trans (+-monoˡ-< m<n) (+-monoʳ-< p<q)

-- From Software Verification Class (nice exercises but the two first are
-- unnecessary in Agda because the proofs are basically the relation
-- definition)
≡0 : ∀ {n : ℕ} → ¬( 0 < n ) → n ≡ 0
≡0 {zero}  _    = refl
≡0 {suc n} ¬0<n = ⊥-elim (¬0<n z<s)

--0< : ∀ {n : ℕ} → n ≢ 0 → 0 < n
0< : ∀ {n : ℕ} → ¬( n ≡ 0 ) → 0 < n
0< {zero} 0≢0 = ⊥-elim (0≢0 refl)
0< {suc n} s≢0 = z<s

¬n<z : ∀ {n : ℕ} → ¬( n < 0 )
¬n<z ()

m<sn→m<n⊎m≡n : {m n : ℕ} → (m < suc n) → (m < n) ⊎ (m ≡ n)
m<sn→m<n⊎m≡n {zero}  {zero}  _ = inj₂ refl
m<sn→m<n⊎m≡n {zero}  {suc n} _ = inj₁ z<s
m<sn→m<n⊎m≡n {suc m} {zero}  (s<s ())
m<sn→m<n⊎m≡n {suc m} {suc n} (s<s m<sn) with m<sn→m<n⊎m≡n {m} {n} m<sn
...                 | inj₁ m<n = inj₁ (s<s m<n)
...                 | inj₂ m≡n = inj₂ (cong suc m≡n)

suc-step : {m n : ℕ} → (m < suc n) × (m ≢ n) → m < n
suc-step {zero}  {zero}  ⟨ 0<1      , 0≢0   ⟩ = 0< 0≢0
suc-step {zero}  {suc n} ⟨ 0<ssn    , 0≢sn  ⟩ = z<s
suc-step {suc m} {zero}  ⟨ s<s m<0  , sm≢0  ⟩ = ⊥-elim (¬n<z m<0)
suc-step {suc m} {suc n} ⟨ s<s m<sn , sm≢sn ⟩ with m<sn→m<n⊎m≡n m<sn
...                 | inj₁ m<n = s<s m<n
...                 | inj₂ m≡n = ⊥-elim (sm≢sn (cong suc m≡n))

-- This idea of using returning ∃ in Athena might be fundamental but it is
-- clumsy or cumbersome in Agda
discrete : ∀ {n : ℕ} → ¬ (∃[ m ] (n < m × m < suc n))
discrete {zero}  ⟨ _     , ⟨ z<s , s<s () ⟩ ⟩
discrete {suc n} ⟨ zero  , ⟨ ()  , _      ⟩ ⟩
discrete {suc n} ⟨ suc m , ⟨ s<s n<m , s<s m<sn ⟩ ⟩ = discrete ⟨ m , ⟨ n<m , m<sn ⟩ ⟩

-- This is unnecessary because it is the same as pred n
-- proj₁ (S4 {_} {n} _) ≡ pred n
--S4 : ∀ {m n : ℕ} → suc m < n → ∃[ n' ] ( n ≡ suc n' )
S4 : ∀ {m n : ℕ} → m < n → ∃[ n' ] ( n ≡ suc n' )
S4 {_} {zero} ()
S4 {_} {suc n} _ = ⟨ n , refl ⟩

-- more interesting is:
S4' : ∀ {m n : ℕ} → suc m ≤ n → ∃[ n' ] ( n ≡ suc n' )
S4' {_} {zero} ()
S4' {_} {suc n} _ = ⟨ n , refl ⟩
-- It is more interesting because, this is not true:
-- S4' : ∀ {m n : ℕ} → m ≤ n → ∃[ n' ] ( n ≡ suc n' )
-- as opposed to S4.
-- But still, it's something that isn't necessary in Agda

irreflexive : ∀ {m : ℕ} → ¬(m < m)
irreflexive {zero} ()
irreflexive {suc m} (s<s m<m) = irreflexive m<m

trichotomy₂ : ∀ (m n) → (m ≡ n × ¬(m < n) × ¬(n < m))
                      ⊎ (m < n ×   m ≢ n  × ¬(n < m))
                      ⊎ (n < m ×   m ≢ n  × ¬(m < n))
trichotomy₂ zero    zero    = inj₁ ⟨ refl , ⟨ irreflexive , irreflexive ⟩ ⟩
trichotomy₂ zero    (suc n) = inj₂ (inj₁ ⟨ z<s , ⟨ (λ()) , (λ()) ⟩ ⟩)
trichotomy₂ (suc m) zero    = inj₂ (inj₂ ⟨ z<s , ⟨ (λ()) , (λ()) ⟩ ⟩)
trichotomy₂ (suc m) (suc n) with trichotomy₂ m n
...                       | inj₁ ⟨ m≡n , ⟨ ¬m<n , ¬n<m ⟩ ⟩ =
      inj₁ ⟨ cong suc m≡n , ⟨ (λ{(s<s m<n) → ¬m<n m<n}) , (λ{(s<s n<m) → ¬n<m n<m}) ⟩ ⟩
...                       | inj₂ (inj₁ ⟨ m<n , ⟨ m≢n , ¬n<m ⟩ ⟩) =
      inj₂ (inj₁ ⟨ s<s m<n , ⟨ (λ{sm≡sn → m≢n (cong pred sm≡sn)}) , (λ{(s<s n<m) → ¬n<m n<m}) ⟩ ⟩)
...                       | inj₂ (inj₂ ⟨ n<m , ⟨ m≢n , ¬m<n ⟩ ⟩) =
      inj₂ (inj₂ ⟨ s<s n<m , ⟨ (λ{sm≡sn → m≢n (cong pred sm≡sn)}) , (λ{(s<s m<n) → ¬m<n m<n}) ⟩ ⟩)

--open import Function.Equivalence using (_⇔_)
record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A

open _⇔_

<-if-≤ : ∀ {m n} → suc m ≤ n → m < n
<-if-≤ {zero}  {suc n} z≤s        = z<s
<-if-≤ {suc m} {suc n} (s≤s sm≤n) = s<s (<-if-≤ sm≤n)

≤-if-< : ∀ {m n} → m < n → suc m ≤ n
≤-if-< {zero} {suc n} z<s = s≤s z≤n
≤-if-< {suc m} {suc n} (s<s m<n) = s≤s (≤-if-< m<n)

≤-iff-< : ∀ {m n} → (suc m ≤ n) ⇔ (m < n)
≤-iff-< = record
  { to   = <-if-≤
  ; from = ≤-if-<
  }

pred-smaller : ∀ {m n} → suc m ≤ n → m ≤ n
pred-smaller {zero}          _          = z≤n
pred-smaller {suc m} {suc n} (s≤s sm≤n) = s≤s (pred-smaller sm≤n)

<-trans-revisited : ∀ {m n p} → m < n → n < p → m < p
<-trans-revisited {m} {n} {p} m<n n<p
  = <-if-≤ (≤-trans (≤-if-< m<n) (pred-smaller (≤-if-< n<p)))

---

data even : ℕ → Set
data odd  : ℕ → Set

data even where
  zero-e : even zero
  suc-e  : ∀ {n : ℕ} → odd n → even (suc n)

data odd where
  suc-o : ∀ {n : ℕ} → even n → odd (suc n)

---

data Can : Bin → Set
data One : Bin → Set

data Can where
  zero-C : Can (⟨⟩ O)
  one-C : ∀ {b : Bin} → One b → Can b

data One where
  oneO : One (⟨⟩ I)
  oneO-O : ∀ {b : Bin} → One b → One (b O)
  oneO-I : ∀ {b : Bin} → One b → One (b I)

_ : Can (⟨⟩ I)
_ = one-C oneO

inc-Bin : ∀ {b : Bin} → One b → One (inc b)
inc-Bin oneO        = oneO-O oneO
inc-Bin (oneO-O ob) = oneO-I ob
inc-Bin (oneO-I ob) = oneO-O (inc-Bin ob)

inc-Can : ∀ {b : Bin} → Can b → Can (inc b)
inc-Can zero-C     = one-C oneO
inc-Can (one-C ob) = one-C (inc-Bin ob)

to-Can : ∀ (n : ℕ) → Can (toᵇ n)
to-Can zero = zero-C
to-Can (suc n) = inc-Can (to-Can n)

twicebinisO : ∀ {b : Bin} → One b → b +ᵇ b ≡ b O
twicebinisO {⟨⟩ I} _ = refl
twicebinisO {b O} (oneO-O ob) rewrite twicebinisO ob = refl
twicebinisO {b I} (oneO-I ob) rewrite twicebinisO ob = refl

to∘from-Can : ∀ {b : Bin} → Can b → toᵇ (fromᵇ b) ≡ b
to∘from-Can zero-C = refl
to∘from-Can (one-C oneO) = refl
to∘from-Can {b O} (one-C (oneO-O ob))
  rewrite monobin (fromᵇ b)
        | to∘from-Can (one-C ob)
        | twicebinisO ob = refl
to∘from-Can {b I} (one-C (oneO-I ob))
  rewrite monobin (fromᵇ b)
        | to∘from-Can (one-C ob)
        | twicebinisO ob = refl

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

module ≤-Reasoning where
  infix  1 begin≤_
  infixr 2 _≤⟨⟩_ _≤⟨_⟩_
  infix  3 _∎≤

  begin≤_ : ∀ {x y : ℕ} → x ≤ y → x ≤ y
  begin≤ x≤y = x≤y

  _≤⟨⟩_ : ∀ (x : ℕ) {y : ℕ} → x ≤ y → x ≤ y
  x ≤⟨⟩ x≤y = x≤y

  _≤⟨_⟩_ : ∀ (x : ℕ) {y z : ℕ} → x ≤ y → y ≤ z → x ≤ z
  x ≤⟨ x≤y ⟩ y≤z = trans-≤ x≤y y≤z

  _∎≤ : ∀ (x : ℕ) → x ≤ x
  x ∎≤ = refl-≤

open ≤-Reasoning

+-monoʳ-≤` : ∀ {n p q : ℕ} → p ≤ q → (n + p) ≤ (n + q)
+-monoʳ-≤` {zero} p≤q = p≤q
+-monoʳ-≤` {suc n} {p} {q} p≤q =
  begin≤
    suc n + p
  ≤⟨⟩
    suc (n + p)
  ≤⟨ s≤s (+-monoʳ-≤` p≤q) ⟩
    suc (n + q)
  ≤⟨⟩
    suc n + q
  ∎≤

pred≡ : ∀ {m n : ℕ} → suc m ≡ suc n → m ≡ n
pred≡ = cong pred

≡to≤ : ∀ {m n : ℕ} → m ≡ n → m ≤ n
≡to≤ {zero}  {zero}  _     = refl-≤
≡to≤ {suc m} {suc n} sm≡sn = s≤s (≡to≤ (cong pred sm≡sn))

+-monoˡ-≤` : ∀ {m n p : ℕ} → m ≤ n → (m + p) ≤ (n + p)
+-monoˡ-≤` {m} {n} {p} m≤n =
  begin≤
    m + p
  ≤⟨ ≡to≤ (comm-+ m p) ⟩
    p + m
  ≤⟨ +-monoʳ-≤` {p} {m} {n} m≤n ⟩
    p + n
  ≤⟨ ≡to≤ (comm-+ p n) ⟩
    n + p
  ∎≤

+-mono-≤` : ∀ {m n p q : ℕ} → m ≤ n → p ≤ q → (m + p) ≤ (n + q)
+-mono-≤` {m} {n} {p} {q} m≤n p≤q =
  begin≤
    m + p
  ≤⟨ +-monoˡ-≤` m≤n ⟩
    n + p
  ≤⟨ +-monoʳ-≤` p≤q ⟩
    n + q
  ∎≤

--even-comm′ : ∀ (m n : ℕ)
--  → even (m + n)
--    ------------
--  → even (n + m)
--even-comm′ m n ev with   m + n  | comm-+ m n
--...                  | .(n + m) | refl       = ev

--------------------------------------- Isomorphism ---------------------------------------

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

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

same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
same-app m n rewrite comm-+ m n = helper m n
  where
    helper : ∀ (m n : ℕ) → m +′ n ≡ n + m
    helper _ zero    = refl
    helper m (suc n) = cong suc (helper m n)

same-+-+′ : _+′_ ≡ _+_
same-+-+′ = extensionality (λ m → extensionality (λ n → same-app m n))

--open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)
--
--private
--  variable
--    ℓ ℓ₁ : Level

--infix 0 _≃_
--record _≃_ (A : Set ℓ) (B : Set ℓ₁) : Set (ℓ ⊔ ℓ₁) where
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

≃-refl : ∀ {A : Set} → A ≃ A
≃-refl =
  record
    { to      = λ x → x
    ; from    = λ y → y
    ; from∘to = λ x → refl
    ; to∘from = λ y → refl
    }

≃-sym : ∀ {A B : Set} → A ≃ B → B ≃ A
≃-sym A≃B =
  record
    { to      = from A≃B
    ; from    = to A≃B
    ; from∘to = to∘from A≃B
    ; to∘from = from∘to A≃B
    }

open import Function.Base using (_∘_)

≃-trans : ∀ {A B C : Set} → A ≃ B → B ≃ C → A ≃ C
≃-trans A≃B B≃C =
  record
    { to      = to B≃C ∘ to A≃B
    ; from    = from A≃B ∘ from B≃C
    ; from∘to = λ{x →
        begin
          from A≃B (from B≃C (to B≃C (to A≃B x)))
        ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
          from A≃B (to A≃B x)
        ≡⟨ from∘to A≃B x ⟩
          x
        ∎
      }
    ; to∘from = λ{y →
        begin
          to B≃C (to A≃B (from A≃B (from B≃C y)))
        ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C y)) ⟩
          to B≃C (from B≃C y)
        ≡⟨ to∘from B≃C y ⟩
          y
        ∎
      }
    }

infix 0 _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

≃-implies-≲ : ∀ {A B : Set} → A ≃ B → A ≲ B
≃-implies-≲ A≃B =
  record
  { to   = to A≃B
  ; from = from A≃B
  ; from∘to = from∘to A≃B
  }

-- Idea: Prove that (ℕ) is isomorph to (Can)
-- Idea: Prove that (+, ℕ) is isomorph to (+ᵇ, Can)
--record _⇔_ (A B : Set) : Set where
--  field
--    to   : A → B
--    from : B → A

-- Exercise: implement reflexive, symetric and transitive properties on _⇔_

ℕ≲Bin : ℕ ≲ Bin
ℕ≲Bin =
  record
  { to   = toᵇ
  ; from = fromᵇ
  ; from∘to = from∘toᵇ
  }

data Dec-Can : Set where
  num : ∀ (b : Bin) → Can b → Dec-Can

toᵈᶜ : ℕ → Dec-Can
toᵈᶜ n = num (toᵇ n) (to-Can n)
--toᵈᶜ n = num (to-Can n)

fromᵈᶜ : Dec-Can → ℕ
fromᵈᶜ (num b _) = fromᵇ b

--from∘toᵈᶜ (suc n) = ?
-- λ n → fromᵈᶜ (toᵈᶜ (suc n)) ≡ suc n
-- λ cb → toᵈᶜ (fromᵈᶜ (num cb)) ≡ num cb
-- λ b ob → toᵈᶜ (fromᵈᶜ (num (b O) (one-C (oneO-O ob))))

--to∘fromᵈᶜ : ∀ (y : Dec-Can) → toᵈᶜ (fromᵈᶜ y) ≡ y
--to∘fromᵈᶜ (num (⟨⟩ O) zero-C)       = refl
--to∘fromᵈᶜ (num (⟨⟩ I) (one-C oneO)) = refl
--to∘fromᵈᶜ (num (b O) (one-C (oneO-O {b} ob))) rewrite monobin (fromᵇ b) = ?
---- λ b ob → toᵈᶜ (fromᵈᶜ (num (b O) (one-C (oneO-O ob))))
---- λ b ob → λ b ob → num (toᵇ (fromᵇ b + fromᵇ b)) (to-Can (fromᵇ b + fromᵇ b))
--to∘fromᵈᶜ = ?
----to∘fromᵈᶜ (num b cb) =
----  begin
----    toᵈᶜ (fromᵈᶜ (num b cb))
----  ≡⟨⟩
----    toᵈᶜ (fromᵇ b)
----  ≡⟨⟩
----    num (toᵇ (fromᵇ b)) (to-Can (fromᵇ b))
----  ≡⟨ ? ⟩
----    num b cb
----  ∎

--ℕ≃Can : ℕ ≃ Dec-Can
--ℕ≃Can =
--  record
--  { to      = toᵈᶜ
--  ; from    = fromᵈᶜ
--  ; from∘to = from∘toᵇ
--  ; to∘from = ? -- to∘fromᵈᶜ -- to∘from-Can
--  }

--num (zero-C)

--------------------------------------- Decidable ---------------------------------------
-- Use `Dec` to create elements for `Can`. Look if this is enough to prove `ℕ ≃ Can`
-- Ans: NO. Decidables don't do what you thought they do

--------------------------------------- Last ---------------------------------------
-- Prove that `sqrt 2` is irrational

-- Stuff to take into account and add to agda neovim:
-- IOTCM "plfa/part1/Naturals.agda" None Direct (Cmd_load "plfa/part1/Naturals.agda" [])
-- IOTCM "plfa/part1/Naturals.agda" None Direct (Cmd_compute_toplevel DefaultCompute "2 + suc 3") # Already done by plugin
-- IOTCM "plfa/part1/Naturals.agda" None Direct (Cmd_infer_toplevel AsIs "2 + suc 3")  # THIS SHOULD BE PART OF THE STUFF IN MAGDA
--
-- Other stuff:
-- IOTCM "plfa/part1/Naturals.agda" None Direct (Cmd_show_module_contents_toplevel AsIs "Eq")
-- IOTCM "plfa/part1/Naturals.agda" None Direct (Cmd_why_in_scope_toplevel "Eq")
-- IOTCM "plfa/part1/Naturals.agda" None Direct (Cmd_why_in_scope (InteractionId 1) (Range (Just "plfa/part1/Naturals.agda") (Interval (Pn () 1 76 1) (Pn () 1 76 19))) "Eq")
---- IOTCM "plfa/part1/Naturals.agda" None Direct (Cmd_autoOne (InteractionId 1) noRange "")
---- IOTCM "plfa/part1/Naturals.agda" NonInteractive Indirect (Cmd_infer Simplified 103992 (intervalsToRange (Just (mkAbsolute "plfa/part1/Naturals.agda")) [Interval (Pn () 50 75 1) (Pn () 52 79 1)]) "3 + suc 2")


text:
module Impure.STLCRef.Properties.Soundness where

open import Data.Nat
open import Data.Sum
open import Data.Product as Pr
open import Data.List
open import Data.Vec hiding (_∷ʳ_)
open import Data.Star
open import Function
open import Extensions.List

open import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.Core using (REL; Reflexive)
open import Relation.Binary.List.Pointwise as PRel hiding (refl)

open import Impure.STLCRef.Syntax hiding (id)
open import Impure.STLCRef.Welltyped
open import Impure.STLCRef.Eval

ref-value-lemma : ∀ {n A Γ Σ} {e : Exp n} → Γ , Σ ⊢ e ∶ Ref A → Val e → ∃ λ i → e ≡ (loc i)
ref-value-lemma (var x) ()
ref-value-lemma (loc p) (loc i) = i , refl
ref-value-lemma (p · p₁) ()
ref-value-lemma (ref p) ()
ref-value-lemma (! p) ()

progress : ∀ {Γ Σ A} {e : Exp 0} {μ} →
           Γ , Σ ⊢ μ →
           Γ , Σ ⊢ e ∶ A →
           --------------------------------------
           Val e ⊎ ∃₂ λ e' μ' → (e , μ ≻ e' , μ')

progress p unit = inj₁ unit
progress p (var ())

progress p (loc {i = i} q) = inj₁ (loc i)

progress p (ƛ wt) = inj₁ (ƛ _ _)

progress p (f · e) with progress p f
progress p (() · e) | inj₁ unit
progress p (() · e) | inj₁ (loc i)
progress p (ƛ f · e) | inj₁ (ƛ _ _) = inj₂ (_ , (_ , AppAbs))
progress p (f · e) | inj₂ (_ , _ , f≻f') = inj₂ (_ , (_ , (Appₗ f≻f')))

progress p (ref wt) with progress p wt
progress p (ref wt) | inj₁ v = inj₂ (_ , (_ , (RefVal v)))
progress p (ref wt) | inj₂ (_ , _ , wt≻wt') = inj₂ (_ , _ , Ref wt≻wt')

progress p (! wt) with progress p wt
progress p (! wt) | inj₁ v with ref-value-lemma wt v
progress p (! loc q) | inj₁ (loc .i) | (i , refl) =
  inj₂ (_ , (_ , (DerefLoc (P.subst (_<_ _) (pointwise-length p) ([]=-length q)))))
progress p (! wt) | inj₂ (_ , _ , wt≻wt') = inj₂ (_ , (_ , (Deref wt≻wt')))

progress p (wt ≔ x) with progress p wt | progress p x
progress p (wt ≔ x) | _ | inj₂ (_ , _ , x≻x') = inj₂ (_ , (_ , (Assign₂ x≻x')))
progress p (wt ≔ x) | inj₂ (_ , _ , wt≻wt') | _ = inj₂ (_ , _ , Assign₁ wt≻wt')
progress p (wt ≔ x) | inj₁ v | inj₁ w with ref-value-lemma wt v
progress p (loc q ≔ x) | inj₁ (loc .i) | inj₁ w | (i , refl) =
  inj₂ (_ , (_ , Assign (P.subst (_<_ _) (pointwise-length p) ([]=-length q)) w))

postulate
  sub-preserves : ∀ {n Γ Σ A B x} {e : Exp (suc n)} →
    (B ∷ Γ) , Σ ⊢ e ∶ A →
    Γ , Σ ⊢ x ∶ B →
    Γ , Σ ⊢ (e / sub x) ∶ A

!!-loc : ∀ {n Σ Σ' A μ i} {Γ : Ctx n} →
         Rel (λ A x → Γ , Σ ⊢ proj₁ x ∶ A) Σ' μ →
         Σ' ⊢loc i ∶ A → (l : i < length μ) → Γ , Σ ⊢ proj₁ (μ !! l) ∶ A
!!-loc [] ()
!!-loc (x∼y ∷ p) here (s≤s z≤n) = x∼y
!!-loc (x∼y ∷ p) (there q) (s≤s l) = !!-loc p q l

-- extending the store preserves expression typings
⊒-preserves : ∀ {n Γ Σ Σ' A} {e : Exp n} → Σ' ⊒ Σ → Γ , Σ ⊢ e ∶ A → Γ , Σ' ⊢ e ∶ A
⊒-preserves ext unit = unit
⊒-preserves ext (var x) = var x
⊒-preserves ext (loc x) = loc (xs⊒ys[i] x ext)
⊒-preserves ext (ƛ p) = ƛ (⊒-preserves ext p)
⊒-preserves ext (p · q) = (⊒-preserves ext p) · ⊒-preserves ext q
⊒-preserves ext (ref p) = ref (⊒-preserves ext p)
⊒-preserves ext (! p) = ! (⊒-preserves ext p)
⊒-preserves ext (p ≔ q) = (⊒-preserves ext p) ≔ (⊒-preserves ext q)

≻-preserves : ∀ {n Γ Σ A} {e : Exp n} {e' μ' μ} →
              Γ , Σ ⊢ e ∶ A →
              Γ , Σ ⊢ μ → e , μ ≻ e' , μ' →
              ---------------------------------
              ∃ λ Σ' → Γ , Σ' ⊢ e' ∶ A × Σ' ⊒ Σ × Γ , Σ' ⊢ μ'

≻-preserves unit p ()
≻-preserves (var x) p ()
≻-preserves (loc p) p₁ ()
≻-preserves (ƛ wt) p ()

≻-preserves {Σ = Σ} (ƛ wt · wt₁) p AppAbs = Σ , sub-preserves wt wt₁ , ⊑-refl , p
≻-preserves {Σ = Σ} (ref {x = x} {A} wt) p (RefVal v) = let ext = ∷ʳ-⊒ A Σ in
  Σ ∷ʳ A ,
    loc (P.subst (λ i → _ ⊢loc i ∶ _) (pointwise-length p) (∷ʳ[length] Σ A)) ,
    ext ,
    pointwise-∷ʳ (PRel.map (⊒-preserves ext) p) (⊒-preserves ext wt)
≻-preserves {Σ = Σ₁} (! loc x) p (DerefLoc l) =
  Σ₁ , !!-loc p x l , ⊑-refl , p
≻-preserves {Σ = Σ₁} (loc x ≔ y) p (Assign l v) =
  Σ₁ , unit , ⊑-refl , pointwise-[]≔ p x l y

-- contextual closure
≻-preserves {Σ = Σ} (wt-f · wt-x) p (Appₗ r) =
  Pr.map
    id
    (λ{ (wt-f' , ext , q) → wt-f' · ⊒-preserves ext wt-x , ext , q})
    (≻-preserves wt-f p r)
≻-preserves (f · x) p (Appᵣ r) =
  Pr.map
    id
    (λ{ (x' , ext , q) → ⊒-preserves ext f · x' , ext , q})
    (≻-preserves x p r)
≻-preserves (ref wt) p (Ref r) = Pr.map id (λ{ (wt' , ext) → ref wt' , ext}) (≻-preserves wt p r)
≻-preserves (! wt) p (Deref r) = Pr.map id (λ{ (wt' , ext) → ! wt' , ext}) (≻-preserves wt p r)
≻-preserves (y ≔ x) p (Assign₁ r) =
  Pr.map
    id
    (λ{ (y' , ext , q) → y' ≔ ⊒-preserves ext x , ext , q})
    (≻-preserves y p r)
≻-preserves (y ≔ x) p (Assign₂ r) =
  Pr.map
    id
    (λ{ (x' , ext , q) → ⊒-preserves ext y ≔ x' , ext , q})
    (≻-preserves x p r)

-- preservation for multistep reductions
preservation : ∀ {n} {e : Exp n} {Γ Σ A μ μ' e'} →
                Γ , Σ ⊢ e ∶ A →
                Γ , Σ ⊢ μ →
                e , μ ≻* e' , μ' →
                -----------------------------------------------
                ∃ λ Σ' → Γ , Σ' ⊢ e' ∶ A × Σ' ⊒ Σ × Γ , Σ' ⊢ μ'
preservation wt ok ε = _ , wt , ⊑-refl , ok
preservation wt ok (x ◅ r) with ≻-preserves wt ok x
... | Σ₂ , wt' , Σ₂⊒Σ , μ₂ok with preservation wt' μ₂ok r
... | Σ₃ , wt'' , Σ₃⊒Σ₂ , μ₃ = Σ₃ , wt'' , ⊑-trans Σ₂⊒Σ Σ₃⊒Σ₂ , μ₃

-- fueled evaluation
open import Data.Maybe
eval : ∀ {e : Exp zero} {Σ A μ} ℕ →
         [] , Σ ⊢ e ∶ A →
         [] , Σ ⊢ μ →
         ---------------------------------------
         Maybe (∃ λ Σ' → ∃ λ e' → ∃ λ μ' →
            (e , μ ≻* e' , μ') × Val e' × ([] , Σ' ⊢ e' ∶ A))
eval 0 _ _ = nothing
eval (suc n) p q with progress q p
eval (suc n) p q | inj₁ x = just (_ , _ , _ , ε , x , p)
eval (suc n) p q | inj₂ (e' , μ' , step) with ≻-preserves p q step
... | (Σ₂ , wte' , ext , μ'-ok) with eval n wte' μ'-ok
... | nothing = nothing
... | just (Σ₃ , e'' , μ'' , steps , v , wte'') = just (Σ₃ , e'' , μ'' , step ◅ steps , v , wte'')


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

module Categories.Adjoint.Alternatives where

open import Level

open import Categories.Adjoint
open import Categories.Category
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation

import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D   : Category o ℓ e

  module _ (L : Functor C D) (R : Functor D C) where
    private
      module C = Category C
      module D = Category D
      module L = Functor L
      module R = Functor R

    record FromUnit : Set (levelOfTerm L ⊔ levelOfTerm R) where

      field
        unit : NaturalTransformation idF (R ∘F L)

      module unit = NaturalTransformation unit

      field
        θ       : ∀ {X Y} → C [ X , R.₀ Y ] → D [ L.₀ X , Y ]
        commute : ∀ {X Y} (g : C [ X , R.₀ Y ]) → g C.≈ R.₁ (θ g) C.∘ unit.η X
        unique  : ∀ {X Y} {f : D [ L.₀ X , Y ]} {g : C [ X , R.₀ Y ]} →
                    g C.≈ R.₁ f C.∘ unit.η X → θ g D.≈ f

      module _ where
        open C.HomReasoning
        open MR C

        θ-natural : ∀ {X Y Z} (f : D [ Y , Z ]) (g : C [ X , R.₀ Y ]) → θ (R.₁ f C.∘ g) D.≈ θ (R.₁ f) D.∘ L.₁ g
        θ-natural {X} {Y} f g = unique eq
          where eq : R.₁ f C.∘ g C.≈ R.₁ (θ (R.₁ f) D.∘ L.₁ g) C.∘ unit.η X
                eq = begin
                  R.₁ f C.∘ g                                      ≈⟨ commute (R.₁ f) ⟩∘⟨refl ⟩
                  (R.₁ (θ (R.₁ f)) C.∘ unit.η (R.F₀ Y)) C.∘ g    ≈⟨ C.assoc ⟩
                  R.₁ (θ (R.₁ f)) C.∘ unit.η (R.₀ Y) C.∘ g       ≈⟨ pushʳ (unit.commute g) ⟩
                  (R.₁ (θ (R.₁ f)) C.∘ R.₁ (L.₁ g)) C.∘ unit.η X ≈˘⟨ R.homomorphism ⟩∘⟨refl ⟩
                  R.₁ (θ (R.₁ f) D.∘ L.₁ g) C.∘ unit.η X         ∎

        θ-cong : ∀ {X Y} {f g : C [ X , R.₀ Y ]} → f C.≈ g → θ f D.≈ θ g
        θ-cong eq = unique (eq ○ commute _)

      θ-natural′ : ∀ {X Y} (g : C [ X , R.₀ Y ]) → θ g D.≈ θ C.id D.∘ L.₁ g
      θ-natural′ g = θ-cong (introˡ R.identity) ○ θ-natural D.id g ○ D.∘-resp-≈ˡ (θ-cong R.identity)
        where open D.HomReasoning
              open MR C

      counit : NaturalTransformation (L ∘F R) idF
      counit = ntHelper record
        { η       = λ d → θ C.id
        ; commute = λ f → begin
          θ C.id D.∘ L.₁ (R.₁ f) ≈˘⟨ θ-natural′ (R.₁ f) ⟩
          θ (R.₁ f)              ≈⟨ unique (CH.⟺ (MR.cancelʳ C (CH.⟺ (commute C.id))) CH.○ CH.⟺ (C.∘-resp-≈ˡ R.homomorphism)) ⟩
          f D.∘ θ C.id           ∎
        }
        where open D.HomReasoning
              module CH = C.HomReasoning

      unique′ : ∀ {X Y} {f g : D [ L.₀ X , Y ]} (h : C [ X , R.₀ Y ]) →
                  h C.≈ R.₁ f C.∘ unit.η X →
                  h C.≈ R.₁ g C.∘ unit.η X → f D.≈ g
      unique′ _ eq₁ eq₂ = ⟺ (unique eq₁) ○ unique eq₂
        where open D.HomReasoning

      zig : ∀ {A} → θ C.id D.∘ L.F₁ (unit.η A) D.≈ D.id
      zig {A} = unique′ (unit.η A)
                        (commute (unit.η A) ○ (C.∘-resp-≈ˡ (R.F-resp-≈ (θ-natural′ (unit.η A)))))
                        (introˡ R.identity)
        where open C.HomReasoning
              open MR C

      L⊣R : L ⊣ R
      L⊣R = record
        { unit   = unit
        ; counit = counit
        ; zig    = zig
        ; zag    = C.Equiv.sym (commute C.id)
        }

    record FromCounit : Set (levelOfTerm L ⊔ levelOfTerm R) where

      field
        counit : NaturalTransformation (L ∘F R) idF

      module counit = NaturalTransformation counit

      field
        θ       : ∀ {X Y} → D [ L.₀ X , Y ] → C [ X , R.₀ Y ]
        commute : ∀ {X Y} (g : D [ L.₀ X , Y ]) → g D.≈ counit.η Y D.∘ L.₁ (θ g)
        unique  : ∀ {X Y} {f : C [ X , R.₀ Y ]} {g : D [ L.₀ X , Y ]} →
                    g D.≈ counit.η Y D.∘ L.₁ f → θ g C.≈ f

      module _ where
        open D.HomReasoning
        open MR D

        θ-natural : ∀ {X Y Z} (f : C [ X , Y ]) (g : D [ L.₀ Y , Z ]) → θ (g D.∘ L.₁ f) C.≈ R.₁ g C.∘ θ (L.₁ f)
        θ-natural {X} {Y} {Z} f g = unique eq
          where eq : g D.∘ L.₁ f D.≈ counit.η Z D.∘ L.₁ (R.₁ g C.∘ θ (L.₁ f))
                eq = begin
                  g D.∘ L.₁ f                                     ≈⟨ pushʳ (commute (L.₁ f)) ⟩
                  (g D.∘ counit.η (L.F₀ Y)) D.∘ L.F₁ (θ (L.F₁ f)) ≈⟨ pushˡ (counit.sym-commute g) ⟩
                  counit.η Z D.∘ L.₁ (R.₁ g) D.∘ L.₁ (θ (L.₁ f))  ≈˘⟨ refl⟩∘⟨ L.homomorphism ⟩
                  counit.η Z D.∘ L.₁ (R.₁ g C.∘ θ (L.₁ f))        ∎

        θ-cong : ∀ {X Y} {f g : D [ L.₀ X , Y ]} → f D.≈ g → θ f C.≈ θ g
        θ-cong eq = unique (eq ○ commute _)

      θ-natural′ : ∀ {X Y} (g : D [ L.₀ X , Y ]) → θ g C.≈ R.₁ g C.∘ θ D.id
      θ-natural′ g = θ-cong (introʳ L.identity) ○ θ-natural C.id g ○ C.∘-resp-≈ʳ (θ-cong L.identity)
        where open C.HomReasoning
              open MR D

      unit : NaturalTransformation idF (R ∘F L)
      unit = ntHelper record
        { η       = λ _ → θ D.id
        ; commute = λ f → begin
          θ D.id C.∘ f           ≈˘⟨ unique (DH.⟺ (cancelˡ (DH.⟺ (commute D.id))) DH.○ D.∘-resp-≈ʳ (DH.⟺ L.homomorphism)) ⟩
          θ (L.₁ f)              ≈⟨ θ-natural′ (L.₁ f) ⟩
          R.₁ (L.₁ f) C.∘ θ D.id ∎
        }
        where open C.HomReasoning
              module DH = D.HomReasoning
              open MR D

      unique′ : ∀ {X Y} {f g : C [ X , R.₀ Y ]} (h : D [ L.₀ X , Y ]) →
                  h D.≈ counit.η Y D.∘ L.₁ f →
                  h D.≈ counit.η Y D.∘ L.₁ g →
                  f C.≈ g
      unique′ _ eq₁ eq₂ = ⟺ (unique eq₁) ○ unique eq₂
        where open C.HomReasoning

      zag : ∀ {B} → R.F₁ (counit.η B) C.∘ θ D.id C.≈ C.id
      zag {B} = unique′ (counit.η B)
                        (⟺ (cancelʳ (⟺ (commute D.id))) ○ pushˡ (counit.sym-commute (counit.η B)) ○ D.∘-resp-≈ʳ (⟺ L.homomorphism))
                        (introʳ L.identity)
        where open D.HomReasoning
              open MR D

      L⊣R : L ⊣ R
      L⊣R = record
        { unit   = unit
        ; counit = counit
        ; zig    = D.Equiv.sym (commute D.id)
        ; zag    = zag
        }

module _ {L : Functor C D} {R : Functor D C} where

  fromUnit : FromUnit L R → L ⊣ R
  fromUnit = FromUnit.L⊣R

  fromCounit : FromCounit L R → L ⊣ R
  fromCounit = FromCounit.L⊣R

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Trying to define ≤ as a datatype in Prop doesn't work very well:

{-# OPTIONS --enable-prop #-}

open import Agda.Builtin.Nat

data _≤'_ : Nat → Nat → Prop where
  zero : (y : Nat) → zero ≤' y
  suc  : (x y : Nat) → x ≤' y → suc x ≤' suc y

≤'-ind : (P : (m n : Nat) → Set)
       → (pzy : (y : Nat) → P zero y)
       → (pss : (x y : Nat) → P x y → P (suc x) (suc y))
       → (m n : Nat) → m ≤' n → P m n
≤'-ind P pzy pss .0 y (zero .y) = ?
≤'-ind P pzy pss .(suc x) .(suc y) (suc x y pf) = ?

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
module Lookup where

data Bool : Set where
  false : Bool
  true  : Bool

data IsTrue : Bool -> Set where
  isTrue : IsTrue true

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

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

module Map
  (Key  : Set)
  (_==_ : Key -> Key -> Bool)
  (Code : Set)
  (Val  : Code -> Set) where

  infixr 40 _⟼_,_
  infix  20 _∈_

  data Map : List Code -> Set where
    ε     : Map []
    _⟼_,_ : forall {c cs} ->
            Key -> Val c -> Map cs -> Map (c :: cs)

  _∈_ : forall {cs} -> Key -> Map cs -> Bool
  k ∈ ε            = false
  k ∈ (k' ⟼ _ , m) with k == k'
  ...              | true  = true
  ...              | false = k ∈ m

  Lookup : forall {cs} -> (k : Key)(m : Map cs) -> IsTrue (k ∈ m) -> Set
  Lookup k ε ()
  Lookup k (_⟼_,_ {c} k' _ m) p with k == k'
  ... | true  = Val c
  ... | false = Lookup k m p

  lookup : {cs : List Code}(k : Key)(m : Map cs)(p : IsTrue (k ∈ m)) ->
           Lookup k m p
  lookup k ε ()
  lookup k (k' ⟼ v , m) p with k == k'
  ... | true  = v
  ... | false = lookup k m p

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2014-03-05, reported by xcycl.xoo, Mar 30, 2009
-- {-# OPTIONS -v tc.with:60 #-}

open import Common.Prelude renaming (Nat to ℕ; module Nat to ℕ)

data Nat : ℕ → Set where
  i : (k : ℕ) → Nat k

toNat : (n : ℕ) → Nat n
toNat n = i n

fun : (n : ℕ) → ℕ
fun n with toNat n
fun .m | i m with toNat m
fun .Set | i .l | i l = 0

-- 'Set' is ill-typed here and should trigger an error

FORCE_FAIL_HERE_UNTIL_ISSUE_142_IS_REALLY_FIXED


text:
id : Set → Set
id A = A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Correctness of differentiation with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Change.Correctness where

-- The denotational properties of the `derive` transformation
-- for Calculus Nehemiah. In particular, the main theorem
-- about it producing the correct incremental behavior.

open import Nehemiah.Syntax.Type
open import Nehemiah.Syntax.Term
open import Nehemiah.Denotation.Value
open import Nehemiah.Denotation.Evaluation
open import Nehemiah.Change.Type
open import Nehemiah.Change.Term
open import Nehemiah.Change.Value
open import Nehemiah.Change.Evaluation
open import Nehemiah.Change.Validity
open import Nehemiah.Change.Derive
open import Nehemiah.Change.Implementation

open import Base.Denotation.Notation
open import Relation.Binary.PropositionalEquality
open import Data.Integer
open import Theorem.Groups-Nehemiah
open import Postulate.Extensionality

import Parametric.Change.Correctness
  Const ⟦_⟧Base ⟦_⟧Const ΔBase
  apply-base diff-base nil-base
  ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧
  meaning-⊕-base meaning-⊝-base meaning-onil-base
  derive-const implementation-structure as Correctness

open import Algebra.Structures

private
  flatmap-funarg-equal : ∀ (f : ℤ → Bag) (Δf : Δ₍ int ⇒ bag ₎ f) Δf′ (Δf≈Δf′ : Δf ≈₍ int ⇒ bag ₎ Δf′) →
    (f ⊞₍ int ⇒ bag ₎ Δf) ≡ (f ⟦⊕₍ int ⇒ bag ₎⟧ Δf′)
  flatmap-funarg-equal f Δf Δf′ Δf≈Δf′ = ext lemma
    where
    lemma : ∀ v → f v ++ FunctionChange.apply Δf v (+ 0) ≡ f v ++ Δf′ v (+ 0)
    lemma v rewrite Δf≈Δf′ v (+ 0) (+ 0) refl = refl

derive-const-correct : Correctness.Structure
derive-const-correct (intlit-const n) = refl
derive-const-correct add-const w Δw .Δw refl w₁ Δw₁ .Δw₁ refl
  rewrite mn·pq=mp·nq {w} {Δw} {w₁} {Δw₁}
  | associative-int (w + w₁) (Δw + Δw₁) (- (w + w₁))
  = n+[m-n]=m {w + w₁} {Δw + Δw₁}
derive-const-correct minus-const w Δw .Δw refl
  rewrite sym (-m·-n=-mn {w} {Δw})
  | associative-int (- w) (- Δw) (- (- w)) = n+[m-n]=m { - w} { - Δw}
derive-const-correct empty-const = refl
derive-const-correct insert-const w Δw .Δw refl w₁ Δw₁ .Δw₁ refl = refl
derive-const-correct union-const w Δw .Δw refl w₁ Δw₁ .Δw₁ refl
  rewrite ab·cd=ac·bd {w} {Δw} {w₁} {Δw₁}
  | associative-bag (w ++ w₁) (Δw ++ Δw₁) (negateBag (w ++ w₁))
  = a++[b\\a]=b {w ++ w₁} {Δw ++ Δw₁}
derive-const-correct negate-const w Δw .Δw refl
  rewrite sym (-a·-b=-ab {w} {Δw})
  | associative-bag (negateBag w) (negateBag Δw) (negateBag (negateBag w))
  = a++[b\\a]=b {negateBag w} {negateBag Δw}
derive-const-correct flatmap-const w Δw Δw′ Δw≈Δw′ w₁ Δw₁ .Δw₁ refl
  rewrite flatmap-funarg-equal w Δw Δw′ Δw≈Δw′ = refl
derive-const-correct sum-const w Δw .Δw refl
  rewrite homo-sum {w} {Δw}
  | associative-int (sumBag w) (sumBag Δw) (- sumBag w)
  = n+[m-n]=m {sumBag w} {sumBag Δw}

open Correctness.Structure derive-const-correct public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

open import Groups.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Groups.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas
open import Groups.Subgroups.Definition
open import Groups.Lemmas
open import Groups.Abelian.Definition
open import Groups.Subgroups.Normal.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Groups.Subgroups.Normal.Lemmas where

data GroupKernelElement {a} {b} {c} {d} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) : Set (a ⊔ b ⊔ c ⊔ d) where
  kerOfElt : (x : A) → (Setoid._∼_ T (f x) (Group.0G H)) → GroupKernelElement G hom

groupKernel : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → Setoid (GroupKernelElement G hom)
Setoid._∼_ (groupKernel {S = S} G {H} {f} fHom) (kerOfElt x fx=0) (kerOfElt y fy=0) = Setoid._∼_ S x y
Equivalence.reflexive (Setoid.eq (groupKernel {S = S} G {H} {f} fHom)) {kerOfElt x x₁} = Equivalence.reflexive (Setoid.eq S)
Equivalence.symmetric (Setoid.eq (groupKernel {S = S} G {H} {f} fHom)) {kerOfElt x prX} {kerOfElt y prY} = Equivalence.symmetric (Setoid.eq S)
Equivalence.transitive (Setoid.eq (groupKernel {S = S} G {H} {f} fHom)) {kerOfElt x prX} {kerOfElt y prY} {kerOfElt z prZ} = Equivalence.transitive (Setoid.eq S)

groupKernelGroupOp : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → (GroupKernelElement G hom) → (GroupKernelElement G hom) → (GroupKernelElement G hom)
groupKernelGroupOp {T = T} {_·A_ = _+A_} G {H = H} hom (kerOfElt x prX) (kerOfElt y prY) = kerOfElt (x +A y) (transitive (GroupHom.groupHom hom) (transitive (Group.+WellDefined H prX prY) (Group.identLeft H)))
  where
    open Setoid T
    open Equivalence eq

groupKernelGroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → Group (groupKernel G hom) (groupKernelGroupOp G hom)
Group.+WellDefined (groupKernelGroup G fHom) {kerOfElt x prX} {kerOfElt y prY} {kerOfElt a prA} {kerOfElt b prB} = Group.+WellDefined G
Group.0G (groupKernelGroup G fHom) = kerOfElt (Group.0G G) (imageOfIdentityIsIdentity fHom)
Group.inverse (groupKernelGroup {T = T} G {H = H} fHom) (kerOfElt x prX) = kerOfElt (Group.inverse G x) (transitive (homRespectsInverse fHom) (transitive (inverseWellDefined H prX) (invIdent H)))
  where
    open Setoid T
    open Equivalence eq
Group.+Associative (groupKernelGroup {S = S} {_·A_ = _·A_} G fHom) {kerOfElt x prX} {kerOfElt y prY} {kerOfElt z prZ} = Group.+Associative G
Group.identRight (groupKernelGroup G fHom) {kerOfElt x prX} = Group.identRight G
Group.identLeft (groupKernelGroup G fHom) {kerOfElt x prX} = Group.identLeft G
Group.invLeft (groupKernelGroup G fHom) {kerOfElt x prX} = Group.invLeft G
Group.invRight (groupKernelGroup G fHom) {kerOfElt x prX} = Group.invRight G

injectionFromKernelToG : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → GroupKernelElement G hom → A
injectionFromKernelToG G hom (kerOfElt x _) = x

injectionFromKernelToGIsHom : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → GroupHom (groupKernelGroup G hom) G (injectionFromKernelToG G hom)
GroupHom.groupHom (injectionFromKernelToGIsHom {S = S} G hom) {kerOfElt x prX} {kerOfElt y prY} = Equivalence.reflexive (Setoid.eq S)
GroupHom.wellDefined (injectionFromKernelToGIsHom G hom) {kerOfElt x prX} {kerOfElt y prY} i = i

groupKernelGroupPred : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → A → Set d
groupKernelGroupPred {T = T} G {H = H} {f = f} hom a = Setoid._∼_ T (f a) (Group.0G H)

groupKernelGroupPredWd : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → {x y : A} → (Setoid._∼_ S x y) → (groupKernelGroupPred G hom x → groupKernelGroupPred G hom y)
groupKernelGroupPredWd {S = S} {T = T} G hom {x} {y} x=y fx=0 = Equivalence.transitive (Setoid.eq T) (GroupHom.wellDefined hom (Equivalence.symmetric (Setoid.eq S) x=y)) fx=0

groupKernelGroupIsSubgroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → Subgroup G (groupKernelGroupPred G hom)
Subgroup.closedUnderPlus (groupKernelGroupIsSubgroup {S = S} {T = T} G {H = H} hom) g=0 h=0 = Equivalence.transitive (Setoid.eq T) (GroupHom.groupHom hom) (Equivalence.transitive (Setoid.eq T) (Group.+WellDefined H g=0 h=0) (Group.identLeft H))
Subgroup.containsIdentity (groupKernelGroupIsSubgroup G hom) = imageOfIdentityIsIdentity hom
Subgroup.closedUnderInverse (groupKernelGroupIsSubgroup {S = S} {T = T} G {H = H} hom) g=0 = Equivalence.transitive (Setoid.eq T) (homRespectsInverse hom) (Equivalence.transitive (Setoid.eq T) (inverseWellDefined H g=0) (invIdent H))
Subgroup.isSubset (groupKernelGroupIsSubgroup G hom) = groupKernelGroupPredWd G hom

groupKernelGroupIsNormalSubgroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → normalSubgroup G (groupKernelGroupIsSubgroup G hom)
groupKernelGroupIsNormalSubgroup {T = T} G {H = H} hom k=0 = transitive groupHom (transitive (+WellDefined reflexive groupHom) (transitive (+WellDefined reflexive (transitive (+WellDefined k=0 reflexive) identLeft)) (transitive (symmetric groupHom) (transitive (wellDefined (Group.invRight G)) (imageOfIdentityIsIdentity hom)))))
  where
    open Setoid T
    open Group H
    open Equivalence eq
    open GroupHom hom

abelianGroupSubgroupIsNormal : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {G : Group S _+_} {pred : A → Set c} → (s : Subgroup G pred) → AbelianGroup G → normalSubgroup G s
abelianGroupSubgroupIsNormal {S = S} {_+_ = _+_} {G = G} record { isSubset = predWd ; closedUnderPlus = respectsPlus ; containsIdentity = respectsId ; closedUnderInverse = respectsInv } abelian {k} {l} prK = predWd (transitive (transitive (transitive (symmetric identLeft) (+WellDefined (symmetric invRight) reflexive)) (symmetric +Associative)) (+WellDefined reflexive commutative)) prK
  where
    open Group G
    open AbelianGroup abelian
    open Setoid S
    open Equivalence eq


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

open import lib.Basics
open import lib.types.Bool
open import lib.types.Empty
open import lib.types.Lift
open import lib.types.Sigma
open import lib.types.Pi

module lib.types.Coproduct where

module _ {i j} {A : Type i} {B : Type j} where

  Coprod-elim : ∀ {k} {C : A ⊔ B → Type k}
    → ((a : A) → C (inl a)) → ((b : B) → C (inr b))
    → Π (A ⊔ B) C
  Coprod-elim f g (inl a) = f a
  Coprod-elim f g (inr b) = g b

  ⊔-elim = Coprod-elim

  Coprod-rec : ∀ {k} {C : Type k}
    → (A → C) → (B → C) → (A ⊔ B → C)
  Coprod-rec {C = C} = Coprod-elim {C = λ _ → C}

  ⊔-rec = Coprod-rec

  Coprod= : Coprod A B → Coprod A B → Type (lmax i j)
  Coprod= (inl a₁) (inl a₂) = Lift {j = (lmax i j)} $ a₁ == a₂
  Coprod= (inl a₁) (inr b₂) = Lift Empty
  Coprod= (inr b₁) (inl a₂) = Lift Empty
  Coprod= (inr b₁) (inr b₂) = Lift {j = (lmax i j)} $ b₁ == b₂

  Coprod=-in : {x y : Coprod A B} → (x == y) → Coprod= x y
  Coprod=-in {inl _} idp = lift idp
  Coprod=-in {inr _} idp = lift idp

  Coprod=-out : {x y : Coprod A B} → Coprod= x y → (x == y)
  Coprod=-out {inl _} {inl _} c = ap inl $ lower c
  Coprod=-out {inl _} {inr _} c = Empty-rec $ lower c
  Coprod=-out {inr _} {inl _} c = Empty-rec $ lower c
  Coprod=-out {inr _} {inr _} c = ap inr (lower c)

  Coprod=-in-equiv : (x y : Coprod A B) → (x == y) ≃ Coprod= x y
  Coprod=-in-equiv x y = equiv Coprod=-in Coprod=-out (f-g x y) (g-f x y)
    where f-g : ∀ x' y' → ∀ c → Coprod=-in (Coprod=-out {x'} {y'} c) == c
          f-g (inl a₁) (inl .a₁) (lift idp) = idp
          f-g (inl a₁) (inr b₂) b = Empty-rec $ lower b
          f-g (inr b₁) (inl a₂) b = Empty-rec $ lower b
          f-g (inr b₁) (inr .b₁) (lift idp) = idp

          g-f : ∀ x' y' → ∀ p → Coprod=-out (Coprod=-in {x'} {y'} p) == p
          g-f (inl _) .(inl _) idp = idp
          g-f (inr _) .(inr _) idp = idp

  inl=inl-equiv : (a₁ a₂ : A) → (inl a₁ == inl a₂) ≃ (a₁ == a₂)
  inl=inl-equiv a₁ a₂ = lower-equiv ∘e Coprod=-in-equiv (inl a₁) (inl a₂)

  inr=inr-equiv : (b₁ b₂ : B) → (inr b₁ == inr b₂) ≃ (b₁ == b₂)
  inr=inr-equiv b₁ b₂ = lower-equiv ∘e Coprod=-in-equiv (inr b₁) (inr b₂)

  inl≠inr : (a₁ : A) (b₂ : B) → (inl a₁ ≠ inr b₂)
  inl≠inr a₁ b₂ p = lower $ Coprod=-in p

  inr≠inl : (b₁ : B) (a₂ : A) → (inr b₁ ≠ inl a₂)
  inr≠inl a₁ b₂ p = lower $ Coprod=-in p

  instance
    ⊔-level : ∀ {n} → has-level (S (S n)) A → has-level (S (S n)) B
              → has-level (S (S n)) (Coprod A B)
    ⊔-level {n} pA pB = has-level-in (⊔-level-aux pA pB) where

      instance _ = pA; _ = pB

      ⊔-level-aux : has-level (S (S n)) A → has-level (S (S n)) B
              → has-level-aux (S (S n)) (Coprod A B)
      ⊔-level-aux _ _ (inl a₁) (inl a₂) = equiv-preserves-level (inl=inl-equiv a₁ a₂ ⁻¹)
      ⊔-level-aux _ _ (inl a₁) (inr b₂) = has-level-in (λ p → Empty-rec (inl≠inr a₁ b₂ p))
      ⊔-level-aux _ _ (inr b₁) (inl a₂) = has-level-in (λ p → Empty-rec (inr≠inl b₁ a₂ p))
      ⊔-level-aux _ _ (inr b₁) (inr b₂) = equiv-preserves-level ((inr=inr-equiv b₁ b₂)⁻¹)

  Coprod-level = ⊔-level

module _ {i j} {A : Type i} {B : Type j} where

  Coprod-rec-post∘ : ∀ {k l} {C : Type k} {D : Type l}
    → (h : C → D) (f : A → C) (g : B → C)
    → h ∘ Coprod-rec f g ∼ Coprod-rec (h ∘ f) (h ∘ g)
  Coprod-rec-post∘ h f g (inl _) = idp
  Coprod-rec-post∘ h f g (inr _) = idp

  ⊔-rec-post∘ = Coprod-rec-post∘

module _ {i i' j j'} {A : Type i} {A' : Type i'} {B : Type j} {B' : Type j'}
  (f : A → A') (g : B → B') where

  ⊔-fmap : A ⊔ B → A' ⊔ B'
  ⊔-fmap (inl a) = inl (f a)
  ⊔-fmap (inr b) = inr (g b)

infix 80 _⊙⊔_
_⊙⊔_ : ∀ {i j} → Ptd i → Ptd j → Ptd (lmax i j)
X ⊙⊔ Y = ⊙[ Coprod (de⊙ X) (de⊙ Y) , inl (pt X) ]

_⊔⊙_ : ∀ {i j} → Ptd i → Ptd j → Ptd (lmax i j)
X ⊔⊙ Y = ⊙[ Coprod (de⊙ X) (de⊙ Y) , inr (pt Y) ]

module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (f : X ⊙→ Z) (g : Y ⊙→ Z) where

  ⊙⊔-rec : X ⊙⊔ Y ⊙→ Z
  ⊙⊔-rec = Coprod-rec (fst f) (fst g) , snd f

  ⊔⊙-rec : X ⊔⊙ Y ⊙→ Z
  ⊔⊙-rec = Coprod-rec (fst f) (fst g) , snd g

module _ {i i' j j'} {X : Ptd i} {X' : Ptd i'} {Y : Ptd j} {Y' : Ptd j'}
  (f : X ⊙→ X') (g : Y ⊙→ Y') where

  ⊙⊔-fmap : X ⊙⊔ Y ⊙→ X' ⊙⊔ Y'
  ⊙⊔-fmap = ⊔-fmap (fst f) (fst g) , ap inl (snd f)

  ⊔⊙-fmap : X ⊔⊙ Y ⊙→ X' ⊔⊙ Y'
  ⊔⊙-fmap = ⊔-fmap (fst f) (fst g) , ap inr (snd g)

codiag : ∀ {i} {A : Type i} → A ⊔ A → A
codiag = Coprod-rec (idf _) (idf _)

⊙codiag : ∀ {i} {X : Ptd i} → X ⊙⊔ X ⊙→ X
⊙codiag = (codiag , idp)

-- A binary sigma is a coproduct
ΣBool-equiv-⊔ : ∀ {i} (Pick : Bool → Type i)
  → Σ Bool Pick ≃ Pick true ⊔ Pick false
ΣBool-equiv-⊔ Pick = equiv into out into-out out-into
  where
  into : Σ _ Pick → Pick true ⊔ Pick false
  into (true , a) = inl a
  into (false , b) = inr b

  out : (Pick true ⊔ Pick false) → Σ _ Pick
  out (inl a) = (true , a)
  out (inr b) = (false , b)

  abstract
    into-out : ∀ c → into (out c) == c
    into-out (inl a) = idp
    into-out (inr b) = idp

    out-into : ∀ s → out (into s) == s
    out-into (true , a) = idp
    out-into (false , b) = idp

⊔₁-Empty : ∀ {i} (A : Type i) → Empty ⊔ A ≃ A
⊔₁-Empty A = equiv (λ{(inl ()); (inr a) → a}) inr (λ _ → idp) (λ{(inl ()); (inr _) → idp})

module _ {i j k} {A : Type i} {B : Type j} (P : A ⊔ B → Type k) where
  Π₁-⊔-equiv-× : Π (A ⊔ B) P ≃ Π A (P ∘ inl) × Π B (P ∘ inr)
  Π₁-⊔-equiv-× = equiv to from to-from from-to
    where
    to : Π (A ⊔ B) P → Π A (P ∘ inl) × Π B (P ∘ inr)
    to f = (λ a → f (inl a)) , (λ b → f (inr b))

    from : Π A (P ∘ inl) × Π B (P ∘ inr) → Π (A ⊔ B) P
    from (f , g) (inl a) = f a
    from (f , g) (inr b) = g b

    abstract
      to-from : ∀ fg → to (from fg) == fg
      to-from _ = idp

      from-to : ∀ fg → from (to fg) == fg
      from-to fg = λ= λ where (inl _) → idp
                              (inr _) → idp

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module nat-to-string where

open import bool
open import char
open import eq
open import list
open import maybe
open import nat
open import nat-division
open import nat-thms
open import product
open import string
open import termination

ℕ-to-digitsh : (base : ℕ) → 1 < base ≡ tt → (x : ℕ) → ↓𝔹 _>_ x → 𝕃 ℕ
ℕ-to-digitsh _ _ 0 _ = []
ℕ-to-digitsh base bp (suc x) (pf↓ fx) with (suc x) ÷ base ! (<=ℕff2 base bp)
... | q , r , p , _ = r :: (ℕ-to-digitsh base bp q (fx (÷<{base}{q}{r}{x} bp p)))

ℕ-to-digits : ℕ → 𝕃 ℕ
ℕ-to-digits x = reverse (ℕ-to-digitsh 10 refl x (↓-> x))

digit-to-string : ℕ → string
digit-to-string 0 = "0"
digit-to-string 1 = "1"
digit-to-string 2 = "2"
digit-to-string 3 = "3"
digit-to-string 4 = "4"
digit-to-string 5 = "5"
digit-to-string 6 = "6"
digit-to-string 7 = "7"
digit-to-string 8 = "8"
digit-to-string 9 = "9"
digit-to-string _ = "unexpected-digit"

digits-to-string : 𝕃 ℕ → string
digits-to-string [] = ""
digits-to-string (d :: ds) = (digit-to-string d) ^ (digits-to-string ds)

ℕ-to-string : ℕ → string
ℕ-to-string 0 = "0"
ℕ-to-string (suc x) = digits-to-string (ℕ-to-digits (suc x))

string-to-digit : char → maybe ℕ
string-to-digit '0' = just 0
string-to-digit '1' = just 1
string-to-digit '2' = just 2
string-to-digit '3' = just 3
string-to-digit '4' = just 4
string-to-digit '5' = just 5
string-to-digit '6' = just 6
string-to-digit '7' = just 7
string-to-digit '8' = just 8
string-to-digit '9' = just 9
string-to-digit _ = nothing

-- the digits are in order from least to most significant
digits-to-ℕh : ℕ → ℕ → 𝕃 ℕ → ℕ
digits-to-ℕh multiplier sum [] = sum
digits-to-ℕh multiplier sum (x :: xs) = digits-to-ℕh (10 * multiplier) (x * multiplier + sum) xs

digits-to-ℕ : 𝕃 ℕ → ℕ
digits-to-ℕ digits = digits-to-ℕh 1 0 digits

string-to-ℕ : string → maybe ℕ
string-to-ℕ s with 𝕃maybe-map string-to-digit (reverse (string-to-𝕃char s))
... | nothing = nothing
... | just ds = just (digits-to-ℕ ds)

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
{-# OPTIONS --type-in-type #-}

module Compilation.Encode.Examples where

open import Context
open import Type.Core
open import Compilation.Data
open import Compilation.Encode.Core

open import Function
open import Data.Product
open import Data.List.Base

module ProdTreeTreeExample where
  open ProdTreeTree
  open prodTreeTree

  ProdTreeTree′ = ⟦ prodTreeTree ⟧ᵈ

  ProdTree′ : Set -> Set -> Set
  ProdTree′ with ProdTreeTree′
  ... | ø ▶ PT′ ▶ T′ = PT′

  Tree′ : Set -> Set
  Tree′ with ProdTreeTree′
  ... | ø ▶ PT′ ▶ T′ = T′

  mutual
    fromProdTree : ∀ {A B A′ B′} -> (A -> A′) -> (B -> B′) -> ProdTree A B -> ProdTree′ A′ B′
    fromProdTree f g (Prod tree) =
      Wrap λ R h -> h $ fromTree (λ{ (x , y) _ k -> k (f x) (g y) }) tree

    fromTree : ∀ {A A′} -> (A -> A′) -> Tree A -> Tree′ A′
    fromTree f (Leaf x)    = Wrap λ R g h -> g $ f x
    fromTree f (Fork prod) = Wrap λ R g h -> h $ fromProdTree f f prod

  {-# TERMINATING #-}
  mutual
    toProdTree : ∀ {A B A′ B′} -> (A -> A′) -> (B -> B′) -> ProdTree′ A B -> ProdTree A′ B′
    toProdTree f g (Wrap k) =
      k _ λ tree -> Prod $ toTree (λ k -> k _ λ x y -> f x , g y) tree

    toTree : ∀ {A A′} -> (A -> A′) -> Tree′ A -> Tree A′
    toTree f (Wrap k) = k _ (Leaf ∘ f) (Fork ∘ toProdTree f f)

module ListExample where
  list : Data⁺ (ε ▻ (ε ▻ ⋆))
  list
    = PackData
    $ ø
    ▶ ( endᶜ
      ∷ Var vz ⇒ᶜ Var (vs vz) ∙ Var vz ⇒ᶜ endᶜ
      ∷ []
      )

  List′ : Set -> Set
  List′ with ⟦ list ⟧ᵈ
  ... | ø ▶ L′ = L′

  fromList : ∀ {A} -> List A -> List′ A
  fromList  []      = Wrap λ R z f -> z
  fromList (x ∷ xs) = Wrap λ R z f -> f x $ fromList xs

  {-# TERMINATING #-}
  toList : ∀ {A} -> List′ A -> List A
  toList (Wrap k) = k _ [] λ x xs -> x ∷ toList xs

module InterListExample where
  data InterList (A B : Set) : Set where
    InterNil  : InterList A B
    InterCons : A -> B -> InterList B A -> InterList A B

  interlist : Data⁺ (ε ▻ (ε ▻ ⋆ ▻ ⋆))
  interlist
    = PackData
    $ ø
    ▶ ( endᶜ
      ∷ Var (vs vz) ⇒ᶜ Var vz ⇒ᶜ Var (vs vs vz) ∙ Var vz ∙ Var (vs vz) ⇒ᶜ endᶜ
      ∷ []
      )

  InterList′ : Set -> Set -> Set
  InterList′ with ⟦ interlist ⟧ᵈ
  ... | ø ▶ IL′ = IL′

  fromInterList : ∀ {A B} -> InterList A B -> InterList′ A B
  fromInterList  InterNil           = Wrap λ R z f -> z
  fromInterList (InterCons x y yxs) = Wrap λ R z f -> f x y $ fromInterList yxs

  {-# TERMINATING #-}
  toInterList : ∀ {A B} -> InterList′ A B -> InterList A B
  toInterList (Wrap k) = k _ InterNil λ x y yxs -> InterCons x y $ toInterList yxs

module TreeForestExample where
  mutual
    data Tree (A : Set) : Set where
      node : A -> Forest A -> Tree A

    data Forest (A : Set) : Set where
      nil  : Forest A
      cons : Tree A -> Forest A -> Forest A

  treeForest : Data⁺ (ε ▻ (ε ▻ ⋆) ▻ (ε ▻ ⋆))
  treeForest
    = PackData
    $ ø
    ▶ ( Var vz ⇒ᶜ Var (vs vz) ∙ Var vz ⇒ᶜ endᶜ
      ∷ []
      )
    ▶ ( endᶜ
      ∷ Var (vs vs vz) ∙ Var vz ⇒ᶜ Var (vs vz) ∙ Var vz ⇒ᶜ endᶜ
      ∷ []
      )

  TreeForest′ = ⟦ treeForest ⟧ᵈ

  Tree′ : Set -> Set
  Tree′ with TreeForest′
  ... | ø ▶ T′ ▶ F′ = T′

  Forest′ : Set -> Set
  Forest′ with TreeForest′
  ... | ø ▶ T′ ▶ F′ = F′

  mutual
    fromTree : ∀ {A} -> Tree A -> Tree′ A
    fromTree (node x forest) = Wrap λ R f -> f x $ fromForest forest

    fromForest : ∀ {A} -> Forest A -> Forest′ A
    fromForest  nil               = Wrap λ R z f -> z
    fromForest (cons tree forest) = Wrap λ R z f -> f (fromTree tree) (fromForest forest)

  {-# TERMINATING #-}
  mutual
    toTree : ∀ {A} -> Tree′ A -> Tree A
    toTree (Wrap k) = k _ λ x forest -> node x $ toForest forest

    toForest : ∀ {A} -> Forest′ A -> Forest A
    toForest (Wrap k) = k _ nil λ tree forest -> cons (toTree tree) (toForest forest)

module MNExample where
  mutual
    data M (A : Set) : Set where
      p : A -> M A
      n : N -> M A

    data N : Set where
      m : M N -> N

  mn : Data⁺ (ε ▻ (ε ▻ ⋆) ▻ ε)
  mn
    = PackData
    $ ø
    ▶ ( Var vz ⇒ᶜ endᶜ
      ∷ Var (vs vz) ⇒ᶜ endᶜ
      ∷ []
      )
    ▶ ( Var (vs vz) ∙ Var vz ⇒ᶜ endᶜ
      ∷ []
      )

  MN′ = ⟦ mn ⟧ᵈ

  M′ : Set -> Set
  M′ with MN′
  ... | ø ▶ M′ ▶ N′ = M′

  N′ : Set
  N′ with MN′
  ... | ø ▶ M′ ▶ N′ = N′

  {-# TERMINATING #-}
  mutual
    fromM : ∀ {A B} -> (A -> B) -> M A -> M′ B
    fromM f (p x) = Wrap λ R g h -> g $ f x
    fromM f (n x) = Wrap λ R g h -> h $ fromN x

    fromN : N -> N′
    fromN (m x) = Wrap λ R f -> f $ fromM fromN x

  {-# TERMINATING #-}
  mutual
    toM : ∀ {A B} -> (A -> B) -> M′ A -> M B
    toM f (Wrap k) = k _ (λ x -> p (f x)) (λ x -> n (toN x))

    toN : N′ -> N
    toN (Wrap k) = k _ λ x -> m (toM toN x)

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


text:
module FFI.Data.Bool where

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

data Bool : Set where
  false : Bool
  true : Bool
{-# COMPILE GHC Bool = data Data.Bool.Bool (Data.Bool.False|Data.Bool.True) #-}

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text: module test where


text:
module Data.Either.Equiv where

import      Lvl
open import Data.Either as Either
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Operator
open import Structure.Setoid
open import Type

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable A B : Type{ℓ}

record Extensionality ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ (equiv : Equiv{ℓₑ}(A ‖ B)) : Type{Lvl.of(A) Lvl.⊔ Lvl.of(B) Lvl.⊔ ℓₑ₁ Lvl.⊔ ℓₑ₂ Lvl.⊔ ℓₑ} where
  constructor intro
  private instance _ = equiv
  field
     ⦃ Left-function ⦄  : Function Left
     ⦃ Right-function ⦄ : Function Right
     ⦃ Left-injective ⦄   : Injective Left
     ⦃ Right-injective ⦄  : Injective Right
     Left-Right-inequality : ∀{x : A}{y : B} → (Left x ≢ Right y)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import HoTT
open import homotopy.SuspProduct
open import homotopy.SuspSmash
open import homotopy.JoinSusp
open import cohomology.Theory

module cohomology.SphereProduct {i} (CT : CohomologyTheory i) where

open CohomologyTheory CT
open import cohomology.Wedge CT

module _ (n : ℤ) (m : ℕ) (X : Ptd i) where

  private

    space-path : ⊙Susp (⊙Lift {j = i} (⊙Sphere m) ⊙× X)
              == ⊙Susp (⊙Lift (⊙Sphere m)) ⊙∨ (⊙Susp X ⊙∨ ⊙Susp^ (S m) X)
    space-path =
      SuspProduct.⊙path (⊙Lift (⊙Sphere m)) X
      ∙ ap (λ Z → ⊙Susp (⊙Lift (⊙Sphere m)) ⊙∨ (⊙Susp X ⊙∨ Z))
           (SuspSmash.⊙path (⊙Lift (⊙Sphere m)) X
            ∙ ⊙*-⊙Lift-⊙Sphere m X)

  C-Sphere× : C n (⊙Lift {j = i} (⊙Sphere m) ⊙× X)
           == C n (⊙Lift (⊙Sphere m)) ×ᴳ (C n X ×ᴳ C n (⊙Susp^ m X))
  C-Sphere× =
    ! (group-ua (C-Susp n (⊙Lift {j = i} (⊙Sphere m) ⊙× X)))
    ∙ ap (C (succ n)) space-path
    ∙ CWedge.path (succ n) (⊙Susp (⊙Lift (⊙Sphere m))) (⊙Susp X ⊙∨ ⊙Susp^ (S m) X)
    ∙ ap (λ H → C (succ n) (⊙Susp (⊙Lift (⊙Sphere m))) ×ᴳ H)
         (CWedge.path (succ n) (⊙Susp X) (⊙Susp^ (S m) X)
          ∙ ap2 _×ᴳ_ (group-ua (C-Susp n X))
                     (group-ua (C-Susp n (⊙Susp^ m X))))
    ∙ ap (λ H → H ×ᴳ (C n X ×ᴳ C n (⊙Susp^ m X)))
         (group-ua (C-Susp n (⊙Lift (⊙Sphere m))))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
------------------------------------------------------------------------
-- A type soundness result
------------------------------------------------------------------------

module Lambda.Closure.Functional.Type-soundness where

import Category.Monad.Partiality as Partiality
open import Category.Monad.Partiality.All as All
  using (All; now; later)
open import Codata.Musical.Notation
open import Data.Fin using (Fin; zero; suc)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Maybe.Relation.Unary.Any as Maybe using (just)
open import Data.Nat
open import Data.Vec using (Vec; []; _∷_; lookup)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary

open All.Alternative
private
  open module E {A : Set} = Partiality.Equality (_≡_ {A = A})
    using (_≈_; now; laterˡ)

open import Lambda.Closure.Functional
open Lambda.Closure.Functional.PF using (fail)
open Lambda.Closure.Functional.Workaround using (⟪_⟫P)
open import Lambda.Syntax
open Lambda.Syntax.Closure Tm

-- WF-Value, WF-Env and WF-MV specify when a
-- value/environment/potential value is well-formed with respect to a
-- given context (and type).

mutual

  data WF-Value : Ty → Value → Set where
    con : ∀ {i} → WF-Value nat (con i)
    ƛ   : ∀ {n Γ σ τ} {t : Tm (1 + n)} {ρ}
          (t∈ : ♭ σ ∷ Γ ⊢ t ∈ ♭ τ) (ρ-wf : WF-Env Γ ρ) →
          WF-Value (σ ⇾ τ) (ƛ t ρ)

  infixr 5 _∷_

  data WF-Env : ∀ {n} → Ctxt n → Env n → Set where
    []  : WF-Env [] []
    _∷_ : ∀ {n} {Γ : Ctxt n} {ρ σ v}
          (v-wf : WF-Value σ v) (ρ-wf : WF-Env Γ ρ) →
          WF-Env (σ ∷ Γ) (v ∷ ρ)

WF-MV : Ty → Maybe Value → Set
WF-MV σ = Maybe.Any (WF-Value σ)

-- Variables pointing into a well-formed environment refer to
-- well-formed values.

lookup-wf : ∀ {n Γ ρ} (x : Fin n) → WF-Env Γ ρ →
            WF-Value (lookup Γ x) (lookup ρ x)
lookup-wf zero    (v-wf ∷ ρ-wf) = v-wf
lookup-wf (suc x) (v-wf ∷ ρ-wf) = lookup-wf x ρ-wf

-- If we can prove All (WF-MV σ) x, then x does not "go wrong".

does-not-go-wrong : ∀ {σ x} → All (WF-MV σ) x → ¬ x ≈ fail
does-not-go-wrong (now (just _)) (now ())
does-not-go-wrong (later x-wf)   (laterˡ x↯) =
  does-not-go-wrong (♭ x-wf) x↯

-- Well-typed programs do not "go wrong".

mutual

  ⟦⟧-wf : ∀ {n Γ} (t : Tm n) {σ} → Γ ⊢ t ∈ σ →
          ∀ {ρ} → WF-Env Γ ρ → AllP (WF-MV σ) (⟦ t ⟧ ρ)
  ⟦⟧-wf (con i)   con             ρ-wf = now (just con)
  ⟦⟧-wf (var x)   var             ρ-wf = now (just (lookup-wf x ρ-wf))
  ⟦⟧-wf (ƛ t)     (ƛ t∈)          ρ-wf = now (just (ƛ t∈ ρ-wf))
  ⟦⟧-wf (t₁ · t₂) (t₁∈ · t₂∈) {ρ} ρ-wf =
    ⟦ t₁ · t₂ ⟧ ρ          ≅⟨ ·-comp t₁ t₂ ⟩P
    ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ   ⟨ (⟦⟧-wf t₁ t₁∈ ρ-wf >>=-congP λ { .{_} (just f-wf) →
                               ⟦⟧-wf t₂ t₂∈ ρ-wf >>=-congP λ { .{_} (just v-wf) →
                               ∙-wf f-wf v-wf }}) ⟩P

  ∙-wf : ∀ {σ τ f v} →
         WF-Value (σ ⇾ τ) f → WF-Value (♭ σ) v →
         AllP (WF-MV (♭ τ)) ⟪ f ∙ v ⟫P
  ∙-wf (ƛ t₁∈ ρ₁-wf) v₂-wf = later (♯ ⟦⟧-wf _ t₁∈ (v₂-wf ∷ ρ₁-wf))

type-soundness : ∀ {t : Tm 0} {σ} → [] ⊢ t ∈ σ → ¬ ⟦ t ⟧ [] ≈ fail
type-soundness t∈ =
  does-not-go-wrong (All.Alternative.sound (⟦⟧-wf _ t∈ []))

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-# OPTIONS --no-termination-check #-}

-- Testing how the pragmas are saved in the agda interface files (using
-- the program dump-agdai).

-- 13 July 2012. Because for example the --no-termination-check is a
-- PragmaOption it is saved as:
--
-- iPragmaOptions = [["--no-termination-check"]]

module OptionPragma where

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
F : (A A : Set) → Set
F A _ = A

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- Andreas, 2020-02-10, issue 4429, reported by Nisse
--
-- Injectivity analysis can make type checker loop (or slow down)
-- since it reduces the rhs of definitions.
--
-- Try to be smarter and do not needlessly invoke the injectivity
-- analysis.  For instance, do not consider a projection pattern
-- a proper match for the sake of injectivity, since a metavariable
-- cannot occupy its position (unlike for constructor and literal patterns).

-- {-# OPTIONS -v tc.inj.check:45 #-}

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A

postulate
  A : Set

{-# TERMINATING #-}

to : A → A
to = to  -- An approximation of slow but terminating code.

{-# TERMINATING #-}

from : A → A
from = from  -- An approximation of slow but terminating code.

works : A ⇔ A
works = record
  { to   = to
  ; from = from
  }

test : A ⇔ A
test ._⇔_.to   = to
test ._⇔_.from = from

-- WAS: Definition by copatterns loops, because the injectivity
-- checker tries to reduce the rhs.

-- Should pass, since now injectivity checker does not consider
-- a projection pattern as proper match.
-- Thus, injectivity for this function would be pointless.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
-- Andreas, 2014-05-22

module _ where

module M where
  f : Set
  f = f

module N where
  f : Set
  f = f

-- OUTPUT IS:
--
-- Termination checking failed for the following functions:
--   f, f
-- Problematic calls:
--   f (at /home/abel/tmp/bla/Agda/test/bugs/TerminationReportQualified.agda:7,7-8)
--   f (at /home/abel/tmp/bla/Agda/test/bugs/TerminationReportQualified.agda:11,7-8)

-- Expected: Qualified names M.f and N.f

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical #-}
module Cubical.Codata.Stream where

open import Cubical.Codata.Stream.Base public

open import Cubical.Codata.Stream.Properties public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
open import Agda.Builtin.Nat

data D : Set where
  c : D → D

record R : Set where
  constructor mkR
  field f : Nat

f : D → R
f (c x) = mkR zero

f' : D → Nat → R
f' (c x) n = mkR n

postulate
  P  : (A : Set) → A → Set
  g  : (x : D) → P R (f x) → P D x
  g' : (n : Nat) (x : D) → P R (f' x n) → P D x

h : (x : D) → P R (mkR zero) → P D (c x)
h x = g _

h' : (n : Nat) (x : D) → P R (mkR n) → P D (c x)
h' n x = g' n _


text:
------------------------------------------------------------------------
-- Functional semantics and type soundness proof for an untyped
-- λ-calculus with constants
------------------------------------------------------------------------

module Lambda.Substitution.Functional where

open import Category.Monad.Partiality as Partiality using (_⊥; never)
open import Category.Monad.Partiality.All as All
  using (All; now; later)
open import Codata.Musical.Notation
open import Data.Maybe as Maybe using (Maybe)
open import Data.Maybe.Relation.Unary.Any as Maybe using (just)
open import Data.Vec using ([])
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

open All.Alternative
private
  open module E {A : Set} = Partiality.Equality (_≡_ {A = A})
  open module R {A : Set} =
    Partiality.Reasoning (P.isEquivalence {A = A})

open import Lambda.Syntax
open WHNF
open import Lambda.Substitution
open import Lambda.Closure.Functional
  using (module PF; module Workaround)
open Workaround hiding (_>>=_)

------------------------------------------------------------------------
-- Semantics

infix 5 _∙_

-- Note that this definition gives us determinism "for free".

mutual

  ⟦_⟧′ : Tm 0 → Maybe (Value 0) ⊥P
  ⟦ con i ⟧′   = return (con i)
  ⟦ var () ⟧′
  ⟦ ƛ t ⟧′     = return (ƛ t)
  ⟦ t₁ · t₂ ⟧′ = ⟦ t₁ ⟧′ >>= λ v₁ →
                 ⟦ t₂ ⟧′ >>= λ v₂ →
                 v₁ ∙ v₂
    where open Workaround

  _∙_ : Value 0 → Value 0 → Maybe (Value 0) ⊥P
  con i ∙ v₂ = fail
  ƛ t₁  ∙ v₂ = later (♯ ⟦ t₁ / sub ⌜ v₂ ⌝ ⟧′)

⟦_⟧ : Tm 0 → Maybe (Value 0) ⊥
⟦ t ⟧ = ⟪ ⟦ t ⟧′ ⟫P

------------------------------------------------------------------------
-- Example

Ω-loops : ⟦ Ω ⟧ ≈ never
Ω-loops = later (♯ Ω-loops)

------------------------------------------------------------------------
-- Some lemmas

open PF hiding (_>>=_)

-- An abbreviation.

infix 5 _⟦·⟧_

_⟦·⟧_ : Maybe (Value 0) ⊥ → Maybe (Value 0) ⊥ → Maybe (Value 0) ⊥
v₁ ⟦·⟧ v₂ = v₁ >>= λ v₁ → v₂ >>= λ v₂ → ⟪ v₁ ∙ v₂ ⟫P
  where open PF

-- _⟦·⟧_ preserves equality.

_⟦·⟧-cong_ : ∀ {k v₁₁ v₁₂ v₂₁ v₂₂} →
             Rel k v₁₁ v₂₁ → Rel k v₁₂ v₂₂ →
             Rel k (v₁₁ ⟦·⟧ v₁₂) (v₂₁ ⟦·⟧ v₂₂)
v₁₁≈v₂₁ ⟦·⟧-cong v₁₂≈v₂₂ =
  v₁₁≈v₂₁ >>=-cong λ v₁ →
  v₁₂≈v₂₂ >>=-cong λ v₂ →
  ⟪ v₁ ∙ v₂ ⟫P ∎

-- The semantics of application is compositional (with respect to the
-- syntactic equality which is used).

·-comp : (t₁ t₂ : Tm 0) →
         ⟦ t₁ · t₂ ⟧ ≅ ⟦ t₁ ⟧ ⟦·⟧ ⟦ t₂ ⟧
·-comp t₁ t₂ =
  ⟦ t₁ · t₂ ⟧                                  ≅⟨ >>=-hom ⟦ t₁ ⟧′ _ ⟩

  PF._>>=_ ⟦ t₁ ⟧ (λ v₁ →
           ⟪ Workaround._>>=_ ⟦ t₂ ⟧′ (λ v₂ →
             v₁ ∙ v₂) ⟫P)                      ≅⟨ ((⟦ t₁ ⟧ ∎) >>=-cong λ _ →
                                                   >>=-hom ⟦ t₂ ⟧′ _) ⟩
  ⟦ t₁ ⟧ ⟦·⟧ ⟦ t₂ ⟧                            ∎

------------------------------------------------------------------------
-- Type soundness

-- WF-Value and WF-MV specify when a (potential) value is well-formed
-- with respect to a given type.

WF-Value : Ty → Value 0 → Set
WF-Value σ v = [] ⊢ ⌜ v ⌝ ∈ σ

WF-MV : Ty → Maybe (Value 0) → Set
WF-MV σ = Maybe.Any (WF-Value σ)

-- If we can prove All (WF-MV σ) x, then x does not "go wrong".

does-not-go-wrong : ∀ {σ x} → All (WF-MV σ) x → ¬ x ≈ PF.fail
does-not-go-wrong (now (just _)) (now ())
does-not-go-wrong (later x-wf)   (laterˡ x↯) =
  does-not-go-wrong (♭ x-wf) x↯

-- Well-typed programs do not "go wrong".

mutual

  ⟦⟧-wf : ∀ (t : Tm 0) {σ} → [] ⊢ t ∈ σ →
          AllP (WF-MV σ) ⟦ t ⟧
  ⟦⟧-wf (con i)   con         = now (just con)
  ⟦⟧-wf (var ())  var
  ⟦⟧-wf (ƛ t)     (ƛ t∈)      = now (just (ƛ t∈))
  ⟦⟧-wf (t₁ · t₂) (t₁∈ · t₂∈) =
    ⟦ t₁ · t₂ ⟧        ≅⟨ ·-comp t₁ t₂ ⟩P
    ⟦ t₁ ⟧ ⟦·⟧ ⟦ t₂ ⟧   ⟨ (⟦⟧-wf t₁ t₁∈ >>=-congP λ { .{_} (just f-wf) →
                           ⟦⟧-wf t₂ t₂∈ >>=-congP λ { .{_} (just v-wf) →
                           ∙-wf f-wf v-wf }}) ⟩P

  ∙-wf : ∀ {σ τ f v} →
         WF-Value (σ ⇾ τ) f → WF-Value (♭ σ) v →
         AllP (WF-MV (♭ τ)) ⟪ f ∙ v ⟫P
  ∙-wf {f = con _} ()      _
  ∙-wf {f = ƛ t₁}  (ƛ t₁∈) v₂∈ =
    later (♯ ⟦⟧-wf _ (/-preserves t₁∈ (sub-preserves v₂∈)))

type-soundness : ∀ {t σ} → [] ⊢ t ∈ σ → ¬ ⟦ t ⟧ ≈ PF.fail
type-soundness t∈ =
  does-not-go-wrong (All.Alternative.sound (⟦⟧-wf _ t∈))


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

module Cham.Name where

open import Data.String

Name : Set
Name = String


text:
------------------------------------------------------------------------------
-- Axiomatic PA properties
------------------------------------------------------------------------------

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

module PA.Axiomatic.Mendelson.PropertiesI where

open import PA.Axiomatic.Mendelson.Base
open import PA.Axiomatic.Mendelson.Relation.Binary.EqReasoning
open import PA.Axiomatic.Mendelson.Relation.Binary.PropositionalEqualityI
  using ( ≈-sym )

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

succCong : ∀ {m n} → m ≈ n → succ m ≈ succ n
succCong = S₂

+-leftIdentity : ∀ n → zero + n ≈ n
+-leftIdentity = S₅

+-rightIdentity : ∀ n → n + zero ≈ n
+-rightIdentity = S₉ A A0 is
  where
  A : ℕ → Set
  A i = i + zero ≈ i

  A0 : A zero
  A0 = +-leftIdentity zero

  is : ∀ i → A i → A (succ i)
  is i ih = succ i + zero   ≈⟨ S₆ i zero ⟩
            succ (i + zero) ≈⟨ S₂ ih ⟩
            succ i          ∎

x+Sy≈S[x+y] : ∀ m n → m + succ n ≈ succ (m + n)
x+Sy≈S[x+y] m n = S₉ A A0 is m
  where
  A : ℕ → Set
  A i = i + succ n ≈ succ (i + n)

  A0 : A zero
  A0 = zero + succ n   ≈⟨ +-leftIdentity (succ n) ⟩
       succ n          ≈⟨ S₂ (≈-sym (+-leftIdentity n)) ⟩
       succ (zero + n) ∎

  is : ∀ i → A i → A (succ i)
  is i ih = succ i + succ n     ≈⟨ S₆ i (succ n) ⟩
            succ (i + succ n)   ≈⟨ S₂ ih ⟩
            succ (succ (i + n)) ≈⟨ S₂ (≈-sym (S₆ i n)) ⟩
            succ (succ i + n)   ∎

+-rightCong : ∀ {m n p} → n ≈ p → m + n ≈ m + p
+-rightCong {m} {n} {p} h = S₉ A A0 is m
  where
  A : ℕ → Set
  A i = i + n ≈ i + p

  A0 : A zero
  A0 = zero + n ≈⟨ S₅ n ⟩
       n        ≈⟨ h ⟩
       p        ≈⟨ ≈-sym (S₅ p) ⟩
       zero + p ∎

  is : ∀ i → A i → A (succ i)
  is i ih = succ i + n   ≈⟨ S₆ i n ⟩
            succ (i + n) ≈⟨ S₂ ih ⟩
            succ (i + p) ≈⟨ ≈-sym (S₆ i p) ⟩
            succ i + p   ∎

+-leftCong : ∀ {m n p} → m ≈ n → m + p ≈ n + p
+-leftCong {m} {n} {p} h = S₉ A A0 is p
  where
  A : ℕ → Set
  A i = m + i ≈ n + i

  A0 : A zero
  A0 = m + zero ≈⟨ +-rightIdentity m ⟩
       m        ≈⟨ h ⟩
       n        ≈⟨ ≈-sym (+-rightIdentity n) ⟩
       n + zero ∎

  is : ∀ i → A i → A (succ i)
  is i ih = m + succ i   ≈⟨ x+Sy≈S[x+y] m i ⟩
            succ (m + i) ≈⟨ S₂ ih ⟩
            succ (n + i) ≈⟨ ≈-sym (x+Sy≈S[x+y] n i) ⟩
            n + succ i   ∎

+-asocc : ∀ m n o → m + n + o ≈ m + (n + o)
+-asocc m n o = S₉ A A0 is m
  where
  A : ℕ → Set
  A i = i + n + o ≈ i + (n + o)

  A0 : A zero
  A0 = zero + n + o   ≈⟨ +-leftCong (+-leftIdentity n) ⟩
       n + o          ≈⟨ ≈-sym (+-leftIdentity (n + o)) ⟩
       zero + (n + o) ∎

  is : ∀ i → A i → A (succ i)
  is i ih = succ i + n + o     ≈⟨ +-leftCong (S₆ i n) ⟩
            succ (i + n) + o   ≈⟨ S₆ (i + n) o ⟩
            succ (i + n + o)   ≈⟨ S₂ ih ⟩
            succ (i + (n + o)) ≈⟨ ≈-sym (S₆ i (n + o)) ⟩
            succ i + (n + o)   ∎

+-comm : ∀ m n → m + n ≈ n + m
+-comm m n = S₉ A A0 is m
  where
  A : ℕ → Set
  A i = i + n ≈ n + i

  A0 : A zero
  A0 = zero + n   ≈⟨ +-leftIdentity n ⟩
       n          ≈⟨ ≈-sym (+-rightIdentity n) ⟩
       n + zero   ∎

  is : ∀ i → A i → A (succ i)
  is i ih = succ i + n   ≈⟨ S₆ i n ⟩
            succ (i + n) ≈⟨ S₂ ih ⟩
            succ (n + i) ≈⟨ ≈-sym (x+Sy≈S[x+y] n i) ⟩
            n + succ i   ∎

*-leftZero : ∀ n → zero * n ≈ zero
*-leftZero = S₇

*-rightZero : ∀ n → n * zero ≈ zero
*-rightZero n = S₉ A A0 is n
  where
  A : ℕ → Set
  A i = i * zero ≈ zero

  A0 : A zero
  A0 = *-leftZero zero

  is : ∀ i → A i → A (succ i)
  is i ih = succ i * zero   ≈⟨ S₈ i zero ⟩
            zero + i * zero ≈⟨ +-leftIdentity (i * zero) ⟩
            i * zero        ≈⟨ ih ⟩
            zero            ∎

x*Sy≈x+[x*y] : ∀ m n → m * succ n ≈ m + m * n
x*Sy≈x+[x*y] m n = S₉ A A0 is m
  where
  A : ℕ → Set
  A i = i * succ n ≈ i + i * n

  A0 : A zero
  A0 = zero * succ n   ≈⟨ *-leftZero (succ n) ⟩
       zero            ≈⟨ ≈-sym (S₅ zero) ⟩
       zero + zero     ≈⟨ +-rightCong (≈-sym (*-leftZero n)) ⟩
       zero + zero * n ∎

  is : ∀ i → A i → A (succ i)
  is i ih =
    succ i * succ n        ≈⟨ S₈ i (succ n) ⟩
    succ n + (i * succ n)  ≈⟨ +-rightCong ih ⟩
    succ n + (i + i * n)   ≈⟨ S₆ n (i + i * n) ⟩
    succ (n + (i + i * n)) ≈⟨ succCong (≈-sym (+-asocc n i (i * n))) ⟩
    succ (n + i + (i * n)) ≈⟨ succCong (+-leftCong (+-comm n i)) ⟩
    succ (i + n + (i * n)) ≈⟨ succCong (+-asocc i n (i * n)) ⟩
    succ (i + (n + i * n)) ≈⟨ succCong (+-rightCong (≈-sym (S₈ i n))) ⟩
    succ (i + succ i * n)  ≈⟨ ≈-sym (S₆ i (succ i * n)) ⟩
    succ i + succ i * n    ∎

*-rightCong : ∀ {m n p} → n ≈ p → m * n ≈ m * p
*-rightCong {m} {n} {p} h = S₉ A A0 is m
  where
  A : ℕ → Set
  A i = i * n ≈ i * p

  A0 : A zero
  A0 = zero * n ≈⟨ *-leftZero n ⟩
       zero     ≈⟨ ≈-sym (*-leftZero p) ⟩
       zero * p ∎

  is : ∀ i → A i → A (succ i)
  is i ih = succ i * n ≈⟨ S₈ i n ⟩
            n + i * n  ≈⟨ +-rightCong ih ⟩
            n + i * p  ≈⟨ +-leftCong h ⟩
            p + i * p  ≈⟨ ≈-sym (S₈ i p) ⟩
            succ i * p ∎

*-leftCong : ∀ {m n p} → m ≈ n → m * p ≈ n * p
*-leftCong {m} {n} {p} h = S₉ A A0 is p
  where
  A : ℕ → Set
  A i = m * i ≈ n * i

  A0 : A zero
  A0 = m * zero ≈⟨ *-rightZero m ⟩
       zero     ≈⟨ ≈-sym (*-rightZero n) ⟩
       n * zero ∎

  is : ∀ i → A i → A (succ i)
  is i ih = m * succ i ≈⟨ x*Sy≈x+[x*y] m i ⟩
            m + m * i  ≈⟨ +-leftCong h ⟩
            n + m * i  ≈⟨ +-rightCong ih ⟩
            n + n * i  ≈⟨ ≈-sym (x*Sy≈x+[x*y] n i) ⟩
            n * succ i ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc