This file has been truncated, but you can view the full file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
[class_instances] class-instance resolution trace | |
[class_instances] (0) ?x_0 : @is_symmetric_smul (@units ℤ int.monoid) N₁ | |
(@mul_action.to_has_scalar (@units ℤ int.monoid) N₁ | |
(@div_inv_monoid.to_monoid (@units ℤ int.monoid) | |
(@group.to_div_inv_monoid (@units ℤ int.monoid) (@units.group ℤ int.monoid))) | |
(@distrib_mul_action.to_mul_action (@units ℤ int.monoid) N₁ | |
(@div_inv_monoid.to_monoid (@units ℤ int.monoid) | |
(@group.to_div_inv_monoid (@units ℤ int.monoid) (@units.group ℤ int.monoid))) | |
(@add_comm_monoid.to_add_monoid N₁ (@add_comm_group.to_add_comm_monoid N₁ _inst_16)) | |
(@units.distrib_mul_action ℤ N₁ int.monoid |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import function | |
open eq function is_equiv equiv is_trunc unit trunc | |
structure is_rel_contr (X Y : Type) := | |
(to_fun : X → Y) | |
(surj : is_split_surjective to_fun) | |
definition is_rel_contr_reflexive (X : Type) : is_rel_contr X X := | |
is_rel_contr.mk id (λ y, fiber.mk y idp) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open eq is_trunc | |
context | |
parameters (X A C : Type) [Xtrunc : is_trunc 2 X] | |
[Atrunc : is_trunc 1 A] [Cset : is_hset C] | |
(ι' : A → X) (ι : C → A) | |
definition fund_dbl_precat_flat_comp₁ {a₁ b₁ a₂ b₂ a₃ b₃ : X} | |
{f₁ : a₁ = b₁} {g₁ : a₂ = b₂} {h₁ : a₁ = a₂} {i₁ : b₁ = b₂} | |
{g₂ : a₃ = b₃} {h₂ : a₂ = a₃} {i₂ : b₂ = b₃} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import algebra.category.basic | |
open precategory morphism truncation eq sigma sigma.ops | |
structure worm_precat {D₀ : Type} (C : precategory D₀) | |
(D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), | |
Type) : Type := | |
(comp₁ : Π {a b c₁ d₁ c₂ d₂ : D₀} ⦃f₁ : hom a b⦄ ⦃g₁ : hom c₁ d₁⦄ ⦃h₁ : hom a c₁⦄ | |
⦃i₁ : hom b d₁⦄ ⦃g₂ : hom c₂ d₂⦄ ⦃h₂ : hom c₁ c₂⦄ ⦃i₂ : hom d₁ d₂⦄, | |
(D₂ g₁ g₂ h₂ i₂) → (D₂ f₁ g₁ h₁ i₁) → (@D₂ a b c₂ d₂ f₁ g₂ (h₂ ∘ h₁) (i₂ ∘ i₁))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/- | |
Copyright (c) 2014 Microsoft Corporation. All rights reserved. | |
Released under Apache 2.0 license as described in the file LICENSE. | |
Module: algebra.binary | |
Authors: Leonardo de Moura, Jeremy Avigad | |
General properties of binary operations. | |
-/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Hinflug : 292$ [2] | |
Hostel LA : 26,90$/Nacht (10-Bett-Zimmer) | |
Greyhound : 60$ | |
Hostel SF : 28$/Nacht (4-Bett-Zimmer) | |
Rückflug : 206$ [1] | |
[1] http://www.skyscanner.com/transport/flights/sfo/pit/141228/airfares-from-san-francisco-international-to-pittsburgh-int-l-apt.-in-december-2014.html?rtn=0 | |
[2] http://www.skyscanner.com/transport/flights/pit/lax/141220/airfares-from-pittsburgh-int-l-apt.-to-los-angeles-international-in-december-2014.html?rtn=0 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import hott.path | |
set_option pp.universes true | |
variables (A : Type.{3}) (a b : A) (B : Type.{1}) | |
check (path (path a b) B) --works | |
check (path (path a b) A) --type mismatch |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# OPTIONS --type-in-type --without-K #-} | |
module HoTT where | |
U = Set4 | |
data Zero : U where | |
data One : U where | |
star : One |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
lemma remdups_adj_obtain_adjacency: | |
assumes "i + 1 < length (remdups_adj xs)" "length xs > 0" | |
obtains j where "j + 1 < length xs" | |
"(remdups_adj xs) ! i = xs ! j" "(remdups_adj xs) ! (i + 1) = xs ! (j + 1)" | |
using assms proof (induction xs arbitrary: i thesis) | |
case Nil | |
hence False by (metis length_greater_0_conv) | |
thus thesis.. | |
next | |
case (Cons x xs) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
lemma remdups_adj_distinction: | |
assumes "length xs > 0" | |
shows "⋀i. i + 1 < length (remdups_adj xs) ⟹ (remdups_adj xs) ! i ≠ (remdups_adj xs) ! (i + 1)" | |
using assms proof (induction xs) | |
case Nil | |
hence "False" by simp | |
thus "remdups_adj [] ! i ≠ remdups_adj [] ! (i + 1)".. | |
next | |
case (Cons x xs) | |
hence "xs ≠ []" by (metis Divides.div_less Suc_eq_plus1 Zero_not_Suc div_eq_dividend_iff list.size(3,4) plus_nat.add_0 remdups_adj.simps(2)) |