Universes.agda

module Universes where

data False : Set where
record True : Set where

data Bool : Set where
  true  : Bool
  false : Bool

isTrue : Bool -> Set
isTrue true  = True
isTrue false = False

infix 30 not_
infixr 25 _and_

not_ : Bool -> Bool
not true  = false
not false = true

_and_ : Bool -> Bool -> Bool
true  and x = x
false and _ = false

notNoId : (a : Bool) -> isTrue (not not a) -> isTrue a
notNoId true p = p
notNoId false ()

andIntro : (a b : Bool) → isTrue a → isTrue b → isTrue (a and b)
andIntro true  _ _ p = p
andIntro false _ o _ = o    -- o は isTrue fase (= False)
-- andIntro false _ () _    -- これが論文に載っている形

open import Data.Nat

nonZero : ℕ → Bool
nonZero 0 = false
nonZero (suc _) = true  -- 何故 nonZero _ = true ではないのか
                        -- suc が必要なのか

postulate _div_ : ℕ → (m : ℕ) {p : isTrue (nonZero m)} → ℕ

three : ℕ
three = 16 div 5

-- 何故か下記の式はエラーにならない．???
div0 = 16 div 0

data Functor : Set1 where
  |Id|  : Functor
  |K|   : Set → Functor
  _|+|_ : Functor → Functor → Functor
  _|x|_ : Functor → Functor → Functor

data _⊕_ (A B : Set) : Set where
  inl : A → A ⊕ B
  inr : B → A ⊕ B

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B


infixr 50 _|+|_ _⊕_
infixr 60 _|x|_ _×_

[_] : Functor → Set → Set
[ |Id| ]    X = X
[ |K| A ]   X = A
[ F |+| G ] X = [ F ] X ⊕ [ G ] X
[ F |x| G ] X = [ F ] X × [ G ] X

map : (F : Functor) {X Y : Set} → (X → Y) → [ F ] X → [ F ] Y
map |Id|      f x = f x
map (|K| A)   f c = c
map (F |+| G) f (inl x) = inl (map F f x)
map (F |+| G) f (inr y) = inr (map G f y)
map (F |x| G) f (x , y) = map F f x , map G f y

data μ_ (F : Functor) : Set where
  <_> : [ F ] (μ F) → μ F

mapFold : ∀ {X} F G → ([ G ] X → X) → [ F ] (μ G) → [ F ] X
mapFold |Id|        G φ < x >   = φ (mapFold G G φ x)
mapFold (|K| x)     G φ c       = c
mapFold (F₁ |+| F₂) G φ (inl x) = {!!}
mapFold (F₁ |+| F₂) G φ (inr x) = {!!}
mapFold (F₁ |x| F₂) G φ (x , y) = {!!}