vikraman

{-# OPTIONS --type-in-type #-}

module Yoneda where

_∘_ : {a b c : Set} → (b → c) → (a → b) → (a → c)
f ∘ g = λ z → f (g z)

record Functor (f : Set → Set) : Set where
  field
    map : {a b : Set} → (a → b) → f a → f b

vikraman

(** * Stlc: Functorial semantics of STLC (McBride) *)

(** Coq programmers usually avoid using dependent types, because
    dependent pattern matching is difficult to use. However, with a
    principled use of the induction principle and using refine/eapply,
    dependently typed programming in Coq can be made enjoyable. *)

Module Stlc.

Inductive Ty : Type :=

vikraman

(set-option :auto-config false)
(set-option :model true)
(set-option :model.partial false)

(set-option :smt.mbqi false)
(define-sort Str () Int)
(declare-fun strLen (Str) Int)
(declare-fun subString (Str Int Int) Str)
(declare-fun concatString (Str Str) Str)
(define-sort Elt () Int)

vikraman

{-# OPTIONS --cubical #-}

module _ where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything

infixr 20 _∷_

data M {ℓ} (A : Type ℓ) : Type ℓ where