co-dan

diff --git a/theories/list.v b/theories/list.v
index 2f1db8e..a200405 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2988,6 +2988,11 @@ Section setoid.
   Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
   Global Instance list_lookup_proper i : Proper ((≡@{list A}) ==> (≡)) (lookup i).
   Proof. induction i; destruct 1; simpl; try constructor; auto. Qed.
+  Global Instance list_lookup_total_proper `{!Inhabited A} i :
+    Proper ((≡@{list A}) ==> (≡)) (lookup_total i).

co-dan

--------------------------------------------------
-- Yoneda lemma

newtype Yoneda f a =
    Yoneda (forall b. (a -> b) -> f b)
    -- Nat (Hom(a, -), F) ~~ F a
    
-- this is `liftYoneda`
yoneda :: (Functor f) => f a -> Yoneda f a
yoneda x = Yoneda $ \f -> fmap f x

co-dan

Fixpoint code_poly (P Q : polynomial) : Type := 
  match P, Q with
  | poly_var, poly_var => Unit
  | poly_const C, poly_const C' => C = C'
  | poly_times Q R, poly_times Q' R' => (code_poly Q Q') * (code_poly R R')
  | poly_plus Q R , poly_plus Q' R'  => (code_poly Q Q') * (code_poly R R')
  | _, _ => Empty
  end.

co-dan

module Map2 where

--------------------------------------------------
-- * Prelude
--------------------------------------------------
-- Taken from: https://github.com/pigworker/Ohrid-Agda
open import Ohrid-Prelude
open import Ohrid-Nat

-- Mini HoTT (Except that we have K)

co-dan

(** Well-founded relations in intuitionistic type theory *)
(** last updated : 5 of April, 2017. email: dfrumin [at] cs.ru.nl *)
Definition relation A := A -> A -> Prop.

Section wf.
  Variable A : Type.
  Variable R : relation A.
  Notation "x '<' y" := (R x y).

  (** * Intuitionistic well-foundedness criteria *)

co-dan

let x = ref (fun z -> z) in
let f = fun z -> (!x) z in
x := f; f ()

(* f () → (!x) () → f () → ... *)

co-dan

#lang racket
(require racket/dict) ;; for dict-lookup for env

; eval-apply interpreter for call-by-value λ-calculus with call/cc
; scroll down to test1, test2 and yin & yang to see example programs

(define id (lambda (x) x))
(define initev '())
(define (ext k v e) 
  (cons (cons k v) e))

co-dan

#
# This simple script displays whether you are in a cabal sandbox
# the the result of checking for a sandbox is cached, but now that I
# actually think about it, it was probably an unnecessary step.
# Don't forget to customize the PROMPT variable at the bottom 
#
# Looks like this with my prompt: https://files.app.net/rjphjAG9.png
#

function update_cabal_sandbox_info () {

co-dan

Resolving dependencies...
Configuring diagrams-contrib-1.0.0.1...
Building diagrams-contrib-1.0.0.1...
Preprocessing library diagrams-contrib-1.0.0.1...

src/Diagrams/TwoD/Tilings.hs:94:39:
     warning: missing terminating ' character [-Winvalid-pp-token]
-- Instead of using Doubles, which can't be compared for equality, it
                                      ^

co-dan

{-# LANGUAGE TypeFamilies,
             MultiParamTypeClasses,
             FlexibleInstances,
             UndecidableInstances,
             FunctionalDependencies #-}

import Control.Concurrent
import Control.Monad
import Control.Monad.Fix
import JavaScript.JQuery