Fun with isomorphisms in Pie

iso.pie

#lang pie

(claim Vect
  (→ U Nat
    U))
(define Vect
  (λ (A n)
    (iter-Nat
      n
      Trivial
      (λ (Rest) (Pair A Rest)))))

(claim vec-to-vect
  (∏ ((A U) (n Nat))
    (→ (Vec A n) (Vect A n))))
(define vec-to-vect
  (λ (A n xs)
    (ind-Vec n xs
      (λ (k v) (Vect A k))
      sole
      (λ (k e es v) (cons e v)))))

;(claim vect-to-vec
;  (∏ ((A U) (n Nat))
;    (→ (Vect A n) (Vec A n))))
;(define vect-to-vec
;  (λ (A n xs)
;    (ind-Nat n
;      (λ (k) (Vec A k))
;      vecnil
;      TODO))) ; not sure how to do this!

(claim list-to-nat
  (→ (List Trivial) Nat))
(define list-to-nat
  (λ (xs)
    (rec-List xs
      zero
      (λ (x xs n) (add1 n)))))

(claim nat-to-list
  (→ Nat (List Trivial)))
(define nat-to-list
  (λ (n)
    (iter-Nat n
      (the (List Trivial) nil)
      (λ (xs) (:: sole xs)))))

(claim Iso
  (→ U U
    U))
(define Iso
  (λ (A B)
    (Σ ((to (→ A B)) (from (→ B A)))
      (Pair
        (∏ ((x A)) (= A x (from (to x))))
        (∏ ((y B)) (= B y (to (from y))))))))

(claim Id
  (Π ((A U))
    (Iso A A)))
(define Id
  (λ (A)
    (cons
      (λ (x) x)
      (cons
        (λ (y) y)
        (cons
          (λ (x) (same x))
          (λ (y) (same y)))))))

(claim cons-sole
  (→ (List Trivial) (List Trivial)))
(define cons-sole
  (λ (xs) (:: sole xs)))

(claim list-to-nat-roundtrip
  (Π ((xs (List Trivial)))
    (= (List Trivial) xs (nat-to-list (list-to-nat xs)))))
(define list-to-nat-roundtrip
  (λ (xs)
    (ind-List xs
      (λ (ys) (= (List Trivial) ys (nat-to-list (list-to-nat ys))))
      (same nil)
      (λ (y ys prf)
        (cong prf cons-sole)))))

(claim add1-nat
  (→ Nat Nat))
(define add1-nat
  (λ (n) (add1 n)))

(claim nat-to-list-roundtrip
  (Π ((n Nat))
    (= Nat n (list-to-nat (nat-to-list n)))))
(define nat-to-list-roundtrip
  (λ (n)
    (ind-Nat n
      (λ (k) (= Nat k (list-to-nat (nat-to-list k))))
      (same zero)
      (λ (k prf)
        (cong prf add1-nat)))))

(claim nat-list-iso (Iso Nat (List Trivial)))
(define nat-list-iso
  (cons nat-to-list
    (cons list-to-nat
      (cons nat-to-list-roundtrip
        list-to-nat-roundtrip))))