worm precategory

gistfile1.txt

import algebra.precategory.basic algebra.precategory.morphism
open precategory morphism truncation eq sigma sigma.ops unit

context
parameter {D₀ : Type}
parameter (C  : precategory D₀)
parameter (D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type)
reducible compose

definition comp₁_type : Type :=
  Π ⦃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₁))

definition ID₁_type : Type :=
  Π ⦃a b : D₀⦄ (f : hom a b), D₂ f f (ID a) (ID b)

definition assoc₁_type (comp₁ : comp₁_type) : Type :=
  Π ⦃a b c₁ d₁ 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₂⦄
    ⦃g₃ : hom c₃ d₃⦄ ⦃h₃ : hom c₂ c₃⦄ ⦃i₃ : hom d₂ d₃⦄
    (w : D₂ g₂ g₃ h₃ i₃) (v : D₂ g₁ g₂ h₂ i₂) (u : D₂ f g₁ h₁ i₁),
    transport _ (assoc i₃ i₂ i₁)
      (transport _ (assoc h₃ h₂ h₁)
        (comp₁ w (comp₁ v u))) = (comp₁ (comp₁ w v) u)

definition id_left₁_type (comp₁ : comp₁_type) (ID₁ : ID₁_type) : Type :=
  Π ⦃a b c d : D₀⦄
    ⦃f : hom a b⦄ ⦃g : hom c d⦄ ⦃h : hom a c⦄ ⦃i : hom b d⦄
    (u : D₂ f g h i),
    transport _ (id_left i)
      (transport _ (id_left h)
        (comp₁ (ID₁ g) u)) = u

definition id_right₁_type (comp₁ : comp₁_type) (ID₁ : ID₁_type) : Type :=
  Π ⦃a b c d : D₀⦄
    ⦃f : hom a b⦄ ⦃g : hom c d⦄ ⦃h : hom a c⦄ ⦃i : hom b d⦄
    (u : D₂ f g h i),
    transport _ (id_right i)
      (transport _ (id_right h)
        (comp₁ u (ID₁ f))) = u

definition homH'_type : Type :=
  Π ⦃a b c d : D₀⦄ ⦃f : hom a b⦄ ⦃g : hom c d⦄ ⦃h : hom a c⦄ ⦃i : hom b d⦄,
    is_hset (D₂ f g h i)

structure worm_precat [class] : Type :=
  (comp₁     : comp₁_type)
  (ID₁       : ID₁_type)
  (assoc₁    : assoc₁_type comp₁)
  (id_left₁  : id_left₁_type comp₁ ID₁)
  (id_right₁ : id_right₁_type comp₁ ID₁)
  (homH'     : homH'_type)
end