Skip to content

Instantly share code, notes, and snippets.

View `is_symmetric_smul (units ℤ) N₁` trace
This file has been truncated, but you can view the full file.
[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))
View rel_contr.hlean
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)
@javra
javra / cases.hlean
Created Mar 11, 2015
cases producing metavariables
View cases.hlean
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₃}
@javra
javra / decl.hlean
Last active Aug 29, 2015
draft for dbl category
View decl.hlean
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₁)))
@javra
javra / binary.lean
Created Nov 29, 2014
binary.lean for arbitrary groupoid-like structures
View binary.lean
/-
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.
-/
@javra
javra / california
Created Nov 20, 2014
Hostel California
View california
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
@javra
javra / universe_test.lean
Created Nov 14, 2014
paths only live in Type.{1}...
View universe_test.lean
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
@javra
javra / HoTT.agda
Created Oct 8, 2014
hott book formalized in agda..
View HoTT.agda
{-# OPTIONS --type-in-type --without-K #-}
module HoTT where
U = Set4
data Zero : U where
data One : U where
star : One
@javra
javra / remdups_adj another lemma
Created Aug 25, 2014
remdups_adj another lemma
View remdups_adj another lemma
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)
View gist:68c7f852a060d7cb6036
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))