Mercurial > hg > Members > kono > Proof > category
diff src/system-t.agda @ 1110:45de2b31bf02
add original library and fix for safe mode
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 07 Oct 2023 19:43:31 +0900 |
parents | ac53803b3b2a |
children |
line wrap: on
line diff
--- a/src/system-t.agda Thu Jul 20 12:36:15 2023 +0900 +++ b/src/system-t.agda Sat Oct 07 19:43:31 2023 +0900 @@ -1,4 +1,7 @@ -module system-t where +{-# OPTIONS --cubical-compatible --safe #-} + +module system-t (U : Set) (V : Set) (v : V) (u : U) where + open import Relation.Binary.PropositionalEquality record _×_ ( U : Set ) ( V : Set ) : Set where @@ -11,11 +14,6 @@ open _×_ -postulate U : Set -postulate V : Set - -postulate v : V -postulate u : U f : U → V f = λ u → v