text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.FiberedProduct where

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

open import Cubical.Data.Sigma

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

private
  variable
    ℓ : Level

module _ (A B C : CommRing ℓ) (α : CommRingHom A C) (β : CommRingHom B C) where

  private
    module A = CommRingStr (snd A)
    module B = CommRingStr (snd B)
    module C = CommRingStr (snd C)
    module α = IsRingHom (snd α)
    module β = IsRingHom (snd β)

  open CommRingStr
  open CommRingHoms
  open IsRingHom

  fbT : Type ℓ
  fbT = Σ[ ab ∈ fst A × fst B ] (fst α (fst ab) ≡ fst β (snd ab))

  fbT≡ : {x y : fbT} → fst (fst x) ≡ fst (fst y) → snd (fst x) ≡ snd (fst y) → x ≡ y
  fbT≡ h1 h2 = Σ≡Prop (λ _ → is-set (snd C) _ _) λ i → (h1 i) , (h2 i)

  0fbT : fbT
  0fbT = (A.0r , B.0r) , α.pres0 ∙ sym β.pres0

  1fbT : fbT
  1fbT = (A.1r , B.1r) , α.pres1 ∙ sym β.pres1

  _+fbT_ : fbT → fbT → fbT
  ((a1 , b1) , hab1) +fbT ((a2 , b2) , hab2) =
    (a1 A.+ a2 , b1 B.+ b2) , α.pres+ a1 a2 ∙∙ (λ i → hab1 i C.+ hab2 i) ∙∙ sym (β.pres+ b1 b2)

  _·fbT_ : fbT → fbT → fbT
  ((a1 , b1) , hab1) ·fbT ((a2 , b2) , hab2) =
    (a1 A.· a2 , b1 B.· b2) , α.pres· a1 a2 ∙∙ (λ i → hab1 i C.· hab2 i) ∙∙ sym (β.pres· b1 b2)

  -fbT_ : fbT → fbT
  -fbT ((a , b) , hab) = (A.- a , B.- b) , α.pres- a ∙∙ cong C.-_ hab ∙∙ sym (β.pres- b)

  fiberedProduct : CommRing ℓ
  fst fiberedProduct = fbT
  0r (snd fiberedProduct) = 0fbT
  1r (snd fiberedProduct) = 1fbT
  _+_ (snd fiberedProduct) = _+fbT_
  _·_ (snd fiberedProduct) = _·fbT_
  -_ (snd fiberedProduct) = -fbT_
  isCommRing (snd fiberedProduct) =
    makeIsCommRing (isSetΣSndProp (isSet× (is-set (snd A)) (is-set (snd B))) λ x → is-set (snd C) _ _)
                   (λ _ _ _ → fbT≡ (A.+Assoc _ _ _) (B.+Assoc _ _ _))
                   (λ _ → fbT≡ (A.+Rid _) (B.+Rid _))
                   (λ _ → fbT≡ (A.+Rinv _) (B.+Rinv _))
                   (λ _ _ → fbT≡ (A.+Comm _ _) (B.+Comm _ _))
                   (λ _ _ _ → fbT≡ (A.·Assoc _ _ _) (B.·Assoc _ _ _))
                   (λ _ → fbT≡ (A.·Rid _) (B.·Rid _))
                   (λ _ _ _ → fbT≡ (A.·Rdist+ _ _ _) (B.·Rdist+ _ _ _))
                   (λ _ _ → fbT≡ (A.·Comm _ _) (B.·Comm _ _))

  fiberedProductPr₁ : CommRingHom fiberedProduct A
  fst fiberedProductPr₁ = fst ∘ fst
  snd fiberedProductPr₁ = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl)

  fiberedProductPr₂ : CommRingHom fiberedProduct B
  fst fiberedProductPr₂ = snd ∘ fst
  snd fiberedProductPr₂ = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl)

  fiberedProductPr₁₂Commutes : compCommRingHom fiberedProduct A C fiberedProductPr₁ α
                             ≡ compCommRingHom fiberedProduct B C fiberedProductPr₂ β
  fiberedProductPr₁₂Commutes = RingHom≡ (funExt (λ x → x .snd))

  fiberedProductUnivProp :
    (D : CommRing ℓ) (h : CommRingHom D A) (k : CommRingHom D B) →
    compCommRingHom D A C h α ≡ compCommRingHom D B C k β →
    ∃![ l ∈ CommRingHom D fiberedProduct ]
        (h ≡ compCommRingHom D fiberedProduct A l fiberedProductPr₁)
      × (k ≡ compCommRingHom D fiberedProduct B l fiberedProductPr₂)
  fiberedProductUnivProp D (h , hh) (k , hk) H =
    uniqueExists f (RingHom≡ refl , RingHom≡ refl)
                 (λ _ → isProp× (isSetRingHom _ _ _ _) (isSetRingHom _ _ _ _))
                 (λ { (g , _) (Hh , Hk) →
                    RingHom≡ (funExt (λ d → fbT≡ (funExt⁻ (cong fst Hh) d)
                                                 (funExt⁻ (cong fst Hk) d))) })
    where
    f : CommRingHom D fiberedProduct
    fst f d = (h d , k d) , funExt⁻ (cong fst H) d
    snd f = makeIsRingHom (fbT≡ (hh .pres1) (hk .pres1))
                          (λ _ _ → fbT≡ (hh .pres+ _ _) (hk .pres+ _ _))
                          (λ _ _ → fbT≡ (hh .pres· _ _) (hk .pres· _ _))


text:
{-# OPTIONS --without-K #-}
module sets.nat.ordering.leq.decide where

open import decidable
open import sets.core
open import sets.nat.core
open import sets.nat.ordering.leq.core
open import sets.nat.ordering.lt.core

_≤?_ : (n m : ℕ) → Dec (n ≤ m)
0 ≤? m = yes z≤n
suc n ≤? 0 = no λ ()
suc n ≤? suc m with n ≤? m
suc n ≤? suc m | yes p = yes (s≤s p)
suc n ≤? suc m | no u = no λ p → u (ap-pred-≤ p)

ext: agda

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- records are allowed in mutual blocks

module Issue138 where

mutual
  B = Set
  record Foo : Set where

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- This file tests that record constructors are used in error
-- messages, if possible.

module RecordConstructorsInErrorMessages where

record R : Set₁ where
  constructor con
  field
    {A}         : Set
    f           : A → A
    {B C} D {E} : Set
    g           : B → C → E

postulate
  A  : Set
  r₁ : R

r₂ : R
r₂ = record
  { A = A
  ; f = λ x → x
  ; B = A
  ; C = A
  ; D = A
  ; g = λ x _ → x
  }

data _≡_ {A : Set₁} (x : A) : A → Set where
  refl : x ≡ x

foo : r₁ ≡ r₂
foo = refl


text:
-- For the first task, we are asked to prove that max is idempotent and
-- associative. The proves presented in this file are as succint as they
-- possibly can. The proves come with added comments to aid understanding as
-- the proves are meant to be short and simple but not very legible. The
-- solution to task 1 starts in lines 44 and 51.

module sv20.assign2.First where

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat using (_≤_; z≤n; s≤s; _<_)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥-elim)
open import Function using (_∘_)

-- First, we define the max function. Notice, how the function differs from the
-- definition offered for the assignment
max : ℕ → ℕ → ℕ
max zero    n       = n
max (suc m) zero    = suc m
max (suc m) (suc n) = suc (max m n)

-- Nonetheless, we can prove that the definition of max presented in the
-- assignment follows from ours.
-- In athena, the first part of the definition corresponds to the sentence
-- "y < x ==> x max y = x", which translated into Agda corresponds to:
less : ∀ {x y} → y < x → max x y ≡ x
-- and it is easily proven by:
less {zero} ()                       -- Nonesense case
less {suc m} {zero} (s≤s z≤n) = refl -- Simplest case, y ≡ 0
less {suc m} {suc n} (s≤s n<m) = cong suc (less n<m)  -- if "n < m → max m n ≡ m" then "suc n < suc m → max (suc m) (suc n) ≡ (suc m)"

-- The second part of the definition asserts (in Athena) that
-- "~ y < x ==> x max y = y"
not-less : ∀ {x y} → ¬ (y < x) → max x y ≡ y
-- which is easily proven by induction with:
not-less {zero} {n} ¬y<x = refl -- Base case 1
not-less {suc m} {zero} ¬z<sm = ⊥-elim (¬z<sm (s≤s z≤n)) -- Base case 2
not-less {suc m} {suc n} ¬sn<sm = cong suc (not-less (¬sn<sm ∘ s≤s)) -- Inductive case
--not-less {suc m} {suc n} ¬sn<sm = cong suc (not-less {m} {n} (λ n<m → ¬sn<sm (s≤s n<m)))
-- The pattern ¬sn<sm ∘ s≤s means that you are creating a function ¬n<m from ¬sn<sm

-- SOLUTIONS
-- max is idempotent
-- By induction:
max-idem : ∀ x → max x x ≡ x
max-idem zero    = refl                  -- Base case: max 0 0 ≡ 0
max-idem (suc n) = cong suc (max-idem n) -- Inductive case: if "max n n ≡ n" then "max (suc n) (suc n) ≡ suc n" because "max (suc n) (suc n) ≡ suc (max n n)"

-- max is associative
-- By induction:
max-assoc : ∀ x y z → max x (max y z) ≡ max (max x y) z
max-assoc zero    _       _       = refl -- Base cases: when one of the numbers is 0, then "max 0 n ≡ n" by definition of max
max-assoc (suc m) zero    _       = refl --
max-assoc (suc m) (suc n) zero    = refl --
max-assoc (suc m) (suc n) (suc o) = cong suc (max-assoc m n o) -- Inductive case: if "max m (max n o) ≡ max (max m n) o" then "max (suc m) (max (suc n) (suc o)) ≡ suc (max m (max n o)) ≡ suc (max (max m n) o) ≡ max (max (suc m) (suc n)) (suc o)"


text:
module PiFrac.Examples where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Data.Nat
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Maybe

open import PiFrac.Syntax
open import PiFrac.Opsem
open import PiFrac.Eval

-----------------------------------------------------------------------------
-- Patterns and data definitions

pattern 𝔹 = 𝟙 +ᵤ 𝟙
pattern 𝔽 = inj₁ tt
pattern 𝕋 = inj₂ tt

𝔹^ : ℕ → 𝕌
𝔹^ 0 = 𝟙
𝔹^ 1 = 𝔹
𝔹^ (suc (suc n)) = 𝔹 ×ᵤ 𝔹^ (suc n)

-----------------------------------------------------------------------------
-- Adaptors

[A+B]+C=[C+B]+A : ∀ {A B C} → (A +ᵤ B) +ᵤ C ↔ (C +ᵤ B) +ᵤ A
[A+B]+C=[C+B]+A = assocr₊ ⨾ (id↔ ⊕ swap₊) ⨾ swap₊

[A+B]+C=[A+C]+B : ∀ {A B C} → (A +ᵤ B) +ᵤ C ↔ (A +ᵤ C) +ᵤ B
[A+B]+C=[A+C]+B = assocr₊ ⨾ (id↔ ⊕ swap₊) ⨾ assocl₊

[A+B]+[C+D]=[A+C]+[B+D] : {A B C D : 𝕌} → (A +ᵤ B) +ᵤ (C +ᵤ D) ↔ (A +ᵤ C) +ᵤ (B +ᵤ D)
[A+B]+[C+D]=[A+C]+[B+D] = assocl₊ ⨾ (assocr₊ ⊕ id↔) ⨾ ((id↔ ⊕ swap₊) ⊕ id↔) ⨾ (assocl₊ ⊕ id↔) ⨾ assocr₊

Ax[BxC]=Bx[AxC] : {A B C : 𝕌} → A ×ᵤ (B ×ᵤ C) ↔ B ×ᵤ (A ×ᵤ C)
Ax[BxC]=Bx[AxC] = assocl⋆ ⨾ (swap⋆ ⊗ id↔) ⨾  assocr⋆

[AxB]×C=[A×C]xB : ∀ {A B C} → (A ×ᵤ B) ×ᵤ C ↔ (A ×ᵤ C) ×ᵤ B
[AxB]×C=[A×C]xB = assocr⋆ ⨾ (id↔ ⊗ swap⋆) ⨾ assocl⋆

[A×B]×[C×D]=[A×C]×[B×D] : {A B C D : 𝕌} → (A ×ᵤ B) ×ᵤ (C ×ᵤ D) ↔ (A ×ᵤ C) ×ᵤ (B ×ᵤ D)
[A×B]×[C×D]=[A×C]×[B×D] = assocl⋆ ⨾ (assocr⋆ ⊗ id↔) ⨾ ((id↔ ⊗ swap⋆) ⊗ id↔) ⨾ (assocl⋆ ⊗ id↔) ⨾ assocr⋆

-- CNOT(b₁,b₂) = (b₁,b₁ xor b₂)
CNOT : 𝔹 ×ᵤ 𝔹 ↔ 𝔹 ×ᵤ 𝔹
CNOT = dist ⨾ (id↔ ⊕ (id↔ ⊗ swap₊)) ⨾ factor

-- Trace
trace⋆ : ∀ {A B C} → (c : ⟦ C ⟧) → A ×ᵤ C ↔ B ×ᵤ C → A ↔ B
trace⋆ c f = uniti⋆r ⨾ (id↔ ⊗ ηₓ c) ⨾ assocl⋆ ⨾
             (f ⊗ id↔) ⨾
             assocr⋆ ⨾ (id↔ ⊗ εₓ _) ⨾ unite⋆r

ex1 ex2 : Maybe ⟦ 𝟙 +ᵤ 𝟙 ⟧
ex1 = eval (trace⋆ (inj₁ tt) swap⋆) (inj₁ tt) -- just (inj₁ tt)
ex2 = eval (trace⋆ (inj₁ tt) swap⋆) (inj₂ tt) -- nothing

-----------------------------------------------------------------------------
-- Higher-Order Combinators
hof/ : {A B : 𝕌} → (A ↔ B) → (v : ⟦ A ⟧) → (𝟙 ↔ 𝟙/ v ×ᵤ B)
hof/ c v = ηₓ v ⨾ (c ⊗ id↔) ⨾ swap⋆

comp/ : {A B C : 𝕌} {v : ⟦ A ⟧} → (w : ⟦ B ⟧) →
        (𝟙/ v ×ᵤ B) ×ᵤ (𝟙/ w ×ᵤ C) ↔ (𝟙/ v ×ᵤ C)
comp/ w = assocl⋆ ⨾ (assocr⋆ ⊗ id↔) ⨾ ((id↔ ⊗ εₓ w) ⊗ id↔) ⨾ (unite⋆r ⊗ id↔)

app/ : {A B : 𝕌} → (v : ⟦ A ⟧) → (𝟙/ v ×ᵤ B) ×ᵤ A ↔ B
app/ v = swap⋆ ⨾ assocl⋆ ⨾ (εₓ _ ⊗ id↔) ⨾ unite⋆l

curry/ : {A B C : 𝕌} → (A ×ᵤ B ↔ C) → (v : ⟦ B ⟧) → (A ↔ 𝟙/ v ×ᵤ C)
curry/ c v = uniti⋆l ⨾ (ηₓ v ⊗ id↔) ⨾ swap⋆ ⨾ assocl⋆ ⨾ (c ⊗ id↔) ⨾ swap⋆

-- h.o. version of cnot specialized to input input (v , w)

htf : ∀ (v w : _) → 𝟙 ↔ 𝟙/ (v , w) ×ᵤ (𝔹 ×ᵤ 𝔹)
htf v w = hof/ CNOT (v , w)

-- applying htf to incoming input
htfc : ∀ (v w : _) → (𝔹 ×ᵤ 𝔹) ↔ (𝔹 ×ᵤ 𝔹)
htfc v w = uniti⋆l ⨾ (htf v w ⊗ id↔) ⨾ app/ (v , w)

htfca : ⟦ 𝔹 ×ᵤ 𝔹 ⟧ → Maybe ⟦ 𝔹 ×ᵤ 𝔹 ⟧
htfca (v , w) = eval (htfc v w) (v , w)

x1 x2 x3 x4 : Maybe ⟦ 𝔹 ×ᵤ 𝔹 ⟧
x1 = htfca (𝔽 , 𝔽) -- just (𝔽 , 𝔽)
x2 = htfca (𝔽 , 𝕋) -- just (𝔽 , 𝕋)
x3 = htfca (𝕋 , 𝔽) -- just (𝕋 , 𝕋)
x4 = htfca (𝕋 , 𝕋) -- just (𝕋 , 𝔽)

-----------------------------------------------------------------------------
-- Algebraic Identities
inv/ : {A : 𝕌} {v : ⟦ A ⟧} → A ↔ (𝟙/_ {𝟙/ v} ↻)
inv/ = uniti⋆r ⨾ (id↔ ⊗ ηₓ _) ⨾ assocl⋆ ⨾ (εₓ _ ⊗ id↔) ⨾ unite⋆l

dist/ : {A B : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} → 𝟙/ (a , b) ↔ 𝟙/ a ×ᵤ 𝟙/ b
dist/ {A} {B} {a} {b} =
  uniti⋆l ⨾ (ηₓ b ⊗ id↔) ⨾ uniti⋆l ⨾ (ηₓ a ⊗ id↔) ⨾ assocl⋆ ⨾
  ([A×B]×[C×D]=[A×C]×[B×D] ⊗ id↔) ⨾
  (swap⋆ ⊗ id↔) ⨾ assocr⋆ ⨾ (id↔ ⊗ εₓ (a , b)) ⨾ unite⋆r

neg/ : {A B : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} → (A ↔ B) → (𝟙/ a ↔ 𝟙/ b)
neg/ {A} {B} {a} {b} c =
  uniti⋆r ⨾ (id↔ ⊗ ηₓ _) ⨾
  (id↔ ⊗ (! c) ⊗ id↔) ⨾ assocl⋆ ⨾
  ((swap⋆ ⨾ εₓ _) ⊗ id↔) ⨾ unite⋆l

fracDist : ∀ {A B} {a : ⟦ A ⟧} {b : ⟦ B ⟧} → 𝟙/ a ×ᵤ 𝟙/ b ↔ 𝟙/ (a , b)
fracDist =
  uniti⋆l ⨾ ((ηₓ _ ⨾ swap⋆) ⊗ id↔) ⨾ assocr⋆ ⨾
  (id↔ ⊗ ([A×B]×[C×D]=[A×C]×[B×D] ⨾ (εₓ _ ⊗ εₓ _) ⨾ unite⋆l)) ⨾ unite⋆r

mulFrac : ∀ {A B C D} {b : ⟦ B ⟧} {d : ⟦ D ⟧}
        → (A ×ᵤ 𝟙/ b) ×ᵤ (C ×ᵤ 𝟙/ d) ↔ (A ×ᵤ C) ×ᵤ (𝟙/ (b , d))
mulFrac = [A×B]×[C×D]=[A×C]×[B×D] ⨾ (id↔ ⊗ fracDist)

addFracCom : ∀ {A B C} {v : ⟦ C ⟧}
        → (A ×ᵤ 𝟙/ v) +ᵤ (B ×ᵤ 𝟙/ v) ↔ (A +ᵤ B) ×ᵤ (𝟙/ v)
addFracCom = factor

addFrac : ∀ {A B C D} → (v : ⟦ C ⟧) → (w : ⟦ D ⟧)
        → (A ×ᵤ 𝟙/_ {C} v) +ᵤ (B ×ᵤ 𝟙/_ {D} w) ↔
         ((A ×ᵤ D) +ᵤ (C ×ᵤ B)) ×ᵤ (𝟙/_ {C ×ᵤ D} (v , w))
addFrac v w = ((uniti⋆r ⨾ (id↔ ⊗ ηₓ w)) ⊕ (uniti⋆l  ⨾ (ηₓ v ⊗ id↔))) ⨾
              [A×B]×[C×D]=[A×C]×[B×D] ⊕ [A×B]×[C×D]=[A×C]×[B×D] ⨾
              ((id↔ ⊗ fracDist) ⊕ (id↔ ⊗ fracDist)) ⨾ factor


text:
------------------------------------------------------------------------------
-- The map-iterate property: A property using co-induction
------------------------------------------------------------------------------

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

-- The map-iterate property (Gibbons and Hutton, 2005):
-- map f (iterate f x) = iterate f (f · x)

module FOTC.Program.MapIterate.MapIterateATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Relation.Binary.Bisimilarity.Type

------------------------------------------------------------------------------
-- The map-iterate property.
≈-map-iterate : ∀ f x → map f (iterate f x) ≈ iterate f (f · x)
≈-map-iterate f x = ≈-coind B h₁ h₂
  where
  -- Based on the relation used by (Giménez and Castéran, 2007).
  B : D → D → Set
  B xs ys = ∃[ y ] xs ≡ map f (iterate f y) ∧ ys ≡ iterate f (f · y)
  {-# ATP definition B #-}

  postulate
    h₁ : ∀ {xs} {ys} → B xs ys →
         ∃[ x' ] ∃[ xs' ] ∃[ ys' ] xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ B xs' ys'
  {-# ATP prove h₁ #-}

  postulate h₂ : B (map f (iterate f x)) (iterate f (f · x))
  {-# ATP prove h₂ #-}

------------------------------------------------------------------------------
-- References
--
-- Giménez, Eduardo and Casterán, Pierre (2007). A Tutorial on
-- [Co-]Inductive Types in Coq.
--
-- Gibbons, Jeremy and Hutton, Graham (2005). Proof Methods for
-- Corecursive Programs. Fundamenta Informaticae XX, pp. 1–14.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Prelude
open import Nat
open import Bij

module NatDelta where

  instance
    NatBij : bij Nat Nat
    NatBij = record {
      convert = λ n → n;
      inj     = λ n → n;
      surj    = λ n → n , refl}

  open import Delta Nat {{NatBij}}

  nat-dd = dd

max_stars_repo_name: nickcollins/dependent-dicts-agda

max_issues_repo_name: nickcollins/dependent-dicts-agda

max_forks_repo_name: nickcollins/dependent-dicts-agda


text:
module Utils.HaskellTypes where

postulate String : Set
{-# BUILTIN STRING String #-}

data Unit : Set where
  triv : Unit
{-# COMPILED_DATA Unit () () #-}

data Prod (A : Set) (B : Set) : Set where
  _,_ : A → B → Prod A B
{-# COMPILED_DATA Prod (,) (,) #-}

data Triple (A B C : Set) : Set where
  triple : A → B → C → Triple A B C
{-# COMPILED_DATA Triple (,,) (,,) #-}

infixr 20 _::_
data List (A : Set) : Set where
  [] : List A
  _::_ : A → List A → List A
{-# COMPILED_DATA List [] [] (:) #-}

max_stars_repo_name: heades/Agda-LLS

max_issues_repo_name: heades/Agda-LLS

max_forks_repo_name: heades/Agda-LLS


text:
module Numeral.Natural.Relation.DivisibilityWithRemainder.Proofs where

import      Lvl
open import Data
open import Data.Boolean.Stmt
open import Functional
open import Logic.Predicate
open import Logic.Propositional
open import Numeral.Finite
import      Numeral.Finite.Proofs as 𝕟
open import Numeral.Natural
open import Numeral.Natural.Inductions
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.Proofs.Order
open import Numeral.Natural.Relation.DivisibilityWithRemainder hiding (base₀ ; base₊ ; step)
open import Numeral.Natural.Relation.Order.Decidable
open import Numeral.Natural.Relation.Order.Proofs
open import Numeral.Natural.Relation.Order
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function
open import Structure.Operator
open import Structure.Operator.Proofs.Util
open import Structure.Relator
open import Syntax.Transitivity
open import Type.Properties.Decidable.Proofs

-- 0 does not divide anything with any remainder.
[∣ᵣₑₘ]-0-divides : ∀{x}{r} → ¬(0 ∣ᵣₑₘ x)(r)
[∣ᵣₑₘ]-0-divides {r = ()}

-- 1 divides everything with the only possible remainder 0.
[∣ᵣₑₘ]-1-divides : ∀{x}{r} → (1 ∣ᵣₑₘ x)(r)
[∣ᵣₑₘ]-1-divides {𝟎}   {r = 𝟎} = DivRem𝟎
[∣ᵣₑₘ]-1-divides {𝐒 x} {r = 𝟎} = DivRem𝐒 [∣ᵣₑₘ]-1-divides

-- The quotient is the dividend when divided by 1.
[∣ᵣₑₘ]-quotient-of-1 : ∀{x}{r} → (p : (1 ∣ᵣₑₘ x)(r)) → ([∣ᵣₑₘ]-quotient p ≡ x)
[∣ᵣₑₘ]-quotient-of-1 {𝟎}  {𝟎} DivRem𝟎     = [≡]-intro
[∣ᵣₑₘ]-quotient-of-1 {𝐒 x}{𝟎} (DivRem𝐒 p) = [≡]-with(𝐒) ([∣ᵣₑₘ]-quotient-of-1 {x}{𝟎} p)

-- [∣ᵣₑₘ]-remainder-dividend : ∀{x y}{r : 𝕟(y)} → (x < y) → (y ∣ᵣₑₘ x)(r) → (x ≡ 𝕟-to-ℕ r)

-- How the arguments in the divisibility relation is related to each other by elementary functions.
-- Note: The division theorem is proven using this. By proving that [∣ᵣₑₘ]-quotient and [∣ᵣₑₘ]-remainder is equal to the algorithmic functions of floored division and modulo, the theorem follows directly from this.
[∣ᵣₑₘ]-is-division-with-remainder : ∀{x y}{r} → (p : (y ∣ᵣₑₘ x)(r)) → ((([∣ᵣₑₘ]-quotient p) ⋅ y) + (𝕟-to-ℕ ([∣ᵣₑₘ]-remainder p)) ≡ x)
[∣ᵣₑₘ]-is-division-with-remainder {𝟎}             {_}   {𝟎}   DivRem𝟎 = [≡]-intro
[∣ᵣₑₘ]-is-division-with-remainder {𝐒 .(x + y)}    {𝐒 y} {𝟎}   (DivRem𝐒 {x = x} p) =
  𝐒([∣ᵣₑₘ]-quotient p) ⋅ 𝐒(y)         🝖[ _≡_ ]-[ [⋅]-with-[𝐒]ₗ {[∣ᵣₑₘ]-quotient p}{𝐒(y)} ]
  (([∣ᵣₑₘ]-quotient p) ⋅ 𝐒(y)) + 𝐒(y) 🝖[ _≡_ ]-[]
  𝐒((([∣ᵣₑₘ]-quotient p) ⋅ 𝐒(y)) + y) 🝖[ _≡_ ]-[ congruence₁(𝐒) (congruence₂ₗ(_+_)(y) ([∣ᵣₑₘ]-is-division-with-remainder p)) ]
  𝐒(x + y)                            🝖-end
[∣ᵣₑₘ]-is-division-with-remainder {𝐒 .(𝕟-to-ℕ r)} {𝐒 y} {𝐒 r} DivRem𝟎 = [≡]-intro
[∣ᵣₑₘ]-is-division-with-remainder {𝐒 .(x + y)} {𝐒(y@(𝐒 _))} {r@(𝐒 _)} (DivRem𝐒 {x = x} p) =
  (([∣ᵣₑₘ]-quotient (DivRem𝐒 p)) ⋅ 𝐒(y)) + (𝕟-to-ℕ r) 🝖[ _≡_ ]-[]
  (𝐒([∣ᵣₑₘ]-quotient p) ⋅ 𝐒(y))          + (𝕟-to-ℕ r) 🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(𝕟-to-ℕ r) ([⋅]-with-[𝐒]ₗ {[∣ᵣₑₘ]-quotient p}{𝐒(y)}) ]
  ((([∣ᵣₑₘ]-quotient p) ⋅ 𝐒(y)) + 𝐒(y))  + (𝕟-to-ℕ r) 🝖[ _≡_ ]-[ One.commuteᵣ-assocₗ {a = ([∣ᵣₑₘ]-quotient p) ⋅ 𝐒(y)}{b = 𝐒(y)}{c = 𝕟-to-ℕ r} ]
  ((([∣ᵣₑₘ]-quotient p) ⋅ 𝐒(y)) + (𝕟-to-ℕ r)) + 𝐒(y)  🝖[ _≡_ ]-[]
  𝐒(((([∣ᵣₑₘ]-quotient p) ⋅ 𝐒(y)) + (𝕟-to-ℕ r)) + y)  🝖[ _≡_ ]-[ congruence₁(𝐒) (congruence₂ₗ(_+_)(y) ([∣ᵣₑₘ]-is-division-with-remainder p)) ]
  𝐒(x + y)                                                 🝖-end

-- When the arguments in the divisibility relation are related to each other.
-- This also indicates that the divisibility relation actually states something about divisibility in the sense of the inverse of multiplication.
[∣ᵣₑₘ]-equivalence : ∀{x y}{r} → (y ∣ᵣₑₘ x)(r) ↔ ∃(q ↦ (q ⋅ y) + (𝕟-to-ℕ r) ≡ x)
[∣ᵣₑₘ]-equivalence = [↔]-intro (p ↦ l {q = [∃]-witness p} ([∃]-proof p)) (p ↦ [∃]-intro ([∣ᵣₑₘ]-quotient p) ⦃ [∣ᵣₑₘ]-is-division-with-remainder p ⦄) where
  l :  ∀{x y q}{r} → ((q ⋅ y) + (𝕟-to-ℕ r) ≡ x) → (y ∣ᵣₑₘ x)(r)
  l {_}{_}{𝟎}  {_} [≡]-intro = DivRem𝟎
  l {x}{y}{𝐒 q}{r} p = substitute₁(x ↦ (y ∣ᵣₑₘ x)(r)) eq (DivRem𝐒 (l{(q ⋅ y) + (𝕟-to-ℕ r)}{y}{q}{r} [≡]-intro)) where
    eq =
      ((q ⋅ y) + (𝕟-to-ℕ r)) + y 🝖[ _≡_ ]-[ One.commuteᵣ-assocₗ {a = q ⋅ y}{b = 𝕟-to-ℕ r}{c = y} ]
      ((q ⋅ y) + y) + (𝕟-to-ℕ r) 🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(𝕟-to-ℕ r) ([⋅]-with-[𝐒]ₗ {q}{y}) ]-sym
      (𝐒(q) ⋅ y) + (𝕟-to-ℕ r)    🝖[ _≡_ ]-[ p ]
      x                          🝖-end

-- ⌊/⌋-when-zero : ∀{x y} → (x ⌊/⌋ 𝐒(y) ≡ 𝟎) → (x ≡ 0)
-- ⌊/⌋-when-positive : ∀{x y q} → (x ⌊/⌋ 𝐒(y) ≡ 𝐒(q)) → ∃(x₀ ↦ (x ≡ x₀ + 𝐒(y)))

{-
[∣ᵣₑₘ]-existence : ∀{x y} → ∃(𝐒(y) ∣ᵣₑₘ x)
∃.witness ([∣ᵣₑₘ]-existence {x} {y}) = ℕ-to-𝕟 (x mod 𝐒(y)) ⦃ {![↔]-to-[→] decide-is-true mod-maxᵣ!} ⦄
∃.proof   ([∣ᵣₑₘ]-existence {x} {y}) = [↔]-to-[←] [∣ᵣₑₘ]-equivalence ([∃]-intro (x ⌊/⌋ 𝐒(y)) ⦃ {!TODO: Insert division theorem here!} ⦄)
-}

DivRem𝟎Alt : ∀{x y} → (xy : (x < y)) → (y ∣ᵣₑₘ x)(ℕ-to-𝕟 x ⦃ [↔]-to-[→] decider-true xy ⦄)
DivRem𝟎Alt {x} {𝐒 y} (succ p) = [≡]-substitutionᵣ (𝕟.𝕟-ℕ-inverse) {expr ↦ (𝐒 y ∣ᵣₑₘ expr)(ℕ-to-𝕟 x)} ((DivRem𝟎{𝐒(y)}{ℕ-to-𝕟 x})) where
  instance
    x<𝐒y : IsTrue (x <? 𝐒(y))
    x<𝐒y = [↔]-to-[→] decider-true ([≤]-with-[𝐒] ⦃ p ⦄)

DivRem𝐒Alt : ∀{x y}{r : 𝕟(y)} → (x ≥ y) → (y ∣ᵣₑₘ x −₀ y)(r) → (y ∣ᵣₑₘ x)(r)
DivRem𝐒Alt{x}{𝟎}{}
DivRem𝐒Alt{x}{𝐒(y)}{r} xy = [≡]-substitutionᵣ ([↔]-to-[→] ([−₀][+]-nullify2ᵣ{𝐒(y)}{x}) xy) {\expr → (𝐒(y) ∣ᵣₑₘ expr) r} ∘ DivRem𝐒{𝐒(y)}{x −₀ 𝐒(y)}{r}

-- Every pair of numbers (positive divisor) when divided will yield a remainder and there is always a proof of it being the case.
-- This is an alternative way of constructing the modulo operator.
[∣ᵣₑₘ]-existence-alt : ∀{x y} → ∃(𝐒(y) ∣ᵣₑₘ x)
[∣ᵣₑₘ]-existence-alt {x} {y} = [ℕ]-strong-induction {φ = x ↦ ∃(𝐒(y) ∣ᵣₑₘ x)} base step {x} where
  base : ∃(𝐒(y) ∣ᵣₑₘ 𝟎)
  base = [∃]-intro 𝟎 ⦃ DivRem𝟎 ⦄

  step : ∀{i} → (∀{j} → (j ≤ i) → ∃(𝐒(y) ∣ᵣₑₘ j)) → ∃(𝐒(y) ∣ᵣₑₘ 𝐒(i))
  step{i} p with [≤][>]-dichotomy {y}{i}
  ... | [∨]-introₗ yi = [∃]-map-proof (DivRem𝐒Alt([≤]-with-[𝐒] ⦃ yi ⦄)) (p{𝐒(i) −₀ 𝐒(y)} ([−₀]-lesser {i}{y}))
  ... | [∨]-introᵣ 𝐒iy = [∃]-intro (ℕ-to-𝕟 (𝐒(i)) ⦃ [↔]-to-[→] decider-true 𝐒iy ⦄) ⦃ DivRem𝟎Alt ([≤]-with-[𝐒] ⦃ 𝐒iy ⦄) ⦄

{-
open import Structure.Setoid.Uniqueness
{-[∣ᵣₑₘ]-uniqueness : ∀{x y}{p : ∃(𝐒(y) ∣ᵣₑₘ x)} → (p ≡ [∣ᵣₑₘ]-existence)
[∣ᵣₑₘ]-uniqueness {.(𝕟-to-ℕ r)} {y} {[∃]-intro r ⦃ DivRem𝟎 ⦄} = {![≡]-intro!}
[∣ᵣₑₘ]-uniqueness {.(x + 𝐒 y)} {y} {[∃]-intro r ⦃ DivRem𝐒 {x = x} p ⦄} = {!!}-}
{-[∣ᵣₑₘ]-unique-remainder : ∀{x y} → Unique(𝐒(y) ∣ᵣₑₘ x)
[∣ᵣₑₘ]-unique-remainder {.(𝕟-to-ℕ a)} {y} {a} {b} DivRem𝟎 q = {!!}
[∣ᵣₑₘ]-unique-remainder {.(x + 𝐒 y)} {y} {a} {b} (DivRem𝐒 {x = x} p) q = {!!}-}
open import Type.Properties.MereProposition
[∣ᵣₑₘ]-mereProposition : ∀{x y}{r : 𝕟(𝐒(y))} → MereProposition((𝐒(y) ∣ᵣₑₘ x)(r))
[∣ᵣₑₘ]-mereProposition = intro proof where
  proof : ∀{x y}{r : 𝕟(𝐒(y))}{p q : (𝐒(y) ∣ᵣₑₘ x)(r)} → (p ≡ q)
  proof {.(𝕟-to-ℕ r)} {y} {r} {DivRem𝟎} {q} = {!!}
  proof {.(x + 𝐒 y)} {y} {r} {DivRem𝐒 {x = x} p} {q} = {!p!}

  -- testor : ∀{y x}{r : 𝕟(𝐒 y)}{p : (𝐒(y) ∣ᵣₑₘ x)(r)} → (p ≡ DivRem𝟎) ∨ ∃(q ↦ (p ≡ DivRem𝐒 q))

  -- TODO: Maybe by injectivity of 𝕟-to-ℕ?
  test : ∀{y}{r : 𝕟(𝐒 y)}{p : (𝐒(y) ∣ᵣₑₘ (𝕟-to-ℕ r))(r)} → (p ≡ DivRem𝟎)
{-  test {y} {r} {p} with 𝕟-to-ℕ r
  test {_} {_} {_} | 𝟎 = {!!}-}
-}

{-
open import Data.Tuple using (_⨯_ ; _,_)
open import Type.Dependent
open import Type.Properties.MereProposition
[∣ᵣₑₘ]-mereProposition : ∀{x y}{r : 𝕟(y)} → MereProposition((y ∣ᵣₑₘ x)(r))
[∣ᵣₑₘ]-mereProposition = intro {!!} where
  proof : ∀{y}{r : 𝕟(y)} → (p q : Σ(ℕ) (x ↦ (y ∣ᵣₑₘ x)(r))) → (p ≡ q)
  proof {y} {r} (intro .(𝕟-to-ℕ r) DivRem𝟎) (intro .(𝕟-to-ℕ r) DivRem𝟎) = [≡]-intro
  proof {y} {r} (intro .(𝕟-to-ℕ r) DivRem𝟎) (intro .(x₂ + y) (DivRem𝐒{x = x₂} p₂)) = {!!}
  proof {y} {r} (intro .(x₁ + y) (DivRem𝐒{x = x₁} p₁)) (intro .(𝕟-to-ℕ r) DivRem𝟎) = {!!}
  proof {y} {r} (intro .(x₁ + y) (DivRem𝐒{x = x₁} p₁)) (intro .(x₂ + y) (DivRem𝐒{x = x₂} p₂)) = {!congruence₂ₗ(_+_)(y) (congruence₁(Σ.left) eq)!} where
    eq = proof (intro x₁ p₁) (intro x₂ p₂)
    test : ∀{a₁ a₂ : A}{b₁ : B(a₁)}{b₂ : B(a₂)} → (a₁ ≡ a₂) → (intro a₁ b₁ ≡ intro a₂ b₂)
-}

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:
{-

  Maybe structure: X ↦ Maybe (S X)

-}
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Structures.Maybe where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.SIP
open import Cubical.Functions.FunExtEquiv

open import Cubical.Data.Unit
open import Cubical.Data.Empty
open import Cubical.Data.Maybe

private
  variable
    ℓ ℓ₁ ℓ₁' : Level

MaybeRel : {A B : Type ℓ} (R : A → B → Type ℓ₁) → Maybe A → Maybe B → Type ℓ₁
MaybeRel R nothing nothing = Lift Unit
MaybeRel R nothing (just _) = Lift ⊥
MaybeRel R (just _) nothing = Lift ⊥
MaybeRel R (just x) (just y) = R x y

congMaybeRel : {A B : Type ℓ} {R : A → B → Type ℓ₁} {S : A → B → Type ℓ₁'}
  → (∀ x y → R x y ≃ S x y)
  → ∀ ox oy → MaybeRel R ox oy ≃ MaybeRel S ox oy
congMaybeRel e nothing nothing = Lift≃Lift (idEquiv _)
congMaybeRel e nothing (just _) = Lift≃Lift (idEquiv _)
congMaybeRel e (just _) nothing = Lift≃Lift (idEquiv _)
congMaybeRel e (just x) (just y) = e x y

module MaybePathP where

  Code : (A : I → Type ℓ) → Maybe (A i0) → Maybe (A i1) → Type ℓ
  Code A = MaybeRel (PathP A)

  encodeRefl : {A : Type ℓ} → ∀ ox → Code (λ _ → A) ox ox
  encodeRefl nothing = lift tt
  encodeRefl (just _) = refl

  encode : (A : I → Type ℓ) → ∀ ox oy → PathP (λ i → Maybe (A i)) ox oy → Code A ox oy
  encode A ox oy p = transport (λ j → Code (λ i → A (i ∧ j)) ox (p j)) (encodeRefl ox)

  decode : {A : I → Type ℓ} → ∀ ox oy → Code A ox oy → PathP (λ i → Maybe (A i)) ox oy
  decode nothing nothing p i = nothing
  decode (just _) (just _) p i = just (p i)

  decodeEncodeRefl : {A : Type ℓ} (ox : Maybe A) → decode ox ox (encodeRefl ox) ≡ refl
  decodeEncodeRefl nothing = refl
  decodeEncodeRefl (just _) = refl

  decodeEncode : {A : I → Type ℓ} → ∀ ox oy p → decode ox oy (encode A ox oy p) ≡ p
  decodeEncode {A = A} ox oy p =
    transport
      (λ k →
        decode _ _ (transp (λ j → Code (λ i → A (i ∧ j ∧ k)) ox (p (j ∧ k))) (~ k) (encodeRefl ox))
        ≡ (λ i → p (i ∧ k)))
      (decodeEncodeRefl ox)

  encodeDecode : (A : I → Type ℓ) → ∀ ox oy c → encode A ox oy (decode ox oy c) ≡ c
  encodeDecode A nothing nothing c = refl
  encodeDecode A (just x) (just y) c =
    transport
      (λ k →
        encode (λ i → A (i ∧ k)) _ _ (decode (just x) (just (c k)) (λ i → c (i ∧ k)))
        ≡ (λ i → c (i ∧ k)))
      (transportRefl _)

  Code≃PathP : {A : I → Type ℓ} → ∀ ox oy → Code A ox oy ≃ PathP (λ i → Maybe (A i)) ox oy
  Code≃PathP {A = A} ox oy = isoToEquiv isom
    where
    isom : Iso _ _
    isom .Iso.fun = decode ox oy
    isom .Iso.inv = encode _ ox oy
    isom .Iso.rightInv = decodeEncode ox oy
    isom .Iso.leftInv = encodeDecode A ox oy

-- Structured isomorphisms

MaybeStructure : (S : Type ℓ → Type ℓ₁) → Type ℓ → Type ℓ₁
MaybeStructure S X = Maybe (S X)

MaybeEquivStr : {S : Type ℓ → Type ℓ₁}
  → StrEquiv S ℓ₁' → StrEquiv (MaybeStructure S) ℓ₁'
MaybeEquivStr ι (X , ox) (Y , oy) e = MaybeRel (λ x y → ι (X , x) (Y , y) e) ox oy

maybeUnivalentStr : {S : Type ℓ → Type ℓ₁} (ι : StrEquiv S ℓ₁')
  → UnivalentStr S ι → UnivalentStr (MaybeStructure S) (MaybeEquivStr ι)
maybeUnivalentStr ι θ {X , ox} {Y , oy} e =
  compEquiv
    (congMaybeRel (λ x y → θ {X , x} {Y , y} e) ox oy)
    (MaybePathP.Code≃PathP ox oy)

maybeEquivAction : {S : Type ℓ → Type ℓ₁}
  → EquivAction S → EquivAction (MaybeStructure S)
maybeEquivAction α e = congMaybeEquiv (α e)

maybeTransportStr : {S : Type ℓ → Type ℓ₁} (α : EquivAction S)
  → TransportStr α → TransportStr (maybeEquivAction α)
maybeTransportStr _ τ e nothing = refl
maybeTransportStr _ τ e (just x) = cong just (τ e x)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import Cubical.Core.Everything

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

-- A helper module for deriving univalence for a higher inductive-recursive
-- universe.
--
--  U is the type of codes
--  El is the decoding
--  uaf is a higher constructor that requires paths between codes to exist
--    for equivalences of decodings
--  comp is intended to be the computational behavior of El on uaf, although
--    it seems that being a path is sufficient.
--  ret is a higher constructor that fills out the equivalence structure
--    for uaf and the computational behavior of El.
--
-- Given a universe defined as above, it's possible to show that the path
-- space of the code type is equivalent to the path space of the actual
-- decodings, which are themselves determined by equivalences.
--
-- The levels are left independent, but of course it will generally be
-- impossible to define this sort of universe unless ℓ' < ℓ, because El will
-- be too big to go in a constructor of U. The exception would be if U could
-- be defined independently of El, though it might be tricky to get the right
-- higher structure in such a case.
module Cubical.Foundations.Univalence.Universe {ℓ ℓ'}
    (U : Type ℓ)
    (El : U → Type ℓ')
    (uaf : ∀{s t} → El s ≃ El t → s ≡ t)
    (comp : ∀{s t} (e : El s ≃ El t) → cong El (uaf e) ≡ ua e)
    (ret : ∀{s t : U} → (p : s ≡ t) → uaf (lineToEquiv (λ i → El (p i))) ≡ p)
  where

minivalence : ∀{s t} → (s ≡ t) ≃ (El s ≡ El t)
minivalence {s} {t} = isoToEquiv mini
  where
  open Iso
  mini : Iso (s ≡ t) (El s ≡ El t)
  mini .fun = cong El
  mini .inv = uaf ∘ pathToEquiv
  mini .rightInv p = comp (pathToEquiv p) ∙ uaη p
  mini .leftInv = ret

isEmbeddingEl : isEmbedding El
isEmbeddingEl s t = snd minivalence

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module Main where
open import IO
open import Data.String
open import Data.List
open import Data.Bool

{-# IMPORT AST #-}

{-# COMPILED_TYPE String AST.Type #-}
{-# COMPILED_TYPE String AST.Identifier #-}

data Variable : Set where
  V : String → String → Variable

varName : Variable → String
varName (V _ name) = name

{-# COMPILED_DATA Variable AST.Variable AST.Variable #-}

data Expression : Set where
  New : String → List Expression → Expression
  FieldAccess : String → Expression → String → Expression
  MethodCall : String → Expression → String → List Expression → Expression
  Var : String → String → Expression

exprType : Expression → String
exprType (New t _) = t
exprType (FieldAccess t _ _) = t
exprType (MethodCall t _ _ _) = t
exprType (Var t _) = t

{-# COMPILED_DATA Expression AST.Expression AST.New AST.FieldAccess AST.MethodCall AST.Var #-}

data Method : Set where
  Mth : String → List Variable → Expression → Method

{-# COMPILED_DATA Method AST.Method AST.Method #-}

data Constructor : Set where
  Cons : List Variable → Constructor

{-# COMPILED_DATA Constructor AST.Constructor AST.Constructor #-}

data Pair (A B : Set) : Set where
  P : A → B → Pair A B

{-# COMPILED_DATA Pair (,) (,) #-}

data SimpleMap (A B : Set) : Set where
  SM : List (Pair A B) → SimpleMap A B

{-# COMPILED_DATA SimpleMap AST.SimpleMap AST.SimpleMap #-}

data Class : Set where
  Cls : String → SimpleMap String String → Constructor → SimpleMap String Method → Class

{-# COMPILED_DATA Class AST.Class AST.Class #-}

data Program : Set where
  Prog : SimpleMap String Class → Program

{-# COMPILED_DATA Program AST.Program AST.Program #-}

postulate
  parseUnsafe : String → Program
  showProgram : Program → String
  getValue : {A B : Set} → A → SimpleMap A B → B

{-# COMPILED parseUnsafe AST.parseUnsafe #-}
{-# COMPILED showProgram AST.showProgram #-}

infixr 5 _++l_

_++l_ : ∀ {a} {A : Set a} → List A → List A → List A
xs ++l ys = Data.List._++_ xs ys

{-# NO_TERMINATION_CHECK #-}
subst : Pair String Expression → Expression → Expression
subst substExpr (New t ps) = New t (map (subst substExpr) ps)
subst substExpr (FieldAccess t e f) = FieldAccess t (subst substExpr e) f
subst substExpr (MethodCall t e m ps) = MethodCall t (subst substExpr e) m (map (subst substExpr) ps)
subst (P name expr) (Var t vName) = if name == vName then expr else (Var t vName)

getMethod : Program → String → String → Method
getMethod (Prog classes) clsName mthName with getValue clsName classes
... | Cls _ _ _ methods = getValue mthName methods

reduceInvk : Program → Expression → String → List Expression → Expression
reduceInvk p e mthName params with getMethod p (exprType e) mthName
... | Mth _ vars body = foldr subst body ((P "this" e) ∷ (zipWith P (map varName vars) params))

data Reduce {Pr : Program} : Expression → Expression → Set where
  RInvk : ∀ {t consParams mthType mthName mthParams} → Reduce {Pr} (MethodCall mthType (New t consParams) mthName mthParams) (reduceInvk Pr (New t consParams) mthName mthParams)
  RCField : ∀ {e₁ e₂ t f} → Reduce {Pr} e₁ e₂ → Reduce {Pr} (FieldAccess t e₁ f) (FieldAccess t e₂ f)
  RCInvk : ∀ {e₁ e₂ t m p} → Reduce {Pr} e₁ e₂ → Reduce {Pr} (MethodCall t e₁ m p) (MethodCall t e₂ m p)
  RCInvkArg : ∀ {e e₁ e₂ t m p₁ p₂} → Reduce {Pr} e₁ e₂ → Reduce {Pr} (MethodCall t e m (p₁ ++l [ e₁ ] ++l p₂)) (MethodCall t e m (p₁ ++l [ e₂ ] ++l p₂))
  RCNewArg : ∀ {e₁ e₂ t p₁ p₂} → Reduce {Pr} e₁ e₂ → Reduce {Pr} (New t (p₁ ++l [ e₁ ] ++l p₂)) (New t (p₁ ++l [ e₂ ] ++l p₂))

main = run (putStrLn (showProgram (parseUnsafe "class A extends Object { A() {super();} }")))

max_stars_repo_name: ademinn/RefactoringVerification

max_issues_repo_name: ademinn/RefactoringVerification

max_forks_repo_name: ademinn/RefactoringVerification


text:
module trees where

  data Tree (A : Set) : Set where
    empty : Tree A
    node : Tree A -> A -> Tree A -> Tree A

  open import Data.Nat

  #nodes : {A : Set} -> Tree A -> ℕ
  #nodes empty = 0
  #nodes (node t x t₁) = (#nodes t) + (1 + (#nodes t₁))

  #leafs : {A : Set} -> Tree A -> ℕ
  #leafs empty = zero
  -- #leafs (node empty x empty) = 1
  #leafs (node t x t₁) with t | t₁
  ...                     | empty | empty = 1
  ...                     | _     | _ = (#leafs t) + (#leafs t₁)

max_stars_repo_name: hablapps/safeoptics

max_issues_repo_name: hablapps/safeoptics

max_forks_repo_name: hablapps/safeoptics


text:
------------------------------------------------------------------------
-- Queue instances for the queues in Queue.Truncated
------------------------------------------------------------------------

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

import Equality.Path as P
open import Prelude
import Queue

module Queue.Truncated.Instances
  {e⁺}
  (eq : ∀ {a p} → P.Equality-with-paths a p e⁺)
  (open P.Derived-definitions-and-properties eq)

  {Q : ∀ {ℓ} → Type ℓ → Type ℓ}
  ⦃ is-queue :
      ∀ {ℓ} →
      Queue.Is-queue equality-with-J Q (λ _ → ↑ _ ⊤) ℓ ⦄
  ⦃ is-queue-with-map :
      ∀ {ℓ₁ ℓ₂} →
      Queue.Is-queue-with-map equality-with-J Q ℓ₁ ℓ₂ ⦄
  where

open Queue equality-with-J
open import Queue.Truncated eq as Q using (Queue)

open import Bijection equality-with-J using (_↔_)
open import Erased.Cubical eq hiding (map)
open import H-level.Closure equality-with-J
open import List equality-with-J as L hiding (map)
open import Maybe equality-with-J
open import Monad equality-with-J hiding (map)
import Nat equality-with-J as Nat

private

  variable
    a ℓ ℓ₁ ℓ₂ : Level
    A         : Type a
    xs        : List A

  module N = Q.Non-indexed

instance

  -- Instances.

  Queue-is-queue : Is-queue (Queue Q) Very-stableᴱ-≡ ℓ
  Queue-is-queue .Is-queue.to-List           = Q.to-List
  Queue-is-queue .Is-queue.from-List         = Q.from-List
  Queue-is-queue .Is-queue.to-List-from-List = _↔_.right-inverse-of
                                                 (Q.Queue↔List _) _
  Queue-is-queue .Is-queue.enqueue           = N.enqueue
  Queue-is-queue .Is-queue.to-List-enqueue   = N.to-List-enqueue
  Queue-is-queue .Is-queue.dequeue           = N.dequeue
  Queue-is-queue .Is-queue.to-List-dequeue   = N.to-List-dequeue
  Queue-is-queue .Is-queue.dequeue⁻¹         = N.dequeue⁻¹
  Queue-is-queue .Is-queue.to-List-dequeue⁻¹ = N.to-List-dequeue⁻¹

  Queue-is-queue-with-map : Is-queue-with-map (Queue Q) ℓ₁ ℓ₂
  Queue-is-queue-with-map .Is-queue-with-map.map         = N.map
  Queue-is-queue-with-map .Is-queue-with-map.to-List-map = N.to-List-map

  Queue-is-queue-with-unique-representations :
    Is-queue-with-unique-representations (Queue Q) ℓ
  Queue-is-queue-with-unique-representations
    .Is-queue-with-unique-representations.from-List-to-List =
    _↔_.left-inverse-of (Q.Queue↔List _) _

------------------------------------------------------------------------
-- Some examples

private

  ns       = Very-stable→Very-stableᴱ 1 $
             Decidable-equality→Very-stable-≡ Nat._≟_
  dequeue′ = dequeue ns
  to-List′ = to-List ns
  empty′   = empty ⦂ Queue Q ℕ

  example₁ : map suc (enqueue 3 empty) ≡ enqueue 4 empty′
  example₁ = _↔_.to Q.≡-for-indices↔≡ [ refl _ ]

  example₂ : dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty))) ≡
             just (10 , enqueue 6 empty)
  example₂ =
    dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty)))  ≡⟨ cong dequeue′ (_↔_.to Q.≡-for-indices↔≡ [ refl _ ]) ⟩
    dequeue′ (cons 10 (enqueue 6 empty))                 ≡⟨ _↔_.right-inverse-of (Queue↔Maybe[×Queue] _) _ ⟩∎
    just (10 , enqueue 6 empty)                          ∎

  example₃ :
    (do x , q ← dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty)))
        return (enqueue (3 * x) q)) ≡
    just (enqueue 30 (enqueue 6 empty))
  example₃ =
    (do x , q ← dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty)))
        return (enqueue (3 * x) q ⦂ Queue Q ℕ))                      ≡⟨ cong (_>>= λ _ → return (enqueue _ _)) example₂ ⟩

    (do x , q ← just (10 , enqueue 6 empty)
        return (enqueue (3 * x) (q ⦂ Queue Q ℕ)))                    ≡⟨⟩

    just (enqueue 30 (enqueue 6 empty))                              ∎

  example₄ :
    (do x , q ← dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty)))
        let q = enqueue (3 * x) q
        return (to-List′ q)) ≡
    just (6 ∷ 30 ∷ [])
  example₄ =
    (do x , q ← dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty)))
        return (to-List′ (enqueue (3 * x) q)))                       ≡⟨ cong (_>>= λ _ → return (to-List′ (enqueue _ _))) example₂ ⟩

    (do x , q ← just (10 , enqueue 6 empty)
        return (to-List′ (enqueue (3 * x) (q ⦂ Queue Q ℕ))))         ≡⟨⟩

    just (to-List′ (enqueue 30 (enqueue 6 empty)))                   ≡⟨ cong just $ to-List-foldl-enqueue-empty _ ⟩∎

    just (6 ∷ 30 ∷ [])                                               ∎

  example₅ :
    ∀ {xs} →
    dequeue′ (from-List (1 ∷ 2 ∷ 3 ∷ xs)) ≡
    just (1 , from-List (2 ∷ 3 ∷ xs))
  example₅ {xs = xs} =
    dequeue′ (from-List (1 ∷ 2 ∷ 3 ∷ xs))       ≡⟨ cong dequeue′ (_↔_.to Q.≡-for-indices↔≡ [ refl _ ]) ⟩
    dequeue′ (cons 1 (from-List (2 ∷ 3 ∷ xs)))  ≡⟨ _↔_.right-inverse-of (Queue↔Maybe[×Queue] _) _ ⟩∎
    just (1 , from-List (2 ∷ 3 ∷ xs))           ∎

  example₆ :
    foldr enqueue empty′ (3 ∷ 2 ∷ 1 ∷ []) ≡
    from-List (1 ∷ 2 ∷ 3 ∷ [])
  example₆ = _↔_.to Q.≡-for-indices↔≡ [ refl _ ]

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)

open import Data.Sum using (_⊎_)
open _⊎_

module AKS.Nat.Roots where

open import AKS.Nat using (ℕ; _≤_; _<_; n≤m⇒n<m⊎n≡m; <-irrefl; *-1-commutativeMonoid)
open ℕ
open import AKS.Nat using ([_,_]; binary-search; acc)
open import AKS.Exponentiation *-1-commutativeMonoid using (_^_)

record Root (n : ℕ) (b : ℕ) : Set where
  constructor Root✓
  field
    root : ℕ
    root^b≤n : root ^ b ≤ n
    n<root^[1+b] : n < (suc root) ^ b

open import AKS.Unsafe using (TODO)

find-root : ∀ n b → Root n b
find-root n b = loop 0 n binary-search
  where
  loop : ∀ l h → [ l , h ] → Root n b
  loop l h (acc downward upward) = TODO

-- root-unique : root ^ b < n → n < (suc root) ^ b

record Power (n : ℕ) (b : ℕ) : Set where
  constructor Power✓
  field
    root : ℕ
    n≡root^b : n ≡ root ^ b

power? : ∀ n b → Dec (Power n b)
power? n b with find-root n b
... | Root✓ root₁ root₁^b≤n n<root₁^[1+b] with n≤m⇒n<m⊎n≡m root₁^b≤n
...   | inj₁ root₁^b<n = no λ { (Power✓ root₂ n≡root₂^b) → TODO }
...   | inj₂ root₁^b≡n = yes (Power✓ root₁ (sym root₁^b≡n))

record Perfect (n : ℕ) : Set where
  constructor Perfect✓
  field
    b : ℕ
    power : Power n b

perfect? : ∀ n → Dec (Perfect n)
perfect? = TODO

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


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

module Function.Surjective.Base where

open import Path
open import Function.Fiber
open import Level
open import HITs.PropositionalTruncation
open import Data.Sigma

Surjective : (A → B) → Type _
Surjective f = ∀ y → ∥ fiber f y ∥

SplitSurjective : (A → B) → Type _
SplitSurjective f = ∀ y → fiber f y

infixr 0 _↠!_ _↠_

_↠!_ : Type a → Type b → Type (a ℓ⊔ b)
A ↠! B = Σ (A → B) SplitSurjective

_↠_ : Type a → Type b → Type (a ℓ⊔ b)
A ↠ B = Σ (A → B) Surjective

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module T where

postulate x : Set
postulate y : Set
postulate p : Set -> Set

e : Set
e = p y

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

@0 A : Set₁
A = Set

macro

  @0 m : Term → TC ⊤
  m B =
    bindTC (quoteTC A) λ A →
    unify A B

B : Set₁
B = m


text:
module Prelude.Bool where

open import Prelude.Unit
open import Prelude.Empty
open import Prelude.Equality
open import Prelude.Decidable
open import Prelude.Function

open import Agda.Builtin.Bool public

infix 0 if_then_else_
if_then_else_ : ∀ {a} {A : Set a} → Bool → A → A → A
if true  then x else y = x
if false then x else y = y
{-# INLINE if_then_else_ #-}

infixr 3 _&&_
infixr 2 _||_

_||_ : Bool → Bool → Bool
true  || _ = true
false || x = x
{-# INLINE _||_ #-}

_&&_ : Bool → Bool → Bool
true  && x = x
false && _ = false
{-# INLINE _&&_ #-}

not : Bool → Bool
not true  = false
not false = true
{-# INLINE not #-}

data IsTrue : Bool → Set where
  instance true : IsTrue true

data IsFalse : Bool → Set where
  instance false : IsFalse false

instance
  EqBool : Eq Bool
  _==_ {{EqBool}} false false = yes refl
  _==_ {{EqBool}} false true  = no λ ()
  _==_ {{EqBool}} true  false = no λ ()
  _==_ {{EqBool}} true  true  = yes refl

decBool : ∀ b → Dec (IsTrue b)
decBool false = no λ ()
decBool true  = yes true
{-# INLINE decBool #-}

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

isNo : ∀ {a} {A : Set a} → Dec A → Bool
isNo = not ∘ isYes

infix 0 if′_then_else_
if′_then_else_ : ∀ {a} {A : Set a} (b : Bool) → ({{_ : IsTrue b}} → A) → ({{_ : IsFalse b}} → A) → A
if′ true  then x else _ = x
if′ false then _ else y = y

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module Prelude.Char where

open import Prelude.Bool

postulate
  Char : Set

{-# BUILTIN CHAR Char #-}

private
  primitive
    primCharEquality : (c c' : Char) -> Bool

postulate
  eof : Char

{-# COMPILED_EPIC eof () -> Int = foreign Int "eof" () #-}

charEq : Char -> Char -> Bool
charEq = primCharEquality


text:
-- Andreas, 2018-06-15, issue #1086
-- Reported by Andrea
-- Fixed by Jesper in https://github.com/agda/agda/commit/242684bca62fabe43e125aefae7526be4b26a135

open import Common.Bool
open import Common.Equality

and : (a b : Bool) → Bool
and true  b = b
and false b = false

test : ∀ a b → and a b ≡ true → a ≡ true
test true true refl = refl

-- Should succeed.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Encoder and decoder instances for Atom.χ-ℕ-atoms
------------------------------------------------------------------------

module Coding.Instances.Nat where

open import Atom

-- The code-Var and code-Const instances are hidden: they are replaced
-- by the code-ℕ instance.

open import Coding.Instances χ-ℕ-atoms public
  hiding (rep-Var; rep-Const)

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


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

open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Setoids.Setoids
open import Numbers.Naturals.Order
open import Vectors

module Sequences where

record Sequence {a : _} (A : Set a) : Set a where
  coinductive
  field
    head : A
    tail : Sequence A

headInjective : {a : _} {A : Set a} {s1 s2 : Sequence A} → s1 ≡ s2 → Sequence.head s1 ≡ Sequence.head s2
headInjective {s1 = s1} {.s1} refl = refl

constSequence : {a : _} {A : Set a} (k : A) → Sequence A
Sequence.head (constSequence k) = k
Sequence.tail (constSequence k) = constSequence k

index : {a : _} {A : Set a} (s : Sequence A) (n : ℕ) → A
index s zero = Sequence.head s
index s (succ n) = index (Sequence.tail s) n

funcToSequence : {a : _} {A : Set a} (f : ℕ → A) → Sequence A
Sequence.head (funcToSequence f) = f 0
Sequence.tail (funcToSequence f) = funcToSequence (λ i → f (succ i))

funcToSequenceReversible : {a : _} {A : Set a} (f : ℕ → A) → (n : ℕ) → index (funcToSequence f) n ≡ f n
funcToSequenceReversible f zero = refl
funcToSequenceReversible f (succ n) = funcToSequenceReversible (λ i → f (succ i)) n

map : {a b : _} {A : Set a} {B : Set b} (f : A → B) (s : Sequence A) → Sequence B
Sequence.head (map f s) = f (Sequence.head s)
Sequence.tail (map f s) = map f (Sequence.tail s)

apply : {a b c : _} {A : Set a} {B : Set b} {C : Set c} (f : A → B → C) (s1 : Sequence A) (s2 : Sequence B) → Sequence C
Sequence.head (apply f s1 s2) = f (Sequence.head s1) (Sequence.head s2)
Sequence.tail (apply f s1 s2) = apply f (Sequence.tail s1) (Sequence.tail s2)

indexAndConst : {a : _} {A : Set a} (a : A) (n : ℕ) → index (constSequence a) n ≡ a
indexAndConst a zero = refl
indexAndConst a (succ n) = indexAndConst a n

mapTwice : {a b c : _} {A : Set a} {B : Set b} {C : Set c} (f : A → B) (g : B → C) (s : Sequence A) → {n : ℕ} → index (map g (map f s)) n ≡ index (map (λ i → g (f i)) s) n
mapTwice f g s {zero} = refl
mapTwice f g s {succ n} = mapTwice f g (Sequence.tail s) {n}

mapAndIndex : {a b : _} {A : Set a} {B : Set b} (s : Sequence A) (f : A → B) (n : ℕ) → f (index s n) ≡ index (map f s) n
mapAndIndex s f zero = refl
mapAndIndex s f (succ n) = mapAndIndex (Sequence.tail s) f n

indexExtensional : {a b c : _} {A : Set a} {B : Set b} (T : Setoid {_} {c} B) (s : Sequence A) (f g : A → B) → (extension : ∀ {x} → (Setoid._∼_ T (f x) (g x))) → {n : ℕ} → Setoid._∼_ T (index (map f s) n) (index (map g s) n)
indexExtensional T s f g extension {zero} = extension
indexExtensional T s f g extension {succ n} = indexExtensional T (Sequence.tail s) f g extension {n}

indexAndApply : {a b c : _} {A : Set a} {B : Set b} {C : Set c} (s1 : Sequence A) (s2 : Sequence B) (f : A → B → C) → {m : ℕ} → index (apply f s1 s2) m ≡ f (index s1 m) (index s2 m)
indexAndApply s1 s2 f {zero} = refl
indexAndApply s1 s2 f {succ m} = indexAndApply (Sequence.tail s1) (Sequence.tail s2) f {m}

mapAndApply : {a b c d : _} {A : Set a} {B : Set b} {C : Set c} {D : Set d} (s1 : Sequence A) (s2 : Sequence B) (f : A → B → C) (g : C → D) → (m : ℕ) → index (map g (apply f s1 s2)) m ≡ g (f (index s1 m) (index s2 m))
mapAndApply s1 s2 f g zero = refl
mapAndApply s1 s2 f g (succ m) = mapAndApply (Sequence.tail s1) (Sequence.tail s2) f g m

assemble : {a : _} {A : Set a} → (x : A) → (s : Sequence A) → Sequence A
Sequence.head (assemble x s) = x
Sequence.tail (assemble x s) = s

allTrue : {a : _} {A : Set a} {c : _} (pred : A → Set c) (s : Sequence A) → Set c
allTrue pred s = (n : ℕ) → pred (index s n)

tailFrom : {a : _} {A : Set a} (n : ℕ) → (s : Sequence A) → Sequence A
tailFrom zero s = s
tailFrom (succ n) s = tailFrom n (Sequence.tail s)

subsequence : {a : _} {A : Set a} (x : Sequence A) → (indices : Sequence ℕ) → ((n : ℕ) → index indices n <N index indices (succ n)) → Sequence A
Sequence.head (subsequence x selector increasing) = index x (Sequence.head selector)
Sequence.tail (subsequence x selector increasing) = subsequence (tailFrom (succ (Sequence.head selector)) x) (Sequence.tail selector) λ n → increasing (succ n)

take : {a : _} {A : Set a} (n : ℕ) (s : Sequence A) → Vec A n
take zero s = []
take (succ n) s = Sequence.head s ,- take n (Sequence.tail s)

unfold : {a : _} {A : Set a} → (A → A) → A → Sequence A
Sequence.head (unfold f a) = a
Sequence.tail (unfold f a) = unfold f (f a)

indexAndUnfold : {a : _} {A : Set a} (f : A → A) (start : A) (n : ℕ) → index (unfold f start) (succ n) ≡ f (index (unfold f start) n)
indexAndUnfold f s zero = refl
indexAndUnfold f s (succ n) = indexAndUnfold f (f s) n


text:
{-

Properties and Formulae about Cardinality

This file contains:
- Relation between abstract properties and cardinality in special cases;
- Combinatorial formulae, namely, cardinality of A+B, A×B, ΣAB, ΠAB, etc;
- A general form of Pigeonhole Principle;
- Maximal value of numerical function on finite sets;
- Set truncation of FinSet is equivalent to ℕ;
- FinProp is equivalent to Bool.

-}
{-# OPTIONS --safe #-}

module Cubical.Data.FinSet.Cardinality where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Transport

open import Cubical.HITs.PropositionalTruncation as Prop
open import Cubical.HITs.SetTruncation as Set

open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Unit
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Bool hiding (_≟_)
open import Cubical.Data.Sum
open import Cubical.Data.Sigma

open import Cubical.Data.Fin using (Fin-inj)
open import Cubical.Data.Fin.LehmerCode as LehmerCode
open import Cubical.Data.SumFin
open import Cubical.Data.FinSet.Base
open import Cubical.Data.FinSet.Properties
open import Cubical.Data.FinSet.FiniteChoice
open import Cubical.Data.FinSet.Constructors
open import Cubical.Data.FinSet.Induction hiding (_+_)

open import Cubical.Relation.Nullary

open import Cubical.Functions.Fibration
open import Cubical.Functions.Embedding
open import Cubical.Functions.Surjection

private
  variable
    ℓ ℓ' ℓ'' : Level
    n : ℕ
    X : FinSet ℓ
    Y : FinSet ℓ'

-- cardinality of finite sets

∣≃card∣ : (X : FinSet ℓ) → ∥ X .fst ≃ Fin (card X) ∥
∣≃card∣ X = X .snd .snd

-- cardinality is invariant under equivalences

cardEquiv : (X : FinSet ℓ)(Y : FinSet ℓ') → ∥ X .fst ≃ Y .fst ∥ → card X ≡ card Y
cardEquiv X Y e =
  Prop.rec (isSetℕ _ _) (λ p → Fin-inj _ _ (ua p))
    (∣ invEquiv (SumFin≃Fin _) ∣ ⋆̂ ∣invEquiv∣ (∣≃card∣ X) ⋆̂ e ⋆̂ ∣≃card∣ Y ⋆̂ ∣ SumFin≃Fin _ ∣)

cardInj : card X ≡ card Y → ∥ X .fst ≃ Y .fst ∥
cardInj {X = X} {Y = Y} p =
  ∣≃card∣ X ⋆̂ ∣ pathToEquiv (cong Fin p) ∣ ⋆̂ ∣invEquiv∣ (∣≃card∣ Y)

cardReflection : card X ≡ n → ∥ X .fst ≃ Fin n ∥
cardReflection {X = X} = cardInj {X = X} {Y = _ , isFinSetFin}

card≡MereEquiv : (card X ≡ card Y) ≡ ∥ X .fst ≃ Y .fst ∥
card≡MereEquiv {X = X} {Y = Y} =
  hPropExt (isSetℕ _ _) isPropPropTrunc (cardInj {X = X} {Y = Y}) (cardEquiv X Y)

-- special properties about specific cardinality

module _
  {X : FinSet ℓ} where

  card≡0→isEmpty : card X ≡ 0 → ¬ X .fst
  card≡0→isEmpty p x =
    Prop.rec isProp⊥ (λ e → subst Fin p (e .fst x)) (∣≃card∣ X)

  card>0→isInhab : card X > 0 → ∥ X .fst ∥
  card>0→isInhab p =
    Prop.map (λ e → invEq e (Fin>0→isInhab _ p)) (∣≃card∣ X)

  card>1→hasNonEqualTerm : card X > 1 → ∥ Σ[ a ∈ X .fst ] Σ[ b ∈ X .fst ] ¬ a ≡ b ∥
  card>1→hasNonEqualTerm p =
    Prop.map
      (λ e →
        e .fst (Fin>1→hasNonEqualTerm _ p .fst) ,
        e .fst (Fin>1→hasNonEqualTerm _ p .snd .fst) ,
        Fin>1→hasNonEqualTerm _ p .snd .snd ∘ invEq (congEquiv e))
      (∣invEquiv∣ (∣≃card∣ X))

  card≡1→isContr : card X ≡ 1 → isContr (X .fst)
  card≡1→isContr p =
    Prop.rec isPropIsContr
        (λ e → isOfHLevelRespectEquiv 0 (invEquiv (e ⋆ substEquiv Fin p)) isContrSumFin1) (∣≃card∣ X)

  card≤1→isProp : card X ≤ 1 → isProp (X .fst)
  card≤1→isProp p =
    Prop.rec isPropIsProp (λ e → isOfHLevelRespectEquiv 1 (invEquiv e) (Fin≤1→isProp (card X) p)) (∣≃card∣ X)

  card≡n : card X ≡ n → ∥ X ≡ 𝔽in n ∥
  card≡n {n = n} p =
    Prop.map
        (λ e →
          (λ i →
            ua e i ,
            isProp→PathP {B = λ j → isFinSet (ua e j)}
              (λ _ → isPropIsFinSet) (X .snd) (𝔽in n .snd) i ))
        (∣≃card∣ X ⋆̂ ∣ pathToEquiv (cong Fin p) ⋆ invEquiv (𝔽in≃Fin n) ∣)

  card≡0 : card X ≡ 0 → X ≡ 𝟘
  card≡0 p =
    propTruncIdempotent≃
      (isOfHLevelRespectEquiv
        1 (FinSet≡ X 𝟘)
          (isOfHLevel≡ 1
            (card≤1→isProp (subst (λ a → a ≤ 1) (sym p) (≤-solver 0 1))) (isProp⊥*))) .fst
      (card≡n p)

  card≡1 : card X ≡ 1 → X ≡ 𝟙
  card≡1 p =
    propTruncIdempotent≃
      (isOfHLevelRespectEquiv
        1 (FinSet≡ X 𝟙)
          (isOfHLevel≡ 1
            (card≤1→isProp (subst (λ a → a ≤ 1) (sym p) (≤-solver 1 1))) (isPropUnit*))) .fst
      (Prop.map (λ q → q ∙ 𝔽in1≡𝟙) (card≡n p))

module _
  (X : FinSet ℓ) where

  isEmpty→card≡0 : ¬ X .fst → card X ≡ 0
  isEmpty→card≡0 p =
    Prop.rec (isSetℕ _ _) (λ e → sym (isEmpty→Fin≡0 _ (p ∘ invEq e))) (∣≃card∣ X)

  isInhab→card>0 : ∥ X .fst ∥ → card X > 0
  isInhab→card>0 = Prop.rec2 m≤n-isProp (λ p x → isInhab→Fin>0 _ (p .fst x)) (∣≃card∣ X)

  hasNonEqualTerm→card>1 : {a b : X. fst} → ¬ a ≡ b → card X > 1
  hasNonEqualTerm→card>1 {a = a} {b = b} q =
    Prop.rec m≤n-isProp (λ p → hasNonEqualTerm→Fin>1 _ (p .fst a) (p .fst b) (q ∘ invEq (congEquiv p))) (∣≃card∣ X)

  isContr→card≡1 : isContr (X .fst) → card X ≡ 1
  isContr→card≡1 p = cardEquiv X (_ , isFinSetUnit) ∣ isContr→≃Unit p ∣

  isProp→card≤1 : isProp (X .fst) → card X ≤ 1
  isProp→card≤1 p = isProp→Fin≤1 (card X) (Prop.rec isPropIsProp (λ e → isOfHLevelRespectEquiv 1 e p) (∣≃card∣ X))

{- formulae about cardinality -}

-- results to be used in direct induction on FinSet

card𝟘 : card (𝟘 {ℓ}) ≡ 0
card𝟘 {ℓ = ℓ} = isEmpty→card≡0 (𝟘 {ℓ}) (Empty.rec*)

card𝟙 : card (𝟙 {ℓ}) ≡ 1
card𝟙 {ℓ = ℓ} = isContr→card≡1 (𝟙 {ℓ}) isContrUnit*

card𝔽in : (n : ℕ) → card (𝔽in {ℓ} n) ≡ n
card𝔽in {ℓ = ℓ} n =  cardEquiv (𝔽in {ℓ} n) (_ , isFinSetFin) ∣ 𝔽in≃Fin n ∣

-- addition/product formula

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ') where

  card+ : card (_ , isFinSet⊎ X Y) ≡ card X + card Y
  card+ = refl

  card× : card (_ , isFinSet× X Y) ≡ card X · card Y
  card× = refl

-- total summation/product of numerical functions from finite sets

module _
  (X : FinSet ℓ)
  (f : X .fst → ℕ) where

  sum : ℕ
  sum = card (_ , isFinSetΣ X (λ x → Fin (f x) , isFinSetFin))

  prod : ℕ
  prod = card (_ , isFinSetΠ X (λ x → Fin (f x) , isFinSetFin))

module _
  (f : 𝟘 {ℓ} .fst → ℕ) where

  sum𝟘 : sum 𝟘 f ≡ 0
  sum𝟘 =
    isEmpty→card≡0 (_ , isFinSetΣ 𝟘 (λ x → Fin (f x) , isFinSetFin))
                   ((invEquiv (Σ-cong-equiv-fst (invEquiv 𝟘≃Empty)) ⋆ ΣEmpty _) .fst)

  prod𝟘 : prod 𝟘 f ≡ 1
  prod𝟘 =
    isContr→card≡1 (_ , isFinSetΠ 𝟘 (λ x → Fin (f x) , isFinSetFin))
                   (isContrΠ⊥*)

module _
  (f : 𝟙 {ℓ} .fst → ℕ) where

  sum𝟙 : sum 𝟙 f ≡ f tt*
  sum𝟙 =
    cardEquiv (_ , isFinSetΣ 𝟙 (λ x → Fin (f x) , isFinSetFin))
              (Fin (f tt*) , isFinSetFin) ∣ Σ-contractFst isContrUnit* ∣

  prod𝟙 : prod 𝟙 f ≡ f tt*
  prod𝟙 =
    cardEquiv (_ , isFinSetΠ 𝟙 (λ x → Fin (f x) , isFinSetFin))
              (Fin (f tt*) , isFinSetFin) ∣ ΠUnit* _ ∣

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ')
  (f : X .fst ⊎ Y .fst → ℕ) where

  sum⊎ : sum (_ , isFinSet⊎ X Y) f ≡ sum X (f ∘ inl) + sum Y (f ∘ inr)
  sum⊎ =
    cardEquiv (_ , isFinSetΣ (_ , isFinSet⊎ X Y) (λ x → Fin (f x) , isFinSetFin))
              (_ , isFinSet⊎ (_ , isFinSetΣ X (λ x → Fin (f (inl x)) , isFinSetFin))
                             (_ , isFinSetΣ Y (λ y → Fin (f (inr y)) , isFinSetFin))) ∣ Σ⊎≃ ∣
    ∙ card+ (_ , isFinSetΣ X (λ x → Fin (f (inl x)) , isFinSetFin))
            (_ , isFinSetΣ Y (λ y → Fin (f (inr y)) , isFinSetFin))

  prod⊎ : prod (_ , isFinSet⊎ X Y) f ≡ prod X (f ∘ inl) · prod Y (f ∘ inr)
  prod⊎ =
    cardEquiv (_ , isFinSetΠ (_ , isFinSet⊎ X Y) (λ x → Fin (f x) , isFinSetFin))
              (_ , isFinSet× (_ , isFinSetΠ X (λ x → Fin (f (inl x)) , isFinSetFin))
                             (_ , isFinSetΠ Y (λ y → Fin (f (inr y)) , isFinSetFin))) ∣ Π⊎≃ ∣
    ∙ card× (_ , isFinSetΠ X (λ x → Fin (f (inl x)) , isFinSetFin))
            (_ , isFinSetΠ Y (λ y → Fin (f (inr y)) , isFinSetFin))

-- technical lemma
module _
  (n : ℕ)(f : 𝔽in {ℓ} (1 + n) .fst → ℕ) where

  sum𝔽in1+n : sum (𝔽in (1 + n)) f ≡ f (inl tt*) + sum (𝔽in n) (f ∘ inr)
  sum𝔽in1+n = sum⊎ 𝟙 (𝔽in n) f ∙ (λ i → sum𝟙 (f ∘ inl) i + sum (𝔽in n) (f ∘ inr))

  prod𝔽in1+n : prod (𝔽in (1 + n)) f ≡ f (inl tt*) · prod (𝔽in n) (f ∘ inr)
  prod𝔽in1+n = prod⊎ 𝟙 (𝔽in n) f ∙ (λ i → prod𝟙 (f ∘ inl) i · prod (𝔽in n) (f ∘ inr))

sumConst𝔽in : (n : ℕ)(f : 𝔽in {ℓ} n .fst → ℕ)(c : ℕ)(h : (x : 𝔽in n .fst) → f x ≡ c) → sum (𝔽in n) f ≡ c · n
sumConst𝔽in 0 f c _ = sum𝟘 f ∙ 0≡m·0 c
sumConst𝔽in (suc n) f c h =
    sum𝔽in1+n n f
  ∙ (λ i → h (inl tt*) i + sumConst𝔽in n (f ∘ inr) c (h ∘ inr) i)
  ∙ sym (·-suc c n)

prodConst𝔽in : (n : ℕ)(f : 𝔽in {ℓ} n .fst → ℕ)(c : ℕ)(h : (x : 𝔽in n .fst) → f x ≡ c) → prod (𝔽in n) f ≡ c ^ n
prodConst𝔽in 0 f c _ = prod𝟘 f
prodConst𝔽in (suc n) f c h =
    prod𝔽in1+n n f
  ∙ (λ i → h (inl tt*) i · prodConst𝔽in n (f ∘ inr) c (h ∘ inr) i)

module _
  (X : FinSet ℓ)
  (f : X .fst → ℕ)
  (c : ℕ)(h : (x : X .fst) → f x ≡ c) where

  sumConst : sum X f ≡ c · card X
  sumConst =
    elimProp
      (λ X → (f : X .fst → ℕ)(c : ℕ)(h : (x : X .fst) → f x ≡ c) → sum X f ≡ c · (card X))
      (λ X → isPropΠ3 (λ _ _ _ → isSetℕ _ _))
      (λ n f c h → sumConst𝔽in n f c h ∙ (λ i → c · card𝔽in {ℓ = ℓ} n (~ i))) X f c h

  prodConst : prod X f ≡ c ^ card X
  prodConst =
    elimProp
      (λ X → (f : X .fst → ℕ)(c : ℕ)(h : (x : X .fst) → f x ≡ c) → prod X f ≡ c ^ (card X))
      (λ X → isPropΠ3 (λ _ _ _ → isSetℕ _ _))
      (λ n f c h → prodConst𝔽in n f c h ∙ (λ i → c ^ card𝔽in {ℓ = ℓ} n (~ i))) X f c h

private
  ≡≤ : {m n l k r s : ℕ} → m ≤ n → l ≤ k → r ≡ m + l → s ≡ n + k → r ≤ s
  ≡≤ {m = m} {l = l} {k = k} p q u v = subst2 (_≤_) (sym u) (sym v) (≤-+-≤ p q)

  ≡< : {m n l k r s : ℕ} → m < n → l ≤ k → r ≡ m + l → s ≡ n + k → r < s
  ≡< {m = m} {l = l} {k = k} p q u v = subst2 (_<_) (sym u) (sym v) (<-+-≤ p q)

sum≤𝔽in : (n : ℕ)(f g : 𝔽in {ℓ} n .fst → ℕ)(h : (x : 𝔽in n .fst) → f x ≤ g x) → sum (𝔽in n) f ≤ sum (𝔽in n) g
sum≤𝔽in 0 f g _ = subst2 (_≤_) (sym (sum𝟘 f)) (sym (sum𝟘 g)) ≤-refl
sum≤𝔽in (suc n) f g h =
  ≡≤ (h (inl tt*)) (sum≤𝔽in n (f ∘ inr) (g ∘ inr) (h ∘ inr)) (sum𝔽in1+n n f) (sum𝔽in1+n n g)

sum<𝔽in : (n : ℕ)(f g : 𝔽in {ℓ} n .fst → ℕ)(t : ∥ 𝔽in {ℓ} n .fst ∥)(h : (x : 𝔽in n .fst) → f x < g x)
  → sum (𝔽in n) f < sum (𝔽in n) g
sum<𝔽in {ℓ = ℓ} 0 _ _ t _ = Empty.rec (<→≢ (isInhab→card>0 (𝔽in 0) t) (card𝟘 {ℓ = ℓ}))
sum<𝔽in (suc n) f g t h =
  ≡< (h (inl tt*)) (sum≤𝔽in n (f ∘ inr) (g ∘ inr) (<-weaken ∘ h ∘ inr)) (sum𝔽in1+n n f) (sum𝔽in1+n n g)

module _
  (X : FinSet ℓ)
  (f g : X .fst → ℕ) where

    module _
      (h : (x : X .fst) → f x ≡ g x) where

      sum≡ : sum X f ≡ sum X g
      sum≡ i = sum X (λ x → h x i)

      prod≡ : prod X f ≡ prod X g
      prod≡ i = prod X (λ x → h x i)

    module _
      (h : (x : X .fst) → f x ≤ g x) where

      sum≤ : sum X f ≤ sum X g
      sum≤ =
        elimProp
          (λ X → (f g : X .fst → ℕ)(h : (x : X .fst) → f x ≤ g x) → sum X f ≤ sum X g)
          (λ X → isPropΠ3 (λ _ _ _ → m≤n-isProp)) sum≤𝔽in X f g h

    module _
      (t : ∥ X .fst ∥)
      (h : (x : X .fst) → f x < g x) where

      sum< : sum X f < sum X g
      sum< =
        elimProp
          (λ X → (f g : X .fst → ℕ)(t : ∥ X .fst ∥)(h : (x : X .fst) → f x < g x) → sum X f < sum X g)
          (λ X → isPropΠ4 (λ _ _ _ _ → m≤n-isProp)) sum<𝔽in X f g t h

module _
  (X : FinSet ℓ)
  (f : X .fst → ℕ) where

  module _
    (c : ℕ)(h : (x : X .fst) → f x ≤ c) where

    sumBounded : sum X f ≤ c · card X
    sumBounded = subst (λ a → sum X f ≤ a) (sumConst X (λ _ → c) c (λ _ → refl)) (sum≤ X f (λ _ → c) h)

  module _
    (c : ℕ)(h : (x : X .fst) → f x ≥ c) where

    sumBoundedBelow : sum X f ≥ c · card X
    sumBoundedBelow = subst (λ a → sum X f ≥ a) (sumConst X (λ _ → c) c (λ _ → refl)) (sum≤ X (λ _ → c) f h)

-- some combinatorial identities

module _
  (X : FinSet ℓ )
  (Y : X .fst → FinSet ℓ') where

  cardΣ : card (_ , isFinSetΣ X Y) ≡ sum X (λ x → card (Y x))
  cardΣ =
    cardEquiv (_ , isFinSetΣ X Y) (_ , isFinSetΣ X (λ x → Fin (card (Y x)) , isFinSetFin))
              (Prop.map Σ-cong-equiv-snd
                (choice X (λ x → Y x .fst ≃ Fin (card (Y x))) (λ x → ∣≃card∣ (Y x))))

  cardΠ : card (_ , isFinSetΠ X Y) ≡ prod X (λ x → card (Y x))
  cardΠ =
    cardEquiv (_ , isFinSetΠ X Y) (_ , isFinSetΠ X (λ x → Fin (card (Y x)) , isFinSetFin))
              (Prop.map equivΠCod
                (choice X (λ x → Y x .fst ≃ Fin (card (Y x))) (λ x → ∣≃card∣ (Y x))))

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ') where

  card→ : card (_ , isFinSet→ X Y) ≡ card Y ^ card X
  card→ = cardΠ X (λ _ → Y) ∙ prodConst X (λ _ → card Y) (card Y) (λ _ → refl)

module _
  (X : FinSet ℓ ) where

  cardAut : card (_ , isFinSetAut X) ≡ LehmerCode.factorial (card X)
  cardAut = refl

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ')
  (f : X .fst → Y .fst) where

  sumCardFiber : card X ≡ sum Y (λ y → card (_ , isFinSetFiber X Y f y))
  sumCardFiber =
      cardEquiv X (_ , isFinSetΣ Y (λ y → _ , isFinSetFiber X Y f y)) ∣ totalEquiv f ∣
    ∙ cardΣ Y (λ y → _ , isFinSetFiber X Y f y)

-- the pigeonhole priniple

-- a logical lemma
private
  ¬ΠQ→¬¬ΣP : (X : Type ℓ)
      (P : X → Type ℓ' )
      (Q : X → Type ℓ'')
      (r : (x : X) → ¬ (P x) → Q x)
    → ¬ ((x : X) → Q x) → ¬ ¬ (Σ X P)
  ¬ΠQ→¬¬ΣP _ _ _ r g f = g (λ x → r x (λ p → f (x , p)))

module _
  (f : X .fst → Y .fst)
  (n : ℕ) where

  fiberCount : ((y : Y .fst) → card (_ , isFinSetFiber X Y f y) ≤ n) → card X ≤ n · card Y
  fiberCount h =
    subst (λ a → a ≤ _) (sym (sumCardFiber X Y f))
          (sumBounded Y (λ y → card (_ , isFinSetFiber X Y f y)) n h)

  module _
    (p : card X > n · card Y) where

    ¬¬pigeonHole : ¬ ¬ (Σ[ y ∈ Y .fst ] card (_ , isFinSetFiber X Y f y) > n)
    ¬¬pigeonHole =
      ¬ΠQ→¬¬ΣP (Y .fst) (λ y → _ > n) (λ y → _ ≤ n)
               (λ y → <-asym') (λ h → <-asym p (fiberCount h))

    pigeonHole : ∥ Σ[ y ∈ Y .fst ] card (_ , isFinSetFiber X Y f y) > n ∥
    pigeonHole = PeirceLaw (isFinSetΣ Y (λ _ → _ , isDecProp→isFinSet m≤n-isProp (≤Dec _ _))) ¬¬pigeonHole

-- a special case, proved in Cubical.Data.Fin.Properties

-- a technical lemma
private
  Σ∥P∥→∥ΣP∥ : (X : Type ℓ)(P : X → Type ℓ')
    → Σ X (λ x → ∥ P x ∥) → ∥ Σ X P ∥
  Σ∥P∥→∥ΣP∥ _ _ (x , p) = Prop.map (λ q → x , q) p

module _
  (f : X .fst → Y .fst)
  (p : card X > card Y) where

  fiberNonEqualTerm : Σ[ y ∈ Y .fst ] card (_ , isFinSetFiber X Y f y) > 1
    → ∥ Σ[ y ∈ Y .fst ] Σ[ a ∈ fiber f y ] Σ[ b ∈ fiber f y ] ¬ a ≡ b ∥
  fiberNonEqualTerm (y , p) = Σ∥P∥→∥ΣP∥ _ _ (y , card>1→hasNonEqualTerm {X = _ , isFinSetFiber X Y f y} p)

  nonInj : Σ[ y ∈ Y .fst ] Σ[ a ∈ fiber f y ] Σ[ b ∈ fiber f y ] ¬ a ≡ b
    → Σ[ x ∈ X .fst ] Σ[ x' ∈ X .fst ] (¬ x ≡ x') × (f x ≡ f x')
  nonInj (y , (x , p) , (x' , q) , t) .fst = x
  nonInj (y , (x , p) , (x' , q) , t) .snd .fst = x'
  nonInj (y , (x , p) , (x' , q) , t) .snd .snd .fst u =
    t (λ i → u i , isSet→SquareP (λ i j → isFinSet→isSet (Y .snd)) p q (cong f u) refl i)
  nonInj (y , (x , p) , (x' , q) , t) .snd .snd .snd = p ∙ sym q

  pigeonHole' : ∥ Σ[ x ∈ X .fst ] Σ[ x' ∈ X .fst ] (¬ x ≡ x') × (f x ≡ f x') ∥
  pigeonHole' =
    Prop.map nonInj
      (Prop.rec isPropPropTrunc fiberNonEqualTerm
        (pigeonHole {X = X} {Y = Y} f 1 (subst (λ a → _ > a) (sym (·-identityˡ _)) p)))

-- cardinality and injection/surjection

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ') where

  module _
    (f : X .fst → Y .fst) where

    card↪Inequality' : isEmbedding f → card X ≤ card Y
    card↪Inequality' p =
      subst2 (_≤_)
        (sym (sumCardFiber X Y f))
        (·-identityˡ _)
        (sumBounded Y (λ y → card (_ , isFinSetFiber X Y f y)) 1
          (λ y → isProp→card≤1 (_ , isFinSetFiber X Y f y)
            (isEmbedding→hasPropFibers p y)))

    card↠Inequality' : isSurjection f → card X ≥ card Y
    card↠Inequality' p =
      subst2 (_≥_)
        (sym (sumCardFiber X Y f))
        (·-identityˡ _)
        (sumBoundedBelow Y (λ y → card (_ , isFinSetFiber X Y f y)) 1
          (λ y → isInhab→card>0 (_ , isFinSetFiber X Y f y) (p y)))

  card↪Inequality : ∥ X .fst ↪ Y .fst ∥ → card X ≤ card Y
  card↪Inequality = Prop.rec m≤n-isProp (λ (f , p) → card↪Inequality' f p)

  card↠Inequality : ∥ X .fst ↠ Y .fst ∥ → card X ≥ card Y
  card↠Inequality = Prop.rec m≤n-isProp (λ (f , p) → card↠Inequality' f p)

-- maximal value of numerical functions

module _
  (X : Type ℓ)
  (f : X → ℕ) where

  module _
    (x : X) where

    isMax : Type ℓ
    isMax = (x' : X) → f x' ≤ f x

    isPropIsMax : isProp isMax
    isPropIsMax = isPropΠ (λ _ → m≤n-isProp)

  uniqMax : (x x' : X) → isMax x → isMax x' → f x ≡ f x'
  uniqMax x x' p q = ≤-antisym (q x) (p x')

  ΣMax : Type ℓ
  ΣMax = Σ[ x ∈ X ] isMax x

  ∃Max : Type ℓ
  ∃Max = ∥ ΣMax ∥

  ∃Max→maxValue : ∃Max → ℕ
  ∃Max→maxValue =
    SetElim.rec→Set
      isSetℕ (λ (x , p) → f x)
             (λ (x , p) (x' , q) → uniqMax x x' p q)

-- lemma about maximal value on sum type
module _
  (X : Type ℓ )
  (Y : Type ℓ')
  (f : X ⊎ Y → ℕ) where

  ΣMax⊎-case : ((x , p) : ΣMax X (f ∘ inl))((y , q) : ΣMax Y (f ∘ inr))
    → Trichotomy (f (inl x)) (f (inr y)) → ΣMax (X ⊎ Y) f
  ΣMax⊎-case (x , p) (y , q) (lt r) .fst = inr y
  ΣMax⊎-case (x , p) (y , q) (lt r) .snd (inl x') = ≤-trans (p x') (<-weaken r)
  ΣMax⊎-case (x , p) (y , q) (lt r) .snd (inr y') = q y'
  ΣMax⊎-case (x , p) (y , q) (eq r) .fst = inr y
  ΣMax⊎-case (x , p) (y , q) (eq r) .snd (inl x') = ≤-trans (p x') (_ , r)
  ΣMax⊎-case (x , p) (y , q) (eq r) .snd (inr y') = q y'
  ΣMax⊎-case (x , p) (y , q) (gt r) .fst = inl x
  ΣMax⊎-case (x , p) (y , q) (gt r) .snd (inl x') = p x'
  ΣMax⊎-case (x , p) (y , q) (gt r) .snd (inr y') = ≤-trans (q y') (<-weaken r)

  ∃Max⊎ : ∃Max X (f ∘ inl) → ∃Max Y (f ∘ inr) → ∃Max (X ⊎ Y) f
  ∃Max⊎ = Prop.map2 (λ p q → ΣMax⊎-case p q (_≟_ _ _))

ΣMax𝟙 : (f : 𝟙 {ℓ} .fst → ℕ) → ΣMax _ f
ΣMax𝟙 f .fst = tt*
ΣMax𝟙 f .snd x = _ , cong f (sym (isContrUnit* .snd x))

∃Max𝟙 : (f : 𝟙 {ℓ} .fst → ℕ) → ∃Max _ f
∃Max𝟙 f = ∣ ΣMax𝟙 f ∣

∃Max𝔽in : (n : ℕ)(f : 𝔽in {ℓ} n .fst → ℕ)(x : ∥ 𝔽in {ℓ} n .fst ∥) → ∃Max _ f
∃Max𝔽in {ℓ = ℓ} 0 _ x = Empty.rec (<→≢ (isInhab→card>0 (𝔽in 0) x) (card𝟘 {ℓ = ℓ}))
∃Max𝔽in 1 f _ =
  subst (λ X → (f : X .fst → ℕ) → ∃Max _ f) (sym 𝔽in1≡𝟙) ∃Max𝟙 f
∃Max𝔽in (suc (suc n)) f _ =
  ∃Max⊎ (𝟙 .fst) (𝔽in (suc n) .fst) f (∃Max𝟙 (f ∘ inl)) (∃Max𝔽in (suc n) (f ∘ inr) ∣ * {n = n} ∣)

module _
  (X : FinSet ℓ)
  (f : X .fst → ℕ)
  (x : ∥ X .fst ∥) where

  ∃MaxFinSet : ∃Max _ f
  ∃MaxFinSet =
    elimProp
      (λ X → (f : X .fst → ℕ)(x : ∥ X .fst ∥) → ∃Max _ f)
      (λ X → isPropΠ2 (λ _ _ → isPropPropTrunc)) ∃Max𝔽in X f x

  maxValue : ℕ
  maxValue = ∃Max→maxValue _ _ ∃MaxFinSet

{- some formal consequences of card -}

-- card induces equivalence from set truncation of FinSet to natural numbers

open Iso

Iso-∥FinSet∥₂-ℕ : Iso ∥ FinSet ℓ ∥₂ ℕ
Iso-∥FinSet∥₂-ℕ .fun = Set.rec isSetℕ card
Iso-∥FinSet∥₂-ℕ .inv n = ∣ 𝔽in n ∣₂
Iso-∥FinSet∥₂-ℕ .rightInv n = card𝔽in n
Iso-∥FinSet∥₂-ℕ {ℓ = ℓ} .leftInv =
  Set.elim {B = λ X → ∣ 𝔽in (Set.rec isSetℕ card X) ∣₂ ≡ X}
    (λ X → isSetPathImplicit)
    (elimProp (λ X → ∣ 𝔽in (card X) ∣₂ ≡ ∣ X ∣₂) (λ X → squash₂ _ _)
      (λ n i → ∣ 𝔽in (card𝔽in {ℓ = ℓ} n i) ∣₂))

-- this is the definition of natural numbers you learned from school
∥FinSet∥₂≃ℕ : ∥ FinSet ℓ ∥₂ ≃ ℕ
∥FinSet∥₂≃ℕ = isoToEquiv Iso-∥FinSet∥₂-ℕ

-- FinProp is equivalent to Bool

Bool→FinProp : Bool → FinProp ℓ
Bool→FinProp true = 𝟙 , isPropUnit*
Bool→FinProp false = 𝟘 , isProp⊥*

injBool→FinProp : (x y : Bool) → Bool→FinProp {ℓ = ℓ} x ≡ Bool→FinProp y → x ≡ y
injBool→FinProp true true _ = refl
injBool→FinProp false false _ = refl
injBool→FinProp true false p = Empty.rec (snotz (cong (card ∘ fst) p))
injBool→FinProp false true p = Empty.rec (znots (cong (card ∘ fst) p))

isEmbeddingBool→FinProp : isEmbedding (Bool→FinProp {ℓ = ℓ})
isEmbeddingBool→FinProp = injEmbedding isSetBool isSetFinProp (λ {x} {y} → injBool→FinProp x y)

card-case : (P : FinProp ℓ) → {n : ℕ} → card (P .fst) ≡ n → Σ[ x ∈ Bool ] Bool→FinProp x ≡ P
card-case P {n = 0} p = false , FinProp≡ (𝟘 , isProp⊥*) P .fst (cong fst (sym (card≡0 {X = P .fst} p)))
card-case P {n = 1} p = true , FinProp≡ (𝟙 , isPropUnit*) P .fst (cong fst (sym (card≡1 {X = P .fst} p)))
card-case P {n = suc (suc n)} p =
  Empty.rec (¬-<-zero (pred-≤-pred (subst (λ a → a ≤ 1) p (isProp→card≤1 (P .fst) (P .snd)))))

isSurjectionBool→FinProp : isSurjection (Bool→FinProp {ℓ = ℓ})
isSurjectionBool→FinProp P = ∣ card-case P refl ∣

FinProp≃Bool : FinProp ℓ ≃ Bool
FinProp≃Bool =
  invEquiv (Bool→FinProp ,
    isEmbedding×isSurjection→isEquiv (isEmbeddingBool→FinProp  , isSurjectionBool→FinProp))

isFinSetFinProp : isFinSet (FinProp ℓ)
isFinSetFinProp = EquivPresIsFinSet (invEquiv FinProp≃Bool) isFinSetBool

-- a more computationally efficient version of equivalence type

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ') where

  isFinSet≃Eff' : Dec (card X ≡ card Y) → isFinSet (X .fst ≃ Y .fst)
  isFinSet≃Eff' (yes p) = factorial (card Y) ,
    Prop.elim2 (λ _ _ → isPropPropTrunc {A = _ ≃ Fin _})
      (λ p1 p2
        → ∣ equivComp (p1 ⋆ pathToEquiv (cong Fin p) ⋆ SumFin≃Fin _) (p2 ⋆ SumFin≃Fin _)
          ⋆ lehmerEquiv ⋆ lehmerFinEquiv
          ⋆ invEquiv (SumFin≃Fin _) ∣)
      (∣≃card∣ X) (∣≃card∣ Y)
  isFinSet≃Eff' (no ¬p) = 0 , ∣ uninhabEquiv (¬p ∘ cardEquiv X Y ∘ ∣_∣) (idfun _) ∣

  isFinSet≃Eff : isFinSet (X .fst ≃ Y .fst)
  isFinSet≃Eff = isFinSet≃Eff' (discreteℕ _ _)

module _
  (X Y : FinSet ℓ) where

  isFinSetType≡Eff : isFinSet (X .fst ≡ Y .fst)
  isFinSetType≡Eff = EquivPresIsFinSet (invEquiv univalence) (isFinSet≃Eff X Y)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decidable setoid membership over vectors.
------------------------------------------------------------------------

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

open import Relation.Binary using (DecSetoid)

module Data.Vec.Membership.DecSetoid {c ℓ} (DS : DecSetoid c ℓ) where

open import Data.Vec using (Vec)
open import Data.Vec.Relation.Unary.Any using (any)
open import Relation.Nullary using (Dec)
open DecSetoid DS renaming (Carrier to A)

------------------------------------------------------------------------
-- Re-export contents of propositional membership

open import Data.Vec.Membership.Setoid setoid public

------------------------------------------------------------------------
-- Other operations

infix 4 _∈?_

_∈?_ : ∀ x {n} (xs : Vec A n) → Dec (x ∈ xs)
x ∈? xs = any (x ≟_) xs


text:
module _ where

open import Agda.Primitive.Cubical

postulate
  PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

{-# BUILTIN PATHP        PathP     #-}


text:
module #8 where

{-
  Define multiplication and exponentiation using recN. Verify that (N, +, 0, ×, 1) is
  a semiring using only indN. You will probably also need to use symmetry and transitivity of
  equality, Lemmas 2.1.1 and 2.1.2.
-}

open import Data.Nat

recₙ : ∀{c}{C : Set c} → C → (ℕ → C → C) → ℕ → C
recₙ c₀ cₛ zero = c₀
recₙ c₀ cₛ (suc n) = cₛ n (recₙ c₀ cₛ n)

mul-recₙ : ℕ → ℕ → ℕ
mul-recₙ n = recₙ 0 (λ _ z → z + n)

exp-recₙ : ℕ → ℕ → ℕ
exp-recₙ n = recₙ 1 (λ _ z → z * n)

ind-ℕ : ∀{k}{C : ℕ → Set k} → C zero → ((n : ℕ) → C n → C (suc n)) → (n : ℕ) → C n
ind-ℕ c0 cs zero = c0
ind-ℕ c0 cs (suc n) = cs n (ind-ℕ c0 cs n)

record Semiring (X : Set) : Set where
  field
    ε : X
    _⊕_ : X → X → X
    _⊛_ : X → X → X
open Semiring {{...}} public

natIsSemiring : Semiring ℕ
natIsSemiring = record { ε = zero
                       ; _⊕_ = _+_
                       ; _⊛_ = _*_
                       }

{- Semiring Laws Follow -}

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
---------------------------------------
-- Pairs of sets
---------------------------------------

{-# OPTIONS --allow-unsolved-meta #-}

module sv20.assign2.SetTheory.Pairs where

-- Everything involving pairs, be them unordered
-- or ordered pairs. Also the definition of power set
-- and cartesian product between sets.

open import sv20.assign2.SetTheory.Logic
open import sv20.assign2.SetTheory.Algebra
open import sv20.assign2.SetTheory.Subset
open import sv20.assign2.SetTheory.ZAxioms

-- Pairs, justified by the pair axiom

_ₚ_ : 𝓢 → 𝓢 → 𝓢
x ₚ y = proj₁ (pair x y)

pair-d : (x y : 𝓢) → ∀ {z} → z ∈ x ₚ y ⇔ (z ≡ x ∨ z ≡ y)
pair-d x y = proj₂ _ (pair x y)

-- Both ∧-projections
pair-d₁ : (x y : 𝓢) → ∀ {z} → z ∈ x ₚ y → (z ≡ x ∨ z ≡ y)
pair-d₁ x y = ∧-proj₁ (pair-d x y)

pair-d₂ : (x y : 𝓢) → ∀ {z} → (z ≡ x ∨ z ≡ y) → z ∈ x ₚ y
pair-d₂ x y = ∧-proj₂ (pair-d x y)

pair-p₁ : (x y : 𝓢) → x ₚ y ≡ y ₚ x
pair-p₁ x y = equalitySubset (x ₚ y) (y ₚ x) (p₁ , p₂)
  where
  p₁ : (z : 𝓢) → z ∈ x ₚ y → z ∈ y ₚ x
  p₁ z z∈x,y = pair-d₂ y x (∨-sym _ _ (pair-d₁ x y z∈x,y))

  p₂ : (z : 𝓢) → z ∈ y ₚ x → z ∈ x ₚ y
  p₂ z z∈y,x = pair-d₂ x y (∨-sym _ _ (pair-d₁ y x z∈y,x))

singleton : 𝓢 → 𝓢
singleton x = x ₚ x

singletonp : (x : 𝓢) → ∀ {z} → z ∈ singleton x → z ≡ x
singletonp x x₁ = ∨-idem _ (pair-d₁ x x x₁)

singletonp₂ : (x : 𝓢) → x ∈ singleton x
singletonp₂ x = pair-d₂ x x (inj₁ refl)

singletonp₃ : (x : 𝓢) → ∀ {y} → x ≡ y → x ∈ singleton y
singletonp₃ x x≡y = pair-d₂ _ _ (inj₁ x≡y)

singletonp₄ : (x y : 𝓢) → x ∈ singleton y → x ∩ singleton y ≡ ∅
singletonp₄ x y h = {!!}
  where
  p₁ : x ≡ y
  p₁ = singletonp _ h

  p₂ : x ∩ singleton x ≡ ∅
  p₂ = {!!}

pair-prop-helper₁ : {a b c : 𝓢} → a ≡ b ∨ a ≡ c → a ≢ b → a ≡ c
pair-prop-helper₁ (inj₁ a≡b) h = ⊥-elim (h a≡b)
pair-prop-helper₁ (inj₂ refl) _ = refl

pair-prop-helper₂ : {a b : 𝓢} → a ≢ b → b ≢ a
pair-prop-helper₂ h b≡a = h (sym _ _ b≡a)

-- Theorem 44, p. 31 (Suppes, 1972).
pair-prop : (x y u v : 𝓢) → x ₚ y ≡ u ₚ v → (u ≡ x ∧ v ≡ y) ∨ (v ≡ x ∧ u ≡ y)
pair-prop x y u v eq = ∨-e _ _ _ (pem (x ≡ y)) h-x≡y h-x≢y
  where
  u∈u,v : u ∈ (u ₚ v)
  u∈u,v = ∨-prop₁ (pair-d₂ u v) refl

  u∈x,y : u ∈ (x ₚ y)
  u∈x,y = memberEq u (u ₚ v) (x ₚ y) (u∈u,v , (sym _ _ eq))

  disj₁ : u ≡ x ∨ u ≡ y
  disj₁ = pair-d₁ _ _ u∈x,y

  v∈u,v : v ∈ (u ₚ v)
  v∈u,v = ∨-prop₂ (pair-d₂ u v) refl

  v∈x,y : v ∈ (x ₚ y)
  v∈x,y = memberEq v (u ₚ v) (x ₚ y) (v∈u,v , (sym _ _ eq))

  disj₂ : v ≡ x ∨ v ≡ y
  disj₂ = pair-d₁ _ _ v∈x,y

  x∈x,y : x ∈ (x ₚ y)
  x∈x,y = ∨-prop₁ (pair-d₂ x y) refl

  x∈u,v : x ∈ (u ₚ v)
  x∈u,v = memberEq x (x ₚ y) (u ₚ v) (x∈x,y , eq)

  disj₃ : x ≡ u ∨ x ≡ v
  disj₃ = pair-d₁ _ _ x∈u,v

  y∈x,y : y ∈ (x ₚ y)
  y∈x,y = ∨-prop₂ (pair-d₂ x y) refl

  y∈u,v : y ∈ (u ₚ v)
  y∈u,v = memberEq y (x ₚ y) (u ₚ v) (y∈x,y , eq)

  disj₄ : y ≡ u ∨ y ≡ v
  disj₄ = pair-d₁ _ _ y∈u,v

  h-x≡y : x ≡ y → (u ≡ x ∧ v ≡ y) ∨ (v ≡ x ∧ u ≡ y)
  h-x≡y eq₂ = inj₁ (x≡u , v≡y)
    where
    x≡u : u ≡ x
    x≡u = ∨-idem _ disj-aux
      where
      disj-aux : u ≡ x ∨ u ≡ x
      disj-aux = subs _ (sym _ _ eq₂) disj₁

    v≡y : v ≡ y
    v≡y = ∨-idem _ disj-aux
      where
      disj-aux : v ≡ y ∨ v ≡ y
      disj-aux = subs _ eq₂ disj₂

  h-x≢y : x ≢ y → (u ≡ x ∧ v ≡ y) ∨ (v ≡ x ∧ u ≡ y)
  h-x≢y ¬eq = ∨-e _ _ _ (pem (x ≡ u)) h₁ h₂
    where
    h₁ : x ≡ u → (u ≡ x ∧ v ≡ y) ∨ (v ≡ x ∧ u ≡ y)
    h₁ x≡u = ∨-e _ _ _ (pem (y ≡ u)) h₁₁ h₁₂
      where
      h₁₁ : y ≡ u → (u ≡ x ∧ v ≡ y) ∨ (v ≡ x ∧ u ≡ y)
      h₁₁ y≡u = ⊥-elim (¬eq (trans x≡u (sym _ _ y≡u)))

      h₁₂ : y ≢ u → (u ≡ x ∧ v ≡ y) ∨ (v ≡ x ∧ u ≡ y)
      h₁₂ h = inj₁ (sym _ _ x≡u , sym _ _ (pair-prop-helper₁ disj₄ h))

    h₂ : x ≢ u → (u ≡ x ∧ v ≡ y) ∨ (v ≡ x ∧ u ≡ y)
    h₂ h = inj₂ (sym _ _ (pair-prop-helper₁ disj₃ h)
                ,
                (pair-prop-helper₁ disj₁ (pair-prop-helper₂ h)))

-- Theorem 45, p. 32 (Suppes 1960).
singleton-eq : (x y : 𝓢) → singleton x ≡ singleton y → x ≡ y
singleton-eq x y eq = sym _ _ (∧-proj₁ (∨-idem _ aux))
  where
  aux : ((y ≡ x) ∧ (y ≡ x)) ∨ ((y ≡ x) ∧ (y ≡ x))
  aux = pair-prop x x y y eq

singleton-⊆ : (x A : 𝓢) → x ∈ A → singleton x ⊆ A
singleton-⊆ x A x∈A t t∈xₛ = subs _ (sym _ _ (singletonp _ t∈xₛ)) x∈A

prop-p₂ : (y z : 𝓢) → y ₚ z ≡ singleton y ∪ singleton z
prop-p₂ y z = equalitySubset _ _ (p₁ , p₂)
  where
  p₁ : (x : 𝓢) → x ∈ y ₚ z → x ∈ singleton y ∪ singleton z
  p₁ _ h = ∪-d₂ _ _ (∨-prop₅ (pair-d₁ _ _ h) (singletonp₃ _) (singletonp₃ _))

  p₂ : (x : 𝓢) → x ∈ singleton y ∪ singleton z → x ∈ y ₚ z
  p₂ x h = pair-d₂ _ _ (∨-prop₅ (∪-d₁ _ _ h) (singletonp _) (singletonp _))

-- Ordered pairs

_ₒ_ : 𝓢 → 𝓢 → 𝓢
x ₒ y = singleton x ₚ (x ₚ y)

-- Just an abvreviation for next theorem
abv₁ : 𝓢 → 𝓢 → 𝓢 → 𝓢 → Set
abv₁ u x v y = (u ₚ u ≡ x ₚ x ∧ u ₚ v ≡ x ₚ y) ∨ (u ₚ v ≡ x ₚ x ∧ u ₚ u ≡ x ₚ y)

-- Theorem 46, p. 32 (Suppes).
ord-p : (x y u v : 𝓢) → x ₒ y ≡ u ₒ v → x ≡ u ∧ y ≡ v
ord-p x y u v eq = ∨-e _ _ _ aux a→c b→c
  where
  aux : (singleton u ≡ singleton x ∧ (u ₚ v) ≡ (x ₚ y)) ∨
          ((u ₚ v) ≡ singleton x ∧ singleton u ≡ (x ₚ y))
  aux = pair-prop _ _ _ _ eq

  a→c : singleton u ≡ singleton x ∧ u ₚ v ≡ x ₚ y → x ≡ u ∧ y ≡ v
  a→c (eqₚ , eqₛ) = x≡u , y≡v
    where
    x≡u : x ≡ u
    x≡u = singleton-eq _ _ (sym _ _ eqₚ)

    p₁ : (x ≡ u ∧ y ≡ v) ∨ (y ≡ u ∧ x ≡ v)
    p₁ = pair-prop _ _ _ _ eqₛ

    p₂ : x ≡ u ∧ y ≡ v → y ≡ v
    p₂ (h₁ , h₂) = h₂

    p₃ : y ≡ u ∧ x ≡ v → y ≡ v
    p₃ (h₁ , h₂) = subs (λ w → w ≡ v) x≡y h₂
      where
      x≡y : x ≡ y
      x≡y = subs (λ w → x ≡ w) (sym y u h₁) x≡u

    y≡v : y ≡ v
    y≡v = ∨-e _ _ _ p₁ p₂ p₃
  b→c : u ₚ v ≡ singleton x ∧ singleton u ≡ x ₚ y → x ≡ u ∧ y ≡ v
  b→c (h₁ , h₂) = p₃ , subs (λ w → w ≡ v) p₈ p₄
    where
    p₁ : (x ≡ u ∧ x ≡ v) ∨ (x ≡ u ∧ x ≡ v)
    p₁ = pair-prop _ _ _ _ h₁

    p₂ : x ≡ u ∧ x ≡ v
    p₂ = ∨-idem _ p₁

    p₃ : x ≡ u
    p₃ = ∧-proj₁ p₂

    p₄ : x ≡ v
    p₄ = ∧-proj₂ p₂

    p₅ : (x ≡ u ∧ y ≡ u) ∨ (y ≡ u ∧ x ≡ u)
    p₅ = pair-prop _ _ _ _ h₂

    p₆ : x ≡ u ∧ y ≡ u
    p₆ = ∨-∧ p₅

    p₇ : y ≡ u
    p₇ = ∧-proj₂ p₆

    p₈ : x ≡ y
    p₈ = subs (λ w → w ≡ y) (sym _ _ p₃) (sym _ _ p₇)

-- Power sets

𝓟_ : 𝓢 → 𝓢
𝓟 x = proj₁ (pow x)

-- Theorem 86, p. 47 (Suppes 1960)
𝓟-d : (x : 𝓢) → ∀ {z} → z ∈ (𝓟 x) ⇔ z ⊆ x
𝓟-d x = proj₂ _ (pow x)

-- Both projections.
𝓟-d₁ : (x : 𝓢) → ∀ {z} → z ∈ (𝓟 x) → z ⊆ x
𝓟-d₁ _ = ∧-proj₁ (𝓟-d _)

𝓟-d₂ : (x : 𝓢) → ∀ {z} → z ⊆ x → z ∈ (𝓟 x)
𝓟-d₂ _ = ∧-proj₂ (𝓟-d _)

-- Theorem 87, p. 47 (Suppes 1960).
A∈𝓟A : (A : 𝓢) → A ∈ 𝓟 A
A∈𝓟A A = 𝓟-d₂ A subsetOfItself

-- Theorem 91, p. 48 (Suppes 1960).
⊆𝓟 : (A B : 𝓢) → A ⊆ B ⇔ 𝓟 A ⊆ 𝓟 B
⊆𝓟 A B = iₗ , iᵣ
  where
  iₗ : A ⊆ B → 𝓟 A ⊆ 𝓟 B
  iₗ A⊆B t t∈𝓟A = 𝓟-d₂ _ t⊆B
    where
     t⊆A : t ⊆ A
     t⊆A = 𝓟-d₁ A t∈𝓟A

     t⊆B : t ⊆ B
     t⊆B = trans-⊆ _ _ _ (t⊆A , A⊆B)
  iᵣ : 𝓟 A ⊆ 𝓟 B → A ⊆ B
  iᵣ 𝓟A⊆𝓟B t t∈A = 𝓟-d₁ _ A∈𝓟B _ t∈A
    where
    A∈𝓟B : A ∈ 𝓟 B
    A∈𝓟B = 𝓟A⊆𝓟B _ (A∈𝓟A _)

-- Theorem 92, p. 48 (Suppes 1960).
𝓟∪ : (A B : 𝓢) → (𝓟 A) ∪ (𝓟 B) ⊆ 𝓟 (A ∪ B)
𝓟∪ A B t t∈𝓟A∪𝓟B = 𝓟-d₂ _ t⊆A∪B
  where
  ∪₁ : t ∈ 𝓟 A ∨ t ∈ 𝓟 B
  ∪₁ = ∪-d₁ _ _ t∈𝓟A∪𝓟B

  p : t ⊆ A ∨ t ⊆ B
  p = ∨-prop₄ aux₁ (𝓟-d₁ _)
    where
    aux₁ : t ⊆ A ∨ t ∈ 𝓟 B
    aux₁ = ∨-prop₃ ∪₁ (𝓟-d₁ _)
  t⊆A∪B : t ⊆ A ∪ B
  t⊆A∪B = ∪-prop₂ _ _ _ p

-- Cartesian Product. First we have to prove some things using
-- the subset axiom in order to be able to define cartesian products.

-- Two abvreviations to make sub₄ shorter.

abv₂ : 𝓢 → 𝓢 → 𝓢 → Set
abv₂ z A B = z ∈ 𝓟 (𝓟 (A ∪ B))

abv₃ : 𝓢 → 𝓢 → 𝓢 → Set
abv₃ z A B = ∃ (λ y → ∃ (λ w → (y ∈ A ∧ w ∈ B) ∧ z ≡ y ₒ w))

--Instance of the subset axiom.
sub₄ : (A B : 𝓢) → ∃ (λ C → {z : 𝓢} → z ∈ C ⇔ abv₂ z A B ∧ abv₃ z A B)
sub₄ A B = sub (λ x → abv₃ x A B) (𝓟 (𝓟 (A ∪ B)))

-- Proved inside theorem 95, p. 49 (Suppes 1960)
prop₁ : (A B x : 𝓢) → abv₃ x A B → abv₂ x A B
prop₁ A B x (y , (z , ((y∈A , z∈B) , eqo))) = subs _ (sym _ _ eqo)  yₒz∈𝓟𝓟A∪B
  where
  yₛ⊆A : singleton y ⊆ A
  yₛ⊆A = singleton-⊆ _ _ y∈A

  yₛ⊆A∪B : singleton y ⊆ A ∪ B
  yₛ⊆A∪B t t∈yₛ = trans-⊆ _ _ _ (yₛ⊆A , (∪-prop _ _)) _ t∈yₛ

  zₛ⊆B : singleton z ⊆ B
  zₛ⊆B = singleton-⊆ _ _ z∈B

  zₛ⊆A∪B : singleton z ⊆ A ∪ B
  zₛ⊆A∪B t t∈zₛ = trans-⊆ _ _ _ (zₛ⊆B , ∪-prop₃ _ _) _ t∈zₛ

  y,z⊆A∪B : y ₚ z ⊆ A ∪ B
  y,z⊆A∪B t t∈y,z = ∪-prop₄ _ _ _ yₛ⊆A∪B zₛ⊆A∪B _ p
    where
    p : t ∈ singleton y ∪ singleton z
    p = subs (λ w → t ∈ w) (prop-p₂ y z) t∈y,z
  yₛ∈𝓟A∪B : singleton y ∈ 𝓟 (A ∪ B)
  yₛ∈𝓟A∪B = 𝓟-d₂ _ yₛ⊆A∪B

  y,z∈𝓟A∪B : y ₚ z ∈ 𝓟 (A ∪ B)
  y,z∈𝓟A∪B = 𝓟-d₂ _ y,z⊆A∪B

  yₒz⊆𝓟A∪B : y ₒ z ⊆ 𝓟 (A ∪ B)
  yₒz⊆𝓟A∪B t t∈o = ∨-e _ _ _ (pair-d₁ _ _ t∈o) i₁ i₂
    where
    i₁ : t ≡ singleton y → t ∈ 𝓟 (A ∪ B)
    i₁ eq = subs _ (sym t (singleton y) eq) yₛ∈𝓟A∪B

    i₂ : t ≡ y ₚ z → t ∈ 𝓟 (A ∪ B)
    i₂ eq = subs _ (sym t (y ₚ z) eq) y,z∈𝓟A∪B
  yₒz∈𝓟𝓟A∪B : y ₒ z ∈ 𝓟 (𝓟 (A ∪ B))
  yₒz∈𝓟𝓟A∪B = 𝓟-d₂ _ yₒz⊆𝓟A∪B

Aᵤ : 𝓢 → 𝓢 → 𝓢
Aᵤ A B = proj₁ (sub₄ A B)

-- Theorem 95, p 49 (Suppes 1960).
pAᵤ : (A B : 𝓢) → {z : 𝓢} → z ∈ (Aᵤ A B) ⇔ abv₂ z A B ∧ abv₃ z A B
pAᵤ A B = proj₂ _ (sub₄ A B)

crts : (A B : 𝓢) → ∃ (λ C → (z : 𝓢) → z ∈ C ⇔ abv₃ z A B)
crts A B  = (Aᵤ A B) , (λ w → ⇔-p₂ w (pAᵤ A B) (prop₁ A B w))

_X_ : 𝓢 → 𝓢 → 𝓢
A X B = proj₁ (crts A B)

-- Theorem 97, p. 50 (Suppes 1960).
crts-p : (A B x : 𝓢) → x ∈ A X B ⇔ abv₃ x A B
crts-p A B x = proj₂ _ (crts A B) x

-- Both projections
crts-p₁ : (A B x : 𝓢) →  x ∈ A X B → abv₃ x A B
crts-p₁ A B x = ∧-proj₁ (crts-p A B x)

crts-p₂ : (A B x : 𝓢) → abv₃ x A B → x ∈ A X B
crts-p₂ A B x = ∧-proj₂ (crts-p A B x)

crts-d₁ : (x y A B : 𝓢) → x ₒ y ∈ A X B → x ∈ A ∧ y ∈ B
crts-d₁ x y A B h = (subs (λ w → w ∈ A) (sym _ _ eq₁) aux∈A)
                         ,
                         subs (λ w → w ∈ B) (sym _ _ eq₂) aux₂∈B
  where
  foo : ∃ (λ z → ∃ (λ w → (z ∈ A ∧ w ∈ B) ∧ (x ₒ y) ≡ (z ₒ w)))
  foo = crts-p₁ A B (x ₒ y) h

  aux : 𝓢
  aux = proj₁ foo

  aux-p : ∃ (λ w → (aux ∈ A ∧ w ∈ B) ∧ (x ₒ y) ≡ (aux ₒ w))
  aux-p = proj₂ _ foo

  aux₂ : 𝓢
  aux₂ = proj₁ aux-p

  aux₂-p : (aux ∈ A ∧ aux₂ ∈ B) ∧ (x ₒ y) ≡ (aux ₒ aux₂)
  aux₂-p = proj₂ _ aux-p

  aux∈A : aux ∈ A
  aux∈A = ∧-proj₁ (∧-proj₁ aux₂-p)

  aux₂∈B : aux₂ ∈ B
  aux₂∈B = ∧-proj₂ (∧-proj₁ aux₂-p)

  eq : x ₒ y ≡ aux ₒ aux₂
  eq = ∧-proj₂ aux₂-p

  eqs : x ≡ aux ∧ y ≡ aux₂
  eqs = ord-p _ _ _ _ eq

  eq₁ : x ≡ aux
  eq₁ = ∧-proj₁ eqs

  eq₂ : y ≡ aux₂
  eq₂ = ∧-proj₂ eqs

-- References
--
-- Suppes, Patrick (1960). Axiomatic Set Theory.
-- The University Series in Undergraduate Mathematics.
-- D. Van Nostrand Company, inc.
--
-- Enderton, Herbert B. (1977). Elements of Set Theory.
-- Academic Press Inc.


text:
postulate
  A : Set
  I : ..(_ : A) → Set
  R : A → Set
  f : ∀ ..(x : A) (r : R x) → I x
 -- can now be used here ^

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module examplesPaperJFP.VariableListForDispatchOnly where

open import Data.Product hiding (map)
open import Data.List

open import NativeIO
open import StateSizedIO.GUI.WxBindingsFFI
open import Relation.Binary.PropositionalEquality

data VarList : Set₁ where
  []      :  VarList
  addVar  :  (A : Set) → Var A → VarList → VarList

prod : VarList → Set
prod  []               =  Unit
prod  (addVar A v [])  =  A
prod  (addVar A v l)   =  A × prod l

takeVar : (l : VarList) → NativeIO (prod l)
takeVar  []                            = nativeReturn unit
takeVar (addVar A v [])                =
  nativeTakeVar {A} v native>>= λ a →  nativeReturn a
takeVar (addVar A v (addVar B v′ l))   =
  nativeTakeVar {A} v     native>>= λ a →
  takeVar (addVar B v′ l) native>>= λ rest →  nativeReturn ( a , rest )

putVar : (l : VarList) → prod l → NativeIO Unit
putVar  [] _                                     = nativeReturn unit
putVar  (addVar A v []) a                        = nativePutVar {A} v a
putVar  (addVar A v (addVar B v′ l)) (a , rest)  =
  nativePutVar {A} v a          native>>= λ _ →
  putVar (addVar B v′ l)  rest  native>>= nativeReturn

dispatch : (l : VarList) → (prod l → NativeIO (prod l)) → NativeIO Unit
dispatch l f =  takeVar l     native>>= λ a   →
                f a           native>>= λ a₁  →
                putVar l a₁

dispatchList : (l : VarList) → List (prod l → NativeIO (prod l)) → NativeIO Unit
dispatchList l []          =  nativeReturn unit
dispatchList l (p ∷ rest)  =  dispatch l p         native>>= λ _ →
                              dispatchList l rest

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

open import lib.Basics

{-
The generic nonrecursive higher inductive type with one point constructor and
one paths constructor.
-}

module lib.types.Generic1HIT {i j} (A : Type i) (B : Type j)
  (g h : B → A) where

{-
data T : Type where
  cc : A → T
  pp : (b : B) → cc (f' b) ≡ cc (g b)
-}
module _ where
  private
    data #T-aux : Type (lmax i j) where
      #cc : A → #T-aux

    data #T : Type (lmax i j) where
      #t : #T-aux → (Unit → Unit) → #T

  T : Type _
  T = #T

  cc : A → T
  cc a = #t (#cc a) _

  postulate  -- HIT
    pp : (b : B) → cc (g b) == cc (h b)

  module Elim {k} {P : T → Type k} (cc* : (a : A) → P (cc a))
    (pp* : (b : B) → cc* (g b) == cc* (h b) [ P ↓ pp b ]) where

    f : Π T P
    f = f-aux phantom  where

      f-aux : Phantom pp* → Π T P
      f-aux phantom (#t (#cc a) _) = cc* a

    postulate  -- HIT
      pp-β : (b : B) → apd f (pp b) == pp* b

open Elim public using () renaming (f to elim)

module Rec {k} {C : Type k} (cc* : A → C)
  (pp* : (b : B) → cc* (g b) == cc* (h b)) where

  private module M = Elim cc* (λ b → ↓-cst-in (pp* b))

  f : T → C
  f = M.f

  pp-β : (b : B) → ap f (pp b) == pp* b
  pp-β b = apd=cst-in {f = f} (M.pp-β b)

module RecType {k} (C : A → Type k) (D : (b : B) → C (g b) ≃ C (h b)) where

  open Rec C (ua ∘ D) public

  coe-pp-β : (b : B) (d : C (g b)) → coe (ap f (pp b)) d == –> (D b) d
  coe-pp-β b d =
    coe (ap f (pp b)) d   =⟨ pp-β _ |in-ctx (λ u → coe u d) ⟩
    coe (ua (D b)) d      =⟨ coe-β (D b) d ⟩
    –> (D b) d ∎

  -- Dependent path in [P] over [pp b]
  module _ {b : B} {d : C (g b)} {d' : C (h b)} where
    ↓-pp-in : –> (D b) d == d' → d == d' [ f ↓ pp b ]
    ↓-pp-in p = from-transp f (pp b) (coe-pp-β b d ∙' p)

    ↓-pp-out : d == d' [ f ↓ pp b ] → –> (D b) d == d'
    ↓-pp-out p = ! (coe-pp-β b d) ∙ to-transp p

    ↓-pp-β : (q : –> (D b) d == d') → ↓-pp-out (↓-pp-in q) == q
    ↓-pp-β q =
      ↓-pp-out (↓-pp-in q)
                        =⟨ idp ⟩
      ! (coe-pp-β b d) ∙ to-transp (from-transp f (pp b) (coe-pp-β b d ∙' q))
                 =⟨ to-transp-β f (pp b) (coe-pp-β b d ∙' q) |in-ctx (λ u → ! (coe-pp-β b d) ∙ u) ⟩
      ! (coe-pp-β b d) ∙ (coe-pp-β b d ∙' q)
                 =⟨ lem (coe-pp-β b d) q ⟩
      q ∎  where

        lem : ∀ {i} {A : Type i} {x y z : A} (p : x == y) (q : y == z)
          → ! p ∙ (p ∙' q) == q
        lem idp idp = idp

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Andreas, 2017-01-12, issue #2386

id : ∀{a}{A : Set a} → A → A
id x = x

data Eq (A : Set) : (x y : id A) → Set where
  refl : (x : A) → Eq A x x

{-# BUILTIN EQUALITY Eq #-}

-- Should be accepted.


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

open import Everything.Safe

-- This file contains everything that is --safe, but uses K.
open import Logic.PropositionalLogic
open import Logic.PropositionalLogicExamples
open import Logic.PropositionalAxiomsTautology

open import Sets.FinSetWithK

open import Groups.FreeGroup.Lemmas
open import Groups.FreeGroup.UniversalProperty
open import Groups.FreeGroup.Parity
open import Groups.FreeProduct.UniversalProperty

module Everything.WithK where


text:
module Generic.Lib.Data.Product where

open import Data.Product renaming (map to pmap; zip to pzip) hiding (map₁; map₂) public

open import Generic.Lib.Intro
open import Generic.Lib.Category

infixl 4 _,ᵢ_

first : ∀ {α β γ} {A : Set α} {B : Set β} {C : A -> Set γ}
      -> (∀ x -> C x) -> (p : A × B) -> C (proj₁ p) × B
first f (x , y) = f x , y

second : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : A -> Set γ}
       -> (∀ {x} -> B x -> C x) -> Σ A B -> Σ A C
second g (x , y) = x , g y

-- `B` and `C` are in the same universe.
firstF : ∀ {α β} {A : Set α} {B : Set β} {C : A -> Set β}
           {F : Set β -> Set β} {{fFunctor : RawFunctor F}}
       -> (∀ x -> F (C x)) -> (p : A × B) -> F (C (proj₁ p) × B)
firstF f (x , y) = flip _,_ y <$> f x

-- `A` and `C` are in the same universe.
secondF : ∀ {α β} {A : Set α} {B : A -> Set β} {C : A -> Set α}
            {F : Set α -> Set α} {{fFunctor : RawFunctor F}}
        -> (∀ {x} -> B x -> F (C x)) -> Σ A B -> F (Σ A C)
secondF g (x , y) = _,_ x <$> g y

record Σᵢ {α β} (A : Set α) (B : .A -> Set β) : Set (α ⊔ β) where
  constructor _,ᵢ_
  field
    .iproj₁ : A
    iproj₂  : B iproj₁
open Σᵢ public

∃ᵢ : ∀ {α β} {A : Set α} -> (.A -> Set β) -> Set (α ⊔ β)
∃ᵢ = Σᵢ _

instance
  ,-inst : ∀ {α β} {A : Set α} {B : A -> Set β} {{x : A}} {{y : B x}} -> Σ A B
  ,-inst {{x}} {{y}} = x , y

  ,ᵢ-inst : ∀ {α β} {A : Set α} {B : .A -> Set β} {{x : A}} {{y : B x}} -> Σᵢ A B
  ,ᵢ-inst {{x}} {{y}} = x ,ᵢ y

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


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

module Cubical.HITs.Modulo where

open import Cubical.HITs.Modulo.Base public
open import Cubical.HITs.Modulo.Properties public


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

module Categories.Utils.EqReasoning where

open import Level
open import Relation.Binary.PropositionalEquality
open import Data.Product using (Σ; _,_; _×_)

open import Categories.Utils.Product

subst₂-sym-subst₂ : {ℓa ℓb ℓp : Level} {A : Set ℓa} {B : Set ℓb} {a₁ a₂ : A} {b₁ b₂ : B}
                    (R : A → B → Set ℓp) {p : R a₁ b₁} (eq₁ : a₁ ≡ a₂) (eq₂ : b₁ ≡ b₂) →
                    subst₂ R (sym eq₁) (sym eq₂) (subst₂ R eq₁ eq₂ p) ≡ p
subst₂-sym-subst₂ R refl refl = refl

subst₂-subst₂-sym : {ℓa ℓb ℓp : Level} {A : Set ℓa} {B : Set ℓb} {a₁ a₂ : A} {b₁ b₂ : B}
                    (R : A → B → Set ℓp) {p : R a₁ b₁} (eq₁ : a₂ ≡ a₁) (eq₂ : b₂ ≡ b₁) →
                    subst₂ R eq₁ eq₂ (subst₂ R (sym eq₁) (sym eq₂) p) ≡ p
subst₂-subst₂-sym R refl refl = refl

subst₂-subst₂ : {ℓa ℓb ℓp : Level} {A : Set ℓa} {B : Set ℓb} {a₁ a₂ a₃ : A} {b₁ b₂ b₃ : B}
              (R : A → B → Set ℓp) {p : R a₁ b₁}
              (eq-a₁₂ : a₁ ≡ a₂) (eq-a₂₃ : a₂ ≡ a₃)
              (eq-b₁₂ : b₁ ≡ b₂) (eq-b₂₃ : b₂ ≡ b₃) →
              subst₂ R eq-a₂₃ eq-b₂₃ (subst₂ R eq-a₁₂ eq-b₁₂ p) ≡ subst₂ R (trans eq-a₁₂ eq-a₂₃) (trans eq-b₁₂ eq-b₂₃) p
subst₂-subst₂ R refl refl refl refl = refl

subst₂-app : ∀ {a₁ a₂ a₃ a₄ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂} {A₃ : Set a₃} {A₄ : Set a₄}
                  (B₁ : A₁ → A₃ → Set b₁) {B₂ : A₂ → A₄ → Set b₂}
                  {f : A₂ → A₁} {h : A₄ → A₃} {x₁ x₂ : A₂} {x₃ x₄ : A₄} (y : B₂ x₁ x₃)
                  (g : ∀ w z → B₂ w z → B₁ (f w) (h z)) (eq₁ : x₁ ≡ x₂) (eq₂ : x₃ ≡ x₄) →
                  subst₂ B₁ (cong f eq₁) (cong h eq₂) (g x₁ x₃ y) ≡ g x₂ x₄ (subst₂ B₂ eq₁ eq₂ y)
subst₂-app _ _ _ refl refl = refl

subst₂-prod : ∀ {ℓa ℓb ℓr ℓs} {A : Set ℓa} {B : Set ℓb}
      (R : A → A → Set ℓr) (S : B → B → Set ℓs) {a b c d : A} {x y z w : B}
      {f : R a b} {g : S x y}
      (eq₁ : a ≡ c) (eq₂ : b ≡ d) (eq₃ : x ≡ z) (eq₄ : y ≡ w) →
      subst₂ (λ { (p , q) (r , s) → R p r × S q s })
      (sym (cong₂ _,_ (sym eq₁) (sym eq₃)))
      (sym (cong₂ _,_ (sym eq₂) (sym eq₄)))
      (f , g)
      ≡
      (subst₂ R eq₁ eq₂ f , subst₂ S eq₃ eq₄ g)
subst₂-prod R S refl refl refl refl = refl

------------------
-- For reasoning with things from Categories.Utils.Product
subst₂-expand : ∀ {a b ℓ ℓ′ p q} {A : Set a} {B : Set b}
  {P : A → Set p} {Q : B → Set q}
  (_∙_ : A → B → Set ℓ) → (_∘_ : ∀ {x y} → P x → Q y → Set ℓ′) →
  {a₁ a₂ : A} {b₁ b₂ : B} {p₁ p₂ : P a₁} {q₁ q₂ : Q b₁}
  (eq₁ : a₁ ≡ a₂) (eq₂ : p₁ ≡ p₂) (eq₃ : b₁ ≡ b₂) (eq₄ : q₁ ≡ q₂) →
  (F : a₁ ∙ b₁) → (G : p₁ ∘ q₁) →
  subst₂ (_∙_ -< _×_ >- _∘_)
      (cong₂ _,_ eq₁ eq₂)
      (cong₂ _,_ eq₃ eq₄)
      (F , G) ≡ (subst₂ _∙_ eq₁ eq₃ F , subst₂ _∘_ eq₂ eq₄ G)
subst₂-expand T₁ T₂ refl refl refl refl F G = refl

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:
module BuildingBlock.BinaryLeafTree where

open import Function
open import Data.Nat
open import Data.Nat.Etc
open import Data.Nat.Properties.Simple using (+-right-identity)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Fin
    using (Fin; toℕ; fromℕ; fromℕ≤; reduce≥)
    renaming (zero to Fzero; suc to Fsuc)

open import Data.Empty

open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; trans; sym; inspect)
open PropEq.≡-Reasoning
--------------------------------------------------------------------------------
-- Complete Binary Leaf Trees

data BinaryLeafTree (A : Set) : ℕ → Set where
    Leaf : A → BinaryLeafTree A 0
    Node : ∀ {n} → BinaryLeafTree A n
                 → BinaryLeafTree A n
                 → BinaryLeafTree A (suc n)

-- splits a BinaryLeafTree into 2
split : ∀ {A n} → BinaryLeafTree A (suc n)
                → BinaryLeafTree A n × BinaryLeafTree A n
split (Node xs ys) = xs , ys

-- merge 2 BinaryLeafTree
merge : ∀ {A n} → BinaryLeafTree A n
                → BinaryLeafTree A n
                → BinaryLeafTree A (suc n)
merge = Node

split-merge : ∀ {n A} → (xs : BinaryLeafTree A (suc n))
            → merge (proj₁ (split xs)) (proj₂ (split xs)) ≡ xs
split-merge (Node xs ys) = refl

-- get the first element
head : ∀ {A n} → BinaryLeafTree A n → A
head (Leaf x) = x
head (Node xs ys) = head xs

-- searching
transportFin : ∀ {a b} → a ≡ b → Fin a → Fin b
transportFin refl i = i

¬a≤b⇒b<a : ∀ {a b} → ¬ (a ≤ b) → b < a
¬a≤b⇒b<a {zero } {b    } p = ⊥-elim (p z≤n)
¬a≤b⇒b<a {suc a} {zero } p = s≤s z≤n
¬a≤b⇒b<a {suc a} {suc b} p = s≤s (¬a≤b⇒b<a (λ z → p (s≤s z)))

elemAt : ∀ {A n} → BinaryLeafTree A n → Fin (2 ^ n) → A
elemAt {n = zero}  (Leaf x)     Fzero = x
elemAt {n = zero}  (Leaf x)     (Fsuc ())
elemAt {n = suc n} (Node xs ys) i with (2 ^ n) ≤? toℕ i
elemAt {n = suc n} (Node xs ys) i | yes p = elemAt ys (transportFin (+-right-identity (2 ^ n)) (reduce≥ {2 ^ n} {2 ^ n + 0} i p))
elemAt {n = suc n} (Node xs ys) i | no ¬p = elemAt xs (fromℕ≤ (¬a≤b⇒b<a ¬p))

-- examples
private
    fier : BinaryLeafTree ℕ 2
    fier = Node
            (Node
                (Leaf 0)
                (Leaf 2))
            (Node
                (Leaf 3)
                (Leaf 1))

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral