Skip to content

Instantly share code, notes, and snippets.

@copumpkin

copumpkin/FinVector-cons.agda

Last active October 14, 2020 05:12
Show Gist options
  • Save copumpkin/72aa6738b5dba8dc05969e2bc286a137 to your computer and use it in GitHub Desktop.
Save copumpkin/72aa6738b5dba8dc05969e2bc286a137 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. copumpkin revised this gist Oct 14, 2020. 1 changed file with 2 additions and 0 deletions.
    2 changes: 2 additions & 0 deletions FinVector-cons.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -1,3 +1,5 @@
    module FinVector-cons (T : Set) where

    data Nat : Set where
    zero : Nat
    suc : Nat → Nat
  2. copumpkin created this gist Oct 14, 2020.
    34 changes: 34 additions & 0 deletions FinVector-cons.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,34 @@
    data Nat : Set where
    zero : Nat
    suc : Nat → Nat

    data Fin : Nat → Set where
    zero : ∀ {n} → Fin (suc n)
    suc : ∀ {n} → Fin n → Fin (suc n)

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

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

    B : Nat → Set
    B n = Fin n → T

    cons : ∀ {n} (t : T) → B n → B (suc n)
    cons x xs zero = x
    cons x xs (suc z) = xs z

    head : ∀ {n} → B (suc n) → T
    head xs = xs zero

    tail : ∀ {n} → B (suc n) → B n
    tail xs n = xs (suc n)


    cons-ok : ∀ {n} → (b : B (suc n)) → ∀ n → cons (head b) (tail b) n ≡ b n
    cons-ok b zero = refl
    cons-ok b (suc n) = refl

    cons-ok-ext : ∀ {n} → (b : B (suc n)) → cons (head b) (tail b) ≡ b
    cons-ok-ext b = funext (cons-ok b)