javra

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))

javra

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)

javra

{-# OPTIONS --type-in-type --without-K #-}

module HoTT where

U = Set4

data Zero : U where

data One : U where
  star : One

javra

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

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

/-
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

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

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

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

[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