Mercurial > hg > Members > kono > Proof > category

comparison src/system-t.agda @ 1110:45de2b31bf02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
1109:71049ed05151 1110:45de2b31bf02
1 module system-t where 1 {-# OPTIONS --cubical-compatible --safe #-}
2
3 module system-t (U : Set) (V : Set) (v : V) (u : U) where
4
2 open import Relation.Binary.PropositionalEquality 5 open import Relation.Binary.PropositionalEquality
3 6
4 record _×_ ( U : Set ) ( V : Set ) : Set where 7 record _×_ ( U : Set ) ( V : Set ) : Set where
5 field 8 field
6 π1 : U 9 π1 : U
9 <_,_> : {U V : Set} → U → V → U × V 12 <_,_> : {U V : Set} → U → V → U × V
10 < u , v > = record {π1 = u ; π2 = v } 13 < u , v > = record {π1 = u ; π2 = v }
11 14
12 open _×_ 15 open _×_
13 16
14 postulate U : Set
15 postulate V : Set
16
17 postulate v : V
18 postulate u : U
19 17
20 f : U → V 18 f : U → V
21 f = λ u → v 19 f = λ u → v
22 20
23 21