From 02fba6e949df5f6e15a03c0f73082bb9e29b40e5 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Thu, 21 Aug 2014 20:26:30 -0700
Subject: [PATCH] feat(library/standard/hott/fibrant.lean): add fibrant to
 library

---
 library/standard/hott/fibrant.lean | 35 ++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 library/standard/hott/fibrant.lean

diff --git a/library/standard/hott/fibrant.lean b/library/standard/hott/fibrant.lean
new file mode 100644
index 000000000..d58a854cd
--- /dev/null
+++ b/library/standard/hott/fibrant.lean
@@ -0,0 +1,35 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Jeremy Avigad
+
+import data.unit data.bool data.nat
+import data.prod data.sum data.sigma
+
+using unit bool nat prod sum sigma
+
+inductive fibrant (T : Type) : Type :=
+| fibrant_mk : fibrant T
+
+namespace fibrant
+
+axiom unit_fibrant : fibrant unit
+axiom nat_fibrant : fibrant nat
+axiom bool_fibrant : fibrant bool
+axiom sum_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A + B)
+axiom prod_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A × B)
+axiom sigma_fibrant {A : Type} {B : A → Type} (C1 : fibrant A) (C2 : Πx : A, fibrant (B x)) :
+  fibrant (Σx : A, B x)
+axiom pi_fibrant {A : Type} {B : A → Type} (C1 : fibrant A) (C2 : Πx : A, fibrant (B x)) :
+  fibrant (Πx : A, B x)
+
+instance unit_fibrant
+instance nat_fibrant
+instance bool_fibrant
+instance sum_fibrant
+instance prod_fibrant
+instance sigma_fibrant
+instance pi_fibrant
+
+theorem test_fibrant : fibrant (nat × (nat + nat)) := _
+
+end fibrant
\ No newline at end of file