Homotopies for Free!
Taichi Uemura
https://arxiv.org/pdf/1701.07937.pdf

glue :
 {Γ : Set}
 {Φ : Γ → Cof}
 {A : res Γ Φ → Set}
 {B : Γ → Set}
 (f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
 → ---------------
 (xu : res Γ Φ) → A xu → Glue Φ A B f (fst xu)
glue {Γ} {Φ} {A} {B} f (x , u) a = ((λ v → moveA v a) , (f x u a , (λ v → cong (λ{(u , a) → f x u a}) (symm (moveMove v))))) where
 moveA : (v : [ Φ x ]) → A (x , u) → A (x , v)
 moveA v = subst (λ v → A (x , v)) (eq (fst (Φ x)))
 moveMove : (v : [ Φ x ]) → (u , a) ≡ (v , moveA v a)
 moveMove v = Σext (eq (fst (Φ x))) refl

Glue :
 {Γ : Set}
 (Φ : Γ → Cof)
 (A : res Γ Φ → Set)
 (B : Γ → Set)
 (f : (x : Γ)(u : [ Φ x ]) → A (x , u) → B x)
 → ---------------
 Γ → Set
Glue Φ A B f x = Σ a ∈ ((u : [ Φ x ]) → A (x , u)) , ⟦ b ∈ (B x) ∣ All u ∈ [ Φ x ] , f x u (a u) ≈ b ⟧

Cohen-Coquand-Huber-Mörtberg (CCHM) Fibrations

у этого есть имя!

Функтор курильщика

functor (F: U -> U): U
   = (fmap: (A B: U) -> (A -> B) -> F A -> F B)
   * (id: (A: U) -> (x: F A) -> Path (F A) (fmap A A (idfun A) x) x)
   * (compose: (A B C: U) (f: B -> C) (g: A -> B) (x: F A) ->
     Path (F C) (fmap A C (o A B C f g) x)
                ((o (F A) (F B) (F C) (fmap B C f) (fmap A B g)) x)) * Unit

Функтор здорового человека

functor_: U = (F: U -> U) * ((A B:U) -> (A->B) -> F A -> F B)

isFunctor (F: functor_): U
   = (id: (A: U) -> (x: F.1 A) -> Path (F.1 A) (F.2 A A (idfun A) x) x)
   * (compose: (A B C: U) (f: B -> C) (g: A -> B) (x: F.1 A) ->
     Path (F.1 C)     (F.2 A C (o A B C f g) x)
      ((o (F.1 A)     (F.1 B)  (F.1 C)
          (F.2 B C f) (F.2 A B g)) x)) * Unit

FUNCTOR: U = (f: functor_) * isFunctor f

-- ap(pure(id),x) = id(x)
-- ap(pure(f),pure(x)) = pure(f(x))
-- ap(ap(ap(pure(o),u),v),w) = ap(u,ap(v,w))
-- ap(u,pure(y)) == ap(pure(\f.f(y)),u)

isApplicative (F: applicative_): U
   = (id:  (A:U) -> (x: F.1 A) ->
      Path (F.1 A) x ((ap F) A A ((pure F) (id A) (idfun A)) x))
   * (hom: (A B:U)(f:A->B)(x: A) ->
      Path (F.1 B) ((pure F) B (f x)) ((ap F) A B ((pure F) (A->B) f) ((pure F) A x)))
   * (cmp: (A B C:U)(v: F.1(A->B))(u:F.1(B->C))(w:F.1 A) ->
      Path (F.1 C) ((ap F) B C u ((ap F) A B v w))
                   ((ap F) A C ((ap F) (A->B) (A->C) ((ap F)(B->C)((A->B)->(A->C))
                   ((pure F) (ot A B C) (o A B C)) u) v) w))
   * (xchg: (A B:U)(x:A)(u:F.1(A->B))(f:A->B) ->
      Path (F.1 B) ((ap F) A B u ((pure F) A x))
                   ((ap F) (A->B) B ((pure F) ((A->B)->B) (\(f:A->B)->f(x))) u))
   * Unit

кто монаду как Домашнее Задание написать хочет?

FUNCTOR:     U = (f: functor_) * isFunctor f
APPLICATIVE: U = (f: applicative_) * (_: isFunctor (f.1,amap f)) * isApplicative f

смотрите control.ctt

MONAD: U = (f: monad_)
               * (_: isFunctor (f.1,f.2.2.1))
               * (_: isApplicative (f.1,f.2.1,f.2.2.1,f.2.2.2.1))
               * isMonad f

pure_sig      (F:U->U):U=   (A: U) ->           A  -> F A
extract_sig   (F:U->U):U=   (A: U) ->         F A  ->   A
extend_sig   (F:U->U):U= (A B: U) ->    (F A -> B) -> F A -> F B
apply_sig     (F:U->U):U= (A B: U) ->   F (A -> B) -> F A -> F B
fmap_sig      (F:U->U):U= (A B: U) ->     (A -> B) -> F A -> F B
unmap_sig     (F:U->U):U= (A B: U) -> (F A -> F B) ->  (A -> B)
contra_sig    (F:U->U):U= (A B: U) ->     (B -> A) -> F A -> F B
uncontra_sig  (F:U->U):U= (A B: U) -> (F A -> F B) ->  (B -> A)
cofmap_sig    (F:U->U):U= (A B: U) ->     (B -> A) -> F B -> F A
uncofmap_sig  (F:U->U):U= (A B: U) -> (F B -> F A) ->  (B -> A)
cocontra_sig  (F:U->U):U= (A B: U) ->     (A -> B) -> F B -> F A
uncoco_sig    (F:U->U):U= (A B: U) -> (F B -> F A) ->  (A -> B)
join_sig      (F:U->U):U=   (A: U) ->      F (F A) -> F A
dup_sig       (F:U->U):U=   (A: U) ->         F A  -> F (F A)
bind_sig      (F:U->U):U= (A B: U) ->    F A ->(A  -> F B)-> F B

что потерял?