From d379e77dab3ff6a854b94af47be6098a2ba6ca64 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 10 Apr 2021 21:59:42 +0100 Subject: start hprop stuff --- hott/Bool_HoTT.thy | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 hott/Bool_HoTT.thy (limited to 'hott/Bool_HoTT.thy') diff --git a/hott/Bool_HoTT.thy b/hott/Bool_HoTT.thy new file mode 100644 index 0000000..57a57b7 --- /dev/null +++ b/hott/Bool_HoTT.thy @@ -0,0 +1,8 @@ +theory Bool_HoTT +imports + MLTT.Prelude + Propositions + +begin + +end -- cgit v1.2.3